BI-based Reasoning about Quantum Programs with Heap Manipulations

TL;DR

This paper introduces a quantum separation logic framework for reasoning about heap-manipulating quantum programs with nondeterministic initial states, enabling formal verification of complex quantum algorithms.

Contribution

It develops a quantum BI-style logic and a sound, relatively complete separation logic for heap-manipulated quantum programs, addressing the challenge of dirty qubits.

Findings

Verified correctness of practical quantum programs

Proved correct usage of dirty ancilla qubits

Established a formal framework for heap manipulations in quantum computing

Abstract

We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations, where allocation statements follow a dirty pattern, meaning that newly allocated qubits can nondeterministically assume arbitrary initial states. To thoroughly characterize heap manipulations in the quantum setting, we develop a quantum BI-style logic that includes interpretations for separating implication ($-\mkern-3mu*$) and separating conjunction ($*$). We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs and present a quantum separation logic which is sound and relatively complete. Finally, we apply our framework to verify the correctness of various practical quantum programs and to prove the correct usage of dirty ancilla qubits.