Seed-Based Forking Lemma — Program Logic Bridge

Wraps the probabilistic seeded forking lemma bounds from CryptoFoundations/SeededFork.lean as quantitative Hoare triples (Triple) for use in the program logic framework.

theorem OracleComp.ProgramLogic.triple_seededFork {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [spec.DecidableEq] [unifSpec ⊂ₒ spec] {α : Type} (main : OracleComp spec α) (qb : ι → ℕ) (js : List ι) (i : ι) (cf : α → Option (Fin (qb i + 1))) [spec.Fintype] [spec.Inhabited] [unifSpec.LawfulSubSpec spec] : Triple (have acc := ∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; acc * (acc / ↑q - h⁻¹)) (main.seededFork qb js i cf) fun (r : Option (α × α)) => if r.isSome = true then 1 else 0

Seeded forking lemma as a quantitative Hoare triple for the fork-success event.