# 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`.

| 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. |