Welcome to Qbricks

Qbricks is open-source environment for automated formal verification of quantum programs. It enables the writing of quantum circuit building programs, specified with their I/O functions and/or their resource requirements. Thanks to a characterization of quantum circuits as paramatrized path-sums, the specifications of Qbricks circuit-building quantum programs reduces to first-order proof obligations. Its host language, the Why3 deductive verification environment, provides an interface with SMT-solvers, enabling an high-level of automation in the vertfication of Qbricks specifications.

So far, Qbricks framework enabled the verified implementation of several emblematic algorithm from the litterature, including the Deutsch-Jozsa algorithm, Quantum Phase Estimation (QPE), Grover search algorithm and Shor order finding (including an implementation of the oracle).

It is developed at the CEA LIST (part of Université Paris-Saclay) in collaboration with Laboratoire Méthodes Formelles(Université Paris-Saclay).

For an introduction to Qbricks, please read our article and see the related presentation slides. A tutorial redaction is under progress.

PostDoc open position (2 years) : verified compilation

The goal of this post-doctoral position is to extend formal verification practice to quantum compilation. Possibilities include, among others, error correction mechanisms in certified quantum code, together with specifications and reasoning technique for certifying its reliability, automatized certified optimizer for quantum circuits, hardware agnostic assembly language together with its compiler,

Keywords: quantum programming, compilation, optimization, formal verification

How to apply

Applications should be sent to christophe.chareton@cea.fr as soon as possible (first come, first served) and by early July 2021 at the latest. Candidates should send a CV, a cover letter, a transcript of all their university results, as well as contact information of two references. Each position is expected to start in October 2021.

Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA) Contact: christophe.chareton@cea.fr

News

• Ongoing Postdoc June 2023 Welcome, Nicolas Blanco, working on parametrized path-sums reewriting.
• New relase March 2023 Qbricks_1 is online! Available on main branch in diffusion, under License LGPL, 2.1. As main novelties the release provides:
  • LANGUAGE : new primitive constructs, containing (1) generic wiring and subcircuit control features (2) further gate constructors as primitives (Toffoli, Fredkin, X,Y,Z rotations, etc).
  • COMPILATION : a fully formally verified circuit transformation process, targetting Oqasm compatibile circuit, and an oqasm output generating function. Works for circuit without ancilla qbits.
  • CASE STUDIES : new implementations of Shor algorithm, illutrating imperative QBricks styled programmation and the Oqasm extraction functionality.
• Our code is back to open source diffusion, under License LGPL, 2.1, April 2022 .
• Ongoing internship April 2022 Welcome, Mohamed Bassiouny, working on automated circuit equivalence verification.
• Book chapter submission March 2022 Our survey on formal methods in quantum computing was submitted, as a Book Chapter to appear in the " "Handbook of Formal Analysis and Verification in Cryptography" (CRC), see the preprint.
• Ongoing PhD March 2022 Welcome, Jérôme Ricciardi, working on mixed path-sums.
• Ongoing internship February 2022 Welcome, Tomas Barros Carneiro, working on an imperative developement interface for quantum formal verification.
• Presentation at IQFA Nov 2021 Qbricks was presented at the 12th Colloquium on Quantum Engineering, Fundamental Aspects to Applications, 2021 (slides).
• Online survey Formal Methods for Quantum Programs: A Survey September 2021.
• Presentation at QPL June 2021 Qbricks was presented at the 2021 online QPL conference (slides).
• Qbricks at ESOP March 2021 Glad to participate to the 2021 online ESOP conference (slides).
• Paper accepted December 2020 Proud that our paper “An Automated Deductive Verification Framework for Circuit-building Quantum Programs” has been accepted at ESOP’21.
• Online preprint March, 2020 Our preprint Toward certified quantum programming is availeble on Arxiv
• Talk at IWQC November, 2020, with online presentation

People

