Module revgate 

Certify reversible logic gates as bijections.

The Silicon tier maps each VM stencil family to a functional unit, and the adiabatic datapath demands those units be reversible. A unit over n bits is reversible iff its truth table is a permutation of {0..2ⁿ} — a bijection whose inverse is the inverse permutation, i.e. a real constructive reverse gate. A purely-linear (CNOT/XOR) block is reversible iff its GF(2) transfer matrix is invertible (∈ GL(n,2)) — reused from crate::gf2.

This is the hardware-gate complement to the software-level Z3 bijectivity proofs in logicaffeine_synth::reversible: there the abelian Rev* opcodes are proved bijective as BV64 maps; here the universal reversible generators they compile to — CNOT (the BitXor→CNOT embedding), Toffoli (the BitAnd→Toffoli embedding), and Fredkin — are certified as gates.

Enums

GateCert

A reversibility certificate for a functional unit.

Functions

certify_gate

Certify an n-bit functional unit from its truth table (table[input] = output, each a state index 0..2ⁿ). Reversible iff the table is a permutation; returns the inverse gate, or the first erasing collision that proves it is not.

certify_linear

Certify a purely-LINEAR n-bit block reversible: its GF(2) transfer matrix (rows[v] a bitmask of which input bits XOR into output bit v) must be invertible (∈ GL(n,2)), giving a linear inverse. This is the fast path for CNOT-only (XOR) datapaths.

cnot

CNOT (2-bit): (a,b) ↦ (a, a⊕b), state encoded a | b<<1. The universal reversible XOR generator — RevXor lifted to a gate.

fredkin

Fredkin / CSWAP (3-bit): swap b and c when a = 1. Conserves 1-count; self-inverse.

toffoli

Toffoli / CCNOT (3-bit): (a,b,c) ↦ (a, b, c⊕(a∧b)). The universal reversible AND generator.