Abstract
This paper introduces a novel duality theorem for hybrid classical-quantum states, bridging a critical gap in the formal verification of hybrid quantum systems. By applying this theorem, the authors develop cqOTL (classical-quantum Optimal Transport Logic), the first relational program logic for hybrid programs that is unconditionally complete. Unlike previous methods that required restrictive "boundedness" assumptions, cqOTL can theoretically prove any true relational property, such as program equivalence or non-interference, even in the presence of infinite classical state spaces.
Introduction
As hybrid quantum computing—where classical controllers manage quantum processors—becomes more prevalent, the need for rigorous verification methods grows. Relational verification is particularly vital, as it allows developers to prove properties comparing two programs or different executions of the same program. This is essential for verifying optimizations, cryptographic protocols, and security properties like non-interference.
However, existing relational logics such as qRHL and EasyPQC suffer from completeness issues. Their assertion languages are often too restrictive to capture the full range of relationships between classical and quantum variables, especially when classical state spaces are infinite. While duality theorems from convex optimization have enabled complete logics for purely probabilistic or purely quantum systems, the hybrid setting remained a challenge due to the mathematical difficulty of maintaining quantum consistency across infinite classical states.
Theoretical Foundations: The Duality Theorem
The core contribution of this work is a new Duality Theorem for classical-quantum states. In the context of optimization, duality allows a problem to be analyzed from two complementary perspectives: the Primal and the Dual. The authors demonstrate that finding a "coupling" (a mathematical witness that two programs are related) is equivalent to satisfying a set of "split" assertions.
To handle countably infinite classical state spaces, the authors developed a dimension-independent analysis of the underlying convex optimization problem. This allows the logic to reason about "unbounded" assertions where values can approach infinity, a significant advancement over previous "bounded-only" frameworks.
The cqOTL Logic and Unconditional Completeness
Building on this duality, the authors introduce cqOTL for the cqWhile language. The logic treats relational assertions as optimal transport problems, proving that if a relationship exists, it can be decomposed into "split" assertions manageable by standard tools like Weakest Preconditions.
The primary result is the achievement of unconditional completeness. As shown in the comparison below, cqOTL fills the gap left by previous logics that were either incomplete or restricted to bounded assertions.
The authors provide rigorous proofs (Theorems 8.1 and 8.2) establishing that cqOTL is both sound and complete. Furthermore, they show that these insights can be "retrofitted" to improve existing logics like eRHL and qOTL, making them complete for unbounded assertions as well.
Implementation and Benchmarks
The logic was formalized in the Lean 4 proof assistant, involving approximately 2,500 lines of code to define positive and density operators. The framework was evaluated against several illustrative benchmarks:
- Quantum Random Walks: Comparing classical probabilistic walks with quantum-initialized versions.
- Deferred Measurement: Proving the equivalence of early measurement versus late measurement using controlled gates.
- Rejection Sampling: Verifying programs with complex loop structures.
Conclusion and Future Work
This work provides a theoretical foundation for the complete relational verification of hybrid quantum programs. While the logic is theoretically complete, practical application in Lean currently requires significant manual effort. Future work will focus on increasing automation (e.g., for Dirac notation), extending support to the Quantum Random Oracle Model (QROM) for cryptographic verification, and incorporating quantitative reasoning for execution complexity.