AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

Quantum programs are an extension of quantum circuits that provide users with greater control over quantum computing by allowing them to use more complex programming constructs like branches and loops. Some of the most advanced quantum algorithms cannot be defined by quantum circuits alone. For example, certain class of programs, such as the repeat-until-success (RUS) algorithms [41] (which are commonly used in generating special quantum gates) and the weak-measurement-based version [6] of Grover’s search algorithm [31], use a loop with the condition being a classical value (0 or 1) obtained by measuring a particular qubit. This added expressivity presents new challenges, particularly in terms of verification. The additional complexity comes from the measurement operation, where a particular qubit is measured to obtain a classical value (and the quantum state is partially collapsed, which might require normalization), and reasoning about control flow induced by branches and loops.

In classical program verification, a prominent role is played by deductive verification [30, 32, 34], represented, e.g., by the tools Dafny [37], KeY [4], Frama-C [8], VeriFast [36], VCC [23], and many more. These tools only require the users to provide specifications in the form of pre- and post-conditions, along with appropriate loop invariants. The rest of the proving process is entirely (in the ideal case) automated. Unfortunately, in the realm of quantum computing, similar fully automated deductive verification tools are, to the best of our knowledge, missing. Advanced tools for analysis and verification of quantum programs—based on, e.g., quantum Hoare logic and the tool CoqQ  [50] or the path-sum formalism [5] and the tool Qbricks  [14]—are quite powerful but require a significant amount of human effort.

To bridge this gap, we present AutoQ 2.0, a major update over AutoQ 1.0  [19] with an added support for quantum programs (AutoQ 1.0 only supported quantum circuits). In AutoQ 1.0, given a triple \(\{P\}\,C\,\{Q\}\), where P and Q are the pre- and post-conditions recognizing sets of (pure) quantum states (represented by tree automata) and C is a quantum circuit, we can verify if all quantum states in P reach some state in Q after executing C. In AutoQ 2.0, we addressed several key challenges to make the support of quantum programs possible. First, we need to handle branch statements. The key issue here is to handle measurement of quantum states whose value is used in a branch condition. For this we developed automata-based algorithms to compute the quantum states after the measurement (Section 5). The second challenge is the handling of loop statements. Similarly to deductive verification of classical programs, we require the users to provide an invariant for each loop. With the loop invariant provided, we developed a framework handling the rest of the verification process fully automatically. Moreover, we show that a naive implementation of the measurement operation will encounter the probability amplitude normalization problem. This is handled by designing a new algorithm for entailment testing (Section 6).

Under this framework, the preconditions, postconditions, and invariants are all described with a new automata model called level-synchronized tree automata (LSTAs) [1]. LSTAs are specifically designed to efficiently encode quantum states and gate operations. As the core data structure of the tool, we provide a formal definition of LSTAs in Section 2.2 to facilitate the presentation of our new entailment testing approach.

We used AutoQ 2.0 to verify various quantum programs using the repeat-until-success (RUS) paradigm [41], as well as the weak-measurement-based version [6] of Grover’s search [31] (Section 7). AutoQ 2.0 can efficiently verify all our benchmarks. The verification process for all RUS algorithms was instantaneous and for the weakly measured versions of Grover, we were able to handle the case of 100 qubits in \(\sim \)20 min. To the best of our knowledge, AutoQ 2.0 is currently the only tool for verification of quantum programs with such a degree of automation.

Related work. Our work aligns with Hoare-style verification of quantum programs, a topic extensively explored in prior studies [27, 39, 43, 48, 51]. This approach, inspired by D’Hondt and Panangaden, utilizes diverse Hermitian operators as quantum predicates, resulting in a robust and comprehensive proof system [25]. However, specifying properties with Hermitian operators is often non-intuitive and difficult for automation due to their vast matrix sizes. Consequently, these methods are typically implemented using proof assistants like Coq  [9], Isabelle  [45], or standalone tools built on top of Coq, like CoqQ  [50]. These tools require substantial manual effort in the proof search. The Qbricks approach [15] addresses the challenge of proof search by combining cutting-edge theorem provers with decision procedures, leveraging the Why3 platform [29]. Nevertheless, this approach still demands considerable human intervention.

