A Verified Compiler for Quantum Simulation (Artifact)

Quantum simulations are designed to model quantum systems, and many compilation frameworks have been developed for executing such simulations on quantum computers. These systems are typically Pauli operation-based and lack clear programmability to show the utility of Hamiltonian simulation. In addition, the compilers were fragmented, focusing on a piece of the compilation pipeline, and were not verified. This paper proposed QBlue, the first verified compilation framework for second-quantization-based Hamiltonian simulation. We intend to lift the Pauli-based Hamiltonians to constraints based on second quantization and examine the programmability of programming Hamiltonian constraints. We then propose a type system to generalize a qubit-based quantum system to quantum particle systems and provide a certified compilation of Hamiltonian simulation for quantum circuits, both digital and analog. All the works are mechanized in Rocq.