The Stalwart UNSAT certificate, format version 1

Normative. © Stalwart Technologies Ltd, published under the Creative Commons Attribution 4.0 International licence (CC BY 4.0): you may copy, quote and adapt it, in a filing or anywhere else, with attribution.

Worked examples of both kinds of certificate, with the files to check them against, are at /certificates/ beside this specification.

1. Conventions

The key words MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, RECOMMENDED, MAY and OPTIONAL are to be interpreted as described in RFC 2119. This specification is normative in English.

A certificate is a JSON object that records why a system of polynomial equations over GF(2) -- the compilation of a policy together with the question asked of it -- has no solution. A checker is any program that reads a certificate and decides what it establishes. A reader is the person who acts on what a checker reports.

A certificate is found either as a document of its own or as the value of the certificate member of a larger report. A checker MUST accept both: where the top-level object has no operations member and has a certificate member that is an object, that object is the certificate.

2. What a checker may conclude

A certificate establishes that a derivation or a refutation is valid: that its premises -- the equations section 5 names -- have no common solution. It does not establish that those equations are the policy. Closing that second step needs the policy compiled again and compared, which is more than a certificate carries. A checker's report MUST NOT say, and a reader MUST NOT conclude from it, that a policy is safe.

3. Versioning

format_version is the first member of every certificate this specification describes, and its value is 1. A document without the member is version 1. A checker MUST refuse a document whose version it does not know rather than read it: a misread document checks to a confident wrong answer rather than to an error.

Adding a member is a compatible change, and the version does not move: a checker MUST ignore members it does not know. Removing a member, retyping one, or changing what one means is a breaking change, and it increases format_version.

4. The two kinds of certificate

certificate_type is the second member of every certificate, and it names which of two kinds the document is. The solver decides a system in phases, and the kind is the phase that refuted it.

• phase0. Phase 0 hands the system to a SAT solver as a CNF, and the SAT solver refuted it. The contradiction is a single asserted row, final_step is an INSERT whose source is cryptominisat-phase0, and operations is empty. What can be checked is the SAT solver's proof, where one was logged (proof_log), and that the CNF it refutes is the system (phase0_system and the CNF decode of section 13).
• algebraic. Every other refutation, reached over GF(2) by the later phases. Phase 1 multiplies the linear equations by each variable, Phase 2 expands and row-reduces the system to degree 2, and Phase 3 closes the quotient beyond degree 2 and, where a finite set of candidate solutions remains, enumerates it. Each step is an INSERT, ADD or MULTIPLY of section 6, so the certificate is a derivation from the premises, ending either in 0 = 1 (origin_class derived) or in an exhausted candidate set proved complete by the refutation record of section 12 (origin_class exhaustion).

A checker MUST read certificate_type before anything else it checks, and MUST treat a document as failed where it is neither value, or where it is phase0 and final_step is not Phase 0's asserted row, or the reverse.

5. The equation grammar, and the premises

Every equation in a certificate is a string in this grammar:

equation := terms " = " ("0" | "1")
terms    := "0" | term (" + " term)*
term     := "1" | variable ("*" variable)*
variable := "x" digits         ; no leading zero unless the variable is x0

Each term is a monomial: the product of the variables it names, over GF(2). A repeated factor is the same monomial (x1*x1 is x1), and a monomial appearing twice cancels (x1 + x1 is 0). The term 1 is the constant and moves to the right-hand side, flipping it. 0 = 1 is the contradiction; 0 = 0 holds of every assignment. Anything outside the grammar is failed. Where a field holds a single monomial rather than an equation -- the refutation record's normal set and border monomials -- it is spelled as one term.

A variable xN is the system's variable with index N. variables names them for a reader, and named_equation and reads_as render equations for a reader; a checker MUST NOT need any of them, and MUST check against equation alone.

