We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.
1 Introduction
Due to the rapid progress of quantum technology in the recent years, it is predicted that practical quantum computers can be built within 10–15 years. Especially during the last 3 years, breakthroughs have been made in quantum hardware. Programmable superconductor quantum computers and trapped ion quantum computers have been built in universities and companies [1, 3, 4, 6, 23].
In another direction, intensive research on quantum programming has been conducted in the last decade [16, 45, 51, 53], as surveyed in [27, 52]. In particular, several quantum programming languages have been defined and their compilers have been implemented, including Quipper [31], Scaffold [35], QWire [47], Microsoft’s LIQUi [25] and Q# [57], IBM’s OpenQASM [22], Google’s Cirq [30], ProjectQ [56], Chisel-Q [40], Quil [55] and \(Q\left| SI \right\rangle \) [39]. These research allow quantum programs to first run on an ideal simulator for testing, and then on physical devices [5]. For instance, many small quantum algorithms and protocols have already been programmed and run on IBM’s simulators and quantum computers [1, 2].
Advertisement
Clearly, simulators can only be used for testing. It shows the correctness of the program on one or a few inputs, not its correctness under all possible inputs. Various theories and tools have been developed to formally reason about quantum programs for all inputs on a fixed number of qubits. Equivalence checking [7, 8], termination analysis [38], reachability analysis [64], and invariant generation [62] can be used to verify the correctness or termination of quantum programs. Unfortunately, the size of quantum programs on which these tools are applicable is quite limited. This is because all of these tools still perform calculations over the entire state space, which for quantum algorithms has size exponential in the number of qubits. For instance, even on the best supercomputers today, simulation of a quantum program is restricted to about 50–60 qubits. Most model-checking algorithms, which need to perform calculations on operators over the state space, are restricted to 25–30 qubits with the current computing resources.
Deductive program verification presents a way to solve this state space explosion problem. In deductive verification, we do not attempt to execute the program or explore its state space. Rather, we define the semantics of the program using precise mathematical language, and use mathematical reasoning to prove the correctness of the program. These proofs are checked on a computer (for example, in proof assistants such as Coq [15] or Isabelle [44]) to ensure a very high level of confidence.
To apply deductive reasoning to quantum programs, it is necessary to first define a precise semantics and proof system. There has already been a lot of work along these lines [9, 20, 21, 61]. A recent result in this direction is quantum Hoare logic (QHL) [61]. It extends to sequential quantum programs the Floyd-Hoare-Naur inductive assertion method for reasoning about correctness of classical programs. QHL is proved to be (relatively) complete for both partial correctness and total correctness of quantum programs.
In this paper, we formalize the theory of quantum Hoare logic in Isabelle/HOL, and use it to verify a non-trivial quantum algorithm – Grover’s search algorithm1. In more detail, the contributions of this paper are as follows.
Advertisement
1.
We formally prove the main results of quantum Hoare logic in Isabelle/HOL. That is, we write down the syntax and semantics of quantum programs, specify the basic Hoare triples, and prove the soundness and completeness of the resulting deduction system (for partial correctness of quantum programs). To our best knowledge, this is the first formalization of a Hoare logic for quantum programs in an interactive theorem prover.
2.
As an application of the above formalization, we verify the correctness of Grover’s search algorithm. In particular, we prove that the algorithm always succeeds on the (infinite) class of inputs where the expected probability of success is 1.
3.
As preparation for the above, we extend Isabelle/HOL’s library for linear algebra. Based on existing work [13, 58], we formalize many further results in linear algebra for complex matrices, in particular positivity and the Löwner order. Another significant part of our work is to define the tensor product of vectors and matrices, in a way that can be used to extend and combine operations on quantum variables in a consistent way. Finally, we implement algorithms to automatically prove identities in linear algebra to ease the formalization process.
The organization of the rest of the paper is as follows. Section 2 gives a brief introduction to quantum Hoare logic. Section 3 describes in detail our formalization of QHL in Isabelle/HOL. Section 4 describes the application to Grover’s algorithm. Section 5 discusses automation techniques, and gives some idea about the cost of the formalization. Section 6 reviews some related work. Finally, we conclude in Sect. 7 with a discussion of future directions of work.
We expect theorem proving techniques will play a crucial role in formal reasoning about quantum computing, as they did for classical computing, and we hope this paper will be one of the first steps in its development.
2 Quantum Hoare Logic
In this section, we briefly recall the basic concepts and results of quantum Hoare logic (QHL). We only introduce the proof system for partial correctness, since the one for total correctness is not formalized in our work. In addition, we make two simplifications compared to the original work: we consider only variables with finite dimension, and we remove the initialization operation. The complete version of QHL can be found in [61].
In QHL, the number of quantum variables is pre-set before each run of the program. Each quantum variable \(q_i\) has dimension \(d_i\). The (pure) state of the quantum variable takes value in a complex vector space of dimension \(d_i\). The overall (pure) state takes value in the tensor product of the vector spaces for the variables, which has dimension \(d = \prod d_i\). The mixed state for variable \(q_i\) (resp. overall) is given by a \(d_i\times d_i\) (resp. \(d\times d\)) matrix satisfying certain conditions (making them partial density operators). The notation \(\overline{q}\) is used to denote some finite sequence of distinct quantum variables (called a quantum register). We denote the vector space corresponding to \(\overline{q}\) by \(\mathcal {H}_{\overline{q}}\).
The syntax of quantum programs is given by the following grammar:
In \(\overline{q}:=U\overline{q}\), U is a unitary operator on \(\mathcal {H}_{\overline{q}}\), i.e., \(U^{\dag }U=UU^{\dag }=\mathbb {I}\), where \(U^{\dag }\) is the conjugate transpose of U.
In \(\mathbf{measure}\ M[\overline{q}]:\overline{S}\), \(M=\{M_m\}\) is a quantum measurement on \(\mathcal {H}_{\overline{q}}\), and \(\overline{S}=\{S_m\}\) gives quantum programs that will be executed after each possible outcome of the measurement;
In \(\mathbf{while}\ M[\overline{q}]=1\ \mathbf{do}\ S\), \(M=\{M_0,M_1\}\) is a yes-no measurement on \(\overline{q}\).
Quantum programs can be regarded as quantum extensions of classical while programs. The skip statement does nothing, which is the same as in the classical case. The unitary transformation changes the state of \(\overline{q}\) according to U. It is the counterpart to the assignment operation in classical programming languages. The sequential composition is similar to its classical counterpart. The measurement statement is the quantum generalisation of the classical case statement \(\mathbf{if}\ (\Box m\cdot b_m\rightarrow S_m)\ \mathbf{fi}\). The loop statement is a quantum generalisation of the classical loop whilebdoS.
Fig. 1.
Proof system \(\textit{qPD}\) for partial correctness
×
Formally, the denotational semantics for quantum programs is defined as a super-operator \(\llbracket S\rrbracket (\cdot )\), assigning to each quantum program S a mapping between partial density operators. As usual, the denotational semantics is defined by induction on the structure of the quantum program:
1.
.
2.
.
3.
.
4.
.
5.
, where \(\bigvee \) stands for the least upper bound of partial density operators according to the Löwner partial order \(\sqsubseteq \).
The correctness of a quantum program S is expressed by a quantum extension of the Hoare triple \(\{P\}S\{Q\}\), where the precondition P and the postcondition Q are matrices satisfying certain conditions for quantum predicates [24]. The semantics for partial correctness is defined as follows:
We note that they become the same when the quantum program S is terminating, i.e. \({\text {tr}}(\llbracket S\rrbracket (\rho ))={\text {tr}}(\rho )\) for all partial density operators \(\rho \).
The proof system \(\textit{qPD}\) for partial correctness of quantum programs is given in Fig. 1. The soundness and (relative) completeness of \(\textit{qPD}\) is proved in [61]:
Theorem 1
The proof system \(\textit{qPD}\) is sound and (relative) complete for partial correctness of quantum programs.
3 Formalization in Isabelle/HOL
In this section, we describe the formalization of quantum Hoare logic in Isabelle/HOL. Isabelle/HOL [44] is an interactive theorem prover based on higher-order logic. It provides a flexible language in which one can state and prove theorems in all areas of mathematics and computer science. The proofs are checked by the Isabelle kernel according to the rules of higher-order logic, providing a very high level of confidence in the proofs. A standard application of Isabelle/HOL is the formalization of program semantics and Hoare logic. See [43] for a description of the general technique, applied to a very simple classical programming language.
3.1 Preliminaries in Linear Algebra
Our work is based on the linear algebra library developed by Thiemann and Yamada in the AFP entry [58]. We also use some results on the construction of tensor products in another AFP entry by Bentkamp [13].
In these libraries, the type
of vectors with entries in type
is defined as pairs (n, f), where n is a natural number, and f is a function from natural numbers to
, such that f(i) is undefined when \(i\ge n\). Likewise, the type
of matrices is defined as triples (nr, nc, f), where nr and nc are natural numbers, and f is a function from pairs of natural numbers to
, such that f(i, j) is undefined when \(i\ge nr\) or \(j\ge nc\). The terms
(resp.
) represent the set of vectors of length n (resp. matrices of dimension \(m\times n\)). In our work, we focus almost exclusively on the case where
is the complex numbers. For this case, existing libraries already define concepts such as the adjoint of a matrix, and the (complex) inner product between two vectors. We further define concepts such as Hermitian and unitary matrices, and prove their basic properties.
A key result in linear algebra that is necessary for our work is the Schur decomposition theorem. It states that any complex \(n\times n\) matrix A can be written in the form \(QUQ^{-1}\), where Q is unitary and U is upper triangular. In particular, if A is normal (that is, if \(AA^{\dag }=A^{\dag }A\)), then A is diagonalizable. A version of the Schur decomposition theorem is formalized in [58], showing that any matrix is similar to an upper-triangular matrix U. However, it does not show that Q can be made unitary. We complete the proof of the full theorem, following the outline of the previous proof.
Next, we define the key concept of positive semi-definite matrices (called positive matrices from now on for simplicity). An \(n\times n\) matrix A is positive if \(v^{\dag }Av\ge 0\) for any vector v. We formalize the basic theory of positive matrices, in particular showing that any positive matrix is Hermitian.
Density operators and partial density operators are then defined as follows:
×
Next, the Löwner partial order is defined as a partial order on the type
as follows:
×
A key result that we formalize states that under the Löwner partial order, any non-decreasing sequence of partial density operators has a least upper bound, which is the pointwise limit of the operators when written as \(n\times n\) matrices. This is used to define the infinite sum of matrices, necessary for the semantics of the while loop.
3.2 Syntax and Semantics of Quantum Programs
We now begin with the definition of syntax and semantics of quantum programs. First, we describe how to model states of a quantum program. Recall that each quantum program operates on a fixed set of quantum variables \(q_i\), where each \(q_i\) has dimension \(d_i\). These information can be recorded in a locale [33] as follows:
×
The total dimension d is given by (here
denotes the product of a list of natural numbers).
The (mixed) state of the system is given by a partial density operator with dimension \(d\times d\). Hence, we declare
×
×
×
Next, we define the concept of quantum programs. They are declared as an inductively-defined datatype in Isabelle/HOL, following the grammar given in Sect. 2.
×
At this stage, we assume that all matrices involved operate on the global state (that is, all of the quantum variables). We will define commands that operate on a subset of quantum variables later. Measurement is defined over any finite number of matrices. Here
is a measurement with n options,
for \(i < n\) are the measurement matrices, and
is the command to be executed when the measurement yields result i. Likewise, the first argument to
gives measurement matrices, where only the first two values are used.
Next, we define well-formedness and denotation of quantum programs. The predicate
expresses the well-formedness condition. For a quantum program to be well-formed, all matrices involved should have the right dimension, the argument to
should be unitary, and the measurements for
and
should satisfy the condition \(\sum _i M_i^{\dag }M_i=\mathbb {I}_n\). Denotation is written as
, defined as in Sect. 2. Both
and
is defined by induction over the structure of the program. The details are omitted here.
3.3 Hoare Triples
In this section, we define the concept of Hoare triples, and state what needs to be proved for soundness and completeness of the deduction system. First, the concept of quantum predicates is defined as follows:
With this, we can give the semantic definition of Hoare triples for partial and total correctness. These definitions are intended for the case where P and Q are quantum predicates, and S is a well-formed program. They define what Hoare triples are valid.
×
×
×
Next, we define what Hoare triples are provable in the \(\textit{qPD}\) system. A Hoare triple for partial correctness is provable (written as
) if it can be derived by combining the rules in Fig. 1. This condition can be defined in Isabelle/HOL as an inductive predicate. The definition largely parallels the formulae shown in the figure.
With these definitions, we can state and prove soundness and completeness of the Hoare rules for partial correctness. Note that the statement for completeness is very simple, seemingly without needing to state “relative to the theory of the field of complex numbers”. This is because we are taking a shallow embedding for predicates, hence any valid statement on complex numbers, in particular positivity of matrices, is in principle available for use in the deduction system (for example, in the assumption to the order rule).
×
×
The soundness of the Hoare rules is proved by induction on the predicate \(\vdash _p\), showing that each rule is sound with respect to \(\models _p\). Completeness is proved using the concept of weakest-preconditions, following [61].
3.4 Partial States and Tensor Products
So far in our development, all quantum operations act on the entire global state. However, for the actual applications, we are more interested in operations that act on only a few of the quantum variables. For this, we need to define an extension operator, that takes a matrix on the quantum state for a subset of the variables, and extend it to a matrix on all of the variables. More generally, we need to define tensor products on vectors and matrices defined over disjoint sets of variables. These need to satisfy various consistency properties, in particular commutativity and associativity of the tensor product. Note that directly using the Kronecker product is not enough, as the matrix to be extended may act on any (possibly non-adjacent) subset of variables, and we need to distinguish between all possible cases.
Before presenting the definition, we first review some preliminaries. We make use of existing work in [13], in particular their encode and decode operations, and emulate their definitions of
and
(used in [13] to convert between tensors represented as a list and matrices). Given a list of dimensions \(d_i\), the encode and decode operations (named
and
) produce a correspondence between lists of indices \(a_i\) satisfying \(a_i<d_i\) for each \(i<n\), and a natural number less than \(\prod _i d_i\). This works in a way similar to finding the binary representation of a number (in which case all “dimensions” are 2). List operation
constructs the subsequence of
containing only the elements at indices in the set
.
The locale
extends
, adding
for a subset of quantum variables. Our goal is to define the tensor product of two vectors or matrices over
and its complement
, respectively.
×
First,
and
are dimensions of variables
and
:
×
The operation
(resp.
) provides the map from the product of
to the product of
(resp.
).
×
With this, tensor products on vectors and matrices are defined as follows (here
is the product of
).
×
×
We prove the basic properties of
and
, including that they behave correctly with respect to identity, multiplication, adjoint, and trace.
Extension of matrices is a special case of the tensor product, where the matrix on
is the identity (here
is the product of
).
×
With
, we can define “partial” versions of quantum program commands
,
and
. They take a set of variables \(\overline{q}\) as an extra parameter, and all matrices involved act on the vector space associated to \(\overline{q}\). These commands are named
,
and
. They are usually used in place of the global commands in actual applications.
More generally, we can define the tensor product of vectors and matrices on any two subsets of quantum variables. For this, we define another locale:
×
To make use of
to define tensor product in this more general setting, we need to find the relative position of variables
within
. This is done using
, which counts the position of
within
.
×
Finally, the more general tensor products are defined as follows (note since we are now outside the
locale, we must use qualified names for
and
, and supply extra arguments for variables in the locale. Here
is the total list of dimensions).
×
×
The partial extension
is defined in a similar way as before.
×
The definitions
and
satisfy several key consistency properties. In particular, they satisfy associativity of tensor product. For matrices, this is expressed as follows:
×
Together, these constructions and consistency properties provide a framework in which one can reason about arbitrary tensor product of vectors and matrices, defined on mutually disjoint sets of quantum variables.
3.5 Case Study: Products of Hadamard Matrices
In this section, we illustrate the above framework for tensor product of matrices with an application, to be used in the verification of Grover’s algorithm in the next section.
In many quantum algorithms, we need to deal with the tensor product of an arbitrary number of Hadamard matrices. The Hadamard matrix (denoted
in Isabelle) is given by:
$$\begin{aligned} H = \frac{1}{\sqrt{2}} \begin{bmatrix}1&1\\1&-1\end{bmatrix} \end{aligned}$$
For example, in Grover’s algorithm, we need to apply the Hadamard transform on each of the first n quantum variables, given by
. A single Hadamard transform on the i’th quantum variable, extended to a matrix acting on the first n quantum variables, is defined as follows:
×
The effect of consecutively applying the Hadamard transform on each of the first n quantum variables is equivalent to multiplying the quantum state by
, where
is defined as follows.
×
Crucially, this matrix product of extensions of Hadamard matrices must equal the tensor product of Hadamard matrices. That is, with
defined as
×
we have the theorem
The proof of this result is by induction, requiring the use of associativity of tensor product stated above.
×
4 Verification of Grover’s Algorithm
In this section, we describe our application of the above framework to the verification of Grover’s quantum search algorithm [32]. Quantum search algorithms [18, 32] concern searching an unordered database for an item satisfying some given property. This property is usually specified by an oracle. In a database of N items, where M items satisfy the property, finding an item with the property requires on average O(N / M) calls to the oracle for classical computers. Grover’s algorithm reduces this complexity to \(O(\sqrt{N/M})\).
The basic idea of Grover’s algorithm is rotation. The algorithm starts from an initial state/vector. At every step, it rotates towards the target state/vector for a small angle. As summarised in [18, 19, 42], it can be mathematically described by the following equation [42, Eq. (6.12)]:
where G represents the operator at each step, \(\left| \psi _0 \right\rangle \) is the initial state, \(\theta =2\arccos {\sqrt{(N-M)/N}}\), \(\left| \alpha \right\rangle \) is the bad state (for items not satisfying the property), and \(\left| \beta \right\rangle \) is the good state (for items satisfying the property). Thus when \(\theta \) is very small, i.e., \(M\ll N\), it costs \(O(\sqrt{{N/M}})\) rounds to reach a target state.
Originally, Grover’s algorithm only resolves the case \(M=1\) [32]. It is immediately generalized to the case of known M with the same idea and the case of unknown M with some modifications [18]. After that, the idea is generalized to all invertible quantum processes [19].
The paper [61] uses Grover’s algorithm as the main example illustrating quantum Hoare logic. We largely follow its approach in this paper. See also [42, Chapter 6] for a general introduction.
First, we setup a locale for the inputs to the search problem.
Here n is the number of qubits used to represent the items. That is, we assume \(N=2^n\) items in total. The oracle is represented by the function f, where only its values on inputs less than \(2^n\) are used. The number of items satisfying the property is given by
.
×
Next, we setup a locale for Grover’s algorithm.
×
As in [61], we assume \(R=\pi /2\theta - 1/2\) is an integer. This implies that the quantum algorithm succeeds with probability 1. This condition holds, for example, for all N, M where \(N=4M\). Since we did not formalize quantum states with infinite dimension, we replace the loop counter, which is infinite dimensional in [61], with a variable of dimension \(K > R\). We also remove the control variable for the oracle used in [61]. Overall, our quantum state consists of n variables of dimension 2 for representing the items, and one variable of dimension K for the loop counter.
We now present the quantum program to be verified. First, the operation that performs the Hadamard transform on each of the first n variables is defined by induction as follows.
Here
denotes the tensor product of a matrix on the first n variables (of dimension \(2^n\times 2^n\)) and a matrix on the loop variable (of dimension \(K\times K\)). Executing this program is equivalent to multiplying the quantum state corresponding to the first n variables by \(H^{\otimes n}\), as shown in Sect. 3.5.
×
The body of the loop is given by:
×
where each of the three matrices
,
and
can be defined directly.
×
Finally, the Grover’s algorithm is as follows. Since we do not have initialization, we skip initialization to zero at the beginning and instead assume that the state begins in the zero state in the precondition.
where the measurements for the while loop and at the end of the algorithm are:
×
×
We can now state the final correctness result. Let
be the outer product \(vv^{\dag }\), and
be \(|k\rangle \langle k|\), where \(|k\rangle \) is the k’th basis vector on the vector space corresponding to the loop variable. Let
and
be given as follows:
×
Then, the (partial) correctness of Grover’s algorithm is specified by the following Hoare triple.
×
We now briefly outline the proof strategy. Following the definition of
, the proof of the above Hoare triple is divided into three main parts, for the initialization by Hadamard matrices, for the while loop, and for the measurement at the end.
In each part, assertions are first inserted around commands according to the Hoare rules to form smaller Hoare triples. In particular, the precondition of the while loop part is exactly the invariant of the loop. Moreover, it has to be shown that these assertions satisfy the conditions for being quantum predicates, which involve computing their dimension, showing positiveness, and being bounded by the identity matrix under the Löwner order. Then, these Hoare triples are derived using our deduction system. Before combining them together, we have to show that the postcondition of each command is equal to the precondition of the later one. After that, the three main Hoare triples can be obtained by combining these smaller ones.
After the derivation of the three Hoare triples above, we prove the Löwner order between the postcondition of each triple and the precondition of the following triple. Afterwards, the triples can be combined into the Hoare triple below:
×
Finally, the (partial) correctness of Grover’s algorithm follows from the soundness of our deduction system.
5 Discussion
Compared to classical programs, reasoning about quantum programs is more difficult in every respect. Instead of discrete mathematics in the classical case, even the simplest reasoning about quantum programs involves complex numbers, unitary and positivity properties of matrices, and the tensor product. Hence, it is to be expected that formal verification of quantum Hoare logic and quantum algorithms will take much more effort. In this section, we describe some of the automation that we built to simplify the manual proof, and give some statistics concerning the amount of effort involved in the formalization.
5.1 Automatic Proof of Identities in Linear Algebra
During the formalization process, we make extensive use of ring properties of matrices. These include commutativity and associativity of addition, associativity of multiplication, and distributivity. Compared to the usual case of numbers, applying these rules for matrices is more difficult in Isabelle/HOL, since they involve extra conditions on dimensions of matrices. For example, the rule for commutativity of addition of matrices is stated as:
×
These extra conditions make the rules difficult to apply for standard Isabelle automation. For our work, we implemented our own tactic handling these rules. In addition to the ring properties, we also frequently need to use the cyclic property of trace (e.g. \({\text {tr}}(ABC)={\text {tr}}(BCA)\)), as well as the properties of adjoint (\((AB)^{\dag }=B^{\dag }A^{\dag }\) and \(A^{\dag \dag }=A\)). For simplicity, we restrict to identities involving only \(n\times n\) matrices, where n is a parameter given to the tactic.
The tactic is designed to prove equality between two expressions. It works by computing the normal form of the expressions – using ring identities and identities for the adjoint to fully expand the expression into polynomial form. To handle the trace, the expression \({\text {tr}}(A_1\cdots A_n)\) is normalized to put the \(A_i\) that is the largest according to Isabelle’s internal term order last. All dimension assumptions are collected and reduced (for example, the assumption
is reduced to
).
Overall, the resulting tactic is used 80 times in our proofs. Below, we list some of the more complicated equations resolved by the tactic. The tactic reduces the goal to dimensional constraints on the atomic matrices (e.g.
and
in the first case).
Overall, the formalization consists of about 11,500 lines of Isabelle theories. An old version of the proof is developed on and off for two years. The current version is re-developed, using some ideas from the old version. The development of the new version took about 5 person months. Detailed breakdown of number of lines for different parts of the proof is given in the following table.
Description
Files
Number of lines
Preliminaries
4197
Semantics
1110
Hoare logic
1417
Tensor product
1664
Grover’s algorithm
3184
Total
11572
In particular, with the verification framework in place, the proof of correctness for Grover’s search algorithm takes just over 3000 lines. While this shows that it is realistic to use the current framework to verify more complicated algorithms such as Shor’s algorithm, it is clear that more automation is needed to enable verification on a larger scale.
6 Related Work
The closest work to our research is Robert Rand’s implementation of \(\mathcal {Q}\)wire in Coq [49, 50]. \(\mathcal {Q}\)wire [47] is a language for describing quantum circuits. In this model, quantum algorithms are implemented by connecting together quantum gates, each with a fixed number of bit/qubit inputs and outputs. How the gates are connected is determined by a classical host language, allowing classical control of quantum computation. The work [49] defines the semantics of \(\mathcal {Q}\)wire in Coq, and uses it to verify quantum teleportation, Deutsch’s algorithm, and an example on multiple coin flips to illustrate applicability to a family of circuits. In this framework, program verification proceeds directly from the semantics, without defining a Hoare logic. As in our work, it is necessary to solve the problem of how to define extensions of an operation on a few qubits to the global state. The approach taken in [49] is to use the usual Kronecker product, augmented either by the use of swaps between qubits, or by inserting identity matrices at strategic positions in the Kronecker product.
There are two main differences between [49] and our work. First, quantum algorithms are expressed using quantum circuits in [49], while we use quantum programs with while loops. Models based on quantum circuits have the advantage of being concrete, and indeed most of the earlier quantum algorithms can be expressed directly in terms of circuits. However, several new quantum algorithms can be more properly expressed by while loops, e.g. quantum walks with absorbing boundaries, quantum Bernoulli factory (for random number generation), HHL for systems of linear equations and qPCA (Principal Component Analysis). Second, we formalized a Hoare logic while [49] uses denotational semantics directly. As in verification of classical programs, Hoare logic encapsulates standard forms of argument for dealing with each program construct. Moreover, the rules for QHL is in weakest-precondition form, allowing the possibility of automated verification condition generation after specifying the loop invariants (although this is not used in the present paper).
Besides Rand’s work, quite a few verification tools have been developed for quantum communication protocols. For example, Nagarajan and Gay [41] modeled the BB84 protocol [12] and verified its correctness. Ardeshir-Larijani et al. [7, 8] presented a tool for verification of quantum protocols through equivalence checking. Existing tools, such as PRISM [37] and Coq, are employed to develop verification tools for quantum protocols [17, 29]. Furthermore, an automatic tool called Quantum Model-Checker (QMC) is developed [28, 46].
Recently, several specific techniques have been proposed to algorithmically check properties of quantum programs. In [63], the Sharir-Pnueli-Hart method for verifying probabilistic programs [54] has been generalised to quantum programs by exploiting the Schrödinger-Heisenberg duality between quantum states and observables. Termination analysis of nondeterministic and concurrent quantum programs [38] was carried out based on reachability analysis [64]. Invariants can be generated at some steps in quantum programs for debugging and verification of correctness [62]. But up to now no tools are available that implements these techniques. Another Hoare-style logic for quantum programs was proposed in [36], but without (relative) completeness.
Interactive theorem proving has made significant progress in the formal verification of classical programs and systems. Here, we focus on listing some tools designed for special kinds of systems. EasyCrypt [10, 11] is an interactive framework for verifying the security of cryptographic constructs in the computational model. It is developed based on a probabilistic relational Hoare logic to support machine-checked construction and verification of game-based proofs. Recently, verification of hybrid systems via interactive theorem proving has also been studied. KeYmaera X [26] is a theorem prover implementing differential dynamic logic (\(d\mathcal {L}\)) [48], for the verification of hybrid programs. In [60], a prover has been implemented in Isabelle/HOL for reasoning about hybrid processes described using hybrid CSP [34].
Our work is based on existing formalization of matrices and tensors in Isabelle/HOL. In [59] (with corresponding AFP entry [58]), Thiemann et al. developed the matrix library that we use here. In [14] (with corresponding AFP entry [13]), Bentkamp et al. developed tensor analysis based on the above work, in an effort to formalize an expressivity result of deep learning algorithms.
7 Conclusion
We formalized quantum Hoare logic in Isabelle/HOL, and verified the soundness and completeness of the deduction system for partial correctness. Using this deduction system, we verified the correctness of Grover’s search algorithm. This is, to our best knowledge, the first formalization of a Hoare logic for quantum programs in an interactive theorem prover.
This work is intended to be the first step of a larger project to construct a framework under which one can efficiently verify the correctness of complex quantum programs and systems. In this paper, our focus is on formalizing the mathematical machinery to specify the semantics of quantum programs, and prove the correctness of quantum Hoare logic. To verify more complicated programs efficiently, better automation is needed at every stage of the proof. We have already begun with some automation for proving identities in linear algebra. In the future, we plan to add to it automation facility for handling matrix computations, tensor products, positivity of matrices, etc., all linked together by a verification condition generator.
Another direction of future work is to formalize various extensions of quantum Hoare logic, to deal with classical control, recursion, concurrency, etc., with the eventual goal of being able to verify not only sequential programs, but also concurrent programs and communication systems.
Acknowledgements
This research is supported through grants by NSFC under grant No. 61625206, 61732001. Bohua Zhan is supported by CAS Pioneer Hundred Talents Program under grant No. Y9RC585036. Yangjia Li is supported by NSFC grant No. 61872342.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
[25] and Q# [57], IBM’s OpenQASM [22], Google’s Cirq [30], ProjectQ [56], Chisel-Q [40], Quil [55] and \(Q\left| SI \right\rangle \) [39]. These research allow quantum programs to first run on an ideal simulator for testing, and then on physical devices [5]. For instance, many small quantum algorithms and protocols have already been programmed and run on IBM’s simulators and quantum computers [1, 2].
.
.
.
.
, where \(\bigvee \) stands for the least upper bound of partial density operators according to the Löwner partial order \(\sqsubseteq \).
of vectors with entries in type
is defined as pairs (n, f), where n is a natural number, and f is a function from natural numbers to
, such that f(i) is undefined when \(i\ge n\). Likewise, the type
of matrices is defined as triples (nr, nc, f), where nr and nc are natural numbers, and f is a function from pairs of natural numbers to
, such that f(i, j) is undefined when \(i\ge nr\) or \(j\ge nc\). The terms
(resp.
) represent the set of vectors of length n (resp. matrices of dimension \(m\times n\)). In our work, we focus almost exclusively on the case where
is the complex numbers. For this case, existing libraries already define concepts such as the adjoint of a matrix, and the (complex) inner product between two vectors. We further define concepts such as Hermitian and unitary matrices, and prove their basic properties.
as follows: 
denotes the product of a list of natural numbers). 
is a measurement with n options,
for \(i < n\) are the measurement matrices, and
is the command to be executed when the measurement yields result i. Likewise, the first argument to
gives measurement matrices, where only the first two values are used.
expresses the well-formedness condition. For a quantum program to be well-formed, all matrices involved should have the right dimension, the argument to
should be unitary, and the measurements for
and
should satisfy the condition \(\sum _i M_i^{\dag }M_i=\mathbb {I}_n\). Denotation is written as
, defined as in Sect. 2. Both
and
is defined by induction over the structure of the program. The details are omitted here.
) if it can be derived by combining the rules in Fig. 1. This condition can be defined in Isabelle/HOL as an inductive predicate. The definition largely parallels the formulae shown in the figure.
and
(used in [13] to convert between tensors represented as a list and matrices). Given a list of dimensions \(d_i\), the encode and decode operations (named
and
) produce a correspondence between lists of indices \(a_i\) satisfying \(a_i<d_i\) for each \(i<n\), and a natural number less than \(\prod _i d_i\). This works in a way similar to finding the binary representation of a number (in which case all “dimensions” are 2). List operation
constructs the subsequence of
containing only the elements at indices in the set
.
extends
, adding
for a subset of quantum variables. Our goal is to define the tensor product of two vectors or matrices over
and its complement
, respectively.
and
are dimensions of variables
and
:
(resp.
) provides the map from the product of
to the product of
(resp.
).
is the product of
).
and
, including that they behave correctly with respect to identity, multiplication, adjoint, and trace.
is the identity (here
is the product of
).
, we can define “partial” versions of quantum program commands
,
and
. They take a set of variables \(\overline{q}\) as an extra parameter, and all matrices involved act on the vector space associated to \(\overline{q}\). These commands are named
,
and
. They are usually used in place of the global commands in actual applications.
to define tensor product in this more general setting, we need to find the relative position of variables
within
. This is done using
, which counts the position of
within
. 
locale, we must use qualified names for
and
, and supply extra arguments for variables in the locale. Here
is the total list of dimensions). 
is defined in a similar way as before. 
and
satisfy several key consistency properties. In particular, they satisfy associativity of tensor product. For matrices, this is expressed as follows:
in Isabelle) is given by:For example, in Grover’s algorithm, we need to apply the Hadamard transform on each of the first n quantum variables, given by
. A single Hadamard transform on the i’th quantum variable, extended to a matrix acting on the first n quantum variables, is defined as follows:
, where
is defined as follows.
defined as
.
denotes the tensor product of a matrix on the first n variables (of dimension \(2^n\times 2^n\)) and a matrix on the loop variable (of dimension \(K\times K\)). Executing this program is equivalent to multiplying the quantum state corresponding to the first n variables by \(H^{\otimes n}\), as shown in Sect. 3.5.
,
and
can be defined directly.
be the outer product \(vv^{\dag }\), and
be \(|k\rangle \langle k|\), where \(|k\rangle \) is the k’th basis vector on the vector space corresponding to the loop variable. Let
and
be given as follows: 
, the proof of the above Hoare triple is divided into three main parts, for the initialization by Hadamard matrices, for the while loop, and for the measurement at the end.
is reduced to
).
and
in the first case).
