{'fraction_non_alphanumeric': 0.04464532079511716, 'fraction_numerical': 0.010452192532256106, 'mean_word_length': 4.351683402244537, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification

Many quantum programs are assured by formal verification, but such verification is usually laborious and time-consuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantum-classical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a type-guided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently perform for many hybrid quantum-classical algorithms, including GHZ, Shor's, Grover's, and quantum walk algorithms, which saves a great amount of human efforts. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.


INTRODUCTION
Quantum computers offer unique capabilities that can be used to program substantially faster algorithms compared to those written for classical computers. For example, Shor's algorithm [42] can factor a number in polynomial time (compared to the sub-exponential time for the best known classical algorithm). Most quantum algorithms are not classically simulatable; therefore, they are verified through rigorous formal methods. Many frameworks have been proposed to verify quantum algorithms [4,15,20,25,48,51], which established quantum semantic interpretations and libraries in some interactive theorem provers, such as Isabelle and Coq. Some attempts towards proof automation have been made by providing some contrived tactics or using solver-based techniques, yet building and verifying quantum algorithms in these frameworks are still time-consuming and require great human efforts. Meanwhile, automated verification is an active research field in classical computation with many proposed frameworks [7,16,17,21,26,29,32,34,[38][39][40]44]. All of these works show strong results in relieving programmers' pain when verifying classical programs. Is there a way to utilize classical automated verification frameworks in verifying quantum programs?
In this paper, we propose Quantum Natural Proof (QNP), a framework that empowers programmers to develop and verify hybrid quantum-classical programs based on the marriage of quantum program semantics and classical automated verification infrastructure. It has several elements, as shown in Figure 1. The core of QNP is a strongly typed, flow-sensitive imperative quantum programming language L Qafny and a classical separation logic style proof system Qafny for L Qafny . In QNP, users specify hybrid quantum-classical programs and input the properties to be verified as pre-and post-conditions and loop invariants. The quantum components of the programs and properties are defined on Qafny and verified by compiling to Dafny [22], a classical separation logic framework, while the classical components are based on the Dafny infrastructure. The quantum program components written in L Qafny can be compiled to quantum circuits and run on a quantum computer via the L Qafny to SQIR and SQIR to OpenQASM 2.0 [8] compilers, along with the classical components being extracted to general-purpose languages by Dafny. The extracted code can then call the compiled quantum components as library functions.

Fig. 2. State Preparation Circuit
In Qafny, quantum states are encoded as arrays and the interpretations of quantum operations are based on the array representations of states. For example, in Figure 2, a quantum state in superposition | ⟩ = 2 =0 1 | ⟩ is prepared by applying a Hadamard gate to each qubit. In Qafny, this can be treated as an 2 -array, denoted by . Each element, which corresponds to each indexed basis element in | ⟩, is a pair of a complex and a natural number. Applying a quantum oracle ( (| ⟩) = (− ) | ⟩) on | ⟩, which essentially evolves each indexed element 1 | ⟩ in | ⟩ to (− ) | ⟩, can be therefore analogized to an array map function that applies ′ ( , ) = ((−1) , ) to each element in . In fact, the design and analysis of many quantum algorithms leveraged the integration of representing different groups of qubits as different state representations, many of which can be viewed as some types of classical arrays [13,31,43]. In Qafny, we identify different types of quantum state representations that are formatted as some classical array data structures (Section 2). Then, the Qafny type system tracks the qubit arrays and their state type transformations, so that specific Qafny proof rules can be defined based on the classification of state types. With such representations, predicates over quantum operations can be trivially translated into predicates over array operations that can be reasoned in Dafny.
Besides the opportunity of automation provided by representing quantum states as arrays, Qafny also utilizes language abstractions such as quantum conditionals and loops, which generalize controlled gates, to enable local reasoning in the presence of quantum entanglement states. In prior works, the common approach in reasoning about quantum controlled gates such as (CNOT) and controlled-gates is to transform these operations into a single inseparable representation such as an unitary matrix, which does not scale up well in an automated verification framework. In Qafny, reasoning about controlled structures amounts to building a structural inductive relation between a quantum conditional and the subpart reasoning about its body, through a deliberately designed proof rule in Sections 3.2 and 4.3. However, this comes with price: Qafny needs to know which qubits are entangled to apply the proof rule correctly. We address this problem by introducing the Qafny type system that is capable of over-approximating the sets of qubits being probably entangled at the type level and providing the proof system with hints for local reasoning.
The L Qafny operation set is universal to define all quantum programs. The proving power of Qafny depends on the classical probability distribution library in Dafny, because we encode the density matrix semantics of quantum measurement as an array filter operation with the Dafny probability library. See Appendix A. 9. As the evidence presented in Figure 15, the Qafny proof system is capable of verifying properties for many quantum algorithms, including GHZ, Shor's, Grover's, quantum walk and other algorithms. We identify several QNP achievements and its correctness statement as follows, which are partly indicated in Figure 1.
• We present a type-guided proof system Qafny based on viewing quantum operations as classical array operations and a language abstraction L Qafny featuring quantum conditionals and loops including its small-step semantics and type system. We also proved in Coq the type soundness for L Qafny and both soundness and relative completeness for Qafny. Thus, the Qafny proof system respects the L Qafny program semantics. To the best of our knowledge, Qafny provides the first proof rule definitions for quantum conditionals and for-loops. See Section 7 for comparison. • We present a tested circuit compiler from L Qafny to SQIR. This is validated by testing program behaviors in an extracted L Qafny interpreter against the ones in the extracted OpenQASM code from SQIR. Since Qafny respects the L Qafny semantics and L Qafny is correctly compiled to quantum circuits, It means that Qafny correctly reflects quantum program semantics. • We proved in Coq the Qafny to separation logic proof system compilation correctness, as a verification for the Qafny to Dafny compiler, by viewing Dafny as a separation logic framework and formalize it in Coq. To the best of our knowledge, this is the first work that connects a quantum proof system and classical separation logic proof system. • We implemented a Qafny to Dafny compiler and verified many quantum algorithms (Figure 15) at a high degree of automation. Section 6 shows how QNP can save human efforts in verifying quantum programs. • We also show in Section 6 two case studies to demonstrate that QNP can help programmers to construct verification for new quantum algorithms based on the reuse of verified quantum algorithm theorems, and to ascertain the intuitive behaviors of quantum programs that are previously described as physical procedures, such as Hamiltonian simulation evolving.

BACKGROUND
Here, we provide background information for quantum computing, and the details of Dafny and classical separation logic methodologies are in Section 7. Quantum Value States and Alternative Value Representations. A quantum value state consists of one or more quantum bits (qubits). A qubit can be expressed as a two-dimensional vector where , , called amplitudes, are complex numbers such that | | 2 + | | 2 = 1. We frequently write the qubit vector as |0⟩ + |1⟩ where |0⟩ = 1 0 and |1⟩ = 0 1 are computational basis kets. When both and are non-zero, we can think of the qubit as being "both 0 and 1 at once, " a.k.a. a superposition [31]. For example, 1 √ 2 (|0⟩ + |1⟩) is an equal superposition of |0⟩ and |1⟩. Joining multiple qubits together can form a larger value state with the tensor product (⊗) from linear algebra. For example, the two-qubit value state |0⟩ ⊗ |1⟩ (also written as |01⟩) corresponds to vector [ 0 1 0 0 ] . Sometimes a multi-qubit value state cannot be expressed as the tensor of individual value states; such value states are called entangled. One example is the value state 1 √ 2 (|00⟩ + |11⟩), known as a Bell pair. -qubit quantum value states are typically represented as 2 dimensional vectors. Alternatively, the values can be represented as different forms. For example, an initialized qubit typically has a value |0⟩ or |1⟩, which is named normal typed value state (Nor) in QNP. qubits that are in superposition but not entangled, such as 1 which are special quantum amplitudes (see below) such that the norm is 1, i.e., | ( )| = 1. In the above value state, we can view the local phase 1 as 0 , and 1 √ 2 0 is the amplitude for every basis ket. This is not a standard form for all unentangled multi-qubit value states, but rather a convenient way of representing a particular class of value states that are common in many quantum algorithms and Qafny can utilize for proof automation. The most general representation is to express quantum value states as a linear combination of basis kets [31], which is named path-sum formula in [2], as =0 | ⟩, where ∈ C is an amplitude, is an -length bitstring named basis, and ≤ 2 . The path-sum formula is same as 0 | 0 ⟩+...+ −1 | −1 ⟩, such that each -th element | ⟩ represents a basis ket in the superposition value state. This is named entanglement typed value state (CH) in QNP. For example, the bell pair can be represented as 2 | ⟩ with 0 = 00 and 1 = 11. Notice that the bases ( ) of basis kets are all distinct in a value state. QNP identifies these three different representations and uses a type system to properly transform quantum value state forms. Quantum Computations and Conditionals. High-level quantum programming languages are usually designed to follow the QRAM model [19], where quantum computers are used as coprocessors to classical computers. The classical computer generates descriptions of circuits to send to the quantum computer and then processes the measurement results. Computation on a quantum value state consists of a series of quantum operations, each of which acts on a subset of qubits in the value state. In the standard presentation, quantum computations are expressed as circuits, as shown in Figure 3a, which constructs a circuit that prepares the Greenberger-Horne-Zeilinger (GHZ) value state [11], which is an -qubit entangled value state of the form: |GHZ ⟩ = 1 √ 2 (|0⟩ ⊗ + |1⟩ ⊗ ). In these circuits, each horizontal wire represents a qubit and boxes on these wires indicate quantum operations, or gates. The circuit in Figure 3a uses qubits and applies gates: a Hadamard (H) gate and − 1 controlled-not (CNOT) gates. Applying a gate to a value state evolves it. Measurement. A special, non-unitary measurement operation is used to extract classical information from a quantum value state, typically when a computation completes. Measurement collapses the value state to one of the basis kets with a probability related to the value state's amplitudes. For example, measuring 1 √ 2 (|0⟩ + |1⟩) will collapse the value state to |0⟩ with probability 1 2 and likewise for |1⟩, returning classical values 0 or 1, respectively. Quantum Oracles. Quantum algorithms manipulate input information encoded in "oracles, " which are callable black box circuits. Oracles are typically viewed as quantum reversible implementations of classical operations, especially arithmetic operations. The quantum oracle behaviors are typically defined in terms of transitions between single basis kets. Through a quantum summation formula that has the behavior as an array map operation in Figure 2, we can infer its global state behavior based on the single basis ket behavior. oqasm [23] is a language that permits the definitions of quantum oracles with efficient verification and testing facilities by using the summation formula.

QAFNY EXAMPLES AND KEY DESIGN PRINCIPLES
Here, we first use two quantum algorithms-GHZ state preparation and quantum order finding-as examples to give an informal overview of our language L Qafny and then highlight several key design principles in Qafny. Figure 3c lists the GHZ proof outline, with initialized to an -qubit Nor typed value |0⟩ ( number of |0⟩ qubits). After preparing a superposition state for a single qubit [0] in line 2, the program executes a for-loop that creates entanglement between each adjacent qubits in . Breaking down the loop statement into pieces, we can view each iteration as a quantum conditional statement (if ( ) { }). In Qafny, an if statement couples all quantum basis kets mentioned in with ones mentioned in , stashes those basis kets not satisfying and finally executes in the remaining state. In the GHZ example, the -th iteration is unrolled Besides the minimal yet practical proof illustrated in the GHZ example, the quantum conditional structure cooperates well with complicated oracles, such as the modulo multiplication that's crucial in implementing quantum order finding. Applying similar proof techniques to the program in Figure 4, we can assert that the loop statement on line 3-5 entangles [0, ) with [0, ) having a In the QNP framework, this can be treated as a 2 -array of pairs where the -th pair represents | ⟩ | % ⟩. Such a representation is useful to define quantum conditionals, measurements, and other quantum operations in Figure 7. The measure( ) expression on line 8 is interpreted as a non-deterministic map filter function that first samples a pair | ⟩ | ⟩, with = % , from the above array and then removes all pairs whose second element disagrees with and finally keeps only the first element in every remaining pair. Because the modulo multiplication function is periodic; there exists a smallest natural number such that % = and the filtered array can be further reordered and rewritten as 1 √ =0 | + ⟩, where is the order. Constructing such proof outlines as ones in Figures 3c and 4 by hand are tedious and error-prone. Fortunately, programmers only need to provide the program and specifications in blue; then, the Qafny proof system will infer and verify the grayed out parts automatically 2 . Below, we introduce key features in our type-guided proof system to make the above verification largely automatic.

Monitoring Possibly Entangled Qubits with Types
Recall in GHZ (Figure 3c), each loop step in line 4-6 entangles [ ] with [0, ). However, the entanglement here is implicit: the program structure doesn't tell directly that [ ] is entangled with each qubit in [0, ) since it's a property from the program semantics. Our systematic approach to resolving the scopes of entanglement is to introduce sessions ( ) to group possibly entangled qubits, standard kind environments (Ω) to record kinds of each variable and session type environments ( ) to keep track of both sessions and their quantum value type.
In Qafny, variables may refer to one of three kinds 3 of values in Figure 5: integers 4 (kind C), measurement outcomes ( , ) (kind M), and quantum values (kind (Q )), where represents the probability of measurement with the outcome , and represents the number of qubits. (Q ) variable represents a physical -length qubit array. For simplicity, we assume there is neither alias in variable names nor overlapping between arrays referred to by any two different identifiers. Every session can then be defined by disjoint ranges, each of which re is represented by ( [ , )), an in-place array slice selected from to (exclusive) in , and there is no shared part between any two ranges in one session, written as re 1 ⊥ re 2 . We abbreviate a singleton session { [ , )} as [ , ) and similarly a singleton range [ , +1) as [ ].
A session type environment ( ) maps sessions to quantum types (Nor, Had, or CH in Section 2), where sessions in the domain are pairwise disjoint 5 . While kind environment is local and persistentthe variable kinds do not change unless it goes out of scope-session type environments are ephemeral: a statement that starts with the environment could end up with a different one ′ since a session could be modified during the execution. By design, a Nor or Had typed quantum value describes an array of qubits of normal typed (|0⟩ or |1⟩) and superposition value states, respectively; while elements in an array of type CH are basis kets | ⟩. We have subtyping relations over quantum types, i.e., Nor and Had are subtypes of CH, which means that Nor and Had typed quantum values can be rewritten as CH-typed ones. The index of session refers to the same position in a value state, which means if is [0, ), is |0⟩ and ↦ → , then [0] refers to the first qubit |0⟩ in .
One primary role of sessions and types in Qafny tracks an operation's session scope, approximating a collection of qubits directly and indirectly affected by the operation application. Figure 3b provides a typical scenario appearing in many quantum algorithms, including the GHZ and order finding examples above, where qubits in the blue part are added to the orange part one by one. In each loop-step in Figure 3c, a Nor-typed qubit [ ] is split from session [ , ) and added to session [0, ). In Figure 4, a Had-typed qubit [ ] is split from [ , ) and added to session { [0, ), [0, )} in each iteration. The former step appends a qubit |0⟩ to the end of every basis ket in the [0, )'s CH-typed value, while the latter duplicates { [0, ), [0, )}'s value and maintains the basis kets being distinct (see Section 4.2 for details). All these rewrites are automated in Qafny because we permit the type guided state equational rewrites (≡), which transform states to ideal forms that can facilitate our automated verification tool to apply proper Qafny proof rules. In Qafny, we enforce any state predicate representing a state to associate with a type environment by sharing the same domain, i.e., dom( ) = dom( ). Thus, the environment rewrites (⪯) gear the state rewrites. For example, the bottom proof step of Figure 6 transforms session [0, ) in to session above it, and the state rewrites in the pre-condition happen accordingly as (rewrites from left to right): Here, we add qubit [ ] (|0⟩) to the end of session [0, ) and transform session [0, + 1) to , so that the upper proof steps in Figure 6 can proceed, which will be discussed in the next subsection. The above example only develops intuition about the Qafny type system and equations. More details about them are explained in Section 4.2.

Qafny: A Type-Guided Proof System
As indicated by the above equation rewrites guided by types, the Qafny proof system is integrated with a type system, where Qafny's type-guided proof triple (Ω; ⊢ { } { }) states that if is a well-formed precondition with respect to , then executing will result in a well-form postcondtion w.r.t. ′ where Ω, ⊢ ⊲ ′ is a valid typing judgment (explained in Section 4.2). The well-formedness of predicates and mandates that each session mentioned in them must be in dom( ) and dom( ′ ) respectively.
On the bottom of Figure 6, other than the session rewrites from [0, ) to described above, a classical separation logic styled frame rule (rule P-Frame in Section 4.3) is applied to ignore the session [ +1, ) that has no effect on the rest proofs, and the type environment is transformed accordingly. On the top of Figure 6, we apply an oracle operation ( [ ] ← − [ ]+1). The behavior of the oracle application in Qafny is analogized to an array map function described in Figure 2. For every [ ] position in session 2 's basis kets, we flip its bit. Since [ ] locates at the first position in session 2 and it is a singleton CH-typed array, we then transform the pre-state 1 |1⟩ |1⟩|1⟩, by flipping the first bit. In Qafny, asserting an atomic operation application (state preparations, oracles, and diffusions) on a session always happens at the session's prefix positions, such as the [ ] position above. We enable state rewrites for permuting qubit positions, guided by type environment rewrites, to adjust qubit positions. For example, to perform the oracle application on the top, we first rewrite 1 to 2 in Figure 6, which transforms the pre-state from 1 |0⟩ |1⟩|1⟩, by pulling [ ], with value |0⟩, to the first position. During this process, the post-state is also transformed accordingly.
The middle proof applies a rule (labeled as P-If in Section 4.3) for a quantum conditional (if ( ) { }). In the proof rule design for a CH-typed state, it is favorable if we can classify all basis kets satisfying in the state, so that we can design a recursive step to handle the proof for applying only on these basis kets. This proof rule constructs an inductive relation between the conditional and its sub-component . Through the Qafny type system, we ascertain the sessions and ′ that can be accessed or manipulated in and , respectively, without consulting the semantics. Because of the no-cloning theorem that is guaranteed by our type system, the two sessions cannot overlap. In addition, we can always manage the CH-typed state as ⊎ ′ ↦ → ; then, for each basis ket in , we can group the prefix | | positions together, check if they satisfy , collect basis kets satisfying , execute on these basis kets, and assemble the result of executing back with those basis kets unsatisfying . In Qafny, we create a frozen construct M to collect basis kets and an unfrozen construct U to assemble the result back to previously frozen basis kets.
In Figure 6  : than | |, but the above basis ket manipulation does not shrink its length, which means that |1⟩ locates at a place beyond the reachability of session , named unreachable positions. In the poststate, we manipulate two U constructs to assemble computation results. The post-state above the is the result of executing , and we replace session 1 with U (1, , ) ( = [ -1]), indicating that the Boolean guard is 1-bit length. This U refers to the satisfying basis kets, and the result session is . For the value state in the pre-state ( ↦ → 2 =0 1 √ 2 | ⟩ |0⟩), we replace with U (¬ ) representing the basis kets unsatisfying . The two U constructs can merge to the final post-state at the bottom. We only keep the basis kets unsatisfying in U (¬ ) and assemble it with the basis kets in the U (1, , ) part by pulling the frozen |1⟩ to its corresponding location.
The detailed formalism of these Qafny design features is given in Section 4.3.

FORMALISM OF QAFNY AND L Qafny
This section presents the L Qafny language's syntax, the Qafny type system, the proof system, as well as the soundness and completeness theorems.

L Qafny Syntax
L Qafny is a C-like flow-sensitive language equipped with quantum data-flow operations, quantum conditionals, and for-loops. We intend to permit high-level quantum operations, such as state preparation (H and QFT [−1] ), oracle ( in Appendix B.4), and quantum reflection operations (Appendix A.1). Figure 7 shows the syntax of the language. Aside from standard form such as sequence ( ; ) and skip {}, statements also includes let binding (let = in ), two forms of quantum data-flow statements (_ ← − _), quantum/classical conditional (if ( ) ) and loop (for The let statement binds either the result of an arithmetic expression ( ) or a computational basis measurement operator (measure( )) to an immutable C/M kind variable and provides the binding to the body . This design ensures that all classical variables are immutable and well-scoped to avoid quantum observer effects by preventing any attempts to mutate a classical variable in the body of a quantum conditional. A quantum data-flow statement is one of ← − that applies state preparation operations (Hadamard H, quantum Fourier transformation QFT, or its inverse QFT −1 ) to qubits in , or ← − that applies an oracle operation to a session 6 . Other operations, including quantum diffusion and amplification operations, are in Appendix A.1. Quantum reversible Boolean guards are implemented as oqasm oracle operations, expressed by one of ( 1 = 2 )@ [ ], ( 1 < 2 )@ [ ], and [ ]. The meaning of these programs is that for each quantum basis ket, we compute 's value 1 = 2 , 1 < 2 and false respectively 7 , and store the result of ⊕ [ ] as a binary in [ ]. In both conditionals and loops, guards are used to represent the qubits that is controlling. In addition to the let bindings, the quantum for-loop also introduces and enumerates C-kind value over interval [ 1 , 2 ) with visible to both the guard and the loop body . As a result of immutability, the loop structure in L Qafny is guaranteed to terminate. If all variables in the guard are classical, the conditional or loop becomes a standard classical one.

Qafny Session Type System
Each L Qafny typing judgment is written as Ω; ⊢ ⊲ ′ , which states that is well-typed under the context mode and environments Ω and . The kind environment Ω is populated through let and for loops that introduce variables. Kinds are reused as context modes (C and M) to enforce no quantum observer effects in a quantum conditional, explained shortly below. L Qafny is a flow-sensitive language that utilizes context mode to detect the location where quantum measurement is not allowed. Selected type rules are given in Figure 8; the rules not mentioned are similar and can be found in Appendix A. The type system enforces three system invariants. Well-formedness. The type system enforces well-formedness and context restrictions on quantum programs. Well-formedness refers to the no-cloning theorem that qubits mentioned in a quantum conditional Boolean guard cannot be accessed in its body. In rule T-If, the side-condition ensures that the session for the Boolean and the conditional body does not overlap. Context restriction prevents quantum observer effects, that quantum conditional bodies cannot create and measure qubits. Each program begins with the context mode C, which permits most L Qafny operations. Once a type rule switches the mode to M, as in T-If, measurement operations are then suspended in this scope, as T-Mea is valid only if the context mode is C. Apart from the no-cloning theorem and the quantum observer effect, well-formed domains (Ω ⊢ dom( )) and well-formed predicates (Ω, ⊢ ) guarantee that every variable used in all sessions of can be found in Ω and all sessions used in logical predicates can also be found in a well-formed environment respectively. These two judgments maintain the scoping of assertions for the proof system. Their definitions are standard and can be found in Definitions A.1 and A.2.
Session Equivalence and Rewriting. The type system tracks the qubit arrangement of sessions and permits the session type environment partial order rewrites (⪯) through rule T-Par. In Qafny, we introduce equivalence relations for type environments (partial order ⪯) and states (≡) to permit automated state rewrites, as discussed in Section 3.1. We develop equivalence relations over quantum sessions, quantum values, type environments, and states (Appendix A.3). The common equivalence relations are state type rewrites, permutations, split and joins. Recall in Section 3.1 that state rewrites are guided by type environment rewrites. Similarly, type rewrites would also transform quantum state value forms. An example is to rewrite a CH-typed value state 1

=0
to Nor-typed 0 0 in Section 6.2. Permutation equivalence refers to two-qubit arrays that are equivalent under permutation. One example is to rewrite the session in Figure 4 line 7 from left to right, as: State joins merge two sessions. Merging a Nor-typed and CH-typed state puts extra qubits in the right location in every basis ket in the CH-typed state as the example in Section 3.1. Merging a Had-typed and CH-typed state duplicates the CH-typed basis kets. In a loop step in Figure 4 The state can be further rewritten to the one in Figure 4 by merging the two parts of the state value. Notice that the basis kets are still all distinct because the two parts above are distinguished by the |0⟩ and |1⟩ of the [ ] position. Merging two CH-type states computes the Cartesian product of basis kets in the two sessions (Appendix A.3). State split cuts a session into two individual sessions. The split of Nor and Had types is no more than an array split, while the split of a CH-type is equal to disentanglement, a hard problem. In quantum algorithms, splitting Nor and Had types are more common than disentanglement and is permitted in Qafny. For splitting CH-type, we invent an upgraded type system in Appendix A.5 to permit a few cases. Session Scope Approximation. The type system approximates the session scopes. In rule T-If, we use ⊎ ′ , as the approximate session that is large enough to describe all possible qubits directly and indirectly mentioned in 8 . Such scope approximation might be over-approximated, which does not cause incorrectness in our proof system, while under-approximation is forbidden. For example, if we combine two Had-typed qubits in our system and transform the value to CH-typed as 1 2 (|00⟩ + |01⟩ + |10⟩ + |11⟩), this is an over-approximation since the two qubits are not entangled. Partially measuring the first qubit leaves the second qubit's value unchanged as 1 √ 2 (|0⟩ + |1⟩). In addition to these system invariants, the type system allows C classical variables introduced by let to be evaluated to values in the type checking stage of the compilation time 9 , while tracks M variables in Ω. Rule T-Exp enforces that a classical variable is replaced with its assignment value in , and classical expressions in containing only are evaluated, so the proof system does not need to handle constants.

The Qafny Semantics and Proof System
Qafny sessions play two roles: as variable names representing quantum arrays and as qubit array structure indicators. We enforce the correctness by well-formedness and well-typed restrictions on states and proof system predicates. Qafny semantics is formalized as a small-step transition ( , , ) −→ ( ′ , ′ , ′ ), where and ′ are stacks storing local classical variables, and and ′ P-Frame are quantum states. To preserve the system invariants mentioned in Section 4.2, every valid proof judgment Ω; ⊢ { } { } also needs to satisfy an implicit type constraint TC as: Rule P-Con describes the proof consequence rule where a well-formed precondition under is replaced by ′ that's well-formed under ′ . This also shifts the type constraint judgment TC ( , , ) to TC ( ′ , ′ , ′ ). Rule P-Frame is a specialized separation logic frame rule 10 that separates both the session type environment and the quantum value state to support local reasoning on quantum states. Rule M-Frame in Figure 9 models the separating conjunction * . In addition to predicate well-formedness, the predicate semantic judgment (Ω, , , |= ) also put restrictions on domains dom( ) ⊆ dom(Ω) and demands the states ( ) well-formedness (Ω; ⊢ ), defined as follows: Definition 4.1 (Well-formed Qafny state). A state is well-formed, written as Ω; ⊢ , iff dom( ) = dom( ), Ω ⊢ dom( ), and: • For every ∈ dom( ) such that ( ) = Nor, ( ) = | ⟩ and | | ≤ | | and | | ≤ 1; specifically, M-mode states have a relaxed well-formedness, | | ≤ | | and =0 | | 2 ≤ 1. Recall that, in the example of Section 3.2, the |1⟩ position is frozen, the session is shrunk, and the session and basis ket qubit length is not the same. The definition models such a case, as it appears in the conditional rule introduced below. There is a trick to utilize the frozen positions for promoting proof automation, as the modeling rule M-Map equates two quantum values by discarding the frozen position qubits, and we will see an example in Section 6.1.
Rule P-Oracle is a classical separation logic style rule for oracles ← − , which analogizes such operations as classical array map operations mentioned in Figure 2. Each cell in the array represents a basis ket | ⟩ in . P-Oracle applies only to the part with type information in that is a subpart of session ⊎ ′ and corresponds to the part of every basis ket. 10 We use (Ω, ) ∩ (Ω, ) = ∅ here because (Ω, ) produces the session that modifies in Qafny. 11 | | and | | are the lengths of and , and | | is the norm. The rest rules similar to those in standard separation logic but with additional Qafny type constraints can be found in Appendix A.4. This freezing mechanism illustrated in Figure 11 and modeled by M-M is accomplished at two levels: stashing all kets not satisfying into ( ′ , ¬ ) and moving qubits satisfying in to the end of ′ in each ket. After substituting ⊎ ′ for M ( , ′ ), besides expelling the parts not satisfying , we also shrink the session ⊎ ′ to ′ , which in turn marked the portion in every basis ket inaccessible as is now invisible in the session type environment. Since type-checking preserves the fact that ′ ↦ → CH (rule T-If), ′ must only mention ′ , as it is required to be well-formed regarding the new environment. To retrieve frozen parts, we substitute session ⊎ ′ for U (| |, ¬ , ⊎ ′ ) in and for U (| |, , ⊎ ′ ) in ′ to represent the part satisfying and its complement. The semantics (M-U), defined as a logical equivalence, describe a special predicate that utilizes the innate relation of separating conjunction and logical complement to assemble the previously frozen, thus unmodified part with the basis kets evolved during the execution of .
Rules S-Loop and P-Loop are the semantic and proof rules for a for loop where ( ) is the loop invariant parameterized over the loop counter . There are other rules in Appendix A.4 that are similar the rules in a separation logic framework with additional Qafny type restrictions. Measurement. A measurement let = measure( ) in collapses a qubit array , binds a M-kind outcome to and restricts its usage in . In Qafny, we encode the density matrix semantics for measurement by an array filter and a classical probability distribution library in Dafny (Appendix A.9). Figure 13 shows an analogy of the measurement behavior (proof rule P-Mea in Figure 12). Assume that the session containing is [0, ) ⊎ . The measurement is essentially a two-step array filter: 1) The CH type state, =0 | ⟩ | ⟩ + ( , ≠ ) in rule S-Mea, is partitioned into two parts by randomly picking a basis ket's first portion as the partition key (the peach part in Figure 13 and in the state); and 2) we create a new array by removing the non-key basis kets (the ( , ≠ ) part) and also remove the [0, ) portion in every remaining basis ket, so that the above state becomes =0 √ | ⟩ as the part is removed. Notice that the newly created array's basis ket size is smaller than the original array; thus, the amplitude of each element is increased by a factor of 1 √ .

Fig. 13. Measurement Analogy
Notice that the orange basis kets appear in a periodical pattern in the whole array in many cases. Many quantum algorithms utilize the periodical pattern. In designing the proof rule P-Mea, a session type operation F ( , , ), with its modeling rule FModel, is introduced to do exactly the two steps above by selecting an -length prefix bitstring in a basis ket for the range [0, ), computing the probability , and assigning ( , {| | }) to variable . Rule P-Mea replaces session [0, ) ⊎ in with the measurement result session F ( , , ) and updates the type state Ω and by replacing [0, ) ⊎ with .
Here, we show a proof fragment above for the partial measurement in Figure 4  Randomly picking a bitstring % also filters a specific in range [0, ), i.e., we collect any having the relation % = % . Notice that modulo multiplication is a periodical function, which means that the relation can be rewritten + % = % , and is the order. Thus, the [0, ) state is rewritten as a summation of : 1 √ =0 | + ⟩. The probability of selecting (| % | ) is 2 . In Qafny, we set up additional axioms for these periodical theorems to grant this kind of pre-and post-condition equivalence.

Qafny Metatheory
Here, we show the type soundness and proof system soundness and completeness. Type Soundness. We prove that well-typed Qafny programs are well-defined, i.e., under the wellformedness assumption, the type system is sound with respect to the semantics, (Definition A.1 and Definition 4.1). The Qafny type soundness is stated as two theorems, type progress and preservation. The proofs are done by induction on statements and mechanized in Coq.  Proof System Soundness and Completeness. Qafny proof system is sound and complete with respect to its semantics for well-typed Qafny programs. This is formalized as theorems and proved in Coq. A critical concept in these theorems is the most general state representation * of evaluating ( , , ) defined in Definition A.3. In Qafny, CH is taken as the most general state representation over Nor and Had since they can all be converted into a CH-typed quantum value, but not the other way around. In proving the theorems, we rewrite post-states to most general forms, then relate the states with predicates. The Qafny proof system only describes the quantum portion built on top of the Dafny system. Since every quantum program in L Qafny doesn't diverge, the soundness and completeness refers to the total correctness of the Qafny proof system. The L Qafny proof system correctness is defined in terms of programs and predicates being well-typed.

QAFNY PROOF SYSTEM AND PROGRAM COMPILATION
Here, we discuss the proof system compilation from Qafny to Dafny, as well as the quantum language compilation from L Qafny to sqir. Ξ is a map from sessions to Dafny predicate variables, holding variables used in ′ and ′ to represent sessions. We formalize rules for this judgment in Coq and prove the compilation correctness, explained shortly below. We also faithfully implement the compiler in Dafny and verify many quantum programs in Section 6.

Translation from Qafny to Dafny
In a separation logic framework, there are stack and heap variables. The former represents pointers, and the latter represents accesses to physical memory locations. In Qafny, sessions are conceptual pointers, such that they identify the scopes of entangled qubits and direct the pointed-to locations of qubits; while quantum values represent quantum heaps that store qubit values. However, sessions are virtual qubit arrays whose scopes can be dynamically modified, and quantum values have three different representations that can also change dynamically. Classical arrays with fixed value forms and sizes cannot capture these features. Therefore, in framing the target compilation data structure, we arrange it as the one in Figure 14. We map sessions to stack variables and quantum values to recursive datatypes of physical arrays. Different physical arrays refer to different range variables in Figure 5 that essentially define physical qubit arrays. Recursive datatypes provide a way of managing different ranges together and forming virtual qubit arrays. Additionally, each recursive datatype has a type field, which determines the type of value form to load. Accessing a value of specific session with a certain type is mapped to a conjunction, type( ) = * ↦ → ′ , where and ′ are the compiled stack variable and recursive datatype for representing and , respectively. Recall that sessions in a state are all disjoint-unioned, and we do not have aliasing and pointer variables in Qafny. At any given time, we enforce that only one stack variable represents a session with a fixed value type , which is tracked by Ξ and .
There are three important steps in the compiler. First, every time there is a change in sessions, such as qubit position permutation and split/join of sessions, we generate additional variables representing transformed sessions. Second, for a program , if there is a change of quantum value types, we insert an additional construct to reflect the change so that Dafny can capture the value type transformation. The physical array qubit locations and values do not change in these two steps. Instead, we manipulate the recursive datatype to perform the proper virtual qubit array arrangement and value type transformation. Third, we generate additional Dafny axioms and inference rules for capturing the Qafny operation semantics and additional construct modeling, such as the oracle operation semantics, frozen and unfrozen construct modeling rules in Section 4.3. In the compiled program, we replace session with variable 4 . In the pre-and post-condition compilation, we connect variables with sessions using the ses function that takes a variable and outputs its pointed-to session. In the Qafny compiler, we use Ξ to track such information, e.g., we need to generate a new variable 4 in Ξ to represent the join session { [0, ), [0]} after the join statement. In addition, we use type predicates to track value types in the compiled conditions.
In compiling quantum conditionals, not only do we need to do the above type conversion, but will we also explicitly insert frozen (M) and unfrozen (U) functions, e.g., in computing the conditional if  The above figure depicts two translation rules with the blue part being the sqir circuits, 12 while the rest is in Appendix A.6. The first rule describes the translation of a quantum conditional to a controlled operation in sqir. Here, we first translate the Boolean guard @ [ ] 13 , and sequentially we translate the conditional body as an sqir expression controlled on the [ ] position. ctrl generates the controlled version of an arbitrary sqir program using standard decompositions [31,Chapter 4.3]. The last rule translates L Qafny for-loops. Essentially, a for-loop is compiled to a series of conditionals with different loop step values. The compiler is implemented in Coq and validated through testing. We extract the L Qafny semantic interpreter and the L Qafny to sqir compiler to Ocaml and compile the compiled sqir programs to OpenQASM [9] via the sqir compiler. Then, we run the test programs in the L Qafny OCaml interpreter and compiler and to see if the results match. 12 Translation in fact threads through the typing judgment, but we elide that for simplicity. 13 [4], andmeans no data. Human efforts measure the time for a single person to finish programming and verifying an algorithm. We do not mean to compare the coding lines to other frameworks since the coding line numbers might vary depending on many factors. We only provide a hint about the automation in Qafny.
Overall, we run 135 unit test programs to test individual operations and small, composed programs, and all the results from the L Qafny interpreter and compiler are matched.

EVALUATION AND CASE STUDIES
We evaluate QNP by (1) demonstrating how many efforts are required to verify existing quantum algorithms, and (2) showing how the design of the system can empower users to prototyping and verifying their new ideas. Figure 15 shows the algorithms being verified in Qafny. The QNP project began with the attempt to verify Shor's algorithm directly on Dafny, which took a researcher 30 days to finish. We then generalized proof techniques, abstracted over the similarities in program structure, and implemented a compiler that transforms Qafny to Dafny, which permits the algorithm expressing in a much cleaner way with the verification completed in 36.3 seconds. Performing most Qafny verification does not take more than a minute to finish, which is relatively comparable to most automated verification frameworks [22,35], and better than the existing quantum automated frameworks, such as QBricks [4], as indicated in Figure 15.
Besides shorter running time, verification in QNP saves programmers' human efforts, indicated by the number of lines (LOC) in writing algorithm specifications in QNP. As shown in Figure 15, all the algorithms are written in less than 49 LOCs. In contrast, algorithm specifications and verification in other frameworks require much more lines. For example, Grover's search specification in quantum Hoare Logic [25] takes 3184 LOCs, and Shor's algorithm specification in QBricks [4] has 1163 LOCs in Figure 15. Concise specifications usually indicates saving human efforts. Most algorithms except Shor's algorithm that was constructed along the development of Qafny (Figure 15) are verified by a single researcher within three days. As a comparison, the complete Shor's algorithm correctness proof [33] was finished by four researchers and took two years.
In addition, we also envision the QNP framework as a rapid prototyping tool for quantum programs with two examples, controlled GHZ gates and quantum walk algorithm.

Controlled GHZ Case Study: Building Quantum Algorithms on Others
Automated verification frameworks such as Dafny encourages programmers to build a program proof based on the reuse of subprogram proofs. However, this perspective is more or less overlooked in previous quantum proof systems. In voqc, verifying the correctness of a controlled GHZ, a simple circuit constructed by extending GHZ with an extra control qubit, requires generalizing the GHZ circuit to any arbitrary inputs. In the QNP, users do not need to undergo this involved process. Figure 16 provides a proof of the Controlled GHZ algorithm based on a proven GHZ method in Figure 3c. The focal point is the quantum conditional on line 5. For verifying a GHZ circuit, its input 16. Controlled GHZ circuit and proof. ghz( ) is given in Figure 3. Lines 3-4 are automatically inferred.
is an -qubit Nor-typed value of all |0⟩, but the given value, in line 4, is a CH-typed entanglement 2 =0 | ⟩ |0⟩. Here is where voqc gets stuck. In Qafny, we automatically verify the proof by rule P-If and the equivalence relation to rewrite a singleton CH value to a Nor one, as 1 After rule P-If is applied on the second and third line, session [0, )'s value is rewritten to a Nor type value on the top as |0⟩|1⟩, where |0⟩ is qubits and |1⟩ is frozen. Since two values are equivalent as Qafny discards frozen bits, |0⟩|1⟩ is equivalent to |0⟩, which satisfies the input condition for GHZ, so that all proof obligations introduced to invoke the ghz method are discharged.

Case Study: Understanding Quantum Walk
Quantum walk [5,46,47] is a quantum version of the classical random walk [37], and an important algorithmic frameworks for writing quantum algorithms. However, most quantum walk analyses were based on Hamiltonian simulation evolving, which deters many computer programmers from inventing quantum walk algorithms. Here, we show that the discrete-time quantum walk, at its very least, is a quantum version of breadth first search. Figure 17 lists the proof outline for the core loop of a discrete-time quantum walk algorithm on a complete binary tree. We first prepare four ranges (registers): a -qubit loop step register in superposition , an -qubit ancilla register ( = 2 ) where [ ] keeps the result of evaluating [0, ) < +1 for -th loop step, a single qubit coin that determines the moving direction of the next step, 1 for the left and 0 for the right, and an -qubit node register that stores the node keys with 0 for the root node. This loop statement entangles all these four registers together as session In executing the -th loop step, all basis kets are divided into two sets, described by the two parts separated by + in ( ). If a basis ket's [0, ) portion is less than , it belongs to the active set, while the other ones are inactive. We also have an invariant that all basis kets in the active set have distinct non-zero node keys. Each loop step performs three operations. First, a basis ket with the [0, ) part equal to is moved to the active set, done by surprisingly the Boolean guard [0, ) < +1. The Boolean guard also freezes inactive basis kets, so the next two operations are only applied on active basis kets. Second, the Hadamard operation on in line 4 creates a mirrored copy for every active basis ket 14 . Recall that active basis kets have distinct keys; thus, the mirrored copy of every active basis ket must have 0 amplitude before the H application, because it is not existed. The H operation creates the mirrored copy of every active basis ket by averaging the two amplitudes. Finally, the operations in line 5-6 transform every active set basis ket's node key stored in [0, ) to its child's key depending on the coin direction 15 . Notice that mirror basis kets always reach two different children nodes and the -depth nodes become ( + 1)-depth after the two applications, so the distinct key property is resumed.
Executing -steps of the for-loop results in a quantum value containing all possible tree nodes up to -depth except the root node, stored as basis kets; stated as the post-condition in Figure 17. The verification in Figure 17 describes the basic property for the quantum walk algorithm framework. The biggest advantage of the framework is to allow the manipulation of different quantum applications on different tree nodes in each loop step, which is why many algorithms [1,5,6,27] have been developed based on the framework.

RELATED WORK
Quantum Proof Systems and Verification Frameworks. Previous quantum proof systems, including quantum Hoare logic [10,25,48,49], quantum separation logic [20,51], quantum relational logic [24,45], and probabilistic Hoare logic for quantum programs [18], enlightened the development of QNP. The problems of these works are three: 1) their conditionals are solely classical, while QNP has quantum conditionals; 2) most of them are theoretical works or implemented as tactics in interactive theorem provers; thus, it is unclear if they can be implemented in a framework that utilizes classical SMT solvers for proof automation for verifying comprehensive quantum programs; and 3) they did not compile quantum programs to circuits. Quantum separation logic [20] develops a frame rule and suggests that a Had typed state can be split into two parts, which is similar to our Had typed state split equation but different from the frame rule in QNP that is based on classical separation logic.
There are works on formally verifying quantum programs, including Qwire [36], sqir [14], and QBricks [4]. These tools have been used to verify a range of quantum algorithms, from Grover's to Shor's algorithms. The former two tools provided libraries in a proof assistant to help verify quantum programs, and they have circuit compilation models, while the latter one built a proof system on top of a proof assistant to achieve some proof automation without providing a circuit compilation model. Some comparison between QBricks and QNP are given in Section 6. The key difference between QBricks and Qafny is that QBricks' deductive system is based on classical operations, such as classical conditionals and sequencing operations, and views quantum operations as nonseparable units; while Qafny develops proof rules for quantum operations, such as state preparation, measurement, and quantum conditionals, such that quantum operations are verified based on the recursive proof of merging sub-proof steps for separable components, as the rules in Figure 10 and the proof in Section 6.1. Classical Proof Systems. Qafny is enlightened by the classical separation logic [38], and many others [17,26,30,41,44,50]. Especially, the Qafny proof system is compiled to Dafny [21], a language that is designed to make it easy to write correct code. It permits imperative programming with logical specifications that can be automatically verified through the Dafny proof system, a separation logic based system. The natural proof methodology enlightens the QNP development [26,28,32], which was first proposed by Madhusudan et al. [28,34]. It exploits a fixed set of proof tactics, keeping the expressiveness of powerful logic, retaining the automated nature of proving validity but giving up on completeness, e.g., the Qafny to Dafny compilation is only sound but not complete, and the Qafny type system essentially classifies a subset of hybrid quantum-classical programs that can be compiled to Dafny for automated verification.

