<jupyter_start><jupyter_text>VOQC: A Verifed Optimizer for Quantum Circuits Welcome to the tutorial for VOQC! VOQC is a **verified optimizer for quantum circuits**, implemented and *formally verified* in the [Coq proof assistant](https://coq.inria.fr/). All VOQC optimizations are *guaranteed* to preserve the semantics of the original circuit, meaning that any optimized circuit produced by VOQC has the same behavior as the input circuit. VOQC was presented as a [distinguished paper at POPL 2021](https://arxiv.org/abs/1912.02250); its code is available at [github.com/inQWIRE/SQIR](https://github.com/inQWIRE/SQIR).To run VOQC, we (1) extract the verified Coq code to OCaml, (2) compile the extracted OCaml code to a library, (3) wrap the OCaml library in C, and (4) provide a Python interface for the C pyvoqc. This tutorial introduces the optimizations available in VOQC through its Python interface. For convenience, we have written Python pyvoqc code that makes VOQC look like an optimization pass in [IBM's Qiskit framework](https://qiskit.org/documentation/getting_started.html), allowing us to take advantage of Qiskit's utilities for quantum programming. In this tutorial, we'll use Qiskit for building and printing circuits. Outline* End-to-end Example* Unitary Optimizations  * Not Propagation  * Single-qubit Gate Cancellation  * Two-qubit Gate Cancellation  * Rotation Merging  * Hadamard Reduction We begin with an example of reading in a circuit, optimizing it using VOQC, and writing it back to a file.We then describe each unitary optimization available in VOQC, along with an example of how to run it in Qiskit.   PreliminariesTo compile the extracted OCaml code into a library, run `dune build lib/libvoqc.so` in the pyvoqc directory.To begin the tutorial, import modules below from Qiskit and VOQC.<jupyter_code># Click on this cell and press Ctrl+Enter or run it with the "Run" button
from qiskit import QuantumCircuit
from pyvoqc.voqc import VOQC
from pyvoqc.qiskit.voqc_optimization import QisVOQC
from qiskit.transpiler import PassManager
from qiskit.qasm import pi<jupyter_output><empty_output><jupyter_text>End-to-end ExampleOur Python interface allows us to pass a Qiskit circuit object through VOQC and receive an optimized Qiskit circuit.VOQC can be called just like Qiskit's built-in transpiler passes (e.g. "Commutative Cancellation" or "CX Cancellation"). Simply append `QisVOQC([opt list])` to a pre-defined `Pass Manager` where `opt list` is an optional argument specifying one or more of the unitary optimizations in VOQC (see *Unitary Optimizations* below). `QisVOQC()` with no arguments will run all optimizations available in VOQC.In the example here, we first read in a small quantum circuit from the qasm file "tof_3_example.qasm". This circuit consists of three 3-qubit CCX (Toffoli) gates that together perform a 4-qubit Toffoli gate. Qiskit will *decompose* these 3-qubit gates into the 1- and 2-qubit gates supported by VOQC. We call the initial circuit `circ`. We then define a pass manager `pm` and schedule our VOQC transpiler pass. Finally, we run `circ` through the pass manager, producing optimized circuit `new_circ`. Rather than printing the resulting circuit (which is fairly large), we print the its gate counts. We also write `new_circ` to the file "tof_3_example_optimized.qasm".<jupyter_code># Read circuit from file
circ = QuantumCircuit.from_qasm_file("tutorial-files/tof_3_example.qasm")
print("Before Optimization:")
print(circ)

# Append VOQC pass without argument to the Pass Manager
pm = PassManager()
pm.append(QisVOQC())
new_circ = pm.run(circ)

# Print info about optimized circuit 
print("\nAfter Optimization:\n")
print('gate counts = ', new_circ.count_ops())
print('circuit depth = ', new_circ.depth())

# Save optimized circuit
qasm_str = new_circ.qasm(filename="tof_3_example_optimized.qasm")<jupyter_output>Before Optimization:
                    
q_0: ──■─────────■──
       │         │  
q_1: ──■─────────■──
       │         │  
q_2: ──┼────■────┼──
       │  ┌─┴─┐  │  
q_3: ──┼──┤ X ├──┼──
     ┌─┴─┐└─┬─┘┌─┴─┐
q_4: ┤ X ├──■──┤ X ├
     └───┘     └───┘

After Optimization:

gate counts =  OrderedDict([('cx', 16), ('t', 8), ('tdg', 7), ('h', 6), ('s', 2), ('sdg', 1)])
circuit depth =  31<jupyter_text>Unitary OptimizationsAppending `QisVOQC()` to the pass manager runs the VOQC's main optimization function, which runs all its unitary optimizations in a predefined order. You can also run optimizations individually, or in a custom order, by passing arguments to the `QisVOQC` class (e.g. `QisVOQC(["not_propagation"])` to run "not propagation"). VOQC provides five unitary optimizations: *not propagation*, *single-qubit gate cancellation*, *two-qubit gate cancellation*, *rotation merging*, and *hadamard reduction*.We provide a brief example of each optimization below. For more details see Section 4 of [our paper](https://arxiv.org/abs/1912.02250) or an earlier paper by [Nam et al. (2018)](https://www.nature.com/articles/s41534-018-0072-4), which inspired many of VOQC's optimizations.  Not Propagation*Not propagation* commutes X (logical NOT) gates rightward through the circuit, cancelling them when possible. In the example below, the leftmost X gate propagates through the CNOT gate to become two X gates. The upper X gate then propagates through the H gate to become a Z, and the two lower X gates cancel.<jupyter_code># Build circuit with 2 qubits and 4 gates
circ = QuantumCircuit(2)
circ.x(0)
circ.cx(0, 1)
circ.h(0)
circ.x(1)
print("Before Optimization:")
print(circ)

# Append "not_propagation" optimization to the Pass Manager
pm = PassManager()
pm.append(QisVOQC(["not_propagation"]))
new_circ = pm.run(circ)

# Print optimized circuit
print("\nAfter Optimization:")
print(new_circ)<jupyter_output>Before Optimization:
     ┌───┐     ┌───┐
q_0: ┤ X ├──■──┤ H ├
     └───┘┌─┴─┐├───┤
q_1: ─────┤ X ├┤ X ├
          └───┘└───┘

After Optimization:
          ┌───┐┌───┐
q_0: ──■──┤ H ├┤ Z ├
     ┌─┴─┐└───┘└───┘
q_1: ┤ X ├──────────
     └───┘<jupyter_text>Single-qubit Gate Cancellation*Single-qubit gate cancellation* has the same "propagate-cancel" structure as not propagation, except that gates revert back to their original positions if they fail to cancel. In the example below, the upper leftmost T gate commutes through the control of the CNOT, combining with the upper rightmost T gate to become an S gate. The lower T gate commutes through the H; CNOT; H subcircuit to cancel with the Tdg gate.<jupyter_code># Build circuit with 2 qubits and 7 gates
circ = QuantumCircuit(2)
circ.t(0)
circ.t(1)
circ.h(1)
circ.cx(0, 1)
circ.h(1)
circ.t(0)
circ.tdg(1)
print("Before Optimization:")
print(circ)

# Append "cancel_single_qubit_gates" optimization to the Pass Manager
pm = PassManager()
pm.append(QisVOQC(["cancel_single_qubit_gates"]))
new_circ = pm.run(circ)

# Print optimized circuit
print("\nAfter Optimization:")
print(new_circ)<jupyter_output>Before Optimization:
     ┌───┐          ┌───┐       
q_0: ┤ T ├───────■──┤ T ├───────
     ├───┤┌───┐┌─┴─┐├───┤┌─────┐
q_1: ┤ T ├┤ H ├┤ X ├┤ H ├┤ TDG ├
     └───┘└───┘└───┘└───┘└─────┘

After Optimization:
               ┌───┐
q_0: ───────■──┤ S ├
     ┌───┐┌─┴─┐├───┤
q_1: ┤ H ├┤ X ├┤ H ├
     └───┘└───┘└───┘<jupyter_text>Two-qubit Gate Cancellation*Two-qubit gate cancellation* is similar to single-qubit gate cancellation, except that it aims to commute and cancel CNOT gates. In the circuit below, the first CNOT gate commutes through the second, to cancel with the third.<jupyter_code># Build circuit with 3 qubits and 3 qates
circ = QuantumCircuit(3)
circ.cx(0, 1)
circ.cx(0, 2)
circ.cx(0, 1)
#circ.h(0)
print("Before Optimization:")
print(circ)

# Append "cancel_two_qubit_gates" optimization to the Pass Manager
pm = PassManager()
pm.append(QisVOQC(["cancel_two_qubit_gates"]))
new_circ = pm.run(circ)

# Print optimized circuit
print("\nAfter Optimization:")
print(new_circ)<jupyter_output>Before Optimization:
                    
q_0: ──■────■────■──
     ┌─┴─┐  │  ┌─┴─┐
q_1: ┤ X ├──┼──┤ X ├
     └───┘┌─┴─┐└───┘
q_2: ─────┤ X ├─────
          └───┘     

After Optimization:
          
q_0: ──■──
       │  
q_1: ──┼──
     ┌─┴─┐
q_2: ┤ X ├
     └───┘<jupyter_text>Rotation Merging*Rotation merging* combines Rz gates that act on the same logical state (see discussion in Sec 4.4 of [our paper](https://arxiv.org/abs/1912.02250)). In the example below, the two Rz(pi/6) gates can be combines into a single Rz(pi/6 + pi/6) = Rz(pi/3) gate.<jupyter_code># Build circuit with 2 qubits and 4 gates
circ = QuantumCircuit(2)
circ.rz(pi/6, 1)
circ.cx(0, 1)
circ.cx(1, 0)
circ.rz(pi/6, 0)
print("Before Optimization:")
print(circ)

# Append "merge_rotations" optimization to the Pass Manager
pm = PassManager()
pm.append(QisVOQC(["merge_rotations"]))
new_circ = pm.run(circ)

# Print optimized circuit
print("\nAfter Optimization:")
print(new_circ)<jupyter_output>Before Optimization:
                      ┌───┐┌──────────┐
q_0: ──────────────■──┤ X ├┤ RZ(pi/6) ├
     ┌──────────┐┌─┴─┐└─┬─┘└──────────┘
q_1: ┤ RZ(pi/6) ├┤ X ├──■──────────────
     └──────────┘└───┘                 

After Optimization:
                      ┌───┐
q_0: ──────────────■──┤ X ├
     ┌──────────┐┌─┴─┐└─┬─┘
q_1: ┤ RZ(pi/3) ├┤ X ├──■──
     └──────────┘└───┘<jupyter_text>Hadamard Reduction*Hadamard reduction* applies a series of identities to reduce the number of H gates in a circuit, for the purpose of making other optimizations (e.g. rotation merging) more effective. In the example below, we replace the first circuit with the second to remove two H gates.<jupyter_code># Build circuit with 2 qubits and 5 gates
circ = QuantumCircuit(2)
circ.h(1)
circ.sdg(1)
circ.cx(0, 1)
circ.s(1)
circ.h(1)

print("Before Optimization:")
print(circ)

# Append "hadamard_reduction" optimization to the Pass Manager
pm = PassManager()
pm.append(QisVOQC(["hadamard_reduction"]))
new_circ = pm.run(circ)

# Print optimized circuit
print("\nAfter Optimization:")
print(new_circ)<jupyter_output>Before Optimization:
                                
q_0: ──────────────■────────────
     ┌───┐┌─────┐┌─┴─┐┌───┐┌───┐
q_1: ┤ H ├┤ SDG ├┤ X ├┤ S ├┤ H ├
     └───┘└─────┘└───┘└───┘└───┘

After Optimization:
                      
q_0: ───────■─────────
     ┌───┐┌─┴─┐┌─────┐
q_1: ┤ S ├┤ X ├┤ SDG ├
     └───┘└───┘└─────┘
{'fraction_non_alphanumeric': 0.15421779882114214, 'fraction_numerical': 0.015073920185525171, 'mean_word_length': 4.3878188443519, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 23, 'https://': 7, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '7', 'dir': 'jupyter-structured-clean-dedup', 'id': '65317', 'license': 'MIT', 'n_tokens_mistral': 3907, 'n_tokens_neox': 3724, 'n_words': 1245, 'path': 'tutorial.ipynb', 'repo_name': 'akshajgaur/pyvoqc', 'size': '10349'}