19 · The certificate specification

This chapter is the normative specification of the certificate format, in enough detail to implement a checker without our software. It is the document the API publishes at api.stalwart.it/certificate-spec, generated from the same conformance definition the engine checks every certificate it writes against, so the two cannot differ. Chapter 7 explains what a certificate means; this chapter states how to read one.

The reference checker, one file under the MIT licence, is published beside it at api.stalwart.it/downloads/qls-check.py, with its digest at qls-check.py.sha256. The certificate corpus gives real certificates to test a checker on, each with the outcome a correct one reports.

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.

Path	Type	Required	Meaning
format_version	integer	yes	The format's version, first in the document so a reader can decide whether it understands the rest before reading it. This specification describes version 1; a document without the field is version 1, and a reader MUST refuse a version it does not know rather than read it.
certificate_type	string	yes	phase0 or algebraic: which kind of refutation this is, and so which check applies. phase0 is Phase 0's SAT solver refuting the CNF encoding of the system, checked through proof_log and the CNF decode. algebraic is everything Phases 1 to 3 conclude over GF(2): a derivation to 0 = 1, or an exhaustion with its refutation record. Present on every certificate, second after format_version.
status	string	yes	Who stands behind the contradiction: verified_unsat where this tool produced it (origin_class derived or exhaustion), proof_unsat where Phase 0's SAT solver asserted it and proof_log attaches a proof a named checker confirms (external_proof), oracle_unsat where an external decision procedure asserted it and nothing attached can confirm it (external_oracle). Always agrees with origin_class, which is the finer discriminator.
detail	string	yes	Always full: the certificate carries its whole derivation. A run that builds no certificate writes none rather than a partial one.
origin_class	string	yes	How the contradiction came to be: derived, exhaustion, external_oracle or external_proof. It decides how the document is checked, and what a reader may conclude from it; see the honesty fields.
origin_class=derived	value	no	Every row was derived from the premises, and replaying operations then final_step reaches 0 = 1. A reader may conclude the derivation is valid; a reader MUST NOT conclude that the premises are the policy, which needs the circuit re-derived and compared.
origin_class=exhaustion	value	no	The contradiction is concluded from an exhausted candidate set, and the refutation record proves the exhaustion: border relations derived from the premises bound the variety by the normal set, and every point of that bound falsifies a premise. Checked by the refutation record, not by replay to 0 = 1.
origin_class=external_oracle	value	no	The contradiction rests on rows an external decision procedure asserted, named in oracle_dependencies. Nothing in the document lets a third party check that part; a reader MUST NOT treat it as a proof.
origin_class=external_proof	value	no	The refutation was asserted by Phase 0's SAT solver and a proof of it is attached: proof_log names the CNF and the FRAT log, which frat-rs elaborates to LRAT and checks. Not replayable here, and checkable by a named external checker.
self_contained	boolean	yes	Whether the document alone suffices to check it: nothing external was asserted, every leaf renders in named variables, and an exhaustion's record is complete. False is honest about a step that could not be derived; a reader MUST NOT read false as failure, nor true as a statement about the policy.
note	string	no	A sentence stating the weaker claim the document makes where a row was asserted rather than derived: by an external procedure, or by this tool with or without a refutation record.
policy	object	no	What was proved about: the policy file, its digest, the parse diagnostics and the unroll depth. Present where the run read a policy.
policy.file	string	yes	The policy file's name as the run was given it.
policy.sha256	string	no	The SHA-256 of the policy file's bytes, so the certificate can be tied to the reviewed file.
policy.parse_diagnostics	integer	yes	How many parse diagnostics the run reported. Non-zero means the circuit may lack edges the file describes.
policy.unroll_depth	array	yes	The unroll depth of each loop the compiler expanded, in order: the bound the proof holds within.
policy.unroll_depth[]	integer	yes	One loop's unroll depth, as the compiler used it.
question	object	no	The question refuted: the action, the obligation's context and every pin. A guardrail certificate refutes the policy together with these, and a pin quietly added would turn a finding into a pass.
question.action	string	no	The action whose obligation was asked about.
question.obligation_context	string	no	The context the action must not fire without, held false by the question.
question.pins	array	yes	Every value the question held fixed, the attack's and the caller's alike.
question.pins[]	object	yes	One pinned value, with the variable it fixes.
question.pins[].name	string	yes	The pinned value's name as the policy writes it.
question.pins[].variable	integer	yes	The variable index the pin fixes.
question.pins[].value	integer	yes	The value it is fixed to: 0 or 1.
question.pins[].source	string	yes	Where the pin came from: the question itself, or a caller's conditioning pin.
variables	object	no	A name for every variable the operations cite, keyed by its index (x12), closed under the definitions of the variables the compiler invented. A rendering for a reader; replay does not read it.
variables.<variable>	object	yes	One cited variable, and what names it.
variables.<variable>.kind	string	yes	What the variable is in the compiled policy: an input the policy reads, an action, a context, or a wire the compiler introduced.
variables.<variable>.subkind	string	no	A finer kind, where the compiler records one.
variables.<variable>.name	string	no	The name the policy gives it, where it has one.
variables.<variable>.qualified	boolean	no	True where the name was qualified to tell two declarations of one identifier apart.
variables.<variable>.colang	object	no	Where in the policy the variable is declared.
variables.<variable>.colang.file	string	yes	The policy file the line is in, as the run named it.
variables.<variable>.colang.flow	string	no	The flow the declaration sits in, where it sits in one.
variables.<variable>.colang.line	integer	yes	The line in the policy file, counted from 1.
variables.<variable>.definition	string	no	For a variable the compiler invented, the product or sum it stands for, over variable indices.
variables.<variable>.named_definition	string	no	The definition rendered over names, present wherever definition is.
variables.<variable>.derived_from	array	no	The variables the definition is over, each with an entry of its own.
variables.<variable>.derived_from[]	string	yes	One operand of the definition, as xN.
variables.<variable>.introduced_because	string	no	Why the compiler introduced the variable, in a sentence.
oracle_dependencies	array	no	The external decision procedures whose assertions the derivation rests on, each named once. Present exactly where an external oracle asserted a row.
oracle_dependencies[]	string	yes	One procedure, by the source name its rows carry.
encoding_check	object	no	Whether the CNF Phase 0 refuted decodes back to the equations it was given. Present where Phase 0 ran and an oracle is depended on.
encoding_check.held	boolean	yes	True where every auxiliary stands for the product it claims and every clause is one equation with its auxiliaries substituted.
encoding_check.equations	integer	yes	How many equations the CNF was compared against.
encoding_check.definitions	integer	yes	How many auxiliary variables the encoding introduced.
encoding_check.means	string	yes	What the check establishes, and what it leaves unchecked, in a sentence.
proof_log	object	no	The proof of a Phase 0 refutation: present exactly when origin_class is external_proof, and only where the encoding check held, since that check alone ties the CNF to these equations.
proof_log.format	string	yes	Always frat: the proof format the solver logs.
proof_log.cnf_file	string	yes	The CNF the solver refuted, by file name. Where it lives is the caller's; the digest binds it.
proof_log.cnf_sha256	string	yes	The SHA-256 of the CNF file's bytes.
proof_log.frat_file	string	yes	The FRAT log of the refutation, by file name.
proof_log.frat_sha256	string	yes	The SHA-256 of the FRAT file's bytes.
proof_log.checker	string	yes	The checker the proof is for: frat-rs, which is then part of what a reader trusts.
proof_log.elaborates_to	string	yes	Always lrat: what the checker elaborates the FRAT log to, so any LRAT checker can confirm it.
proof_log.solver	string	yes	The SAT solver and its version that wrote the log.
proof_log.tbuddy	boolean	yes	Whether the solver was built with tbuddy, which logs its Gauss-Jordan steps. Always true on a conforming document: without it the log omits steps and still looks complete.
phase0_system	array	no	The equations Phase 0 was handed, in the order the CNF encodes them: what a reader decodes proof_log's CNF back to. Present exactly where proof_log is. A document issued before the field was written carries proof_log alone and does not conform; a checker MAY read it on the reader's explicit request, tying the CNF to the document by its digest alone and saying so.
phase0_system[]	object	yes	One equation of the system Phase 0 encoded.
phase0_system[].equation	string	yes	The equation, in the equation grammar.
phase0_system[].named_equation	string	no	The same equation over names, where the run had a symbol table.
proof_log_omitted	object	no	Why a proof the run wrote was not kept. The document is then the one the run gives without the proof: no proof_log, and origin_class external_oracle.
proof_log_omitted.reason	string	yes	self_check_failed (frat-rs did not verify it, or a file was missing) or artefact_limit (keeping it would pass the key's proof size limit).
proof_log_omitted.bytes	integer	no	Under artefact_limit, the size of the proof that was not kept, CNF and FRAT together.
refutation	object	no	The proof of an exhaustion: a normal set N, a derived relation for every border monomial of N, and every point of the variety those relations cut out, each falsifying a premise. Present where origin_class is exhaustion and a record was kept.
refutation.kind	string	yes	quotient-exhaustion or candidate-verification: whether the candidates came from a Phase 3 quotient, or from Phase 2's rank leaving exactly one.
refutation.variable_count	integer	yes	The system's variable count n. Every point is an assignment to x0 .. x(n-1), and the closure is over all n variables.
refutation.candidates	integer	yes	How many candidate points the enumeration produced. A checker MUST require exactly this many points, and exactly as many as the normal set has members.
refutation.unsubstantiated	integer	no	Candidates the enumeration rejected that satisfy the system on re-checking. Where present and non-zero the record does not refute on its own.
refutation.incomplete	string	no	The sentence stating that the record lists fewer points than were rejected, and why.
refutation.closure_gap	string	no	Why the closure evidence is incomplete: a border monomial whose normal form left N, or a relation no derivation was recorded for. Where present the record does not check.
refutation.normal_set	array	yes	N, the normal set, each member a monomial spelled as a term. It MUST hold 1.
refutation.normal_set[]	string	yes	One member of N, as a term: 1, or variables joined by *.
refutation.border_relations	array	yes	One entry per border monomial of N: every product of a variable and a member of N that is not itself in N.
refutation.border_relations[]	object	yes	One border monomial, and the row of operations that reduces it over N.
refutation.border_relations[].monomial	string	yes	The border monomial, as a term.
refutation.border_relations[].operation	integer	yes	The id of the row in operations deriving the relation: the monomial plus members of N, derived from the premises.
refutation.points	array	yes	Every candidate point, none omitted and none sampled.
refutation.points[]	object	yes	One candidate point, and the premise it falsifies.
refutation.points[].index	integer	yes	The point's position in the enumeration.
refutation.points[].assignment	string	yes	The whole point: n binary digits, the i-th the value of x(i-1). Points MUST be distinct, and each MUST satisfy every border relation.
refutation.points[].falsifies	object	yes	The premise the point violates.
refutation.points[].falsifies.operation	integer	yes	The id of the premise leaf in operations. Substituting the point MUST leave it violated.
refutation.points[].falsifies.system	string	yes	S1 or S2: which half of the system the row is in.
refutation.points[].falsifies.row	integer	yes	The row's index within that half.
refutation.points[].named_assignment	object	no	The point on the falsified premise's variables, keyed by name, where the run had a symbol table. A reading aid; the checker reads assignment.
refutation.points[].named_assignment.<name>	integer	yes	One named variable's value: 0 or 1.
steps_to_contradiction	integer	yes	How many entries operations has: the derivation's length, the final step excluded.
operations	array	yes	The derivation, in depth-first post-order: every operand appears before the operation consuming it. Empty where the contradiction was asserted directly.
operations[]	object	yes	One row of the derivation: a leaf, a sum or a product.
operations[].id	integer	yes	The row's id, unique in the document; later rows name it.
operations[].op	string	yes	INSERT, ADD or MULTIPLY: a leaf, a sum of two rows, or a row times a variable.
operations[].parents	array	no	For ADD: the two rows summed, by id.
operations[].parents[]	integer	yes	One summed row's id, defined earlier in operations.
operations[].base_id	integer	no	For MULTIPLY: the row multiplied, by id.
operations[].multiplier	string	no	For MULTIPLY: the variable the row is multiplied by, as xN.
operations[].source	string	no	For INSERT: where the leaf comes from. original-S1 and original-S2 are the premises; any other source names the procedure that asserted the row, which then carries oracle or internal_assertion.
operations[].oracle	boolean	no	For INSERT: true where an external decision procedure asserted the row.
operations[].internal_assertion	boolean	no	For INSERT: true where this tool asserted the row; the refutation block is its evidence.
operations[].equation	string	no	For INSERT: the leaf, in the equation grammar. The normative form; every unasserted INSERT carries it.
operations[].named_equation	string	no	The leaf over names, where the run had a symbol table: always the same equation as equation.
operations[].reads_as	string	no	The leaf read as a sentence about the policy, where one can be said.
operations[].colang	object	no	For a leaf compiled from the policy: where in it.
operations[].colang.file	string	yes	The policy file the line is in, as the run named it.
operations[].colang.flow	string	no	The flow, where the line sits in one.
operations[].colang.line	integer	yes	The line in the policy file, counted from 1.
operations[].pin	object	no	For a leaf that is a pin: the pinned name and its value.
operations[].pin.name	string	yes	The pinned value's name as the policy writes it.
operations[].pin.value	integer	yes	The value the pin fixes it to: 0 or 1.
operations[].origin	string	no	For a leaf that is neither policy nor pin: expandability-padding, patch or negated-patch.
operations[].pivot	integer	no	The pivot bucket the row was reduced into, a trace of where the solver found it.
final_step	object or null	yes	The operation that produces 0 = 1, withheld from operations so a reader performs it: replaying operations MUST NOT reach 0 = 1, and applying this step MUST. Null where there is no derivation.
final_step.op	string	yes	ADD, MULTIPLY, or INSERT where the contradiction was asserted directly.
final_step.inputs	array	no	For ADD the two rows, for MULTIPLY the one row, by id.
final_step.inputs[]	integer	yes	One input row's id, defined in operations.
final_step.multiplier	string	no	For MULTIPLY: the variable, as xN.
final_step.source	string	no	For INSERT: the procedure that asserted 0 = 1.
final_step.oracle	boolean	no	For INSERT: true where an external decision procedure asserted it.
final_step.internal_assertion	boolean	no	For INSERT: true where this tool asserted it.
final_step.instruction	string	yes	What to do with the step, in a sentence.
provenance	object	yes	Where each control the refutation cites is asserted from: the systems of record a source manifest declares. Present on every certificate, empty where no manifest was given.
provenance.declared	boolean	yes	Whether a source manifest was supplied to the run. False means every control below is undeclared because nothing was declared, not because the manifest omitted it.
provenance.manifest_sha256	string	no	The SHA-256 of the source manifest the run read, so the declarations can be traced to the reviewed file that made them. Absent where no manifest was supplied.
provenance.controls	object	yes	The declared controls the refutation cites, keyed by the certificate's own variable index rather than by name, because one identifier can name two kinds.
provenance.controls.<variable>	object	yes	One cited control and the source the manifest says asserts it.
provenance.controls.<variable>.name	string	yes	The control's name as the policy writes it, without the leading $.
provenance.controls.<variable>.source	string	yes	The manifest's name for the source that asserts the control.
provenance.controls.<variable>.system	string	yes	The system of record the source is, as the manifest names it for a reader.
provenance.controls.<variable>.authority	string	yes	authoritative, derived or advisory: whether the source is the system of record for the value, computes it from one, or only suggests it.
provenance.controls.<variable>.model_writable	boolean	yes	Whether the model can write the value the control reads. True means the guarantee rests on a value the thing it constrains can set.
provenance.controls.<variable>.version	string	yes	header, endpoint or none: how a reading of the source is tied to a version of the record it came from.
provenance.controls.<variable>.freshness_seconds	integer	no	How old a reading may be, in seconds, where the manifest states a window.
provenance.controls.<variable>.freshness_citation	string	no	Where the freshness window comes from: the rule, contract or design document that sets it.
provenance.undeclared	array	yes	The cited controls no source in the manifest asserts, by variable index. The proof still holds; what it rests on is unattributed.
provenance.undeclared[]	string	yes	One cited control no source asserts, as xN.
provenance.limits	array	yes	What provenance cannot establish, stated on every certificate: the residuals that remain after every check, each with what bounds it.
provenance.limits[]	string	yes	One residual provenance cannot close, and what bounds it.
control_integrity	object	yes	Whether any control the refutation cites can be reached from a classifier's verdict on the requester's intent, which would let the requester's wording satisfy the guard.
control_integrity.checked	boolean	yes	Whether the question was asked for this certificate. False is not a pass: nothing was examined.
control_integrity.clean	boolean	no	Whether no cited control is reachable from an intent. Present only where the question was checked, and always the opposite of whether findings is non-empty.
control_integrity.findings	array	yes	Each cited control an intent can reach, with the path that reaches it.
control_integrity.findings[]	object	yes	One cited control an intent can reach, and how.
control_integrity.findings[].control	string	yes	The control an intent can reach.
control_integrity.findings[].intent	string	yes	The intent whose classifier verdict reaches the control.
control_integrity.findings[].path	array	yes	The wires from the intent to the control, in order, as the circuit names them.
control_integrity.findings[].path[]	string	yes	One wire on the path, as the circuit names it.
detection	object	yes	Whether the obligation rests on a classifier being right, and if so the bound on how often it is wrong.
detection.computed	boolean	yes	Whether the partition was computed for this certificate. False means the question was not asked, not that the answer was independent.
detection.dependent	boolean	no	Whether the control rests on an intent or a classifier concept. Independent means the proof holds over every classifier output, misclassifications included.
detection.atoms	array	yes	The intents and classifier concepts the control rests on, each with its calibration where it has one.
detection.atoms[]	object	yes	One intent or concept the control rests on.
detection.atoms[].name	string	yes	The intent or concept the control rests on.
detection.atoms[].kind	string	yes	intent or concept: which kind of classifier verdict the atom is.
detection.atoms[].calibrated	boolean	yes	Whether the atom carries a complete calibration: a false-negative rate, its corpus, the corpus size and when it was measured.
detection.atoms[].fn_rate	number	no	The atom's measured false-negative rate, printed so that it reads back as the same number.
detection.atoms[].corpus	string	no	The corpus the rate was measured on, as the calibration names it.
detection.atoms[].n	integer	no	How many examples the corpus held.
detection.atoms[].measured	string	no	When the rate was measured, as the calibration states it.
detection.bound	number or null	yes	The union bound over the atoms' rates: how often, per emission, a misclassification can let the action through. Null where any atom is uncalibrated, because a sum missing a term is not a bound.
detection.uncalibrated	array	yes	The atoms with no complete calibration, which are why bound is null.
detection.uncalibrated[]	string	yes	One atom with no complete calibration, by name.
residual	object	no	Where the refutation rests on classifier verdicts named by a concept manifest: the union bound on how often a misclassification lets the action through, over the atoms in this certificate's support.
residual.support	string	yes	Always certificate: the bound is over this derivation's atoms, not the whole circuit.
residual.bound	number	yes	The union bound over the atoms' residuals.
residual.bound_text	string	yes	The bound written for a reader.
residual.method	string	yes	How the bound is computed, and why it needs no independence assumption.
residual.statement	string	yes	What the bound means for this certificate, in a sentence.
residual.concepts	array	yes	The concepts the atoms belong to.
residual.concepts[]	object	yes	One concept the derivation's atoms belong to.
residual.concepts[].name	string	yes	The concept's name in the manifest.
residual.concepts[].bound_by	string	yes	decoder or classifier: what bounds the concept's error.
residual.concepts[].judge	string	yes	The judge that decides the concept.
residual.concepts[].independent	boolean	yes	Whether the concept's judge is independent of the others.
residual.concepts[].threshold	number	no	The judge's decision threshold, where it has one.
residual.concepts[].residual	number	yes	The concept's error rate, as calibrated.
residual.concepts[].counted	boolean	yes	Whether the concept's residual is a term of the bound.
residual.concepts[].calibration	object	no	Where the residual was measured.
residual.concepts[].calibration.corpus	string	yes	The corpus the residual was measured on.
residual.concepts[].calibration.n	integer	yes	How many examples the calibration corpus held.
residual.concepts[].calibration.measured	string	yes	When the residual was measured.
residual.atoms	array	yes	The classifier verdicts in the derivation's support.
residual.atoms[]	object	yes	One classifier verdict the derivation rests on.
residual.atoms[].name	string	yes	The atom's name in the concept manifest.
residual.atoms[].variable	string	yes	The variable the atom is, as xN.
residual.atoms[].concept	string	yes	The concept the atom belongs to, by name.
residual.atoms[].bound_by	string	yes	decoder or classifier: what bounds the atom's error.
residual.atoms[].judge	string	yes	The judge that decides the atom's verdict.
residual.atoms[].independent	boolean	yes	Whether its judge is independent of the others.
residual.atoms[].consulted_on	array	no	The phases that consulted the atom.
residual.atoms[].consulted_on[]	string	yes	One phase that consulted the atom, by name.
residual.atoms[].loop_iteration	integer	no	The loop iteration the atom belongs to, where it is unrolled.
residual.atoms[].chain_step	integer	no	The chain step the atom belongs to, where the question spans several.
residual.atoms[].support	array	yes	The operation ids the atom is cited in.
residual.atoms[].support[]	integer	yes	One operation id in whose leaf the atom appears.
residual.decoder_bound_residual	string	no	Where an atom is bounded by a constrained decoder, why its term is 0 rather than calibrated.