CONCLUSION
We present QNP, a system for expressing and automatically verifying hybrid quantum-classical programs whose quantum components can be compiled to quantum circuits. QNP's methodology is to develop a proof system, Qafny, that views quantum operations as classical array aggregate operations, e.g., viewing quantum measurements as array filters, so that we can map the proof system to classical verification infrastructure. The Qafny proof system is sound and complete with respect to the L Qafny semantics for well-typed L Qafny programs. We have verified the soundness of the compilation from Qafny to Dafny and utilized the Dafny proof infrastructure to verify many quantum programs. We also compile Qafny programs to SQIR, which permits quantum programs to run on a quantum computer. We believe that programmers can utilize QNP to develop quantum algorithms and verify them through our automated verification engine with a great saving of human efforts, as demonstrated in Section 6.

A QAFNY FULL DEFINITION AND MORE EXAMPLES
Here, we provide the details of the Qafny language and proof system, with more examples. : A.2 Qafny function with Session Generation Here, we discuss the function for calculating a session in an expression, such as arithmetic and Boolean equations, which is related to a hidden check-in Qafny-the kind check. The calculation for other kinds of statements and expressions follows the same pattern. Figure 19 provides the kind check rules for arithmetic and Boolean equations. Here, we enforce a partial order on variables kinds as C ≤ M ≤ Q, such that the kind of an expression depends on the most general variable kind in the expression. The construct − here refers to arithmetic, Boolean equations, or a statement.

