logicaffeine_proof/
revgate.rs

1//! Certify reversible logic gates as bijections.
2//!
3//! The Silicon tier maps each VM stencil family to a functional unit,
4//! and the adiabatic datapath demands those units be reversible. A unit over `n` bits is reversible
5//! iff its truth table is a permutation of `{0..2ⁿ}` — a bijection whose inverse is the inverse
6//! permutation, i.e. a real constructive reverse gate. A purely-linear (CNOT/XOR) block is reversible
7//! iff its GF(2) transfer matrix is invertible (`∈ GL(n,2)`) — reused from [`crate::gf2`].
8//!
9//! This is the hardware-gate complement to the software-level Z3 bijectivity proofs in
10//! `logicaffeine_synth::reversible`: there the abelian `Rev*` opcodes are proved bijective as BV64
11//! maps; here the universal reversible generators they compile to — CNOT (the `BitXor→CNOT`
12//! embedding), Toffoli (the `BitAnd→Toffoli` embedding), and Fredkin — are certified as gates.
13
14use crate::gf2::is_invertible_gf2;
15
16/// A reversibility certificate for a functional unit.
17#[derive(Debug, PartialEq, Eq)]
18pub enum GateCert {
19    /// Reversible: `inverse[output] = input`, the constructive reverse gate (itself a truth table).
20    Reversible { inverse: Vec<usize> },
21    /// Irreversible: two distinct inputs collide to the same output — information is erased (the
22    /// Landauer cost the adiabatic tier forbids). Carries the witnessing collision.
23    Collision {
24        input_a: usize,
25        input_b: usize,
26        output: usize,
27    },
28}
29
30/// Certify an `n`-bit functional unit from its truth table (`table[input] = output`, each a state
31/// index `0..2ⁿ`). Reversible iff the table is a permutation; returns the inverse gate, or the first
32/// erasing collision that proves it is not.
33pub fn certify_gate(n: u32, table: &[usize]) -> GateCert {
34    let size = 1usize << n;
35    assert_eq!(
36        table.len(),
37        size,
38        "an n-bit truth table must have exactly 2^n rows"
39    );
40    let mut inverse = vec![usize::MAX; size];
41    for (input, &output) in table.iter().enumerate() {
42        assert!(
43            output < size,
44            "truth-table output {output} out of range for {n} bits"
45        );
46        if inverse[output] != usize::MAX {
47            // A second input mapping to `output` means the map is not injective — it erases.
48            return GateCert::Collision {
49                input_a: inverse[output],
50                input_b: input,
51                output,
52            };
53        }
54        inverse[output] = input;
55    }
56    GateCert::Reversible { inverse }
57}
58
59/// CNOT (2-bit): `(a,b) ↦ (a, a⊕b)`, state encoded `a | b<<1`. The universal reversible XOR
60/// generator — `RevXor` lifted to a gate.
61pub fn cnot() -> Vec<usize> {
62    (0..4)
63        .map(|s| {
64            let (a, b) = (s & 1, (s >> 1) & 1);
65            a | ((a ^ b) << 1)
66        })
67        .collect()
68}
69
70/// Toffoli / CCNOT (3-bit): `(a,b,c) ↦ (a, b, c⊕(a∧b))`. The universal reversible AND generator.
71pub fn toffoli() -> Vec<usize> {
72    (0..8)
73        .map(|s| {
74            let (a, b, c) = (s & 1, (s >> 1) & 1, (s >> 2) & 1);
75            a | (b << 1) | ((c ^ (a & b)) << 2)
76        })
77        .collect()
78}
79
80/// Fredkin / CSWAP (3-bit): swap `b` and `c` when `a = 1`. Conserves 1-count; self-inverse.
81pub fn fredkin() -> Vec<usize> {
82    (0..8)
83        .map(|s| {
84            let (a, b, c) = (s & 1, (s >> 1) & 1, (s >> 2) & 1);
85            let (b2, c2) = if a == 1 { (c, b) } else { (b, c) };
86            a | (b2 << 1) | (c2 << 2)
87        })
88        .collect()
89}
90
91/// Certify a purely-LINEAR `n`-bit block reversible: its GF(2) transfer matrix (`rows[v]` a bitmask
92/// of which input bits XOR into output bit `v`) must be invertible (`∈ GL(n,2)`), giving a linear
93/// inverse. This is the fast path for CNOT-only (XOR) datapaths.
94pub fn certify_linear(n: u32, rows: &[u64]) -> bool {
95    is_invertible_gf2(n, rows)
96}
97
98#[cfg(test)]
99#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/revgate/tests.rs"]
100mod tests;
logicaffeine_proof/revgate.rs

logicaffeine_proof/
revgate.rs
