various updates to build system & directions for extraction

Makefile

@@ -1,8 +1,6 @@
 .DEFAULT_GOAL := sqir
 
 all:
-	git submodule init;
-	git submodule update;
 	@dune build
 
 sqir: FORCE
@@ -12,12 +10,11 @@ voqc: FORCE
 	@dune build VOQC
 
 examples: FORCE
-	@dune build examples
+	@dune build examples/examples
+	@dune build examples/ghz
 
 shor:
-	git submodule init;
-	git submodule update;
-	@dune build shor
+	@dune build examples/shor
 
 clean:
 	@dune clean

README.md

@@ -14,22 +14,21 @@ If you are interested in learning more about formal verification of quantum prog
 
 ## Table of Contents
 
-- [SQIR & VOQC](#sqir--voqc)
+- [SQIR \& VOQC](#sqir--voqc)
   - [Table of Contents](#table-of-contents)
   - [Setup](#setup)
   - [Compilation](#compilation)
-  - [Using With Other Projects]()
+  - [Using With Other Projects](#using-with-other-projects)
   - [Directory Contents](#directory-contents)
     - [SQIR](#sqir)
-    - [externals](#externals)
     - [VOQC](#voqc)
     - [examples](#examples)
   - [Acknowledgements](#acknowledgements)
   - [Citations](#citations)
 
 ## Setup
 
-To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/), [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.1.0), and the [Coq Interval package](http://coq-interval.gforge.inria.fr/). We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) to install Coq and `opam switch` to manage Coq versions. We currently support Coq **versions 8.12-8.15**. If you run into errors when compiling our proofs, first check your version of Coq (`coqc -v`).
+To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/) and [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.1.0). In order to build the Shor proof, you will also need the [Coq Interval package](http://coq-interval.gforge.inria.fr/) and the [coq-euler](https://github.com/taorunz/euler) library. We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) 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.
 ```
@@ -44,16 +43,14 @@ eval $(opam env)
 # install Coq -- this will take a while!
 opam install coq
 
-# install dune 
-opam install dune
-
 # install the QuantumLib library
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam update
 opam install coq-quantumlib.1.1.0
 
-# install Interval package (optional, needed to compile proofs in examples/shor)
+# 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*:
@@ -93,10 +90,6 @@ Definition of the SQIR language.
 - UnitaryOps.v : Utilities for manipulating unitary SQIR programs.
 - UnitarySem.v : Semantics for unitary SQIR programs.
 
-### externals
-
-External dependencies linked as git submodules. Currently, our proof of Shor's algorithm depends on the number theory in the [euler](https://github.com/taorunz/euler) development.
-
 ### VOQC
 
 Verified transformations of SQIR programs. The optimizations and mapping routines extracted to our OCaml library ([inQWIRE/mlvoqc](https://github.com/inQWIRE/mlvoqc)) are all listed in **Main.v**. So this file is a good starting point for getting familiar with VOQC.
@@ -128,6 +121,7 @@ The rest of the files in the VOQC directory can be split into the following cate
   - GreedyLayout.v : Generate a layout based on the input program and architecture.
   - Layouts.v : Utilities for describing a physical <-> logical qubit mapping (i.e., layout).
   - MappingConstraints.v : Utilities for describing a program that satisfies architecture constraints.
+  - MappingGateSet.v : Mapping gate set U + {CX, SWAP}, where U is an arbitrary set of single-qubit gates.
   - MappingValidation.v : Check whether two programs (which differ only in SWAP placement) are equivalent.
   - SwapRoute.v: Simple mapping for an architecture described by a directed graph.
 
@@ -166,10 +160,6 @@ This project is the result of the efforts of many people. The primary contacts f
 * Runzhou Tao
 * Finn Voichick
 
-Maintainers:
-* Kesha Hietala (@khieta)
-* Robert Rand (@rnrand)
-
 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.
 
 ## Citations

VOQC/dune

@@ -1,3 +1,4 @@
 (coq.theory
   (name VOQC)
-  (package coq-voqc))
+  (package coq-voqc)
+  (theories SQIR))

_CoqProject

@@ -2,4 +2,3 @@
 -R _build/default/examples/examples Examples
 -R _build/default/examples/shor Shor
 -R _build/default/VOQC VOQC
--R _build/default/examples/shor/externals/euler Shor.externals.euler

coq-sqir.opam

@@ -3,7 +3,7 @@ opam-version: "2.0"
 version: "1.1.0"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
-inQWIRE's VOQC is a Coq library for reasoning
+inQWIRE's SQIR is a Coq library for reasoning
  about quantum circuits
 """
 maintainer: ["inQWIRE Developers"]
@@ -13,7 +13,6 @@ homepage: "https://github.com/inQWIRE/SQIR"
 bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq-interval" {>= "4.6.1"}
   "coq-quantumlib" {>= "1.1.0"}
   "coq" {>= "8.12"}
   "odoc" {with-doc}

coq-voqc.opam

@@ -3,8 +3,8 @@ opam-version: "2.0"
 version: "1.1.0"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
-inQWIRE's VOQC is a Coq tool for verified
- compilation of quantum circuits, with some common gate sets
+inQWIRE's VOQC is a Coq library for verified
+ optimization of quantum circuits
 """
 maintainer: ["inQWIRE Developers"]
 authors: ["inQWIRE"]
@@ -13,7 +13,6 @@ homepage: "https://github.com/inQWIRE/SQIR"
 bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq-interval" {>= "4.6.1"}
   "coq-quantumlib" {>= "1.1.0"}
   "coq-sqir" {>= "1.1.0"}
   "coq" {>= "8.12"}

dune-project

@@ -1,5 +1,5 @@
 (lang dune 2.8)
-(name coq-sqirvoqc)
+(name coq-sqir-voqc)
 (version 1.1.0)
 (using coq 0.2)
 
@@ -13,22 +13,20 @@
 (package
  (name coq-sqir)
  (synopsis "Coq library for reasoning about quantum circuits")
- (description "\| inQWIRE's VOQC is a Coq library for reasoning
+ (description "\| inQWIRE's SQIR is a Coq library for reasoning
               "\|  about quantum circuits
  )
  (depends
-   (coq-interval (>= 4.6.1))
    (coq-quantumlib (>= 1.1.0))
    (coq (>= 8.12))))
 
 (package
  (name coq-voqc)
  (synopsis "A verified optimizer for quantum compilation")
- (description "\| inQWIRE's VOQC is a Coq tool for verified
-              "\|  compilation of quantum circuits, with some common gate sets
+ (description "\| inQWIRE's VOQC is a Coq library for verified
+              "\|  optimization of quantum circuits
  )
  (depends
-   (coq-interval (>= 4.6.1))
    (coq-quantumlib (>= 1.1.0))
    (coq-sqir (>= 1.1.0))
    (coq (>= 8.12))))

examples/examples/dune

@@ -2,4 +2,4 @@
 
 (coq.theory
   (name Examples)
-  (theories SQIR ghz))
+  (theories SQIR))

examples/ghz/README.md

@@ -0,0 +1,9 @@
+# GHZ Example
+
+This directory contains an implementation and proof of GHZ state preparation, plus an example for how to extract Coq/SQIR programs to OCaml/OpenQASM 2.0. You can use this as a model for extracting other SQIR programs.
+
+How to "run" GHZ:
+1. Run `make examples` in the top-level directory (`../..`). This compiles the GHZ Coq definitions and proofs (along with several other examples) and the extracted OCaml code in the `extraction/` directory.
+2. In the current directory, run `dune exec --root extraction -- ./ghz.exe N` where N is the number of qubits you want in the GHZ state. This runs our OCaml executable (`ghz.exe`) on the input `N`. It will produce a file called `ghz.qasm` that contains the generated OpenQASM code.
+
+The code in the `extraction/` directory was generated using the `./extract.sh` script. You can re-generate the extracted code using this script. Note that it was last tested with Coq version 8.15.2. Other versions of Coq will likely require modifications.

examples/examples/ghz/dune → examples/ghz/dune

@@ -1,4 +1,3 @@
-
 (coq.theory
   (name ghz)
   (theories SQIR))

examples/examples/ghz/extract.sh → examples/ghz/extract.sh

@@ -5,10 +5,10 @@ cd extraction
 
 # Perform extraction.
 echo "Extracting code..."
-coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlList.v
-coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlR.v
-coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlNatZ.v
-coqc -R ../../.. Top Extraction.v
+coqc ExtrOcamlList.v
+coqc ExtrOcamlNatZ.v
+coqc -R ../../../_build/default/SQIR SQIR ExtrOcamlR.v
+coqc -R ../../../_build/default/SQIR SQIR -R ../../../_build/default/examples/ghz ghz Extraction.v
 
 # Remove unneeded files.
 echo "Deleting unneeded files..."

examples/ghz/extraction/ExtrOcamlList.v

@@ -0,0 +1,13 @@
+Require Coq.extraction.Extraction.
+Require Export List.
+
+(* A few common list functions *)
+Extract Constant length => "(fun l -> Z.of_int (List.length l))".
+Extract Inlined Constant app => "List.append".
+Extract Inlined Constant rev => "List.rev".
+Extract Inlined Constant rev_append => "List.rev_append".
+Extract Inlined Constant List.map => "List.map".
+Extract Inlined Constant fold_right => "(fun f a l -> List.fold_right f l a)".
+Extract Inlined Constant forallb => "List.for_all".
+Extract Inlined Constant List.tl => "List.tl".
+Extract Inlined Constant List.hd_error => "(fun l -> List.nth_opt l 0)".

examples/ghz/extraction/ExtrOcamlNatZ.v

@@ -0,0 +1,18 @@
+Require Coq.extraction.Extraction.
+Require Import ZArith.
+
+(* Custom extraction from nat -> OCaml Z (arbitrary precision integers) *)
+Extract Inductive nat => "Z.t" [ "Z.zero" "Z.succ" ]
+  "(fun fO fS n -> if Z.equal n Z.zero then fO () else fS (Z.pred n))".
+Extract Constant Nat.pred => "(fun a -> Z.max (Z.pred a) Z.zero)".
+Extract Inlined Constant Nat.add => "Z.add".
+Extract Constant Nat.sub => "(fun a b -> Z.max (Z.sub a b) Z.zero)".
+Extract Inlined Constant Nat.mul => "Z.mul".
+Extract Inlined Constant Nat.div => "Z.div".
+Extract Inlined Constant Nat.modulo => "Z.rem".
+Extract Constant Nat.pow => "(fun a b -> Z.pow a (Z.to_int b))".
+Extract Inlined Constant Nat.gcd => "Z.gcd".
+Extract Constant Nat.log2 => "fun n -> (Z.of_int (Z.log2 n))".
+Extract Inlined Constant Nat.eqb => "Z.equal".
+Extract Inlined Constant Nat.leb => "Z.leq".
+Extract Inlined Constant Nat.ltb => "Z.lt".

examples/ghz/extraction/ExtrOcamlR.v

@@ -0,0 +1,29 @@
+Require Coq.extraction.Extraction.
+Require Export Reals.
+Require Import ExtractionGateSet.
+
+(* Custom extraction from R -> OCaml float. *)
+Extract Inlined Constant R => "float".
+Extract Inlined Constant R0 => "0.0".
+Extract Inlined Constant R1 => "1.0".
+Extract Inlined Constant R2 => "2.0".
+Extract Inlined Constant R4 => "4.0".
+Extract Inlined Constant Rplus => "( +. )".
+Extract Inlined Constant Rmult => "( *. )".
+Extract Inlined Constant Ropp => "((-.) 0.0)".
+Extract Inlined Constant Rinv => "((/.) 1.0)".
+Extract Inlined Constant Rminus => "( -. )".
+Extract Inlined Constant Rdiv => "( /. )".
+Extract Inlined Constant pow => "(fun a b -> a ** Z.to_float b)".
+Extract Inlined Constant cos => "cos".
+Extract Inlined Constant sin => "sin".
+Extract Inlined Constant tan => "tan".
+Extract Inlined Constant atan => "atan".
+Extract Inlined Constant acos => "acos".
+Extract Inlined Constant PI => "Float.pi".
+Extract Inlined Constant IZR => "Z.to_float".
+Extract Inlined Constant INR => "Z.to_float".
+
+(* Extracting the following to dummy values to supress warnings *)
+Extract Constant ClassicalDedekindReals.sig_forall_dec  => "failwith ""Invalid extracted value"" ".
+Extract Constant ClassicalDedekindReals.DRealRepr  => "failwith ""Invalid extracted value"" ".

examples/ghz/extraction/dune

@@ -0,0 +1,3 @@
+(executable
+  (name ghz)
+  (libraries Ghz_ml unix))

examples/examples/ghz/extraction/ml/dune → examples/ghz/extraction/ml/dune

@@ -1,5 +1,5 @@
 (library
-  (name ml)
+  (name Ghz_ml)
   (wrapped false)
   (flags (:standard -w -3-32-33-34-39))
   (libraries zarith unix))

examples/shor/README.md

@@ -16,7 +16,7 @@ Core formalization
 
 Utilities
 * ContFrac.v - Results about continued fractions.
-* EulerTotient.v - Re-statement of Euler's totient function from externals/euler.
+* EulerTotient.v - Re-statement of Euler's totient function from the [coq-euler](https://github.com/taorunz/euler) library.
 * ExtrShor.v - Shor's algorithm defined in a gate set amenable to extraction; proofs that the new definition is equivalent to the original.
 * NumTheory.v - General number theory results.
 * Reduction.v - Proof of the reduction from factorization to order finding.
@@ -30,16 +30,17 @@ Compiling the extracted code requires dune and zarith (`opam install dune zarith
 
 Our extracted code uses the [ddsim simulator](https://github.com/iic-jku/ddsim) (through its Qiskit interface) to execute Shor's order finding circuit so running our extracted code requires **Python version >= 3.6, qiskit, and ddsim**. Once you have a suitable version of Python, you can install the latter two with `pip install qiskit jkq.ddsim`. If you run into trouble with your Python environment, then consider using anaconda per [these directions for installing Qiskit](https://qiskit.org/documentation/getting_started.html). 
 
-To test your Python setup, run `python run_circuit.py test.qasm`. You should see the output 7, which corresponds to measuring '111'. Our OCaml code runs this command with a generated order finding circuit as input. If you find that you need to run a different command on your system (e.g., `python3.9 ...`), then you can modify line 45 of [extraction/ml/Run.ml](extraction/ml/Run.ml).
+To test your Python setup, run `python run_circuit.py test.qasm`. You should see the output 7, which corresponds to measuring '111'. Our OCaml code runs this command with a generated order finding circuit as input. If you find that you need to run a different command on your system (e.g., `python3.9 ...`), then you can modify line 47 of [extraction/ml/Run.ml](extraction/ml/Run.ml).
 
 ### Extraction to OCaml
 
-The first step is to compile the Coq code. You can do this by running `make shor` in the top-level (`../..`) directory. The next step is to extract the compiled Coq code to OCaml by running `./extract.sh` in the current directory. This will produce a bunch of .ml files in `extraction/ml` and compile them into an executable in `extraction/_build`.
+You can compile the Coq code and extracted OCaml code in the `extraction/` directory by running `make shor` in the top-level (`../..`) directory.
+
+The code in the `extraction/` directory was generated using the `./extract.sh` script. You can re-generate and re-build the extracted code using this script. Note that it was last tested with Coq version 8.15.2. Other versions of Coq will likely require modifications.
 
 If you are on MacOS, you may see the following warnings:
 ```
 ld: warning: directory not found for option '-L/opt/local/lib'
-ld: warning: directory not found for option '-L/opt/homebrew/lib'
 ```
 This is caused by our use of zarith, and seems to be safe to ignore.
 

examples/shor/dune

@@ -1,5 +1,3 @@
-(include_subdirs qualified)
-
 (coq.theory
   (name Shor)
   (theories SQIR Examples))

examples/shor/extract.sh

@@ -5,10 +5,10 @@ cd extraction
 
 # Perform extraction.
 echo "Extracting code..."
-coqc -R ../../.. Top ExtrOcamlList.v
-coqc -R ../../.. Top ExtrOcamlR.v
-coqc -R ../../.. Top ExtrOcamlNatZ.v
-coqc -R ../../.. Top Extraction.v
+coqc ExtrOcamlList.v
+coqc ExtrOcamlNatZ.v
+coqc -R ../../../_build/default/SQIR SQIR ExtrOcamlR.v
+coqc -R ../../../_build/default/SQIR SQIR -R ../../../_build/default/examples/examples Examples -R ../../../_build/default/examples/shor Shor Extraction.v
 
 # Remove unneeded files.
 echo "Deleting unneeded files..."
@@ -23,7 +23,7 @@ rm -f Bin* ClassicalDedekindReals.ml ConstructiveCauchyReals.ml NumTheory.ml \
 echo "Moving generated files to ml/..."
 mv ExtractionGateSet.ml ContFrac.ml Datatypes.ml DiscreteProb.ml ExtrShor.ml \
    List0.ml Main.ml ModMult.ml Nat.ml PeanoNat.ml RCIR.ml RealAux.ml \
-   Rfunctions.ml Shor.ml \
+   Shor.ml Summation.ml \
    ml
 
 # Build extracted code.

examples/shor/extraction/Extraction.v

@@ -1,5 +1,5 @@
 Require Coq.extraction.Extraction.
-Require Import DiscreteProb.
+Require Import QuantumLib.DiscreteProb.
 Require Import Shor.
 Require Import Main.
 

examples/shor/extraction/dune

@@ -1,3 +1,4 @@
 (executable
   (name run_shor)
-  (libraries ml unix))
+  (flags (:standard -w -32))
+  (libraries Shor_ml unix))