Documentation

CslibFrontier.Tactic.PPT

Certifying functional probabilistic programs #

ppt combines the proved closed and oracle PPT rules with deterministic polytime automation. Programs use ordinary do notation, captured inputs and conditionals with plain ComputableInPolyTime guards (cond', ite'). Named and local certificates are reused, and tuple arguments are prepared with the shared routine-call matcher. Closed proofs supply 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.

Strict oracle PPT goals (IsOraclePPTOn, IsOraclePPT) search with the OraclePPT, PPT and PolyTime Aesop rule sets while keeping simp disabled on oracle goals so charged reply prefixes (List.take _ <$> ProbOracleComp.query _) are never fused into surrounding maps or binds. Local and structure-field oracle routine calls prepare tuple arguments with IsOraclePPTOn.preprocess'; pure, ProbOracleComp.sample and query_take' bridge to deterministic PolyTime, closed PPT and plain request/limit bounds; sequencing, captured maps, plain conditionals and bounded-growth OracleComp.iterate loops search jointly. Handler substitution and general adaptive loop invariants keep their explicit theorems (IsOraclePPT.run_interpret_preprocess', IsOraclePPTOn.iterate_spec', IsOraclePPTOn.iterateWith_spec').

Before searching, ppt [f, g] unfolds the hinted definitions in the goal and inlines the lets they expose. Every form also unfolds local encoding lets and adds the certificates stored in fields of local structures as local facts, as polytime does. On ordinary failure, ppt includes one failed compositional attempt when the backend has reported one, as polytime does.

Main definitions #

References #

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

source
theorem Cslib.Tactic.PPT.Internal.oracleIterate_of_length_le {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : σ → Probability.WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableInPolyTime initial input stateEncoding) (hstep : Probability.IsOraclePPTOn stateEncoding stateEncoding step) (hshrink : ∀ (state next : σ), next ∈ OracleComp.support (step state) → (stateEncoding next).length ≤ (stateEncoding state).length) :
Probability.IsOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)

Iteration of a strict oracle PPT step that never increases its encoded state needs no additive growth constant.

source
def Cslib.Tactic.PPT.Internal.nonOracleNormSimp :
Aesop.RuleTac

PolyTime normalization simp skipped on oracle PPT goals so charged queries stay intact.

Instances For
    source
    def Cslib.Tactic.PPT.Internal.nonOracleSimpFallback :
    Aesop.RuleTac

    PolyTime fallback simp skipped on oracle PPT goals so charged queries stay intact.

    Instances For
      source
      def Cslib.Tactic.PPT.pptTactic :
      Lean.ParserDescr

      Certify a closed or oracle probabilistic program using proved sampling, composition and deterministic rules. Goals may be IsPPTOn, IsPPT, IsOraclePPTOn or IsOraclePPT.

      ppt [f, g] first unfolds the definitions f and g in the goal. Like polytime, every form replaces local encoding lets by their values and adds the certificates stored in fields of local structures (S.encrypt_ppt, hA.guess, …) as local facts.

      Instances For
        source
        def Cslib.Tactic.PPT.evalPPT :
        Lean.Elab.Tactic.Tactic

        Elaborate ppt: prepare the goal and unfold IsOraclePPT before and after exposing structure fields, then search with [OraclePPT, PPT, PolyTime] (preserving query syntax) on oracle goals or [PPT, PolyTime] on closed goals.

        Instances For