Name	Position	Affiliation	Web site
Sébastien Bardin	Senior	CEA LIST, Université Paris-Saclay	Sébastien Bardin
Benoît Valiron	Senior	LMF, Université Paris-Saclay	Benoît Valiron
Christophe Chareton	Junior	CEA LIST, Université Paris-Saclay	Christophe Chareton
Jérôme Ricciardi	PhD student	CEA LIST, Université Paris-Saclay	Jérôme Ricciardi
Tomas Barros Carneiro	Intern	CEA LIST, Université Paris-Saclay	Tomas Barros Carneiro
Mohamed Bassiouny	Intern	CEA LIST, Université Paris-Saclay	Mohamed Bassiouny

Publications

International conference

• An Automated Deductive Verification Framework for Circuit-building Quantum Programs, March, 2021 at ESOP’21.

Survey

• Formal Methods for Quantum Programs: A Survey, 09/2021. Due to the destructive aspect of quantum measurement, formal methods are prone to play a decisive role in the emerging field of quantum software. In this survey, we present the challenges adressed to formal verificatio at every stage of the quantum development process: high-level program design, implementation, compilation, etc. and we introduce the current most promising research directions

Preprint

• Toward certified quantum programming, March, 2020

Short articles

• A formally certified implementation of Shor algorithm quantum circuit, IWQC, November 2020 video
• Qbricks, a framework for formal verification in quantum computing PlanQC, January 2020 video
• Toward_certified_quantum_programming_ IWQC, November,2018 (2nd International Workshop on Quantum Compilation).(link)

Installation

Installation with Docker

Please note that all the following tools are external tools, please refer to their webpage for more information.

Licence

• Docker: licence

• CVC3: licence

• CVC4: licence

• CVC5: licence

• Z3: licence

• Alt-Ergo: licence

• Why3: licence

• OCaml: licence

• Qiskit: licence

• OpenQASM: licence

• Matplotlib: licence

Installation

1. Docker installation

2. Post-installation steps for Linux

3. Build Docker image make build (alternative make pull)

4. Build container make container

5. Start container make start

Quick Start - Examples

Files can be edited outside of the Docker container using your preferred text editor.

Proof

Open shor.mlw with why3-ide:

1. cd Case_studies/

2. make ide_shor

Qbricks to OpenQASM

Example: Toffoli

1. To define a quantum circuit, modify the file Qbricks_to_oqasm/Examples/To_openqasm_examples.mlw by adding your circuit description in the Qbricks language. For example, you can replace the existing run function by the following line to define a Toffoli gate on qubits 0, 1, 2, and 3:

let run() : string = string_oq (toffoli 0 1 2 3)

2. Translate to OpenQASM

Use make run_to_openqasm to perform a full translation process. This includes both the extraction from WhyML to OCaml and the OCaml compilation. This command is suitable when you need to translate and compile your quantum circuit descriptions in one go.

Once the full translation process has been executed with make run_to_openqasm and all OCaml code has been extracted, you can use make run_to_openqasm_ne. This command extracts only the example file and compiles it. It is useful for subsequent compilations when you only need to update and compile the example file without repeating the full extraction process.

3. Retrieve the OpenQASM file

After translation, you can find the OpenQASM file at extracted/To_openqasm_examples.qasm. The file will contain the quantum circuit description in OpenQASM format, similar to the example below:

OPENQASM 2.0;
include "qelib1.inc";
qreg q[3];
h q[2];
u1 (2 * pi / 2^(3)) q[0];
rz (2 * pi / 2^(3)) q[2];
cx q[0], q[2];
rz (-2 * pi / 2^(3)) q[2];
cx q[0], q[2];
u1 (2 * pi / 2^(3)) q[1];
rz (2 * pi / 2^(3)) q[2];
cx q[1], q[2];
rz (-2 * pi / 2^(3)) q[2];
cx q[1], q[2];
cx q[0], q[1];
u1 (-2 * pi / 2^(3)) q[1];
rz (-2 * pi / 2^(3)) q[2];
cx q[1], q[2];
rz (2 * pi / 2^(3)) q[2];
cx q[1], q[2];
cx q[0], q[1];
h q[2];

Qiskit simulation

Simulation

To simulate the toffoli 0 1 2 3 circuit extracted using the Qiskit Aer Simulator, use the following command:

python3 scripts/run_to_qiskit.py extracted/To_openqasm_examples.qasm

This will output:

Testing all possible input states for the given quantum circuit:
Verification completed in 0.01 seconds.

For a more detailed simulation that displays the circuits and results, use the verbose mode by adding true as an additional argument:

python3 scripts/run_to_qiskit.py extracted/To_openqasm_examples.qasm true

Testing all possible input states for the given quantum circuit:
Circuit for input state 000:
     ┌─────────┐                                                                                                                    ┌─┐   »
q_0: ┤ U1(π/4) ├─────────────■────────────────■────────────────────────────────────────■─────────────────────────────────────────■──┤M├───»
     ├─────────┤             │                │                                      ┌─┴─┐    ┌──────────┐                     ┌─┴─┐└╥┘┌─┐»
q_1: ┤ U1(π/4) ├─────────────┼────────────────┼───────────────■────────────────■─────┤ X ├────┤ U1(-π/4) ├──■───────────────■──┤ X ├─╫─┤M├»
     └──┬───┬──┘┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌──┴───┴───┐└──────────┘┌─┴─┐┌─────────┐┌─┴─┐├───┤ ║ └╥┘»
q_2: ───┤ H ├───┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(-π/4) ├────────────┤ X ├┤ Rz(π/4) ├┤ X ├┤ H ├─╫──╫─»
        └───┘   └─────────┘└───┘└──────────┘└───┘└─────────┘└───┘└──────────┘└───┘└──────────┘            └───┘└─────────┘└───┘└───┘ ║  ║ »
c: 3/════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩══╩═»

Input: 000 (q2, q1, q0)
Output: 000 (q2, q1, q0)
...
     ┌───┐┌─────────┐                                                                                                                    ┌─┐»
q_0: ┤ X ├┤ U1(π/4) ├─────────────■────────────────■────────────────────────────────────────■─────────────────────────────────────────■──┤M├»
     ├───┤├─────────┤             │                │                                      ┌─┴─┐    ┌──────────┐                     ┌─┴─┐└╥┘»
q_1: ┤ X ├┤ U1(π/4) ├─────────────┼────────────────┼───────────────■────────────────■─────┤ X ├────┤ U1(-π/4) ├──■───────────────■──┤ X ├─╫─»
     ├───┤└──┬───┬──┘┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌──┴───┴───┐└──────────┘┌─┴─┐┌─────────┐┌─┴─┐├───┤ ║ »
q_2: ┤ X ├───┤ H ├───┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(-π/4) ├────────────┤ X ├┤ Rz(π/4) ├┤ X ├┤ H ├─╫─»
     └───┘   └───┘   └─────────┘└───┘└──────────┘└───┘└─────────┘└───┘└──────────┘└───┘└──────────┘            └───┘└─────────┘└───┘└───┘ ║ »
c: 3/═════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═»
                                                                                                                                          0 »
«           
«q_0: ──────
«     ┌─┐   
«q_1: ┤M├───
«     └╥┘┌─┐
«q_2: ─╫─┤M├
«      ║ └╥┘
«c: 3/═╩══╩═
«      1  2 
Input: 111 (q2, q1, q0)
Output: 011 (q2, q1, q0)
----------------------------------------
Verification completed in 0.06 seconds.          

Equivalence Check

To check the equivalence of the toffoli 0 1 2 3 circuit extracted with Qbricks to OpenQASM with the Qiskit Aer Simulator, use the following command:

python3 scripts/run_to_qiskit_equiv.py extracted/To_openqasm_examples.qasm Qbricks_to_oqasm/Examples/toffoli.qasm 

This will output:

All input states result in identity. The two circuits are equivalent.
Verification time: 0.01 seconds

For a detailed equivalence check that displays the circuits and results, use the verbose mode by adding true as an additional argument:

