Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

TL;DR

This paper introduces a new quantum Hoare logic with distribution formulas for local reasoning about probabilistic behavior in classical-quantum programs, verified through Coq embedding and applied to complex algorithms.

Contribution

It presents a novel quantum Hoare logic that handles probabilistic behavior and unbounded loops, with formal verification and Coq integration.

Findings

Proves soundness of the proof rules with respect to denotational semantics.

Successfully verifies quantum algorithms like HHL and Shor's.

Provides a semi-automated reasoning framework in Coq for classical-quantum programs.

Abstract

Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.