Main (voqc.Voqc.Main)

Overview

VOQC contains utilities for optimizing quantum circuits and mapping them to a connectivity graph. VOQC was first presented at POPL 2021. The extended version of the POPLpaper is available here. In the remainder of this document we refer to this paper as "POPL VOQC".

This file lists the functions we provide in VOQC, as well as properties we have verified about them. In general, our goal is to prove that VOQC circuit transformations are semantics preserving, meaning that the behavior of a circuit (its "semantics") does not change after our transformations are applied. The semantics of a unitary circuit over d qubits is a 2^d x 2^d unitary matrix, so proving semantics-preservation requires showing that two (symbolic) matrices are equal. Sometimes we also show that the output of a transformation has a particular property, such as using a particular gate set.

In the remainder of this document, we will use the following shorthand for properties proved:

Preserves semantics -- The semantics-preservation property is written in Coq as forall (c : circ), [[opt c]] = [[c]] for optimization opt. In our development, we support several variations on semantics-preservation:
- (WT) -- We include the annotation (WT) to indicate that a transformation preserves semantics provided that the input circuit is well-typed. A circuit is "well-typed" for some dimension (i.e. number of qubits) d if every gate in the circuit applies to qubit(s) less than d and no gate has duplicate arguments. Some optimizations do not preserve semantics when the input is ill-typed because they can produce a well-typed circuit from an ill-typed input. In Coq, this requirement is written as forall c, well_typed c -> [[opt c]] = [[c]].
- (phase) -- We include the annotation (phase) to indicate that the semantics are preserved up to a global phase. The unitary matrices X and e^(ix)X have the same action on all input states, and can thus be considered equivalent. However, this definition of equivalence is not compositional in the sense that the controlled versions of these matrices are not equivalent (because the phase is no longer global). In Coq, this restriction is written as forall c, exists x, [[opt c]] = e^(ix) [[c]].
- (perm) -- We include the annotation (perm) to indicate that the semantics are preserved up to a permutation of qubits. This will be the case after applying circuit mapping. In Coq, for permutation matrices P1 and P2, this variation is written as forall c, exists P1 P2, [[c]] = P1 x [[opt c]] x P2.
Preserves WT -- This property says that if the input circuit is well-typed, then the output circuit will also be well-typed. In our semantics, the denotation of a well-typed circuit is a unitary matrix while the denotation of an ill-typed circuit is the zero matrix, so all of the variations on semantics-preservation actually imply WT-preservation.
Preserves mapping -- This property says that, for any connectivity graph G, if the input circuit respects the constraints in G then the output circuit also respects the constraints in G. This property allows us to apply optimizations after mapping, preserving our guarantee that the output program satisfies hardware constraints.
Uses gates {g1, ..., gn} -- This property says that every operation in the circuit is an application of one of {g1, ..., gn}.
Respects constraints G -- This property says that every two-qubit interaction in the circuit is allowed by the connectivity graph G.

Types

type circ =
  FullGateSet.FullGateSet.coq_Full_Unitary UnitaryListRepresentation.gate_list

The circ type is a list of gates from the full gate set.

type layout

A layout describes a mapping from logical to physical qubits. For an architecture with n qubits, a layout should be a bijection on integers {0, ..., n-1}. Under the hood, layout is a pair of functions (nat -> nat) * (nat -> nat) that maps logical qubits to physical qubits and physical qubits back to logical qubits. A layout is well-formed if these two functions accurately represent a bijection and its inverse.

You can construct a layout using the functions list_to_layout, trivial_layout, or greedy_layout.

type c_graph

A connectivity graph (c_graph) is a pair nat * (nat -> nat -> bool), that consists of the total number of qubits in the system and a an oracle that indicates whether a directed edge exists between two qubits.

You can construct a connectivity graph using make_lnn, make_lnn_ring, or make_grid.

type path_finding_fun

A path_finding_fun is a function nat -> nat -> nat list that produces an undirected path between any two nodes in a graph. It is used for circuit mapping.

You can construct an object of this type using lnn_path_finding_fun, lnn_ring_path_finding_fun, or grid_path_finding_fun.

type qubit_ordering_fun

A qubit_ordering_fun is a function nat option -> nat list that produces an ordering of all qubits in the system, excluding its optional argument. It is used for ranking pysical qubits when generating layouts.

You can construct an object of this type using lnn_qubit_ordering_fun or lnn_ring_qubit_ordering_fun.

API

Utility Functions

val check_well_typed : circ -> int -> bool

Check if a circuit is well-typed with the given number of qubits (i.e. every gate is applied to qubits within range and never applied to duplicates).

val convert_to_ibm : circ -> circ

Restrict a program to use gates in the IBM gate set (this may be done implicitly when calling certain optimizations).

Verified Properties: preserves semantics, preserves WT, preserves mapping, uses gates {U1, U2, U3, CX}

val convert_to_rzq : circ -> circ

Restrict a circuit to use gates in the RzQ gate set (this may be done implicitly when calling certain optimizations).

Verified properties: preserves semantics (phase), preserves WT, preserves mapping, uses gates {H, X, Rzq, CX}

val replace_rzq : circ -> circ

Replace the (non-standard) Rzq gate with its equivalent Rz, Z, T, S, Tdg, or Sdg gate.

Verified Properties: preserves semantics, preserves WT, preserves mapping, uses any gate in the full set except Rzq

val decompose_to_cnot : circ -> circ

Decompose CZ, SWAP, CCX, and CCZ gates so that the only multi-qubit gate is CX (also called "CNOT").

Verified Properties: preserves semantics, preserves WT, uses any gate in the full set except {CZ, SWAP, CCX, CCZ}

val count_I : circ -> int

val count_X : circ -> int

val count_Y : circ -> int

val count_Z : circ -> int

val count_H : circ -> int

val count_S : circ -> int

val count_T : circ -> int

val count_Sdg : circ -> int

val count_Tdg : circ -> int

val count_Rx : circ -> int

val count_Ry : circ -> int

val count_Rz : circ -> int

val count_Rzq : circ -> int

val count_U1 : circ -> int

val count_U2 : circ -> int

val count_U3 : circ -> int

val count_CX : circ -> int

val count_CZ : circ -> int

val count_SWAP : circ -> int

val count_CCX : circ -> int

val count_CCZ : circ -> int

val count_1q : circ -> int

Count the number of 1-qubit gates.

val count_2q : circ -> int

Count the number of 2-qubit gates.

val count_3q : circ -> int

Count the number of 3-qubit gates.

val count_total : circ -> int

Count the total number of gates (i.e. length of the instruction list).

val count_rzq_clifford : circ -> int

Count the Rzq gates parameterized by a multiple of PI/2 (i.e. "Clifford" Rz gates).

Optimization Functions

val optimize_ibm : circ -> circ

Implementation of Qiskit's Optimize1qGates routine, which merges adjacent 1-qubit gates. Internally uses the IBM gate set.