feat(framework): deferred-sampling + relational-coupling engine

[alik-eth]

Adds the deferred-sampling and relational-coupling engine that the GPV/#188 and MLDSA/#228 security proofs build on. Purely additive: no existing declaration is changed or removed.

What's included

• VCVio/OracleComp/QueryTracking/RandomOracle/DeferredSampling.lean — expectation algebra for deferred draws: i.i.d. bind-commutation (evalDist_bind_comm), the ε-multiplicity kernel (tsum_probOutput_fresh_mul_count_le), the Factorizes front-tape predicate with evalDist_step_commute_tape, and the state-relation transfer lemma tsum_probOutput_simulateQ_run_mul_of_rel.
• VCVio/OracleComp/QueryTracking/RandomOracle/ProbeEps.lean — hidden-target read games: single-target q·ε bound (probEvent_hiddenReadMany_le), i.i.d. multi-key n·q·ε bound (probEvent_hiddenReadList_le), the averaged E[n]·q·ε bridge, single-draw deferral (probEvent_bind_fire_le_of_gen), and the explicit front-block drawList.
• VCVio/ProgramLogic/Relational/SimulateQ.lean (additions) — relational-triple monotonicity/implication lemmas, the single-world expected-query-slack accumulator (probEvent_bad_simulateQ_run_le_expectedQuerySlack), and the bare-measure averaged-bad primitives (avgBadM, postStepOutM, avgBadM_query_bind_eq_tsum_output, tsum_tsum_postStepOutM_mul) used by the aborting-signer coupling.
• VCVio/ProgramLogic/Relational/ProgrammingOracle.lean (additions) — TV-distance-to-bad-event bounds for programmed random oracles, including the caching/programming bridge consumed by the GPV reduction.
• VCVio/EvalDist/Defs/Basic.lean (additions) — the first-moment bound probEvent_le_tsum_probOutput_mul_cost (+ support-restricted variant).

A soundness note for reviewers of the averaged-bad layer: the per-output invariant threading is stated over un-normalized sub-probability state measures (postStepOutM has no output-conditioning division), which is the formulation that avoids the mass-concentration pathology of a per-output conditioned invariant. The packaged PMF-typed telescoping layer that earlier drafts carried was dropped — both downstream consumers telescope directly from the bare-measure primitives, so only the consumed API ships.

Verification

• lake build of the full CI library set: green.
• #print axioms on the load-bearing engine lemmas (probEvent_le_of_relTriple_simulateQ_run, probEvent_bad_simulateQ_run_le_expectedQuerySlack, tvDist_simulateQ_randomOracle_withProgramming_le_probEvent_bad, probEvent_hiddenReadList_le, probEvent_bind_fire_le_of_gen, tsum_probOutput_fresh_mul_count_le, evalDist_step_commute_tape, tsum_probOutput_simulateQ_run_mul_of_rel): all [propext, Classical.choice, Quot.sound] — no sorryAx, no custom axioms.
• New files are clean under -Dweak.linter.mathlibStandardSet=true.

Relation to the other PRs

The GPV/#188+Falcon PR and the MLDSA/#228 PR are stacked on this branch and consume this engine; this PR must merge first.

[github-actions]

🤖 PR Summary

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	2034
❌ Lines Removed	18

---

Lean Declarations

✏️ Removed: 1 declaration(s)

VCVio/CryptoFoundations/ReplayFork.lean (1)

• private lemma tsum_probOutput_map_mul [IsUniformSpec spec] {γ δ : Type} (mn : OracleComp spec γ)

✏️ Added: 60 declaration(s)

VCVio/EvalDist/Defs/Basic.lean (2)

• lemma probEvent_le_tsum_probOutput_mul_cost (mx : m α) (p : α → Prop) (c : α → ℝ≥0∞)
• lemma probEvent_le_tsum_probOutput_mul_cost_of_mem_support

VCVio/EvalDist/Monad/Basic.lean (4)

