<!--
Copyright 2022 Yingte Xu
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-->
# NQPV - Nondeterministic Quantum Program Verifier
**Version: 0.4b1**
NQPV is an verification assistant tool for the formal verification of nondeterministic quantum programs. Different former tools which are based on theorem provers, the goal of NQPV is to mitigate the overload of the user and help complete particular verification tasks efficiently.
## Install
NQPV is written in pure Python. It can be easily installed through PyPI. To do this, after installing Python3 and pip, open a command prompt and run this command:
```
pip install NQPV
```
Github repository: https://github.com/LucianoXu/NQPV. Example codes can be found there.
Dependence: this tool depends on the following python packages.
- ply
- numpy
- cvxpy
## Introduction
For a general introduction to the formal verification of quantum programs using Hoare logic, please refer to this article:
*Ying M. Floyd--hoare logic for quantum programs[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 2012, 33(6): 1-49.*
This assistant tool is an implementation of [not published yet], and please refer to this article for more detailed information. Briefly speaking, formal verification means to check whether particular properties hold for the given program, with the solid gurantee from mathematics. This tool, NQPV, mainly focuses on the partial correctness of quantum programs, which says that initial quantum states satisfying the precondition will also satisfy the postcondition when they terminate after the program computation.
Here, the quantum programs in consideration consist of skip, abort, initialization, unitary transformation, if, while and nondeterministic choice. The conditions (or assertions) are represented by sets of proper Hermitian operators. These will be introduced in the following.
This tool does not depend on any existing proof assistants, and there are several pros and cons due to this approach. NQPV will not be as expressive as other verfication tools that based on proof assistants, and can only deal with numerical operators. However, the proof hints from the user is the natural program code, and NQPV supports a high degree of automation.
To work with this verifier, an individual folder is needed, which contains the quantum program and the operators used in the program. The verifier will check the program's grammar, verify the correctness property automatically.
## NQPV : Hello World
Here is a hello-world example of NQPV. Create a new python script with the following content, and run the script **at the same folder**. In this example, the script creates a ".nqpv" file, indicating the verification description, which is later processed in the python script by the *verify* method.
**Important Note:** we strongly recommand to run the python script at the same folder, meaning the current path of the command prompt is the same folder that the script is in. This is mainly for the consideration of file operation, since the *open* method in Python operates according to the command prompt path.
```Python
import nqpv
code = '''
def pf := proof [q] :
{ P0[q] };
q *= X;
{ P1[q] }
end
show pf end
'''
fp = open("example.nqpv","w")
fp.write(code)
fp.close()
nqpv.entrance.verify("example.nqpv")
```
The expected output should be:
```
(example, line 8)
proof [q] :
{ P0[q] };
{ P0[q] };
[q] *= X;
{ P1[q] }
```
which is actually the output message of the *show* command. This example verifies the correctness formula
$$
\{\ket{0}_{q}\bra{0}\}\ q\ *= X\ \{\ket{1}_{q}\bra{1}\}
$$
by defining a corresponding proof term, and the automatically generated proof outlines are shown afterwards.
## Verification Language - Scopes and Commands
NQPV uses a language to organize and carry out the verification task.
This language uses *variables* to store and represent essential items, such as quantum operators, programs or correctness proofs. Variables are stored and managed in *scopes*, which are also variables themselves. Therefore a scope can contain subscopes as its variables, forming a variable hierarchy. Variables use *identifiers* as their names, which follows the same rule as that in C or Python (regular expression: '[a-zA-Z_][a-zA-Z_0-9]*').
We use *commands* to manipulate the proof system.
### Scopes
A *Scope* is a variable environment, containing the related program descriptions and calculation results.
When the verifier processes a *".npqv"* file, it opens up a global scope called *"global"*, which contains the preloaded operators variables. In a ".nqpv" file, with the command
```
show global end
```
the processing output should be something like
```
(prog, line 1)
<scope global.>
EPS : 1e-07 ;
SDP precision : 1e-09 ;
SILENT : True ;
IDENTIVAL_VAR_CHECK : True ;
OPT_PRESERVING : True
I operator 1 qubit
X operator 1 qubit
Y operator 1 qubit
Z operator 1 qubit
H operator 1 qubit
CX operator 2 qubit
CH operator 2 qubit
SWAP operator 2 qubit
CCX operator 3 qubit
Idiv2 operator 1 qubit
Zero operator 1 qubit
P0 operator 1 qubit
P0div2 operator 1 qubit
P1 operator 1 qubit
P1div2 operator 1 qubit
Pp operator 1 qubit
Ppdiv2 operator 1 qubit
Pm operator 1 qubit
Pmdiv2 operator 1 qubit
Eq01_2 operator 2 qubit
Neq01_2 operator 2 qubit
Eq01_3 operator 3 qubit
M01 measurement 1 qubit
M10 measurement 1 qubit
Mpm measurement 1 qubit
Mmp measurement 1 qubit
MEq01_2 measurement 2 qubit
MEq10_2 measurement 2 qubit
prog scope
```
The description contains the local settings for the scope and the variables in the scope. In fact, the processing result of a ".npqv" file is also returned as a scope.
Variables of the local scope will overlap those in the global scope with the same name, which works just like that in C or Python. We can also refer to a vairable by its path, such as:
```
show I end
show global.I end
```
will print the same result.
To better organize the proofs, we can also define scopes. For example, the example code of hello world can be rewritten as:
```
def hello_world :=
def pf := proof [q] :
{ P0[q] };
q *= X;
{ P1[q] }
end
end
// Comment: the command in the next line is illegal.
// show pf end
show hello_world.pf end
```
### Commands
Commands are excuted in a scope.
Currently, the commands in NQPV are separated into three groups:
- definition: including commands for defining different variables
- show: to show detailed information of variables
- save: to save a generated operator as a binary file
- setting: used to adjust the settings for verification
#### Command : **def**
The command **def** defines a variable. The syntax is :
```
def <identifier> := <expression> end
```
The name of the variable is determined by the *identifier*, and its value is determined by *expression*. There are several kinds of expression:
- proof hint : we will focus on it in the next section.
- loaded operator : the verifier loads a numpy ".npy" file as the operator value.
- scope : a new sub-scope will be defined.
**loaded operator**: example code. Of course, there should exists the binary file at the specified location. The location is relative to the ".nqpv" module file.
```
def Hpost := load "Hpost.npy" end
show Hpost end
```
**Note:** The numpy ndarray for quantum operators here are in a special form. For a $n$-qubit operator, the corresponding numpy object should be a $2n$ rank tensor, with distychus indices. What's more, the first $n$ indices corresponds to the ket space, and the second $n$ indices corresponds to the bra space. The qubit-mapping is like this: high address qubits are at the front. (It may be a little abstract, but you can show several preloaded standard operators to discover the restrain.)
**scope**: example code already shown in the last subsection.
#### Command : **show**
The usage of the *show* command is simple. It just outputs the expression. The syntax is:
```
show <expression> end
```
Example codes include:
```
show CX end
show global end
show
proof [q] :
{ P0[q] };
q *= X;
{ P1[q] }
end
```
#### Command : **save**
During a verification, predicates of intermediate weakest preconditions will be automatially generated and preseved in the scope. We can save the as numpy ".npy" binary files for later analysis.
The syntax is:
```
save <variable> at <address> end
```
An example code is:
```
def pf :=
proof [q] :
{ P0[q] };
q *= X;
{ P1[q] }
end
save VAR0 at "var0.npy" end
```
#### Command : **settings**
A scope contains the settings for the verification. There are three settings:
- EPS (float) : controls the precision of equivalence between float numbers.
- SDP_PRECISION (float) : controls the precision of the SDP solver.
- SILENT (**true** or **false**) : controls whether the intermediate procedures are output during the verification. This is for the purpose of monitoring a time consuming task.
- IDENTICAL_VAR_CHECK (**true** or **false**) : controls whether identical variables (operators) are detected to keep the naming more informative. Default is on, and this function is especially time consuming. Turn if off for verification of programs with large qubit number.
The syntax of **setting** is:
```
setting [EPS | SDP_PRECISION | SILENT] := <value> end
```
and this command will take effect immediately in the current scope. An example code:
```
// expl.nqpv
setting SILENT := false end
show global.expl end
def pf := proof [q] :
{ P0[q] };
q *= X;
{ P1[q] }
end
```
And a verbose output of the procedure is provided.
## Quantum Program - Constructing the proof
The verification of program correctness is through the definition of a proof term. Here in NQPV, we do not need to provide a proof of full details (like what is required in CoqQ or QHLProver). Instead, we write a *"proof hint"*, which briefly describes the correctness formula we want to proof, and provides the required loop invariants.
In the following we will explain the syntax of a proof hint.
If you found the formal description of the grammar hard to understand, you may refer to the examples for an intuitive idea.
The expression of a proof hint should be:
> proof_hint ::= proof [ id_ls ] : <br>
> { herm_ls } <br>
> sequence <br>
> { herm_ls }
<!--
> $$
\begin{aligned}
\mathrm{prog} ::=\ & \mathrm{qvar}\ [\ \mathrm{id\_ls}\ ]\\
& \{\ \mathrm{herm\_ls} \}\\
& \mathrm{sequence} \\
& \{\ \mathrm{herm\_ls} \}
\end{aligned}
> $$
-->
The first line "proof [id_ls]" indicates all the quantum variables. The second and forth line indicates the pre and post conditions. The third line indicates the sequence of verification.
"id_ls" is a list of one or more identifiers.
> id_ls ::= <br>
> id <br>
> | id_ls id
<!--
> $$
\begin{aligned}
\mathrm{id\_ls} ::=\ & \mathrm{id} \\
&|\ \mathrm{id\_ls}\quad \mathrm{id}
\end{aligned}
> $$
-->
"herm_ls" is a list of one or more operators.
> herm_ls ::= <br>
> id [ id_ls ] <br>
> | herm_ls id [ id_ls ]
<!--
> $$
\begin{aligned}
\mathrm{herm\_ls} ::=\ & \mathrm{id}\ [\ \mathrm{id\_ls}\ ]\\
&|\ \mathrm{herm\_ls}\quad \mathrm{id}\ [\ \mathrm{id\_ls}\ ]
\end{aligned}
> $$
-->
"id [ id_ls ]" describes a particular operator, with the identifier list specifying the Hilbert space of the operator. For example,
$$
\mathrm{P0}\ [\ \mathrm{q1}\ ]
$$
may refer to a Herimitian operator |0><0| on the space of variable q1, and
$$
\mathrm{CX}\ [\ \mathrm{q2}\ \mathrm{q1}\ ]
$$
may refer to the controlled-X gate with q2 being the control and q1 being the target.
"sequence" is a list of verification tasks (programs or intermediate conditions), which are composed by sequential combination.
> sequence ::= <br>
> sentence <br>
> | sequence ; sentence
<!--
> $$
\begin{aligned}
\mathrm{sequence} ::=\ & \mathrm{sentence}\\
&|\ \mathrm{sequence};\ \mathrm{sentence}
\end{aligned}
> $$
-->
And "sentence" is just a piece of verification task, which can be skip, abort, initialization, unitary transformation, if, while, nondeterministic choice. Besides, it can also be a quantum predicate (as the intermediate condition), or a former proof term.
> sentence ::= <br>
> skip <br>
> | abort <br>
> | [ id_ls ] := 0 <br>
> | [ id_ls ] *= id <br>
> | if id [ id_ls ] then sequence else sequence end <br>
> | { inv : herm_ls } while id [ id_ls ] do sequence end <br>
> | ( sequence \# sequence \# ... \# sequence) <br>
> | { herm_ls }
<!--
> $$
\begin{aligned}
\mathrm{sentence} ::=\ & \mathrm{skip}\\
&|\ \mathrm{abort}\\
&|\ [\ \mathrm{id\_ls}\ ] := 0\\
&|\ [\ \mathrm{id\_ls}\ ] *= \mathrm{id}\\
&|\ \mathrm{if}\ \mathrm{id}\ [\ \mathrm{id\_ls}\ ]\ \mathrm{then}\ \mathrm{sequence}\ \mathrm{else}\ \mathrm{sequence}\ \mathrm{end}\\
&|\ \{\ \mathrm{inv}:\ \mathrm{herm\_ls}\ \}\\
&\quad \mathrm{while}\ \mathrm{id}\ [\ \mathrm{id\_ls}\ ]\ \mathrm{do}\ \mathrm{sequence}\ \mathrm{end}\\
&|\ (\ \mathrm{sequence}\ \#\ \mathrm{sequence}\ )
\end{aligned}
> $$
-->
The last three rules of the grammar above correspond to the (multiple) nondeterministic choice, the use of former proof and the intermediate predicate, respectively.
## Program Verification Procedure
Here the syntactic analysis checks whether the content can be properly interpreted with the grammar. The semantic analysis afterwards checks whether there is any problem in the meaning of the verification task. It will mainly examine the following aspects:
- whether all operators mentioned can be found,
- whether there are repeat identifiers in some identifier list, and
- whether the qubit number of operators and identifier lists matches. For example, CX [ q1 ] or X [ q1 q2 ] will not be acceptable.
If there are syntactic or semantic errors, the verifier will stop there, providing the error information.
The verification utilizes a technique called *backward predicate transformation*. If there is not any while structures in the program, the whole calculation can be done automatically. That is, the weakest (liberal) precondition with respect to the given postcondition will be derived and compared with the desired precondition. Based on this, the verification tool will give a definite conclusion between the following two:
- Property holds.
- Property does not hold.
However, if there are while structures, the automatical calculation relies on the specified *loop invariant* from the user. The verifier will first check whether it is a valid loop invariant. If not, the verification will stop and the failure will be reported. Otherwise, the corresponding precondition is derivied and the procedure continues. In this case, the verification result can be:
- Property holds.
- Property cannot be determined. A suitable loop invariant may be sufficient.
The tool can only give a definite conclusion if the property does hold.
## Examples
This section gives some examples of verification tasks. The source can be found in the Github repository.
### Error Correction Code
This example shows that the error correction code here is robust against single big-flip errors, for a random single qubit pure state.
1. Create a folder called "error_correction_code"
2. In this folder, create a file called "example.nqpv" with the following content:
```
def Hrand := load "Hrand.npy" end
def pf := proof[q] :
{ Hrand[q] };
[q1 q2] :=0;
[q q1] *= CX;
[q q2] *= CX;
(skip # q *= X # q1 *= X # q2 *= X);
[q q1] *= CX;
[q q2] *= CX;
[q1 q2 q] *= CCX;
{ Hrand[q] }
end
show pf end
```
3. In the same folder of "error_correction_code", create a python script "example.py" with the following content:
```Python
import nqpv
import numpy as np
# create a Hermitian on a random ket
theta = np.random.rand() * np.pi
phi = np.random.rand() * np.pi * 2
ket = np.array([np.cos(theta), np.sin(theta)*np.exp(phi*1j)])
Hrand = np.outer(ket, np.conj(ket))
np.save("Hrand", Hrand)
# verify
nqpv.verify("./prog.nqpv")
```
4. Run the python script in the folder. (Note that the run path also needs to be the folder.)
### Deutsch Algorithm
1. Create a folder called "Deutsch_algorithm"
2. In this folder, create a file called "prog.nqpv" with the following content:
```
def Hpost := load "Hpost.npy" end
def pf := proof[q q1] :
{ I[q] };
[q1 q2] :=0;
q1 *= H;
q2 *= X;
q2 *= H;
if M01[q] then
(
[q1 q2] *= CX
#
q1 *= X;
[q1 q2] *= CX;
q1 *= X
)
else
(
skip
#
q2 *= X
)
end;
q1 *= H;
if M01[q1] then
skip
else
skip
end;
{ Hpost[q q1] }
end
show pf end
```
3. In the same folder of "Deutsch_algorithm", create a python script "example.py" with the following content:
```Python
import nqpv
import numpy as np
# create the required operators
Hpost = np.array([[1., 0., 0., 0.],
[0., 0., 0., 0.],
[0., 0., 0., 0.],
[0., 0., 0., 1.]])
np.save("./Hpost", Hpost.reshape((2,2,2,2)))
# verify
nqpv.verify("./prog.nqpv")
```
4. Run the python script in the folder. (Note that the run path also needs to be the folder.)
### Quantum Walk
1. Create a folder called "quantum_walk"
2. In this folder, create a file called "prog.nqpv" with the following content:
```
def invN := load "invN.npy" end
def MQWalk := load "MQWalk.npy" end
def W1 := load "W1.npy" end
def W2 := load "W2.npy" end
def pf := proof[q1 q2] :
{ I[q1] };
[q1 q2] :=0;
{inv: invN[q1 q2]};
while MQWalk[q1 q2] do
(
[q1 q2] *= W1; [q1 q2] *= W2
#
[q1 q2] *= W2; [q1 q2] *= W1
)
end;
{ Zero[q1] }
end
show pf end
```
3. In the same folder of "quantum_walk", create a python script "example.py" with the following content:
```Python
import nqpv
import numpy as np
# create the required operators
W1 = np.array([[1., 1., 0., -1.],
[1., -1., 1., 0.],
[0., 1., 1., 1.],
[1., 0., -1., 1.]]) / np.sqrt(3)
W2 = np.array([[1., 1., 0., 1.],
[-1., 1., -1., 0.],
[0., 1., 1., -1.],
[1., 0., -1., -1.]]) / np.sqrt(3)
np.save("W1", W1.reshape((2,2,2,2)))
np.save("W2", W2.reshape((2,2,2,2)))
P0 = np.array([[0., 0., 0., 0.],
[0., 0., 0., 0.],
[0., 0., 1., 0.],
[0., 0., 0., 0.]])
P1 = np.array([[1., 0., 0., 0.],
[0., 1., 0., 0.],
[0., 0., 0., 0.],
[0., 0., 0., 1.]])
MQWalk = np.stack((P1,P0), axis = 0)
np.save("MQWalk", MQWalk.reshape((2,2,2,2,2)))
# the invariant N
invN = np.array([[1., 0., 0., 0.],
[0., 0.5, 0., 0.5],
[0., 0., 0., 0.],
[0., 0.5, 0., 0.5]])
np.save("invN", invN.reshape((2,2,2,2)))
# verify
nqpv.verify("prog.nqpv")
```
4. Run the python script in the folder. (Note that the run path also needs to be the folder.)
## Contact
If you find any bug or have any questions, do not hesitate to contact lucianoxu@foxmail.com.
## Development Log
### 0.4b1
- We refactored this software and deleted some redundant functions, including subprogram, subproof and module import.
### 0.3b9
- Now the verification tool will try to find an existing variable for the particular value before creating a new one with an auto name.
Raw data
{
"_id": null,
"home_page": "https://github.com/LucianoXu/NQPV",
"name": "NQPV",
"maintainer": "",
"docs_url": null,
"requires_python": "",
"maintainer_email": "",
"keywords": "quantum programs,program verification,automatic theorem proving",
"author": "Yingte Xu",
"author_email": "lucianoxu@foxmail.com",
"download_url": "https://files.pythonhosted.org/packages/01/3a/2843a99750a3a95881f8ddf2cb416c4621bbc8ea295818d10ef9cacedae8/NQPV-0.4b1.tar.gz",
"platform": "Windows",
"description": "<!--\r\n Copyright 2022 Yingte Xu\r\n Licensed under the Apache License, Version 2.0 (the \"License\");\r\n you may not use this file except in compliance with the License.\r\n You may obtain a copy of the License at\r\n\r\n http://www.apache.org/licenses/LICENSE-2.0\r\n\r\n Unless required by applicable law or agreed to in writing, software\r\n distributed under the License is distributed on an \"AS IS\" BASIS,\r\n WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\r\n See the License for the specific language governing permissions and\r\n limitations under the License.\r\n-->\r\n\r\n# NQPV - Nondeterministic Quantum Program Verifier\r\n\r\n**Version: 0.4b1**\r\n\r\nNQPV is an verification assistant tool for the formal verification of nondeterministic quantum programs. Different former tools which are based on theorem provers, the goal of NQPV is to mitigate the overload of the user and help complete particular verification tasks efficiently.\r\n\r\n## Install\r\nNQPV is written in pure Python. It can be easily installed through PyPI. To do this, after installing Python3 and pip, open a command prompt and run this command:\r\n```\r\npip install NQPV\r\n```\r\n\r\nGithub repository: https://github.com/LucianoXu/NQPV. Example codes can be found there.\r\n\r\nDependence: this tool depends on the following python packages.\r\n- ply\r\n- numpy\r\n- cvxpy\r\n\r\n## Introduction\r\nFor a general introduction to the formal verification of quantum programs using Hoare logic, please refer to this article:\r\n\r\n*Ying M. Floyd--hoare logic for quantum programs[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 2012, 33(6): 1-49.*\r\n\r\nThis assistant tool is an implementation of [not published yet], and please refer to this article for more detailed information. Briefly speaking, formal verification means to check whether particular properties hold for the given program, with the solid gurantee from mathematics. This tool, NQPV, mainly focuses on the partial correctness of quantum programs, which says that initial quantum states satisfying the precondition will also satisfy the postcondition when they terminate after the program computation. \r\n\r\nHere, the quantum programs in consideration consist of skip, abort, initialization, unitary transformation, if, while and nondeterministic choice. The conditions (or assertions) are represented by sets of proper Hermitian operators. These will be introduced in the following.\r\n\r\nThis tool does not depend on any existing proof assistants, and there are several pros and cons due to this approach. NQPV will not be as expressive as other verfication tools that based on proof assistants, and can only deal with numerical operators. However, the proof hints from the user is the natural program code, and NQPV supports a high degree of automation.\r\n\r\nTo work with this verifier, an individual folder is needed, which contains the quantum program and the operators used in the program. The verifier will check the program's grammar, verify the correctness property automatically.\r\n\r\n\r\n## NQPV : Hello World\r\n\r\nHere is a hello-world example of NQPV. Create a new python script with the following content, and run the script **at the same folder**. In this example, the script creates a \".nqpv\" file, indicating the verification description, which is later processed in the python script by the *verify* method.\r\n\r\n**Important Note:** we strongly recommand to run the python script at the same folder, meaning the current path of the command prompt is the same folder that the script is in. This is mainly for the consideration of file operation, since the *open* method in Python operates according to the command prompt path.\r\n\r\n```Python\r\nimport nqpv\r\n\r\ncode = '''\r\ndef pf := proof [q] :\r\n { P0[q] };\r\n q *= X;\r\n { P1[q] }\r\nend\r\n\r\nshow pf end\r\n'''\r\n\r\nfp = open(\"example.nqpv\",\"w\")\r\nfp.write(code)\r\nfp.close()\r\n\r\nnqpv.entrance.verify(\"example.nqpv\")\r\n```\r\n\r\nThe expected output should be:\r\n```\r\n\r\n (example, line 8)\r\n\r\nproof [q] :\r\n { P0[q] };\r\n\r\n { P0[q] };\r\n [q] *= X;\r\n\r\n { P1[q] }\r\n\r\n```\r\nwhich is actually the output message of the *show* command. This example verifies the correctness formula\r\n$$\r\n\\{\\ket{0}_{q}\\bra{0}\\}\\ q\\ *= X\\ \\{\\ket{1}_{q}\\bra{1}\\}\r\n$$\r\nby defining a corresponding proof term, and the automatically generated proof outlines are shown afterwards.\r\n\r\n\r\n## Verification Language - Scopes and Commands\r\n\r\nNQPV uses a language to organize and carry out the verification task. \r\n\r\nThis language uses *variables* to store and represent essential items, such as quantum operators, programs or correctness proofs. Variables are stored and managed in *scopes*, which are also variables themselves. Therefore a scope can contain subscopes as its variables, forming a variable hierarchy. Variables use *identifiers* as their names, which follows the same rule as that in C or Python (regular expression: '[a-zA-Z_][a-zA-Z_0-9]*').\r\n\r\nWe use *commands* to manipulate the proof system.\r\n\r\n\r\n### Scopes\r\nA *Scope* is a variable environment, containing the related program descriptions and calculation results.\r\n\r\nWhen the verifier processes a *\".npqv\"* file, it opens up a global scope called *\"global\"*, which contains the preloaded operators variables. In a \".nqpv\" file, with the command\r\n\r\n```\r\nshow global end\r\n```\r\n\r\nthe processing output should be something like \r\n```\r\n\r\n (prog, line 1) \r\n<scope global.>\r\nEPS : 1e-07 ;\r\nSDP precision : 1e-09 ;\r\nSILENT : True ;\r\nIDENTIVAL_VAR_CHECK : True ;\r\nOPT_PRESERVING : True\r\n I operator 1 qubit\r\n X operator 1 qubit\r\n Y operator 1 qubit\r\n Z operator 1 qubit\r\n H operator 1 qubit\r\n CX operator 2 qubit\r\n CH operator 2 qubit\r\n SWAP operator 2 qubit\r\n CCX operator 3 qubit\r\n Idiv2 operator 1 qubit\r\n Zero operator 1 qubit\r\n P0 operator 1 qubit\r\n P0div2 operator 1 qubit\r\n P1 operator 1 qubit\r\n P1div2 operator 1 qubit\r\n Pp operator 1 qubit\r\n Ppdiv2 operator 1 qubit\r\n Pm operator 1 qubit\r\n Pmdiv2 operator 1 qubit\r\n Eq01_2 operator 2 qubit\r\n Neq01_2 operator 2 qubit\r\n Eq01_3 operator 3 qubit\r\n M01 measurement 1 qubit\r\n M10 measurement 1 qubit\r\n Mpm measurement 1 qubit\r\n Mmp measurement 1 qubit\r\n MEq01_2 measurement 2 qubit\r\n MEq10_2 measurement 2 qubit\r\n prog scope\r\n\r\n```\r\nThe description contains the local settings for the scope and the variables in the scope. In fact, the processing result of a \".npqv\" file is also returned as a scope.\r\n\r\nVariables of the local scope will overlap those in the global scope with the same name, which works just like that in C or Python. We can also refer to a vairable by its path, such as:\r\n```\r\nshow I end\r\nshow global.I end\r\n```\r\nwill print the same result.\r\n\r\nTo better organize the proofs, we can also define scopes. For example, the example code of hello world can be rewritten as:\r\n```\r\ndef hello_world :=\r\n def pf := proof [q] :\r\n { P0[q] };\r\n q *= X;\r\n { P1[q] }\r\n end\r\nend\r\n\r\n// Comment: the command in the next line is illegal.\r\n// show pf end\r\nshow hello_world.pf end\r\n```\r\n\r\n### Commands\r\nCommands are excuted in a scope.\r\n\r\nCurrently, the commands in NQPV are separated into three groups:\r\n- definition: including commands for defining different variables\r\n- show: to show detailed information of variables\r\n- save: to save a generated operator as a binary file\r\n- setting: used to adjust the settings for verification\r\n\r\n#### Command : **def**\r\nThe command **def** defines a variable. The syntax is :\r\n```\r\ndef <identifier> := <expression> end\r\n```\r\nThe name of the variable is determined by the *identifier*, and its value is determined by *expression*. There are several kinds of expression:\r\n- proof hint : we will focus on it in the next section.\r\n- loaded operator : the verifier loads a numpy \".npy\" file as the operator value.\r\n- scope : a new sub-scope will be defined.\r\n\r\n**loaded operator**: example code. Of course, there should exists the binary file at the specified location. The location is relative to the \".nqpv\" module file.\r\n```\r\ndef Hpost := load \"Hpost.npy\" end\r\nshow Hpost end\r\n```\r\n**Note:** The numpy ndarray for quantum operators here are in a special form. For a $n$-qubit operator, the corresponding numpy object should be a $2n$ rank tensor, with distychus indices. What's more, the first $n$ indices corresponds to the ket space, and the second $n$ indices corresponds to the bra space. The qubit-mapping is like this: high address qubits are at the front. (It may be a little abstract, but you can show several preloaded standard operators to discover the restrain.)\r\n\r\n**scope**: example code already shown in the last subsection.\r\n\r\n\r\n#### Command : **show**\r\nThe usage of the *show* command is simple. It just outputs the expression. The syntax is:\r\n\r\n```\r\nshow <expression> end\r\n```\r\n\r\nExample codes include:\r\n```\r\nshow CX end\r\nshow global end\r\nshow\r\n proof [q] :\r\n { P0[q] };\r\n q *= X;\r\n { P1[q] }\r\nend\r\n```\r\n#### Command : **save**\r\nDuring a verification, predicates of intermediate weakest preconditions will be automatially generated and preseved in the scope. We can save the as numpy \".npy\" binary files for later analysis.\r\n\r\nThe syntax is:\r\n```\r\nsave <variable> at <address> end\r\n```\r\n\r\nAn example code is:\r\n```\r\ndef pf := \r\n proof [q] :\r\n { P0[q] };\r\n q *= X;\r\n { P1[q] }\r\nend\r\n\r\nsave VAR0 at \"var0.npy\" end\r\n```\r\n\r\n#### Command : **settings**\r\nA scope contains the settings for the verification. There are three settings:\r\n- EPS (float) : controls the precision of equivalence between float numbers.\r\n- SDP_PRECISION (float) : controls the precision of the SDP solver.\r\n- SILENT (**true** or **false**) : controls whether the intermediate procedures are output during the verification. This is for the purpose of monitoring a time consuming task.\r\n- IDENTICAL_VAR_CHECK (**true** or **false**) : controls whether identical variables (operators) are detected to keep the naming more informative. Default is on, and this function is especially time consuming. Turn if off for verification of programs with large qubit number.\r\n \r\nThe syntax of **setting** is:\r\n```\r\nsetting [EPS | SDP_PRECISION | SILENT] := <value> end\r\n```\r\nand this command will take effect immediately in the current scope. An example code:\r\n```\r\n// expl.nqpv\r\nsetting SILENT := false end\r\nshow global.expl end\r\ndef pf := proof [q] :\r\n { P0[q] };\r\n q *= X;\r\n { P1[q] }\r\nend\r\n```\r\nAnd a verbose output of the procedure is provided.\r\n\r\n\r\n## Quantum Program - Constructing the proof\r\nThe verification of program correctness is through the definition of a proof term. Here in NQPV, we do not need to provide a proof of full details (like what is required in CoqQ or QHLProver). Instead, we write a *\"proof hint\"*, which briefly describes the correctness formula we want to proof, and provides the required loop invariants.\r\n\r\nIn the following we will explain the syntax of a proof hint.\r\nIf you found the formal description of the grammar hard to understand, you may refer to the examples for an intuitive idea.\r\n\r\nThe expression of a proof hint should be:\r\n\r\n> proof_hint ::= proof [ id_ls ] : <br>\r\n> { herm_ls } <br>\r\n> sequence <br>\r\n> { herm_ls }\r\n\r\n<!--\r\n> $$\r\n\\begin{aligned}\r\n \\mathrm{prog} ::=\\ & \\mathrm{qvar}\\ [\\ \\mathrm{id\\_ls}\\ ]\\\\\r\n & \\{\\ \\mathrm{herm\\_ls} \\}\\\\\r\n & \\mathrm{sequence} \\\\\r\n & \\{\\ \\mathrm{herm\\_ls} \\}\r\n\\end{aligned}\r\n> $$\r\n-->\r\n\r\nThe first line \"proof [id_ls]\" indicates all the quantum variables. The second and forth line indicates the pre and post conditions. The third line indicates the sequence of verification. \r\n\r\n\r\n\"id_ls\" is a list of one or more identifiers. \r\n> id_ls ::= <br>\r\n> id <br>\r\n> | id_ls id\r\n\r\n<!--\r\n> $$\r\n\\begin{aligned}\r\n \\mathrm{id\\_ls} ::=\\ & \\mathrm{id} \\\\\r\n &|\\ \\mathrm{id\\_ls}\\quad \\mathrm{id}\r\n\\end{aligned}\r\n> $$\r\n-->\r\n\r\n\"herm_ls\" is a list of one or more operators. \r\n> herm_ls ::= <br>\r\n> id [ id_ls ] <br>\r\n> | herm_ls id [ id_ls ]\r\n\r\n\r\n<!--\r\n> $$\r\n\\begin{aligned}\r\n \\mathrm{herm\\_ls} ::=\\ & \\mathrm{id}\\ [\\ \\mathrm{id\\_ls}\\ ]\\\\\r\n &|\\ \\mathrm{herm\\_ls}\\quad \\mathrm{id}\\ [\\ \\mathrm{id\\_ls}\\ ]\r\n\\end{aligned}\r\n> $$\r\n-->\r\n\r\n\"id [ id_ls ]\" describes a particular operator, with the identifier list specifying the Hilbert space of the operator. For example, \r\n$$\r\n\\mathrm{P0}\\ [\\ \\mathrm{q1}\\ ]\r\n$$\r\nmay refer to a Herimitian operator |0><0| on the space of variable q1, and \r\n$$\r\n\\mathrm{CX}\\ [\\ \\mathrm{q2}\\ \\mathrm{q1}\\ ]\r\n$$\r\nmay refer to the controlled-X gate with q2 being the control and q1 being the target.\r\n\r\n\"sequence\" is a list of verification tasks (programs or intermediate conditions), which are composed by sequential combination.\r\n\r\n> sequence ::= <br>\r\n> sentence <br>\r\n> | sequence ; sentence\r\n\r\n<!--\r\n> $$\r\n\\begin{aligned}\r\n \\mathrm{sequence} ::=\\ & \\mathrm{sentence}\\\\\r\n &|\\ \\mathrm{sequence};\\ \\mathrm{sentence}\r\n\\end{aligned}\r\n> $$\r\n-->\r\n\r\nAnd \"sentence\" is just a piece of verification task, which can be skip, abort, initialization, unitary transformation, if, while, nondeterministic choice. Besides, it can also be a quantum predicate (as the intermediate condition), or a former proof term.\r\n\r\n> sentence ::= <br>\r\n> skip <br>\r\n> | abort <br>\r\n> | [ id_ls ] := 0 <br>\r\n> | [ id_ls ] *= id <br>\r\n> | if id [ id_ls ] then sequence else sequence end <br>\r\n> | { inv : herm_ls } while id [ id_ls ] do sequence end <br>\r\n> | ( sequence \\# sequence \\# ... \\# sequence) <br>\r\n> | { herm_ls }\r\n\r\n<!--\r\n> $$\r\n\\begin{aligned}\r\n \\mathrm{sentence} ::=\\ & \\mathrm{skip}\\\\\r\n &|\\ \\mathrm{abort}\\\\\r\n &|\\ [\\ \\mathrm{id\\_ls}\\ ] := 0\\\\\r\n &|\\ [\\ \\mathrm{id\\_ls}\\ ] *= \\mathrm{id}\\\\\r\n &|\\ \\mathrm{if}\\ \\mathrm{id}\\ [\\ \\mathrm{id\\_ls}\\ ]\\ \\mathrm{then}\\ \\mathrm{sequence}\\ \\mathrm{else}\\ \\mathrm{sequence}\\ \\mathrm{end}\\\\\r\n &|\\ \\{\\ \\mathrm{inv}:\\ \\mathrm{herm\\_ls}\\ \\}\\\\\r\n &\\quad \\mathrm{while}\\ \\mathrm{id}\\ [\\ \\mathrm{id\\_ls}\\ ]\\ \\mathrm{do}\\ \\mathrm{sequence}\\ \\mathrm{end}\\\\\r\n &|\\ (\\ \\mathrm{sequence}\\ \\#\\ \\mathrm{sequence}\\ )\r\n\\end{aligned}\r\n> $$\r\n-->\r\n\r\nThe last three rules of the grammar above correspond to the (multiple) nondeterministic choice, the use of former proof and the intermediate predicate, respectively.\r\n\r\n## Program Verification Procedure\r\n\r\nHere the syntactic analysis checks whether the content can be properly interpreted with the grammar. The semantic analysis afterwards checks whether there is any problem in the meaning of the verification task. It will mainly examine the following aspects:\r\n- whether all operators mentioned can be found,\r\n- whether there are repeat identifiers in some identifier list, and\r\n- whether the qubit number of operators and identifier lists matches. For example, CX [ q1 ] or X [ q1 q2 ] will not be acceptable.\r\n\r\nIf there are syntactic or semantic errors, the verifier will stop there, providing the error information. \r\n\r\nThe verification utilizes a technique called *backward predicate transformation*. If there is not any while structures in the program, the whole calculation can be done automatically. That is, the weakest (liberal) precondition with respect to the given postcondition will be derived and compared with the desired precondition. Based on this, the verification tool will give a definite conclusion between the following two:\r\n- Property holds.\r\n- Property does not hold.\r\n\r\nHowever, if there are while structures, the automatical calculation relies on the specified *loop invariant* from the user. The verifier will first check whether it is a valid loop invariant. If not, the verification will stop and the failure will be reported. Otherwise, the corresponding precondition is derivied and the procedure continues. In this case, the verification result can be:\r\n- Property holds.\r\n- Property cannot be determined. A suitable loop invariant may be sufficient.\r\n\r\nThe tool can only give a definite conclusion if the property does hold.\r\n\r\n## Examples\r\nThis section gives some examples of verification tasks. The source can be found in the Github repository.\r\n\r\n### Error Correction Code\r\nThis example shows that the error correction code here is robust against single big-flip errors, for a random single qubit pure state.\r\n1. Create a folder called \"error_correction_code\"\r\n2. In this folder, create a file called \"example.nqpv\" with the following content:\r\n ```\r\n def Hrand := load \"Hrand.npy\" end\r\n\r\n def pf := proof[q] :\r\n { Hrand[q] };\r\n\r\n [q1 q2] :=0;\r\n [q q1] *= CX;\r\n [q q2] *= CX;\r\n (skip # q *= X # q1 *= X # q2 *= X);\r\n [q q1] *= CX;\r\n [q q2] *= CX;\r\n [q1 q2 q] *= CCX;\r\n\r\n { Hrand[q] }\r\n end\r\n\r\n show pf end\r\n ```\r\n3. In the same folder of \"error_correction_code\", create a python script \"example.py\" with the following content:\r\n\r\n ```Python\r\n import nqpv\r\n import numpy as np\r\n\r\n # create a Hermitian on a random ket\r\n theta = np.random.rand() * np.pi\r\n phi = np.random.rand() * np.pi * 2\r\n\r\n ket = np.array([np.cos(theta), np.sin(theta)*np.exp(phi*1j)])\r\n\r\n Hrand = np.outer(ket, np.conj(ket))\r\n\r\n np.save(\"Hrand\", Hrand)\r\n\r\n # verify\r\n nqpv.verify(\"./prog.nqpv\") \r\n ```\r\n\r\n4. Run the python script in the folder. (Note that the run path also needs to be the folder.)\r\n\r\n### Deutsch Algorithm\r\n1. Create a folder called \"Deutsch_algorithm\"\r\n2. In this folder, create a file called \"prog.nqpv\" with the following content:\r\n ```\r\n\r\n def Hpost := load \"Hpost.npy\" end\r\n\r\n def pf := proof[q q1] :\r\n { I[q] };\r\n [q1 q2] :=0;\r\n q1 *= H;\r\n q2 *= X;\r\n q2 *= H;\r\n if M01[q] then\r\n ( \r\n [q1 q2] *= CX\r\n #\r\n q1 *= X;\r\n [q1 q2] *= CX;\r\n q1 *= X\r\n )\r\n else\r\n (\r\n skip\r\n #\r\n q2 *= X\r\n )\r\n end;\r\n q1 *= H;\r\n if M01[q1] then\r\n skip\r\n else\r\n skip\r\n end;\r\n { Hpost[q q1] }\r\n end\r\n\r\n show pf end\r\n ```\r\n3. In the same folder of \"Deutsch_algorithm\", create a python script \"example.py\" with the following content:\r\n\r\n ```Python\r\n import nqpv\r\n import numpy as np\r\n\r\n # create the required operators\r\n Hpost = np.array([[1., 0., 0., 0.],\r\n [0., 0., 0., 0.],\r\n [0., 0., 0., 0.],\r\n [0., 0., 0., 1.]])\r\n np.save(\"./Hpost\", Hpost.reshape((2,2,2,2)))\r\n\r\n # verify\r\n nqpv.verify(\"./prog.nqpv\")\r\n ```\r\n\r\n4. Run the python script in the folder. (Note that the run path also needs to be the folder.)\r\n\r\n### Quantum Walk\r\n\r\n1. Create a folder called \"quantum_walk\"\r\n2. In this folder, create a file called \"prog.nqpv\" with the following content:\r\n ```\r\n def invN := load \"invN.npy\" end\r\n def MQWalk := load \"MQWalk.npy\" end\r\n def W1 := load \"W1.npy\" end\r\n def W2 := load \"W2.npy\" end\r\n\r\n def pf := proof[q1 q2] :\r\n { I[q1] };\r\n\r\n [q1 q2] :=0;\r\n\r\n {inv: invN[q1 q2]};\r\n while MQWalk[q1 q2] do\r\n (\r\n [q1 q2] *= W1; [q1 q2] *= W2\r\n #\r\n [q1 q2] *= W2; [q1 q2] *= W1\r\n )\r\n end;\r\n\r\n { Zero[q1] }\r\n\r\n end\r\n\r\n show pf end\r\n ```\r\n3. In the same folder of \"quantum_walk\", create a python script \"example.py\" with the following content:\r\n\r\n ```Python\r\n import nqpv\r\n import numpy as np\r\n\r\n # create the required operators\r\n W1 = np.array([[1., 1., 0., -1.],\r\n [1., -1., 1., 0.],\r\n [0., 1., 1., 1.],\r\n [1., 0., -1., 1.]]) / np.sqrt(3)\r\n W2 = np.array([[1., 1., 0., 1.],\r\n [-1., 1., -1., 0.],\r\n [0., 1., 1., -1.],\r\n [1., 0., -1., -1.]]) / np.sqrt(3)\r\n np.save(\"W1\", W1.reshape((2,2,2,2)))\r\n np.save(\"W2\", W2.reshape((2,2,2,2)))\r\n\r\n P0 = np.array([[0., 0., 0., 0.],\r\n [0., 0., 0., 0.],\r\n [0., 0., 1., 0.],\r\n [0., 0., 0., 0.]])\r\n P1 = np.array([[1., 0., 0., 0.],\r\n [0., 1., 0., 0.],\r\n [0., 0., 0., 0.],\r\n [0., 0., 0., 1.]])\r\n \r\n MQWalk = np.stack((P1,P0), axis = 0)\r\n np.save(\"MQWalk\", MQWalk.reshape((2,2,2,2,2)))\r\n\r\n # the invariant N\r\n invN = np.array([[1., 0., 0., 0.],\r\n [0., 0.5, 0., 0.5],\r\n [0., 0., 0., 0.],\r\n [0., 0.5, 0., 0.5]])\r\n np.save(\"invN\", invN.reshape((2,2,2,2)))\r\n\r\n # verify\r\n nqpv.verify(\"prog.nqpv\")\r\n ```\r\n\r\n4. Run the python script in the folder. (Note that the run path also needs to be the folder.)\r\n\r\n\r\n## Contact\r\nIf you find any bug or have any questions, do not hesitate to contact lucianoxu@foxmail.com.\r\n\r\n\r\n## Development Log\r\n### 0.4b1\r\n- We refactored this software and deleted some redundant functions, including subprogram, subproof and module import.\r\n\r\n### 0.3b9\r\n- Now the verification tool will try to find an existing variable for the particular value before creating a new one with an auto name.\r\n",
"bugtrack_url": null,
"license": "",
"summary": "An assistant tool for the formal verification of nondeterministic quantum programs.",
"version": "0.4b1",
"split_keywords": [
"quantum programs",
"program verification",
"automatic theorem proving"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "5255de67cde0476f553327ff117d20710b6d0e76dccc5bd8ba434604b1ad109c",
"md5": "ac4842efe1f1fc4cf4e2ee0bf69679ad",
"sha256": "9a82e6d6e753fea6183256ec6f34b7af4e759a1e71d9e0ddff5dbf2f504d79fe"
},
"downloads": -1,
"filename": "NQPV-0.4b1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "ac4842efe1f1fc4cf4e2ee0bf69679ad",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": null,
"size": 57607,
"upload_time": "2023-01-24T08:14:52",
"upload_time_iso_8601": "2023-01-24T08:14:52.233064Z",
"url": "https://files.pythonhosted.org/packages/52/55/de67cde0476f553327ff117d20710b6d0e76dccc5bd8ba434604b1ad109c/NQPV-0.4b1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "013a2843a99750a3a95881f8ddf2cb416c4621bbc8ea295818d10ef9cacedae8",
"md5": "76ef19a910810595fa22fdd9e5ef1e20",
"sha256": "55e2b4b3e524f6739716c2ec891540e6e3d0a5380d2a78027f910536358aa7ae"
},
"downloads": -1,
"filename": "NQPV-0.4b1.tar.gz",
"has_sig": false,
"md5_digest": "76ef19a910810595fa22fdd9e5ef1e20",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 48374,
"upload_time": "2023-01-24T08:14:56",
"upload_time_iso_8601": "2023-01-24T08:14:56.003597Z",
"url": "https://files.pythonhosted.org/packages/01/3a/2843a99750a3a95881f8ddf2cb416c4621bbc8ea295818d10ef9cacedae8/NQPV-0.4b1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-01-24 08:14:56",
"github": true,
"gitlab": false,
"bitbucket": false,
"github_user": "LucianoXu",
"github_project": "NQPV",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "nqpv"
}
JSON
