and MooreRoşu et al2013]
authorpersonGrigore Roşu, personAndrei
Ştefănescu, personŞtefan Ciobâcă, and
personBrandon M. Moore. year2013.
One-Path Reachability Logic. In
booktitleProceedings of the 28th Symposium on Logic in
Computer Science (LICS'13). publisherIEEE,

[Sammler, Lepigre, Krebbers, Memarian, Dreyer,
and GargSammler et al2021]
authorpersonMichael Sammler, personRodolphe
Lepigre, personRobbert Krebbers, personKayvan
Memarian, personDerek Dreyer, and personDeepak
Garg. year2021.
RefinedC: Automating the Foundational Verification
of C Code with Refined Ownership Types. In
booktitleProceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation (Virtual,
Canada) (seriesPLDI 2021). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

authorpersonP.W. Shor.
Algorithms for quantum computation: discrete
logarithms and factoring. In booktitleProceedings 35th
Annual Symposium on Foundations of Computer Science.

authorpersonP. W. Shor.
Algorithms for quantum computation: Discrete
logarithms and factoring. In booktitleProceedings 35th
Annual Symposium on Foundations of Computer Science
(seriesFOCS '94).

[Ta, Le, Khoo, and ChinTa
et al2016]
authorpersonQuang-Trung Ta, personTon Chanh
Le, personSiau-Cheng Khoo, and personWei-Ngan
Chin. year2016.
titleAutomated Mutual Explicit Induction Proof in
Separation Logic.

[Tatsuta, Chin, and Al AmeenTatsuta
et al2019]
authorpersonMakoto Tatsuta, personWei-Ngan
Chin, and personMahmudul Faisal Al Ameen.
Completeness and expressiveness of pointer program
verification by separation logic.
journalInformation and Computation
volume267 (year2019), pages1–27.

authorpersonDominique Unruh.
Quantum Relational Hoare Logic.
journalProc. ACM Program. Lang.
volume3, numberPOPL, Article articleno33
(datejan year2019), numpages31 pages.

authorpersonSalvador Elías Venegas-Andraca.
Quantum walks: a comprehensive review.
journalQuantum Information Processing
volume11, number5 (datejul
year2012), pages1015–1106.

authorpersonThomas G. Wong.
Unstructured search by random and quantum walk.
journalQuantum Information and Computation
volume22, number1&2 (datejan
year2022), pages53–85.

[Yang and O'HearnYang and O'Hearn2002]
authorpersonHongseok Yang and personPeter
O'Hearn. year2002.
A Semantic Basis for Local Reasoning. In
booktitleFoundations of Software Science and Computation
Structures, editorpersonMogens Nielsen and
personUffe Engberg (Eds.). publisherSpringer Berlin
Heidelberg, addressBerlin, Heidelberg,

authorpersonMingsheng Ying.
Floyd–Hoare Logic for Quantum Programs.
journalACM Trans. Program. Lang. Syst.
volume33, number6, Article articleno19
(dateJan. year2012), numpages49 pages.

authorpersonMingsheng Ying.
Toward Automatic Verification of Quantum Programs.
journalForm. Asp. Comput. volume31,
number1 (datefeb year2019),

authorpersonBohua Zhan.
Efficient Verification of Imperative Programs Using
Auto2. In booktitleTools and Algorithms for the
Construction and Analysis of Systems,
editorpersonDirk Beyer and personMarieke
Huisman (Eds.). publisherSpringer International Publishing,
addressCham, pages23–40.

[Zhou, Barthe, Hsu, Ying, and YuZhou
et al2021]
authorpersonLi Zhou, personGilles Barthe,
personJustin Hsu, personMingsheng Ying, and
personNengkun Yu. year2021.
A Quantum Interpretation of Bunched Logic and
Quantum Separation Logic. In booktitleProceedings of the
36th Annual ACM/IEEE Symposium on Logic in Computer Science (Rome, Italy)
(seriesLICS '21). publisherAssociation for
Computing Machinery, addressNew York, NY, USA, Article
articleno75, numpages14 pages.

[Zhou, Barthe, Strub, Liu, and YingZhou
et al2023]
authorpersonLi Zhou, personGilles Barthe,
personPierre-Yves Strub, personJunyi Liu, and
personMingsheng Ying. year2023.
CoqQ: Foundational Verification of Quantum
journalProc. ACM Program. Lang.
volume7, numberPOPL, Article articleno29
(datejan year2023), numpages33 pages.

§ KIND CHECKING, $FV$ FUNCTION, AND LOCUS GENERATION

[ ]Ω(x)=∨Ω(x)=Ω⊢x : Ω(x)

[ ]Ω(x)=n
0 ≤i ≤j ≤nΩ⊢x : xij

[ ] Ω⊢a_1 : q_1
Ω⊢a_2 : q_2 Ω⊢a_1    a_2 : q_1 ⊔q_2

[ ] Ω⊢a_1 : q_1
Ω⊢a_2 : q_2 Ω⊢a_1 ·a_2 : q_1 ⊔q_2

[ ] Ω⊢a_1 : q_1
Ω⊢a_2 : q_2
Ω⊢x[n] : q_3  Ω⊢a_1=a_2x[n] : q_1 ⊔q_2⊔q_3

[ ] Ω⊢a_1 : q_1
Ω⊢a_2 : q_2
Ω⊢x[n] : q_3  Ω⊢a_1<a_2x[n] : q_1 ⊔q_2⊔q_3

[ ] Ω⊢b : qΩ⊢b : q

[ ] Ω⊢e : ζ_2 ⊔ζ_1 Ω⊢e : ζ_1 ⊔ζ_2

\[
\begin{array}{l}
g \sqcup \kappa = \kappa
\qquad
\cmode \sqcup \mmode = \mmode
\qquad
g \sqcup g = g
\qquad
\kappa \sqcup \kappa' = \kappa\sqcupplus\kappa'
\end{array}
\]

Arith and Bool Kind Checking

The $FV(\Omega,-)$ function calculation is based on the kind checking procedure $\Omega\vdash - : (g_k,\kappa)$.
When the term $-$ is a $\cmode$ or $\mmode$ kind term, the output is $(g,\emptyset)$, while if the term $-$ is a quantum value with kind $\qmode{n}$, the output is $(\qmode{n},\kappa)$, where $\kappa$ contains all qubits mentioned in the term $-$ and its length $\slen{\kappa}=n$. As an abbreviation, we can think of the kind checking procedure has the form $\Omega\vdash - : g_k$ when the term $-$ is $\cmode$ or $\mmode$, while it has the form $\Omega\vdash - : \kappa$ when the term $-$ is of kind $\qmodename$.

<Ref> provides the kind check rules for arithmetic and Boolean expressions.
Here, we enforce a partial order over variable kinds as $\cmode \le \mmode \le \qmodename$,
such that the kind of an expression depends on the most general variable kind in the expression.
When two $\qmodename$ variables meet, their locus $\kappa$ and $\kappa'$ cannot be overlapped, as we enforce the disjoint union property $\kappa\sqcupplus\kappa'$, because quantum expressions are reversible. For any arithmetic operation, if the two parts of an expression, such as $q_1$ and $q_2$, is an addition $q_1 \splus q_2$, have overlapped locus fragments, the reversibility fails.
In the Boolean guards $\qbool{a_1}{=}{a_2}{x[n]}$ and $\qbool{a_1}{<}{a_2}{x[n]}$, the index appearing in quantum array $x$ must be a $\cmode$-kind value,
so the type system simplifies the expression to a natural number $n$ in the compilation time, which is why we use the value $n$ instead of an expression $a_3$ in the guards.

The $FV(\Omega,-)$ function produces a locus in the term $-$, similar to computing free variables in a term.
Based on the kind checking procedure, the $FV$ calculation is defined as follows:

$\Omega\vdash - :  \kappa \Rightarrow FV(\Omega,-) = \kappa$

The construct $-$ here refers to arithmetic, Boolean equations, or a statement.

§ WELL-FORMED AND WELL-TYPED DEFINITIONS

The kind checking procedure $\Omega\vdash - : (g_k,\kappa)$ in <Ref> is essentially a well-formedness restriction that we place on the term $-$. There are two additional well-formed and well-typed restrictions in our type and proof systems.

The domain of a environment $\sigma$ (or state $\varphi$) is well-formed, written as
$\Omega \vdash \dom{\sigma}$ (or $\dom{\varphi}$), iff for every locus $\kappa\in \dom{\sigma}$ (or $\dom{\varphi}$):

* $\kappa$ is disjoint unioned, i.e., for every two ranges $x\srange{i}{j}$ and $y\srange{i'}{j'}$, $x\srange{i}{j}\cap y\srange{i'}{j'}=\emptyset$.

* For every range $x\srange{i}{j}\in\kappa$, $\Omega(x)=\qmode{n}$ and $[i,j) \subseteq [0,n)$.

A predicate $P$ is well-formed, written as $\Omega;\sigma \vdash P$, iff every variable and locus appearing in $P$ is defined in $\Omega$ and $\sigma$, respectively; particularly, if $P=\kappa \mapsto q * P'$, $\kappa \in \dom{\sigma}$.

§ SMALL-STEP SEMANTICS

[S-ExpC]   (ψ,φ,xne) ⟶(ψ,φ,e[n/x])

(ψ,φ⊎{κκ':  q},κ∘) ⟶(ψ,φ⊎{κκ': ∘^κq},{})

[S-ExpM]   (ψ,φ,x(r,n)e) ⟶(ψ[x↦(r,n)],φ,e)

[S-If]  FV(Ω,x[n])=κ
(ψ,φ⊎{κ': S^κ(qκ,x[n])},e)
⟶(ψ',φ⊎{κ': q'},e')
(ψ,φ⊎{κκ' : qκ,x[n]+qκ,x[n]},x[n]e) ⟶(ψ',φ⊎{ κκ' : P(q')+qκ,x[n]},x[n]e')

[S-Ifb]  FV(Ω,b @ x[n])=κ
(ψ,φ⊎{κκ' : q},b @ x[n]e) ⟶(ψ',φ⊎{κκ': b @ x[n]^κq},x[n]e)

[S-Loop] n < n'
b' = b[n_1/j]
e' = e[n_1/j]
(ψ,φ,jnn'b{e}) ⟶(ψ,φ,b'e'jn1n'b{e})
(ψ,φ,{}e_2) ⟶(ψ,φ,e_2)

[S-Mea]κ=y0n   r= ∑_j z_j^2 (ψ,φ⊎{κκ': ∑_j z_j|c⟩η_j+qκ,c ≠κ},xye) ⟶(ψ[x↦(r,c)],φ⊎{κ' :   ∑_j z_j/√(r)η_j},e)

[S-Seq2](ψ,φ,e_1) ⟶(ψ',φ',e'_1)
(ψ,φ,e_1e_2) ⟶(ψ',φ',e'_1e_2)

\begin{array}{lclcl}
\denote{\circ}^{n}(\sum_{j}{z_j\ket{c_j}\eta_j})
\sum_{j}{z_j(\denote{\circ}\ket{c_j})\eta_j} & \texttt{where}& (\circ = \mu\vee \circ = op) \wedge \forall j\,\slen{c_j}=n
\\[0.2em]
\qfun{(\sum_{i}{z_i}{\ket{c_{i}}}{\eta_i}+q)}{\kappa,b} &\triangleq& \sum_{i}{z_i}{\ket{c_{i}}}{\eta_i}
&\texttt{where}&\forall i.\,\slen{c_{i}}=\slen{\kappa}\wedge \denote{b[c_{i}/\kappa]}=\texttt{true}
\\[0.2em]
S^n(\sum_{j}{z_j\ket{c_j}\beta_j\tos{\beta'_j}}) &\triangleq& \sum_{j}{z_j\beta_j\tos{\ket{c_j}\beta'_j}} &\texttt{where}&\forall j\,\slen{c_j}=n
\\[0.2em]
P(\sum_{j}{z_j\beta_j\tos{\ket{c_j}\beta'_j}}) &\triangleq& \sum_{j}{z_j\ket{c_j}\beta_j\tos{\beta'_j}}
\end{array}

Selected small-step semantic rules. $\tov{c}$ turns basis $c$ to an integer.

Here, we show an alternative small-step transition semantics
$(\psi,\varphi,e) \longrightarrow (\psi',\varphi',e')$, with $\psi$ / $\psi'$ being local classical variable states mapping from variables to $(r,n)$, and $\varphi$ / $\varphi'$ being global quantum states in <Ref>.
The judgment states that a program $s$ with the pre-states $\psi$ and $\varphi$ is transitioned to a post-state $(\psi',\varphi',e')$, with the post-state program $e'$, shown in <Ref>.

Conditional Analogy

Measurement Analogy

Assignment Operations
Rules S-ExpC and S-ExpM define the behaviors for $\cmode$ and $\mmode$ kind classical variable assignments, respectively.
Rule S-OP defines the quantum heap mutation for applying a Hadamard gate ($\ihadh$) and an oracle expression ($\mu$) on a locus $\kappa$, respectively.
Here, we assume that the $\tcht$-typed value, for the locus containing $\kappa$, is transformed to the form $\kappa \sqcupplus \kappa'$ putting $\kappa$ in the beginning, possibly through equivalence rewrites described in <Ref>.
The operation's semantic function $\denote{\circ}^{n}$, $\circ$ being $\ihadh$ or $\mu$, is applied on the first $n$ basis bits of each basis-ket in the value of locus $\kappa \sqcupplus \kappa'$, which refers to the $\kappa$ portion because its length is $n$.

below might need to go.
There are two special features of an $\ihadh$ application.
First, different locations of the application might serve different operational meanings.
When it appears at the beginning of a program whose state is of type $\tnort$,
such as in <Ref>, it acts as a state preparation operation to prepare a superposition state, as the $\thadt$ type state in <Ref>.
On the contrary, it serves as an amplitude amplifier inside a quantum conditional to increase the amplitudes of some target basis-kets when we apply it to an $\tcht$ typed state, such as in <Ref>.
In Qafny, we realize the difference by designing different semantic and proof rules for handling $\ihadh$ gate applications in different circumstances, shown in <Ref>.
Second, while oracle applications do not modify $\tcht$ typed state basis-ket size, $\ihadh$ applications increase the size.
For example, if we apply a $\ihadh$ gate to $\kappa_2$'s first basis position P-Oracle in <Ref>,
the state becomes $\textcolor{spec}{\frac{1}{2}\ket{0}\ket{\overline{1}}}\textcolor{stack}{\cmsg{\ket{1}}}\textcolor{spec}{+\frac{1}{2}\ket{1}\ket{\overline{1}}}\textcolor{stack}{\cmsg{\ket{1}}}$.
In the Qafny proof system implementation [It is not a problem in the Qafny formalism.], we interpret quantum states as arrays indexed by basis-kets;
it is necessary to combine the same basis-kets, i.e., if two basis-kets $zw$ and $z'w$ have the same basis $w$, we replace them with a new element $(z\texttt{+}z')w$.
In <Ref>, we introduce implementation-level optimizations based on different operation functionality to make the combination procedure more effective.

Quantum Conditionals
Rule S-If describes the quantum conditional semantics, analogized in <Ref>,
while rule S-Ifb evaluates the side-effect in the Boolean guard onto the quantum state.
The difference between the small step and the big-step S-If in <Ref> is that the small step version transitions a single step in $e$.

Quantum Measurement
A measurement $\sexp{x}{\smea{y}}{e}$ collapses a qubit array $y$,
binds a $\mmode$-kind outcome to $x$ and restricts its usage in \(e\).
<Ref> shows an analogy of the partial measurement behavior (semantic rule S-Mea in <Ref>) [A complete measurement is a special case of a partial measurement when $\kappa'$ is empty in S-Mea].
In this small step version, the measurement expression is transitioned to the evaluation of evaluating the following expression $e$.

§ FULL DEFINITION AND MORE EXAMPLES

Here, we provide the details of the language and proof system, with more examples.

§.§ Full Syntax

\[\begin{array}{llcl}
\text{\oqasm Expr} & \mu\\
\text{Arith Expr} & a & ::= & x \mid v \mid a \,\splus\, a \mid a \cdot a \mid ... \\
\text{Bool Expr} & b & ::= & x[a] \mid \qbool{a_1}{=}{a_2}{\textcolor{red}{x[a]}} \mid \qbool{a_1}{<}{a_2}{\textcolor{red}{x[a]}} \mid ... \\
\text{Predicate Locus} & \Kappa & ::= & \kappa \mid \mea(x,n,\kappa) \mid \frz(b,\kappa,\kappa) \mid \ufrz(b,\kappa,\kappa)\\
\text{Predicate} & P,Q,R & ::= & a_1 = a_2 \mid a_1 < a_2 \mid \Kappa \mapsto q \mid P \wedge P \mid P * P \mid ... \\
\text{Gate Expr} & op & ::= & \texttt{H} \mid \iqft[\lbrack -1 \rbrack]{}{} \\
\text{C/M Kind Expr}& am & ::= & a \mid \smea{y} \\
\text{Statement} & e & ::= & \sskip \mid \sexp{x}{am}{e} \mid  \ssassign{\kappa}{}{op} \mid \ssassign{\kappa}{}{\mu}
\\ & & \mid & \sseq{e}{e} \mid \sifq{b}{e} \mid
\sqwhile{j}{a_1}{a_2}{b}{\{e\}}
\\ & & \textcolor{red}{\mid} & \textcolor{red}{\sifb{b}{e}{e}\mid\ssassign{\kappa}{}{\sdis} \mid \ssassign{\kappa}{}{\sreduce{c}{n}}}
\end{array}
\]

Full Syntax

<Ref> provides the syntax definition with extended constructs.
In the Boolean guard syntax, the marked red parts can be omitted if the expressions do not contain any quantum variables, e.g., if variables $x$ and $y$ in expression $x=y$ are classical, we do not need an additional field after it to store the Boolean result.
The marked red part in a statement syntax contains three additional operations.
$\sifb{b}{e}{e}$ is a classical conditional operation, where $b$ has kind $\cmode$ or $\mmode$.
A quantum diffusion operation $\ssassign{\kappa}{}{\sdis}$ manipulates the amplitude of basis-kets of a locus containing \(\kappa\).
$\ssassign{\kappa}{}{\sreduce{c}{n}}$ is a quantum amplification operation that multiplies the basis-ket $\ket{c}$ in $\kappa$ with an amplitude $\frac{1}{\sqrt[4]{2^n}}$ and any other basis-kets with an amplitude $\sqrt{1-\frac{1}{\sqrt{2^n}}}$. Essentially, it reduces the amplitude volume in the basis-ket $\ket{c}$ while keeping the amplitudes of other basis-kets.

§.§ Additional Semantic Rules

(φ',e)⇓φ”(φ,e) ⇓φ”

[SH-Nor] (φ⊎{κ: |c⟩},κ) ⇓φ⊎{κ: 2^κκ1α(1/2^c[j])}

(r_j≥1/2⇒c[j]=1) ∨(r_j<1/2⇒c[j]=0) (φ⊎{κ: 2^nn1α(r_j)},κ) ⇓φ⊎{κ: |c⟩}

[S-IfT]  (φ,e_1)⇓φ'
(φ,truee_1e_2) ⇓φ'

[S-IfF]  (φ,e_2)⇓φ'
(φ,falsee_1e_2) ⇓φ'

(φ⊎{κκ': q},κ) ⇓φ⊎{κκ' : D(κ,q)}

(φ⊎{κκ': q},κcn) ⇓φ⊎{κκ' : A(κ,q)}

\begin{array}{l}
\forall u\in [0, 2^t).\, \tob{u}=c\Rightarrow z_{cu}=\frac{1}{\sqrt[4]{2^n}} \wedge \tob{u}\neq c\Rightarrow z_{cu}=\sqrt{1-\frac{1}{\sqrt{2^n}}}
\\[0.2em]
\begin{array}{l@{~}c@{~}l}
\mathpzc{D}(n,\Msum_{i=0}^{m}\scha{2^{n}\sminus 1}{z_{ij}}{j}{\ket{c_{ij}}}) &\triangleq&
\Msum_{i=0}^{m}\scha{2^n}{(\frac{1}{2^{n-1}}\sum_{u=0}^{2^n\sminus 1}z_{iu} - z_{ij})}{j}{\ket{c_{ij}}}
\\[0.2em]
\mathpzc{A}(n,\Msum_{i=0}^{m}\scha{2^{t}\sminus 1}{z_{ij}}{j}{\ket{c_{ij}}})&\triangleq& \Msum_{i=0}^{m}\scha{2^t\sminus 1}{(\frac{1}{2^{t-1}}\sum_{u=0}^{2^t\sminus 1}z_{cu}\cdot z_{iu} - z_{cj}\cdot z_{ij})}{j}{\ket{c_{ij}}}
\end{array}
\end{array}

Additional big-step semantic rules. $c[j]$ gets the $j$-th bit in the bitstring $c$. $\tob{u}$ turns an integer $u$ to a bitstring as basis.

Here, we describe additional big-step semantics of the ones in <Ref>.
The rules are given in <Ref>.
Rule SH-Nor describes the semantics for an $\cn{H}$ gate when its applicant state value is of $\tnort$ type,
while rule SH-Had deals with the case when the applicant state value is of $\thadt$ type.
These two rules show any example semantic rules for defining the behaviors of state preparation and oracle operations when their applicant state types are not $\tcht$ type.
The rules for the other state preparation and oracle operations are defined in the same manner.
One thing worth noting is that any $\tnort$ or $\thadt$ type value can be rewritten to an $\tcht$ type value,
so these rules for $\tnort$ or $\thadt$ type values are equivalent shortcuts of the rules for $\tcht$ type values.

Rules S-IfT and S-IfF describe the semantics for classical conditional. Since the big-step semantics utilize a substitution-based approach for dealing with classical variables, the Boolean guards should have been freed of variables at the time when they are being evaluated; thus, they can be simplified as either $\cn{true}$ or $\cn{false}$.
Rules S-Dis and S-Red describe the semantics of amplitude diffusion and amplification operations, which are explained in <Ref>.

§.§ Additional Typing Rules and Equivalence Relations

[T-Skip]Ω;σ⊢_g ▹σ

[TH-Nor]Ω;σ⊎{κ:} ⊢_g κop ▹σ⊎{κ:}

[TH-Had]Ω;σ⊎{κ:} ⊢_g κ ▹σ⊎{κ:}

[T-IfC]Ω⊢b : g

Ω;σ⊢_g' e_1 ▹σ'
Ω;σ⊢_g' e_2 ▹σ'
Ω;σ⊢_g be_1e_2 ▹σ'

[T-Dis]Ω,σ⊎{κκ':} ⊢_g κ ▹σ⊎{κκ':}

[T-Red]Ω,σ⊎{κκ':} ⊢_g κcn ▹σ⊎{κκ':}

Additional type rules

\[
\begin{array}{l@{~}cl}
\tau & \sqsubseteq & \tau \\[0.3em]
\tnort &\sqsubseteq& \tcht\\[1.3em]
\thadt &\sqsubseteq& \tcht
\end{array}
\]

\[
\begin{array}{l@{~}cl}
q & \equiv_{\slen{q}} & q \\[0.3em]
\ket{c} &\equiv_n& \sch{0}{ }{\ket{c}}\\[0.5em]
\shad{2^n}{n\sminus 1}{\alpha(r_j)} &\equiv_n& \sch{2^n\sminus 1}{\frac{\alpha(\sum_{k=0}^{n\sminus 1} r_k \cdot \tob{j}[k])}{\sqrt{2^n}}}{\ket{j}}
\end{array}
\]

Quantum Value Equivalence

\[
\begin{array}{l @{~} c @{~} l l@{~}c @{~} l l @{~}c @{~} l l @ {~} c @{~} l}
\kappa &\equiv & \kappa
\qquad
x[n,n) & \equiv & \emptyset
\qquad
\emptyset \sqcupplus \kappa & \equiv & \kappa
\qquad
x[n,m)\sqcupplus\kappa & \equiv & x[n,j)\sqcupplus x[j,m) \sqcupplus\kappa
\\
\texttt{where}\;\;n \le j < m

\end{array}
\]

locus Equivalence

type/state relations.

<Ref> provides additional type rules.
Rule T-Skip defines the identity type rule for $\texttt{SKIP}$ operations.
Rules TH-Nor and TH-Had to track the types for Hadamard $\cn{H}$ state preparation operations with the applicant types to be $\tnort$ and $\thadt$ type values.
Rule T-IfC defines the behaviors for classical conditionals with $b$ being of kind $\cmode$ or $\mmode$.
We require that the two different branches $e_1$ and $e_2$ output the same type of judgment ($\sigma'$).
Rules T-Dis and T-Red types the amplitude diffusion and amplification operations.
We require the input and output types for $\kappa$, as a locus fragment of $\kappa\sqcupplus\kappa'$, have the type $\tcht$.

As we suggested in <Ref>, utilizes type environment and quantum state equations to rewrite loci 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 circuits. In <Ref>, 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 <Ref>, we sometimes need quantum loci to be split and regrouped. All these properties are formulated in as equational properties in <Ref> that rely on locus 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 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 to track the uses, split, and join of loci, as well as the three value types in every transition step so that the system knows how to apply an equation.

[PH-Nor]Ω{κ: }gκ↦|c⟩κκ↦2^κκ1α(1/2^c[j])

(r_j≥1/2⇒c[j]=1) ∨(r_j<1/2⇒c[j]=0)
Ω{κ: }gκ↦2^nn1α(r_j)κκ↦|c⟩

[P-ExpM]Ω⊢a :

Ω{κκ':}gκκ'↦qκ κκ'↦D(κ,q)

[P-Loop1] n ≥n'
Ω{κκ':}gκκ'↦qκcn κκ'↦A(κ,q)

Additional Proof Rules

<Ref> shows the equivalence relations on types and values.
<Ref> shows the subtyping relation such that $\tnort$ and $\thadt$ subtype to $\tcht$.
Correspondingly, the subtype of $\tnort$ to $\tcht$ represents the first line equation in <Ref>, where a $\tnort$-typed value is converted to an $\tcht$ typed value. Similarly, a $\thadt$-typed value can be converted to an $\tcht$ value in the second line.
Additionally, <Ref> defines the equivalence relations for the locus concatenation operation $\sqcupplus$: associative, identified with the identity empty locus element $\emptyset$.
We also view a range $x[n,n)$ to be empty ($\emptyset$), and a range $x[n,m]$ can be split into two ranges in the locus as $x[n,j) \uplus x[j,m)$.

§.§ Additional Proof Rules

<Ref> provides additional proof rules.
Rule P-Skip shows the proof rule for a  operation.
Rules PH-Nor and PH-Had are proof rules for the $\texttt{H}$ state preparation operation with its value being of $\tnort$ and $\thadt$ typed values. As mentioned above, rules for state preparation operations with states other than $\tcht$ type are shortcuts for our automated verification tool.

Rule P-ExpM describes the proof rule for a let-binding with $\mmode$-kind variable, which introduces an invariant property of the statement, where $x$ is assigned to an invariant value ($x=a$) along $e$'s evaluation, and the invariant is removed after $x$'s scope is ended.
Rule P-IfC shows a classical conditional rule, which is the same as a conditional rule in Hoare Logic.
The other rules (P-Dis and P-Red) are amplitude manipulation operations, which will be introduced in <Ref>.
Rule P-Loop1 defines the loop case when the upper bound $n'$ is greater than the lower bound $n$.

\[\hspace*{-0.5em}
\begin{array}{r l}
\textcolor{blue}{1}
\textcolor{spec}{
\{A(x) * A(y) * B \}}
\;\;\text{where}\;\;
A(\beta) = \beta\srange{0}{n} \mapsto \ket{\overline{0}}
\\
\qquad\qquad\qquad
\qquad\qquad\quad\;\;
B = 1 < a < N * n > 0 \;* N < 2^n \cdot \texttt{gcd}(a,N)=1
\\[0.4em]
\textcolor{blue}{2}
& \qass{x\srange{0}{n}\;}{\;\ihadh};\\[0.2em]

\textcolor{blue}{3}
\textcolor{auto}{
\{x\srange{0}{n} \mapsto \dabs{\ihadh}(\ket{\overline{0}}) * A(y) * B \}
\\[0.4em]
\textcolor{blue}{4}
\textcolor{auto}{
\Rightarrow
\{x\srange{0}{n} \mapsto C * A(y) * B \}
\;\;\text{where}\;\;
C = \shad{2^n}{n\sminus 1}{}
\\[0.4em]
\textcolor{blue}{5}
& \qass{y\srange{0}{n}\;}{\;y\srange{0}{n}\,\splus\, 1};
\\[0.4em]

\textcolor{blue}{6}
\textcolor{auto}{
\{x\srange{0}{n} \mapsto C * y\srange{0}{n} \mapsto \dabs{y\splus 1}(\ket{\overline{0}}) * B \}
\\[0.4em]
\textcolor{blue}{7}
\textcolor{auto}{
\Rightarrow
\{x\srange{0}{n} \mapsto C * y\srange{0}{n} \mapsto \ket{\overline{0}}\ket{1} * B\}
\\[0.4em]
\textcolor{blue}{8}
\textcolor{auto}{
\Rightarrow
\{ E(0) * B\}
\;\;
\texttt{where}\;\;
E(t) =
\\
\qquad\qquad\qquad\quad
\begin{array}{l}
x\srange{t}{n} \mapsto \shadi{2^{n \,\sminus\,  t}}{n \sminus t\sminus 1}{}\;*
\\
x\srange{0}{t}\sqcupplus y\srange{0}{n} \mapsto \schai{2^t\sminus 1}{\frac{1}{\sqrt{2^t}}}{i}{\ket{a^{i}\;\mmod\;N}}
\end{array}
\\[0.4em]
\textcolor{blue}{9}
\qfor{j}{0}{n\,\sminus\,1}{x[j]}
\\[0.4em]
\textcolor{blue}{10}
\quad
\textcolor{spec}{\{E(j) * B\}}
\\[0.4em]
\textcolor{blue}{11}
\quad\qass{y\srange{0}{n}\;}{\;a^{2^j}\cdot y\srange{0}{n}\;\mmod\; N};
\\[0.4em]
\textcolor{blue}{12}
\textcolor{auto}{
\{E(n) * B\}
\\[0.4em]
\textcolor{blue}{13}
\textcolor{auto}{
\Rightarrow
\{x\srange{0}{n}\sqcupplus y\srange{0}{n} \mapsto \schai{2^{n}\sminus 1}{\frac{1}{\sqrt{2^{n}}}}{i}{\ket{a^{i}\;\mmod\;N}} * B\}
\\[0.4em]
\textcolor{blue}{14}
& \sexp{u}{\smea{y}}{}
\\[0.2em]
\textcolor{blue}{15}
\textcolor{auto}{
\{
x\srange{0}{n} \mapsto \smch{\frac{1}{\sqrt{s}}}{s\sminus 1}{t\,\splus\,k p}
p = \texttt{ord}(a,N)
s=\texttt{rnd}(\frac{2^n}{p}) * B
\}
\\[0.4em]
\textcolor{blue}{16}
\quad\qass{x\srange{0}{n}\;}{\;\iqft[-1]{}{}};
\\[0.4em]
\textcolor{blue}{17}
\textcolor{auto}{
\{
x\srange{0}{n} \mapsto \smich{\frac{1}{\sqrt{s 2^n}}}{2^n\sminus 1}{(\omega^{tk}\Msum_{j=0}^{s\sminus 1}\omega^{tkj})}{k}
p = \texttt{ord}(a,N)
s=\texttt{rnd}(\frac{2^n}{p}) * B
\}
\\[0.4em]
\textcolor{blue}{18}
\quad\sexp{w}{\smea{x}}{}
\\[0.4em]
\textcolor{blue}{19}
\textcolor{auto}{
\{
w=(\frac{4}{\pi ^ {2 p}},p)
p = \texttt{ord}(a,N)
s=\texttt{rnd}(\frac{2^n}{p}) * B
\}
\\[0.4em]
\textcolor{blue}{20}
\quad\quad\texttt{post}(w)
\\[0.4em]
\textcolor{blue}{21}
\textcolor{spec}{
\{
\texttt{post}(w)=(\frac{4e^{-2}}{\pi^2 \texttt{log}_2^4 N},p)
p = \texttt{ord}(a,N)
s=\texttt{rnd}(\frac{2^n}{p}) * B
\}
\end{array}
\]

The order finding of Shor's algorithm as the quantum portion. Type environments are on the right. $\sord{a,N}$ gets the order of $a$ and $N$. $\srnd{r}$ rounds $r$ to the nearest integer. The right-hand side contains the types of loci involved. $\ket{i}$ is an abbreviation of $\ket{\tob{i}}$.
$\tob{i}$ turns a number $i$ to a bitstring basis.
$\omega=e^{\frac{2\pi i}{2^n}}$

§.§ The Proof of The Order Finding Portion in Shor's Algorithm

Here, we show the complete proof scheme of Shor's algorithm <cit.> in .
Given an integer $N$, Shor's algorithm finds its nontrivial prime factors, which has the following step: (1) randomly pick a number $1 < a < N$ and compute $k=\texttt{gcd}(a,N)$;
(2) if $k \neq 1$, $k$ is the factor; (3) otherwise, $a$ and $N$ are coprime and we find the order $p$ of $a$ mode $N$;
(4) if $p$ is even and $a^{\frac{p}{2}} \neq -1\; \mmod\; N$, $\texttt{gcd}(a^{\frac{p}{2}}\pm 1,N)$ are the factors; otherwise, we repeat the process. Step (2) is Shor's algorithm's quantum component, an order-finding algorithm.
<Ref> discusses its pre-measurement part. Without the type environments, we show the full proof in <Ref>.
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 <Ref> in requires no states grayed out; only the conditions marked blue.
In <Ref>, The steps before line 5 prepare the $\thadt$ type value for the range $x[0,n)$ and add 1 to the range $y\srange{0}{n}$, which flips $y$'s lowest bit. The two results result in the state as the beginning of <Ref>.

After the two steps, <Ref> discusses all the steps up to line 15 in <Ref>.
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 $k$ values to the basis-ket's amplitudes as $\omega^{tk}\Msum_{j=0}^{s}\omega^{tkj}$. Then, line 18 measures variable $x$. In this procedure, we will get the period $p$ as part of the measurement result $w$ as $(\frac{4}{\pi ^ {2 p}},p)$. However, $w$ cannot be directly used as an order number in the actual order-finding implementation. Instead, we need a post step, the continued fraction method, to retrieve the order, which is stated as $\texttt{post}(w)$ in line 20. The post step takes an $\mmode$-kind value and returns a $\mmode$-kind value $\texttt{post}(w)=(\frac{4e^{-2}}{\pi^2 \texttt{log}_2^4 N},p)$, where $p$ is the order number that we are looking for, and $\frac{4e^{-2}}{\pi^2 \texttt{log}_2^4 N}$ is its probability value.
In the implementation in Dafny, we implement the conditioned fraction post steps and all these probability theorems by writing them as Dafny library functions and providing mechanized proofs by mimicking the proofs in <cit.>.

Ωσ_2X(j) * x0jy0n↦C(j).1 e X(j) * x0jy0n↦C'(j).1
Ωσ_2X(j) * (b,x[j1],x0jy0n)↦0.C(j)+1.C(j) e X(j) * x0jy0n↦C'(j).1
Ω,σ_1⊢_ {X(j) * x0j1y0n↦0.C(j)+1.C(j)} x[j]e

{ X(j) * (x[j],x[j],x0j1y0n)↦0.C(j)
* (x[j],x[j],x0j1y0n)↦C'(j).1}

ΩσX(j) * x0jy0n↦C(j) x[j]e X(j  1) * x0j1y0n ↦0.C(j)+1.C'(j)

X(j)=x\srange{j}{n}\mapsto \shad{2^{n \,\sminus\,  j}}{n \sminus j\sminus 1}{}
\qquad
C(j)=\sch{2^k\sminus 1}{\frac{1}{\sqrt{2^k}}}{\ket{\tob{j}^{k}}\ket{a^{\tob{j}^k}\;\mmod\;N}}
\\[0.2em]
d.C(j)=\sch{2^{\snext{k}}\sminus 1}{\frac{1}{\sqrt{2^{\snext{k}}}}}{\ket{\tob{j}^k}\ket{d}\ket{a^{\tob{j}^k}\;\mmod\;N}}
\qquad
C'(j).d=\sch{2^{\snext{k}}\sminus 1}{\frac{1}{\sqrt{2^{\snext{k}}}}}{\ket{a^{\tob{j}^k.1}\;\mmod\;N}\ket{\tob{j}^k}\ket{d}}
\\[0.2em]
d.C'(j)=\sch{2^{\snext{k}} \sminus 1}{\frac{1}{\sqrt{2^{\snext{k}}}}}{\ket{\tob{j}^k}\ket{d}\ket{{a^{\tob{j}^k.1}\;\mmod\;N}}}
\qquad
\sigma_1=\{x\srange{0}{n\sminus (j\splus 1)} : \thadt, \{x\srange{0}{j\splus 1},y\srange{0}{n}\} : \tcht \}
\\[0.2em]
\sigma=\{x\srange{0}{n\sminus (j\splus 1)} : \thadt, y\srange{0}{n\sminus (j\splus 1)} : \tcht \}
\qquad
e=\qass{y\srange{0}{n}\;}{\;a^{2^j}\cdot y\srange{0}{n}\;\mmod\; N}
\end{array}$

As an additional example for the frozen and unfrozen functions in the proof rule of quantum conditionals in <Ref>, we provide an additional proof tree for the quantum conditional in a loop step in lines 9-11 in <Ref> above.
Here, $\tob{j}$ means to turn natural number $j$ to a bitstring and $c.d$ means concatenating a single bit $d$ to the end of bitstring $c$.
The proof is built from the bottom up. We first cut the $\thadt$ type value into two loci ($x\srange{0}{n\sminus (j\splus 1)}$ and $x[j]$), join $x[j]$ with locus $x\srange{0}{j}\sqcupplus y\srange{0}{n}$, and duplicate the value elements to be $0.C(j)+1.C(j)$, which is proved by applying the consequence rule (P-Con) in <Ref>. Notice that the type environment also transitions from $\sigma$ to $\sigma_1$.
By the same strategy of the $\ufrz$ transformer in <Ref> , we combine the two $\ufrz$ terms into the final result.
The second step applies rule P-IF to substitute locus $x\srange{0}{j\splus 1}\sqcupplus y\srange{0}{n}$ with the frozen construct $\frz(b,x[j\splus 1],x\srange{0}{j}\sqcupplus y\srange{0}{n})$ in the pre-condition and create two $\ufrz$ terms in the post-condition. The step on the top applies the modulo multiplication on every element in the frozen value $\mapsto C(j).1$ by rule P-OP.

§ TRANSLATION FROM TO SEPARATION LOGIC

The types and loci are extra annotations associated with programs and predicates for proof automation.
In the implementation in Dafny, these annotations are not present—qubits are arranged as simple array structures without extra metadata such as locus types.
This section shows how annotations can be safely erased with no loss of
expressiveness, e.g., loci are represented as virtual-level dynamic sequences without types, and equational rewrites are compiled with extra operations in the compiled language. We present a compilation algorithm that converts from to , a C-like language admitting a subset of an array separation logic proof system.

A,B &::=& \overline{n}\\
\widetilde{op}&::=&\mu\mid op\\
\widetilde{e} &::=& x=\texttt{alloc}{(A)}\\
&\mid& \texttt{mutate}{(n,\widetilde{op},x)}\\
&\textcolor{red}{\mid}& \textcolor{red}{(r,n)=\texttt{pick}{(x,m)}}\\
&\textcolor{red}{\mid}& \textcolor{red}{\texttt{filter}{(x,b)}}\\
&\textcolor{red}{\mid}& \textcolor{red}{\texttt{amp}{(x,r)}}\\
&\mid& ...
\end{array}

Heap Layout

Compilation Proof Diagram

Target Compilation Language.
is based on a variant of the separation logic introduced by <cit.>,
which is sound and complete.
Mainly, we utilize the allocation (alloc), heap lookup and mutation operations (mutate) in the work,
with three additional operations (marked red in <Ref>).
In , program states are divided into virtual and physical levels in <Ref>.
Every program starts with a physical qubit array, analogous to physical heap structures. The program operations are applied on qubit sequences of array indices ($A$), representing a collection of physical qubit locations and living at the virtual level. permits immutable program variables ($x$) representing these sequences.

An allocation $x=\texttt{alloc}{(A)}$ allocates a new array $x$ that copies $A$'s content and has the same length as $A$, while a heap mutation $\texttt{mutate}{(n,\widetilde{op},x)}$ mutates the first $n$ elements of the array pointed to by $x$, by applying the operation $\widetilde{op}$. Operations $\cn{pick}$, $\cn{filter}$, and $\cn{amp}$ are variations of heap lookups and mutations.
$(r,n)=\texttt{pick}{(x,m)}$ measures the first $m$ qubits in $x$, with the outcome $n=\tov{c}$ and its probability $r$, similar to the computation in S-Mea (<Ref>).
$\texttt{filter}{(x,b)}$ mutates $x$'s pointed-to quantum value by filtering out basis-kets that are not satisfying $b$,
and $\texttt{amp}{(x,r)}$ multiples $r$ to every basis-kets in $x$'s quantum value.
<cit.> maintains completeness by carefully designing the proof rules so heap mutations do not modify pointer references. ensures the same property by immutable variables, i.e., if a sequence changes, we allocate a new array and a new variable pointing to the array. For example, to join two loci represented by two sequences $A$ and $B$, respectively pointed to by variables $x$ and $y$, we allocate a new space for the two sequences' concatenation ($A@B$); so we compile the join to $u=\cn{alloc}(A@B)$. We must abandon using $x$ and $y$ after the join and only refer to $u$ in the following computation.

Compilation Formalism.
As shown in <Ref>,
we compile the language to and achieve the proof system compilation through the proof system completeness in and .
For every program, we translate the program and states to .
Then, every provable triple in can be translated to a provable triple through the language translation from to as the diagram (<Ref>).
The compilation is defined by extending 's typing judgment thusly:
$\Omega;\sigma\vdash_g (\theta,\varphi,e) \gg (\theta,\widetilde{\psi},\widetilde{\varphi},\widetilde{e})$.
We include an initial state $\varphi$, the output local store ($\widetilde{\psi}$), mapping variables to qubit location sequences, and state ($\widetilde{\varphi}$), mapping from locations to quantum values.
$\theta$ and $\theta'$ are maps from locus locations in $\varphi$ to qubit locations in $\widetilde{\varphi}$.

Due to space constraints, we explain the rules for compilation by examples of compiling the operations to .
The locus rewrites (<Ref>) are compiled to the array allocations, such as the join operation above.
Additionally, the split of a locus is compiled to two consecutive allocations of two sequences, respectively representing the two split result loci.
In compiling a measurement statement ($\sexp{x}{\smea{y}}{...}$), where $y$ locates in the locus $y\srange{0}{n}\sqcupplus \kappa$,
let's assume that the locus is mapped in $\theta$ by sequence $[0,n+m)$, pointed to by $u$ in $\widetilde{\psi}$,
while the range $y\srange{0}{n}$ is mapped by the sequence $[0,n)$;
the operation is compiled to:

$\sseq{(r,p)=\cn{pick}{(u,m)}}{\sseq{\cn{filter}(u,u[0,n) = p)}{\sseq{\cn{amp}{(u,\sum_j\frac{z_j}{\sqrt{r}})}}{t=\cn{alloc}({[n,n\splus m))}}}}$

Here, we first pick a key $p$, filter out the basis-kets whose $u[0,n)$'s position bases are not $p$,
normalizes the amplitudes of the remaining basis-kets (<Ref>),
and allocate a new space $t$ for the quantum residue after the measurement.
We must also update $\kappa$ in $\theta$ to map to the newly allocated space of $t$ instead of $[n,n\splus m)$.
We compile an operation $\qass{x\srange{0}{n}\sqcupplus y[0]}{\qbool{x}{<}{5}{y[0]}}$ with its initial state $\varphi$ ($C=\shad{2^n}{n\sminus 1}{}$) to , with $D=\scha{2^n\sminus 1}{}{j}{\ket{{j\,\slt\,5}}}$. Such an operation computes the Boolean comparison of $x\,\slt\,5$ and stores the value to $y[0]$.

\begin{array}{l@{~}c@{~}l}
\begin{array}{l}
\quad\textcolor{spec}{\varphi=\big{\{}x\srange{0}{n}: C, y[0]:\ket{0}\big{\}}}\\[0.1em]
\qquad\qass{x\srange{0}{n}\sqcupplus y[0]\;}{\;\qbool{x}{<}{5}{y[0]}}\\[0.1em]
\quad\textcolor{spec}{\varphi'=\big{\{}x\srange{0}{n}\sqcupplus y[0]:D \big{\}}}
\end{array}
\text{\scalebox{1.5}{\quad$\gg$}\quad}
\begin{array}{l}
\textcolor{spec}{\widetilde{\psi}=\big{\{}p: [0,n), t : \{n\} \big{\}}, \widetilde{\varphi}=\big{\{} [0,n) : C * \{n\}:\ket{0}\big{\}}}
\\[0.2em]
\quad{\sseq{u=\cn{alloc}([0,n\splus 1))}{\cn{mutate}(n\splus 1,u[0,n)\,\slt\,5@ u[n],u)}}
\\[0.2em]
\textcolor{spec}{
\widetilde{\psi'}=
\widetilde{\psi}\cup
\big{\{}
u: [n\,\splus\, 1\,,\;2 n\,\splus\, 2)\big{\}}, \widetilde{\varphi'}=\widetilde{\varphi}\cup\big{\{} [n\,\splus\, 1\,,\;2 n\,\splus\, 2): D \big{\}}}
\end{array}
\end{array}

After the compilation, we create two local variables $p$ and $t$ to represent the loci $x$ and $y$, mapping to sequences $[0,n)$ and $\{n\}$. We then add an allocation $u=\cn{alloc}([0,n\,\splus\, 1))$ allocating a new space $[n\splus 1,2 n\,\splus\, 2)$ to join the two loci. The post-state contains a new variable $u$, pointing to the concatenated new sequence $[n\,\splus\, 1\,,\,2 n\,\splus\, 2)$.
The old arrays $p$ and $t$ are still in the stores, but we refer to the locus $x\srange{0}{n}\sqcupplus y[0]$ as the newly allocated space in the following computation by mapping the locus to the new space in $\theta'$.
The language compilation correctness from to is stated below,
which is validated by testing the compiler's semantic equivalence on 203 unit test programs.

For any $e$, $\theta$ and $\theta'$, such that $\Omega;\sigma \vdash_g e \triangleright \sigma'$, $\Omega;\sigma \vdash_g \varphi$, and $\Omega;\sigma\vdash_g (\theta,\varphi,e) \gg (\theta',\widetilde{\psi},\widetilde{\varphi},\widetilde{e})$; thus, if $(\varphi,e)\Downarrow \varphi'$, then
$(\widetilde{\psi},\widetilde{\varphi},\widetilde{e})\Downarrow (\widetilde{\psi'},\widetilde{\varphi'})$, where $\widetilde{\varphi'}$ is the compiled results of $\varphi'$ with the $\theta'$ map.

§ HUMAN EFFORT COMPARISON

GHZ     < 1     -     10     -     -

Deutsch–Jozsa     < 1     3     12     -     -

Grover's search     2     3     7     30     14

Shor's algorithm     5     28     1040     -     -

Controlled GHZ     < 1     -     -     -     -

Quantum Walk     3     -     -     -     -

Human effort comparison, which measures the time for a single person to finish programming and verifying an algorithm;  means no data.

We did a small survey regarding the human efforts of different groups of researchers who work on quantum program verification.
We sent out survey questionnaires to the different research groups listed in <Ref> through emails regarding two major questions: 1) the human efforts in verifying the list of quantum programs and 2) the quantum research experience the researchers had before verifying the programs.

The data are summarized in <Ref>.
We show the total number of days for each algorithm by summing the time for individuals finishing the algorithm verification, each column per group.
We show the human efforts for ,  <cit.>,  <cit.>, Quantum Hoare Logic Implementation (QHL) <cit.>, and <cit.>.
We show the results for verifying four different algorithms, including GHZ, Deutsch–Jozsa, Grover's search, and Shor's algorithm, because these are the common quantum algorithms that many research groups verified.
The verification of Controlled GHZ and Quantum Walk is uniquely done in , as the examples show that is suitable for verifying new quantum algorithms beyond the standard ones, such as the four algorithms above.
QHL and mainly focus on verifying HCQ programs, and the only quantum program among the four algorithms they verified is Grover's search algorithm.

Since we are measuring human efforts, the survey subjects to the personal efforts of individuals, such as the hours that these researchers spent on the project per day and their familiarity with the systems.
The verification of quantum programs in was finished by a student who was not the developer and had one year of experience in the study of quantum computing.
For , the verification of the GHZ and Deutsch–Jozsa algorithms was done by a non-developer student having two-year of experience in quantum computing, while Grover's search verification was finished by the developer, having studied quantum computing for three years at the time of performing the verification.
Shor's algorithm was verified by four experienced researchers, including the developer.
The algorithm verification, done by , QHL, and , was finished by the developer of the frameworks, who had at least three years of quantum computing experience, respectively.

Some of the algorithm verification has different content. As we mentioned in <Ref>, verifying Shor's algorithm from is finished by assuming without proving many mathematical theorems. In contrast, verified every mathematical theorem in verifying their version of Shor's algorithm.

Unlike , for both and , we can see that the framework verification is not scalable to large program verification, as verifying a large algorithm, such as Shor's algorithm, requires significantly more time than verifying small and well-known programs.
The GHZ, Deutsch–Jozsa, and Grover's search algorithms are relatively small, and their step-by-step behaviors are well-known in much literature, while some parts of Shor's algorithm, such as the probability bounds, are not known until the verification is done by .

The only algorithm verification done in QHL is Grover's search algorithm, which has 3184 lines of code.
It took the QHL developer one month to finish the verification.
inherits the style of verification from QHL, with a proof system to verify hybrid classical-quantum (HCQ) programs.
The style of the quantum component verification in QHL and is similar to .
Other than Grover's search, finishes several other kinds of HCQ program verification,
which is beyond the scope of the paper. These algorithms typically assume that a large portion of quantum components is given as black boxes and verify the behaviors of utilizing the black-boxed quantum components as procedures in a classical program.
For example, the definition of the quantum phase estimation (QPE) program in differs from the one.
In , the QPE's oracle part is defined as a loop structure, each loop step contains a controlled-$U$ gate, while the oracle part in the version is defined as a big black box, with the given assumptions of the pre- and post-conditions of the black box.

§ AMPLITUDE MANIPULATION OPERATIONS

Diffusion Analogy

Quantum amplitude manipulation operations are to manipulate the amplitudes of basis-kets in a quantum state.
As shown in <Ref>, the quantum walk framework is a framework for manipulating specific basis-kets in a state if certain conditions are met, such as the controlled Hadamard operation in <Ref> line 5.
In fact, the controlled Hadamard operation is a simple case for using amplitude manipulation operations in a quantum walk framework. Here, its utility duplicates basis-kets so that we can allow two children's tree nodes to appear simultaneously.
In <Ref>,
rules S-Dis and P-Dis as well as S-Red  and P-Red
show the semantic and proof rules for quantum amplitude manipulation operations.
The former two show the rules for amplitude diffusion, and the latter two show the rules for amplification operations.
The difference between a diffusion and an amplification is that the different functionality, i.e.,
the former is used to duplicate basis-kets or average the amplitudes in different basis-kets, while the latter is to amplify the amplitudes of some basis-kets so they can have a better chance to measure out.
As we know, amplitudes associated with basis-kets represent the likelihood the basis-ket is present when a measurement happens.
Amplifying the amplitudes certainly increases the chance of measuring the basis-kets the amplitudes are attached to.

Quantum diffusion operations ($\ssassign{\kappa}{}{\sdis}$) 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 <Ref>. More specifically, the diffusion function $\mathpzc{D}(n,q)$ (Rule SDis and PDis in <Ref>) first takes an $n'$-element $\tcht$ typed value $\schi{t=0}{z_t}{c_t}$, where $n$ corresponds to the number of qubits in $\kappa$.
Then, we rearrange the value by extending the element number from $n'$ to $m*n$ by probably adding new elements that originally have zero amplitude (the white elements in <Ref>).
Here, let us view a basis $c_{t}$ as a little-endian (LSB) number
$\tov{c_{t}}$. The rearrangement of changing bases $c_{t}$ (for all $t$) to
$\tob{j}.c_{ij}$ is analogized to rewrite a number $\tov{c_{t}}$ to be the form
$2^n i+j$, with $j\in [0,2^n)$, i.e., the reshaping step rearranges the
basis-kets to be a periodic counting sequence, with $2^n$ being the order.
The mean computation analogy (the second arrow in <Ref>) takes every period in the reshaped value. For each basis-ket in a period, we redistribute its amplitude by the formula $(\frac{1}{2^{n-1}}\sum_{u=0}^{2^n\sminus 1}z_{iu} - z_{ij})$.
The diffusion function $\mathpzc{D}(n,q)$ is implemented as a locus predicate transformer in , similar to $\frz$ and $\ufrz$ in <Ref>.
An example of the quantum walk algorithm that uses diffusion operations is given in <Ref>.

Rules SRed and PRed are the semantic and proof rules for the quantum amplification ($\texttt{reduce}$). It is similar to the diffusion operation, except we only need to multiply an additional amplitude factor $z_{cu}$ for each amplitude term.
For each $u \in [0,2^t)$, if $\tob{u}=c$, we multiply the factor $\frac{1}{\sqrt[4]{2^n}}$, if $\tob{u}\neq c$, we multiply the factor
$\sqrt{1-\frac{1}{\sqrt{2^n}}}$. One example usage is to rewrite the quantum walk algorithm in <Ref> to a new one by replacing the diffusion operation with $\ssassign{u}{}{\sreduce{\overline{0}}{n}}$, where $n$ is an 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 representing 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 $\snext{j}$-th depth nodes have higher amplitudes than basis-kets having $j$-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.

§.§ The Grover's Search Proof in with a New Amplitude Representation

\[\hspace*{-0.5em}
\begin{array}{r l}
\textcolor{blue}{1}
\textcolor{spec}{
\big{\{} x\srange{0}{n}\mapsto \ket{\overline{0}} * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}}
\;\;
\texttt{where}\;\;
\xi=\cos^{-1}(\frac{1}{\sqrt{2^n}})
\wedge \chi=\pi - 2\xi
\\[0.4em]
\textcolor{blue}{2}
& \qass{x\;}{\;\ihadh};
\\[0.2em]
\textcolor{blue}{3}
\textcolor{auto}{
\big{\{}x\srange{0}{n} \mapsto \shad{2^n}{n\sminus 1}{} * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}
\\[0.4em]
\textcolor{blue}{4}
\textcolor{auto}{
\Rightarrow
\big{\{}x\srange{0}{n} \mapsto \frac{1}{\sqrt{2^n}}\ket{k} + \frac{1}{\sqrt{2^n}}\ssum{j=0\wedge j\neq k}{2^n\sminus 1}{\ket{j}} * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}
\\[0.4em]
\textcolor{blue}{5}
\textcolor{auto}{
\Rightarrow
\big{\{}x\srange{0}{n} \mapsto \cos\varrho_0 \ket{k} + \sin\varrho_0 \cdot q * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}
\;\;\texttt{where}\;\;q=\frac{1}{\sqrt{2^n-1}}\ssum{j=0\wedge j\neq k}{2^n\sminus 1}{\ket{j}}
\wedge \varrho_i=\xi-j\cdot \chi
\\[0.4em]
\textcolor{blue}{6}
\texttt{for}~\;{j \in [0,N)}
\\[0.4em]
\textcolor{blue}{7}
\;\;
\textcolor{spec}{\big{\{} x\srange{0}{n} \mapsto \cos\varrho_j \ket{k} + \sin\varrho_j \cdot q * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}}
\\[0.4em]
\textcolor{blue}{8}
\{
\\[0.4em]
\textcolor{blue}{9}
\quad
\qass{x\;}{\;U()};
\\[0.4em]

\textcolor{blue}{10}
& \quad\qass{x\;}{\;\sdis};
\\[0.4em]
\textcolor{blue}{11}
\}
\\[0.4em]
\textcolor{blue}{12}
\textcolor{auto}{
\big{\{} x\srange{0}{n} \mapsto \cos\varrho_N \ket{k} + \sin\varrho_N \cdot q * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}
\\[0.4em]
\textcolor{blue}{13}
\sexp{y}{\smea{x}}{\sskip}
\\[0.4em]
\textcolor{blue}{14}
\textcolor{spec}{
\big{\{} y=(p,k) * p > \cos^2(\chi) * N = \lfloor \frac{\xi}{\chi} \rfloor \big{\}}
\end{array}
\]

Grover's Search in .

Amplitudes $z$ in <Ref> are complex numbers. In general, they are hard to admit proof automation.
In the implementation in Dafny, we observe the common patterns of many quantum algorithms,
and implement amplitudes $z$ as $r\cdot e^{2\pi i \cdot \frac{1}{n}}$, where $r$ is a real number in the range $[0,1)$ and $e^{2\pi i \cdot \frac{1}{n}}$ is a phase. Since a phase always has the pattern $e^{2\pi i \cdot \frac{1}{n}}$, we can represent it as a natural number $n$. In addition, $r$ can also be approximated by rational numbers. Thus, in Dafny, we represent an amplitude by a pair of a rational number, representing the $r$ amplitude, and a natural number $n$, representing the phase part $e^{2\pi i \cdot \frac{1}{n}}$.
With this setting, we enable many rewrite theories of rational and natural numbers for proof automation on capturing the changes of amplitudes, which successfully help us verify the programs in <Ref>, except Grover's search.

A quantum program involving amplitude manipulation operations usually requires a comprehensive representation with a new theory library to promote proof automation.
Here, we utilize Grover's search proof <cit.> as an example to highlight the use of a comprehensive representation: the trigonometric amplitude representations.
<Ref> provides the proof steps of the algorithm in .
The proof system can automatically infer the gray parts in the proof with some understanding of trigonometric theorems defined by our researcher in the Dafny framework.
The function $U()$ is a predefined oracle function. There are two properties for it.
First, we know that $k$ is the key in the oracle function. $U()\ket{j}=-1\cdot{j}$, if $j=k$; otherwise, $U()\ket{j}=-1\cdot{j}$.
Second, we also require that such a key is unique for all $j \in [0,2^n)$.
Thus, if we input an $\tcht$ typed value $\sch{2^n}{}{\ket{j}}$ to the oracle function, the result value can be divided into two parts:
$-\frac{1}{\sqrt{2^n}}\ket{k} + \frac{1}{\sqrt{2^n}}\ssum{j=0\wedge j\neq k}{2^n\sminus 1}{\ket{j}}$.

Notice that for any quantum value $\sch{m}{z_j}{\ket{c_j}}$, we have $\sum_{j=0}^{m}\slen{z_j}^2 = 1$.
For the above two parts, if we view $\frac{1}{\sqrt{2^n}}$ as $\cos\xi$, the second part can be rewritten as $\sin\xi \cdot q$ with $q=\frac{1}{\sqrt{2^n-1}}\ssum{j=0\wedge j\neq k}{2^n\sminus 1}{\ket{j}}$.
Thus, the loop invariant in line 7 is given as
$x\srange{0}{n} \mapsto \cos\varrho_j \ket{k} + \sin\varrho_j \cdot q * N = \lfloor \frac{\xi}{\chi} \rfloor$.
Here, we define $\varrho_j = \xi-j\cdot \chi$, so $\varrho_0=\xi=\cos^{-1}(\frac{1}{\sqrt{2^n}})$.
When we apply the $U()$ function inside the loop, we see that $x$'s value is transformed to $-\cos\varrho_j \ket{k} + \sin\varrho_j\cdot q$. 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 $x$ as $\cos\varrho_{j\splus 1} \ket{k} + \sin\varrho_{j\splus 1} \cdot q$.
The reason is set up as an additional theorem in Dafny, and the transitions are as follows:

\[
\begin{array}{l}
2\paren{-\cos\xi\cos\varrho_j+\sin\xi\sin\varrho_j}\paren{\cos\xi\ket{k}+\sin\xi \cdot q}
-\paren{-\cos\varrho_j\ket{k}+\sin\varrho_j\cdot q}\\
= \paren{-2\cos^2\xi\cos\varrho_j+2\sin\xi\sin\varrho_j\cos\xi +\cos\varrho_j}\ket{k}
+ \paren{-2\sin\xi\cos\xi\cos\varrho_j+2\sin^2\xi\sin\varrho_j -\sin\varrho_j}\cdot q\\
= \paren{\paren{1-2\cos^2\xi}\cos\varrho_j+2\sin\xi\sin\varrho_j\cos\xi}\ket{k}
+ \paren{-2\sin\xi\cos\xi\cos\varrho_j+2\sin\varrho_j\paren{\sin^2\xi - 1}}\cdot q\\
+ \paren{-\sin\paren{2\xi}\cos\varrho_j-\sin\varrho_j\cos\paren{2\xi}}\cdot q\\
= \paren{\cos\paren{\pi - 2\xi}\cos\varrho_j+\sin\paren{\pi - 2\xi}\sin\varrho_j}\ket{k}
+ \paren{-\sin\paren{\pi - 2\xi}\cos\varrho_j+\sin\varrho_j\cos\paren{\pi - 2\xi}}\cdot q\\
= \paren{\cos\paren{\chi}\cos\varrho_j+\sin\paren{\chi}\sin\varrho_j}\ket{k}
+ \paren{-\sin\paren{\chi}\cos\varrho_j+\sin\varrho_j\cos\paren{\chi}}\cdot q\\
= \cos\paren{\varrho_j-\chi}\ket{k} + \sin\paren{\varrho_j-\chi}\cdot q\\
= \cos\paren{\varrho_{j+1}}\ket{k} + \sin\paren{\varrho_{j+1}}\cdot q
\end{array}
\]

A quantum diffusion operation can also be viewed as a trigonometric rotation, and the above calculation shows that the rotation eventually turns the $\varrho_j$ degree to $\varrho_{j+1}$.
At the end of the program in <Ref>, before the measurement,
the $x$'s value is $\cos\varrho_N \ket{k} + \sin\varrho_N$ with $\varrho_N = \xi-\lfloor \frac{\xi}{\chi} \rfloor\cdot \chi$.
Notice that $0 \le \varrho_N < \chi$, so we will have the probability of $p$ reaching the measurement result $k$ to be greater than $\cos^2(\chi)$.
The estimation can be better, but any other analysis will follow the same pattern introduced here.

In the implementation, we set trigger rules to rewrite the term in line 4 in <Ref> to the trigonometric format in line 5. Then, we also provide theorems to support the rewrite of $x$'s value from $-\cos\varrho_j \ket{k} + \sin\varrho_j\cdot q$ to
$\cos\paren{\varrho_{j+1}}\ket{k} + \sin\paren{\varrho_{j+1}}\cdot q$ in line 10. The Dafny proof system automatically derives the other proof.

§ AN UPGRADED TYPE SYSTEM AND EQUIVALENCE RELATIONS

Here, we describe an upgraded type system based on the one in <Ref>, which upgrades it to a dependent type system by including bases in every basis-kets. The type system is under construction in the implementation.
We first show some additional syntax in <Ref>.

Each construct type is only associated with additional flags depending on the quantum states. The flag $\topt{c}$ for $\tnort$ means we can track the basis-ket bitstring of the $\tnort$ typed value $z\ket{c}$ in the type checking stage. Sometimes, we might be unable to track the basis so we will classify it as $\infty$. Similar to the $\tnort$ typed situation, we use $\bigcirc$ to represent that a $\thadt$ typed value is in uniformed superposition. If not, we can classify the $\thadt$ typed basis-ket as $\infty$. In dealing with $\tcht$ typed values, we will use a set of bases $\overline{c}(m)$ to refer to the basis-ket bitstrings appearing in an $\tcht$ typed value $\sch{m}{z_j}{c_j}$.
In $\overline{c}(m)$, $\overline{c}$ is a basis set, and $m$ is the element number, and it can be abbreviated as $\overline{c}$.

\[
\begin{array}{llcl}
\text{Indexed basis set} & \overline{c}(m) & ::= & \{c_0,c_1,...,c_{m-1}\}       \\
\text{Option} & p \in\; \topt{'a} & ::= & 'a \mid \infty \\
\text{Uniform Distribution} & \bigcirc \\
\text{Type} & \tau & ::= & \tnor{(\topt{c})}\mid \thad{(\topt{\bigcirc})}
\mid \tch{(\topt{\overline{c}(m)})}
\end{array}
\]

Upgraded Type Syntax

\[
\begin{array}{l@{~}cl}
\tnor{\infty} &\sqsubseteq_n& \tch{\infty}\\
\tnor{c} &\sqsubseteq_n& \tch{\{c\}}\\
\tch{\overline{c}(1)} &\sqsubseteq_n& \tnor{\overline{c}[0]}\\
\thad{p} &\sqsubseteq_n& \tch{\{\tob{j}|j\in[0,2^n)\}(2^n)}\\
\tch{\{0,1\}} &\sqsubseteq_1& \thad{\infty}\\
\tch{p} &\sqsubseteq_n& \tch{\infty}
\end{array}
\]

Upgraded Subtyping

\[
\begin{array}{l@{~}cl}
\ket{c} &\equiv_n& \sch{0}{ }{\ket{c}}\\
\sch{0}{z_j}{\ket{c_j}} &\equiv_n& \ket{c_0}\\
\shad{2^n}{n\sminus 1}{\alpha(r_j)} &\equiv_n& \sch{2^n\sminus 1}{\frac{\alpha(\sum_{k=0}^{n\sminus 1} r_k \cdot \tob{j}[k])}{\sqrt{2^n}}}{\ket{j}}\\
\sch{1}{z_j}{c_j} &\equiv_1& \shad{2}{0}{\frac{\sqrt{2}z_1}{z_0}}\\
&&\qquad\texttt{when }c_0=0\;\;c_1=1
\end{array}
\]

Upgraded Quantum Value Equivalence

type/value state relations. $\overline{c}[n]$ produces the $n$-th element in set $\overline{c}$. $\{\tob{j}|j\in[0,2^n)\}(2^n)$ defines a set $\{\tob{j}|j\in[0,2^n)\}$ with the emphasis that it has $2^n$ elements. $\{0,1\}$ is a set of two single element bitstrings $0$ and $1$. $\cdot$ is the multiplication operation, $\tob{j}$ turns a number $j$ to a bitstring basis, $\tob{j}[k]$ takes the $k$-th element in the bitstring $\tob{j}$, and $\ket{j}$ is an abbreviation of $\ket{\tob{j}}$.

The most significant 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 in the to Dafny compilation. We have new subtyping and quantum value equivalence relations in <Ref>.
The subtyping relation $\sqsubseteq_n$ and the value equivalence $\equiv_n$ is not associated with a qubit number (locus length number) $n$, such that they establish relations between two quantum values describing a locus of length $n$.
$\sqsubseteq_n$ in <Ref> describes a type term on the left that can be used as a type on the right. For example, a  type qubit array $\tnor{c}$ can be used as a single element entanglement type term $\tch{\{c\}}$ [If a qubit array only consists of $0$ and $1$, it can be viewed as an entanglement of unique possibility. ].
Correspondingly, value equivalence relation $\equiv_n$, in <Ref>, describes the two values to be equivalent; specifically, the left state term can be used as the right one, e.g., a single element entanglement value $\sch{0}{z_j}{\ket{c_j}}$ can be used as a  typed value $\ket{c_0}$ with the fact that $z_0$ is now a global phase that can be neglected.

In addition to the rewrites in <Ref>, we now permit the rewrites from an $\tcht$ typed value to a $\tnort$ typed one if we find that the $\tcht$ typed value contains a singleton basis-ket, while an $\tcht$ typed value can also be rewritten to a $\thadt$ typed one if we find that the length of the $\tcht$ typed value is $1$, and it contains exactly two basis-kets.

\[
\begin{array}{r@{~}c@{~}l@{~}cl}
&&\{\emptyset:\tau\} \cup \sigma &\preceq& \sigma\\
\tau\sqsubseteq_{\slen{\kappa}}\tau' &\Rightarrow& \{\kappa:\tau\} \cup \sigma &\preceq& \{\kappa:\tau'\} \cup \sigma\\
&&\{\kappa_1\sqcupplus s_1 \sqcupplus s_2 \sqcupplus \kappa_2 :\tau\} \cup \sigma &\preceq& \{\kappa_1\sqcupplus s_2 \sqcupplus s_1 \sqcupplus \kappa_2 : \texttt{mut}(\tau,\slen{\kappa_1})\} \cup \sigma\\
&&\{\kappa_1 :\tau_1\} \cup \{\kappa_2 :\tau_2\} \cup \sigma &\preceq& \{\kappa_1 \sqcupplus \kappa_2 :\texttt{mer}(\tau_1,\tau_2)\} \cup \sigma \\
\texttt{spt}(\tau,\slen{\kappa_1})=(\tau_1,\tau_2)&\Rightarrow&\{\kappa_1 \sqcupplus \kappa_2 :\tau\} \cup \sigma &\preceq& \{\kappa_1 :\tau_1\} \cup \{\kappa_2 :\tau_2\} \cup \sigma
\end{array}
\]

\[
\begin{array}{l}
\texttt{pmut}((c_1.i_1.i_2.c_2),n)=(c_1.i_2.i_1.c_2) \;\;\texttt{when}\;\slen{c_1}=n
\\
\texttt{mut}(\tnor{c},n)=\tnor{\texttt{pmut}(c,n)}
\qquad
\texttt{mut}(\tch{\overline{c}(m)},n)=\tch{\{\texttt{pmut}(c,n)|c\in\overline{c}(m)\}(m)}
\qquad
\texttt{mut}(\tau,n)=\tau\;\;[\texttt{owise}]
\\
\texttt{mer}(\tnor{c_1},\tnor{c_2})=\tnor{(c_1.c_2)}
\qquad
\texttt{mer}(\thad{\bigcirc},\thad{\bigcirc})=\thad{\bigcirc}
\qquad
\texttt{mer}(T\;\infty,T\;t)=T\;\infty
\\
\texttt{mer}(\tch{\overline{c_1}(m_1)},\tch{\overline{c_2}(m_2)})=\tch{(\overline{c_1}\times \overline{c_2})(m_1*m_2)}
\\
\texttt{spt}(\tnor{c_1.c_2},n)=(\tnor{c_1},\tnor{c_2}) \;\;\texttt{when}\;\slen{c_1}=n
\qquad
\texttt{spt}(\thad{t},n)=(\thad{t},\thad{t})
\\
\texttt{spt}(\tch{\{c_j.c|j\in [0,m)\wedge |c_j|=n\}(m)},n)=(\tch{\{c_j|j\in [0,m)\wedge |c_j|=n\}(m)},\tnor{c})
\end{array}
\]

Upgraded type environment partial order. We use set union ($\cup$) to describe the type environment concatenation with the empty set operation $\emptyset$. $i$ is a single bit either $0$ or $1$. The $.$ operation is a bitstring concatenation. $\times$ is the Cartesian product of two sets.
$T$ is either $\texttt{Nor}$, $\texttt{Had}$ or $\texttt{CH}$.

\[
\begin{array}{r@{~}c@{~}l@{~}cl}
&&\{\emptyset:q\} \cup \varphi &\equiv& \varphi\\
q\equiv_{\slen{\kappa}}q' &\Rightarrow& \{\kappa:q\} \cup \varphi &\equiv& \{\kappa:q'\} \cup \varphi\\
&&\{\kappa_1\sqcupplus s_1 \sqcupplus s_2 \sqcupplus \kappa_2 :q\} \cup \varphi &\equiv& \{\kappa_1\sqcupplus s_2 \sqcupplus s_1 \sqcupplus \kappa_2 : \texttt{mut}(q,\slen{\kappa_1})\} \cup \varphi\\
&&\{\kappa_1 :q_1\} \cup \{\kappa_2 :q_2\} \cup \varphi &\equiv& \{\kappa_1 \sqcupplus \kappa_2 :\texttt{mer}(q_1,q_2)\} \cup \varphi \\
\texttt{spt}(\tau,\slen{\kappa_1})=(\tau_1,\tau_2)&\Rightarrow&\{\kappa_1 \sqcupplus \kappa_2 :\tau\} \cup \sigma &\preceq& \{\kappa_1 :\tau_1\} \cup \{\kappa_2 :\tau_2\} \cup \sigma
\end{array}
\]

\[
\begin{array}{l}
\texttt{pmut}((c_1.d_1.d_2.c_2),n)=(c_1.d_2.d_1.c_2) \;\;\texttt{when}\;\slen{c_1}=n
\\
\texttt{mut}(\ket{c},n)=\ket{\texttt{pmut}(c,n)}
\qquad
\texttt{mut}(\sch{m}{z_j}{\ket{c_j}},n)=\sch{m}{z_j}{\ket{\texttt{pmut}(c_j,n)}}
\\
\texttt{mut}(\frac{1}{\sqrt{2^m}}(q_1 \bigotimes (\ket{0}+\alpha(r_n)\ket{1}) \bigotimes (\ket{0}+\alpha(r_{n+1})\ket{1}) \bigotimes q_2),n)
\\
\qquad\qquad
=\frac{1}{\sqrt{2^m}}(q_1 \bigotimes (\ket{0}+\alpha(r_{n+1})\ket{1}) \bigotimes (\ket{0}+\alpha(r_n)\ket{1}) \bigotimes q_2)
\quad\texttt{when\;}\slen{q_1}=n
\\
\texttt{mer}(\ket{c_1},\ket{c_2})=\ket{c_1}\ket{c_2}
\\
\texttt{mer}(\shad{2^n}{n\sminus 1}{\alpha(r_j)},\shad{2^m}{m\sminus 1}{\alpha(r_j)})=\shad{2^{n+m}}{n\splus m\sminus 2}{\alpha(r_j)}
\\
\texttt{mer}(\sch{n}{z_j}{\ket{c_j}},\schk{m}{z_k}{c_k})=\schi{n\cdot m}{z_j\cdot z_k}{c_j}\ket{c_k}
\\
\texttt{spt}(\ket{c_1.c_2},n)=(\ket{c_1},\ket{c_2}) \;\;\texttt{when}\;\slen{c_1}=n
\qquad
\texttt{spt}(q_1\bigotimes q_2,n)=(q_1,q_2) \;\;\texttt{when}\;\slen{q_1}=n
\\
\texttt{spt}(\sch{m}{z_j}{\ket{c_j}}\ket{c},n)=(\sch{m}{z_j}{\ket{c_j}},\ket{c})
\end{array}
\]

Upgraded quantum state equivalence. We use set union ($\cup$) to describe the state concatenation with the empty set operation $\emptyset$. $i$ is a single bit either $0$ or $1$. The $.$ operation is a bitstring concatenation.
Term $\Msum^{n\cdot m}P$ is a summation formula that omits the indexing details.
Term $(\frac{1}{\sqrt{2^{n}}}\Motimes_{j=0}^{n\sminus 1}q_j) \bigotimes(\frac{1}{\sqrt{2^{m}}}\Motimes_{j=0}^{m\sminus 1}q_j)$ is equivalent to $\frac{1}{\sqrt{2^{n+m}}}\Motimes_{j=0}^{n\splus m \sminus 2}q_j$.

[T-Mea] Ω(y)=j
Ω[x↦],σ⊎{κ: ∞}⊢_ e ▹σ'Ω,σ⊎{y0jκ: τ} ⊢_ xye ▹σ'

[T-MeaN] Ω(y)=j
c'={c_2 | n.c_2∈c∧n=j}

Ω[x↦],σ⊎{κ: c'(c')}⊢_ e ▹σ'Ω,σ⊎{y0jκ: c(m)} ⊢_ xye ▹σ'

[TA-CH]c'={(μc_1).c_2 | c_1.c_2∈c∧c_1=κ}
Ω,σ⊎{κκ':c(m)} ⊢_g κμ ▹σ⊎{κκ':c'(m)}

FV(b@x[j])=κxjj   1

FV(b@x[j])∩FV(e) =∅

σ(κxjj   1κ_1)=c(m)

Ω,σ⊢_ e ▹{κxjj   1κ_1:c'(m)}
Ω,σ⊢_g b@x[j]e ▹{κxjj   1κ_1:c”(m)}

\[
\begin{array}{l}
\overline{c''}=\{\tob{n}.1.c_2\;\bm{|}\;\tob{n}.d.c_1 \in \overline{c} \wedge \tob{n}.d.c_2 \in \overline{c'} \wedge b[\tob{n}/\kappa] \oplus d \wedge \slen{\tob{n}}=\slen{\kappa} \}
\\ \qquad\quad \cup \{\tob{n}.0.c_1\;\bm{|}\; \tob{n}.d.c_1 \in \overline{c} \wedge \neg (b[\tob{n}/\kappa] \oplus d) \wedge \slen{\tob{n}}=\slen{\kappa} \}
\end{array}
\]

type system. $\llbracket \mu \rrbracket c$ is the semantics of interpreting reversible expression $\mu$ in <Ref>. Boolean expression $b$ can be $a_1=a_2$, $a_1 < a_2$ or . $b[\tob{n}/\kappa]$ means that we treat $b$ as a $\mu$ expression, replace qubits in array $\kappa$ with bits in bitstring basis $\tob{n}$, and evaluate it to a Boolean value.
$\sigma(\kappa)=\tau$ is an abbreviation of $\sigma(\kappa)=\{\kappa\mapsto \tau\}$. $FV(-)$ produces a locus by union all qubits appearing in $-$.

<Ref> and <Ref> provide upgraded equivalence relations for type environments and quantum states.
The most significant improvement compared to the ones in <Ref> and <Ref> is the split of an $\tcht$ typed quantum state. Notice that splitting an $\tcht$ typed quantum state is equivalent to disentanglement, and we only provide one case for such splitting. The split function ($\texttt{spt}$) sees if every basis-ket in the $\tcht$ type has a common factor. If so, we can split the state by factoring in the common factor.
For example, $\ket{00}+\ket{10}$ can be disentangled as $(\ket{0}+\ket{1})\otimes \ket{0}$, as the common factor $\ket{0}$ is factored out from the original formula $\ket{00}+\ket{10}$.

<Ref> provides some rules in the upgraded type system. Other than the functionality discussed in <Ref>. The most significant difference is that we now need to track the basis-ket bitstrings appearing in $\tcht$, $\thadt$, and $\tcht$ typed values.
In rule TA-CH, the oracle $\mu$ is applied on $\kappa$ belonging to a locus $\kappa \sqcupplus \kappa'$. Correspondingly, the locus's type is $\tch{\overline{c}(m)}$, for each basis $c_1.c_2\in \overline{c}$, with $\slen{c_1}=\slen{\kappa}$, we apply $\mu$ on the $c_1$ and leave $c_2$ unchanged.
Here, we utilize the semantics that describes transitions from a $\texttt{Nor}$-typed quantum value to another $\texttt{Nor}$ one, and we generalize it to apply the semantic function on every element in the  type.
During the transition, the number of elements $m$ does not change.
Similarly, applying a partial measurement on range $y\srange{0}{j}$ of the locus $y\srange{0}{j}\sqcupplus\kappa$ in rule T-MeaN
can be viewed as an array filter, i.e., for an element, $c_1.c_2$ in set $\overline{c}$ of the type $\tch{\overline{c}(m)}$, with $\slen{c_1}=j$, we keep only the ones with $c_1=\tob{n}$ ($n$ is the measurement result) in the new set $\overline{c'}$ and recompute $\slen{\overline{c'}}$. In , the tracking procedure is to generate symbolic predicates that permit the production of the set $\overline{c'}(\slen{c'})$, not to produce such sets. If the predicates are not effectively trackable, we can always use $\infty$ to represent the set given in rule T-Mea.

In addition, the upgraded type system enforces equational properties of
quantum qubit loci through a partial order relation over type environments, including subtyping, qubit position mutation, merge, and split quantum loci.
This property is enforced with the additional equivalence relations in <Ref> and <Ref>.
Based on the new  type with the set $\overline{c_1}\times \overline{c_2}$,
the quantum conditional (T-If) creates a new set based on $\overline{c_1}\times \overline{c_2}$, i.e., for each element $\tob{n}.d.c$ in the set, with $\slen{\tob{n}}=\slen{\kappa_1}$, we compute Boolean guard $b$ value by substituting qubit variables in $b$ with the bitstring basis $\tob{n}$. The result $b[\tob{n} / \kappa_1] \oplus d$ is true or not ($d$ represents the bit value for the qubit at $x\srange{j}{j\,\splus\, 1}$); if it is true, we replace the $c$ basis by an updated basis by applying the semantics of the conditional body if we can learn about its semantics; otherwise, we keep $c$ to be the same.
In short, the quantum conditional behavior can be understood as applying a conditional map function on an $m$ 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 $b$.

§ TRANSLATION FROM TO FULL RULES

Ω[x↦];Υ;n⊢s[m/x] →ϵ
Ω;Υ;n⊢xms →ϵ

Ω[x↦];Υ;n⊢s[(r,n)/x] →ϵ
Ω;Υ;n⊢x(r,n)s →ϵ

Ω;Υ;n⊢κop →op(Υ(κ))

Ω;Υ;n⊢κμ →ϵ

Ω;Υ;n⊢κ →(Υ(κ))

Ω;Υ;n⊢s_1s_2 →ϵ_1ϵ_2

to translation rules (circuits are marked blue)

In addition to <Ref>, <Ref> provides the other compilation rules for the operations in <Ref>. In compiling the value and diffusion operations, we utilize the verified infrastructure <cit.> for the $\texttt{H}$, $\texttt{QFT}$, and diffusion circuits. The function $\Upsilon(\kappa)$ translates the locus $\kappa$ to a qubit array with the physical indices required in .
The last two rules in the first line show how a $\texttt{let}$-binding is handled for a $\cmode$ and $\mmode$ kind variable.
Similar to the type system, we assume that -binding introduces new variables, probably with proper variable renaming.
The rule for $\ssassign{\kappa}{}{\mu}$ describes an oracle application compilation, which is handled by the compiler <cit.>. The type system ensures that the qubits mentioned in $\mu$ are the same as qubits in locus $\kappa$ so that the translation does not rely on $\kappa$ itself.

§.§ The Limitation of the Dafny Classical Distribution Library

The is universal in terms of the power of expressing quantum programs
since all gates in the universal RzQ gate set $\{\texttt{H}, \texttt{X}, \texttt{RZ}, \texttt{CNOT}\}$.
can be defined by the state preparation operation,
$\texttt{X}$ and $\texttt{RZ}$ can be defined by the oracle operation,
and $\texttt{CNOT}$ gate can be defined by the quantum conditional in .
The measurement operation in allows us to define a computational basis ($\ket{0}$ and $\ket{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 we can utilize to verify all quantum programs, especially hybrid quantum-classical ones, automatically.
permits automated verification for programs in <Ref>, with some supporting library theorems in Dafny.
We can summarize a common pattern can verify from these programs as a structure $U;\texttt{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 by the methodology shown in this paper.

If programmers want to measure some qubits resulting in $(r,n)$, with $r$ being the probability and $n$ being the measurement result,
and then utilize the result $n$ as an input to another quantum program $s$; the 's proving power depends on the properties the programmers want to verify.
If the programmers only want to verify the post-state of executing $s$ with the input $n$, this scenario is perfect for .
On the other hand, if programmers want to know the probability of having the post-state of executing $s$ with the input probability of $r$, 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 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 hybrid quantum-classical programs.
Essentially, the '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 's proof system can perform proof automation on questioning
properties related to probability bounds such as the one above.

§ : AN ASSEMBLY LANGUAGE FOR QUANTUM ORACLES

The expression $\mu$ used in <Ref> places an additional wrapper on top of the expression $\iota$ given in <Ref>. Here, we first provide a step-by-step explanation of ; then show the additional wrapper in <Ref>.

is designed to express efficient quantum
oracles that can be easily tested and, if desired, proved
operations leverage both the standard
computational basis and an alternative basis connected by the quantum
Fourier transform (QFT).
's type system tracks the bases of variables in
programs, forbidding operations that would introduce
entanglement. states are therefore efficiently
represented, so programs can be effectively tested and are simpler to
verify and analyze. In addition, 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

This section presents states and the language's syntax,
semantics, typing, and soundness results. As a running example, the QFT
adder <cit.> is shown in <Ref>. The Coq
function rz_adder generates an program that adds two
natural numbers a and b, each of length n qubits.

@C=0.5em @R=0.75em
|a_n-1⟩         5                                 |a_n-1⟩

|a_n-2⟩             4                             |a_n-2⟩

⋮                                         ⋮

|a_0⟩                             1             |a_0⟩

|b_n-1⟩     5          3                 5     5^-1         |a_n-1 + b_n-1⟩

|b_n-2⟩                                     ^-1         |a_n-2 + b_n-2⟩

⋮                                         ⋮

|b_0⟩                                   ^-1          |a_0 + b_0⟩

Quantum circuit

Fixpoint rz_adder' (a b:var) (n:nat)
:= match n with
| 0 => ID (a,0)
| S m => CU (a,m) (SR m b);
rz_adder' a b m
Definition rz_adder (a b:var) (n:nat)
:= Rev a ; Rev b ; $\texttt{QFT}$ b ;
rz_adder' a b n;
$\texttt{QFT}^{-1}$ b; Rev b ; Rev a.

metaprogram (in Coq)

Example program: QFT-based adder

§.§ States

\[\hspace*{-0.5em}
\begin{array}{l>{$} p{1.2cm} <{$} c l}
\text{Bit} & b & ::= & 0 \mid 1 \\
\text{Natural number} & n & \in & \mathbb{N} \\
\text{Real} & r & \in & \mathbb{R}\\
\text{Phase} & \alpha(r) & ::= & e^{2\pi i r} \\
\text{Basis} & \tau & ::= & \texttt{Nor} \mid \texttt{Phi}\;n \\
\text{Unphased qubit} & \overline{q} & ::= & \ket{b} ~~\mid~~ \qket{r} \\
\text{Qubit} & q & ::= &\alpha(r) \overline{q}\\
\text{State (length $d$)} & \varphi & ::= & q_1 \otimes q_2 \otimes \cdots \otimes q_d
\end{array}
\]
\caption{\oqasm state syntax}
\label{fig:vqir-state}
\end{figure}

An \oqasm program state is represented according to the grammar in
\Cref{fig:vqir-state}. A state $\varphi$ of $d$ qubits is
a length-$d$ tuple of qubit values $q$; the state models the tensor
product of those values. This means that the size of $\varphi$ is
$O(d)$ where $d$ is the number of qubits. A $d$-qubit state in a
language like \sqir is represented as a length $2^d$ vector of complex
numbers, $O(2^d)$ 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

A qubit value $q$ has one of two forms $\overline{q}$, scaled by a
global phase $\alpha(r)$. The two forms depend on the \emph{basis} $\tau$ that the qubit is in---it could be either \texttt{Nor} or \texttt{Phi}. A \texttt{Nor} qubit has form
$\ket{b}$ (where $b \in \{ 0, 1 \}$), which is a
computational basis value.
A \texttt{Phi} qubit has the form $\qket{r} = \frac{1}{\sqrt{2}}(\ket{0}+\alpha(r)\ket{1})$, which is a value of the (A)QFT basis.
The number $n$ in \texttt{Phi}$\;n$ indicates the precision of the state $\varphi$.
As shown by~\citet{qft-adder}, 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.

\subsection{\oqasm Syntax, Typing, and Semantics}\label{sec:oqasm-syn}

\begin{figure}[t]
\begin{minipage}[t]{0.5\textwidth}
{\small \centering

$ \hspace*{-0.8em}
\begin{array}{llcl}
\text{Position} & p & ::= & (x,n) \qquad   \text{Nat. Num}~n
\qquad   \text{Variable}~x\\
\text{Instruction} & \instr & ::= & \iskip{p} \mid \inot{p}
\mid \irz[\lbrack -1 \rbrack]{n}{p} \mid \iseq{\instr}{\instr}\\
& & \mid &  \isr[\lbrack -1 \rbrack]{n}{x} \mid \iqft[\lbrack -1 \rbrack]{n}{x} \mid \ictrl{p}{\instr}  \\
& & \mid & \ilshift{x} \mid \irshift{x} \mid \irev{x}
\end{array}
\caption{\oqasm syntax. For an operator \texttt{OP}, $\texttt{OP}^{\lbrack -1 \rbrack}$ indicates that the operator has a built-in inverse available.}
\label{fig:vqir}
\end{minipage}
\hfill
\begin{minipage}[t]{0.45\textwidth}
\centering
\begin{tabular}{c@{$\quad=\quad$}c}
\begin{minipage}{0.3\textwidth}
\Small
\Qcircuit @C=0.5em @R=0.5em {
\lstick{} & \qw     & \multigate{4}{\texttt{SR m}} & \qw & \qw \\
\lstick{} & \qw     & \ghost{\texttt{SR m}}           & \qw & \qw \\
\lstick{} & \vdots & & \vdots & \\
\lstick{} & & & & \\
\lstick{} & \qw     & \ghost{\texttt{SR m}}           & \qw  & \qw
\end{minipage} &
\begin{minipage}{0.3\textwidth}
\Small
\Qcircuit @C=0.5em @R=0.5em {
\lstick{} & \qw     & \gate{\texttt{RZ (m+1)}} & \qw & \qw \\
\lstick{} & \qw     & \gate{\texttt{RZ m}}          & \qw & \qw \\
\lstick{} & & \vdots & & \\
\lstick{} & & & & \\
\lstick{} & & & & \\
\lstick{} & \qw     & \gate{\texttt{RZ 1}}           & \qw  & \qw
\end{minipage}
\end{tabular}
\caption{\texttt{SR} unfolds to a series of \texttt{RZ} instructions}
\label{fig:sr-meaning}
\end{minipage}
\end{figure}

\Cref{fig:vqir} presents \oqasm's syntax. An \oqasm program consists of
a sequence of instructions $\instr$. Each instruction applies an
operator to either a variable $x$, representing a group of qubits, or a \emph{position} $p$, which identifies a particular offset into a variable $x$.

The instructions in the first row correspond to simple single-qubit
quantum gates---$\iskip{p}$, $\inot{p}$, and $\irz[\lbrack -1 \rbrack]{n}{p}$
---and instruction sequencing.
The instructions in the next row apply to whole variables: $\iqft{n}{x}$
applies the AQFT to variable $x$ with $n$-bit precision and
$\iqft[-1]{n}{x}$ applies its inverse.
If $n$ equals the size of $x$, then the AQFT operation is exact.
$\isr[\lbrack -1 \rbrack]{n}{x}$
applies a series of \texttt{RZ} gates (\Cref{fig:sr-meaning}).
Operation $\ictrl{p}{\instr}$
applies instruction $\instr$ \emph{controlled} on qubit position
$p$. All of the operations in this row---\texttt{SR}, \texttt{QFT}, and \texttt{CU}---will be translated to multiple \sqir
gates. The function \coqe{rz_adder} in \Cref{fig:circuit-example}(b) uses
many of these instructions; e.g., it uses \texttt{QFT} and \texttt{QFT}$^{-1}$ and applies
\texttt{CU} to the $m$th position of variable \texttt{a} to control
instruction \texttt{SR m b}.

In the last row of \Cref{fig:vqir}, instructions $\ilshift{x}$,
$\irshift{x}$, and $\irev{x}$ are \emph{position shifting operations}.
Assuming that $x$ has $d$ qubits and $x_k$ represents the $k$-th qubit
state in $x$, $\texttt{Lshift}\;x$ changes the $k$-th qubit state to
$x_{(k + 1)\mmod d}$, $\texttt{Rshift}\;x$ changes it to
$x_{(k + d - 1)\mmod d}$, and \texttt{Rev} changes it to $x_{d-1-k}$. In
our implementation, shifting is \emph{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.

\begin{figure}[t]
\begin{minipage}[t]{0.6\textwidth}
\begin{mathpar}
\inferrule[X]{\Omegaty(x)=\texttt{Nor} \\ n < \Omegasz(x)}{\Sigma;\Omega \vdash \inot{(x,n)}\triangleright \Omega}

\inferrule[RZ]{\Omegaty(x)=\texttt{Nor} \\ n < \Omegasz(x)}{\Sigma;\Omega \vdash \irz{q}{(x,n)} \triangleright \Omega}

\inferrule[SR]{\Omegaty(x)=\tphi{n} \\ m < n}{\Sigma;\Omega \vdash \texttt{SR}\;m\;x\triangleright \Omega}

\inferrule[QFT]{\Omegaty(x)=\texttt{Nor}\\n \le \Omegasz(x)}{\Sigma; \Omega \vdash \iqft{n}{x}\triangleright \Omega[x\mapsto \tphi{n}]}

\inferrule[RQFT]{\Omegaty(x)=\tphi{n}\\n \le \Omegasz(x)}{\Sigma; \Omega \vdash \iqft[-1]{n}{x}\triangleright \Omega[x\mapsto \texttt{Nor}]}

\inferrule[CU]{\Omegaty(x)=\texttt{Nor} \\ \texttt{fresh}~(x,n)~\instr \\\\ \Sigma; \Omega\vdash \instr\triangleright \Omega \\ \texttt{neutral}(\instr)}{\Sigma; \Omega \vdash \texttt{CU}\;(x,n)\;\instr \triangleright \Omega}

\inferrule[LSH]{\Omegaty(x)=\texttt{Nor}}{\Sigma; \Omega \vdash \texttt{Lshift}\;x\triangleright \Omega}

\inferrule[SEQ]{\Sigma; \Omega\vdash \instr_1\triangleright \Omega' \\ \Sigma; \Omega'\vdash \instr_2\triangleright \Omega''}{\Sigma; \Omega \vdash \instr_1\;;\;\instr_2\triangleright \Omega''}

\end{mathpar}
\caption{Select \oqasm typing rules}
\label{fig:exp-well-typed}
\end{minipage}
\hfill
\begin{minipage}[t]{0.38\textwidth}
\begin{center}\hspace*{-1em}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=3.2cm,
\tikzstyle{every state}=[fill=black,draw=none,text=white]

\node[state] (A)              {$\texttt{Nor}$};
\node[state]         (C) [left of=A] {$\tphi{n}$};

\path (A) edge [loop above]            node {$\Big\{\begin{array}{l}\texttt{ID},~\texttt{X},~\texttt{RZ}^{\lbrack -1 \rbrack},~\texttt{CU},\\
\texttt{Rev},\texttt{Lshift},\texttt{Rshift}\end{array}\Big\}$} (A)
edge   node [above] {\{$\texttt{QFT}\;n$\}} (C);
\path (C) edge [loop above]            node {$\{\texttt{ID},~\texttt{SR}^{\lbrack -1 \rbrack}\}$} (C)
edge  [bend right]             node {$\{\texttt{QFT}^{-1}\;n\}$} (A);
\end{tikzpicture}
\end{center}
\caption{Type rules' state machine}
\label{fig:state-machine}
\end{minipage}
\end{figure}

\myparagraph{Typing}
\label{sec:vqir-typing}

In \oqasm, typing is concerning a \emph{type environment}
$\Omega$ and a predefined \emph{size
environment} $\Sigma$, which map \oqasm
variables to their basis and size (number of qubits), respectively.
The typing judgment is written $\Sigma; \Omega\vdash \instr \triangleright \Omega'$ which
states that $\instr$ is well-typed under $\Omega$ and $\Sigma$, and
transforms the variables' bases to be as in $\Omega'$ ($\Sigma$ is unchanged).
$\Sigma$ is fixed because the number of qubits in execution is always fixed.
It is generated in the high-level language compiler, such as \sourcelang in \cite{oracleoopsla}.
The algorithm generates $\Sigma$ by taking an \sourcelang program and scanning through
all the variable initialization statements.
Select type rules are given in \Cref{fig:exp-well-typed};
the rules not shown (for \texttt{ID}, \texttt{Rshift}, \texttt{Rev}, \texttt{RZ}$^{-1}$, and \texttt{SR}$^{-1}$) are similar.

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 \rulelab{X}) and that any control qubit is distinct from the
target(s) (the \texttt{fresh} premise in
\rulelab{CU}).  This latter property enforces the quantum
\emph{no-cloning rule}.
For example, applying the \texttt{CU} in \code{rz\_adder'} (\Cref{fig:circuit-example}) is valid
because position \code{a,m} is distinct from variable \code{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
\Cref{fig:state-machine}. For example, $\texttt{QFT}\;n$ transforms a variable from \texttt{Nor} to
$\tphi{n}$ (rule \rulelab{QFT}), while $\texttt{QFT}^{-1}\;n$
transforms it from $\tphi{n}$ back to \texttt{Nor} (rule
\rulelab{RQFT}). Position shifting operations
are disallowed on variables $x$ in
the \texttt{Phi} basis because the qubits that makeup $x$ are
internally related (see \Cref{appx:well-formed}) and cannot be rearranged. Indeed, applying a
\texttt{Lshift} and then a $\texttt{QFT}^{-1}$ on $x$ in \texttt{Phi}
would entangle $x$'s qubits.

Third, the type system enforces that the effect of position-shifting
operations can be statically tracked. The \texttt{neutral} condition of
\rulelab{CU} requires that any shifting within $\instr$ is restored by the time it
For example, $\sseq{\ictrl{p}{(\ilshift{x})}}{\inot{(x,0)}}$ is not well-typed because knowing the final physical position of qubit $(x,0)$ would require statically knowing the value of $p$.
On the other hand, the program $\sseq{\ictrl{c}{(\sseq{\ilshift{x}}{\sseq{\inot{(x,0)}}{\irshift{x}}})}}{\inot{(x,0)}}$ is well-typed
because the effect of the \texttt{Lshift} is ``undone'' by an \texttt{Rshift} inside the body of the \texttt{CU}.

\myparagraph{Semantics}\label{sec:pqasm-dsem}

\begin{figure}[t]
\[
\begin{array}{lll}
\llbracket \iskip{p} \rrbracket\varphi &= \varphi\\[0.2em]

\llbracket \inot{(x, i)} \rrbracket\varphi &= \app{\uparrow\xsem(\downarrow\varphi(x,i))}{\varphi}{(x,i)}
& \texttt{where  }\xsem(\ket{0})=\ket{1} \qquad\, \xsem(\ket{1})=\ket{0}
\\[0.5em]

\llbracket \ictrl{(x,i)}{\instr} \rrbracket\varphi &=  \csem(\downarrow\varphi(x,i),\instr,\varphi)
\texttt{where  }
\csem({\ket{0}},{\instr},\varphi)=\varphi\quad\;\,
\csem({\ket{1}},{\instr},\varphi)=\llbracket \instr \rrbracket\varphi
\\[0.4em]

\llbracket \irz{m}{(x,i)} \rrbracket\varphi &= \app{\uparrow {\rsem}({m},\downarrow\varphi(x,i))}{\varphi}{(x,i)}
&\texttt{where  }{\rsem}(m,\ket{0})=\ket{0} \; \quad{\rsem}(m,\ket{1})=\alpha(\frac{1}{2^m})\ket{1}
\\[0.5em]

\llbracket \irz[-1]{m}{(x,i)} \rrbracket\varphi &= \app{\uparrow {\rrsem}({m},\downarrow\varphi(x,i))}{\varphi}{(x,i)}
&\texttt{where  }{\rrsem}(m,\ket{0})=\ket{0}
\quad{\rrsem}(m,\ket{1})=\alpha(-\frac{1}{2^m})\ket{1}
\\[0.5em]

\llbracket \isr{m}{x} \rrbracket\varphi &
\multicolumn{2}{l}{= \app{\uparrow \qket{r_i+\frac{1}{2^{m-i+1}}}}{\varphi}{\forall i \le m.\;(x,i)}
\qquad \texttt{when  }
\downarrow\varphi(x,i) = \qket{r_i}}\\[0.5em]

\llbracket \isr[-1]{m}{x} \rrbracket\varphi&\multicolumn{2}{l}{= \app{\uparrow \qket{r_i-\frac{1}{2^{m-i+1}}}}{\varphi}{\forall i \le m.\;(x,i)}
\qquad \texttt{when  }
\downarrow\varphi(x,i) = \qket{r_i}}\\[0.5em]

\llbracket \iqft{n}{x} \rrbracket\varphi &= \app{\uparrow\qsem(\Sigma(x),\downarrow\varphi(x),n)}{\varphi}{x}
& \texttt{where  }\qsem(i,\ket{y},n)=\bigotimes_{k=0}^{i-1}(\qket{\frac{y}{2^{n-k}}})
\\[0.5em]

\llbracket \iqft[-1]{n}{x} \rrbracket\varphi &=  \app{\uparrow\qsem^{-1}(\Sigma(x),\downarrow\varphi(x),n)}{\varphi}{x}
\\[0.5em]

\llbracket \ilshift{x} \rrbracket\varphi &= \app{{\psem}_{l}(\varphi(x))}{\varphi}{x}
\texttt{where  }{\psem}_{l}(q_0\otimes q_1\otimes \cdots \otimes q_{n-1})=q_{n-1}\otimes q_0\otimes q_1 \otimes \cdots
\\[0.5em]

\llbracket \irshift{x} \rrbracket\varphi &= \app{{\psem}_{r}(\varphi(x))}{\varphi}{x}
\texttt{where  }{\psem}_{r}(q_0\otimes q_1\otimes \cdots \otimes q_{n-1})=q_1\otimes \cdots \otimes q_{n-1} \otimes q_0
\\[0.5em]

\llbracket \irev{x} \rrbracket\varphi &= \app{{\psem}_{a}(\varphi(x))}{\varphi}{x}
\texttt{where  }{\psem}_{a}(q_0\otimes \cdots \otimes q_{n-1})=q_{n-1}\otimes \cdots \otimes q_0
\\[0.5em]

\llbracket \iota_1; \iota_2 \rrbracket\varphi &= \llbracket \iota_2 \rrbracket (\llbracket \iota_1 \rrbracket\varphi)
\end{array}
\]
\begin{array}{l}
\\[0.2em]
\downarrow \alpha(b)\overline{q}=\overline{q}
\qquad
\downarrow (q_1\otimes \cdots \otimes q_n) = \downarrow q_1\otimes \cdots \otimes \downarrow q_n
\\[0.2em]
\app{\uparrow \overline{q}}{\varphi}{(x,i)}=\app{\alpha(b)\overline{q}}{\varphi}{(x,i)}
\qquad \texttt{where  }\varphi(x,i)=\alpha(b)\overline{q_i}
\\[0.2em]
\app{\uparrow \alpha(b_1)\overline{q}}{\varphi}{(x,i)}=\app{\alpha(b_1+b_2)\overline{q}}{\varphi}{(x,i)}
\qquad \texttt{where  }\varphi(x,i)=\alpha(b_2)\overline{q_i}
\\[0.2em]
\app{q_x}{\varphi}{x}=\app{q_{(x,i)}}{\varphi}{\forall i < \Sigma(x).\;(x,i)}
\\[0.2em]
\app{\uparrow q_x}{\varphi}{x}=\app{\uparrow q_{(x,i)}}{\varphi}{\forall i < \Sigma(x).\;(x,i)}
\end{array}
\caption{\oqasm semantics}
\label{fig:deno-sem}
\end{figure}

The semantics of an \oqasm program is a partial function
$\llbracket\rrbracket$ from
an instruction $\instr$ and input state $\varphi$ to an output state
$\varphi'$, written
$\llbracket \instr \rrbracket\varphi=\varphi'$, shown in \Cref{fig:deno-sem}.

Recall that a state $\varphi$ is a tuple of $d$ qubit values,
modeling the tensor product $q_1\otimes \cdots \otimes q_d$.
The rules implicitly map each variable $x$ to a
range of qubits in the state, e.g.,
$\varphi(x)$ corresponds to some sub-state $q_k\otimes \cdots \otimes q_{k+n-1}$
where $\Omegasz(x)=n$.
Many of the rules in \Cref{fig:deno-sem} update a \emph{portion} of a
state. $\app{q_{(x,i)}}{\varphi}{(x,i)}$ updates the $i$-th
qubit of variable $x$ to be the (single-qubit) state $q_{(x,i)}$, and
$\app{q_{x}}{\varphi}{x}$ to update variable $x$ according to
the qubit \emph{tuple} $q_x$.
$\app{\uparrow q_{(x,i)}}{\varphi}{(x,i)}$ and $\app{\uparrow q_{x}}{\varphi}{x}$ are similar, except that they also accumulate the previous global phase of $\varphi(x,i)$ (or $\varphi(x)$).
$\downarrow$ is to convert a qubit $\alpha(b)\overline{q}$ to an unphased qubit $\overline{q}$.

Function $\xsem$ updates the state of a single
qubit according to the rules for the standard quantum gate $X$.
\texttt{cu} is a conditional operation
depending on the \texttt{Nor}-basis qubit $(x,i)$.
\texttt{RZ} (or $\texttt{RZ}^{-1}$) is an z-axis phase rotation operation.
Since it applies to \texttt{Nor}-basis, it applies a global phase.
By \Cref{thm:sem-same}, when it is compiled to \sqir,
the global phase might be turned into a local one.
For example, to prepare the state $\sum_{j=0}^{2^n\sminus 1}(-i)^x\ket{x}$ \cite{ChildsNAND},
a series of Hadamard gates are applied, followed by several controlled-\texttt{RZ} gates on $x$,
where the controlled-\texttt{RZ} gates are definable by \oqasm.
\texttt{SR} (or
$\texttt{SR}^{-1}$) applies an $m+1$ series of \texttt{RZ} (or
$\texttt{RZ}^{-1}$) rotations where the $i$-th rotation
applies a phase of $\alpha({\frac{1}{2^{m-i+1}}})$
(or $\alpha({-\frac{1}{2^{m-i+1}}})$).
$\qsem$ applies an approximate quantum Fourier transform; $\ket{y}$ is an abbreviation of
$\ket{b_1}\otimes \cdots \otimes \ket{b_i}$ (assuming $\Omegasz(y)=i$) and $n$ is the degree of approximation.
If $n = i$, then the operation is the standard<EMAIL_ADDRESS>Otherwise, each qubit in the state is mapped to $\qket{\frac{y}{2^{n-k}}}$, which is equal to $\frac{1}{\sqrt{2}}(\ket{0} + \alpha(\frac{y}{2^{n-k}})\ket{1})$ when $k < n$ and $\frac{1}{\sqrt{2}}(\ket{0} + \ket{1}) = \ket{+}$ when $n \leq k$ (since $\alpha(n) = 1$ for any natural number $n$).
$\qsem^{-1}$ is the inverse function of $\qsem$.
Note that the input state to $\qsem^{-1}$ is guaranteed to have the form $\bigotimes_{k=0}^{i-1}(\qket{\frac{y}{2^{n-k}}})$ because it has type $\tphi{n}$.
$\psem_l$, $\psem_r$, and
$\psem_a$ are the semantics for \itext{Lshift},
\itext{Rshift}, and \itext{Rev}, respectively.

\subsection{\oqasm Metatheory}\label{sec:metatheory}

\myparagraph{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.

\begin{definition}[Well-formed \oqasm state]\label{appx:well-formed}\rm
A state $\varphi$ is \emph{well-formed}, written
$\Sigma;\Omega \vdash \varphi$, iff:
\begin{itemize}
\item For every $x \in \Omega$ such that $\Omegaty(x) = \texttt{Nor}$,
for every $k <\Omegasz(x)$, $\varphi(x,k)$ has the form

\item For every $x \in \Omega$ such that $\Omegaty(x) = \tphi{n}$ and $n \le \Omegasz(x)$,
there exists a value $\upsilon$ such that for
every $k < \Omegasz(x)$, $\varphi(x,k)$ has the form
$\alpha(r)\qket{\frac{\upsilon}{ 2^{n- k}}}$.\footnote{Note that $\Phi(x) = \Phi(x + n)$, where the integer $n$ refers to phase $2 \pi n$; so multiple choices of $\upsilon$ are possible.}
\end{itemize}
\end{definition}

\noindent
Type soundness is stated as follows; the proof is by induction on $\instr$ and is mechanized in Coq.

\begin{theorem}\label{thm:type-sound-oqasm}\rm[\oqasm type soundness]
If $\Sigma; \Omega \vdash \instr \triangleright \Omega'$ and $\Sigma;\Omega \vdash \varphi$ then there exists $\varphi'$ such that $\llbracket \instr \rrbracket\varphi=\varphi'$ and $\Sigma;\Omega' \vdash \varphi'$.
\end{theorem}

\myparagraph{Algebra}
Mathematically, the set of well-formed $d$-qubit \oqasm states for a given $\Omega$ can be interpreted as a subset $\hsp{S}^d$ of a $2^d$-dimensional Hilbert space $\hsp{H}^d$ \footnote{A \emph{Hilbert space} is a vector space with an inner product that is complete with respect to the norm defined by the inner product. $\hsp{S}^d$ is a sub\emph{set}, not a sub\emph{space} of $\hsp{H}^d$ because $\hsp{S}^d$ is not closed under addition: Adding two well-formed states can produce a state that is not well-formed.}. The semantics function $\llbracket \rrbracket$ can be interpreted as a $2^d \times 2^d$ unitary matrix, as is standard when representing the semantics of programs without measurement~\cite{PQPC}.
Because \oqasm's semantics can be viewed as a unitary matrix, correctness properties extend by linearity from $\hsp{S}^d$ to $\hsp{H}^d$---an oracle that performs addition for classical \texttt{Nor} inputs will also perform addition over a superposition of \texttt{Nor} inputs. The following statement is proved: $\hsp{S}^d$ is closed under well-typed \oqasm programs.

Given a qubit size map $\Sigma$ and type environment $\Omega$, the set of \oqasm programs that are well-typed concerning $\Sigma$ and $\Omega$ (i.e., $\Sigma;\Omega \vdash \instr \triangleright \Omega'$) form an algebraic structure $(\{\instr\},\Sigma, \Omega,\hsp{S}^d)$, where $\{\instr\}$ defines the set of valid program syntax, such that there exists $\Omega'$, $\Sigma;\Omega \vdash \instr \triangleright \Omega'$ for all $\instr$ in $\{\instr\}$; $\hsp{S}^d$ is the set of $d$-qubit states on which programs $\instr\in \{\instr\}$ are run, and are well-formed ($\Sigma;\Omega \vdash \varphi$) according to \Cref{appx:well-formed}.
From the \oqasm semantics and the type soundness theorem, for all $\instr \in \{\instr\}$ and $\varphi \in \hsp{S}^d$, such that $\Sigma;\Omega \vdash \instr \triangleright \Omega'$ and $\Sigma;\Omega \vdash \varphi$, and $\llbracket \instr \rrbracket\varphi=\varphi'$, $\Sigma;\Omega' \vdash \varphi'$, and $\varphi' \in \hsp{S}^d$. Thus, $(\{\instr\},\Sigma, \Omega,\hsp{S}^d)$, where $\{\instr\}$ defines a groupoid.

The groupoid can be certainly extended to another algebraic structure $(\{\instr'\},\Sigma,\hsp{H}^d)$, where $\hsp{H}^d$ is a general $2^d$ dimensional Hilbert space $\hsp{H}^d$ and $\{\instr'\}$ is a universal set of quantum gate operations.
Clearly, the following is true: $\hsp{S}^d \subseteq \hsp{H}^d$ and $\{\instr\} \subseteq \{\instr'\}$, because sets $\hsp{H}^d$ and $\{\instr'\}$ can be acquired by removing the well-formed ($\Sigma;\Omega \vdash \varphi$) and well-typed ($\Sigma;\Omega \vdash \instr \triangleright \Omega'$) definitions for $\hsp{S}^d$ and $\{\instr\}$, respectively.
$(\{\instr'\},\Sigma,\hsp{H}^d)$ is a groupoid because every \oqasm operation is valid in a traditional quantum language like \sqir. The following two theorems are to connect \oqasm operations with operations in the general Hilbert space:

\begin{theorem}\label{thm:subgroupoid}\rm
$(\{\instr\},\Sigma, \Omega,\hsp{S}^d) \subseteq (\{\instr\},\Sigma,\hsp{H}^d)$ is a subgroupoid.
\end{theorem}

\begin{theorem}\label{thm:sem-same}\rm
Let $\ket{y}$ be an abbreviation of $\bigotimes_{m=0}^{d-1} \alpha(r_m) \ket{b_m}$ for $b_m \in \{0,1\}$.
If for every $i\in [0,2^d)$, $\llbracket \instr \rrbracket\ket{y_i}=\ket{y'_i}$, then $\llbracket \instr \rrbracket (\sum_{i=0}^{2^d-1} \ket{y_i})=\sum_{i=0}^{2^d-1} \ket{y'_i}$.
\end{theorem}

The following theorems are proved as corollaries of the compilation correctness theorem from \oqasm to \sqir (\cite{oracleoopsla}).
\Cref{thm:subgroupoid} suggests that the space $\hsp{S}^d$ is closed under the application of any well-typed \oqasm operation.
\Cref{thm:sem-same} says that \oqasm oracles can be safely applied to superpositions over classical states.\footnote{Note that a superposition over classical states can describe \emph{any} quantum state, including entangled states.}

\begin{figure}[t]
\begin{mathpar}
\inferrule[ ]{}{\inot{(x,n)}\xrightarrow{\text{inv}} \inot{(x,n)}}

\inferrule[  ]{}{\texttt{SR}\;m\;x\xrightarrow{\text{inv}} \texttt{SR}^{-1}\;m\;x}

\inferrule[ ]{}{\iqft{n}{x} \xrightarrow{\text{inv}}  \iqft[-1]{n}{x}}

\inferrule[ ]{}{\texttt{Lshift}\;x\xrightarrow{\text{inv}} \texttt{Rshift}\;x}

\inferrule[ ]{\instr \xrightarrow{\text{inv}} \instr'}{\texttt{CU}\;(x,n)\;\instr \xrightarrow{\text{inv}} \texttt{CU}\;(x,n)\;\instr'}

\inferrule[ ]{\instr_1 \xrightarrow{\text{inv}} \instr'_1 \\ \instr_2 \xrightarrow{\text{inv}} \instr'_2}{\instr_1\;;\;\instr_2\xrightarrow{\text{inv}} \instr'_2\;;\;\instr'_1}

\end{mathpar}
\caption{Select \oqasm inversion rules}
\label{fig:exp-reversed-fun}
\end{figure}

\begin{figure}[t]
\centering
\begin{tabular}{c@{$\quad=\quad$}c@{\qquad}c@{$\quad=\quad$}c}
\begin{minipage}{0.25\textwidth}
\footnotesize
\Qcircuit @C=0.25em @R=0.35em {
& \qw & \multigate{3}{(x+a)_n} & \qw \\
& \vdots & & \\
& & & \\
& \qw & \ghost{(x+a)_n} & \qw \\
\end{minipage}
\begin{minipage}{.45\textwidth}
\footnotesize
\Qcircuit @C=0.35em @R=0.55em {
& \qw & \gate{\texttt{SR}\;0} & \multigate{3}{\texttt{SR}\;1} & \qw & \qw & \qw & \multigate{5}{\texttt{SR}\;(n-1)} & \qw  \\
& & & & & \dots & & &  \\
& \qw & \qw  &  \ghost{\texttt{SR}\; 1} & \qw & \qw & \qw & \ghost{\texttt{SR}\;(n-1)} & \qw \\
& & & & & & & &  \\
& & & & & & & &  \\
& \qw & \qw & \qw & \qw & \qw & \qw & \ghost{\texttt{SR}\;(n-1)}  & \qw
\end{minipage}
\begin{minipage}{0.25\textwidth}
\footnotesize
\Qcircuit @C=0.25em @R=0.35em {
& \qw & \multigate{3}{(x-a)_n} & \qw \\
& \vdots & & \\
& & & \\
& \qw & \ghost{(x+a)_n} & \qw \\
\end{minipage}
\begin{minipage}{.45\textwidth}
\footnotesize
\Qcircuit @C=0.35em @R=0.55em {
& \qw & \multigate{5}{\texttt{SR}^{-1} (n-1)} & \qw & \qw & \qw & \multigate{3}{\texttt{SR}^{-1} 1} & \gate{\texttt{SR}^{-1} 0} & \qw \\
&     &                                  &     & \dots &   &                              &                      &   \\
& \qw & \ghost{\texttt{SR}^{-1} (n-1)}        & \qw & \qw   & \qw & \ghost{\texttt{SR}^{-1} 1} & \qw & \qw  \\
& & & & & & & &  \\
& & & & & & & &  \\
& \qw & \ghost{\texttt{SR}^{-1} (n-1)} & \qw & \qw & \qw & \qw & \qw & \qw
\end{minipage}
\end{tabular}
\caption{Addition/subtraction circuits are inverses}
\label{fig:circuit-add-sub}
\end{figure}

\oqasm programs are easily invertible, as shown by the rules in \Cref{fig:exp-reversed-fun}.
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 (\Cref{fig:exp-reversed-fun}).
This allows us to reuse the proof of addition in the proof of subtraction.
The inversion function satisfies the following properties:

\begin{theorem}\label{thm:reversibility}\rm[Type reversibility]
For any well-typed program $\instr$, such that $\Sigma; \Omega \vdash \instr \triangleright \Omega'$, its inverse $\instr'$, where $\instr \xrightarrow{\text{inv}} \instr'$, is also well-typed and $\Sigma;\Omega' \vdash \instr' \triangleright \Omega$. Moreover, $\llbracket \instr ; \instr' \rrbracket \varphi=\varphi$.
\end{theorem}

\subsection{Explaining the Oracle Expression $\mu$ in \qafny }\label{sec:exp-mu}

The \oqasm expression $\mu$ used in \Cref{fig:vqimp} places an additional wrapper on top of the \oqasm expression $\iota$ given in \Cref{fig:vqir}. The wrapper is given as:

\[
\mu \triangleq \lambda \overline{p} .\, \iota
\]

Here $\overline{p}$ is a list of positions, and $\iota$ is an \oqasm instruction in \Cref{fig:vqir}. Here, we require all qubit positions mentioned in $\iota$ to be in $\overline{p}$. Ranges and loci are directly related to positions. Given a range $x\srange{n}{m}$, it is equal to a list of positions: $(x,n),(x,n\splus 1),...,(x,m\sminus 1)$, while a locus is a list of disjoint ranges and it can be understood as concatenations of different ranges in the locus. For simplicity, we can understand the above $\mu$ definition as $\lambda \kappa .\, \iota$ by rearranging the positions as a locus.
In the predicate $FV(\Omega,\mu)=\kappa$ in rule \rulelab{TA-CH} in \Cref{fig:exp-sessiontype},
function $FV(\Omega,\mu)$ returns $\kappa$, which means that the $\mu$ lambda expression is given as $\lambda \kappa .\, \iota$.
Given a $\mu$ expression as $\lambda \kappa .\, \iota$,
to evaluate an oracle expression $\ssassign{\kappa'}{}{\mu}$, we actually do the following:

\[
\ssassign{\kappa'}{}{\lambda \kappa . \, \iota} \longrightarrow \denote{\iota[\kappa'/\kappa]}
\]

Here, we replace the positions $\kappa$ in $\iota$ with qubits mentioned in locus $\kappa'$ and then evaluate the expression $\iota[\kappa'/\kappa]$. In the paper, we also utilize some oracle expressions from OQIMP \cite{oracleoopsla}, the arithmetic operation language based on \oqasm. The expression $ \qass{y\srange{0}{n}\;}{\;y\srange{0}{n}\,\splus\, 1}$ is actually a syntactic sugar for the expression:
$\qass{y\srange{0}{n}\;}{\;(\lambda u\srange{0}{n} . \,\qass{u\;}{\;u\, \splus\, 1})}$. Here, the expression $\qass{u\;}{\;u\, \splus\, 1}$ is an OQIMP expression, meaning we apply the function $\lambda \,x. \,x\splus 1$ to a qubit array $u$, where $u$ is a $n$-length qubit array.
In addition, the expression $\qass{y\srange{0}{n}\;}{a^{2^j}\cdot y\srange{0}{n}\;\mmod\; N}$ is a syntactic sugar for the expression: $\qass{y\srange{0}{n}\;}{\;(\lambda u\srange{0}{n} . \, \qass{u\;}{\;a^{2^j}\cdot u\;\mmod\; N})}$.

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 $\lambda u\srange{0}{n}\sqcupplus w\srange{0}{n}.\,\qass{u\;}{\;(u \;\mmod\; m,w)}$, meaning that $u$ and $w$ are $n$-length qubit array. we compute the modulo operation $u \;\mmod\; m$ and put the result in $u$, while $w$ is an additional ancillary qubits required for the computation.
Then, the oracle operation for the modulo function in \qafny is written as:

\[
\qass{x\srange{0}{n}\sqcupplus y\srange{0}{n}\;}{\;(\lambda u\srange{0}{n}\sqcupplus w\srange{0}{n}.\,\qass{u\;}{\;(u \;\mmod\; m,w)})}
\]

In \qafny, the expression computes $x \;\mmod\; m$ and then assigns the value to the range $x\srange{0}{n}$, while $y$ is an array of additional ancillary qubits required for the computation.
In the Shor's example in \Cref{appx:shors}, the oracle application ($\qass{y\srange{0}{n}\;}{\;a^{2^j}\cdot y\srange{0}{n}\;\mmod\; N}$) 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 $\ket{0}$.
All oracle examples in the paper 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.

\end{document}