In the realm of automatic quantum software analysis tools, circuit equivalence checkers [5, 22, 23, 33, 47] prove to be efficient but less flexible in specifying desired properties, primarily focusing on equivalence. These tools are valuable in compiler validation, with notable examples being QCEC [13], Feynman  [5], and SliQEC  [17, 44]. Quantum model checking, supporting a rich specification language (various temporal logics [28, 40, 46]), is, due to its limited scalability, more suited for verifying high-level protocols [7]. QPMC  [28] stands out as a notable tool in this category. Quantum abstract interpretation [42, 49] over-approximates the reachable state space to achieve better scalability, but so far handles only circuits. The work in [26, 52] aims at the verification of parameterized quantum programs like variational quantum eigensolver (VQE) or quantum approximate optimization algorithm (QAOA). However, the correctness properties they focused are very different from what AutoQ 2.0 can handle. While the mentioned tools are fully automated, they serve different purposes or address different phases of the development cycle compared to AutoQ 2.0.

Before we start, we first provide a minimal background needed for this work.

In this section, we provide an overview of automata-based quantum program verification with a running example (chosen for its simplicity). In the example, the quantum program creates the effect of a non-standard quantum gate “\(-X\)” (applying the X gate and negating all amplitude values) using the standard gates X, H, and CX (Algorithm 1). The program operates on a 2-qubit system and performs the “\(-X\)” gate on the second qubit when the first qubit is measured to be 1; otherwise, (the first qubit is 0 after measurement) the state stays unchanged.

For all \(a_0,\ a_1\in \mathbb C\), we verify Algorithm 1 against the precondition \(\{a_0\mathinner {|{10}\rangle }+ a_1\mathinner {|{11}\rangle }\}\), which allows the state with the first qubit \(\mathinner {|{1}\rangle }\) and the second qubit \(a_0\mathinner {|{0}\rangle }+a_1\mathinner {|{1}\rangle }\), and the postcondition \(\{a_0\mathinner {|{10}\rangle }+ a_1\mathinner {|{11}\rangle },\ {-}a_1\mathinner {|{10}\rangle }- a_0\mathinner {|{11}\rangle }\}\), which includes the original state and the state after the “\(-X_2\)” gate.

Our approach first constructs two LSTAs P and Q that can recognize the states (binary trees) of the pre- and post-conditions, respectively, and then computes another LSTA by executing the gates \(H_1;CX^1_2\) from P (see Fig. 2(a) for the only quantum state accepted by P) with the gate algorithm introduced in [1]. This results in an LSTA \(P_1\) that recognizes the state shown in Fig. 2(b). After applying the operator \(M_1\) to measure \(x_1\) (Line 3), \(P_1\) splits into two copies. One copy, \(P_2\), accepts the only quantum state shown in Fig. 2(c), where the first qubit is measured to be 0. The other copy, \(P_3\), accepts the only quantum state shown in Fig. 2(d), where the first qubit is measured to be 1.

It is important to note that the probability amplitudes of the quantum states from Figs. 2(c) and 2(d) have not been normalized yet. To do that, we need to multiply all leaves with the normalization factor \(\sqrt{2}\). This will ensure that the square sum of their absolute amplitude values becomes 1. Although the quantum states are not yet normalized, we, however, still have sufficient information to obtain the corresponding normalized states. In AutoQ 2.0, we choose to ignore all normalization factors and design a new entailment testing algorithm (Section 6) that can detect the equivalence of two non-normalized states. After both the true and false paths of the if statement in the example are processed, we obtain two LSTAs \(P_2\) and \(P_3\) capturing all reachable states. We then construct their union and test if all states in the union are included in the post-condition (recognized by Q) by testing entailment.

