Reversible-circuit resource cost — the derived gate-list cost model (ECDLP Tranche 1b)

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

The cost half of the reversible-circuit substrate (Circuit.lean). The design decision (locked in specs/ecdlp-resource-plan.md): a circuit's resource cost is a function of its gate list, not a number annotated onto an opaque Equiv. So "operation op costs ≤ B Toffolis" is a theorem — exhibit a circuit c, prove denote c = op and (circuitCost c).toffoli ≤ B — not a trusted constant. This is what makes the downstream ECDLP resource accounting genuinely machine-checked.

Cost bundles the standard fault-tolerant resource fields (qubit width, ancilla, Toffoli count and depth, CNOT count, T-count, measurements), all ℕ. circuitCost reads each additive field off the gate list by (c.map (gateCost · |>.field)).sum, deliberately avoiding an AddMonoid Cost instance (the width fields qubits/ancilla are NOT additive under composition — they combine by max / accumulation — so a single monoid structure would be wrong for them). The composition lemmas below make the additive/non-additive split explicit: Toffoli/CNOT counts add exactly; Toffoli depth is ≤-subadditive (here equality, since the model is sequential); width is ≤ max (here trivial, since circuitCost fixes qubits := n — genuine width/ancilla accounting is a Pass-2 refinement).

structure Reversible.Cost : Type

Fault-tolerant resource cost of a reversible circuit: qubit width, ancilla count, Toffoli count and depth, CNOT count, T-count, and measurement count. All ℕ. The count fields are additive under sequential composition; qubits/ancilla are width fields (combine by max/accumulation, not +).

• qubits : ℕ

  Number of (logical) qubits the circuit acts on.

• ancilla : ℕ

  Number of ancilla qubits used.

• toffoli : ℕ

  Number of Toffoli (CCX) gates.

• toffoliDepth : ℕ

  Toffoli depth (longest chain of dependent Toffolis); for a sequential gate list, the count.

• cnot : ℕ

  Number of CNOT (CX) gates.

• tCount : ℕ

  T-gate count (Pass-2 refinement; 0 at the abstract Pass-1 model).

• meas : ℕ

  Number of measurements.

def Reversible.instDecidableEqCost.decEq (x✝ x✝¹ : Cost) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Reversible.instDecidableEqCost : DecidableEq Cost

Equations

• Reversible.instDecidableEqCost = Reversible.instDecidableEqCost.decEq

@[instance_reducible]

instance Reversible.instReprCost : Repr Cost

Equations

• Reversible.instReprCost = { reprPrec := Reversible.instReprCost.repr }

def Reversible.instReprCost.repr : Cost → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Reversible.gateCost {n : ℕ} : Gate n → Cost

Per-gate resource cost. X is free (a classical bit flip, no T/Toffoli); CX is one CNOT; CCX is one Toffoli at depth one; swap is three CNOTs (the standard CNOT decomposition). The width fields (qubits/ancilla) are 0 here — they are supplied at the circuit level by circuitCost, since a single gate does not determine the register width. That last point is a modelling decision, not proved and not provable from the gate alone: nothing forces width 0 rather than, say, the largest index mentioned. It is chosen so that width composes at the circuit level instead of being double-counted per gate.

Cost is syntactic: it is a function of the gate, not of the permutation it realises. A degenerate gate (control = target, e.g. CCX i j i) acts as the identity under denoteGate yet is still billed its full cost. This is the conservative (upper-bound) convention for resource accounting — circuitCost c bounds the true cost of any realisation of c — so do NOT assume denoteGate g = id ⇒ gateCost g = 0. A degenerate-gate–stripping simplify pass before costing is a possible Pass-2 refinement.

Equations

• Reversible.gateCost (Reversible.Gate.X i) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 0, tCount := 0, meas := 0 }
• Reversible.gateCost (Reversible.Gate.CX c t) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 1, tCount := 0, meas := 0 }
• Reversible.gateCost (Reversible.Gate.CCX c₁ c₂ t) = { qubits := 0, ancilla := 0, toffoli := 1, toffoliDepth := 1, cnot := 0, tCount := 0, meas := 0 }
• Reversible.gateCost (Reversible.Gate.swap i j) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 3, tCount := 0, meas := 0 }

