Add artifact

Dockerfile

@@ -0,0 +1,68 @@
+FROM ubuntu:22.04
+
+RUN apt-get update && apt-get install -y time unzip python3 python3-pip opam cabal-install cargo openjdk-17-jre-headless cmake
+RUN pip install pytket==1.18.0 qiskit==0.44.1
+RUN opam init --disable-sandboxing --compiler=4.13.1 --shell-setup && eval $(opam env) && opam install core core_unix ppx_deriving -y && opam pin add voqc 0.3.0 -y
+RUN cabal update && cabal v1-install alex happy
+
+WORKDIR /root
+ADD https://github.com/meamy/feynman/archive/cc053850a6bf06ecbf6378cd68c9fcf0c90a308b.zip feynman.zip
+RUN unzip feynman.zip && mv feynman-cc053850a6bf06ecbf6378cd68c9fcf0c90a308b feynman
+ADD https://github.com/Quantomatic/quizx/archive/5299303c9d64c2e9fec1d49c0248321e2591fa27.zip quizx.zip
+RUN unzip quizx.zip && mv quizx-5299303c9d64c2e9fec1d49c0248321e2591fa27 quizx
+ADD https://github.com/inQWIRE/mlvoqc/archive/3e6b6222937e949f395fc2f193425d45cad0ad4d.zip mlvoqc.zip
+RUN unzip mlvoqc.zip && mv mlvoqc-3e6b6222937e949f395fc2f193425d45cad0ad4d mlvoqc
+ADD https://github.com/quantum-compiler/quartz/archive/0c4afdba4bb5637c2a68637d7da2af4784b3b512.zip quartz.zip
+RUN unzip quartz.zip && mv quartz-0c4afdba4bb5637c2a68637d7da2af4784b3b512 quartz
+
+WORKDIR /root/feynman
+RUN cabal v1-install --bindir=. && cp feynopt /root/feynopt
+
+WORKDIR /root
+RUN mkdir queso
+WORKDIR /root/queso
+ADD SymbolicOptimizer-1.0-SNAPSHOT-jar-with-dependencies.jar ./
+# Generate rules
+RUN java --enable-preview -cp SymbolicOptimizer-1.0-SNAPSHOT-jar-with-dependencies.jar EnumeratorPrune -g nam -q 3 -s 6
+
+WORKDIR /root/quizx/quizx
+# Add frontend runner script
+ADD run_quizx.rs src/bin/simp_and_extract.rs
+RUN cargo build --release && cp target/release/simp_and_extract /root/run_quizx
+
+WORKDIR /root/mlvoqc
+# Add frontend runner script
+ADD run_voqc.ml example.ml
+RUN eval $(opam env) && make example && cp _build/default/example.exe /root/run_voqc
+
+WORKDIR /root/quartz
+# Add frontend runner script
+ADD run_quartz.cpp src/test/test_nam.cpp
+# Modify CMakeLists.txt to exclude python bindings
+RUN sed -i -e '5,31d' -e 's/pybind11::embed//' CMakeLists.txt
+# Remove python bindings and simulator from source
+RUN rm -r src/quartz/pybind src/quartz/simulator
+RUN mkdir build
+WORKDIR build
+# Generate rules
+RUN cmake .. && make gen_ecc_set && ./gen_ecc_set && mv 3_2_5_complete_ECC_set.json ../
+RUN make test_nam && cp test_nam /root/run_quartz
+
+WORKDIR /root
+ADD tower-src/ ./tower-src/
+WORKDIR /root/tower-src
+RUN eval $(opam env) && make && cp tower /root
+
+WORKDIR /root
+ADD circuits.tar.xz reference_outputs.tar.xz ./
+ADD run_feynopt_mctExpand.sh run_feynopt_toCliffordT.sh ./
+ADD run_quizx.sh run_quizx_big.sh ./
+ADD run_voqc.sh ./
+ADD run_quartz.sh ./
+ADD run_queso.sh ./
+ADD run_pytket_zx.py run_pytket_zx.sh run_pytket_peephole.py run_pytket_peephole.sh ./
+ADD run_qiskit.py run_qiskit.sh run_qiskit_big.sh ./
+ADD gen_circuits.sh gen_qasm.sh run_timing.sh run_timing_big.sh ./
+ADD count_T.py to_qasm.py ./
+ADD length_simplified.twr ./
+ADD run.sh run_fast.sh ./

