Module proof_emit 

Standard proof-trace emission — DRAT, LRAT, and DPR text from our in-memory ProofStep stream, so the certified refutations this crate produces are not merely self-checked but replayable by the SAT community’s independent (and in cake_lpr’s case formally verified) checkers.

Three formats, three trust reaches:

• DRAT (Wetzler/Heule/Hunt 2014) — clause additions and deletions, no hints. The universal interchange format; checked by drat-trim. We emit it for any refutation whose added clauses are all RUP (our plain-CDCL fallback, the BVE/vivification RUP path).
• LRAT (Cruz-Filipe et al. 2017) — DRAT plus an explicit hint chain of antecedent clause IDs per step, so the checker replays in O(hint) rather than re-searching. This is what the CakeML-verified cake_lpr consumes. We synthesise the hints by instrumenting the very same unit-propagation core the RUP checker uses (rup), then ship an independent check_lrat that re-validates them.
• DPR (Heule/Kiesl/Biere 2017) — additions carrying an assignment witness for a propagation-redundant (model-removing) clause; checked by dpr-trim. This is the format SaDiCaL emits for its positive-reduct PR clauses, and the one our SDCL path lands in.

The honesty seam. Our symmetry crusher certifies clauses with a substitution witness under the SR (substitution-redundancy) criterion — strictly stronger than the PR that dpr-trim checks (the PHP swap clause ¬x(i,h) is SR-but-not-PR). So the DPR emitter does not blindly transcribe a substitution: it try_assignment_witnesses each one — reduce to a candidate assignment, then re-verify it against pr::is_pr — and emits standard DPR only when that genuinely holds. A substitution that is irreducibly SR makes the emitter return EmitError::RequiresSubstitutionRedundancy, never a bogus PR line. Fail-closed: we would rather decline to emit than emit a proof an honest checker rejects.

Structs

SizeSink

A byte-counting write sink that measures a proof’s serialized size without materializing it: it keeps only a running length, discarding every chunk the moment its bytes are counted, and once the total would exceed cap it refuses further writes (returning core::fmt::Error, which the streaming emitters map to EmitError::SizeCapExceeded). This lets us report our own proof size on the benchmarks page in O(1) memory, and guarantees a pathological (super-linear) proof aborts early rather than exhausting RAM — the streaming, capped counterpart to emit_*(...).len().

Enums

EmitError

Why a proof could not be emitted in a requested standard format.

Functions

check_lrat

Independently verify an LRAT proof against original — the small, naive checker whose simplicity is the trust. Replays each addition’s hint chain (every hinted clause must be unit at its turn, the last must conflict) and accepts iff a line derives the empty clause. Rejects a corrupted hint, a dangling id, or a chain that fails to conflict.

emit_dpr

Emit a DPR proof: RUP additions as bare clauses, PR additions as C 0 ω 0 (witness ω re-verified and laid out pivot-first per the dpr-trim convention), deletions as d C 0. A Pr step whose witness is irreducibly SR yields EmitError::RequiresSubstitutionRedundancy.

emit_drat

Emit a DRAT proof (additions + deletions, no hints, no witnesses). Returns EmitError::PrInRupOnlyFormat if any step is a Pr step — DRAT cannot carry a PR witness; use emit_dpr for those. The trailing empty clause is appended iff it is RUP.

emit_lrat

Emit an LRAT proof: each RUP addition as <id> <clause> 0 <hints> 0, deletions as <id> d <deleted-id> 0, and a final empty-clause line. Returns EmitError::PrInRupOnlyFormat for any Pr step (LRAT proper carries no PR witness).

emit_sr

Emit our refutation in Marijn Heule’s .sr (substitution-redundancy) proof format — the input sr2drat expands into plain DRAT for drat-trim to verify. This is the pipeline that makes our marquee symmetry proofs externally machine-checkable, closing the “SR witnesses not yet exportable” gap: a Pr step carrying a Witness::Substitution no longer dead-ends at EmitError::RequiresSubstitutionRedundancy but is written as a substitution line sr2drat knows.

parse_dpr

Parse a DRAT/DPR proof body back into ProofSteps — one clause per line. A bare C 0 line is a RUP addition; C 0 ω 0 is a PR addition with an Witness::Assignment; d C 0 is a deletion. Used to round-trip our own emission through our own checker.

try_assignment_witness

Reduce a Witness to a standard PR assignment witness for clause against db, returning Some(ω) only when ω genuinely satisfies pr::is_pr — so the caller can emit a dpr-trim-checkable line — and None when the witness is irreducibly SR.

write_sr

Streaming core of emit_sr: write the SR proof into any core::fmt::Write sink rather than a String, so its serialized size can be measured through a capped SizeSink in O(1) memory (and bail early on a pathological proof) instead of building the whole text. Byte-for-byte identical to emit_sr; the String-backed wrapper above simply cannot hit EmitError::SizeCapExceeded.