Fast #eval-able reversible-circuit evaluation — the Array Bool bridge (ECDLP testing infra)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). This is testing infrastructure, not part of the ECDLP cost / correctness claims.

Purpose

A strict Array Bool-backed evaluator (runArr) for Reversible.Circuit, with a proven bridge (runArr_apply, regValRangeArr_eq) to the reference denote semantics. The point is fast, theorem-independent value cross-checks: #eval-ing runArr / regValRangeArr on a concrete circuit witness produces a number that is certified equal (by the bridge lemmas) to the denote / regValRange value the correctness theorems are stated about. So the #eval checks the real denote-based semantics, not a separate evaluator.

The pathology it fixes

The reference state is State n := Fin n → Bool and denoteGate uses Function.update (and, for swap, Equiv.swap). Under #eval / native_decide these are lazy: reading one final-wire bit of denote c s re-reads the inner state through the whole gate history. A CCX reads 3 bits, so a single final-bit read recurses 3 ^ depth through the fold — exponential blowup. On the Fin 27, 61-gate cModAdd circuit this hangs.

runArr represents the state as a strict Array Bool: each gate is O(1) array work (Array.set! / Array.getElem!), the whole run is O(gates), no re-reads. It evaluates instantly.

The bridge

• applyGate_apply — the step lemma: applyGate g a matches denoteGate g s wire-for-wire, given a represents s (a.size = m and ∀ j, a[j]! = s j), and preserves the representation.
• runArr_apply — headline: (runArr c (ofState s))[i]! = denote c s i for all i. Induction on c, maintaining the representation invariant; ofState seeds it via Array.getElem_ofFn.
• regValRangeArr_eq — the consumer-facing bridge: regValRangeArr f (runArr c (ofState s)) k = regValRange f (denote c s) k (a Finset.sum_congr over runArr_apply). So #eval regValRangeArr f (runArr c (ofState s)) k is a fast number, equal to the regValRange f (denote c s) k of the correctness theorems.

runArr_apply and regValRangeArr_eq are pure structural / arithmetic proofs (foundational triple only); no native_decide appears in any proven lemma. The demonstration examples below use decide / rfl on small witnesses to exhibit a green, fast, theorem-independent value check.

The strict Array Bool evaluator

def Reversible.applyGate {m : ℕ} (g : Gate m) (a : Array Bool) : Array Bool

A single gate's action on a strict Array Bool state. Each gate is O(1) array work (Array.getElem! / Array.set!). Degenerate forms (control = target) act as the identity, mirroring denoteGate. Out-of-bounds indices are inert (set! = setIfInBounds); on a size-m array indexed by Fin m every access is in bounds, which is what the bridge lemmas assume.

Equations

• Reversible.applyGate (Reversible.Gate.X i) a = a.set! ↑i !a[↑i]!
• Reversible.applyGate (Reversible.Gate.CX c t) a = if c = t then a else a.set! (↑t) (a[↑c]! ^^ a[↑t]!)
• Reversible.applyGate (Reversible.Gate.CCX c₁ c₂ t) a = if t = c₁ ∨ t = c₂ then a else a.set! (↑t) (a[↑t]! ^^ a[↑c₁]! && a[↑c₂]!)
• Reversible.applyGate (Reversible.Gate.swap i j) a = (a.set! (↑i) a[↑j]!).set! (↑j) a[↑i]!

def Reversible.runArr {m : ℕ} (c : Circuit m) (a : Array Bool) : Array Bool

Run a circuit on a strict Array Bool state (fold applyGate over the gate list). O(gates).

Equations

• Reversible.runArr c a = List.foldl (fun (a : Array Bool) (g : Reversible.Gate m) => Reversible.applyGate g a) a c

def Reversible.ofState {m : ℕ} (s : State m) : Array Bool

Seed the array representation of a State m. (ofState s).size = m and (ofState s)[j]! = s j.

Equations

• Reversible.ofState s = Array.ofFn s

@[simp]

theorem Reversible.ofState_size {m : ℕ} (s : State m) : (ofState s).size = m

theorem Reversible.ofState_getElem! {m : ℕ} (s : State m) (j : Fin m) : (ofState s)[↑j]! = s j

