Generation of reversible circuits from high-level code is an important problem in the compilation flow of quantum algorithms to lower-level hardware. The instantiation of quantum oracles in particular will require mapping classical circuits to a reversible implementation. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent so far on verifying the correctness of the results.
In the paper “Verified compilation of space-efficient reversible circuits,” Matt Amy, Martin Roetteler, and Krysta M. Svore present a reversible circuit compiler ReVerC (pronounced “Reverse”). It has been formally verified and compiles circuits that operate correctly with respect to the input program. The compiler compiles a subset of the higher-level .NET language F# into combinational reversible circuits with as few ancillary bits as possible, and provably cleans temporary values which is a crucial property for maintaining coherence in large-scale quantum algorithms. The proofs of correctness were written in the F* proof system.
The ReVerC software is available from GitHub. Read the arXiv preprint.