python3 scripts/run_to_qiskit_equiv.py extracted/To_openqasm_examples.qasm Qbricks_to_oqasm/Examples/toffoli.qasm true 

This will output detailed information including:

Testing equivalence by checking if the combined circuit results in identity for all input states:
Circuit for input state 000:
     ┌─────────┐                                                                                                                         ┌─┐»
q_0: ┤ U1(π/4) ├─────────────■────────────────■────────────────────────────────────────■─────────────────────────────────────────■────■──┤M├»
     ├─────────┤             │                │                                      ┌─┴─┐    ┌──────────┐                     ┌─┴─┐  │  └╥┘»
q_1: ┤ U1(π/4) ├─────────────┼────────────────┼───────────────■────────────────■─────┤ X ├────┤ U1(-π/4) ├──■───────────────■──┤ X ├──■───╫─»
     └──┬───┬──┘┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌──┴───┴───┐└──────────┘┌─┴─┐┌─────────┐┌─┴─┐├───┤┌─┴─┐ ║ »
q_2: ───┤ H ├───┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(-π/4) ├────────────┤ X ├┤ Rz(π/4) ├┤ X ├┤ H ├┤ X ├─╫─»
        └───┘   └─────────┘└───┘└──────────┘└───┘└─────────┘└───┘└──────────┘└───┘└──────────┘            └───┘└─────────┘└───┘└───┘└───┘ ║ »
c: 3/═════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═»
                                                                                                                                          0 »
«           
«q_0: ──────
«     ┌─┐   
«q_1: ┤M├───
«     └╥┘┌─┐
«q_2: ─╫─┤M├
«      ║ └╥┘
«c: 3/═╩══╩═
«      1  2 
Input: 000, Output: 000 - PASS
----------------------------------------
Circuit for input state 001:
        ┌───┐   ┌─────────┐                                                                                                              ┌─┐»
q_0: ───┤ X ├───┤ U1(π/4) ├──■────────────────■────────────────────────────────────────■─────────────────────────────────────────■────■──┤M├»
     ┌──┴───┴──┐└─────────┘  │   

...

«c: 3/═══════════╩══╩══╩═
«                0  1  2 
Input: 110, Output: 110 - PASS
----------------------------------------
Circuit for input state 111:
     ┌───┐┌─────────┐                                                                                                                    »
q_0: ┤ X ├┤ U1(π/4) ├─────────────■────────────────■────────────────────────────────────────■─────────────────────────────────────────■──»
     ├───┤├─────────┤             │                │                                      ┌─┴─┐    ┌──────────┐                     ┌─┴─┐»
q_1: ┤ X ├┤ U1(π/4) ├─────────────┼────────────────┼───────────────■────────────────■─────┤ X ├────┤ U1(-π/4) ├──■───────────────■──┤ X ├»
     ├───┤└──┬───┬──┘┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌─────────┐┌─┴─┐┌──────────┐┌─┴─┐┌──┴───┴───┐└──────────┘┌─┴─┐┌─────────┐┌─┴─┐├───┤»
q_2: ┤ X ├───┤ H ├───┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(π/4) ├┤ X ├┤ Rz(-π/4) ├┤ X ├┤ Rz(-π/4) ├────────────┤ X ├┤ Rz(π/4) ├┤ X ├┤ H ├»
     └───┘   └───┘   └─────────┘└───┘└──────────┘└───┘└─────────┘└───┘└──────────┘└───┘└──────────┘            └───┘└─────────┘└───┘└───┘»
c: 3/════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════»
                                                                                                                                         »
«          ┌─┐      
«q_0: ──■──┤M├──────
«       │  └╥┘┌─┐   
«q_1: ──■───╫─┤M├───
«     ┌─┴─┐ ║ └╥┘┌─┐
«q_2: ┤ X ├─╫──╫─┤M├
«     └───┘ ║  ║ └╥┘
«c: 3/══════╩══╩══╩═
«           0  1  2 
Input: 111, Output: 111 - PASS
----------------------------------------
All input states result in identity. The two circuits are equivalent.
Verification time: 0.05 seconds