• lemma tsum_probOutput_bind_mul (mx : m α) (g : α → m β) (f : β → ℝ≥0∞) :
• lemma tsum_probOutput_map_mul [LawfulMonad m] (mx : m α) (f : α → β) (g : β → ℝ≥0∞) :
• lemma tsum_probOutput_mul_of_const_on_support [MonadLiftT m SetM] [EvalDistCompatible m]
• lemma tsum_probOutput_pure_mul (y : α) (f : α → ℝ≥0∞) :

VCVio/OracleComp/QueryTracking/RandomOracle/DeferredSampling.lean (9)

• def Factorizes {γ τ : Type} (run : ProbComp γ) (tape : ProbComp τ)
• lemma tsum_count_eq_length {C : Type} [DecidableEq C] (rl : List C) :
• lemma tsum_probOutput_fresh_mul_count_le {C P : Type} [DecidableEq C]
• theorem Factorizes.bind {γ τ δ : Type} {run : ProbComp γ} {tape : ProbComp τ}
• theorem evalDist_bind_comm {α β γ : Type} (oa : ProbComp α) (ob : ProbComp β)
• theorem evalDist_bind_congr_left {α β : Type} (oa : ProbComp α) (f g : α → ProbComp β)
• theorem evalDist_bind_const_neverFails {α γ : Type} (od : ProbComp α) (hmass : Pr[⊥ | od] = 0)
• theorem evalDist_step_commute_tape {γ S Ans τ ρ : Type}
• theorem tsum_probOutput_simulateQ_run_mul_of_rel

VCVio/OracleComp/QueryTracking/RandomOracle/ProbeEps.lean (17)

• @[simp] lemma probFailure_drawList (oa : ProbComp R) (n : ℕ) :
• lemma tsum_probOutput_drawList_eq_one (oa : ProbComp R) (n : ℕ) :
• noncomputable def drawList (oa : ProbComp R) : ℕ → ProbComp (List R)
• noncomputable def hiddenReadList (oa : ProbComp R) (q : ℕ) (σ : List Bool → R) :
• noncomputable def hiddenReadMany (oa : ProbComp R) (q : ℕ) (σ : List Bool → R) : ProbComp Bool
• noncomputable def readMany (w : R) : ℕ → (List Bool → R) → Bool
• noncomputable def readManyList (ws : List R) (q : ℕ) (σ : List Bool → R) : Bool
• theorem probEvent_bind_const_or_pure (q : Bool) (mb : ProbComp Bool) :
• theorem probEvent_bind_fire_eq_defer {α : Type} (oa : ProbComp R)
• theorem probEvent_bind_fire_le_of_gen {α : Type} {oa : ProbComp R} {ε : ℝ≥0∞}
• theorem probEvent_bind_fire_le_of_marginal_eq_readMany {α : Type} {oa : ProbComp R} {ε : ℝ≥0∞}
• theorem probEvent_bind_hiddenReadList_le {oa : ProbComp R} {ε : ℝ≥0∞}
• theorem probEvent_hiddenReadList_le {oa : ProbComp R} {ε : ℝ≥0∞} (hε : ∀ r : R, Pr[= r | oa] ≤ ε)
• theorem probEvent_hiddenReadMany_le {oa : ProbComp R} {ε : ℝ≥0∞}
• theorem probEvent_le_of_eq_bind_hiddenReadList {β : Type} {run : ProbComp β} {bad : β → Prop}
• theorem readManyList_true_iff (ws : List R) (q : ℕ) (σ : List Bool → R) :
• theorem readMany_true_iff (w : R) (q : ℕ) (σ : List Bool → R) :

VCVio/ProgramLogic/Relational/ProgrammingOracle.lean (4)

• private lemma probOutput_withProgramming_eq_withCachingTrackingPolicy_of_not_bad_output'
• theorem tvDist_simulateQ_randomOracle_withProgramming_le_probEvent_bad
• theorem tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad'
• theorem tvDist_withProgramming_withCachingTrackingPolicy_run_le_probEvent_bad'

