7 · Certificates¶

A certificate is the part of a verdict you can hand to someone who does not trust us. It records why the equations of a question have no solution, in steps simple enough to check with a page of code. This chapter says what a certificate proves and what it does not, how one is built, the two ways to replay one and which question each answers, and how to cite one.

What a certificate proves¶

A certificate comes with an UNSAT verdict: the obligation holds. It establishes that the equations it starts from, its premises, have no common solution. The premises are the compiled policy, the question's pins, any patch, and nothing else: every other starting point in the document is flagged as something asserted rather than derived, and the procedure that asserted it is named.

Under the fast profile there is no certificate at all; under patch and proof there is (chapter 10). A repair always carries one of its own: the certificate that the policy plus that repair rules the outcome out (chapter 8).

What it does not prove¶

A certificate establishes a derivation, not that its premises are your policy. Checking it shows that the equations it starts from have no common solution. It does not show that those equations are a faithful compilation of your policy file: a compiler defect that dropped a rule would produce premises that are consistent with each other and wrong about your policy, and the certificate would check. The certificate names the policy it was compiled from, with its SHA-256, so the file can be compiled again and compared; doing that is a second step, which the certificate does not carry.

And it proves nothing about a question you did not ask. It is a certificate for one obligation, under its pins (chapter 4). No checker's report says, and no reader may conclude from one, that a policy is safe.

How a certificate is built¶

Each step the algebraic engine takes to eliminate the impossible is a row operation over the two values 0 and 1, and the engine records where every row it relies on came from. That record is a directed acyclic graph of three kinds of step:

INSERT brings in a premise: one equation of the system, quoted as it is.
ADD adds two earlier rows: their terms are combined, and a term in both cancels.
MULTIPLY multiplies an earlier row by one variable.

When the engine finds the contradiction, the row that says 0 = 1, it writes out that row's ancestry and nothing else, in depth-first post-order, so every row a step uses appears before the step. A certificate is therefore small: tens of steps for a policy of realistic size, an object a reviewer can read rather than one only a machine can audit.

The last step is withheld on purpose. The certificate's operations stop one step short of the contradiction, and the step that completes it is given separately as final_step. Replaying operations must not produce 0 = 1; applying final_step must. So whoever checks a certificate produces the contradiction themselves, rather than being shown it.

That shape is the asymmetry the whole product rests on: finding the derivation was expensive, and checking it is cheap. Each step is the sum of two sparse rows or one row times a variable, with no search, no heuristics and no solver. That is why we can hand the checking away without handing the engine away.

The two kinds, and what each can be checked by¶

certificate_type says which part of the engine refuted the system, and origin_class says how the refutation can be checked:

`certificate_type`	`origin_class`	`status`	Checked by
`algebraic`	`derived`	`verified_unsat`	replay: run `operations`, apply `final_step`, reach `0 = 1`
`algebraic`	`exhaustion`	`verified_unsat`	the refutation record: the engine reduced the question to a finite set of candidate solutions, proved the set complete, and showed every candidate fails
`phase0`	`external_proof`	`proof_unsat`	a proof checker: the SAT solver's FRAT proof, checked by `frat-rs`, over a CNF the reference checker decodes back to the equations
`phase0`	`external_oracle`	`oracle_unsat`	nothing in the document: the SAT solver asserted it, and confirming it means running a solver again

Three fields say what kind of claim the document makes, and a careful reader reads them before anything else:

self_contained is true where the document alone settles it: nothing external was asserted, every premise is legible, and an exhaustion's record is complete. false is honest, not a failure.
oracle_dependent is true where the refutation rests on an external decision procedure, the SAT solver. It is reported beside the certificate, on the verdict, so it is there even for a run that built no certificate.
origin_class says which of the four rows above the document is. An oracle-dependent refutation cannot be replayed step by step: operations is empty and final_step is the oracle's assertion.

A FRAT proof of a Phase 0 refutation: `external_proof`¶

Under the default profiles, a refutation the SAT solver reaches is its assertion. Ask for frat_proof on a guardrail or batch job and, for each refutation Phase 0 decides, the SAT solver is run again with proof logging on, and two files come back as proof artefacts: the CNF it refuted and a FRAT log of the refutation. The certificate's proof_log names both, with their SHA-256 digests.

What that proof establishes is that the CNF has no satisfying assignment. What ties the CNF to your equations is the encoding check: the CNF the solver was given decodes, clause by clause, back to the equations the certificate carries as phase0_system, and the reference checker performs that decode itself. With both, the trust in the oracle is replaced by trust in two checkers you can run: the reference checker for the decode, and frat-rs for the proof. frat-rs therefore joins what a reader trusts. The class is not derived, because the three steps of a replay cannot express clause resolution: it is a fourth class, and self_contained stays false.

result = client.verify_guardrail("transfers.co", "execute_transfer_funds", "is_authenticated",
                                 profile="proof", frat_proof=True)