The premises are the system's own equations: the leaves whose source is original-S1 or original-S2. They are the compiled policy, the question's pins, the patch and any padding, and the citations beside a leaf (colang, pin, origin) say which. Every other leaf MUST carry oracle: true or internal_assertion: true: it was asserted rather than derived, by the procedure its source names. A leaf from any other source that carries neither flag is a statement the document chose to make, and a checker MUST treat the document as failed -- a derivation from it would refute the system together with that statement, not the system alone.

6. The operations

operations is the derivation, as a list of rows. Each row has an id that no other row in the document has, and an op:

1. INSERT adds a leaf. Its equation is the leaf. An INSERT without an equation MUST carry oracle: true or internal_assertion: true.
2. ADD sums the two rows its parents name: the symmetric difference of their monomials, and the exclusive or of their right-hand sides.
3. MULTIPLY multiplies the row base_id names by the variable multiplier: each monomial gains the variable (unchanged where it already has it), equal monomials then cancel in pairs, and a right-hand side of 1 becomes the monomial of that variable alone, with the right-hand side then 0.

The rows are in depth-first post-order: every row a row names appears before it. A row naming a row that does not appear earlier makes the document malformed. Every row is a consequence of the leaves it descends from, so a row descending only from premises holds wherever the premises do.

7. The withheld final step

The row that produces 0 = 1 is not in operations. It is final_step, and the reader performs it. That places two obligations on a checker:

1. Executing operations MUST NOT produce 0 = 1 at any row. A document whose operations already reach the contradiction did not withhold the step, and is malformed.
2. Under derived, applying final_step to the rows operations produced MUST produce 0 = 1: the empty set of monomials with right-hand side 1. For ADD, inputs names exactly two rows; for MULTIPLY, exactly one row and a multiplier. A derived document with no final_step is failed.

A final_step whose op is INSERT is a contradiction asserted directly, by the procedure its source names: Phase 0's (phase0), an external procedure's (external_oracle), or this tool's own conclusion from an exhausted candidate set (exhaustion, carrying internal_assertion: true), which the refutation record proves.

8. The honesty fields

Four members say what kind of claim a certificate makes, and what a reader may not conclude from it.

• self_contained is true where the document alone suffices: nothing external was asserted, every leaf is legible, and an exhaustion's record is complete. False is honest, not a failure.
• status says who stands behind the contradiction: verified_unsat where this tool produced it (derived or exhaustion), proof_unsat where Phase 0's SAT solver asserted it and proof_log attaches a proof frat-rs confirms (external_proof), and oracle_unsat where an external procedure asserted it and nothing attached confirms it (external_oracle). It MUST agree with origin_class.
• oracle_dependencies names every external decision procedure an asserted row came from, each once. Present exactly where one is depended on.
• origin_class is the discriminator a checker reads after certificate_type. Its four values, and what each lets a reader conclude, are in the field reference (section 14). A derived document MUST carry no row flagged oracle or internal_assertion.

9. The provenance blocks

provenance, control_integrity and detection are present on every certificate. They say what the refutation's leaves rest on: the systems of record that assert each cited control, whether a requester's wording can reach a control through a classifier, and how often a misclassification could let the action through. They are keyed on variable indices (x12), never on names, because one identifier can name two kinds -- and because renumbering the rows' ids, which canonicalisation does, leaves variable indices intact. They take no part in checking; their fields are in section 14.

10. Checking a certificate

A checker MUST take these steps, in order, and report one of three outcomes: verified, not_self_contained or failed. failed names its reason. The step that decides ends the check.

