Certifying functional probabilistic programs

ppt combines the proved closed PPT rules with deterministic polytime automation. Programs use ordinary do notation, captured inputs and conditionals. Named and local certificates are reused, and tuple arguments are prepared with the shared routine-call matcher. Every proof supplies the uniform strict fair-coin machine contract of IsPPTOn. IsPPT goals and local certificates expose the standard unary-parameter/word encoding automatically.

Unknown algorithms need certificates. Fair bits, uniform words with efficiently computed unary lengths, memoized closed samplers and bounded loops with additive state growth polynomial in the original input are certified here. General loop invariants use IsPPTOn.iterate_spec; oracle PPT needs further rules.

Main definitions

• ppt: prove a closed encoded PPT certificate using the PPT and PolyTime Aesop rule sets.

References

Adapted from Cslib/Tactic/PPT.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine realization and tidy calculus.

def Cslib.Tactic.PPT.tacticPpt : Lean.ParserDescr

Certify a probabilistic program using proved sampling, composition and deterministic rules.