Module proof 

Shared proof-step vocabulary for the certified checkers.

A refutation is an ordered stream of clause additions, each carrying a justification a tiny independent checker can replay:

• ProofStep::Rup — the clause follows by reverse unit propagation (the DRAT/RUP unit).
• ProofStep::Pr — the clause is propagation-redundant with an explicit Witness (Heule, Kiesl & Biere, Short Proofs Without New Variables, CADE 2017). This is the only form that can certify a model-removing addition — exactly what a symmetry-breaking predicate is — so it is the seam through which certified symmetry breaking flows.

The witness may be an explicit partial Witness::Assignment or a literal Witness::Substitution (a permutation / automorphism). The substitution form is mere sugar: against a clause C whose falsifying assignment is α = ¬C, the substitution σ denotes the assignment witness ω = { ¬σ(l) : l ∈ C } — the image of the “bad” corner of the cube under the symmetry, which is the canonical PR witness for a lex-leader SBP. The checker (crate::pr) reduces every substitution to that assignment, so there is a single well-specified propagation-redundancy criterion to trust.

Structs

Perm

A literal permutation that respects negation: σ(¬l) = ¬σ(l). Represented by the image of each variable’s positive literal, so the negation invariant holds by construction.

Enums

ProofStep

One step of a refutation: add a clause with the justification a checker replays, or delete a clause from the working database (the DRAT deletion that inprocessing — vivification, BVE — relies on; deletions are unchecked, only additions carry a redundancy obligation).

Witness

A redundancy witness for a ProofStep::Pr clause.