A drawback of Algorithm 1 is that the desired effect “\(-X\)” manifests only if \(M_1 = 1\). In the case \(M_1 = 0\), we need to run the same algorithm again until we get a measurement of 1. To achieve this, we can use a while loop statement, as shown in Algorithm 2. The loop allows us to repeatedly execute the same branch statement until the desired outcome is achieved.

To verify that the loop works correctly, we require the user to provide a loop invariant in the form of an LSTA. The invariant here is \(\{\frac{a_0}{\sqrt{2}}\mathinner {|{00}\rangle }+ \frac{a_1}{\sqrt{2}}\mathinner {|{01}\rangle }- \frac{a_1}{\sqrt{2}}\mathinner {|{10}\rangle }- \frac{a_0}{\sqrt{2}}\mathinner {|{11}\rangle }\}\) (cf. Fig. 2(b)). The verification process then involves checking if the invariant is inductive, covers all reachable states before entering the loop, and does not contain any state that would violate the post-condition. More details on the verification process will be given in Section 5.3. With the loop invariant provided, we can ensure that the algorithm ends up with a state where the “\(-X\)” gate is applied to the second qubit when it terminates.

In AutoQ 2.0, preconditions, postconditions, and invariants are represented as sets of quantum states, encoded using the LSTA model. Therefore, it is important for users to understand how to encode a set of quantum states with an LSTA. Below, we provide two examples to give a basic understanding of the process. In the first example, we show how to encode the postcondition of Algorithm 1, \(\{a_0\mathinner {|{10}\rangle }+ a_1\mathinner {|{11}\rangle },\ \mathrm {-}a_1\mathinner {|{10}\rangle }- a_0\mathinner {|{11}\rangle }\}\).

The corresponding LSTA is shown in Fig. 3. The LSTA constructs trees that depict quantum states beginning from the initial state p at the root. It continues to build the tree by choosing transitions to explore new child states at each step, and this process continues until it reaches the leaves. For instance, the tree in Fig. 2(c) can be generated by first picking the transition , then the two transitions and , and ending with the three leaf transitions , , and . Similar to the conventional tree automata (TAs) model, LSTAs utilize disjunctive branches to represent various states that share a common structure. In Fig. 3, the state p has two possible outgoing transitions. If one picks the other transition at the beginning, we can generate the tree shown in Fig. 2(d).

The previous example does not fully demonstrate why incorporating a set of choices (the numbers in the curly brackets) into the design of LSTAs is beneficial. Let us consider another well-known example: the set of Bell states \(\{\mathinner {|{00}\rangle }\pm \mathinner {|{11}\rangle }, \mathinner {|{01}\rangle }\pm \mathinner {|{10}\rangle }\}\), generated by the LSTA in Fig. 4(a). Without the restriction that all transitions at the same level must share a common choice, this LSTA would generate eight different trees (since \(q_+\), \(q_\pm \), and \(r_\pm \) each have two outgoing transitions), which correspond to the quantum states \(\{\mathinner {|{00}\rangle }\pm \mathinner {|{11}\rangle }, \mathinner {|{01}\rangle }\pm \mathinner {|{10}\rangle }, \mathinner {|{00}\rangle }\pm \mathinner {|{10}\rangle }, \mathinner {|{01}\rangle }\pm \mathinner {|{11}\rangle }\}\). However, only four of these trees correspond to the Bell states, meaning the others are unintended. The LSTA uses the labeled choices to rule out the unintended trees. More specifically, at level 2, the two transitions labeled \(\{1\}\) can be used simultaneously, as they share the common choice 1. Similarly, the two transitions labeled \(\{2\}\) can be used together due to their common choice 2. In contrast, a transition labeled \(\{1\}\) cannot be used alongside one labeled 2, as their choice sets are disjoint. At level 3, the transitions from \(r_\pm \) can be used freely with those from \(r_+\) and \(r_0\), since \(\{1\}\text { (and }\{2\}\text {) } \cap \{1,2\} \ne \emptyset \). There are two valid combinations of transitions at levels 2 and 3, and this LSTA generates exactly the four Bell states using the nine transitions shown in the figure. The corresponding .lsta file, which illustrates the input format for AutoQ 2.0, is shown in Fig. 4(b). In .lsta files, transitions are labeled with pairs [a, b], where a indicates the symbol \(x_a\) and b is the set of choices.