Interface lemmas (CONVENTIONS §9.1, F1): the per-constructor costs, stated once, so consumers cite a lemma instead of unfolding the match. Not @[simp] — existing proofs unfold by name and must keep their behaviour.

theorem Reversible.gateCost_X {n : ℕ} (i : Fin n) : gateCost (Gate.X i) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 0, tCount := 0, meas := 0 }

An X gate is free in every counted resource.

theorem Reversible.gateCost_CX {n : ℕ} (c t : Fin n) : gateCost (Gate.CX c t) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 1, tCount := 0, meas := 0 }

A CX gate costs one CNOT.

theorem Reversible.gateCost_CCX {n : ℕ} (c₁ c₂ t : Fin n) : gateCost (Gate.CCX c₁ c₂ t) = { qubits := 0, ancilla := 0, toffoli := 1, toffoliDepth := 1, cnot := 0, tCount := 0, meas := 0 }

A CCX gate costs one Toffoli at depth one.

theorem Reversible.gateCost_swap {n : ℕ} (i j : Fin n) : gateCost (Gate.swap i j) = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 3, tCount := 0, meas := 0 }

A swap costs three CNOTs.

def Reversible.circuitCost {n : ℕ} (c : Circuit n) : Cost

The derived cost of a circuit: each additive field is the gate-list sum of that field of gateCost; the width is qubits := n (the circuit acts on n wires) with ancilla := 0 (the classical reversible layer introduces no ancilla — ancilla accounting is a Pass-2 refinement).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Reversible.circuitCost_nil {n : ℕ} : circuitCost [] = { qubits := n, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 0, tCount := 0, meas := 0 }

@[simp]

theorem Reversible.circuitCost_qubits {n : ℕ} (c : Circuit n) : (circuitCost c).qubits = n

@[simp]

theorem Reversible.circuitCost_ancilla {n : ℕ} (c : Circuit n) : (circuitCost c).ancilla = 0

theorem Reversible.cost_comp_toffoli_count {n : ℕ} (c₁ c₂ : Circuit n) : (circuitCost (c₁ ++ c₂)).toffoli = (circuitCost c₁).toffoli + (circuitCost c₂).toffoli

Toffoli count is additive under composition. Exact equality: the gate list of c₁ ++ c₂ is the concatenation, and the sum of a concatenation splits (List.map_append + List.sum_append).

theorem Reversible.cost_comp_cnot_count {n : ℕ} (c₁ c₂ : Circuit n) : (circuitCost (c₁ ++ c₂)).cnot = (circuitCost c₁).cnot + (circuitCost c₂).cnot

CNOT count is additive under composition.

theorem Reversible.cost_comp_toffoli_depth_le {n : ℕ} (c₁ c₂ : Circuit n) : (circuitCost (c₁ ++ c₂)).toffoliDepth ≤ (circuitCost c₁).toffoliDepth + (circuitCost c₂).toffoliDepth

Toffoli depth is ≤-subadditive under composition. For a sequential gate list this holds with equality; stated as ≤ because depth is genuinely subadditive (parallel scheduling can only lower it), which is the bound downstream resource accounting relies on.

theorem Reversible.cost_comp_qubits_le {n : ℕ} (c₁ c₂ : Circuit n) : (circuitCost (c₁ ++ c₂)).qubits ≤ max (circuitCost c₁).qubits (circuitCost c₂).qubits

Width is ≤ max under composition. Composing two circuits on the same n wires does not widen the register. (At the abstract Pass-1 model circuitCost fixes qubits := n, so this is n ≤ max n n; genuine width/ancilla accounting is a Pass-2 refinement.)

theorem Reversible.cost_inverse_toffoli {n : ℕ} (c : Circuit n) : (circuitCost (inverse c)).toffoli = (circuitCost c).toffoli

The inverse circuit has the same cost. inverse = List.reverse permutes the gate list, and every additive field is a List.sum of a List.map, invariant under reversal (List.map_reverse + List.sum_reverse); the width fields are constant.

theorem Reversible.cost_inverse_cnot {n : ℕ} (c : Circuit n) : (circuitCost (inverse c)).cnot = (circuitCost c).cnot