equiv_receipt

equiv-receipt — portable, independently re-derivable logic-equivalence receipts.

FORMAT = 'equiv-receipt/1'
class ReceiptError(builtins.Exception):

Raised when a receipt fails verification.

def prove_equivalence( build_a, build_b, inputs: Sequence[str], *, name_a: str = 'circuit_a', name_b: str = 'circuit_b', seed: int = 1, max_depth: int = 60, refute=None) -> Dict:

Build a miter, refute it, and return an EQUIV-1 receipt.

UNSAT of the miter means the circuits are equivalent; a satisfying assignment is a concrete input on which they differ, and is bound into the receipt.

refute defaults to the bundled demonstration solver. Pass equiv_receipt.solver.refute() to use an external one — the receipt is unchanged in kind, because the solver was never trusted: its proof is re-checked here and again by every reader.

def build_receipt( *, verdict: str, description_a: str, description_b: str, encoder_id: str, cnf_text: str, drat_text: str = '', counterexample: Optional[Dict] = None, seed: int = 1, meta: Optional[Dict] = None) -> Dict:

Assemble an EQUIV-1 receipt.

verdict is "EQUIVALENT" or "COUNTEREXAMPLE". The verdict is recorded but re-derived by verify_receipt(); recording it is a convenience, never a basis for acceptance.

def verify_receipt(receipt: Dict) -> Dict:

Re-derive the verdict and the commitments. Returns a result dict.

Checks, in order: format; chain integrity; commitment root over the payload; and — the one that matters — the verdict, re-derived by running the RUP checker over the committed formula and proof, or by re-simulating the committed counterexample.

def write_receipt(path, receipt: Dict) -> pathlib.Path:
def read_receipt(path) -> Dict:
def canon(obj: Any) -> bytes:
def forward_rup_check(clauses: Sequence[List[int]], drat_text: str) -> dict:

Verify a DRAT refutation by forward RUP checking.

Returns a dict with verified, n_lemmas, and — on failure — the failed_lemma and its zero-based failed_index so the defect is locatable rather than merely reported.

A refutation is accepted when an empty clause is derived, or when the final active set propagates to a conflict with no assumptions.

def parse_drat(drat_text: str) -> List[Tuple[str, List[int]]]:

Parse DRAT into ("a"|"d", clause) steps. Comment lines (c) are skipped.

Raises MalformedProof on unparseable input. Callers that must not crash should use forward_rup_check(), which converts this into a rejection — an unreadable proof proves nothing, which is a verdict, not an error condition.

def bcp( clauses: Sequence[List[int]], assumed: Sequence[int]) -> Tuple[bool, Dict[int, bool]]:

Unit propagation. Returns (conflict, assignment).

conflict is True when propagation derives a contradiction.

class ClauseDB:

A clause store with two watched literals per clause.

The naive checker re-scans every active clause on every propagation round, and the active set grows by one on every lemma — so the cost of checking a proof grows worse than the product of its two dimensions. Watching two literals per clause means a clause is only visited when one of the two literals it is watching becomes false, which is what makes long proofs checkable.

The watch invariant survives between calls because every call propagates from an empty assignment and undoes nothing: there is no backtracking to invalidate.

ClauseDB(clauses: Sequence[List[int]] = ())
cl: List[List[int]]
watch: Dict[int, List[int]]
units: List[int]
deleted: set
index: Dict[Tuple[int, ...], List[int]]
has_empty
def add(self, lits: Sequence[int]) -> int:
def delete(self, lits: Sequence[int]) -> bool:

Mark one clause with exactly these literals deleted. False if absent.

Deletion is lazy: the index entry is dropped and the clause is added to a deleted set that propagation skips. Removing it from its two watch lists eagerly would cost more than skipping it.

def live(self):

The currently active clauses, in insertion order.

def propagate(self, assumed: Sequence[int]) -> Tuple[bool, Dict[int, bool]]:

Unit propagation from assumed. Returns (conflict, assignment).

Semantics are identical to bcp(); only the cost differs.

