Module reverse_module 

R5 — the SVA REVERSE-MODULE OBLIGATION for Hardware Studio.

A Silicon functional unit U is reversible iff there exists a module R with R ∘ U = id. This discharges that obligation for a combinational unit THREE independent ways that MUST AGREE:

1. Exhaustive bit-blast — the unit’s 2ⁿ-row truth table is a permutation (each output distinct); its inverse permutation IS the constructive reverse module R.
2. Algebraic certificate — for a linear (CNOT/XOR) unit, its GF(2) transfer matrix is invertible (∈ GL(n,2)); reused from logicaffeine_proof::revgate.
3. Z3 equivalence — (behind the verification feature) check_z3_hw_equivalence proves the composed R ∘ U structurally equals the identity.

The obligation FAILS LOUDLY if any two discharged methods disagree — the “our bit-blaster == Z3 == algebra” pattern from phase_hw_native_vs_z3.rs, now for reversibility. It emits the SVA property that pins R(U(x)) == x, the hardware-level twin of the software forward ; reverse ≡ id lock.

Structs

JournaledInjectivity

A discharged JOURNALED-op injectivity obligation — the hardware twin of the software minimal-bit journaling (corner 1). A Journaled op F is many-to-one (it erases), but AUGMENTED with its Bennett ancilla J (the journal entry — the exact bits it destroyed), the map x ↦ (F(x), J(x)) is INJECTIVE: the reverse module reconstructs x from the post-state AND the ancilla. This closes the R4 gap — the Z3/exhaustive proofs covered the Bijection core, and this covers every Journaled op the same way.

ReverseModuleObligation

A discharged reverse-module obligation: the constructive reverse gate plus the SVA property that pins the reverse-module identity, produced only when every attempted method AGREED that U is reversible.

Functions

discharge_journaled_injective

Prove a Journaled op is INJECTIVE once augmented with its Bennett ancilla. augmented[x] is the packed (F(x), J(x)) output for input x (all 2^in_bits inputs present). Injective iff every packed output is distinct — an EXHAUSTIVE bit-blast, the same rigor as certify_gate, so the core needs no SMT solver. Fails loud on a collision: two inputs share an augmented output, so the ancilla did NOT capture the erased bits — a genuine (un-reversible) Landauer erasure.

discharge_reverse_module

Discharge the reverse-module obligation for the n-bit combinational unit truth_table. Proves reversibility by exhaustive bit-blast AND — when linear_rows (the GF(2) transfer matrix) is given — the algebraic GF(2) certificate, and REQUIRES the two verdicts to agree. On success returns the reverse module + SVA property; on failure names the erasure or the method disagreement.