A VALUE-EXACT constant-propagation pass on reversible circuits

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Constant propagation on a reversible circuit: a forward abstract interpretation over the gate list that tracks each wire as Zero / One / Unknown (seeded from the classical initial state — ancillas are |0⟩) and folds the Toffolis it can decide:

• a CCX with a control known 0 never fires → drop it;
• a CCX with a control known 1 acts as a CX on the other control → fold to CX.

Both folds are value-exact — they change the gate list but not the function computed — so the pass is a proved circuit-to-circuit transform, cprop_denote, and every Toffoli it removes is a Toffoli the resource count (Cost.lean) no longer sees. The abstract state is deliberately conservative (any written wire becomes Unknown; only swap moves knowledge), which is sound and already captures the main benefit — a fresh |0⟩ ancilla stays known-0 until it is written, so every Toffoli reading it as a control while it is still 0 is dropped. (The transform was first needed as the dominant Toffoli lever of the reversible-arithmetic application that lives in the Ecdsafail repository, specs/ecdsa/ecdlp-resource-plan.md there, where it is applied informally; here it is the theorem.)

@[reducible, inline]

abbrev Reversible.Abs (m : ℕ) : Type

Abstract wire values: none = Unknown, some b = provably b``.

Equations

• Reversible.Abs m = (Fin m → Option Bool)

def Reversible.absAgree {m : ℕ} (α : Abs m) (s : State m) : Prop

The abstract state α soundly describes concrete state s: every wire α claims to know has that value in s.

Equations

• Reversible.absAgree α s = ∀ (i : Fin m) (b : Bool), α i = some b → s i = b

Folding one gate against the abstract state

def Reversible.foldGate {m : ℕ} (α : Abs m) : Gate m → Circuit m

Fold a gate given known-constant wires. Only CCX folds: a degenerate CCX (target is a control) is the identity → drop; a control known 0 → drop; a control known 1 → collapse to a CX on the other control. Every other gate is kept. VALUE-EXACT (foldGate_denote).

Equations

• One or more equations did not get rendered due to their size.
• Reversible.foldGate α x✝ = [x✝]

theorem Reversible.foldGate_denote {m : ℕ} {α : Abs m} {s : State m} (h : absAgree α s) (g : Gate m) : denote (foldGate α g) s = denoteGate g s

foldGate is value-exact. On any state the abstract α correctly describes, the folded gate list computes exactly what the original gate does.

Forward-updating the abstract state

def Reversible.stepAbs {m : ℕ} (α : Abs m) : Gate m → Abs m

Conservative forward abstract-state update. X flips a known bit; swap exchanges; a CX/CCX write makes the target Unknown (sound over-approximation). Wires not written keep their knowledge — so a fresh |0⟩ ancilla stays known-0 until something writes it.

Equations

• Reversible.stepAbs α (Reversible.Gate.X i) = Function.update α i none
• Reversible.stepAbs α (Reversible.Gate.CX c t) = Function.update α t none
• Reversible.stepAbs α (Reversible.Gate.CCX c₁ c₂ t) = Function.update α t none
• Reversible.stepAbs α (Reversible.Gate.swap i j) = fun (k : Fin m) => if k = i then α j else if k = j then α i else α k

theorem Reversible.stepAbs_agree {m : ℕ} {α : Abs m} {s : State m} (h : absAgree α s) (g : Gate m) : absAgree (stepAbs α g) (denoteGate g s)

stepAbs is sound. If α describes s, the updated abstract state describes the gate's output state. Every write-target becomes Unknown (vacuously sound); swap exchanges knowledge; untouched wires keep it.

The pass and its value-exactness

def Reversible.cprop {m : ℕ} (α : Abs m) : Circuit m → Circuit m

The constant-propagation pass. Fold each gate against the running abstract state, threading the forward update. Seeded with α describing the input (e.g. ancillas some false).

Equations

• Reversible.cprop α [] = []
• Reversible.cprop α (g :: gs) = Reversible.foldGate α g ++ Reversible.cprop (Reversible.stepAbs α g) gs

theorem Reversible.cprop_denote {m : ℕ} {α : Abs m} (c : Circuit m) {s : State m} (h : absAgree α s) : denote (cprop α c) s = denote c s

THE HEADLINE — cprop is VALUE-EXACT. For any input s the seed α correctly describes, the propagated circuit computes exactly the same function: denote (cprop α c) s = denote c s. So folding provably-determined Toffolis changes the gate list (fewer/cheaper gates) but NOT the computed value — the frontier's key lever, machine-checked.

A concrete win: a known-0 ancilla control drops its Toffoli

def Reversible.demoAbs : Abs 3

Layout: wire 0 is a known-0 ancilla; 1, 2 are data.

Equations

• Reversible.demoAbs i = if i = 0 then some false else none

theorem Reversible.demoAbs_agree (s : State 3) (h0 : s 0 = false) : absAgree demoAbs s

On a state where wire 0 is false, demoAbs is sound.

cprop is a sound REDUCING optimization (cost side)

cprop_denote shows the pass preserves the computed VALUE. These show it never increases — and, on a known-constant control, strictly decreases — the emitted Toffoli count. Together: cprop is a certified value-exact Toffoli-reducing pass, exactly the frontier's key lever, proved both correct and beneficial.

theorem Reversible.foldGate_toffoli_le {m : ℕ} (α : Abs m) (g : Gate m) : (circuitCost (foldGate α g)).toffoli ≤ (gateCost g).toffoli

Folding never increases a gate's Toffoli count. A CCX folds to [], [CX], or [CCX] — Toffoli count 0, 0, or 1, all ≤ 1; every other gate is unchanged.

theorem Reversible.cprop_toffoli_le {m : ℕ} (α : Abs m) (c : Circuit m) : (circuitCost (cprop α c)).toffoli ≤ (circuitCost c).toffoli

cprop never increases the Toffoli count. So constant-propagation is a valid optimization: it computes the same value (cprop_denote) with no more Toffolis.

theorem Reversible.foldGate_ccx_known_false {m : ℕ} (α : Abs m) (c₁ c₂ t : Fin m) (hdeg : ¬(t = c₁ ∨ t = c₂)) (h0 : α c₁ = some false ∨ α c₂ = some false) : foldGate α (Gate.CCX c₁ c₂ t) = []

The reduction mechanism. A non-degenerate CCX with a control known to be false folds AWAY (to []): its Toffoli is dropped entirely. This is where constant propagation buys Toffolis.

theorem Reversible.andCell_constprop_reduces : (circuitCost (cprop (fun (i : Fin 4) => if i = 2 then some false else none) [Gate.CCX 0 1 3, Gate.CCX 0 2 3, Gate.CCX 1 2 3])).toffoli = 1 ∧ (circuitCost [Gate.CCX 0 1 3, Gate.CCX 0 2 3, Gate.CCX 1 2 3]).toffoli = 3

A real multi-Toffoli win on the AND-adder's carry cell. The three-CCX carry cell [CCX a b g, CCX a c g, CCX b c g] with the carry-in c a known-0 ancilla constant-propagates to a SINGLE Toffoli — a value-exact 3 → 1 (67%) Toffoli reduction, exactly the structure constant folding exploits in a ripple/AND adder whose low carry-in is |0⟩.