A.3 State Equivalence
As we suggested in Section 4.3, Qafny utilizes type environment and quantum state equations to rewrite sessions and states in predicates to a canonical form, where the automated verification tool can apply proof rules by pattern matching. Essentially, quantum computation is implemented as

Fig. 19. Arith and Bool Checking
circuits. In Figure 3a, if the first and second circuit lines and qubits are permuted, it is intuitive that the two circuit results are equivalency up to the permutation. Additionally, as mentioned in Section 4.3, we sometimes need quantum sessions to be split and regrouped. All these properties are formulated in Qafny as equational properties in Figure 20 that rely on session rewrites, which can then be used as built-in libraries in the proof system. As one can imagine, the equational properties might bring non-determinism in the Qafny implementation, such that the automated system does not know which equations to apply in a step. In dealing with the non-determinism, we design a type system for Qafny to track the uses, split, and join of sessions, as well as the three value state types in every transition step so that the system knows how to apply an equation. Figure 20 shows the equivalence relations on types and values. Figure 20a shows the subtyping relation such that Nor and Had subtype to CH. Correspondingly, the subtype of Nor to CH represents the first line equation in Figure 20b, where a Nor-typed value is converted to a CH form. Similarly, a Had-typed value can also be converted to a CH value in the second line. Additionally, Figure 20c defines the equivalence relations for the session concatenation operation ⊎: it is associative, identified with the identity empty session element ∅. We also view a range [ , ) to be empty (∅), and a range [ , ] can be split into two ranges in the session as [ , ) ⊎ [ , ).
The main result to define state equivalence is to capture the permutation symmetry, split, and join of sessions introduced in Section 4.3. The first rule describes the case for the empty session, while the second rule in Figure 20e connects the quantum value state equivalence to the state equivalence. The third rule describes the qubit permutation equivalence by the mut function. The fourth rule describes the joining of two sessions in a state. A join means an array concatenation for the two sessions of the type Nor and Had. If the two sessions have CH types, a join means a Cartesian product of the two basis kets. The final rule is to split a session, where we only allow the split of a Nor and Had-typed state, and their splits are simply array splits. Splitting a CH-typed state is equivalent to qubit disentanglement, which is a hard problem, and we need to upgrade the type system to permit certain types of such disentanglement. In Appendix A.5, we upgrade the Qafny type system to a dependent type system to track the disentanglement of CH-typed state; thus, we upgrade the equivalence relations to a new set.

