<!-- 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 a verification assistant tool for the formal verification of nondeterministic quantum programs. Different form 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 guarantee 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 verification tools that are based on proof assistants and can only deal with numerical operators. However, the proof hints from the user are 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 and 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 recommend running the python script in 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.

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 follow 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 variable 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 executed 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 on 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 exist 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 distichous indices. What's more, the first $n$ indices correspond to the ket space, and the second $n$ indices correspond 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 automatically generated and preserved 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 m