key: cord-0060409-gbpzwvfc
authors: Chareton, Christophe; Bardin, Sébastien; Bobot, François; Perrelle, Valentin; Valiron, Benoît
title: An Automated Deductive Verification Framework for Circuit-building Quantum Programs
date: 2021-03-23
journal: Programming Languages and Systems
DOI: 10.1007/978-3-030-72019-3_6
sha: b2963705bfddbe006ddd0d1175efbf606359be1d
doc_id: 60409
cord_uid: gbpzwvfc

While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.

1.1 Quantum computing. Quantum programming is seen as a potential revolution for many computing applications: cryptography [61] , deep learning [7] , optimization [23, 22] , solving linear systems [33] , etc. In all of these domains, current quantum algorithms beat the best known classical algorithms by either quadratic or even exponential factors. In parallel to the rise of quantum algorithms, the design of quantum hardware has moved from lab-benches [14] to programmable, 50-qubits machines designed by industrial actors [4, 38] reaching the point where quantum computers beat classical computers for specific tasks [4] . This has stirred a shift from a theoretical standpoint on quantum algorithms to a more programming-oriented view with the question of their concrete coding and implementation [66, 65, 55] .

In this context, an important problem is the adequacy between the mathematical description of an algorithm and its concrete implementation as a program.

1.2 The hybrid model. The vast majority of quantum algorithms are described within the quantum co-processor model [42] , i.e. a hybrid model where a classical computer controls a quantum co-processor holding a quantum memory (cf. Figure 1 ). The co-processor is able to apply a fixed set of elementary operations (buffered as quantum circuits) to update and query (measure) the quantum memory. Importantly, while measurement allows one to retrieve classical (probabilistic) information from the quantum memory, it also modifies it (destructive effect). The quantum memory state is represented by a linear combination of possible concrete values, generalizing the classical notion of probabilities to the complex case, and the core of a quantum algorithm consists in successfully setting the memory in a specific quantum state.

Major quantum programming languages such as Quipper [30] , Liqui| [67] , Q# [64] , ProjectQ [63] , Silq [8] , and the rich ecosystem of existing quantum programming frameworks [55] follow this hybrid model. Such circuit-building quantum languages are the current consensus for high-level executable quantum programming languages.

The problem with quantum algorithms. Starting from an initial state, a quantum algorithm typically describes a series of high-level operations which, once composed, realize the desired state. Each high-level operation may itself be described in a similar way, until one reaches elementary operations (quantum gates). Describing an algorithm therefore requires both to list these elementary operations, or quantum circuit, and to specify the circuit's behavior.

A major issue is then to verify that the quantum circuit generated by the code written as an implementation of a given algorithm is indeed a run of this algorithm, and that the circuit has indeed the specified characteristics of shape (for instance: a polynomial size).

While testing and debugging are the common verification practice in classical programming, they become extremely complicated in the quantum case: debugging and assertion checking are problematic due to the destructive aspect of quantum measurement, the probabilistic nature of quantum algorithms seriously impedes system-level quantum testing, and classical emulation of quantum algorithms is (strongly believed to be) intractable. On the other hand, nothing prevents a priori the formal verification [15] of quantum programs.

Our goal is to provide an automated formal verification framework for circuit-building quantum programs. Such a framework should satisfy the following principles: (1) Parametricity: it should allow parametric (i.e. scale-invariant) specifications and proofs, so as to enable the generic specification and verification of parametrized implementations. This is crucial as quantum algorithms always describe parametrized families of circuits; (2) Proof automation: it should, as far as possible, provide automatic proof means in order to ease adoption.

Prior works on quantum formal verification do not fully reach these goals together, as they are either not parametric, or not automated. Model-checking methods [27, 70] are fully automatic but not parametric -moreover they are highly scale-sensitive. Recently, Amy [1, 2] developed a powerful framework for reasoning over quantum circuits, the path-sums symbolic representation. Thanks to their good compositional properties, reasoning with path-sums is well automated and can scale up to large problem instances (up to 100 qubits). Yet, the method is not parametric and only addresses fixed-size circuits. On the other side of the spectrum, several approaches deal with parametricity but sacrifice automation as they generate proof obligations in higher-order logic, supported with proof assistants such as Coq or Isabelle/HOL. One can cite the approach of Boender et al. [10] , Qwire [53, 58] , SQIR [35, 34] or QHL [68, 71, 46, 69, 45] . Combined with the use of the standard matrix semantics for quantum circuitsthat we show in Section 8 cumbersome for automation -only very few realistic quantum programs have been verified in a parametric way [45, 35, 34] .

1.5 Proposal. We propose Qbricks, an automated formal verification framework for circuit-building quantum programs, featuring parametric specification together with a high degree of proof automation.

We bring two key innovations along the road: (Key 1) we propose the new parametrized path-sums (PPS) symbolic representation of families of quantum circuits, extending path-sums [1] to the parametric case while keeping good compositional properties. PPS prove extremely useful both as a specification mechanism and as an automation mechanism; (Key 2) we carefully tune together our programming language (Qbricks-DSL) and specification logic (Qbricks-Spec) so that the corresponding verification problem remains automatable in practice -first-order proof obligations -while the framework is still expressive enough to write, specify and verify realistic quantum programs (Shor order finding -Shor-OF [61] , QPE [41, 16] , Grover [31] ).

1.6 Contributions. We bring the following contributions.

