About SQIR/VOQC
Verified optimizer for quantum circuits in Coq. Provides a small quantum intermediate representation (SQIR) and the first formally verified circuit optimizer (VOQC). Focuses on gate-level optimization with proofs of semantic preservation.
Proof Assistant and Foundation
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Proof assistant | Coq (v8.x) | Lean 4 |
| Language paradigm | Gallina (dependently typed functional) | Lean 4 (dependently typed, do-notation, monads) |
| Code extraction | Coq extraction to OCaml (trusted) | Native compilation; no extraction needed |
| Tactic language | Ltac / Ltac2 | Lean 4 metaprogramming framework |
| Math library | Custom matrix/complex libraries (built on QWIRE's) | Mathlib (comprehensive, community-maintained) |
Abstraction Level
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Level | Quantum circuit (gate sequences) | Program-level (Dirac notation + classical expressions) |
| Program model | U := U1; U2 | G q | G q1 q2 — sequence of gate applications | Layered: CExpr -> Label -> Dirac -> LDirac -> Program |
| Classical control | Branching measurement only (meas q P1 P2) | Native classical expressions, data types, arrays |
| Notation | Dirac notation used informally in proofs only | First-class Dirac notation AST with formal semantics |
| Target use | Close to hardware execution | Close to textbook mathematical notation |
Quantum State Representation
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Matrix definition | Functions N -> N -> C with phantom type dimensions | Mathlib Matrix with DataType-indexed dimensions |
| Well-formedness | External WF_Matrix predicate (M i j = 0 outside bounds) | Enforced by Lean/Mathlib type system (Fintype indices) |
| Ill-typed denotation | Zero matrix (simplifies proofs) | Option.none (explicit failure) |
| Gate lifting | Tensor products with identity matrices (apply_1, apply_2) | Access path model with register atom reindexing |
| Register model | Natural number indices into global register | Named register labels with hierarchical access paths |
Type System
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Complexity | Minimal: gate set + register size, bounds checking | Rich: DataType, DiracSort, UnifiedContext, DTIso |
| Qubit identity | Concrete numeric indices (m != n means different qubits) | Named variables with structured access paths |
| Register arrays | Not supported | First-class: DataType.array n t with arrayIdx |
| Big operators | Not supported | bigSum and bigTsr for parametric system size |
| Design rationale | Simplicity — concrete indices simplified proofs vs QWIRE's abstract approach | Expressiveness — named registers for algorithm-level reasoning |
Optimization and Compilation
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Optimizer | VOQC: 5+ verified optimization passes (not propagation, Hadamard reduction, gate cancellation, rotation merging, circuit mapping) | Not targeted; compilation is future work |
| Verified compilation | SQIR -> OpenQASM translator; circuit mapping for hardware connectivity | Planned (roadmap item D) |
| Performance | 17.8% total gate reduction, 41.4% T-gate reduction on 28 benchmarks | N/A |
| Gate set | {H, X, Rz(k), CNOT} with rational rotation parameters | Any operator expressible in Dirac notation |
| Hardware mapping | Verified for Tenerife, LNN, ring, 2D grid topologies | Not yet addressed |
Automation
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Key tactic | gridify: normalizes matrix expressions into grid normal form | dirac_eq: certified term rewriting for Dirac equalities |
| Target domain | Circuit-level matrix equivalences (up to ~5 qubits) | Mathematical-level Dirac notation equalities |
| Gate list framework | Library functions for manipulating SQIR programs as gate lists | Dirac term AST with evaluation semantics |
| Well-formedness automation | Phantom types reduce proof burden | Type inference functions produce typing derivations |
Case Studies
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| GHZ state preparation | Verified (arbitrary n) | Not yet |
| Quantum teleportation | Verified (fixed n=3) | Not yet |
| Deutsch-Jozsa | Verified | Dirac encoding available |
| Grover's search | Verified | Not yet |
| QPE | Verified | Not yet |
| Circuit optimizations | 28 benchmarks verified correct | Not targeted |
| Dirac identities | Not formalized | Encoded and verified (QCQI, Pauli, KLM) |
Complementarity
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Compilation backend | Could serve as SQIR target for Fanal's compilation pipeline | Could compile programs down to SQIR circuits |
| Proof technique sharing | gridify tactic for matrix normalization | D-Hammer-inspired decision procedures for Dirac |
| Cross-verification | Circuit-level algorithm implementations as reference | Program-level encodings for cross-validation |
| Limitation | Different proof assistants (Coq vs Lean 4) — requires porting | Different proof assistants (Lean 4 vs Coq) — requires porting |
Summary: Key Differences
| Aspect | SQIR/VOQC | Fanal |
|---|---|---|
| Proof System | Coq (Calculus of Constructions) | Lean 4 (CIC with quotients) |
| Abstraction Level | Gate-level circuits (SQIR IR) | High-level quantum programs |
| Primary Goal | Verified circuit optimization | Program verification & reasoning |
| Compilation | Verified compilation to OpenQASM | Compilation planned |
| Expressiveness | No loops or classical control | Classical-quantum language with loops |