README.md

@@ -0,0 +1,28 @@
+# Spire Artifact
+
+This is the artifact for the paper "The _T_-Complexity Costs of Error Correction for Control Flow in Quantum Computation" by Charles Yuan and Michael Carbin. It contains the sources for the Spire compiler, the benchmark programs and circuits used in the paper, and the evaluation package.
+
+The artifact requires [Docker Desktop](https://www.docker.com/products/docker-desktop/) to be installed. To build and run, first download `circuits.tar.xz` and `reference_outputs.tar.xz` from the Releases on the right and copy these two archives into this repository. Then, run
+
+```[shell]
+docker build -t spire-artifact .
+docker run --name spire -it spire-artifact /bin/bash
+```
+
+Then, inside the Docker shell, you can find the sources in `tower-src/`, the benchmark programs in `tower-src/tests/` and `length_simplified.twr`, and their corresponding circuits in `circuits/`.
+
+The evaluation package consists of the scripts in the main directory.  The `reference_output/` directory contains the pre-generated outputs of these scripts, and can be regenerated by running each script whose name starts with `run`.
+
+To run all of the fast benchmarks (takes ~1hr), run
+
+```[shell]
+./run_fast.sh
+```
+
+To run all of the benchmarks from the paper (takes several days), run
+
+```[shell]
+./run.sh
+```
+
+Note that timing results will vary depending on the machine used. Also, certain optimizers, in particular Qiskit, Quartz, and QUESO, sometimes produce nondeterministic results, so the outputs may not match exactly.

count_T.py

@@ -0,0 +1,41 @@
+#!/usr/bin/env python3
+
+import fileinput
+
+count = 0
+T_PER_TOFFOLI = 7
+
+TOFFOLI_GATES = {"tof", "ccx", "ccz"}
+T_GATES = {"t", "tdg", "t*",
+           # Used by QuiZX
+           "rz(0.25*pi)", "rz(-0.25*pi)", "rz(0.75*pi)", "rz(-0.75*pi)",
+           # Used by Qiskit
+           # Note: Qiskit produces floating points such as 0.2961504522271827.
+           # In these cases, we report an undercount of Qiskit's T-complexity.
+           "rz(pi/4)", "rz(-pi/4)",
+           # Used by VOQC
+           "rzq(1,4)", "rzq(3,4)", "rzq(5,4)", "rzq(7,4)",
+           # Used by Pytket
+           # Note: Pytket produces floating points such as 3.914666934476273*pi.
+           # In these cases, we report an undercount of Pytket's T-complexity.
+           "rz(1.25*pi)", "rz(1.75*pi)",
+           "rz(2.25*pi)", "rz(2.75*pi)",
+           "rz(3.25*pi)", "rz(3.75*pi)",
+           # Used by QUESO
+           # Note: QUESO produces floating points that are a mix of multiples of
+           # pi/2 and pi/4.
+           "rz(pi/4.0)", "rz(-pi/4.0)",
+           "rz(-0.7853981633974483)", "rz(0.7853981633974483)"}
+
+for line in fileinput.input():
+    try:
+        gate = line.split(maxsplit=1)[0].lower()
+        if gate in TOFFOLI_GATES:
+            c = line.count(" ")
+            if c >= 3:
+                count += ((c - 3) * 2 + 1) * T_PER_TOFFOLI
+        elif gate in T_GATES:
+            count += 1
+    except IndexError:
+        pass
+print(count)

gen_circuits.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+
+TOWER_ROOT=tower-src
+set -x
+mkdir -p circuits circuits/qc
+
+for i in {1..10}
+do
+./tower -c --optimize_lir --word_size 2 --mem_size 4 --dotQC -b length:$i $TOWER_ROOT/tests/list.twr length_simplified.twr > circuits/qc/length_simplified$i.qc
+./tower -c --optimize_lir --disable_with_do --word_size 2 --mem_size 4 --dotQC -b length:$i $TOWER_ROOT/tests/list.twr length_simplified.twr > circuits/qc/length_simplified_only_cf$i.qc
+./tower -c --optimize_lir --disable_nested_if --word_size 2 --mem_size 4 --dotQC -b length:$i $TOWER_ROOT/tests/list.twr length_simplified.twr > circuits/qc/length_simplified_only_cn$i.qc
+./tower -c --word_size 2 --mem_size 4 --dotQC -b length:$i $TOWER_ROOT/tests/list.twr length_simplified.twr > circuits/qc/length_simplified_orig$i.qc
+
+./tower -c --optimize_lir --dotQC -b length:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/length.twr > circuits/qc/length$i.qc
+./tower -c --dotQC -b length:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/length.twr > circuits/qc/length_orig$i.qc
+
+./tower -c --optimize_lir --dotQC -b sum:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/sum.twr > circuits/qc/sum$i.qc 2> circuits/sum$i.log
+./tower -c --dotQC -b sum:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/sum.twr > circuits/qc/sum_orig$i.qc 2> circuits/sum_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b find_pos:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/find_pos.twr > circuits/qc/find_pos$i.qc 2> circuits/find_pos$i.log
+./tower -c --dotQC -b find_pos:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/find_pos.twr > circuits/qc/find_pos_orig$i.qc 2> circuits/find_pos_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b remove:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/remove.twr > circuits/qc/remove$i.qc 2> circuits/remove$i.log
+./tower -c --dotQC -b remove:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/remove.twr > circuits/qc/remove_orig$i.qc 2> circuits/remove_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b push_back:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/queue.twr > circuits/qc/push_back$i.qc 2> circuits/push_back$i.log
+./tower -c --dotQC -b push_back:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/queue.twr > circuits/qc/push_back_orig$i.qc 2> circuits/push_back_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b pop_front:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/queue.twr > circuits/qc/pop_front$i.qc 2> circuits/pop_front$i.log
+./tower -c --dotQC -b pop_front:$i $TOWER_ROOT/tests/list.twr $TOWER_ROOT/tests/queue.twr > circuits/qc/pop_front_orig$i.qc 2> circuits/pop_front_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b is_prefix:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/is_prefix$i.qc 2> circuits/is_prefix$i.log
+./tower -c --dotQC -b is_prefix:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/is_prefix_orig$i.qc 2> circuits/is_prefix_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b num_matching:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/num_matching$i.qc 2> circuits/num_matching$i.log
+./tower -c --dotQC -b num_matching:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/num_matching_orig$i.qc 2> circuits/num_matching_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b compare:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/compare$i.qc 2> circuits/compare$i.log
+./tower -c --dotQC -b compare:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr > circuits/qc/compare_orig$i.qc 2> circuits/compare_orig$i.log
+done
+
+for i in {1..10}
+do
+./tower -c --optimize_lir --dotQC -b insert:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr $TOWER_ROOT/tests/radix_tree.twr > circuits/qc/insert$i.qc 2> circuits/insert$i.log
+./tower -c --dotQC -b insert:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr $TOWER_ROOT/tests/radix_tree.twr > circuits/qc/insert_orig$i.qc 2> circuits/insert_orig$i.log
+
+./tower -c --optimize_lir --dotQC -b contains:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr $TOWER_ROOT/tests/radix_tree.twr > circuits/qc/contains$i.qc 2> circuits/contains$i.log
+./tower -c --dotQC -b contains:$i $TOWER_ROOT/tests/word.twr $TOWER_ROOT/tests/string_word.twr $TOWER_ROOT/tests/radix_tree.twr > circuits/qc/contains_orig$i.qc 2> circuits/contains_orig$i.log
+done

gen_qasm.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -x
+mkdir -p circuits/qasm
+
+# Convert Toffoli to CCZ by inserting two Hadamard gates
+to_ccz() {
+    sed -E 's/ccx(.*) q\[(.*)\];/h q[\2];\nccz\1 q[\2];\nh q[\2];/g' $1
+}
+
+# feynopt -mctExpand without -O2 only converts MCX to Toffoli without any optimization
+for i in {1..10}
+do
+./feynopt -mctExpand circuits/qc/length_simplified$i.qc | ./to_qasm.py > circuits/qasm/length_simplified$i.qasm
+./feynopt -mctExpand circuits/qc/length_simplified_only_cf$i.qc | ./to_qasm.py > circuits/qasm/length_simplified_only_cf$i.qasm
+./feynopt -mctExpand circuits/qc/length_simplified_only_cn$i.qc | ./to_qasm.py > circuits/qasm/length_simplified_only_cn$i.qasm
+to_ccz circuits/qasm/length_simplified$i.qasm > circuits/qasm/length_simplified_ccz$i.qasm
+./feynopt -mctExpand circuits/qc/length$i.qc | ./to_qasm.py > circuits/qasm/length$i.qasm
+to_ccz circuits/qasm/length$i.qasm > circuits/qasm/length_ccz$i.qasm
+done
+
+for i in {1..10}
+do
+./feynopt -mctExpand circuits/qc/length_simplified_orig$i.qc | ./to_qasm.py > circuits/qasm/length_simplified_orig$i.qasm
+to_ccz circuits/qasm/length_simplified_orig$i.qasm > circuits/qasm/length_simplified_orig_ccz$i.qasm
+./feynopt -mctExpand circuits/qc/length_orig$i.qc | ./to_qasm.py > circuits/qasm/length_orig$i.qasm
+to_ccz circuits/qasm/length_orig$i.qasm > circuits/qasm/length_orig_ccz$i.qasm
+done

length_simplified.twr

@@ -0,0 +1,20 @@
+fun len_helper[n](xs: ptr<list>, acc: uint) -> uint {
+    with {
+        let xs_null <- xs == null;
+    } do if xs_null {
+        let out <- acc;
+    } else with {
+        let temp <- default<list>;
+        /* *xs <-> temp; */
+        let next <- temp.2;
+        let r <- acc /* + 1 */;
+    } do {
+        let out <- len_helper[n-1](next, r);
+    }
+    return out;
+}
+
+fun length[n](xs: ptr<list>) -> uint {
+    let out <- len_helper[n](xs, 0);
+    return out;
+}

run.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -x
+
+# Optional: regenerate circuits
+# ./gen_circuits.sh
+# ./gen_qasm.sh
+
+# Run fast optimizers
+./run_feynopt_mctExpand.sh
+./run_feynopt_toCliffordT.sh
+./run_qiskit.sh
+./run_pytket_zx.sh
+./run_quizx.sh
+./run_voqc.sh
+
+# Run timing
+./run_timing.sh
+
+# Run slow optimizers
+./run_pytket_peephole.sh
+./run_qiskit_big.sh
+./run_quartz.sh
+./run_queso.sh
+./run_timing_big.sh
+
+# Too big to run
+# ./run_quizx_big.sh

run_fast.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -x
+
+# Optional: regenerate circuits
+# ./gen_circuits.sh
+# ./gen_qasm.sh
+
+# Run fast optimizers
+./run_feynopt_mctExpand.sh
+./run_feynopt_toCliffordT.sh
+# ./run_qiskit.sh
+# ./run_pytket_zx.sh
+# ./run_quizx.sh
+# ./run_voqc.sh
+
+# Run timing
+./run_timing.sh
+
+# Run slow optimizers
+# ./run_pytket_peephole.sh
+# ./run_qiskit_big.sh
+# ./run_quartz.sh
+# ./run_queso.sh
+# ./run_timing_big.sh
+
+# Too big to run
+# ./run_quizx_big.sh

run_feynopt_mctExpand.sh

@@ -0,0 +1,36 @@
+#!/bin/bash
+
+MEMORY_LIMIT_KB=32000000
+TIMEOUT_SEC=3600
+set -x
+mkdir -p feynopt_mctExpand_out
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length_simplified$i.qc > feynopt_mctExpand_out/length_simplified$i.qc 2> feynopt_mctExpand_out/length_simplified$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length_simplified_only_cf$i.qc > feynopt_mctExpand_out/length_simplified_only_cf$i.qc 2> feynopt_mctExpand_out/length_simplified_only_cf$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length_simplified_only_cn$i.qc > feynopt_mctExpand_out/length_simplified_only_cn$i.qc 2> feynopt_mctExpand_out/length_simplified_only_cn$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length_simplified_orig$i.qc > feynopt_mctExpand_out/length_simplified_orig$i.qc 2> feynopt_mctExpand_out/length_simplified_orig$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length$i.qc > feynopt_mctExpand_out/length$i.qc 2> feynopt_mctExpand_out/length$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -mctExpand -O2 circuits/qc/length_orig$i.qc > feynopt_mctExpand_out/length_orig$i.qc 2> feynopt_mctExpand_out/length_orig$i.log ) || echo 'errored or timed out'
+done