-A flexible symbolic representation for reasoning about quantum states, building upon the recent path-sum symbolic representation [1, 2] . Our representation, called parametrized path-sums (PPS), retains the compositional and closure properties of regular path-sums while allowing genericity and parametricity of both specifications and proofs. Especially, first-order logic together with PPS provide a unified and powerful way to reason about many essential quantum concepts (Section 5.2) and fit well with the standard way of describing quantum algorithms. We are the first to highlight this connection and make PPS a "first-class" concept, where prior works are limited to standard path sums, or rely on the standard matrix semantics; -A programming and verification framework, that is: on one hand, a core domain-specific language (Qbricks-DSL, Section 4) for describing families of quantum circuits, with enough expressive power to describe parametric circuits from non-trivial quantum algorithms; and on the other hand, a first-order logical (domain-specific) specification language (Qbricks-Spec, Section 5), tightly integrated with PPS and Qbricks-DSL to specify properties of parametrized programs representing families of quantum circuits. The careful interplay between these two components yields first-order proof obligations, and thus is a key aspect of proof automation;

-A dedicated proof engine: we introduce the Hybrid Quantum Hoare Logic (HQHL) deduction system for deductive verification over circuit-building quantum programs. It is tightly coupled with PPS and produces proof obligations in the Qbricks-Spec logic (Section 6); -This framework is embedded in the Why3 deductive verification tool [9, 24] as a DSL (Section 7), and provides proof automation mechanisms dedicated to the quantum case. This material is grounded in standard mathematics theories (linear algebra, arithmetic, complex numbers, binary operations, etc.) with 450+ definitions and 1,000+ lemmas. All lemmas have been proved in Why3, and the whole framework is publicly available; -We present in Section 8 the first ever verified parametric implementation of the quantum part of Shor's factoring algorithm [61] (Order Finding, including the polynomial complexity of the circuits produced by our implementation and probability requirements), as well as verified parametric implementations of other major quantum algorithms: Quantum Phase Estimation (QPE) [41, 16] 3 , Grover's (search) algorithm [31] and Quantum Fourier Transform (QFT) [18] . Our method achieves a high level of proof automation (96% on Shor-OF), significantly reducing proof effort (factor 13.6x vs. QHL on Grover, factors 7.7x and 6.4x vs. SQIR on resp. QPE and Grover).

Additional technical material can be found in the online extended versione [13] . Implementation and benchmarks are available online [54] .

1.7 Discussion. The scope of this paper is limited to proving properties of circuit-building quantum programs. We do not claim to support right now the interactions between classical data and quantum data (referred to as "classical control" in the literature), nor the probabilistic side-effect resulting from the measurement. Still, we are already able to target realistic implementations of famous quantum algorithms, and thanks to equational theories for complex and real number we can automatically reason on the probabilistic outcome of a measurement. Also, we do not claim any novelty in the proofs for Shor-OF, QPE or Grover by themselves, but rather the first highly-automated parametric correctness proofs of the circuits produced by programs implementing them, and the first parametric correctness proofs of an implementation of Shor-OF.

While in classical computing, the state of a bit is either 0 or 1, in quantum computing [50] the state of a quantum bit (or qubit) is described by amplitudes over the two elementary values 0 and 1 (denoted in the Dirac notation with |0 and |1 ), i.e. linear combinations α 0 |0 + α 1 |1 where α 0 and α 1 are any complex values satisfying |α 0 | 2 + |α 1 | 2 = 1. In a sense, amplitudes are generalization of probabilities. More generally, the state of a qubit register of n qubits ("qubit-vector") is any superposition of the 2 n elementary bit-vectors ("basis element", where a bit-vector k ∈ {0..2 n − 1} is denoted |k n ), that is any |u n = 2 n −1 k=0 α k |k n such that 2 n −1 k=0 |α k | 2 = 1. For example, in the case of two qubits, the basis is |00 , |01 , |10 and |11 (also abbreviated |0 2 , |1 2 , |2 2 and |3 2 ). Such a (quantum state) vector |k n is called a ket of length n (and dimension 2 n ).

Technically speaking, we say that the quantum state of a register of n qubits is represented by a normalized vector in a Hilbert space of finite dimension 2 n (a.k.a. finite-dimensional Hilbert space), whose basis is generated by the Kronecker product (a.k.a. tensor product, denoted ⊗) over the elementary bitvectors. For instance, for n = 2: |0 ⊗ |0 , |0 ⊗ |1 , |1 ⊗ |0 and |1 ⊗ |1 act as definitions for |00 , |01 , |10 and |11 .

2.1 Quantum data manipulation. The core of a quantum algorithm consists in manipulating a qubit register through two main classes of operations.

(1) Quantum gate. Local operation on a fixed number of qubits, whose action consists in the application of a unitary map to the corresponding quantum state vector i.e. a linear and bijective operation preserving norm and orthogonality. The fact that unitary maps are bijective ensures that every unitary gate admits an inverse. Unitary maps over n qubits are usually represented as 2 n × 2 n matrices.

(2) Measurement. The retrieval of classical information out of the quantum memory. This operation is probabilistic and modifies the state of a quantum register: measuring the n-qubit system 2 n −1 k=0 α k |k n returns the bitvector k of length n with probability |α k | 2 . Quantum gates might be applied in sequence or in parallel: sequence application corresponds to map composition (or, equivalently, matrix multiplication), while parallel application corresponds to the Kronecker product, or tensor product, of the original maps -or, equivalently, the Kronecker product of their matrix representations. 4

. combinators, including: parallel and sequential compositions, circuit inverting, controlling, iteration, ancilla creation, etc. As an example of a quantum circuit, we show in Figure 2 the bird's-eye view of the circuit for QPE, the (quantum) phase estimation algorithm, a standard primitive in many quantum algorithms. QPE is parametrized by n (a number of wires) and U (a unitary oracle) and is built as follows. First, a register of n qubits is initialized in state |0 , while another one is initialized in state |v n . Then comes the circuit itself: a structured sequence of quantum gates, using the unary Hadamard gate H, the circuits U 2 i (realizing U to the power 2 i ) and the reversed Quantum Fourier Transform inverse(QFT (n)) . Sub-circuits U 2 i and inverse(QFT (n)) are both defined in a similar way.