We present the architecture of AutoQ 2.0 in Fig. 5. The tool is written in C++ and uses the SMT solver Z3  [24] for satisfiability and entailment checking of constraints. We allow the use of any theory that is supported by Z3. In our experiments, we used NIRA (non-linear integer and real arithmetic). While this logic is generally undecidable, Z3  always quickly solved the formulae we presented to it in our experiments.

Similar to verifiers for classical programs, in order to use AutoQ 2.0, the user needs to provide the following: (i) a quantum program in the OpenQASM 3.0 format, (ii) pre- and post-conditions in the .lsta format along with SMT formulae in the .smt format to constrain the terms, and (iii) invariant for each loop in the .lsta format together with an SMT formula. The specification (pre- and post-conditions) and the invariant (for each loop) can be written as an LSTA (an .lsta file). Once these files are provided, AutoQ 2.0 will process them and report either “Verified” or “Failed”.

Compared to AutoQ 1.0, there are several major changes in AutoQ 2.0. Firstly, it features a new input interface to facilitate the use of quantum programs (instead of only circuits) and uses LSTA as the back-end model (instead of standard tree automata). Additionally, Program Executor now supports measurement and branch statements. Another significant addition is the new Invariant Checker component, which handles loop invariants. The Invariant Checker also uses the Entailment Checker to verify the inductiveness of the invariant, which we do not explicitly show in the figure.

We will start by presenting the syntax of quantum programs that AutoQ 2.0 can handle and then informally describe their semantics. We use a flavor of quantum programs that is similar to the one in [48], which is captured by the following grammar:where P is a quantum program, U is a quantum gate annotated with its control and target qubits (e.g., \(CX_1^2\)), \(b\in \{0,1\}\), and \(M_i\) is the measured value of the i-th qubit. AutoQ 2.0 supports standard non-parameterized quantum gates that allow (approximate) universal computation [3, 12], including Clifford gates (H, S, and \(\textit{CX}\)), T, Z, \( SWAP \), Toffoli, etc.

The execution of quantum gate U updates a quantum state (tree) in the standard way [20]. The language allows sequential composition (P; P) of gate operations, branches (if...else...), and loops (while...). When using if and while statements, the condition \(M_i = b\) (denoting that the value obtained from measuring \(x_i\) was b) is used to determine in which path to continue.

In our approach, we use a special entailment test at some points, which we call entailment up to scaling, denoted as \(\mathcal {A}\mathrel {\models ^{ uts }}\mathcal {B}\). The reason for a special entailment relation is that—as mentioned before—at measurements, we do not perform normalization. Intuitively, given two LSTAs \(\mathcal {A}=\langle Q_\mathcal {A},\Sigma ,\Delta _\mathcal {A},\mathcal {R}_\mathcal {A},\varphi _\mathcal {A} \rangle \) and \(\mathcal {B}=\langle Q_\mathcal {B},\Sigma ,\Delta _\mathcal {B},\mathcal {R}_\mathcal {B},\varphi _\mathcal {B} \rangle \), the relation \(\mathcal {A}\mathrel {\models ^{ uts }}\mathcal {B}\) holds if and only if for every tree \(T_\mathcal {A}\) in the language of \(\mathcal {A}\) and assignment to the variables occurring in \(T_\mathcal {A}\), we can find a linearly scaled copy of \(T_\mathcal {A}\) in the semantics of \(\mathcal {B}\) (such that the values of variables occurring in both \(T_\mathcal {A}\) and \(T_\mathcal {B}\) match). Formally,where \(r \cdot T\) denotes the tree with the same structure as T with all numbers in leaves multiplied by r and \( vars (\gamma )\) for any mathematical object \(\gamma \) (a term, a tree with terms in leaves, a set of terms, etc.) denotes the set of free variables occurring in the object. The \(\mathrel {\models ^{ uts }}\) relation is central to our approach.

