A Formalization of the Ionescu-Tulcea Theorem in Mathlib

Schröer et al. [Philipp Schröer et al., 2023] developed a verification infrastructure for rapid prototyping of automated verification techniques for probabilistic programs (PPs), which is based on the quantitative intermediate verification language HeyVL. In a nutshell, users encode programs, specifications, and proof rules into a single HeyVL program. The verification conditions obtained from such a HeyVL program are then discharged with SMT solvers or probabilistic model checkers. However, ensuring that a HeyVL encoding is correct can be subtle and error-prone, just like reasoning about PPs in general. In this paper, we develop mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory. To this end, we formalize Markov decision processes (MDPs) - a standard model for assigning operational semantics to PPs. We construct suitable probability spaces for MDPs to ground them in probability theory. Furthermore, we develop least fixed-point characterizations of expected total costs of MDPs, which are useful for relating program logics or denotational semantics to an operational MDP semantics. We apply these characterizations to formalize sound weakest-precondition-style calculi for both partial and total correctness reasoning about the expected behavior of PPs with unbounded loops, nondeterminism, and conditioning. Finally, we develop a deep embedding of the HeyVL intermediate verification language. We apply the above machinery to prove the correctness of various existing HeyVL encodings. During that process, we improved the original HeyVL encoding of an invariant-based proof rule for loops. All of our results have been formalized in the interactive theorem prover Lean on top of mathlib.