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].

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 algorithmFootnote 1. In more detail, the contributions of this paper are as follows.

  1. 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. 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. 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:

$$S{{:}{:}}=\mathbf{skip}\mid \overline{q}:=U\overline{q}\mid S_1;S_2\mid \mathbf{measure}\ M[\overline{q}]:\overline{S}\mid \mathbf{while}\ M[\overline{q}]=1\ \mathbf{do}\ S$$

where

  • 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 while b do S.

Fig. 1.
figure 1

Proof system \(\textit{qPD}\) for partial correctness

Full size image

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. 1.

    .

  2. 2.

    .

  3. 3.

    .

  4. 4.

    .

  5. 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:

$$\models _{\textit{par}}\{P\}S\{Q\} \text{ iff } {\text {tr}}(P\rho )\le {\text {tr}}(Q\llbracket S\rrbracket (\rho ))+{\text {tr}}(\rho )-{\text {tr}}(\llbracket S\rrbracket (\rho ))$$

for all partial density operators \(\rho \). Here \({\text {tr}}\) is the trace of a matrix. The semantics for total correctness is defined similarly:

$$\models _{\textit{tot}}\{P\}S\{Q\} \text{ iff } {\text {tr}}(P\rho )\le {\text {tr}}(Q\llbracket S\rrbracket (\rho )).$$

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:

figure i

Next, the Löwner partial order is defined as a partial order on the type as follows:

figure k

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:

figure l

The total dimension d is given by (here denotes the product of a list of natural numbers).

figure n

The (mixed) state of the system is given by a partial density operator with dimension \(d\times d\). Hence, we declare

figure o
figure p

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.

figure q

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:

figure ac

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.

figure ad
figure ae

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).

figure ag
figure ah

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.

figure au

First, and are dimensions of variables and :

figure az

The operation (resp. ) provides the map from the product of to the product of (resp. ).

figure bf

With this, tensor products on vectors and matrices are defined as follows (here is the product of ).

figure bi
figure bj

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 ).

figure bp

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:

figure bx

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 .

figure ce

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).

figure cj
figure ck

The partial extension is defined in a similar way as before.

figure cm

The definitions and satisfy several key consistency properties. In particular, they satisfy associativity of tensor product. For matrices, this is expressed as follows:

figure cp

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:

figure cs

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.

figure cv

Crucially, this matrix product of extensions of Hadamard matrices must equal the tensor product of Hadamard matrices. That is, with defined as

figure cx

we have the theorem

figure cy

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)]:

$$\begin{aligned} G^{k}\left| \psi _0 \right\rangle = \cos (\frac{2k+1}{2}\theta )\left| \alpha \right\rangle +\sin (\frac{2k+1}{2}\theta )\left| \beta \right\rangle , \end{aligned}$$

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.

figure cz

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.

figure db

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.

figure dc

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:

figure de

where each of the three matrices , and can be defined directly.

figure di

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.

figure dj

where the measurements for the while loop and at the end of the algorithm are:

figure dk

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:

figure dp

Then, the (partial) correctness of Grover’s algorithm is specified by the following Hoare triple.

figure dq

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:

figure ds

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:

figure dt

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).

$$\begin{aligned} {\text {tr}}(MM^{\dag }(PP^{\dag }))= & {} {\text {tr}}((P^{\dag }M)(P^{\dag }M)^{\dag }) \\ {\text {tr}}(M_0AM_0^{\dag }) + {\text {tr}}(M_1AM_1^{\dag })= & {} {\text {tr}}((M_0^{\dag }M_0+M_1^{\dag }M_1)A) \\ H^{\dag }(Ph^{\dag }(H^{\dag }Q_2H)Ph)H= & {} (HPhH)^{\dag }Q_2(HPhH) \end{aligned}$$

5.2 Statistics

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.