The seed array represents its source state: (ofState s)[j]! = s j.

The representation predicate and the bridge

def Reversible.Represents {m : ℕ} (a : Array Bool) (s : State m) : Prop

a represents the State m s: it has the right size and agrees with s on every wire. The invariant maintained by applyGate / runArr.

Equations

• Reversible.Represents a s = (a.size = m ∧ ∀ (j : Fin m), a[↑j]! = s j)

theorem Reversible.ofState_represents {m : ℕ} (s : State m) : Represents (ofState s) s

@[simp]

theorem Reversible.applyGate_size {m : ℕ} (g : Gate m) (a : Array Bool) : (applyGate g a).size = a.size

applyGate preserves array size.

Local getElem!-only rewrite lemmas for set! (= setIfInBounds). Stated purely in Array.getElem! to keep proof terms term-independent (the dependent getElem bounds proof breaks rw). Both route a[i]! through a[i]? via Array.getElem!_eq_getD.

theorem Reversible.getElem!_set!_self {a : Array Bool} {i : ℕ} {v : Bool} (h : i < a.size) : (a.set! i v)[i]! = v

Updating in bounds, then reading the updated index: (a.set! i v)[i]! = v for i < a.size.

theorem Reversible.getElem!_set!_ne {a : Array Bool} {i j : ℕ} {v : Bool} (h : i ≠ j) : (a.set! i v)[j]! = a[j]!

Updating index i, then reading a different index j: (a.set! i v)[j]! = a[j]!.

theorem Reversible.applyGate_apply {m : ℕ} (g : Gate m) {a : Array Bool} {s : State m} (h : Represents a s) : Represents (applyGate g a) (denoteGate g s)

The step lemma. If a represents s, then applyGate g a represents denoteGate g s: the size is preserved and (applyGate g a)[i]! = denoteGate g s i wire-for-wire. Cased on g; each case is Array.set! (= setIfInBounds) reasoning matched against Function.update / Equiv.swap.

theorem Reversible.runArr_represents {m : ℕ} (c : Circuit m) {a : Array Bool} {s : State m} (h : Represents a s) : Represents (runArr c a) (denote c s)

runArr preserves the representation invariant (fold of applyGate_apply).

theorem Reversible.runArr_apply {m : ℕ} (c : Circuit m) (s : State m) (i : Fin m) : (runArr c (ofState s))[↑i]! = denote c s i

Bridge headline. The strict Array Bool run of a circuit on ofState s reproduces the reference denote semantics wire-for-wire: (runArr c (ofState s))[i]! = denote c s i. So an #eval of runArr is a faithful, fast computation of denote.

The register-value bridge (regValRange)

def Reversible.regValRangeArr {m : ℕ} (f : ℕ → Fin m) (a : Array Bool) (k : ℕ) : ℕ

Place-value readout of the low k bits of a register laid out on wires f i, read off a strict Array Bool state. The Array-backed counterpart of regValRange.

Equations

• Reversible.regValRangeArr f a k = ∑ i ∈ Finset.range k, a[↑(f i)]!.toNat * 2 ^ i

theorem Reversible.regValRangeArr_eq {m : ℕ} (f : ℕ → Fin m) (c : Circuit m) (s : State m) (k : ℕ) : regValRangeArr f (runArr c (ofState s)) k = regValRange f (denote c s) k

Consumer-facing bridge. The fast Array-backed register read equals the reference regValRange of the denote semantics. Hence #eval regValRangeArr f (runArr c (ofState s)) k is a fast number, certified equal to the regValRange f (denote c s) k the correctness theorems use.

Demonstration: a green, fast, theorem-independent value cross-check

The Fin m denote evaluator blows up under #eval on a many-gate circuit (lazy Function.update re-reads, exponential in depth). runArr evaluates instantly. The witness is the S6.3a 2-bit reducer modReduceLayout2 : ModReduceLayout 13 2 at the x = 3 ↦ 0 subtract-branch state.

The #eval prints the fast Array-backed value; the example confirms — fast, via decide — that the Array-backed register read equals that number; and regValRangeArr_eq certifies that this same number is the regValRange (denote …) of modReduce_correct.