Enumerating all trees of \(\mathcal {A}\) and looking for their scaled copies in \(\mathcal {B}\) would be too inefficient and even impossible in the case of LSTA s recognizing infinitely many finite trees (such as those modelling invariants of parameterized quantum programs [1]). Therefore, we modified the algorithm for LSTA language inclusion test presented in [1]. We note that language inclusion testing for LSTAs is more involved than for standard TAs (cf. [2, 11, 35, 38]). In the modification, we allow to relate the leaf values with a linear factor for scaling (in contrast to only by identity as done in the original inclusion testing algorithm), so that it tests the entailment \(\mathcal {A}\mathrel {\models ^{ uts }}\mathcal {B}\).

The algorithm makes use of the following essential property of trees generated by an LSTA  \(\mathcal {A}\): if two nodes at the same level of a tree T are labelled by the same state in an accepting run of \(\mathcal {A}\) on T, then the subtrees rooted in these nodes are identical (this follows from the semantics of LSTA s and the restriction on transitions, cf. Section 2.2).

Intuitively, the algorithm works as follows. It starts in the root states of \(\mathcal {A}\) and \(\mathcal {B}\) and performs a downward traversal through the LSTA s, level by level, remembering, at each level, how states from \(\mathcal {A}\) can map to the states in \(\mathcal {B}\). Moreover, the algorithm also remembers how the terms in the leaves of the tree from \(\mathcal {A}\) map to the terms in the leaves of the tree from \(\mathcal {B}\). The downward successors of each level are computed from transitions leaving states at the level that need to be synchronized on their choice. The algorithm explores the space of all of the reachable mappings until it reaches a point such that the tree from \(\mathcal {A}\) has all branches terminated. At this moment, we check whether the terms from the leaf transitions of \(\mathcal {A}\) can be mapped (up to scaling) to the corresponding terms from the leaf transitions in \(\mathcal {B}\). If not, conclude that the entailment does not hold.

Formally, the algorithm performs a search in the directed graph (V, E) (constructed on the fly), where each vertex \(v\in V\) is of the form \(v=(D,\ \{(f_1,\ g_1),\ \ldots ,\ (f_m,\ g_m)\})\) for some m where \(D\subseteq Q_\mathcal {A}\) is called the domain, each \(f_i:D \rightarrow 2^{Q_\mathcal {B}}\) is a map that assigns every state of \(\mathcal {A}\) from the domain D a set of states of \(\mathcal {B}\), and each \(g_i:\textsf {term}(\mathbb {C}, \mathbb {X})\rightarrow 2^{\textsf {term}(\mathbb {C}, \mathbb {X})}\) is a (partial) mapping from terms to sets of terms. Intuitively, D represents the set of states of \(\mathcal {A}\) at one level of \(\mathcal {A}\)’s run \(\rho \), and every \(f_i\) represents the same level of some possible run \(\rho _i\) of \(\mathcal {B}\) on the same tree and the way it can match the run \(\rho \) of \(\mathcal {A}\). For instance, in Section 6, the state q of \(\mathcal {A}\) corresponds to the states r, s of \(\mathcal {B}\) because they are used in the same tree level and the same tree nodes, so we have \(f_i(q) = \{r,s\}\). Due to the property that all occurrences of a state at the same level in a run generate the same subtree mentioned above, we only need to maintain encountered states and their alignment with each another. The term mappings \(g_i\) are used to remember how the terms from the leaves of \(\mathcal {A}\) are mapped to terms in the leaves of \(\mathcal {B}\). For instance, if some term t from a leaf of \(\mathcal {A}\) is mapped by two different terms \(t_1\) and \(t_2\) of \(\mathcal {B}\), we will later need to check whether there is a scaling factor r such that \(t = r\cdot t_1\) and, at the same time, \(t = r \cdot t_2\) (and the global constraints of \(\mathcal {A}\) and \(\mathcal {B}\) are satisfied). We give a general algorithm here; for LSTAs that accept only perfect trees (as is the case for the ones encoding quantum states), all branches of the accepted trees terminate at the same time so there is no need to remember the term mappings g across different levels and the scaling compatibility could be checked only locally.

