Codegen 97 declarations in 8 modules
FormalRV.Codegen.DeviceProgramParse
FormalRV/Codegen/DeviceProgramParse.lean
FormalRV.Codegen.DeviceProgramParse — Lean-side parser of the shared
DEVICE-PROGRAM 1.0 syntax (plus the shared backend JSON), closing the
Lean ↔ FTQ-VM interop loop:
Lean Schedule ──emitSchedule──▶ program.dp ──┬─▶ this parser ─▶ List SysCall
│ └─▶ the decidable invariant
│ bundle (same checkers
│ the theorems use)
└─▶ ftq_vm (Python) ─▶ discrete-event
finite-service verdict
One schedule file, two independent checkers. The grammar is exactly what
`Codegen/SysCallEmit.emitSchedule` produces (round-trip: `parse (emit s) = s`,
asserted at runtime by `scripts/CheckDeviceProgram.lean`); the backend JSON is
the FTQ-VM machine description, from which this module reconstructs the
`ZonedArch`, `OperationCapacityModel`, `SlotCapacityModel` and `AncillaModel`
the strict bundle needs (zone ids = zones sorted by `site_lo`; the `x-lean`
block carries the Lean-only parameters).
defparseNat
private def parseNat (s : String) : Except String Nat
defparseInterval
private def parseInterval (tok : String) : Except String (Nat × Nat)
Parse `[a,b)us` into `(a, b)`.
defparseQref
private def parseQref (tok : String) : Except String Nat
Parse `q[7]` into `7`.
defparseKV
private def parseKV (key : String) (tok : String) : Except String Nat
Parse `key=7` (checking the key) into `7`.
defparseNamedKV
private def parseNamedKV (key : String) (lookup : String → Option Nat)
(tok : String) : Except String NatParse `key=NAME` through a canonical name table (gates and bases are
NAMED, never numeric: `gate=CNOT`, `basis=Z`).
defparseOpLine
private def parseOpLine (line : String) : Except String SysCall
Parse one op line (already known to start with `[`).
defparseDeviceProgram
def parseDeviceProgram (text : String) : Except String (List SysCall)
Parse a full DEVICE-PROGRAM 1.0 text into a `Schedule`.
defparallelGroups
def parallelGroups (sched : List SysCall) :
List ((Nat × Nat) × List SysCall)Group a schedule into parallel layers by exact `[begin, end)` window,
preserving first-occurrence order.
defmaxSimultaneous
def maxSimultaneous (sched : List SysCall) : Nat
The widest simultaneous layer (1 = fully sequential).
structureParsedBackend
structure ParsedBackend
Everything the strict invariant bundle needs, reconstructed from the
shared backend file.
defgetNatD
private def getNatD (j : Json) (key : String) (dflt : Nat) : Nat
defgetBoolD
private def getBoolD (j : Json) (key : String) (dflt : Bool) : Bool
defobjEntries
private def objEntries (j : Json) : Except String (List (String × Json))
defparseBackend
def parseBackend (text : String) : Except String ParsedBackend
Parse the shared backend JSON.
defcheckDeviceProgram
def checkDeviceProgram (backendText programText : String) :
Except String BoolParse the shared backend + program files; the verdict conjoins
1. `gate_support_ok` — every named gate/measure/request is SUPPORTED
by the backend gate table and takes exactly its hardware time;
2. the strict invariant bundle — the same `Bool` function the
`native_decide` theorems certify, evaluated on the parsed input.
defgates_supported_ok
def gates_supported_ok (table : GateTable) (sched : List SysCall) : Bool
Every named gate exists in the hardware table (support only).
defgate_durations_ok
def gate_durations_ok (table : GateTable) (sched : List SysCall) : Bool
Gates PRESENT in the table take exactly their hardware time.
defgate_parallelism_ok
def gate_parallelism_ok (cap : OperationCapacityModel)
(sched : List SysCall) : BoolPhysical-gate concurrency (gate1q/gate2q/measure classes).
defdecoder_overload_ok
def decoder_overload_ok (cap : OperationCapacityModel)
(sched : List SysCall) : BoolDecoder concurrency against the finite worker pool.
defcontrol_parallelism_ok
def control_parallelism_ok (cap : OperationCapacityModel)
(sched : List SysCall) : BoolThe remaining op-concurrency caps (classical control plane).
defdiagnose
def diagnose (pb : ParsedBackend) (sched : List SysCall) : List String
The canonical contract codes violated by the schedule (`[]` = PASS).
The union of these checks equals `checkDeviceProgram`'s verdict (the
split refines the bundle's conjuncts without changing their meaning).
defdiagnoseDeviceProgram
def diagnoseDeviceProgram (backendText programText : String) :
Except String (List String)Parse both files and report the violated contract codes (`.error` for
parse failures = the SYNTAX code; `[]` = PASS).
FormalRV.Codegen.EGateQasm
FormalRV/Codegen/EGateQasm.lean
FormalRV.Codegen.EGateQasm — emit OpenQASM 2.0 from the measurement-augmented `EGate` IR
(base gates + `mz` measurement-reset), reusing the proven `Gate` emitter for base gates.
`mz q` (measurement-based uncomputation's value-effect: measure and reset to |0⟩) emits the
QASM `measure q -> c; reset q;` pair, whose computational-basis effect is `update f q false`
— exactly `EGate.applyNat (mz q)`. Base gates emit via `GateQasm.emitOps`.
Faithfulness is PROVEN (`emitEOps_applyNat`): the emitted op-list's computational-basis action
equals `EGate.applyNat`. Rendering (ops → text) is then a syntactic serialization, and the text
emitter `emitEGate`/`toQasmE` shares those exact ops.
inductiveEQasmOp
inductive EQasmOp
One emitted QASM op for the `EGate` IR: a native `QasmOp`, or a measure-and-reset.
defEQasmOp.applyNat
def EQasmOp.applyNat : EQasmOp → (Nat → Bool) → (Nat → Bool) | EQasmOp.op o, f => o.applyNat f | EQasmOp.meas q, f => Function.update f q false
Computational-basis action. `meas q` (measure + reset to |0⟩) sets bit `q` to `false`.
defapplyEProg
def applyEProg (prog : List EQasmOp) (f : Nat → Bool) : Nat → Bool
Run an emitted EGate program.
theoremapplyEProg_append
theorem applyEProg_append (p q : List EQasmOp) (f : Nat → Bool) :
applyEProg (p ++ q) f = applyEProg q (applyEProg p f)theoremapplyEProg_map_op
theorem applyEProg_map_op (l : List QasmOp) (f : Nat → Bool) :
applyEProg (l.map EQasmOp.op) f = applyProg l fA `QasmOp`-only program embeds into an `EQasmOp` program with the same action.
defemitEOps
def emitEOps : EGate → List EQasmOp | EGate.base g => (emitOps g).map EQasmOp.op | EGate.mz q => [EQasmOp.meas q] | EGate.seq a b => emitEOps a ++ emitEOps b
*Structured EGate emitter.**
theorememitEOps_applyNat
theorem emitEOps_applyNat (g : EGate) (f : Nat → Bool) :
applyEProg (emitEOps g) f = EGate.applyNat g f*★ EGate emitter faithfulness ★** — the emitted program's computational-basis action
equals `EGate.applyNat`. (Base gates via `emitOps_applyNat`; `mz` via measure-reset.)
defEQasmOp.render
def EQasmOp.render : EQasmOp → List String
| EQasmOp.op o => [o.render]
| EQasmOp.meas q => ["measure " ++ qref q ++ " -> c[" ++ toString q ++ "];",
"reset " ++ qref q ++ ";"]Render one emitted op to QASM source line(s).
defemitEGate
def emitEGate (g : EGate) : List String
Emit an `EGate` as a list of QASM source lines (rendering the proven-faithful op-list).
defegateWidth
def egateWidth : EGate → Nat | EGate.base g => widthOf g | EGate.mz q => q + 1 | EGate.seq a b => max (egateWidth a) (egateWidth b)
Qubit width touched by an `EGate`.
deftoQasmE
def toQasmE (g : EGate) : String
Full OpenQASM 2.0 program for an `EGate` (with a classical register for measurements).
defemittedCcxCount
def emittedCcxCount (g : EGate) : Nat
Number of emitted `ccx` op-lines — i.e. the emitted Toffoli count,
cross-checking `EGate.toffoli` at the text level.
FormalRV.Codegen.GateQasm
FormalRV/Codegen/GateQasm.lean
FormalRV.Codegen.GateQasm — emit logical OpenQASM 2.0 from the `Gate` IR,
with PROVED faithfulness theorems at BOTH the classical (native) and the
quantum (Clifford+T) level.
## What is proved
NATIVE (`x`/`cx`/`ccx`): `emitOps_applyNat` — the emitted native program,
under its Boolean (qelib1) semantics, equals the verified `Gate.applyNat`.
CLIFFORD+T (`h`/`t`/`tdg`/`x`/`cx`): `emitCliffT_acts_on_basis` — the
emitted Clifford+T program's UNITARY (`progMat`, built from `BaseUCom`
`uc_eval` matrices) acts on every basis state exactly as `Gate.applyNat`.
The `CCX` lowering is aligned with `BaseUCom.CCX` (the 7-T decomposition
the whole verified Shor stack rides on); its Toffoli action is the repo's
proven `gate_ccx_acts_on_basis`, so nothing about the 7-T identity is
re-derived or assumed.
Both are kernel-clean; rendering (ops → text) is a syntactic serialization.
defqref
def qref (q : Nat) : String
OpenQASM register reference `q[i]`.
inductiveQasmOp
inductive QasmOp
The classical-reversible `qelib1` gates: bit-flip, CNOT, Toffoli.
defQasmOp.applyNat
def QasmOp.applyNat : QasmOp → (Nat → Bool) → (Nat → Bool) | QasmOp.x q, f => update f q (!f q) | QasmOp.cx c t, f => update f t (xor (f t) (f c)) | QasmOp.ccx a b c, f => update f c (xor (f c) (f a && f b))
Boolean (basis-state) semantics, matching `qelib1` and `Gate.applyNat`.
defapplyProg
def applyProg (prog : List QasmOp) (f : Nat → Bool) : Nat → Bool
Run a native program left-to-right.
defQasmOp.render
def QasmOp.render : QasmOp → String | QasmOp.x q => "x " ++ qref q ++ ";" | QasmOp.cx c t => "cx " ++ qref c ++ "," ++ qref t ++ ";" | QasmOp.ccx a b c => "ccx " ++ qref a ++ "," ++ qref b ++ "," ++ qref c ++ ";"
OpenQASM 2.0 text for one native op.
theoremapplyProg_append
theorem applyProg_append (p q : List QasmOp) (f : Nat → Bool) :
applyProg (p ++ q) f = applyProg q (applyProg p f)defemitOps
def emitOps : Gate → List QasmOp | Gate.I => [] | Gate.X q => [QasmOp.x q] | Gate.CX c t => [QasmOp.cx c t] | Gate.CCX a b c => [QasmOp.ccx a b c] | Gate.seq g₁ g₂ => emitOps g₁ ++ emitOps g₂
*Native emitter (structured).**
theorememitOps_applyNat
theorem emitOps_applyNat (g : Gate) (f : Nat → Bool) :
applyProg (emitOps g) f = Gate.applyNat g f*★ Native faithfulness ★** — the emitted native program equals the
verified Boolean semantics `Gate.applyNat`, for every gate.
defwidthOf
def widthOf : Gate → Nat | Gate.I => 0 | Gate.X q => q + 1 | Gate.CX c t => max (c + 1) (t + 1) | Gate.CCX a b c => max (max (a + 1) (b + 1)) (c + 1) | Gate.seq g₁ g₂ => max (widthOf g₁) (widthOf g₂)
defpackBits
def packBits (dim : Nat) (f : Nat → Bool) : Nat
defpermAt
def permAt (dim : Nat) (g : Gate) (x : Nat) : Nat
defpermAtProg
def permAtProg (dim : Nat) (prog : List QasmOp) (x : Nat) : Nat
theorememitOps_permAt
theorem emitOps_permAt (dim : Nat) (g : Gate) (x : Nat) :
permAtProg dim (emitOps g) x = permAt dim g xdefemitNative
def emitNative (g : Gate) : List String
Native OpenQASM text.
inductiveCliffTOp
inductive CliffTOp
A Clifford+T OpenQASM op.
defCliffTOp.render
def CliffTOp.render : CliffTOp → String | CliffTOp.h n => "h " ++ qref n ++ ";" | CliffTOp.t n => "t " ++ qref n ++ ";" | CliffTOp.tdg n => "tdg " ++ qref n ++ ";" | CliffTOp.x n => "x " ++ qref n ++ ";" | CliffTOp.cx c tg => "cx " ++ qref c ++ "," ++ qref tg ++ ";"
OpenQASM 2.0 text for one Clifford+T op.
defCliffTOp.mat
noncomputable def CliffTOp.mat (dim : Nat) : CliffTOp → Square dim | CliffTOp.h n => uc_eval (BaseUCom.H n) | CliffTOp.t n => uc_eval (BaseUCom.T n) | CliffTOp.tdg n => uc_eval (BaseUCom.TDAG n) | CliffTOp.x n => uc_eval (BaseUCom.X n) | CliffTOp.cx c tg => uc_eval (BaseUCom.CNOT c tg)
The `BaseUCom` unitary of one Clifford+T op at dimension `dim`.
defprogMat
noncomputable def progMat (dim : Nat) : List CliffTOp → Square dim | [] => 1 | op :: l => progMat dim l * op.mat dim
Unitary realised by a Clifford+T program: circuit order left-to-right =
matrix product right-to-left, starting from the identity.
theoremprogMat_append
theorem progMat_append (dim : Nat) (l1 l2 : List CliffTOp) :
progMat dim (l1 ++ l2) = progMat dim l2 * progMat dim l1defemitCliffTOps
def emitCliffTOps : Gate → List CliffTOp
| Gate.I => []
| Gate.X q => [CliffTOp.x q]
| Gate.CX c t => [CliffTOp.cx c t]
| Gate.CCX a b c =>
[CliffTOp.h c, CliffTOp.cx b c, CliffTOp.tdg c, CliffTOp.cx a c,
CliffTOp.t c, CliffTOp.cx b c, CliffTOp.tdg c, CliffTOp.cx a c,
CliffTOp.cx a b, CliffTOp.tdg b, CliffTOp.cx a b,
CliffTOp.t a, CliffTOp.t b, CliffTOp.t c, CliffTOp.h c]
| Gate.seq g₁ g₂ => emitCliffTOps g₁ ++ emitCliffTOps g₂*Clifford+T emitter (structured).** `CCX` → the exact 7-T sequence of
`BaseUCom.CCX` (controls `a`,`b`; target `c`).
defemitCliffT
def emitCliffT (g : Gate) : List String
Clifford+T OpenQASM text = rendering of the verified ops.
theoremprogMat_CCX
theorem progMat_CCX (dim a b c : Nat) :
progMat dim (emitCliffTOps (Gate.CCX a b c)) = uc_eval (BaseUCom.CCX a b c : BaseUCom dim)The emitted 7-T sequence realises exactly the `BaseUCom.CCX` unitary
(same 15 gate factors, re-associated).
theorememitCliffT_acts_on_basis
theorem emitCliffT_acts_on_basis (dim : Nat) (g : Gate) :
∀ (f : Nat → Bool), Gate.WellTyped dim g →
progMat dim (emitCliffTOps g) * f_to_vec dim f = f_to_vec dim (Gate.applyNat g f)*The emitted Clifford+T circuit's unitary acts on every basis state
exactly as the verified Boolean semantics `Gate.applyNat`.** The `CCX`
case is the repo's proven `gate_ccx_acts_on_basis` (the 7-T Toffoli
action); `X`/`CX` use `gate_x/cx_acts_on_basis`; `seq` composes via
`progMat_append`. Requires `Gate.WellTyped dim g` (the gate identities
need each qubit `< dim` and the multi-qubit gates' qubits distinct).
deftoQasm
def toQasm (g : Gate) (cliffT : Bool
Full OpenQASM 2.0 program. `cliffT = true` ⇒ Clifford+T basis.
example(example)
example : emitNative (Gate.X 0) = ["x q[0];"]
example(example)
example : (emitCliffT (Gate.CCX 0 1 2)).length = 15
example(example)
example : permAtProg 2 (emitOps (qubit_swap 0 1)) 1 = 2
example(example)
example : permAt 3 (Gate.CCX 0 1 2) 3 = 7
defdemos
def demos : List (String × Gate)
FormalRV.Codegen.QASMEmit
FormalRV/Codegen/QASMEmit.lean
FormalRV.Codegen.QASMEmit — a UNIFORM OpenQASM emission framework.
A `Gadget` bundles a name with a width-parametric `Gate`-IR circuit.
`emitQASM` turns ANY gadget, at ANY width `n`, into an OpenQASM 2.0 program
via the faithful `toQasm` emitter. Every arithmetic gadget exposes one
`Gadget` descriptor and emits uniformly:
#eval IO.println (emitQASM CuccaroAdder 3)
The same interface is intended for every `Gate`-IR circuit in the project
(arithmetic gadgets, and QFT/QPE once exposed as `Gate`), so emission code
is written once, here, not per gadget.
structureGadget
structure Gadget
A named, width-parametric quantum circuit gadget that can be emitted to
OpenQASM. `circuit n` is the gadget at register width `n`, placed at qubit
offset 0. Every arithmetic/logic gadget should expose one of these.
deftoQASM
def toQASM (g : Gadget) (n : Nat) : String
The emitted OpenQASM 2.0 program for gadget `g` at width `n`
(Clifford+T basis).
deftoQASMNative
def toQASMNative (g : Gadget) (n : Nat) : String
The emitted program in the native (CX/CCX/X) basis instead of Clifford+T.
deftcount
def tcount (g : Gadget) (n : Nat) : Nat
Exact T-count of the gadget at register width `n`.
defgateCount
def gateCount (g : Gadget) (n : Nat) : Nat
Exact total gate count of the gadget at register width `n`.
defresourceReport
def resourceReport (g : Gadget) (n : Nat) : String
A human-readable exact resource line.
defemitQASM
def emitQASM (g : Gadget) (n : Nat) : String
*Uniform QASM emitter.** `emitQASM g n` is the OpenQASM 2.0 program for
gadget `g` at register width `n`. Works for every `Gadget` — e.g.
`emitQASM CuccaroAdder 3`.
FormalRV.Codegen.SysCallEmit
FormalRV/Codegen/SysCallEmit.lean
FormalRV.Codegen.SysCallEmit — a textual "device program" syntax that emits BOTH physical
operations and system calls from one schedule.
The `Architecture.SysCall` IR already unifies the two:
PHYSICAL operations — `Gate1q`, `Gate2q`, `Measure`, `TransitQubit` (the routing/transit);
SYSTEM calls — `RequestFreshAncilla`, `RequestMagicState`, `DecodeSyndrome`,
`PauliFrameUpdate`.
A `Schedule = List SysCall` therefore already interleaves both. This file renders a schedule to
a timestamped, category-tagged textual program (`DEVICE-PROGRAM 1.0`) so a backend can read off a
single stream containing the quantum gates AND the classical/factory/decoder system calls.
Rendering is a syntactic serialization; the schedule's MEANING (timing, conflicts, the wait law,
the I1–I4 invariants) is what `System.DeviceSchedule` / `ScheduleInvariantsExplicit` verify.
defqref
def qref (q : Nat) : String
defgate2qNames
def gate2qNames : List String
Canonical two-qubit gate names, indexed by `gate_id`.
defgate1qNames
def gate1qNames : List String
Canonical single-qubit gate names, indexed by `gate_id`.
defbasisNames
def basisNames : List String
Canonical measurement basis names, indexed by `basis`.
defgate2qName
def gate2qName (g : Nat) : String
defgate1qName
def gate1qName (g : Nat) : String
defbasisName
def basisName (b : Nat) : String
defgate2qIdOf
def gate2qIdOf (s : String) : Option Nat
Inverse lookups (used by the parser; `none` = unknown name).
defgate1qIdOf
def gate1qIdOf (s : String) : Option Nat
defbasisIdOf
def basisIdOf (s : String) : Option Nat
defcategoryOf
def categoryOf : SysCallKind → String | .Gate1q _ _ => "PHYS" | .Gate2q _ _ _ => "PHYS" | .Measure _ _ => "PHYS" | .TransitQubit _ _ => "PHYS" | .RequestFreshAncilla _ => "SYS " | .RequestMagicState _ => "SYS " | .DecodeSyndrome _ => "SYS " | .PauliFrameUpdate _ => "SYS "
Is a SysCall a PHYSICAL operation or a SYSTEM call?
defrenderKind
def renderKind : SysCallKind → String | .Gate1q q g => "gate1q " ++ qref q ++ " gate=" ++ gate1qName g | .Gate2q a b g => "gate2q " ++ qref a ++ "," ++ qref b ++ " gate=" ++ gate2qName g | .Measure q bas => "measure " ++ qref q ++ " basis=" ++ basisName bas | .TransitQubit q c => "transit " ++ qref q ++ " via channel=" ++ toString c | .RequestFreshAncilla site => "request_ancilla " ++ qref site | .RequestMagicState z => "request_magic factory=" ++ toString z | .DecodeSyndrome r => "decode_syndrome round=" ++ toString r | .PauliFrameUpdate c => "pauli_frame_update corr=" ++ toString c
Render one SysCall's operation. Gates and bases are rendered by NAME
(`gate=CNOT`, `basis=Z`) and the ancilla request names its exact qubit
(`request_ancilla q[100]`) — explicit, checkable syntax.
defrenderCall
def renderCall (sc : SysCall) : String
One program line: time window, category, operation.
defemitSchedule
def emitSchedule (name : String) (sched : Schedule) : String
Emit a full device program from a schedule (physical ops + system calls, in one stream).
defphysCount
def physCount (sched : Schedule) : Nat
Count of physical-operation lines emitted.
defsysCount
def sysCount (sched : Schedule) : Nat
Count of system-call lines emitted.
deftoffoliViaTeleport
def toffoliViaTeleport : Schedule
defparallelTwoMagic
def parallelTwoMagic : Schedule
Example: TWO magic states distilled in PARALLEL factories (overlapping `request_magic` system
calls), each routed and teleported into a distinct data qubit on disjoint channels — physical
ops and system calls interleaved and concurrent.
FormalRV.Codegen.SysCallEmitDemo
FormalRV/Codegen/SysCallEmitDemo.lean
FormalRV.Codegen.SysCallEmitDemo — STANDALONE demo that PRINTS the emitted `DEVICE-PROGRAM` text
for the example schedules. It has `#eval`s (so it is NOT part of the umbrella `lake build`); run
it on demand with:
lake env lean FormalRV/Codegen/SysCallEmitDemo.lean
The schedules themselves, and their invariant pass/fail verdicts, live in build-checked modules
(`Codegen/SysCallEmit.lean`, `System/SystemInvariantExamples.lean`); this file only renders them.
(no documented top-level declarations)
FormalRV.Codegen.UComQasm
FormalRV/Codegen/UComQasm.lean
FormalRV.Codegen.UComQasm — a UNIFORM, faithful OpenQASM emitter for the
FULL `BaseUCom` unitary IR (rotations included), generalizing the Gate-IR
emitter (`GateQasm`) onto the SAME semantic-faithfulness contract:
progMat (emit c) = uc_eval c.
## Why this exists
The reversible `Gate` IR (`I`/`X`/`CX`/`CCX`) underlying `Codegen.QASMEmit`
cannot express continuous rotations, so genuinely-quantum gadgets — the
(inverse) QFT, QPE — live in `BaseUCom` (`H`/`Rz`/`CNOT`/…). Rather than a
bespoke per-gadget emitter, this module emits ANY `BaseUCom` faithfully and
proves the emitted op program's unitary (`uprogMat`, built from `uc_eval`
matrices) equals the circuit's `uc_eval` — the exact contract the Clifford+T
arithmetic emitter (`GateQasm.progMat` / `emitCliffT_acts_on_basis`) already
satisfies. Arithmetic gadgets factor through this emitter via `Gate.toUCom`
(`uprogMat_emitUComOps_toUCom`), so emission is one framework, two op-sets.
`BaseUnitary` has exactly two primitives — `R θ φ λ` (1-qubit) and `CNOT`
(2-qubit) — and `BaseUnitary 3` is empty, so a two-op IR (`UOp.u`/`UOp.cx`)
represents every `BaseUCom` with no gaps. The op `UOp.u θ φ λ n` is exactly
the OpenQASM 2.0 built-in `U(θ,φ,λ) q[n]` (whose matrix is the framework's
`rotation θ φ λ`), so the emission is a literal, faithful translation.
Machine-checked: `uprogMat_emitUComOps` is `uc_eval`-equality by structural
induction (each op's matrix is DEFINED as the corresponding `uc_eval`).
inductiveUOp
inductive UOp
A single emitted `BaseUCom` op: a general 1-qubit rotation `U(θ,φ,λ)` or a
`CX`. (`θ,φ,λ : ℝ`, so the op carries exact rotation data; text rendering of
arbitrary reals is non-computable and handled separately for circuits whose
angles are dyadic multiples of `π`.)
defmat
noncomputable def mat (dim : Nat) : UOp → Square dim | UOp.u θ φ lam n => ueval_r dim n (BaseUnitary.R θ φ lam) | UOp.cx c t => ueval_cnot dim c t
The `BaseUCom` unitary of one op at dimension `dim`. DEFINED to be the
`uc_eval` of the corresponding primitive, so faithfulness is structural.
defuprogMat
noncomputable def uprogMat (dim : Nat) : List UOp → Square dim | [] => 1 | op :: l => uprogMat dim l * op.mat dim
Unitary realised by an op program: circuit order left-to-right = matrix
product right-to-left, starting from the identity (mirrors `GateQasm.progMat`).
theoremuprogMat_append
theorem uprogMat_append (dim : Nat) (l1 l2 : List UOp) :
uprogMat dim (l1 ++ l2) = uprogMat dim l2 * uprogMat dim l1defemitUComOps
def emitUComOps {dim : Nat} : BaseUCom dim → List UOp
| UCom.seq a b => emitUComOps a ++ emitUComOps b
| UCom.app1 (BaseUnitary.R θ φ lam) n => [UOp.u θ φ lam n]
| UCom.app2 BaseUnitary.CNOT m n => [UOp.cx m n]
| UCom.app3 u _ _ _ => nomatch u*The faithful `BaseUCom` emitter.** `seq` concatenates; `app1 (R …)` and
`app2 CNOT` map to the two ops; `app3` is unreachable (`BaseUnitary 3` empty).
theoremuprogMat_emitUComOps
theorem uprogMat_emitUComOps {dim : Nat} (c : BaseUCom dim) :
uprogMat dim (emitUComOps c) = uc_eval c*★ Faithfulness ★** — the emitted op program's unitary equals the
circuit's `uc_eval`, for EVERY `BaseUCom`. The same `progMat = uc_eval`
contract the Clifford+T arithmetic emitter satisfies, now over the full
unitary IR.
theoremuprogMat_emitUComOps_toUCom
theorem uprogMat_emitUComOps_toUCom (dim : Nat) (g : FormalRV.Framework.Gate) :
uprogMat dim (emitUComOps (FormalRV.BQAlgo.Gate.toUCom dim g))
= uc_eval (FormalRV.BQAlgo.Gate.toUCom dim g)A reversible `Gate` circuit, embedded into `BaseUCom` via `Gate.toUCom`,
emits faithfully through `emitUComOps`: the emitted op program's unitary equals
the gate's `uc_eval`. This is the same `uc_eval` the arithmetic Clifford+T
emitter (`GateQasm`) targets, so arithmetic gadgets and quantum gadgets share
one emission framework.
structureUGadget
structure UGadget
defUGadget.emitQASM
def UGadget.emitQASM (g : UGadget) (n : Nat) : String
*Uniform QASM emitter for quantum gadgets.** `emitQASM g n` is the
OpenQASM 2.0 program for quantum gadget `g` at parameter `n` (e.g.
`IQFTGadget.emitQASM 3`) — the `BaseUCom` analogue of `Codegen.emitQASM`.
FormalRV.Codegen.WindowedEmitDemo
FormalRV/Codegen/WindowedEmitDemo.lean
FormalRV.Codegen.WindowedEmitDemo — END-TO-END demonstration (logical level):
1. COUNT — evaluate the structurally-proven resource counts of the windowed
multiplier and the babbush unary-iteration QROM, and the RSA-2048
cost-model Toffoli total, confirming they match Gidney–Ekerå.
2. EMIT — write runnable OpenQASM 2.0 for the full windowed multiplier
(`Gate` IR) and the babbush QROM (`EGate` IR, with measurement-uncompute).
Run: lake env lean FormalRV/Codegen/WindowedEmitDemo.lean
(writes C:/tmp/qasm_demo/{windowed_mul_w2,babbush_qrom_w2}.qasm and prints the QROM).
SEMANTICS are verified separately by `native_decide` in `FormalRV.Shor.WindowedCircuitExec`
(the multiplier computes a·y) and `FormalRV.Shor.MeasUncomputeExec` (the QROM reads T[a]);
the emitted QASM is additionally checked in Qiskit by `verify_emitted_qrom.py`.
Counts are PROVEN by `windowedMulCircuit_toffoli`, `width_windowedMulCircuit`,
`toffoli_unaryQROM`, `toffoli_babbushLookupAdd`, `toffoliCount_rsa2048`; the emitter is
PROVEN faithful by `GateQasm.emitOps_applyNat` and `EGateQasm.emitEOps_applyNat`.
(no documented top-level declarations)