Codegen 50 declarations in 5 modules
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.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
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=" ++ toString g | .Gate2q a b g => "gate2q " ++ qref a ++ "," ++ qref b ++ " gate=" ++ toString g | .Measure q bas => "measure " ++ qref q ++ " basis=" ++ toString bas | .TransitQubit q c => "transit " ++ qref q ++ " via channel=" ++ toString c | .RequestFreshAncilla z => "request_ancilla zone=" ++ toString z | .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.
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.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)