The graph search begins from the source vertices, one for each state \(q \in \mathcal {R}_\mathcal {A}\), of the form \((\{q\},\{(\{q\mapsto \{r_1\}\}, \emptyset ),\ldots ,(\{q\mapsto \{r_k\}\}, \emptyset )\})\), where \(\{r_1,\ldots , r_k \} = \mathcal {R}_\mathcal {B}\), corresponding to the root states of both \(\mathcal {A}\) and \(\mathcal {B}\) (the \(\emptyset \)’s denote empty term mappings). If the search finds a terminal vertex \((\emptyset , F)\), where \((\emptyset , g) \notin F\), meaning that an accepting run of \(\mathcal {A}\) has been found, but there is no corresponding matching run of \(\mathcal {B}\) (for any g), we can conclude that the entailment test failed (it represents the case when \(\mathcal {A}\) finished reading all branches of the tree but \(\mathcal {B}\) did not). On the other hand, if there is \((\emptyset , g) \in F\), we still need to check that the set of terms g is compatible. The graph’s edges represent generating the next level of runs for both \(\mathcal {A}\) and \(\mathcal {B}\) and how the respective states align with each other. The specific construction of the edges from a vertex \(v = (D, \{(f_1, g_1), \ldots , (f_m,g_m)\})\), where \(D \ne \emptyset \), to each lower-level vertex \(v' = (D', \{(f'_1, g'_1), \ldots , (f'_n, g'n)\})\) follows.