Truth is tracked as a set of true literals rather than a variable-to-bool map. "Is this literal true" becomes one set lookup and "is it false" becomes one on its negation, which removes an abs() and a second lookup from the innermost loop — measurably the hottest path in the file.

def refute(clauses: Sequence[List[int]], *, max_depth: int = 60) -> dict:

Search for a refutation, emitting DRAT lemmas.

Returns {"unsat": bool, "drat": str, "n_lemmas": int, "model": dict|None}. When unsat is False a satisfying assignment is returned instead — for a miter that is a counterexample: the two circuits differ on it.

def miter( build_a, build_b, inputs: Sequence[str]) -> Tuple[List[List[int]], Netlist]:

Build a miter CNF for two single-output circuit builders.

build_a(net, prefix) -> output_signal_name. The returned CNF is satisfiable iff the two circuits differ on some input assignment; therefore UNSAT means equivalent.

class Netlist:

A tiny combinational netlist over AND / OR / NOT / XOR gates.

Inputs are named; every gate produces a new named signal. Deliberately minimal — this exists so the package is usable and testable without a synthesis tool, not to replace one.

Netlist(inputs: Sequence[str])
inputs
def var(self, name: str) -> int:
def NOT(self, out: str, a: str) -> str:
def AND(self, out: str, a: str, b: str) -> str:
def OR(self, out: str, a: str, b: str) -> str:
def XOR(self, out: str, a: str, b: str) -> str:
def BUF(self, out: str, a: str) -> str:

An alias. Needed when a signal must be renamed rather than computed.

def CONST(self, out: str, value: bool) -> str:

A signal pinned to a constant, as a unit clause.

Sequential unrolling needs it for latch reset values; combinational use does not.

clauses: List[List[int]]
def n_vars(self) -> int:
def parse_dimacs(text: str, *, strict: bool = True) -> List[List[int]]:

Parse DIMACS CNF.

With strict=True (the default) a malformed header, a non-integer token, or an unterminated final clause raises CNFParseError. Silently returning a partial or empty clause list would let a caller reason confidently about a formula that is not the one on disk — the worst failure mode available to a proof checker.

Pass strict=False for the older lenient behaviour.

def to_dimacs(clauses: Sequence[List[int]]) -> str:

Serialize to DIMACS with a correct header.

The byte-level output is deterministic: this is what a receipt commits to, so an unstable serializer would make receipts unverifiable.

def prove_sequential_equivalence( a: Dict, b: Dict, *, k: int = 1, refute=None, name_a: str = 'A', name_b: str = 'B', seed: int = 1) -> Dict:

Prove a and b sequentially equivalent, or find a counterexample.

refute(clauses) -> {"unsat", "drat", "model"}; defaults to the bundled solver. Pass equiv_receipt.solver.refute() for a real one.

Two arguments are attempted, in this order, and the receipt records which one carried the result:

  1. Register correspondence — the stronger invariant "corresponding latches hold equal values". Three obligations: it holds at reset, it is preserved by one step, and it implies equal outputs. When it goes through, one step of induction settles every time, which is why it is tried first.
  2. k-induction on outputs — the general argument, for designs whose state encodings do not correspond.

Base cases from the reset state are always run first, because a failure there is a real counterexample rather than an artefact of an unreachable assumed state.

def verify_seq_receipt(receipt: Dict) -> Dict:

Re-derive a sequential receipt from scratch. Never reads the verdict.

Four things are checked, and the third is the one a combinational receipt cannot do: the CNF of every obligation is re-encoded from the committed design and compared, so the formula is proven to be the circuits.

def write_seq_receipt(path, receipt: Dict):
def read_seq_receipt(path) -> Dict:
def emit(res: Dict, fmt: str, **kw) -> str:
def to_json(res: Dict, source: str = 'receipt') -> str:
def to_jsonl(res: Dict, source: str = 'receipt') -> str:
def to_sarif(res: Dict, source: str = 'receipt') -> str:
def to_junit(res: Dict, source: str = 'receipt') -> str:
__version__ = '1.0.0'