On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop
Xin Sun, Xingchi Su, Xiaoning Bian, Anran Cui
TL;DR
The paper tackles the longstanding problem of relative completeness for satisfaction-based Probabilistic Hoare Logic (PHL) in the presence of While loops. It introduces a new satisfaction-based PHL that uses probabilistic assignment $X\xleftarrow{\$}\{a_1:k_1,\dots,a_n:k_n\}$, showing language expressiveness equivalent to existing systems while enabling a tractable weakest preterm calculus. The authors establish completeness in two steps: first a calculus for deterministic assertions using weakest preconditions $wp(C,\psi)$, then a weakest preterm framework $pt(C,r)$ to handle probabilistic expressions and formulas via $WP(C,\Phi)$. The resulting sound and complete system advances formal verification of probabilistic programs with loops and lays groundwork for extensions to quantum Hoare logic and other probabilistic formalisms, with potential impact on cryptography and machine learning settings that rely on discrete distributions.
Abstract
Probabilistic Hoare logic (PHL) is an extension of Hoare logic and is specifically useful in verifying randomized programs. It allows researchers to formally reason about the behavior of programs with stochastic elements, ensuring the desired probabilistic properties are upheld. The relative completeness of satisfaction-based PHL has been an open problem ever since the birth of the first PHL in 1979. More specifically, no satisfaction-based PHL with While-loop has been proven to be relatively complete yet. This paper solves this problem by establishing a new PHL with While-loop and prove its relative completeness. The programming language concerned in our PHL is expressively equivalent to the existing PHL systems but brings a lot of convenience in showing completeness. The weakest preterm for While-loop command reveals how it changes the probabilistic properties of computer states, considering both execution branches that halt and infinite runs. We prove the relative completeness of our PHL in two steps. We first establish a semantics and proof system of Hoare triples with probabilistic programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertions, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of our PHL is then obtained as a consequence of the weakest preterm calculus.