1. Read the document as JSON, and take the certificate from it (section 1). A document that is not JSON, or holds no object, is failed.
2. Read format_version (section 3). A version other than 1 is failed.
3. Check the format invariants. Each violation is failed: certificate_type agrees with final_step (section 4); status agrees with origin_class (section 8); every INSERT without an equation is flagged as asserted (section 6); a derived document carries no asserted row (section 8); and proof_log, phase0_system and origin_class: external_proof occur together or not at all.
4. Read origin_class and go to the step it names: derived to step 5, exhaustion to step 6, external_oracle to step 7, external_proof to step 8. Any other value is failed.
5. Replay. Execute operations in order (section 6), holding each row by its id. A malformed row, a reused id, a row naming a row not yet defined, an equation outside the grammar, a leaf that is neither a premise nor flagged (section 5), or a row that is 0 = 1 is failed. Then apply final_step (section 7); a result other than 0 = 1 is failed. Otherwise the outcome is verified.
6. The refutation record. Execute operations as in step 5. final_step MUST be an INSERT carrying internal_assertion: true. Check refutation as section 12 sets out; a record that does not check is failed, and one that does is verified.
7. An external oracle. Nothing in the document checks the asserted rows. The outcome is not_self_contained, naming every entry of oracle_dependencies.
8. A proof log. Read the CNF file proof_log.cnf_file names. A missing file, a digest that is not 64 lowercase hexadecimal digits, or a file whose SHA-256 is not proof_log.cnf_sha256 is failed. Decode it (section 13) and compare it with phase0_system; any discrepancy is failed. Otherwise the outcome is not_self_contained, naming the command that checks the refutation of the CNF -- frat-rs elab <frat_file> <cnf_file> -- which the checker does not run.

A certificate issued before phase0_system was written carries proof_log without it, and fails step 3: nothing in a document says when it was issued, so a missing field cannot be told from a removed one. A checker MAY read such a document when its reader asks for it explicitly, skipping that invariant and the decode of step 8. The CNF is then tied to the document by proof_log.cnf_sha256 alone, and the outcome MUST say that nothing ties it to the equations.

A checker's report MUST state that it establishes a derivation or a refutation, not that the policy is safe (section 2).

11. Why an exhaustion refutes the system

Write I for the ideal the premises generate, in the ring of Boolean polynomials in x0 .. x(n-1) (each variable squares to itself), and V(I) for its points: the assignments satisfying every premise. The system is unsatisfiable exactly when V(I) is empty.

Phase 3 does not always reach 0 = 1 as a row. It may instead close the quotient: it finds a set N of monomials, the normal set, and for every border monomial -- a product x_i * t of a variable and a member of N that is not itself in N -- a relation of I reducing it to members of N. Write J for the ideal those relations generate. Every relation is derived from the premises, so J is contained in I and V(I) is contained in V(J).

N bounds V(J). Let S be span(N) + J. N holds 1, so S holds 1. For every member t of N and every variable x_i, x_i * t is in N or is a border monomial, which J reduces into span(N); so x_i * S is contained in S. A subspace holding 1 and closed under every variable is the whole ring, so the quotient by J is spanned by N, and its dimension is at most |N|. The quotient of the Boolean ring by J is the ring of functions on V(J), whose dimension is |V(J)|; so |V(J)| <= |N|.

The points are all of V(J). The record lists |N| distinct assignments, each satisfying every border relation, so each is a point of V(J). There are |N| of them and V(J) has at most |N| points, so they are all of V(J).

None of them is a solution. Each point falsifies a premise, so none is in V(I). V(I) is contained in V(J) and meets none of its points, so V(I) is empty.

The certificate carries every part of that argument: the border relations as rows of operations, derived from the premises; N; and the points, each citing the premise it falsifies. Nothing in it is taken on the run's word. Phase 2's rank shortcut -- the expansion leaving exactly one candidate -- is the case N = {1}: its border monomials are the n variables, and its relations fix each to the candidate's value.

12. The refutation record

A checker checks refutation in these steps; any one that does not hold is failed.