VCVio/ProgramLogic/Relational/SimulateQ.lean (24)

• lemma avgBadM_eq_tsum_pure
• lemma avgBadM_pure_state
• lemma avgBadM_pure
• lemma avgBadM_query_bind_eq_tsum_output
• lemma avgBadM_query_bind_eq
• lemma avgBadM_telescope_eq_tsum_postStep
• lemma expectedQuerySlack_charged_read_expected_growth_le
• lemma expectedQuerySlack_expected_resource_le
• lemma tsum_tsum_postStepOutM_mul
• noncomputable def avgBadM
• noncomputable def postStepJointM
• noncomputable def postStepOutM
• private lemma probOutput_simulateQ_run_eq_of_not_output_bad'
• private lemma probOutput_simulateQ_run_eq_zero_of_output_bad'
• private lemma tsum_probOutput_mul_tvDist_le_const
• private lemma tsum_prod_right_bool_eq_of_zero {A B : Type} (f : A × B × Bool → ℝ≥0∞)
• theorem probEvent_bad_simulateQ_run_le_expectedQuerySlack
• theorem probEvent_dist_simulateQ_mono
• theorem probEvent_le_of_relTriple_imp
• theorem probEvent_marginal_simulateQ_mono
• theorem probEvent_output_bad_eq'
• theorem relTriple_simulateQ_run_mono
• theorem tvDist_simulateQ_run_le_probEvent_output_bad
• theorem tvDist_simulateQ_run_le_queryBoundP_mul

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• VCVio/ProgramLogic/Relational/SimulateQ.lean (+1083/-0)

---

📄 **Per-File Summaries**

• VCVio.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/CryptoFoundations/ReplayFork.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/EvalDist/Defs/Basic.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/EvalDist/Monad/Basic.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/OracleComp/QueryTracking/RandomOracle/DeferredSampling.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/OracleComp/QueryTracking/RandomOracle/ProbeEps.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/ProgramLogic/Relational/ProgrammingOracle.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
• VCVio/ProgramLogic/Relational/SimulateQ.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}

---

Last updated: 2026-07-02 19:09 UTC.

[dtumad]

Could you add this in VCVio/EvalDist/Monad/* somewhere and state it over a general monad instead? Also I think this could reasonably be simp.

[alik-eth]

Done in e110e6e — moved to VCVio/EvalDist/Monad/Basic.lean (new Expectation algebra section), stated over a general monad with [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF], and tagged @[simp].

[dtumad]

These three other tsum lemmas could be generalized too I think.

[alik-eth]

Done — all four now live there. tsum_probOutput_map_mul additionally takes [LawfulMonad m], and tsum_probOutput_mul_of_const_on_support takes [MonadLiftT m SetM] [EvalDistCompatible m] for the support reasoning. The general map lemma also subsumes the private tsum_probOutput_map_mul that ReplayFork.lean was carrying, so that copy is gone too. The two downstream PRs (#466, #467) are rebased onto this.

[dtumad]

If you wanted to try I think this theory could also be abstracted into m with LawfulMonadLiftT m SPMF, but we could leave it at ProbComp for now and generalizing later when there is a consumer.

[alik-eth]

Agreed — leaving the Factorizes theory at ProbComp for now as you suggest. Both current consumers (the GPV tape factorization in #466 and the Fiat–Shamir-with-abort coupling in #467) instantiate at ProbComp, so I'd rather generalize to [LawfulMonadLiftT m SPMF] once a genuinely monad-parametric consumer exists.

[alik-eth]

Review addressed in e110e6e: the four expectation-algebra lemmas now live in VCVio/EvalDist/Monad/Basic.lean, stated over a general monad, with tsum_probOutput_pure_mul tagged @[simp]; the general map lemma also replaces the private copy in ReplayFork.lean. #466 and #467 are rebased on top. Full CI library set builds clean locally with the new @[simp] in place. @dtumad ready for another look.

[dtumad]

Thanks, I think this looks good to merge now.