Here, one should simply note two things: (1) the circuit is made of parallel compositions of Hadamard gates and of sequential compositions of controlled U 2 i (the controlled operation is depicted with vertical lines and symbol •); (2) the circuit is parametrized by n and by U . This is very common: in general, a quantum algorithm constructs a circuit whose size and shape depend on the parameters of the problem. It describes a family of quantum circuits.

Reasoning on circuits and the matrix semantics. Quantum circuits essentially describe unitary operators [50] acting on Hilbert spaces. In finite dimension, unitary matrices faithfully represent unitary operators: it has been the original mathematical formalism for circuits -coined here as the matrix semantics. If this representation is well-adapted for representing simple high-level circuit combinators such as the action of control or inversion, it is not well-suited for specifying the behavior of many complex circuits coming from the literature. Because of this cumbersomeness, textbook descriptions of circuits make use of an informal representation: operators are described by their action on a basis vector (see, for example the description of Shor-OF in [50, p. 232] ). This is however understood as a shortcut notation for matrices which remains the main medium for reasoning on circuits. Formal approaches to quantum computation [35, 34, 53, 58, 68, 71, 46, 69, 45] witness this prevalence of matrices as circuit representation.

2.4 Path-sum representation. Path sums [1, 2] are a recent symbolic representation. Its strength is to formalize the notation used in quantum algorithm literature (eg, [50] ). A unitary operator U is written as U : |x → PS(x) where x is a bit vector and PS(x) is defined with the syntax of Fig. 3 . In the Figure, addition and multiplication over real are denoted rescpectively with + and ·, and x [i] is the i th projection of bit vector x. The term n is an integer index, characterizing the range of the path-sum. Then each term k ∈ 0, 2 n in the path-sum is defined through:

1. the phase polynomial P k (x) -a real value building complex scalar e 2·π·i·P k (x) ; 2. the basis-ket function φ k (x), defining the ket-vector |φ k (x) this scalar value applies to.

This representation is closed under functional composition and Kronecker product. For instance, if U is defined as in Fig. 3 and if V sends y to P S (y) defined 

which is in the form shown in Figure 3 . The compositionality of this semantics is used by Amy [2] to prove the equivalence of large circuit instances. Nonetheless, its main limitation stands in the fact that path-sums only address fixed-size circuits. Albeit a compositional tool, useful to automate proofs, it cannot be used for proving properties of parametrized circuit-building quantum programs. This paper proposes an extension of path-sum semantics to address the parametric verification of quantum programs.

In this section, we introduce the main logical apparatus of our framework: parametrized path-sums. We first present a motivating example and then discuss the construction.

A circuit C n defined as

Precondition: n ≥ 0 is even.

Post-conditions: C n sends |x to |x C n consists of n gates. Let us consider the n-indexed family of circuits consisting of n Hadamard gates, in sequence, as shown in Figure 4 . Sequencing two Hadamard gates can easily be shown equivalent to the identity operation. In other word, when fed with |0 , if n is even the circuit outputs |0 . Albeit small, this circuit family together with its simple specification exemplifies the typical framework we aim at in the context of certification of quantum programs.

-The description of the circuit family is parametrized by a classical parameter (here, the non-negative integer n);

-The pre-condition imposes both constraints (here, the evenness of n) and soundness conditions (here, the non-negativeness of n) on the parameters; -The post-condition can both refer to the semantics of the circuit result and to its form and shape (here, its size).

The circuit family presented in Figure 4 will be used in the rest of the paper as a running, toy example for Qbricks. In particular, we show in Example 1 how to code it in our framework and how to express the specification in Example 4. Its parametrized implementation in Qbricks is three lines of code long and its specifications takes six lines. It is proved by recurrence over the parameter n, the induction step requiring two calls for lemmas (depending on the evenness of parameter n).

3.2 Parametrizing path-sums. In order to formalize the semantics of the example of Fig. 4 , we aim at generalizing path-sums.

For a fixed n, the circuit C n implements either the identity (when n is even), in which case the path-sum is P S Id (x) = 1

k=0 e 2iπ k·x 2 |k A candidate parametric path-sum for the family of circuits {C n } n from Figure 4 could then be written in factorized form as

Generalization. In general, parametrized Path Sums (PPS) are defined over a language of typed terms with possibly free (typed) variables. At the very minimum the language has to be equipped with Boolean values (to handle the values of the ket-vector) and integers (for instance to handle the range). Given such a language, a PPS is a path-sum where the range, the phase polynomial and the basis-ket can in general be explicit, open terms referring to external parameters. Formally, a pps is defined as a function inputting a set of parameters p and outputting:

a parametrized integer pps_width(h, p), featuring the number of qubits the target circuit is acting on -its width; -another parametrized integer pps_range(h, p), abbreviated as r(h, p). It indicates the range of the sum (defined as the set BV r(h,p) of bit vectors of length r(h, p)); -a basis ket function pps_ket(h, p), generalizing term φ from Table 3 . For any pair (x, y), of a bit vector x of length pps_width(h, p) (standing for an input basis vector) and a bit vector of length r(h, p), it returns a bit vector of length pps_width(h, p) (standing for an output basis vector); -a parametrized angle function pps_angle(h, p)(x, y), generalizing the phase polynomial P from Table 3 . For any pair (x, y) such as above, it returns a real value θ.

Then, the behaviour of a parametrized quantum circuit C(p) is described as the i/o function inputting a basis ket |x(p) of length the width of C(p) and outputting the parametrized sum term:

