Merge pull request #2 from inQWIRE/mapping

Adding new mapping functions

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "benchmarks/VOQC-benchmarks"]
-	path = benchmarks/VOQC-benchmarks
-	url = https://github.com/inQWIRE/VOQC-benchmarks
 [submodule "extraction/SQIR"]
 	path = extraction/SQIR
 	url = https://github.com/inQWIRE/SQIR

CHANGES.md

@@ -1,3 +1,10 @@
+## 0.3.0 (2022-07-07)
+
+- Added support for a new mapping validation function (`check_swap_equivalence`).
+- Updated the interfaces of mapping-related functions.
+- Generally improved organization and documentation.
+- Moved benchmarking scripts to [VOQC-benchmarks](https://github.com/inQWIRE/VOQC-benchmarks).
+
 ## 0.2.1 (2021-06-21)
 
 - Updated to the most recent version of SQIR & extracted using Coq v8.13.2.

Makefile

@@ -4,8 +4,8 @@ install:
 uninstall:
 	dune uninstall
 
-voqc-cli:
-	dune build voqc_cli.exe
+example:
+	dune build example.exe
 
 doc:
 	dune build @doc

README.md

@@ -1,20 +1,21 @@
 # mlvoqc
 
-This repository contains OCaml code for running the VOQC quantum circuit compiler, [presented at POPL 2021](https://dl.acm.org/doi/10.1145/3434318). The `.ml` files in `ml/extracted` are *extracted* from the verified Coq definitions in `VOQC` directory of [inQWIRE/SQIR](https://github.com/inQWIRE/SQIR). For instructions on how to re-generate the extracted OCaml code from our Coq definitions see [Extraction](#extraction) below. 
+This repository contains OCaml code for running the VOQC quantum circuit compiler, [presented at POPL 2021](https://dl.acm.org/doi/10.1145/3434318). The `.ml` files in `ml/extracted` are *extracted* from the verified Coq definitions in the `VOQC` directory of [inQWIRE/SQIR](https://github.com/inQWIRE/SQIR). For instructions on how to re-generate the extracted OCaml code from our Coq definitions see [Extraction](#extraction) below. 
 
-`voqc-cli.ml` in the top-level directory provides a simple command line interface for interacting with the VOQC compiler. Instructions for compiling and running `voqc-cli.ml` are given below. **However**, we recommend using our Python wrapper available in [inQWIRE/pyvoqc](https://github.com/inQWIRE/pyvoqc) instead. The pyvoqc repository also includes a tutorial.
-
-Scripts to run VOQC on the benchmarks described in our paper are available in the `benchmarks` directory. See the README in that directory for more information.
+`example.ml` is an example OCaml program that uses the VOQC library; we include instructions for compiling and running it below. However, we recommend using our Python wrapper available in [inQWIRE/pyvoqc](https://github.com/inQWIRE/pyvoqc) instead. The pyvoqc repository also includes a tutorial.
 
 ## Table of Contents
 
-* [Setup](#setup)
-* [Installation](#installation)
-* [Usage](#usage)
-* [Documentation](#documentation)
-* [Extraction](#extraction)
-* [Contributing](#contributing)
-* [Acknowledgements](#acknowledgements)
+- [mlvoqc](#mlvoqc)
+  - [Table of Contents](#table-of-contents)
+  - [Setup](#setup)
+  - [Installation](#installation)
+  - [Usage](#usage)
+  - [Documentation](#documentation)
+  - [Extraction](#extraction)
+    - [Notes on Extraction](#notes-on-extraction)
+  - [Contributing](#contributing)
+  - [Acknowledgements](#acknowledgements)
 
 ## Setup
 
@@ -25,43 +26,38 @@ opam init
 eval $(opam env)
 
 # install some version of the OCaml compiler in a switch named "voqc"
-opam switch create voqc 4.12.0
+opam switch create voqc 4.13.1
 eval $(opam env)
 
 # install dune (needed to build VOQC)
 opam install dune
 ```
 
-*Notes*:
-* Depending on your system, you may need to replace 4.12.0 in the instructions above with something like "ocaml-base-compiler.4.12.0".
-* Opam error messages and warnings are typically informative, so if you run into trouble then make sure you read the console output.
+*Note*: opam error messages and warnings are typically informative, so if you run into trouble then make sure you read the console output.
 
 ## Installation
 
-You can install the VOQC library using the opam package manager.
+You can now install the VOQC library using the opam package manager.
 ```
 opam install voqc
 ```
-If for some reason that doesn't work, then you can also install VOQC locally using `make install`.
 
-Once you have the VOQC library installed, you can build the command line interface with `make voqc-cli`.
+Once you have the VOQC library installed, you can build the example program with `make example`.
 
 *Notes*: 
 * When building the VOQC executable on a Mac, you will likely see the warning `ld: warning: directory not found for option '-L/opt/local/lib'`. This is due to zarith (see [ocaml/opam-repository#3000](https://github.com/ocaml/opam-repository/issues/3000)) and seems to be fine to ignore.
-* If you are building VOQC locally, you may need to run `opam install openqasm` first.
+* If you decide to build mlvoqc locally (using `make install`) instead of through opam, you will need to install the OCaml OpenQASM parser (`opam install openQASM`).
 
 ## Usage
 
-Since the VOQC CLI is built using dune, you need to run it with `dune exec`. Here are a few examples:
+Since the example program is built using dune, you need to run it with `dune exec`. Here is an example run:
 ```
-# Run the "Nam" optimizations on input program <inf> and write the output to <outf>
-dune exec -- ./voqc_cli.exe -i inf -o outf -optimize-nam
-
-# Run the "Nam" and "IBM" optimizations on input program <inf> and write the output to <outf>
-dune exec -- ./voqc_cli.exe -i inf -o outf -optimize-nam -optimize-ibm
+$ dune exec -- ./example.exe -f example.qasm 
 
-# list all available options
-dune exec -- ./voqc_cli.exe --help
+Input circuit has 3 gates and uses 5 qubits.
+After decomposition to the RzQ gate set, the circuit uses 45 gates : { H : 6, X : 0, Rzq : 21, CX : 18 }.
+After mapping, the circuit uses 70 gates : { H : 6, X : 0, Rzq : 21, CX : 43 }.
+After optimization, the circuit uses 61 gates : { U1 : 14, U2 : 6, U3 : 0, CX : 41 }.
 ```
 
 VOQC supports OpenQASM programs that use the following gates:
@@ -82,9 +78,9 @@ Documentation for the VOQC library (generated with [odoc](https://github.com/oca
 
 To re-generate the extracted OCaml code (e.g. when you want to update to include new features from [inQWIRE/SQIR](https://github.com/inQWIRE/SQIR)), change into the `extraction` directory and run `./extract.sh`. This will run Coq on our `Extraction.v` file and move the generated OCaml code to the correct directory. Depending on updates made to the Coq code, you may need to modify `extract.sh` or `Extraction.v`.
 
-In order to perform extraction, you will need to have Coq installed (`opam install coq`). Extraction has only been tested with Coq versions 8.12.x and 8.13.x.
+In order to perform extraction, you will need to have Coq installed (`opam install coq`). Extraction has been tested with Coq versions 8.12-8.15.
 
-*Notes*:
+### Notes on Extraction
 
 For performance, we:
 * Extract Coq nat to OCaml int.
@@ -93,7 +89,7 @@ For performance, we:
 
 This makes the assumption that these OCaml data structures satisfy the properties proved about their corresponding Coq implementations. Note that nats are only used to identify qubit indices and we do not perform arithmetic over qubit indices, so an overflow is unlikely.
 
-Perhaps more problematic, we have decided to extract Coq's axiomatized Reals (used for continuous gate parameters) to OCaml floats. This invites the possibility of floating point rounding error, which is not accounted for in our proofs. We have not observed errors cause by this during testing, but it's something to keep in mind. We are working to come up with a better solution. To avoid this potentially-buggy feature, you can avoid the rz, u1, u2, and u3 gates in favor of the rzq gate, whose parameter is described using OCaml multi-precision rational numbers. Also, do not use the optimize_ibm, optimize_1q_gates, or cx_cancellation functions as they will interally convert to u1, u2, and u3 gates.
+Perhaps more problematic, we have decided to extract Coq's axiomatized Reals (used for continuous gate parameters) to OCaml floats. This invites the possibility of floating point rounding error, which is not accounted for in our proofs. We have not observed errors cause by this during testing, but it's something to keep in mind. We are working to come up with a better solution.
 
 ## Contributing