equiv_receipt.receipt

EQUIV-1 receipts — a portable, independently re-derivable equivalence verdict.

The receipt binds, into a salted hash chain: the two circuit descriptions, the identity of the encoder that produced the formula, the formula itself, and the refutation. A verifier re-runs the RUP check over the committed formula and proof and recomputes the chain. It needs nothing from the producer.

The design choice that matters: the receipt commits to the encoder identity and the formula bytes, so a verifier can detect a formula that does not correspond to the circuits it claims to. A receipt carrying only a proof would let a producer supply a valid refutation of the wrong formula.

Standard library only.

FORMAT = 'equiv-receipt/1'

DOMAIN_LEAF = b'EQUIV-leaf-v1'

DOMAIN_NODE = b'EQUIV-node-v1'

DOMAIN_SALT = b'EQUIV-salt-v1'

DOMAIN_CHAIN = b'EQUIV-chain-v1'

GENESIS = '0000000000000000000000000000000000000000000000000000000000000000'

class ReceiptError(builtins.Exception):

Raised when a receipt fails verification.

def canon(obj: Any) -> bytes:

def derive_salts(master: bytes, n: int) -> List[bytes]:

def leaf_hash(i: int, salt: bytes, blob: bytes) -> bytes:

def merkle_root(leaves: List[bytes]) -> bytes:

def chain(records: List[Dict]) -> List[Dict]:

Hash-chain a record list. Each record carries the digest of the previous.

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: