Skip to content

qafny/qafny_impl

BranchesTags

Repository files navigation

Qafny

Qafny is a programming language for quantum programs. Its intended use is as a high-level representation to verify and compile quantum circuits, but we have also used it to implement verified versions of several quantum algorithms.

We first presented Qafny and its Dafny verification techniques in our paper Qafny: A Quantum Program Verifier at ECOOP 2024. We provided additional details in our paper Embedding Quantum Program Verification into Dafny presented at OOPSLA 2025.

This repository contains our Python implementation of Qafny as well as several verified quantum algorithms.

If you are interested in learning more about formal verification of quantum programs in general, we recommend Robert Rand's Verfied Quantum Computing tutorial.

Table of Contents

QAFNY

  1. Table of Contents
  2. Installation
  3. Usage
  4. Directory Contents
  5. Acknowledgements
  6. Citations

Installation

To run Qafny, you will need Python v3.11.5 and the python packages antlr4-python3-runtime version 4.9.2 and rich version 13.9.4. The python packages are also listed in requirements.txt.

Assuming you have Python and Pip installed, the following script will clone this repository, setup a virtual environment and download the required dependencies.

# repository clone
git clone https://github.com/qafny/qafny_impl.git qafny
cd qafny

# environment setup
python -m venv .venv
python -m pip install -r ./src/requirements.txt

Usage

Once the repository has been downloaded and the python depedencies are setup, running python . in the src/ directory will run qafny. When this script is provided a filename, such as in python . supercoding.qfy it will attempt to convert and verify supercoding.qfy as a Qafny file. When the script is run without a filename, it will attempt to verify the test files in test/Qafny.

OPTIONS:

The main script also accepts a few options, including:

  • -d, --print-dafny: Outputs the generated Dafny code before verifying.
  • -o [out_filename], --output [out_filename]: Writes the Dafny code to a file before verifying.
  • -x, --skip-verify: Skips verification. Useful for inspecting the Dafny code without verifying it or manually running dafny.

Directory Contents

src/

Contains all the code associated with Qafny. The transformation from Qafny to Dafny involves parsing the file with ExpParser.py, transforming the ANTLR AST into a cleaner AST with ProgramTransformer.py, converting the Qafny AST to Dafny with ProgramTransfer.py and ultimately piping the Dafny AST into Dafny for verification.

Important files include:

__main__.py: The main Qafny file. Outlines the process for transforming Qafny to Dafny.

Exp.g4, ExpParser.py, ExpVisitor.py, etc.: Exp.g4 defines the Qafny grammar in ANTLR v4 syntax. All classes/files with the Exp prefix are generated from this grammar file.

Programmer.py: Defines an intermediate Qafny grammar.

ProgramTransformer.py: Converts an AST generated by ANTLR into the AST defined in Programmer.py.

ProgramTransfer.py: Converts a Qafny AST into a Dafny one.

src/error_reporter

Contains classes relating to printing formatted and stylized source code on the terminal.

src/tests

Contains internal testing code for various classes.

test/Qafny

Formal verifications of quantum algorithms written in Qafny code. All qafny code has the suffix .qfy.

Acknowledgements

This project is the result of the efforts of many people. The primary contacts for this project are Dr. Liyi Li (@liyili2) and Feifei Cheng (@jump-orange). The full list of contributors include:

  • Liyi Li
  • Feifei Cheng
  • Sushen Vangeepuram
  • Seyed Mohammad Reza Jafari
  • Alex Potanin
  • Henry Allard
  • Mingwei Zhu
  • Rance Cleaveland
  • Alexander Nicolellis
  • Yi Lee
  • Le Chang
  • Xiaodi Wu

Citations

If you use Qafny in your work, please cite our papers:

Qafny: A Programming Language for Quantum Verification

@InProceedings{li_et_al:LIPIcs.ECOOP.2024.24,
    author    = {Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
    title     = {{Qafny: A Quantum-Program Verifier}},
    booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)},
    pages     = {24:1--24:31},
    series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
    ISBN      = {978-3-95977-341-6},
    ISSN      = {1868-8969},
    year      = {2024},
    volume    = {313},
    editor    = {Aldrich, Jonathan and Salvaneschi, Guido},
    publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
    address   = {Dagstuhl, Germany},
    URL       = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.24},
    URN       = {urn:nbn:de:0030-drops-208735},
    doi       = {10.4230/LIPIcs.ECOOP.2024.24},
    annote    = {Keywords: Quantum Computing, Automated Verification, Separation Logic}
    note      = {ECOOP '24}
}

Embedding Quantum Program Verification into Dafny

@InProceedings {cheng_et_al:
    doi       = {10.1145/3763157},
}

Alternatively, you can cite our repository using the information in CITATION.cff.

About

Qafny to Dafny Compiler

Resources

Readme

License

BSD-2-Clause license
Activity
Custom properties

Stars

5 stars

Watchers

3 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 6

Languages