run_feynopt_toCliffordT.sh

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+MEMORY_LIMIT_KB=32000000
+TIMEOUT_SEC=3600
+set -x
+mkdir -p feynopt_toCliffordT_out
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -toCliffordT -O2 circuits/qc/length_simplified_orig$i.qc > feynopt_toCliffordT_out/length_simplified_orig$i.qc 2> feynopt_toCliffordT_out/length_simplified_orig$i.log ) || echo 'errored or timed out'
+done
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec timeout $TIMEOUT_SEC /usr/bin/time -v ./feynopt -toCliffordT -O2 circuits/qc/length_orig$i.qc > feynopt_toCliffordT_out/length_orig$i.qc 2> feynopt_toCliffordT_out/length_orig$i.log ) || echo 'errored or timed out'
+done

run_pytket_peephole.py

@@ -0,0 +1,16 @@
+#!/usr/bin/env python3
+
+from pytket import OpType
+from pytket.qasm import circuit_from_qasm, circuit_to_qasm_str
+from pytket.passes import FullPeepholeOptimise, RemoveRedundancies, SequencePass
+from pytket.transform import Transform
+from pytket.utils.stats import gate_counts
+import sys
+
+c = circuit_from_qasm(sys.argv[1])
+print("Starting peephole optimization", file=sys.stderr)
+SequencePass([FullPeepholeOptimise(), RemoveRedundancies()]).apply(c)
+print("Finished peephole optimization", file=sys.stderr)
+Transform.RebaseToPyZX().apply(c)
+print("Rz Count After: " + str(gate_counts(c)[OpType.Rz]), file=sys.stderr)
+print(circuit_to_qasm_str(c))

run_pytket_peephole.sh

@@ -0,0 +1,10 @@
+#!/bin/bash
+
+MEMORY_LIMIT_KB=32000000
+set -x
+mkdir -p pytket_peephole_out
+
+for i in {1..10}
+do
+( ulimit -v $MEMORY_LIMIT_KB && exec /usr/bin/time -v ./run_pytket_peephole.py circuits/qasm/length_simplified_orig$i.qasm > pytket_peephole_out/length_simplified_orig$i.qasm 2> pytket_peephole_out/length_simplified_orig$i.log ) || echo 'errored or timed out'
+done