Matthew Amy
Contributors:
- Alex Parent
- Martin Roetteler
ReVerC (pronounced “reverse”) is a reversible circuit compiler which compiles a high-level, ml-like language to combinational reversible circuits. It is fully verified in the sense that the program and compiled circuit, when generated by ReVerC, will produce the same output for every input. Furthermore, it is formally verified that any ancilla bits used by the compiler are correctly cleaned and returned to the pool of 0-initialized ancillas.
The core of ReVerC is exported as a library, reverlib. The ReVerC library can be imported into F# projects, and provides functions to (among other things)
- Compile F# code quotations into reversible circuits
- Ouput compiled circuits to Q# or .qc files
- Count bits and gates used
- Infer the size of registers
- Verify assertions in F# quotations
The examples folder contains examples of the usage reverlib and the relevant API calls to compile and generate Q# files.
An executable version (reverc) is also included, which provides various commands and a suite of example programs for compilation.
Before building, ensure the F* binary is built in .fstar. This can be done by executing
git submodule update --init
make -C .fstar/src
The build system for ReVerC is separated into three stages: verification, code generation, and compilation. The command
make verify
on linux uses the F* compiler to check all verification conditions in the F* source code. Note that the Makefile should be updated manually to specify the path to the F* home directory.
make fs
extracts F# code from the F* source, which may then be compiled with
make
Note: F# extraction is currently in experimental status and isn't fully supported, so the repository includes manually extracted F# code. Effectively, this means the user should compile ReVerC with the command
make
A visual studio solution is included in the folder VS. To compile the library, executable and examples, simply build the visual studio solution.
ReVerC may also be verified by running
make verify
at the command line. Again, the Makefile should be changed to reflect the path to the F* home directory.
Run ReVerC with
reverc.exe
or on Unix-based systems
mono reverc.exe
The user interfaces with ReVerC through a read-evaluate-print loop, which receives a command and program (possibly with an integer parameter), then runs that commands on the specific program and parameter. To see a full list of commands and Revs programs registered together with their descriptions, the user can type "help" or "-h" at the REPL.
New commands and programs can be registered in the ReVerC compiler by adding a registerProg or registerCmd statement in the source code. Programs and commands registered via register commands are immediately available to the compiler after recompiling the binary.
Typing "exit" quits the REPL.
The ReVerC library does not currently have a documented API, but examples of its usage are include in the examples folder. As ReVerC compiles F# code quotations, the typical workflow is to
- Import ReVerC
- Write the program to be compiled as an F# quotation
- Use ReVerC functions to compile the quotation to a circuit
- Output the circuit in Q# or .qc format
Executing the F# code, either by compiling then running or interpreting via an F# compiler, will then produce the desired Q# or .qc code, which can be used in other projects. Alternatively, ReVerC provides the ability to compile and output resource counts if only the resource counts are needed.
If you use ReVerC to generate circuits for use in publications, please cite as
Matthew Amy, Martin Roetteler and Krysta Svore, Verified compilation of space-efficient reversible circuits. Proc. Computer Aided Verification, 2017.