For sake of readability, we often ommit the explicit mention of the parameters. For instance, the PPS P induced by (2) is parametrized by the integer n. It is such that for any int n, pps_width(P, n) = 1 and pps_range(P, n) = n%2. Furthermore for any bit vectors x, y of lengths 1 and n%2, pps_ket(P, n)(x, y) is equal to x if n is even and to y otherwise, and pps_angle(P, n)(

. One then gets expression (2) by applying pps_apply(P, p). Hence, the term language needed for describing PPS of otherwise sophisticated families of quantum circuits can afford to be minimal: first-order typed terms equipped with an equational theory are enough. We also find out that first-order, predicate logic is suitable for specifying the properties of quantum programs: there is no need for higher-order logic such as the ones of Coq or Isabelle/HOL. This is the key to automation.

Qbricks-DSL is the (domain-specific) language of our framework. It is designed as a first-order, functional language aimed at circuit description. Measurement is out of the scope of the language, and all Qbricks-DSL expressions are terminating. We follow a very simple strategy for circuit building: we use a regular inductive datatype for circuits, where the data constructors are elementary gates, sequential and parallel composition, and ancilla creation. In particular, unlike Quipper [30] or Qwire [53] , a quantum circuit is not a function acting on qubits: it is a simple, static object. Nonetheless, as illustrated by our experimentations (Section 8), this does impede neither expressiveness nor parametricity.

Furthermore, even if the language does not feature measurement, it is nonetheless possible to reason on probabilistic outputs of circuits, if we were to measure the result of a circuit. Indeed, this can be expressed in a regular theory of real and complex numbers (See Section 6.5).

Qbricks-DSL is a small first-order functional, call-by-value language with a special datatype circ as the medium to build and manipulate circuits. The core of Qbricks-DSL can be presented as the simply-typed calculus presented in Figure 6 . The basic data constructors for circ are CNOT, SWAP, ID, the Hadamard superposition gate H, phase shift gate Ph(e) and the parametrized rotation R z (e). The constructors for high-level circuit operations are sequential composition SEQ, parallel composition PAR and ancilla creation/termination ANC (see Figure 5 for details). On top of circ, the type system of Qbricks-DSL features the type of integers int (with constructors n, one for each integer n), the type of Booleans bool (with constructors tt and ff) and the type of n-ary products (with constructor e 1 , . . . , e n ). This type system is not meant to be exhaustive and it can be extended with usual constructs such as floats, lists and other user-defined inductive datatypes -its embedding into WhyML makes it easy to use such types. The term constructs are limited to function calls, let-style composition, test with if-then-else and simple iteration: iter f n a stands for f (f (· · · f (a) · · · )), with n calls to f . We again stress that this could easily be extended -we just do not need it.

The language is first-order: this is reflected by the types A of expressions. The type of a function is given by the types of its arguments and the type of its output. The type of a function with inputs of types A i and output of type B is written Figure 5 for the intuitive definition of circuit combinators. The typing rules are the usual ones, summarized for convenience in Table 7 .

As any other regular functional programming language, Qbricks-DSL is equipped with an operational semantics based on beta-reduction and substitution. We define a notion of value and applicative context as in Fig. 6 . We then define a rewriting strategy as the relation defined with C[e] → C[e ] whenever e → e is one of the rule of Table 8 . The table is split into the rules for the language constructs and the rules defining the behavior of the constant functions. We only give a subset of the latter rules. For instance, the arithmetic operations are defined in a canonical manner, and the Boolean and comparison operators are defined in a similar manner on values of type int and bool. The rules for the constant functions acting on circuits are also for the most part straightforward: the size of a sequence is the sum of the sizes of the compounds for instance. The rules which we do not provide are the ones for the control operation ctl: the intuition behind their definition can be found in [13] . For the elementary gates, any definition can be used (see e.g. [50] ), as long as it can be written with the chosen set of gates. One just has to adjust the lemmas referring to ctl in Qbricks-Spec. Similarly, the inverse of elementary gates are not given: we can choose the usual ones from the literature -and this definition is then parametrized by the choice of gates.

4.3 Properties. The targeted low-level representation for an expression of type circ is a value made of the circuit data constructors presented in Table 6 : a value v of type circ is made out of the grammar

Since recursions are reduced to finite iterations, we can derive the following lemma through a simple inductive reasoning: if tt then e1 else e2 → e1 if ff then e1 else e2 → e2 when n ≤ 0: iter f n a → a when n > 0: iter f n a → f (iter f n − 1 a) Constant functions (subset of the rules) 

A universal (resp. pseudo-universal ) set of elementary gates is such that they can be composed thanks to sequence or parallelism so as to perform (resp. approach arbitrarily close) any unitary matrix. In Qbricks-DSL, we chose the small pseudouniversal elementary set {CNOT, SWAP, ID, H} ∪ n∈N {Ph(n), R z (n), }. Other gates can then be defined as macros on top of them. If one aims at using Qbricks inside a verification compilation tool-chain, these macros can for instance be the gates of the targeted architecture.

A circuit is represented as a rigid rectangular shape with a fixed number of input and output wires. In particular, there is a notion of validity: a circ object only makes sense provided two constraints:

in SEQ(C 1 , C 2 ), the two circuits C 1 and C 2 should have the same width. For instance, SEQ(CNOT, H) is not valid. This is a simple syntactic constraint; -in ANC(C), the circuit C should have n + 1 wires. Moreover, if given as input a vector where the last qubit is in state |0 , its output should also leave this qubit in state |0 . This condition is, on the other hand, a semantic constraint.

Note that even these syntactic constraints cannot be checked by a simple typing procedure, because of the higher-order reasoning involved here: the constraints must hold for any value of the parameters. All these constraints apply on parametrized circuits. They translate into constraints for the parameters of their related PPS and are expressed in our domain-specific logical specification language, Qbricks-Spec. They are meant to be sent as proof obligations to a proof engine.

Example 2. Note how the circuit generated by main in Example 1 is not necessarily a valid circuit (although in this case it is). This is one of the constraints that can be handled by Qbricks-Spec, as shown in Example 4.

As all expressions in Qbricks-DSL are terminating, one can use regular sets as denotational semantics for the language. In order to be able to handle the definitions coming up in Section 5, we include in the denotation of each type an "error" element ⊥ We therefore define the denotation of basic types as the set of their values: Note that in the denotational semantics one can build non-valid circuits. For instance, the circuit SEQ(CNOT, H) is a member of [|circ|]. This is to be expected as we have the following property: It is however possible to formalize the notion of syntactically valid circuits as a subset of [|circ|]. Definition 1. We define the (syntactic) unary relation V syntax on [|circ|] as follows: Each one of the gates belongs to V syntax ; if C 1 and C 2 belongs to V syntax then so does PAR(C 1 , C 2 ); if moreover 2 ≤ [|width|](C 1 ) then ANC(C 1 ) belongs to V syntax and if [|width|](C 1 ) = [|width|](C 2 ) then SEQ(C 1 , C 2 ) belongs to V syntax .

The language Qbricks-DSL is only aimed at manipulating circuits. The reasoning features of Qbricks -and the PPS introduced in Section 3-are defined in the logic and the specification tools offered within Qbricks-Spec.

We define Qbricks-Spec as a first-order, predicate logic with the following syntax.

Formula φ, ψ :

The first-order expressionsê form a subset of Qbricks-DSL: they are restricted to variables and (formal) function calls to other first-order expressions. Unlike regular, general expressions -meant to be computational vehicles-these firstorder expressions only aim at being reasoned upon. The function names are then expanded with counterpart logical functions f . Among these new functions, we introduce one function iter f : int × A → A for each function f : A → A, standing for the equational counterpart of the iteration 5 . The logic functions are defined equationally in the logic: see Section 6.4 for details. The relation R ranges over a list of constant relations over first-order expressions. In Qbricks-Spec, we identify relations and functions of return type bool. A special relation is the equality: we explicitly introduce it in the syntax to emphasize the fact that Qbricks-Spec is meant to deal with equational theories.

The type system of Qbricks-Spec is extended with opaque types, equipped with constant functions and relations to reason upon them. They come with no computational content: the aim is purely to be able to express and prove specification properties of programs. This is why we do not incorporate them in Qbricks-DSL's type system.

The opaque types we consider in Qbricks-Spec are complex, real, pps, ket and bitvector. The operators and relations for these new types are given in Table 9 . Note that in the rest of the paper we will omit the cast operations i_to_r and r_to_c. We will also use a declared exponentiation function [−] [−] overloaded with types complex × int → complex and real × int → real. For any integer n and boolean b, constructor bv_cst buildsthe bit vector of length n and constant value b. Other functions for types complex, real and bitvector are standard. Types pps and ket are novel and form the main reasoning vehicle in Qbricks-Spec.

The types pps and ket. In short, the type pps encodes our parametrized path sum (PPS) representation for expressions of type circ in Qbricks-DSL, while ket encodes the notion of ket-vector. As these types are pure reasoning apparatuses, we only need them in Qbricks-Spec and they are defined uniquely through an equational theory. The type pps is equipped with four opaque accessors: pps_width, pps_width, pps_width, pps_ket and pps_angle acting on pps from Section 3.2 and with the function circ_apply. If path-sums compose nicely, a given linear map does not have a unique representative path-sum (partly due to the fact that phase polynomials are equal modulo 2π). To capture this equivalence, we introduce the constant relation pps_equiv. In order to relate circuits and PPS, we introduce the constant function circ_to_pps: it returns one possible PPS that represents the input circuit. The chosen PPS is built in a constructive manner on the structure of the circuit. A useful relation is (− −) relating a circuit and a PPS: it is defined as (c h) pps_equiv(circ_to_pps(c), h). Another useful macro is function circ_apply : circ × ket → ket, defined as circ_apply(C, k) pps_apply(circ_to_pps(C), k)

The type ket is equipped with standard operations for manipulating ketvectors (Table 9 ). bv_to_ket turns a bit vector into a basis ket-vector ; ket_length returns the number of qubits in the ket ; ket_get returns the amplitude of the corresponding basis ket-vector. The other operations are the usual operations on vectors: addition, subtraction, tensors, scalar multiplication. The defined PPS follows the structure of the circuit. For instance, as shown in Eq. (1) on Page 154 the PPS circ_to_pps(SEQ(C 1 , C 2 )) is the sequential composition of the two PPS circ_to_pps(C 1 ) and circ_to_pps(C 2 ). This kind of compositionality is what helps with automation.

Qbricks-Spec. Formulas in Qbricks-Spec are typed objects -and, as mentioned in Section 5.1 one can identify them with firstorder expressions of type bool. Due to this correspondence, we shall only say that logic judgments in Qbricks-Spec are well-formed judgments of the form Δ φ where the well-formedness means that Δ φ : bool is a valid typing judgment in Qbricks-DSL. That being said, a well-formed judgment Δ φ is valid whenever it holds in the denotational semantics: for every instantiation σ sending x : A in Δ to [|A|], the denotation [|φ|] σ is valid. In particular, the (free) variables of φ can be regarded as universally quantified by the context Δ.

A regular path-sum is not parametric: it represents one fixed functional. So why did we chose [|pps|] to be a set of path-sums? Let us consider an example. It can be regarded as a relation between PPS h and integers n, valid whenever h represents main(n). Technically, this relation is not quite the graph of a function (since several PPS might match the circuit main(n)).

Similarly to the type pps, Qbricks is endowed with a (logical) type matrix to handle the matrix interpretation of circuits, together with various functions and relations to reason on it. In particular, Qbricks features a function mat_get : matrix × int × int → complex, formalizing the access to a matrix element, and a function circ_to_mat : circ → matrix realizing the matrix corresponding to a circuit. We then formally show, within our framework (proven in Why3), that for any valid circuit C and ket k of length width(C), applying circ_to_pps(C) on k is equivalent to multiplying it by circ_to_mat(C):

Theorem 1 (Soundness of PPS wrt matrix semantics).

C : circ, k : ket ket_length(k) = width(C) ∧ valid(C) → apply_mat(circ_to_mat C, k) = pps_apply(circ_to_pps C, k)

Thanks to the logic presented in Section 5.4, it is possible to write Qbricks-Spec formulas and to express properties of terms of the restricted syntax of Section 5.1. Provided that the regular sequents are simple enough, these can automatically be handled with the use of SMT solvers.

In this section, we define a specific Hoare logic, Hybrid Hoare Logic (HQHL), to express pre-and post-conditions for arbitrary Qbricks-DSL terms. We then discuss the validity of such judgments and explain how to decompose them into elementary, regular sequents (proof obligations). The claim -backed up by our experiments in Section 8-is that the obtained sequents are in practice simple enough to be dealt with automatically.

We do not present all HQHL rules here, but simply aim to give an intuition of how and why one can rely on an automated deductive system to derive Qbricks-Spec judgments. The complete set of HQHL rules is presented in [13] .

6.1 HQHL judgments. In order to be able to express program specifications with pre-and post-conditions, we introduce Hybrid Quantum Hoare Logic (HQHL) sequents of the form Δ {φ}e{ψ} : A (we omit the type A when irrelevant or clear). The formula ψ can make use of a reserved free variable result of type A. Such a sequent is then well-formed provided that Δ φ : bool, Δ, result : A ψ : bool and Δ e : A are valid typing judgments. Note how the reserved free variable result is being added to Δ for typing ψ. For convenience, as syntactic sugar we allow indexed variables result i to stand for the ith projection of a tuple.

The validity of an HQHL sequent can be defined semantically, similarly to what was done in Section 5.4: Δ {φ}e{ψ} : A is valid whenever it is both well-formed and when for every instantiation σ sending x : A in Δ to [|A|] and sending result to [|e|], the denotation [|φ → ψ|] σ is valid.

In the following sections, we describe the deduction rules that we rely on in Qbricks. They are designed to be used in a bottom-up strategy to break down judgments into pieces reasoning on smaller terms. Along the way, there is the need for introducing invariants and assertions. As usual, some of these assertions can be derived by computing the weakest-preconditions: we do not necessarily have to introduce every single one. When attaining a term of the restricted grammar of Qbricks-Spec that cannot be further decomposed, one can rely on the rule

to generate a proof obligation as a regular sequent in Qbricks-Spec.

6.2 Deduction rules for term constructs. Figure 10 presents the deduction rules for the term constructs of Qbricks-DSL carrying a computational content: iteration, tests, function evaluation, etc. We also present a standard weakening rule (weaken) and an example of rule for rewriting: The deduction rule (eq) states that whenever two expressions are equal one can substitute one 6.3 Deduction rules for pps. The main tools to relate circuits and PPS are the constant function circ_to_pps, its relational counterpart (− −), and the declared function circ_apply. They can be specified inductively on the structure of the input circuit. The complete set of rules for circ_to_pps and (− −) can be found in [13] .

Compositionality of SEQ. For instance, one can derive the deduction rules for circ_apply applied to SEQ from Table 11 . These rules can be used in a bottom-up manner to derive composable, elementary properties of circuits out of sub-circuits. In the table, we abbreviate pps_acc(circ_to_pps(−)) with C acc , for acc ∈ {width, range, ket,angle} and, given two bit vectors x and y, x · y denotes their concatenation.

Example of deduction rule for HAD. Using the notations from above, we define the following axiom for function circ_to_pps applied to the gate HAD: We can now give a specification to the function main, as follows:

The fact that circ_apply is well-defined implies that C is valid.

6.4 Equational reasoning. The SMT solvers we aim at using to discharge proof obligations require equational theories describing how to reason on the constant functions that were introduced. Some of these equational theories, such as bit-vectors and algebraic fields, are standard and well-known in verification. Together with a few properties on square-root, exponentiation, real and imaginary parts, the latter is all we need for real and complex: in quantum computation, the manipulations of real and complex numbers turn out to be quite limitedwe do not need anything related to real or complex analysis.

The main difficulty in the design of Qbricks has been to lay out equational theories and lemmas for circ, pps and ket that can efficiently help in automatically discharging proof obligations. Many of these equations and lemmas are quite straightforward. For instance, we turn the rewriting rules of Table 8 into equations, such as (x, y : circ) width(PAR(x, y)) = width(x) + width(y), or a : A, n : int iter f (a, n + 1) = f (iter f (a, n) ). These equations maps the (syntactic) computational behavior of expressions into the logic.

Other equations express purely semantic properties. For instance,

(together with a few hypotheses ensuring correct widths) can be derived from Table 11 and is part of the equational theory.

6.5 Additional deductive rules. Qbricks provides additional reasoning rules, that we do not have space enough to detail here. Upon them are:

Circuit complexity. Certifying the complexity of quantum implementations (e.g., polynomial number of gates in the size of the input) is of primary importance as in mid-term, implementations will have to deal with limited hardware capacities, hence the need for tight circuit constructions. We stress that, while raised by several programming [30] or compilation works [48] , this aspect of certification is not addressed by existing formal verification approaches [35, 45, 1] .

Probabilities. The probability of obtaining a result by a measurement is correlated with the amplitudes of the corresponding ket-basis vectors in the quantum state of the memory. In Qbricks-Spec we define proba_partial_measure : circ × ket × bitvector → real meaning that when the input circuit is applied to the input ket, if we were to measure the result the probability of obtaining the given vector would be the result of the function.

Wire identification. In some situation, to add a gate in a circuit it is easier to give the number (identifier) of the wire on which the gate applies (such as "apply HAD on wire n") instead of sequencing the circuit with Id ⊗n−1 ⊗ HAD. This is for instance the design chosen in QASM or SQIR [35] .

In Qbricks it is possible to define such a macro with the use of a derived constructor PLACE(C, k, n). For any circuit C and any integers k, n, if 0 ≤ k ≤ n−width(C), PLACE(C, k, n) applies C on wires k to k+width(C)−1. It is defined as ID ⊗k ⊗ C ⊗ ID ⊗n−k−C_width(C) , where for any 0 < i, ID i iter par-ID (i − 1) ID and par-ID(C) PAR(C, ID). Similarly, Qbricks also provides constructor CONT(C, c, k, n) with additional index c in 0, n and not in k, k + width(c) . Using adequate qubit permutation, through combinations of PLACE and SWAP, it applies PLACE(C, k, n) with control c.

The framework described so far is implemented as a DSL embedded inside the Why3 deductive verification platform [9, 25] , written in the WhyML programming language. This allows us to benefit from several strengths of Why3, such as efficient code extraction toward Ocaml, generation of proof obligations (to implement the HQHL mechanism) and access to several proof means: SMT solvers, interactive proof commands or export to proof assistants (Coq, Isabelle/HOL) -although we do not use this latter option in our case-studies.

The development itself counts 17,000+ lines of code, including 400+ definitions and 1700+ lemmas, all proved within Why3. Most of the development concerns the (verified) mathematical libraries. They cover the mathematical structures at stake in quantum computing (complex numbers, Kronecker product, bit-vectors, etc.), together with a formally verified collection of mathematical results. Only two theorems are assumed (for any real x: if 0 ≤ x ≤ 1 then sin(πx) ≤ πx, and x ≤ sin(π x 2 )). Proving them requires function derivation material, not available in Why3 so far. Hence we chose to assume these standard results.

We develop and prove parametric implementations of Grover's search, the Quantum Fourier Transform (QFT), the Quantum Phase Estimation (QPE) and the first ever verified implementation of the quantum part of Shor's algorithm (Shor-OF) . We also implemented Deutsch-Jozsa (DJ) for comparison.

8.1 Examples of formal specifications. Let us first introduce some of the formal specifications we proved. The specification for QPE [41, 16] is shown in Figure 12 (a). The procedure inputs a unitary operator U and an eigenvector |v of U and finds the ghost ( [26] ) eigenvalue e 2πiΦv associated with |v . The specification for Shor-OF [61] is shown in Figure 12 (b). We developed a certified concrete implementation following the implementation proposed in [5] -a reference in term of complexity. 6 The specification for Grover [31] is shown in Figure 12 (c). Given a predicate with k true value in 0, 2 n , Grover's algorithm outputs one of these true values with good probability.

Each of these specifications makes use of specific functions that we do not have the space to detail here (see [13] for details). We however want to note two things. First, these specifications describe results of measurement (with the dedicated functions proba_partial_measure_x). As discussed in Section 6.5, if Qbricks-DSL is not able to handle measurement we are still able with Qbricks-Spec to reason on the result of a measurement, as this is a simple function over complex amplitudes. Another thing to note is that, for Shor-OF and Grover, our specification discuss the polynomial size of the produced circuit.

Γ, (f : pps), (C : circ), (|v : ket), (k, n : int), (ghost θ : real), (j : ghost int)

(a) Specification for our implementation of Quantum Phase estimation

(c) Specification for our implementation of Grover's algorithm Table 13 7 : lines of decorated code, number of lemmas, proof obligations (PO), automatically proven PO (within time limit 5 seconds) and their percentage among POs, interactive commands we entered to discharge them and time required for the automatic verification of these proofs.

Note that metrics for each implementation strictly concern the code that is proper to it (eg., QPE contains calls to QFT but QPE line in Table 13 does not include the QFT implementation. The whole Shor-OF development is reported in the "Shor-OF full".

Result. Qbricks did allow us to implement and verify in a parametric manner the Shor-OF, QPE and Grover algorithms, at a rather smooth cost and with high proof automation (95% on average, 95% for full Shor-OF).

8.3 Prior verification efforts. Before comparing our approach to prior attempts (Table 14) , we first introduce these cases. DJ  57  11  2  1  72  61  >84%  39 1m19s  Grover  193  39  6  8  505  479 >94% 125 4m43s  QFT  65  18  3  0  62  53  >85%  37 1m11s  QPE  175  24  3  8  282  262 >92%  94 QHL. Liu et al. [45] report about the parametric verification of Grover search algorithm, on a restricted case 8 and in the high-level algorithm description formalism of QHL -especially QHL has no notion of circuit. So for instance one cannot reason upon the size of a circuit within QHL.

SQIR. Finally, Hietala et al. [35] have presented a parametric (circuit-building) implementation of the Deutsch-Jozsa algorithm in Coq, with two independent full correctness proofs. Recently (Oct. 2020), the authors also presented parametrized versions of QFT, QPE and Grover algorithms [34] .

Qbricks. So as to evaluate the proof effort gain of using pps instead of matrices, Table 14 shows some comparison between our case studies implementations and equivalent proved implementations from the literature: the Grover algorithm implementation from [45] in Isabelle/HOL and the implementations [35, 34] using SQIR and Coq. As supplementary comparison terms, we implemented Qbricks versions of both QFT and Deutsch-Jozsa using exclusively matrices. For example the Qbricks implementation of QFT with pps is 18 lines long, with 47 lines of specifications and intermediary lemmas, and its proof required 37 additional interactive commands, hence Spec + Cmd = 84. In comparison, the corresponding SQIR development uses 287 interactive commands (7.7x more).

Conclusion. Relying on PPS semantics and first-order logic instead of matrices and higher-order logics strongly eases the proof effort. In term of command 

Formal verification of quantum circuits. Prior efforts regarding quantum circuit verification [27, 45, 70, 53, 56, 1, 2, 35, 34] have been described throughout the paper, especially in Sections 1, 3.1 and 8. Our technique is more automated than those based on interactive proving [35, 34, 45] , borrows and extends the path sum representation [2] to the parametric case, and do consider a circuit-building language rather than a high-level algorithm description language [45] .

Quantum Languages and Deductive Verification. Liu et al. [45] introduce Quantum Hoare Logic for high-level description of quantum algorithms. QHL and our own HQHL are different, as the underlying formalisms have different focus. While QHL deals with measurement and classical control, it does not allow reasoning on the structure of the circuit. On the other hand, Qbricks does not handle classical control, but it brings better proof automation and deduction rules for reasoning on circuits. Combining the two approaches is an exciting research direction.

Verified Circuit Optimizations. Formal methods and other program analysis techniques are also used in quantum compilation for verifying circuit optimization techniques [52, 6, 32, 3, 62, 57, 35] . Epecially, the ZX-calculus [17] represents quantum circuits by diagrams amenable to automatic simplification through dedicated rewriting rules. This framework leads to a graphical proof assistant [40] geared at certifying the semantic equivalence between circuit diagrams, with application to circuit equivalence checking and certified circuit compilation and optimization [21, 20, 39 ]. Yet, formal tools based on ZX-calculus are restricted to fixed circuits, and parametrized approaches are so far limited to pen-and-paper proofs [12] .

Other quantum applications of formal methods. Huang et al. [36, 37] proposes a "runtime-monitoring like" verification method for quantum circuits, with an annotation language restricted to structural properties of interest (e.g., superposition or entanglement). Similarly, [44] describes a projection based assertion language for quantum programs. Verification of these assertions is led by statistical testing instead of formal proofs. The recent Silq language [8] also represents an advance in the way toward automation in quantum programming. It automatizes uncomputation operations, enabling the programmer to abstract from low level implementation details. Also specialized type systems for quantum programming languages, based on linear logic [60, 59, 43] and dependent types [51, 53] , have been developed to tackle the non-duplicability of qubits and structural circuit constraints. Finally, formal methods are also at stake for the verification of quantum cryptography protocols [49, 29, 11, 47, 19 ].

We address the problem of automating correctness proofs of quantum programs. While relying on the general framework of deductive verification, we finely tune our domain-specific circuit-building language Qbricks-DSL together with its new logical specification language Qbricks-Spec in order to keep correctness reasoning over relevant quantum programs within first-order theory. Also, we introduce and intensively build upon parametrized path sums (PPS), a symbolic representation for quantum circuits represented as functions transforming quantum data registers. We develop verified parametric implementations of the Shor-OF algorithm (first verified implementation) and other famous non-trivial quantum algorithms (including QPE and Grover search), showing significant improvement over prior attempts -when available.

Formal Methods in Quantum Circuit Design

Towards large-scale functional verification of universal quantum circuits

Verified compilation of space-efficient reversible circuits

Quantum supremacy using a programmable superconducting processor

Circuit for shor's algorithm using 2n+ 3 qubits

Reversible pebble games for reducing qubits in hierarchical quantum circuit synthesis

Quantum machine learning

Silq: a high-level quantum language with safe uncomputation and intuitive semantics

Why3: Shepherd Your Herd of Provers

Formalization of quantum protocols using coq

How to verify a quantum computation

SZX-calculus: Scalable graphical quantum reasoning

Toward certified quantum programming

Experimental implementation of fast quantum searching

Formal methods: State of the art and future directions

Quantum algorithms revisited

Picturing quantum processes

An approximate fourier transform useful in quantum factoring

Formal verification techniques using quantum process calculus

Pauli fusion: a computational model to realise quantum transformations from ZX terms

Optimising Clifford circuits with Quantomatic

A quantum approximate optimization algorithm

A quantum adiabatic evolution algorithm applied to random instances of an npcomplete problem

The Why/Krakatoa/Caduceus platform for deductive program verification

Why3 -where programs meet provers

The spirit of ghost code

QMC: a model checker for quantum systems

Quantum simulation

Verification of quantum computation: An overview of existing approaches. Theory of Computing Systems

Quipper: A scalable quantum programming language

A fast quantum mechanical algorithm for database search

SAT-based exact synthesis: Encodings, topology families, and parallelism

Quantum algorithm for linear systems of equations

Proving quantum programs correct

A verified optimizer for quantum circuits

QDB: from quantum algorithms towards correct quantum programs

Statistical assertions for validating patterns and finding bugs in quantum programs

Proceedings of the 46th International Symposium on Computer Architecture (ISCA 2019)

On quantum supremacy

Reducing t-count with the ZX-calculus

Quantomatic: A proof assistant for diagrammatic reasoning

Quantum measurements and the abelian stabilizer problem

Conventions for quantum pseudocode

Quantum implicit computational complexity

Projection-based runtime assertions for testing and debugging quantum programs

Formal verification of quantum algorithms using quantum hoare logic

A theorem prover for quantum hoare logic and its applications

Classical verification of quantum computations

Enabling accuracy-aware quantum compilers using symbolic resource estimation

Formal verification of quantum protocols

Quantum computation and quantum information

qPCF: Higher-order languages and quantum circuits

REVS: a tool for space-optimized reversible circuit synthesis

QWIRE: a core language for quantum circuits

Qbricks repository

Quantum Computing Report. List of tools. Available online 11

Formally Verified Quantum Programming

ReQWIRE: Reasoning about reversible quantum circuits

QWIRE practice: Formal verification of quantum circuits in coq

Algebraic and Logical Methods in Quantum Computation

A lambda calculus for quantum computation with classical control

Algorithms for quantum computation: Discrete log and factoring

Programming quantum computers using design automation

ProjectQ: an open source software framework for quantum computing. Quantum, 2:49

Q#: Enabling scalable quantum computing and development with a high-level domain-specific language

The quantum future of computation

Programming the quantum future

LIQUi| : A software design architecture and domainspecific language for quantum computing

Floyd-hoare logic for quantum programs

Toward automatic verification of quantum programs

Model-checking linear-time properties of quantum systems

Invariants of quantum programs: characterisations and generation

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