A.4 Additional Typing Semantic and Proof Rules and Well-formedness
Here, we first provide the well-formed session domain and state predicate definitions below.
Definition A.1 (Well-formed session domain). The domain of a environment (or state ) is well-formed, written as Ω ⊢ dom( ) (or dom( )), iff for every session ∈ dom( ) (or dom( )): is a single bit either 0 or 1. The . operation is a bitstring concatenation. Term * is a summation formula that omits the indexing details. Term ( 1 • is disjoint unioned, i.e., for every two ranges Definition A.2 (Well-formed state predicate). A predicate is well-formed, written as Ω, ⊢ , iff every variable and session appearing in is defined in Ω and , respectively; particularly, if = ↦ → * ′ , ∈ dom( ). Figure 21 provides additional Qafny type rules. Here, we have additional rules TP-N, TP-H, and TP-CH to track the type transformations for state preparation operations if the initial values are in Nor, Had, and CH types, respectively. If a session has Had type, the type transformation is allowed only for H operations. Rule TRed types the amplification operation, similar to the diffusion typing rule. Rule TInit provides the type judgment for qubit allocations. Here, we assume that variable PExpM

Fig. 22. Additional Semantic and Proof Rules A
is a fresh variable, and once the allocation happens, the variable represents a physical qubit array location named , and its scope is global to the whole program execution, as [0, ) stays at the type environment . We handle the variable scope in the Qafny implementation by always converting newly introduced variables, appearing in let and qubit allocation operations, to the fresh variable by proper alpha conversions. Quantum diffusion operations ( ← − dis) reorient the amplitudes of basis kets. They are analogized to an aggregate operation of reshape and mean computation; both appeared in some programming languages, such as Python. The aggregate operation first applies a reshape, where elements are regrouped into a normal form, as the first arrow of Figure 24. More specifically, the diffusion function D ( , ) (Rule SDis and PDis in Figure 23) first takes an ′ -element CH typed value state =0 | ⟩, where

Fig. 23. Additional Semantic and Proof Rules B
corresponds to the number of qubits in . Then, we rearrange the value by extending the element number from ′ to * by probably adding new elements that originally have zero amplitude (the white elements in Figure 23). Here, let us view a basis as a small-endian (LSB) number {| | }. The rearrangement of changing bases (for all ) to (| | ). is analogized to rewrite a number {| | } to be the form 2 + , with ∈ [0, 2 ), i.e., the reshape step rearranges the basis kets to be a periodical counting sequence, with 2 being the order. The mean computation analogy (the second arrow in Figure 24) takes every period in the reshaped value state, and for each basis ket in a period, we redistribute its amplitude by the formula (  arbitrary number. If we do so, whenever a new basis ket is introduced to the active set, its amplitude will be reduced compared to other basis kets in the active set. The amplitudes, which represent the basis ket likelihood, are low for each basis ket here. In quantum computing, amplification operations serve the opposite of quantum diffusion to increase certain basis ket amplitudes. Notice that every new basis ket that becomes active in each loop step starts with the root node, which means that basis kets having S -th depth nodes have higher amplitudes than basis kets having -th depth nodes so that those leaf nodes having the biggest amplitudes, which is ideal because most tree algorithms are likely to work on the leaves rather than the middle transition nodes.

A.5 An Upgraded Type System and Equivalence Relations
Here, we describe an upgraded type system based on the one in Figure 7, which upgrades it to a dependent type system by including basese in every basis kets. The type system is under construction in the Qafny implementation. We first show some additional syntax below: Each construct type is only associated with additional flags depending on the quantum states. The flag opt for Nor means that we can track the basis ket bitstring of the Nor typed value state | ⟩ in the type checking stage. Sometimes, we might be unable to track the basis, so we will classify it as ∞. Similar to the Nor typed situation, we use ⃝ to represent that a Had typed value state is in uniformed superposition. If not, we can classify the Had typed basis ket as ∞. In dealing with CH typed value states, we will use a set of bases ( ) to refer to the basis ket bitstrings appearing in a CH typed value state =0 | ⟩. In ( ), is a basis set and is the element number, and it can be abbreviated as .
The biggest advantage of the upgraded type system is to permit additional quantum state equational rewrites based directly on type predicates without developing additional built-in predicates 26. Upgraded type environment partial order. We use set union (∪) to describe the type environment concatenation with the empty set operation ∅. is a single bit either 0 or 1. The . operation is a bitstring concatenation. × is the Cartesian product of two sets. is either Nor, Had or CH.
in the Qafny to Dafny compilation. We have new subtyping and quantum value state equivalence relations in Figure 25. The subtyping relation ⊑ and the value state equivalence ≡ are not associated with a qubit number (session length number) , such that they establish relations between two quantum values describing a session of length . ⊑ in Figure 25a describes a type term on the left that can be used as a type on the right. For example, a Nor type qubit array Nor can be used as a single element entanglement type term CH { } 16 . Correspondingly, value state equivalence relation ≡ , in Figure 25b, describes the two value states to be equivalent; specifically, the left state term can be used as the right one, e.g., a single element entanglement value state 1 =0 | ⟩ can be used as a Nor typed value state | 0 ⟩ with the fact that 0 is now a global phase that can be neglected.
In addition to the rewrites in Figure 20, we now permit the rewrites from a CH typed value to a Nor typed one if we find that the CH typed value contains a singleton basis ket, while a CH typed value state can also be rewritten to a Had typed one if we find that the length of the CH typed value state is 1, and it contains exactly two basis kets. Figure 26 and Figure 27 provide upgraded equivalence relations for type environments and quantum states. The biggest improvement compared to the ones in Figure 20d and Figure 20e is the split of a CH typed quantum state. Notice that splitting a CH typed quantum state is equivalent to disentanglement, and we only provide one case for such splitting. The split function (spt) sees if every basis ket in the CH type has a common factor. If so, we can split the state by factoring in the common factor. For example, |00⟩ + |10⟩ can be disentangled as (|0⟩ + |1⟩) ⊗ |0⟩, as the common factor |0⟩ is factored out from the original formula |00⟩ + |10⟩. Figure 28 provides some rules in the upgraded type system. Other than the functionality we discussed in Appendix A.1. The biggest difference is that we now need to track the basis ket bitstrings appearing in CH, Had, and CH typed value states. In rule TA-CH, we find that the oracle is applied on belonging to a session ⊎ ′ . Correspondingly, the session's type is CH ( ), for each basis 1 . 2 ∈ , with | 1 | = | |, we apply on the 1 and leave 2 unchanged. Here, we utilize the oqasm semantics that describes transitions from a Nor-typed value state to another Nor one, and we generalize it to apply the semantic function on every element in the CH type. During the transition, the number of elements does not change. Similarly, applying a partial measurement on range [0, ) of the session [0, ) ⊎ in rule TMEA-N can be viewed as an array filter, i.e., for an element, 1 . 2 in set of the type CH ( ), with | 1 | = , we keep only the ones with 1 = (| | ) ( 27. Upgraded quantum state equivalence. We use set union (∪) to describe the state concatenation with the empty set operation ∅. is a single bit either 0 or 1. The . operation is a bitstring concatenation. Term * is a summation formula that omits the indexing details. Term ( 1 is the measurement result) in the new set ′ and recompute | ′ |. In Qafny, the tracking procedure is to generate symbolic predicates that permit the production of the set ′ (| ′ |), not to produce such sets. If the predicates are not effectively trackable, we can always use ∞ to represent the set. In addition, the upgraded type system enforces equational properties of quantum qubit sessions through a partial order relation over type environments, including subtyping, qubit position mutation, merge, and split quantum sessions. This property is enforced with the additional equivalence relations in Figure 26 and Figure 27. Based on the new CH type with the set 1 × 2 , the quantum conditional creates a new set based on 1 × 2 , i.e., for each element (| | ). . in the set, with |(| | )| = | 1 |, we compute Boolean guard value by substituting qubit variables in with the bitstring basis (| | ), and the result [(| | )/ 1 ] ⊕ is true or not ( represents the bit value for the qubit at [ , S ]); if it is true, we replace the basis by an updated basis by applying the semantics of the conditional body if we can learn about its semantics; otherwise, we keep to be the same. In short, the quantum conditional behavior can be understood as applying a conditional map function on an array of bitstrings, and we only apply the conditional body's effect on the second part of some bitstrings whose first part is checked to be true by computing the Boolean guard .
A.6 Translation from L Qafny to sqir Full Rules In addition to Section 5.2, Figure 29 provides the other compilation rules for the operations in Figure 7. In compiling the value and diffusion operations, we utilize the verified voqc infrastructure [15] for the H, QFT, and diffusion circuits. The function ( ) translates the session to a qubit array with the physical indices required in sqir. The last two rules in the first line show how a let-binding is handled for a C and M kind variable. Similar to the type system, we assume that let-binding introduces new variables, probably with proper variable renaming. The rule for ← − describes an oracle application compilation, which is handled by the oqasm compiler [23]. The Qafny type system ensures that the qubits mentioned in are the same as qubits in session so that the translation does not rely on itself.

A.7 The Proof of The Order Finding Portion in Shor's Algorithm
We first discuss Shor's algorithm [43]. Given an integer , Shor's algorithm finds its nontrivial prime factors, which has the following step: (1) randomly pick a number 1 < < and compute = gcd( , ); (2) if ≠ 1, is the factor; (3) otherwise, and are coprime and we find the order of mode ; (4) if is even and 2 ≠ −1% , gcd( 2 ± 1, ) are the factors, otherwise, we repeat the process.
Step (2) is Shor's algorithm's quantum component, which is an order-finding algorithm. Figure 4 discusses its pre-measurement part. Without the type environments, we show the full Qafny proof in Figure 30. In the Qafny implementation, verifying a quantum program requires only the user input of the pre-, post-, and loop invariant. For example, the proof of Figure 30 in Qafny requires no states grayed out; only the conditions marked blue. The core of the ordering finding algorithm in Figure 4 can be analogized as an efficient array filter operation, given in Figure 31. Figure 4 discusses all the steps up to line 15 in Figure 30. Here, we focus on the later parts. Line 16-18 is the quantum phase estimation part of the order finding algorithm. In line 16, we apply an inversed QFT gate. The main functionality is to push the values to the basis state's amplitudes as =0 . Then, line 18 measures variable . In this procedure, we will get the period as part of the measurement result as ( 4 2 , ). However, in the actual order-finding implementation, cannot be directly used as an order number. Instead, we need a post step, the continued fraction method, to retrieve the order, which is stated as is its probability value. In the QNP implementation, we implement the conditioned fraction post steps and all these probability theorems in Dafny by writing them as a Dafny library and providing mechanized proofs by mimicking the proofs in [33].
As an additional example for the frozen and unfrozen functions in the proof rule of quantum conditionals in Section 4.3, we provide an additional proof tree for the quantum conditional in a loop step in line 9-11 in Figure 30 Figure 9. Notice that the type environment is also transitioned from to 1 . By the same strategy of the U rule in Figure 10

A.8 The Program and Proof of Grover's Search in Qafny
Here, we show the Qafny program and proof for Grover's search algorithm [12]. Figure 32 provides the proof steps of the algorithm in Qafny. The Qafny proof system can automatically infer the gray parts in the proof with some understanding of trigonometric theorems provided by our researcher in the Dafny framework. The function () is a predefined oracle function. There are two properties for it. First, we know that is the key in the oracle function. () | ⟩ = −1 · , if = ; otherwise, () | ⟩ = −1 · . Second, we also require that such a key is unique for all ∈ [0, 2 ). Thus, if we input a CH typed value state 2 =0 | ⟩ to the oracle function, the result value can be divided into two parts: − 1 Notice that for any quantum value =0 | ⟩, we have =0 | | 2 = 1. For the above two parts, if we view 1 ). When we apply the () function inside the loop, we can see that 's value state is transformed to − cos | ⟩ + sin · . The second step is to apply the quantum diffusion operation, which increases the amplitude values. The result gives us the post-loop step state for as cos +1 | ⟩ + sin +1 · . The reason is set up as an additional theorem in Dafny, and the transitions are as follows: 2 − cos cos + sin sin (cos | ⟩ + sin · ) − − cos | ⟩ + sin · = −2 cos 2 cos + 2 sin sin cos + cos | ⟩ + −2 sin cos cos + 2 sin 2 sin − sin · = 1 − 2 cos 2 cos + 2 sin sin cos | ⟩ + −2 sin cos cos + 2 sin sin 2 − 1 · = − cos (2 ) cos + sin (2 ) sin | ⟩ + − sin (2 ) cos − sin cos (2 ) · = cos ( − 2 ) cos + sin ( − 2 ) sin | ⟩ + − sin ( − 2 ) cos + sin cos ( − 2 ) · = cos ( ) cos + sin ( ) sin | ⟩ + − sin ( ) cos + sin cos ( ) · = cos − | ⟩ + sin − · = cos +1 | ⟩ + sin +1 · A quantum diffusion operation can also be viewed as a trigonometric rotation, and the above calculation shows that the rotation eventually turns the degree to +1 . At the end of the program in Figure 32, before the measurement, the 's value is cos | ⟩ + sin with = − ⌊ ⌋ · . Notice that 0 ≤ < , so we will have the probability of reaching the measurement result to be greater than cos 2 ( ). The estimation can be better, but any other analysis will follow the same pattern introduced here.
In the Qafny implementation, we set up trigger rules to rewrite the term in line 4 in Figure 32 to the trigonometric format in line 5. Then, we also provide theorems to support the rewrite of 's value state from − cos | ⟩ + sin · to cos +1 | ⟩ + sin +1 · in line 10. The Dafny proof system automatically derives the other proof.

A.9 The Limitation of the Dafny Classical Distribution Library
The L Qafny is universal in terms of the power of expressing quantum programs since all gates in the universal RzQ gate set {H, X, RZ, CNOT}. H can be defined by the L Qafny state preparation operation, X and RZ can be defined by the oracle operation, and CNOT gate can be defined by the quantum conditional in L Qafny . The measurement operation in L Qafny allows us to define a computational basis (|0⟩ and |1⟩) measurement, which permits us to define any measurement operations with the universal gate set.
However, being able to define all possible quantum programs does not mean that we can utilize QNP to automatically verify all quantum programs, especially hybrid quantum-classical programs. QNP permits automated verification for programs in Figure 15, with some supporting library theorems in Dafny. We can summarize a common pattern QNP can verify from these programs as a structure ; measure, where we first apply some quantum unitary operations with measurement operations at the end. The measurement operations do not need to happen simultaneously, as we permit partial measurement operations. However, each qubit can only measure once. Any program with such a structure can be largely verified automatically in QNP by the methodology shown in this paper.
If programmers want to measure some qubits resulting in ( , ), with being the probability and being the measurement result, and then utilize the result as an input to another quantum program ; the QNP's proving power depends on the properties the programmers want to verify. If the programmers only want to verify the post-state of executing with the input , this is a perfect scenario for QNP. On the other hand, if programmers want to know the probability of having the post-state of executing with the input probability of , this scenario will require additional theorems to be proved in the Dafny's classical probability distribution library, which is out of the scope of the paper mainly focusing on the Qafny proof system. In the current stage, the library in Dafny is not powerful enough to automatically verify many cases. The above scenario typically appears in quantum cryptography protocol algorithms. In verifying such algorithms, it is not likely that Dafny's probability library will be able to infer the probability bound of encryption breaking with a large degree of proof automation.
In future work, we intend to enhance Dafny's probability distribution library to automatically verify many of these kinds of hybrid quantum-classical programs. Essentially, the Qafny's encoding of the density operators for quantum measurements is to model them as array filter operations with the support of Dafny's classical probability distribution library. If the library is powerful enough, the Qafny's proof system can perform proof automation on questioning properties related to probability bounds such as the one above.

B OQASM: AN ASSEMBLY LANGUAGE FOR QUANTUM ORACLES
The oqasm expression used in Figure 7 places an additional wrapper on top of the oqasm expression given in Figure 35. Here, we first provide a step-by-step explanation of oqasm; then show the additional wrapper in Appendix B.4.
oqasm is designed to express efficient quantum oracles that can be easily tested and, if desired, proved correct. oqasm operations leverage both the standard computational basis and an alternative basis connected by the quantum Fourier transform (QFT). oqasm's type system tracks the bases of variables in oqasm programs, forbidding operations that would introduce entanglement. oqasm states are therefore efficiently represented, so programs can be effectively tested and are simpler to verify and analyze. In addition, oqasm uses virtual qubits to support position shifting operations, which support arithmetic operations without introducing extra gates during translation. All of these features are novel to quantum assembly languages.
This section presents oqasm states and the language's syntax, semantics, typing, and soundness results. As a running example, the QFT adder [3] is shown in Figure 33. The Coq function rz_adder generates an oqasm program that adds two natural numbers a and b, each of length n qubits.

B.1 oqasm States
An oqasm program state is represented according to the grammar in Figure 34. A state of qubits is a length-tuple of qubit values ; the state models the tensor product of those values. This means that the size of is ( ) where is the number of qubits. A -qubit state in a language like sqir is represented as a length 2 vector of complex numbers, which is (2 ) in the number of qubits. Our linear state representation is possible because applying for any well-typed oqasm program on any well-formed oqasm state never causes qubits to be entangled.
A qubit value has one of two forms , scaled by a global phase ( ). The two forms depend on the basis that the qubit is in-it could be either Nor or Phi. A Nor qubit has form | ⟩ (where ∈ {0, 1}), which is a computational basis value. A Phi qubit has the form |Φ( )⟩ = 1 √ 2 (|0⟩ + ( ) |1⟩), which is a value of the (A)QFT basis. The number in Phi indicates the precision of the state . As shown by Beauregard [3], arithmetic on the computational basis can sometimes be more efficiently carried out on the QFT basis, which leads to the use of quantum operations (like QFT) when implementing circuits with classical input/output behavior.
B.2 oqasm Syntax, Typing, and Semantics Figure 35 presents oqasm's syntax. An oqasm program consists of a sequence of instructions . Each instruction applies an operator to either a variable , representing a group of qubits, or a position , which identifies a particular offset into a variable .
The instructions in the first row correspond to simple single-qubit quantum gates-ID , X , and RZ [−1] -and instruction sequencing. The instructions in the next row apply to whole variables: QFT applies the AQFT to variable with -bit precision and QFT −1 applies its inverse. If is equal to the size of , then the AQFT operation is exact. SR [−1] applies a series  Fig. 36. SR unfolds to a series of RZ instructions of RZ gates ( Figure 36). Operation CU applies instruction controlled on qubit position . All of the operations in this row-SR, QFT, and CU-will be translated to multiple sqir gates. Function rz_adder in Figure 33(b) uses many of these instructions; e.g., it uses QFT and QFT −1 and applies CU to the th position of variable a to control instruction SR m b.
In the last row of Figure 35, instructions Lshift , Rshift , and Rev are position shifting operations. Assuming that has qubits and represents the -th qubit state in , Lshift changes the -th qubit state to ( +1)% , Rshift changes it to ( + −1)% , and Rev changes it to −1− . In our implementation, shifting is virtual, not physical. The oqasm translator maintains a logical map of variables/positions to concrete qubits and ensures that shifting operations are no-ops, introducing no extra gates.
Other quantum operations could be added to oqasm to allow reasoning about a larger class of quantum programs while still guaranteeing a lack of entanglement.
Typing. In oqasm, typing is concerning a type environment Ω and a predefined size environment Σ, which map oqasm variables to their basis and size (number of qubits), respectively. The typing judgment is written Σ; Ω ⊢ ⊲ Ω ′ which states that is well-typed under Ω and Σ, and transforms the variables' bases to be as in Ω ′ (Σ is unchanged). Σ is fixed because the number of qubits in execution is always fixed. It is generated in the high-level language compiler, such as Oqimp in [23]. The algorithm generates Σ by taking an Oqimp program and scanning through all the variable initialization statements. Select type rules are given in Figure 37; the rules not shown (for ID, Rshift, Rev, RZ −1 , and SR −1 ) are similar.

Fig. 39. oqasm semantics
The type system enforces three invariants. First, it enforces that instructions are well-formed, meaning that gates are applied to valid qubit positions (the second premise in X) and that any control qubit is distinct from the target(s) (the fresh premise in CU). This latter property enforces the quantum no-cloning rule. For example, applying the CU in rz_adder' (Figure 33) is valid because position a,m is distinct from variable b.
Second, the type system enforces that instructions leave affected qubits on a proper basis (thereby avoiding entanglement). The rules implement the state machine shown in Figure 38. For example, QFT transforms a variable from Nor to Phi (rule QFT), while QFT −1 transforms it from Phi back to Nor (rule RQFT). Position shifting operations are disallowed on variables in the Phi basis because the qubits that makeup are internally related (see Definition B.1) and cannot be rearranged. Indeed, applying a Lshift and then a QFT −1 on in Phi would entangle 's qubits.
Third, the type system enforces that the effect of position-shifting operations can be statically tracked. The neutral condition of CU requires that any shifting within is restored by the time it completes. For example, CU (Lshift ) ; X ( , 0) is not well-typed because knowing the final physical position of qubit ( , 0) would require statically knowing the value of . On the other hand, the program CU (Lshift ; X ( , 0) ; Rshift ) ; X ( , 0) is well-typed because the effect of the Lshift is "undone" by an Rshift inside the body of the CU.
Semantics. The semantics of an oqasm program is a partial function ⟦⟧ from an instruction and input state to an output state ′ , written ⟦ ⟧ = ′ , shown in Figure 39.
Recall that a state is a tuple of qubit values, modeling the tensor product 1 ⊗ · · · ⊗ . The rules implicitly map each variable to a range of qubits in the state, e.g., ( ) corresponds to some sub-state ⊗ · · · ⊗ + −1 where Σ( ) = . Many of the rules in Figure 39 update a portion of a state. [( , ) ↦ → ( , ) ] updates the -th qubit of variable to be the (single-qubit) state ( , ) , and [ ↦ → ] to update variable according to the qubit tuple . [( , ) ↦ → ↑ ( , ) ] and [ ↦ → ↑ ] are similar, except that they also accumulate the previous global phase of ( , ) (or ( )). ↓ is to convert a qubit ( ) to an unphased qubit . Function xg updates the state of a single qubit according to the rules for the standard quantum gate . cu is a conditional operation depending on the Nor-basis qubit ( , ). RZ (or RZ −1 ) is an z-axis phase rotation operation. Since it applies to Nor-basis, it applies a global phase. By Theorem B.4, when it is compiled to sqir, the global phase might be turned into a local one. For example, to prepare the state 2 =0 (− ) | ⟩ [5], a series of Hadamard gates are applied, followed by several controlled-RZ gates on , where the controlled-RZ gates are definable by oqasm. SR (or SR −1 ) applies an + 1 series of RZ (or RZ −1 ) rotations where the -th rotation applies a phase of ( 1 2 − +1 ) (or (− 1 2 − +1 )). qt applies an approximate quantum Fourier transform; | ⟩ is an abbreviation of | 1 ⟩ ⊗ · · · ⊗ | ⟩ (assuming Σ( ) = ) and is the degree of approximation. If = , then the operation is the standard QFT. Otherwise, each qubit in the state is mapped to |Φ( 2 − )⟩, which is equal to 1 for any natural number ). qt −1 is the inverse function of qt. Note that the input state to qt −1 is guaranteed to have the form −1 =0 (|Φ( 2 − )⟩) because it has type Phi . pm , pm , and pm are the semantics for Lshift, Rshift, and Rev, respectively.

B.3 oqasm Metatheory
Soundness. The following statement is proved: well-typed oqasm programs are well-defined; i.e., the type system is sound concerning the semantics. Below is the well-formedness of an oqasm state.
• For every ∈ Ω such that Ω( ) = Phi and ≤ Σ( ), there exists a value such that for every < Σ( ), ( , ) has the form ( ) |Φ( 2 − )⟩. 17 Type soundness is stated as follows; the proof is by induction on and is mechanized in Coq.
Algebra. Mathematically, the set of well-formed -qubit oqasm states for a given Ω can be interpreted as a subset S of a 2 -dimensional Hilbert space H , 18 and the semantics function ⟦⟧ can be interpreted as a 2 × 2 unitary matrix, as is standard when representing the semantics of programs without measurement [14]. Because oqasm's semantics can be viewed as a unitary matrix, correctness properties extend by linearity from S to H -an oracle that performs addition for classical Nor inputs will also perform addition over a superposition of Nor inputs. The following statement is proved: S is closed under well-typed oqasm programs.
Given a qubit size map Σ and type environment Ω, the set of oqasm programs that are well-typed concerning Σ and Ω (i.e., Σ; Ω ⊢ ⊲ Ω ′ ) form an algebraic structure  If for every ∈ [0, 2 ), ⟦ ⟧ | ⟩ = | ′ ⟩, then ⟦ ⟧( 2 −1 =0 | ⟩) = 2 −1 =0 | ′ ⟩. The following theorems are proved as corollaries of the compilation correctness theorem from oqasm to sqir ( [23]). Theorem B.3 suggests that the space S is closed under the application of any well-typed oqasm operation. Theorem B.4 says that oqasm oracles can be safely applied to superpositions over classical states. 19 oqasm programs are easily invertible, as shown by the rules in Figure 40. This inversion operation is useful for constructing quantum oracles; for example, the core logic in the QFT-based subtraction circuit is just the inverse of the core logic in the addition circuit ( Figure 40). This allows us to reuse the proof of addition in the proof of subtraction. The inversion function satisfies the following properties: Theorem B.5. [Type reversibility] For any well-typed program , such that Σ; Ω ⊢ ⊲ Ω ′ , its inverse ′ , where inv − − → ′ , is also well-typed and Σ; Ω ′ ⊢ ′ ⊲ Ω. Moreover, ⟦ ; ′ ⟧ = .

B.4 Explaining the Oracle Expression in Qafny
The oqasm expression used in Figure 7 places an additional wrapper on top of the oqasm expression given in Figure 35. The wrapper is given as: Here is a list of positions, and is an oqasm instruction in Figure 35. Here, we require that all qubit positions mentioned in must be in . Ranges and sessions are directly related to positions. Given a range [ , ), it is equal to a list of positions: ( , ), ( , +1), ..., ( , -1), while a session is a list of disjoint ranges and it can be understood as concatenations of different ranges in the session. For simplicity, we can understand the above definition as . by rearranging the positions as a session. In the predicate (Ω, ) = in rule TA-CH in Figure 8, function (Ω, ) returns , which means that the lambda expression is given as . . Given a expression as . , to evaluate an oracle expression ′ ← − , we actually do the following: Here, we first replace the positions in with qubits mentioned in session ′ and then evaluate the expression [ ′ / ]. In the paper, we also utilize some oracle expressions from OQIMP [23], the arithmetic operation language based on oqasm. The expression [0, ) ← − [0, )+1 is actually a syntactic sugar for the expression: [0, ) ← − ( [0, ). ← − +1). Here, the expression ← − +1 is an OQIMP expression, meaning that we apply the function . + 1 to a qubit array , where is a -length qubit array. In addition, the expression [0, ) ← − 2 [0, ) % is a syntactic sugar for the expression: [0, ) ← − ( [0, ). ← − 2 % ).
Sometimes, in OQIMP, we will need additional ancillary qubits to guarantee that an arithmetic operation is reversible, a requirement in quantum oracle computation. For example, if we want to express a modulo expression in OQIMP, we need to write { [0, ), [0, )}. ← − ( % , ), meaning that and are -length qubit array. we compute the modulo operation % and put the result in , while is an additional ancillary qubits required for the computation. Then, the oracle operation for the modulo function in Qafny is written as: In Qafny, the expression computes % and then assigns the value to the range [0, ), while is an array of additional ancillary qubits required for the computation. In the Shor's example in Appendix A.7, the oracle application ( [0, ) ← − 2 [0, ) % ) requires hidden ancillary qubits, but builtin reversed circuits will clean up those qubits in the modulo multiplication itself, i.e., before the modulo multiplication function ends, all ancillary qubits are reversed to their initial values |0⟩. In all oracle examples in the paper, either they do not have ancillary qubits, or they only have hidden ones that will be cleaned up before the oracle execution ends. Thus, Qafny treats them as nonexistence and leaves them for oqasm to handle.