A Small Quantum Intermediate Representation
SQIR is a Small Quantum Intermediate Representation for quantum programs. Its intended use is as an intermediate representation in a Verified Optimizer for Quantum Circuits (VOQC), but we have also used it to implement verified versions of several quantum algorithms.
We first presented SQIR and its use in VOQC in our paper A Verified Optimizer for Quantum Circuits at POPL 2021. We provide additional details of verifying SQIR programs (including QPE and Grover's) in our paper Proving Quantum Programs Correct, presented at ITP 2021. We describe a SQIR formalization of Shor's factoring algorithm in our draft A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm.
This repository contains our Coq formalization of SQIR and VOQC as well as several verified quantum algorithms. If you are interested in running the VOQC compiler, then you should look at our OCaml library (inQWIRE/mlvoqc) or Python library (inQWIRE/pyvoqc) instead. The OCaml library is extracted from our Coq definitions and the Python library is a wrapper around the OCaml library.
If you are interested in learning more about formal verification of quantum programs in general, we recommend Robert Rand's Verified Quantum Computing tutorial.
To compile SQIR and VOQC, you will need Coq and QuantumLib (version 1.1.0). In order to build the Shor proof, you will also need the Coq Interval package and the coq-euler library. We strongly recommend using opam to install Coq and opam switch
to manage Coq versions. We currently support Coq versions 8.12-8.16. If you run into errors when compiling our proofs, first check your version of Coq (coqc -v
).
Assuming you have opam installed (following the instructions in the link above), follow the steps below to set up your environment.
# environment setup
opam init
eval $(opam env)
# install some version of the OCaml compiler in a switch named "voqc"
opam switch create voqc 4.13.1
eval $(opam env)
# install Coq -- this will take a while!
opam install coq
# install the QuantumLib library
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-quantumlib.1.1.0
# Optional, if you want to compile the proofs in examples/shor
opam install coq-interval
opam pin coq-euler https://github.com/taorunz/euler.git
Notes:
After following the setup directions above, you can run make
to compile the core files of SQIR, make voqc
to compile proofs about VOQC, make examples
to compile proofs of correctness for quantum algorithms (excluding those in examples/shor), and make shor
to compile proofs about Shor's algorithm. Use make all
to compile everything.
Our proofs are resource intensive so expect make all
to take a little while. If you have cores to spare, then you can speed things up by compiling with the -j
flag (e.g., make all -j8
). On a 2015 dual-core MacBook Pro running Coq version 8.15.2, compilation takes around 30 minutes.
To install SQIR, run
opam pin coq-sqir https://github.com/inQWIRE/SQIR.git
To pull subsequent updates, run opam install coq-sqir
.
To import SQIR files, use
Require Import SQIR.FILENAME
Definition of the SQIR language.
Verified transformations of SQIR programs. The optimizations and mapping routines extracted to our OCaml library (inQWIRE/mlvoqc) are all listed in Main.v. So this file is a good starting point for getting familiar with VOQC.
The rest of the files in the VOQC directory can be split into the following categories:
Utilities
Optimizations over unitary programs, inspired by those in Qiskit and Nam et al. [2018]
Optimizations over non-unitary programs
Mapping routines
Experimental extensions
Examples of verifying correctness properties of quantum algorithms.
make shor
to compile separately, see the README in the shor directory for more details)This project is the result of the efforts of many people. The primary contacts for this project are Kesha Hietala (@khieta) and Robert Rand (@rnrand). Other contributors include:
This project is supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Quantum Testbed Pathfinder Program under Award Number DE-SC0019040 and the Air Force Office of Scientific Research under Grant Number FA95502110051.
If you use SQIR or VOQC in your work, please cite our papers.
@article{hietala2021verified,
title = {A Verified Optimizer for {{Quantum}} Circuits},
author = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Wu, Xiaodi and Hicks, Michael},
year = {2021},
month = jan,
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
eid = {37},
pages = {37},
numpages = {29},
doi = {10.1145/3434318},
archiveprefix = {arXiv},
eprint = {1912.02250},
url = {https://github.com/inQWIRE/SQIR},
abstract = {We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.},
keywords = {programming languages, formal verification, certified compilation, quantum computing, circuit optimization},
note = {POPL '21}
}
@inproceedings{hietala2020proving,
title = {{Proving Quantum Programs Correct}},
author = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Li, Liyi and Hicks, Michael},
year = {2021},
month = jun,
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}},
address = {Dagstuhl, Germany},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {193},
eid = {21},
pages = {21:1--21:19},
doi = {10.4230/LIPIcs.ITP.2021.21},
url = {https://github.com/inQWIRE/SQIR},
abstract = {As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover's algorithm and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.},
keywords = {formal verification, quantum computing, proof engineering}
}
Alternatively, you can cite our repository using the information in CITATION.cff.