You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+9-10Lines changed: 9 additions & 10 deletions
Original file line number
Diff line number
Diff line change
@@ -1,6 +1,6 @@
1
1
# AutoQ: An automata-based C++ tool for quantum program verification.
2
2
3
-
AutoQ is a command-line utility written in C++ for verifying partial correctness of quantum programs automatically based on non-deterministic finite tree automata (NFTA) along with the concept of Hoare-style proof systems.
3
+
AutoQ is a command-line utility written in C++ for verifying partial correctness of quantum programs automatically based on non-deterministic finite tree automata (NFTA) along with the concept of Hoare-style proof systems.
4
4
5
5
Consider a triple \{ $P$ \} $C$ \{ $Q$ \}, where $P$ and $Q$ are the pre- and post-condition recognizing sets of (pure) quantum states (represented by NFTA) and $C$ is a quantum program. Let $\mathcal L(.)$ denote the mapping from a condition $x$ to the set of all quantum states satisfying $x$ (characterized by $x$). Then AutoQ essentially checks whether all the quantum states in $\mathcal L(P)$ reach some state in $\mathcal L(Q)$ after the program $C$ is executed. If we further let $C(.)$ denote the mapping from a condition $x$ to the evolution of $x$ after a program segment $C$ is executed, then AutoQ simply checks whether $\mathcal L(C(P)) \subseteq \mathcal L(Q)$.
6
6
@@ -15,31 +15,30 @@ Currently, for Linux (Ubuntu/Debian) and macOS, the dependency of AutoQ can be b
15
15
make release
16
16
make test
17
17
```
18
-
The first command compiles the source code with compiler optimizations enabled, while the second command runs several unit tests to verify the correctness of the implementation. If you need to compile the library for debugging, you can replace make release with `make debug`.
18
+
The first command compiles the source code with compiler optimizations enabled, while the second command runs several unit tests to verify the correctness of the implementation. If you need to compile the library for debugging, you can replace `make release` with `make debug`.
19
19
20
20
---
21
21
22
22
## Command-Line
23
-
There are 5 modes listed in the following help message, which can be accessed by typing their respective subcommands. Each mode (subcommand) also has its own usage instructions.
23
+
There are 4 modes listed in the following help message, which can be accessed by typing their respective subcommands. Each mode (subcommand) also has its own usage instructions.
24
24
```
25
25
$ ./build/cli/autoq -h
26
26
AutoQ: An automata-based C++ tool for quantum program verification.
27
27
Usage: autoq [OPTIONS] [SUBCOMMAND]
28
28
29
29
Options:
30
-
-h,--help Print this help message and exit
30
+
-h,--help Print this help message and exit.
31
31
32
32
Subcommands:
33
-
exC Concrete Execution
34
-
verC Concrete Verification
35
-
exS Symbolic Execution
36
-
verS Symbolic Verification
37
-
eq Equivalence Checking
33
+
ex Execute a quantum circuit with a given precondition.
34
+
ver Verify the execution result against a given postcondition.
35
+
eq Check equivalence of two given quantum circuits.
36
+
print Print the set of quantum states.
38
37
```
39
38
```
40
39
$ ./build/cli/autoq ver benchmarks/all/Grover/03/pre.lsta benchmarks/all/Grover/03/circuit.qasm benchmarks/all/Grover/03/post.lsta
41
40
The quantum program has [6] qubits and [54] gates.
42
-
The verification process [passed] in [0.0s] with [16MB] memory usage.
41
+
The verification process [passed] in [0.0s] with [7MB] memory usage.
43
42
```
44
43
AutoQ provides two file extensions, *.hsl and *.lsta, for users to indicate the format they use to describe a set of quantum states. The simpler format is *.hsl, which does not require users to have a background in NFTA. However, since our current implementation of *.hsl has not yet been optimized, we strongly recommend using *.lsta as the number of qubits increases. The detailed formats can be found in the following documents.
Copy file name to clipboardExpand all lines: docs/hsl_description.md
+18-9Lines changed: 18 additions & 9 deletions
Original file line number
Diff line number
Diff line change
@@ -1,30 +1,30 @@
1
1
## How to describe a set of quantum states? `*.hsl`
2
2
3
-
This file may contain multiple lines. Each line represents a quantum state. A quantum state is naturally described by a linear combination of computational basis states with complex coefficients. Coefficients here can be expressed in [addition `+`], [subtraction `-`], [multiplication `*`] operations on [rationals], $[e^{i2\pi(r)}\ |\ r=k/8,\ k\in\mathbb Z]$and the [exponentiation `^`] operation with "nonnegative" exponents. Operator precedence follows the standard convention. You can also do $/\sqrt2 ^ k$ by writing `/ sqrt2 ^ k` after the above operations are already done if you wish. Nevertheless, due to the automatic scaling in the verification process, users do not need $/\sqrt2 ^ k$.
3
+
This file may contain multiple lines. Each line represents a quantum state. A quantum state is naturally described by a linear combination of computational basis states with complex coefficients. Coefficients here can be expressed in [addition `+`], [subtraction `-`], [multiplication `*`] operations on [rationals], $[e^{i2\pi(r)}\ |\ r=k/8,\ k\in\mathbb Z]$, $[e^{i\pi(r)}\ |\ r=k/4,\ k\in\mathbb Z]$ and the [exponentiation `^`] operation with "nonnegative" exponents. Operator precedence follows the standard convention. You can also do $/\sqrt2 ^ k$ by writing `/ sqrt2 ^ k` after the above operations are already done if you wish. <!--Nevertheless, due to the automatic scaling in the verification process, users do not need $/\sqrt2 ^ k$.-->
This file describes two quantum states $-e^{i2\pi(1/8)}\ |01\rangle + (-1 - e^{i2\pi(2/8)} - 2\cdot e^{i2\pi(3/8)})\ |10\rangle + e^{i2\pi(3/8)}\ |11\rangle$ and $e^{i2\pi(1/8)}\ |00\rangle - e^{i2\pi(3/8)}\ |10\rangle + (1 + e^{i2\pi(2/8)} - 2\cdot e^{i2\pi(3/8)})\ |11\rangle$. If there are so many states having the same amplitude, you can also use the "wildcard state" $|\*\rangle$ at the end of a line to denote all other computational basis states whose amplitudes have not been specified so far. For instance, $0.5\ |00\rangle - 0.5\ |*\rangle = 0.5\ |00\rangle - 0.5\ |01\rangle - 0.5\ |10\rangle - 0.5\ |11\rangle$.
12
+
This file contains two quantum states $-e^{i2\pi(1/8)}\ |01\rangle + (-1 - e^{i2\pi(2/8)} - 2\cdot e^{i2\pi(3/8)})\ |10\rangle + e^{i2\pi(3/8)}\ |11\rangle$ and $e^{i\pi(1/4)}\ |00\rangle - e^{i\pi(3/4)}\ |10\rangle + (1 + e^{i\pi(1/2)} - 2\cdot e^{i\pi(3/4)})\ |11\rangle$. If there are so many states having the same amplitude, you can also use the "wildcard state" $|\*\rangle$ at the end of a line to denote all other computational basis states whose amplitudes have not been specified so far. For instance, $0.5\ |00\rangle - 0.5\ |*\rangle = 0.5\ |00\rangle - 0.5\ |01\rangle - 0.5\ |10\rangle - 0.5\ |11\rangle$.
13
13
14
14
### # Constants
15
15
For simplicity, one can define some complex constants in the *Constants* section before the *Extended Dirac* section, and the example becomes
16
16
```
17
17
Constants
18
18
c1 := ei2pi(1/8)
19
19
c2 := ei2pi(2/8)
20
-
c3 := ei2pi(3/8)
20
+
c3 := eipi(3/4)
21
21
Extended Dirac
22
22
(-1 + -1 * c2 + -2 * c3) |10> + c3 |11> - c1 |01>
23
23
c1 |00> + (1 + 1 * c2 + -2 * c3) |11> - c3 |10>
24
24
```
25
25
26
26
### # Variables and Constraints
27
-
Nonconstant tokens not defined in the Constants section are automatically regarded as *free symbolic variables*. These variables may have some constraints such as being nonzero. One can impose some constraints on these variables in the *Constraints* section after the *Extended Dirac* section. For instance,
27
+
Nonconstant tokens not defined in the Constants section are automatically regarded as *free symbolic variables*. These variables may have some constraints such as not being zero. One can impose some constraints on these variables in the *Constraints* section after the *Extended Dirac* section. For instance,
28
28
```
29
29
Constants
30
30
c0 := 0
@@ -41,10 +41,19 @@ One may want to take the absolute value of a ***real*** number in some applicati
41
41
42
42
We say a description file contains a quantum state $|s\rangle$ only if $|s\rangle$ satisfies all the boolean formulae in the *Constraints* section.
43
43
44
-
### # Tensor Products and Existentially Quantified Variables
45
-
For convenience, AutoQ also supports the ***tensor product operator***`#`. The usage is very easy: just put `#` between two quantum states $|x\rangle$ and $|y\rangle$ in a line to denote the quantum state $|x\rangle \otimes |y\rangle$. AutoQ also supports the ***existentially quantified variable***`\/ |i|=n :` over all $n$-bit binary strings. This variable is used to constrain all basis states $|i\rangle$ appearing after this notation in a line. If there is some quantum state $|s\rangle$ satisfying this line for some $i$, then we say $|s\rangle$ is described in this line.
44
+
### # Logical $\lor$ Operator
45
+
We use the logical $\lor$ operator to compute the union of the two sets of quantum states connected by this operator. For instance, `|00> \/ |01>` means that $|00\rangle$ and $|01\rangle$ are both included in the file. Please note that you can also use `V` in place of `\/` to obtain the same result.
46
46
47
-
One more example to get a closer look at `*.hsl`.
47
+
### # Existentially Quantified Variables
48
+
Many real-world sets of quantum states have some common patterns in qubits. In light of this, AutoQ supports the ***existentially quantified variable***`\/|i|=n:` over all $n$-bit binary strings. This variable is used to constrain all substrings `i` and `i'` (i.e., $1$'s complement of `i`) appearing after this notation in a line. If there is some quantum state $|s\rangle$ matches the pattern in this line for some $\\{i\in\\{0,1\\}^n\\}$, then we say $|s\rangle$ is contained in this line. For instance, `\/|i|=2: a|i0> + b|i'1>` describes the following four states $\\{a|000\rangle+b|111\rangle,\ a|010\rangle+b|101\rangle,\ a|100\rangle+b|011\rangle,\ a|110\rangle+b|001\rangle\\}$.
49
+
50
+
### # Tensor Products
51
+
For convenience, AutoQ also supports the ***tensor product operator***`#`. The usage is very easy: just put `#` between the two sets of quantum states $S_1$ and $S_2$ in a line to denote the resulting set of quantum states $\\{|x\rangle \otimes |y\rangle\ |\ |x\rangle\in S_1,\ |y\rangle\in S_2\\}$.
52
+
53
+
### # Operator Precedence
54
+
The ***tensor product operator***`#` has the lowest precedence. That is, they split a line into multiple units. In each unit, logical $\lor$ operators and existentially quantified variables cannot be used at the same time. Besides, substrings `i` and `i'` in different units are invisible to each other.
55
+
56
+
<!--One more example to get a closer look at `*.hsl`.
Finally, we should be noticed that not all strings described by `*.hsl` are valid quantum states. For instance, the sum of absolute squares of amplitudes of all computational basis states may not be $1$.
Since the underlying structure of a set of quantum states is still an NFTA in AutoQ, we reserve the `*.lsta` format for users to describe a set of quantum states with an NFTA. The *Constants* and *Constraints* sections remain, but the *Extended Dirac* section should be replaced with two new sections *Root States* and *Transitions* now. (Unary) states in an NFTA can be arbitrary strings (no need to enclose with double quotation marks).
4
+
5
+
### # Root States
6
+
This section is responsible for specifying a set of root states. It should contain only one line starting with "Root States" and ending with a set of root states separated by whitespaces.
7
+
8
+
### # Transitions
9
+
This section is responsible for specifying a set of transitions. One transition per line. Notice that the extension name `*.lsta` stands for Level-Synchronized (Nondeterministic Finite) Tree Automata which means that each transition is associated with a nonnegative integer denoting a set of choices in AutoQ. A (bottom-up) transition $f(q_1, q_2, ..., q_n) \to q$ associated with a set of choices $C$ is written as `[f,C](q1, q2, ..., qn) -> q`. Each pair of transitions `[f1,C1](...) -> q` and `[f2,C2](...) -> q` with the same `q` must satisfy $C_1 \\& C_2 = 0$. In each layer of all used transitions for an accepted quantum state, the bitwise $\\&$ of all used $C$'s must be positive. In this tool, a symbol can only be a positive integer $i$ with arity $2$ for specifying the $i$-th qubit or any expression describing a complex number with arity $0$ for specifying the amplitude of some computational basis states.
0 commit comments