print(result.status, result.verdict["origin_class"])
for artefact in result.artifacts:
    if artefact.role in ("certificate", "proof"):
        print(artefact.role, artefact.filename)
        artefact.save(artefact.filename)       # checked against its digest as it is written

The proof costs nothing unless you ask for it. Asked for, it adds a second solve of a refutation Phase 0 already reached; on the reference refutations that is milliseconds, and the files are kilobytes, but that is not a bound (chapter 10). Where the service discards a proof, because it failed the worker's own frat-rs check or would exceed the key's max_proof_bytes, the certificate goes back to external_oracle and oracle_unsat, and says why in proof_log_omitted.

The provenance blocks¶

Every certificate carries three blocks that say what its premises rest on. They take no part in checking, and they are keyed on variable indices (x12), never on names:

provenance: which system of record asserts each control the refutation cites, where the deployment declared them, and every control nobody declared, under undeclared;
control_integrity: whether a requester's own words can reach a control through a classifier, which would let the person the control protects against set it;
detection: whether the obligation depends on a detector recognising something, and if so the bound on how often a misclassification could let the action through, with the corpus that bound was measured on.

Each block lists its own limits in the document. A declared source can be false; a resolver can launder an argument into a reading; a detection bound is only as good as its corpus.

Checking a certificate yourself¶

There are two replay paths, and they answer different questions.

	The reference checker	The service's replay
The question it answers	can I confirm this without trusting the vendor?	does this certificate replay in the product I am running?
What you trust	your own reading of one short file, or your own implementation of the specification	our service
What it needs	Python, one file, no key, no network	a key, and the `replay_certificate` mode
What it handles	the certificates a policy produces	any certificate the engine emits
What it reports	the outcome and its reason	the outcome, with the engine's own conformance diagnostics in full
Reach for it when	you are a second line, an auditor, or were handed a certificate and nothing else	you operate the service and want to know a run's artefact is sound

Neither replaces the other. A replay performed by our service is not independent verification: it establishes that our software agrees with itself. That is useful to an operator and worthless to an auditor, and a team that confuses the two has not done an audit.

The reference checker¶

The reference checker is one Python file, standard library only, under the MIT licence, published with its digest. It reports one of three outcomes, verified, not_self_contained or failed, and exits 0, 2 or 1 to match:

$ python qls-check.py FCA-01a/patch.certificate.json
qls-check: verified
replayed 105 operation(s), and the withheld final step yields 0 = 1
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
0

$ python qls-check.py FCA-01a/proof.certificate.json
qls-check: not_self_contained
the contradiction rests on rows asserted by cryptominisat-phase0, which nothing in the certificate checks
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
2

The same file is carried in the stalwart-agents package, as stalwart check certificate.json, which needs no key; stalwart check --print-source writes it out to compare with the published one. To build your own checker instead, the certificate specification is normative and complete, and the corpus gives you certificates to test it on, each with the outcome a correct checker reports.

The service's replay¶

The replay_certificate mode replays a certificate you hold, or one of your artefacts by its id, with the engine's own replayer. replay is replayed, failed or out_of_scope: out of scope is a sound refutation of a kind replay does not check (an exhaustion, or an oracle's assertion), not an error.

replayed = client.replay_certificate("certificate.json")
print(replayed.replay)                   # replayed, failed or out_of_scope

checked = check_certificate("certificate.json")   # the reference checker, here, offline
print(checked.outcome, checked.reason)

Conformance is not replay¶

Two separate checks are made of a certificate, and passing one does not imply the other:

Conformance is the document's format: every INSERT without an equation is flagged as asserted, certificate_type agrees with final_step, a derived document rests on no asserted row, and no equation in a self-contained document holds a column nobody can decode. A schema-valid certificate can still fail to replay.
Replay is the arithmetic: the operations, then the final step, reach 0 = 1. A certificate can replay and still declare self_contained: false, because it rests on something asserted.

Both checkers make both checks, and report them separately. Both produce a green result, which is why conflating them is the misreading most worth guarding against.

Citing a certificate¶

A certificate stays checkable by someone who was not there, so cite what lets them check it:

the job id and the artefact id it was downloaded from, and its SHA-256 (the artefact record carries it, and the download is verified against it in flight);
the policy file it names and that file's SHA-256, which the certificate records under policy;
the question: the action, the context and every pin, all recorded under question;
the profile, from the job's run block.

Two runs of the same question can produce different certificates, with different step counts: the engine's search is parallel and finds whichever valid derivation it reaches first. That is not a discrepancy. Each certificate is a valid proof of the same fact, checkable on its own terms, and the question an auditor asks is whether the one you filed checks, not whether a new run reproduces it byte for byte.

The limits¶

A certificate establishes that its premises have no common solution, not that the premises are your policy.
It proves one obligation, under its pins, and nothing about any other question.
self_contained: false means the document alone does not settle it: an oracle's assertion is trusted, or, for external_proof, frat-rs is.
A replay by our service is not independent verification.
Conformance and replay are separate checks; passing one does not imply the other.