From Verified Compilation to Shor's Algorithm
summary
A verified compiler stack implements a small IR called Squire and a proven optimizer Vox that preserves denotational semantics across rewrites. The project contains about 3,900 LOC of source and 3,500 LOC of proofs, proves optimizations like NOT propagation and rotation merging, cuts total gate count ~19% on benchmarks, and connects a verified reversible arithmetic compiler to Squire to produce a full, end‑to‑end verified implementation of Shor’s algorithm (≈10,000 LOC) validated on a simulator up to 200.
AI-written summary · about
chapters (22)
- 0:00Intro
- 0:30Quantum Programming is Hard
- 1:44Verified Quantum Programming
- 3:04Goal: Verified Compiler Stack
- 4:15Our Work: SQIR and VOQC
- 6:00Outline
- 7:36Unitary SQIR
- 12:04SQIR Metaprogramming
- 13:27Proofs of Correctness in Coq
- 14:51SQIR's Design for Proof
- 17:44Proofs so far
- 18:28VOQC: Verified Optimizer for Quantum Circuits
- 19:13Semantics Preservation
- 19:47Example: X Propagation
- 24:00Verifying Matrix Equivalences
- 24:44Circuit Mapping
- 25:32Evaluation
- 25:57Benchmark
- 26:58Summary Results
- 28:15Verified Shor's Algorithm
- 29:52Challenges
- 31:54Summary and Future Work
related talks
24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
29mA Verified Optimizer for Quantum Circuits
33mVerified Compilation of Quantum Oracles
16mCompiling and Running High-level Quantum Programs
39mBuilding a Compiler for Quantum Computers
29mEfficiently Verifying Quantum Programs with Few T Gates
22mEfficient Formal Verification of Quantum Error Correcting Programs
01h 10mThe Rise & Collapse of a Quantum State