Efficient finite case analysis for probabilistic programs #
A computed finite tag selects among certified programs retaining the original input. The finite control type and its branch machines are fixed independently of runtime input. Each branch may return values of unbounded encoded length, which its certificate charges.
Main results #
Cslib.Probability.IsPPTOn.finite_cases: finite probabilistic dispatch with captured input.
References #
Adapts Computability/Probabilistic/Finite.lean on the cslib crypto branch at
5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing tidy calculus and closed PPT rules.
theorem Cslib.Probability.IsPPTOn.finite_cases {α β Tag : Type} [Finite Tag] {input : α ↪ List Bool} {output : β ↪ List Bool} {tagEncoding : Tag ↪ List Bool} {tag : α → Tag} {branch : Tag → α → ProbComp β} (htag : Turing.MultiTapeTM.ComputableTidilyInPolyTime tag input tagEncoding) (hbranch : ∀ (choice : Tag), IsPPTOn input output (branch choice)) :
IsPPTOn input output fun (a : α) => branch (tag a) a
A fixed finite tag selects a certified probabilistic branch with captured input. The result has the chosen branch's exact distribution, including state returned with its output.