1. variable_count is a whole number n, and no row of operations names a variable at or above it. candidates is a whole number of at least 1. unsubstantiated is absent or 0, and closure_gap is absent.
2. Every member of normal_set parses as a term (section 5) over variables below n, no member appears twice, and 1 is a member. Call the set N.
3. Each entry of border_relations names a monomial that parses as a term, is not in N and is named by no other entry, and an operation that is a row of operations. That row's monomials MUST be the entry's monomial and members of N, and nothing else; its right-hand side is free, since 1 is in N.
4. For every member t of N and every variable x_i with i below n that t does not contain, x_i * t is in N or is the monomial of a border relation.
5. points lists exactly candidates entries, and candidates is |N|.
6. Each point's assignment is a string of exactly n characters, each 0 or 1, the i-th the value of x(i-1). No two points are equal.
7. Each point satisfies every border relation: the exclusive or of the relation's monomials whose variables are all 1 equals its right-hand side.
8. Each point's falsifies.operation is the id of a premise leaf (section 5), and the point does not satisfy that leaf's equation.

A record that passes all eight proves the premises have no common solution (section 11), and the outcome is verified.

13. The proof log and the CNF decode

Where Phase 0's SAT solver refuted the system and a proof was logged, proof_log names two files: the CNF the solver refuted, in DIMACS form, and the FRAT log of the refutation, which frat-rs elaborates to LRAT and checks. Their digests are 64 lowercase hexadecimal digits. The certificate's phase0_system lists the equations Phase 0 was handed, in order. Checking the refutation of the CNF is frat-rs's; tying the CNF to phase0_system is this decode's.

Phase 0 is handed equations of degree at most 2, and the encoding below names a product of two variables and no more. An equation of phase0_system with a monomial of degree 3 or more is a discrepancy.

The CNF file is DIMACS: comment lines beginning c, one p cnf <variables> <clauses> header, then the clauses, each a list of non-zero literals ended by 0. Variable v in the file is the system's variable x(v-1). A comment line c original_variables <n> gives the number of the system's own variables; every file variable above n is an auxiliary or a connector. A file without that comment, or whose clause count is not the header's, is failed.

Decode the clauses in order, as blocks:

1. A definition is three consecutive clauses (-x -y z), (x -z), (y -z), in that order, with z an auxiliary: z stands for the product of x and y. The two MUST be distinct system variables, and an auxiliary MUST NOT be defined as two different products.
2. A parity block over k variables (1 to 3), named in the same order in every clause, is the 2^(k-1) clauses that each forbid one assignment of the wrong parity: a clause negating exactly the variables set to 1 in the assignment it forbids. All its clauses negate an odd number of variables, or all an even number; the block asserts that the variables' exclusive or is 1 where the number is even, and 0 where it is odd.
3. An equation is a single parity block over one or two variables, or a chain: blocks over three variables (a, b, c1), (c1, d, c2), ..., (c_(m-1), y, c_m) of parity 0, closed by a block over two variables (c_m, z) of any parity. Each c is a connector, and the chain asserts that the exclusive or of a, b, d, ..., y, z is the closing block's parity.
4. The empty clause is the equation 0 = 1.

Anything that is none of these, a chain left open at the end of the file, a connector that is a system variable or is defined as a product or appears in more than the two blocks it joins, and a connector that is also a term of an equation, are discrepancies.

Then compare: drop every 0 = 0 from phase0_system. The decoded equations and what remains MUST be equal in number. Replace each auxiliary in the i-th decoded equation by the product it stands for; it MUST name no monomial twice, and it MUST have the same right-hand side as the i-th remaining equation and the same set of monomials, that equation's monomials taken after section 5's normalisation (repeated factors collapse, a monomial appearing twice cancels). Each difference is a discrepancy.

14. Field reference

Every member a certificate can carry. A path names a member from the certificate's top level: [] is an array's elements, <variable> a key that is a variable index (x12) and <name> a variable's name. Required means the member is present wherever its parent is -- on every certificate, for a member at the top level. The four origin_class= rows are the values of origin_class.

This specification as Markdown · Licence: CC BY 4.0