First, we compute possible successors of the D-component of v. To do this, we need to explore all feasible sets \(\Gamma _\mathcal {A}\) of transitions from D in \(\mathcal {A}\). More concretely, in each set \(\Gamma _\mathcal {A}\), we select exactly one downward transition \(\delta _{q_\mathcal {A}}\) originating from each \(q_\mathcal {A}\in D\), such that all transitions in \(\Gamma _\mathcal {A}\) share a common choice (as required by the definition of an accepting run (cf. Section 2.2). Formally, given \(D = \{q_1, \ldots , q_k\}\), we consider all sets of transitions \(\Gamma _\mathcal {A}= \{\delta _1, \ldots , \delta _k\}\) such that the following formula holds:We will denote the set of all such \(\Gamma _\mathcal {A}\)’s from a set of states D as \(\texttt{FTrans}(\mathcal {A}, D)\).

Next, we will show how to construct the set of all feasible pairs of mappings \(\{(f'_1, g'_1),\ldots (f'_n, g'_n)\}\) for some \(\Gamma _\mathcal {A}\) and a pair of upper level mappings (f, g). Each pair of mappings \((f'_j, g'_j)\) at the lower level is derived from some pair of mappings \((f_i,g_i)\) at the upper level and a set of downward transitions \(\Gamma _\mathcal {B}\) from \(\mathcal {B}\). The construction process is described in Algorithm 4, where we use (f, g) to denote an upper level state and term mapping respectively and \((f',g')\) to denote their lower level counterparts.

The basic idea of the algorithm is simple: (i) we use the upper level mapping f and transitions \(\Gamma _\mathcal {A}\) to compute the set of top states Q (Line 1), (ii) then, we find all feasible transitions \(\Gamma _\mathcal {B}\) from Q (Line 2), and, finally, (iii) for each pair \((\Gamma _\mathcal {A}, \Gamma _\mathcal {B})\), we construct one pair of lower level state and term mappings \((f',g')\) (Lines 4–9). Specifically, in step (iii), it must hold that for each transition \(\delta _\mathcal {A}\in \Gamma _\mathcal {A}\), every state \(q \in f(\texttt{top}(\delta _\mathcal {A}))\) needs to be able to match \(\delta _\mathcal {A}\) by a transition from \(\Gamma _\mathcal {B}\). To check this, for every such q we select from \(\Gamma _\mathcal {B}\) the transition \(\delta _\mathcal {B}\), which is the transition of \(\Gamma _\mathcal {B}\) with q as its top (it follows from \(\texttt{FTrans}\) that there is exactly one). There are three possible cases:

Finally, the main entailment testing routine is summarized in Algorithm 5. Line 2 creates the set of source vertices of the explored graph. Lines 3–4 pick a vertex (D, F) that has not been processed yet. Lines 6–10 check whether (D, F) is a terminal vertex and conclude that the entailment test fails when such a vertex is reached. This check consists of looking at all pairs \((\emptyset , g)\) in F and checking whether there is a way how the \(\mathcal {B}\)-terms from the g’s can together cover (modulo a scaling factor) the behaviour of the \(\mathcal {A}\)-terms. Lines 11–16 are the edge construction procedure. Lines 11–12 enumerate all feasible \(\Gamma _\mathcal {A}\) and use them to create the next vertex \((D',F')\). Specifically, \(D'\) are the bottom states from \(\Gamma _\mathcal {A}\) (Line 12), and \(F'\) are the union of all feasible mappings of \(\Gamma _\mathcal {A}\) (Lines 13–16). The successor term mapping is computed from the upper-level one and from the one returned by by, for each term of \(\mathcal {A}\), merging corresponding sets of terms of mappings: \(g \mathop {\Cup }g' = \{x \mapsto Y \mid x \in \textrm{dom}(g \cup g'), Y = g(x) \cup g'(x)\}\) (Line 15).

A crucial part of the algorithm is the term mapping g check between the terms from \(\mathcal {A}\) and the terms from \(\mathcal {B}\) (Lines 7–10). Here, we want to check that for every possible value that we can obtain from a term t on the left-hand side of the entailment (satisfying \(\mathcal {A}\)’s global constraint \(\varphi _\mathcal {A}\)) and every term \(t_i\) from \(g(t) = \{t_1, \ldots , t_k\}\), there is a way to obtain a value (satisfying \(\mathcal {B}\)’s global constraint \(\varphi _\mathcal {B}\)) such that for all these values, there is a common scaling factor r to make them equal to the value from t. We emphasize the way how we need to deal with the quantified variables. Variables \(\mathbb {Y}\) occurring on the left-hand side (and possibly also on the right-hand side, since we may need to synchronize the values) are quantified universally, while variable \(\mathbb {Z}\) occuring only on the right-hand side of the entailment are quantified existentially. This scaling check requires invoking an SMT solver with a formula in the NIRA (non-linear integer and real arithmetic) logic. In the special case where all leaf symbols are constants, r is the only variable, and global constraints are \(\textbf{true}\), the problem reduces to a simple QF_LRA (quantifier-free linear real arithmetic) formula.

We demonstrate the use of AutoQ 2.0  [21] on two real-world use cases consisting of quantum programs with loops that were proposed in [6, 41]. We ran all experiments on a server running Ubuntu 22.04.3 LTS with an AMD EPYC 7742 64-core processor (1.5 GHz), 1,152 GiB of RAM, and a 1 TB SSD.

We presented a major extension of AutoQ 1.0  [19] with an added support for control flow constructs and evaluated its feasibility on a family of programs for the weak-measurement-based version of Grover’s algorithm and on implementations of a number of non-standard quantum gates using repeat-until-success circuits. In the future, we wish to extend the framework with automating invariant generation (e.g., using a modification of the symbolic-execution-based technique from [16]) and add support for dealing with more complex loops that give rise to mixed states.