Deferred sampling: tape factorization of answer-irrelevant draws

This module collects the reusable, scheme-independent kernels behind the deferred-sampling technique: rewriting a probabilistic computation whose per-step draws do not influence the control flow into one where those draws are front-loaded into a single independent "tape", drawn ahead of time and then consumed.

The technique underlies several proofs in this library (Fiat–Shamir with abort, GPV preimage sampling, collision/birthday bounds). Those proofs each instantiate a bespoke state machine; what is genuinely generic — and lives here — is:

• i.i.d. bind-commutation (evalDist_bind_comm, evalDist_bind_const_neverFails, evalDist_bind_congr_left): the answer-irrelevant draw commutes past its continuation step at the distribution level. OracleComp's syntactic bind is not commutative, but its evalDist image into SPMF is; this is what lets a per-step draw be moved to the front tape.
• The list-multiplicity ε-kernel (tsum_count_eq_length, tsum_probOutput_fresh_mul_count_le): one fresh draw w ← oa, independent of a value-free list rl, contributes expected multiplicity E[rl.count (key w)] ≤ ε · rl.length whenever each slot is hit with probability ≤ ε. This is the single source of the ε in deferred-sampling read bounds.
• The general factorization statement (DeferredTape.Factorizes): an abstract predicate packaging "the read-recording run distributes as a single front draw block followed by a tape-consuming run". Scheme-specific factorizations (e.g. FiatShamirWithAbort.evalDist_deferredDrawRead_eq_drawList_tapeDrawRead) are instances of this shape; the predicate names the target so downstream consumers share vocabulary.

The genuinely hard, scheme-specific glue — proving a particular state machine's run is a tape factorization — is not generic and stays with each scheme. What this module provides is the toolbox that those proofs are built out of.

i.i.d. bind-commutation at the distribution level

These lemmas implement the answer-irrelevant draw commutes past its continuation step. OracleComp's bind is syntactic and not commutative as a free monad, but its evalDist image into SPMF is — the two iterated sums over independent draws exchange by ENNReal.tsum_comm. This is the local resampling step that front-loads a draw whose value the rest of the computation may use but whose position is irrelevant.

theorem OracleComp.DeferredSampling.evalDist_bind_comm {α β γ : Type} (oa : ProbComp α) (ob : ProbComp β) (k : α → β → ProbComp γ) : 𝒟[do let a ← oa let b ← ob k a b] = 𝒟[do let b ← ob let a ← oa k a b]

i.i.d. bind-commutation. Two independent draws oa, ob feeding a common continuation k may be drawn in either order without changing the output distribution.

theorem OracleComp.DeferredSampling.evalDist_bind_const_neverFails {α γ : Type} (od : ProbComp α) (hmass : Pr[⊥ | od] = 0) (k : ProbComp γ) : 𝒟[do let _ ← od k] = 𝒟[k]

Dropping a never-failing value-irrelevant prefix. A leading draw od whose continuation ignores its value contributes only its total mass; when od never fails (mass 1, e.g. a drawList front block) it can be discarded from the output distribution.

theorem OracleComp.DeferredSampling.evalDist_bind_congr_left {α β : Type} (oa : ProbComp α) (f g : α → ProbComp β) (h : ∀ (a : α), 𝒟[f a] = 𝒟[g a]) : 𝒟[oa >>= f] = 𝒟[oa >>= g]

Distribution-level congruence under a leading bind. If two continuations agree as distributions pointwise then the bound computations agree as distributions.

The list-multiplicity ε-kernel

The single source of the ε in a deferred-sampling read bound: one fresh draw, independent of a value-free list, hits each list slot with probability ≤ ε.

theorem OracleComp.DeferredSampling.tsum_count_eq_length {C : Type} [DecidableEq C] (rl : List C) : ∑' (rc : C), ↑(List.count rc rl) = ↑rl.length

Summing the multiplicity rl.count rc of every element rc over the whole index type recovers the list length (the multiplicities partition the list).

theorem OracleComp.DeferredSampling.tsum_probOutput_fresh_mul_count_le {C P : Type} [DecidableEq C] (oa : ProbComp (C × P)) (rl : List C) (ε : ℝ) (hGuess : ∀ (cm : C), Pr[= cm | Prod.fst <$> oa] ≤ ENNReal.ofReal ε) : ∑' (w : C × P), Pr[= w | oa] * ↑(List.count w.1 rl) ≤ ENNReal.ofReal ε * ↑rl.length

The atomic value-free charge. One fresh draw w ← oa : ProbComp (C × P), independent of a value-free list rl : List C, contributes expected multiplicity E[rl.count (key w)] ≤ ε · rl.length: each of the rl.length slots of rl is hit by the fresh draw's key with probability Pr[= slot | key <$> oa] ≤ ε.

Stated for key = Prod.fst (a draw of a (C × P)-pair, of which only the C-component is matched against the list), as it arises when a commitment draw carries an auxiliary private state. This is the irreducible probabilistic kernel of a deferred-sampling read bound.

The general factorization shape

The hard, scheme-specific content of deferred sampling is proving that a particular read-recording run equals a front-tape factorization. The shape of that target is generic and named here, so that scheme instances and downstream consumers share a single vocabulary.

def OracleComp.DeferredSampling.Factorizes {γ τ : Type} (run : ProbComp γ) (tape : ProbComp τ) (tapeRun : τ → ProbComp γ) : Prop

The deferred-tape factorization predicate. Factorizes run tape tapeRun asserts that running the deferred-draw computation run : ProbComp γ is distributionally identical to first drawing an independent front tape tape : ProbComp τ and then running the tape-consuming variant tapeRun : τ → ProbComp γ that reads its per-step draws off the tape head-first:

𝒟[run] = 𝒟[tape >>= tapeRun].

A scheme establishes this by induction on its adversary computation: at an answer-irrelevant step the front tape commutes past the query (evalDist_bind_comm), and at a drawing step the inline draw block is split off the front tape. The over-provisioned suffix of the tape is discarded by the never-failing prefix lemma (evalDist_bind_const_neverFails). See FiatShamirWithAbort.evalDist_deferredDrawRead_eq_drawList_tapeDrawRead for a worked instance.

theorem OracleComp.DeferredSampling.Factorizes.bind {γ τ δ : Type} {run : ProbComp γ} {tape : ProbComp τ} {tapeRun : τ → ProbComp γ} (h : Factorizes run tape tapeRun) (k : γ → ProbComp δ) : Factorizes (run >>= k) tape fun (t : τ) => tapeRun t >>= k

A factorization may be rewritten through any distribution-level continuation: if run factorizes through tape/tapeRun, then binding a continuation k after run factorizes through tape and tapeRun >=> k (definitional unfolding plus evalDist_bind associativity). This is the recombination step used when a factorized head feeds a fold.

The answer-irrelevant step commute (the framework induction step)

The inductive heart of a tape factorization is: at a query whose per-step draw does not consult the tape, the front tape commutes past the step. This is the abstract, state-shape-independent form of that step — it takes the per-continuation factorization as a hypothesis (the inductive hypothesis) and concludes the factorization for one more leading answer-irrelevant step. Drawing and read steps are handled by their own (scheme-specific) splice/commute; this is the answer-irrelevant case, which is fully generic.

theorem OracleComp.DeferredSampling.evalDist_step_commute_tape {γ S Ans τ ρ : Type} (step : ProbComp (Ans × S)) (tape : ProbComp τ) (proj : γ × ρ → γ × S) (defCont : Ans → S → ProbComp (γ × S)) (tapeCont : Ans → S × τ → ProbComp (γ × ρ)) (hcont : ∀ (a : Ans) (s' : S), 𝒟[defCont a s'] = 𝒟[do let t ← tape proj <$> tapeCont a (s', t)]) : 𝒟[do let p ← step defCont p.1 p.2] = 𝒟[do let t ← tape proj <$> do let p ← (fun (p : Ans × S) => (p.1, p.2, t)) <$> step tapeCont p.1 p.2]

Answer-irrelevant step commutes past the front tape. An answer-irrelevant step step : ProbComp (Ans × S) (a query whose answer-draw does not consult the front tape) composed with a deferred continuation defCont factors as the front tape tape : ProbComp τ drawn first, followed by a tape-threaded continuation:

• defCont a s' : ProbComp (γ × S) is the deferred continuation after the step;
• tapeCont a (s', t) : ProbComp (γ × ρ) is its tape-consuming variant, threading the tape t;
• proj : γ × ρ → γ × S discards the spent-tape suffix on output.

Given the per-continuation factorization hcont (supplied by the inductive hypothesis), the leading answer-irrelevant step commutes past the front draw block: the continuation is rewritten by hcont under the step bind (evalDist_bind_congr_left), the front tape commutes past the answer-irrelevant step (evalDist_bind_comm), and the inner step bind is re-associated into the mapped tape-step form (bind_map_left/map_bind). This is the genuine framework content of a tape factorization's non-drawing case; see FiatShamirWithAbort.evalDist_tapePreserving_step_commute for the worked Fiat–Shamir instance (tape := drawList (ids.commit pk sk) L, S := DeferredReadState …).

State-relation transfer for expected output functionals

The value-substitution lemmas of deferred sampling (e.g. "the recorded read list of the run is independent of the rejected-draw content of the start state") are instances of a single generic fact: an expected output functional through simulateQ impl of a StateT σ ProbComp handler is equal at two start states related by Rel, provided every query step transfers Rel to its continuation and the functional is Rel-invariant.

theorem OracleComp.DeferredSampling.tsum_probOutput_simulateQ_run_mul_of_rel {ι : Type} {spec : OracleSpec ι} {σ : Type} (impl : QueryImpl spec (StateT σ ProbComp)) {γ : Type} (oa : OracleComp spec γ) (Rel : σ → σ → Prop) (hstep : ∀ (t : spec.Domain) (s₁ s₂ : σ), Rel s₁ s₂ → ∀ (K : spec.Range t → σ → ENNReal), (∀ (b : spec.Range t) (t₁ t₂ : σ), Rel t₁ t₂ → K b t₁ = K b t₂) → ∑' (p : spec.Range t × σ), Pr[= p | (impl t).run s₁] * K p.1 p.2 = ∑' (p : spec.Range t × σ), Pr[= p | (impl t).run s₂] * K p.1 p.2) (F : γ → σ → ENNReal) : (∀ (g : γ) (s₁ s₂ : σ), Rel s₁ s₂ → F g s₁ = F g s₂) → ∀ (s₁ s₂ : σ), Rel s₁ s₂ → ∑' (z : γ × σ), Pr[= z | (simulateQ impl oa).run s₁] * F z.1 z.2 = ∑' (z : γ × σ), Pr[= z | (simulateQ impl oa).run s₂] * F z.1 z.2

State-relation transfer for an expected output functional. Let impl : QueryImpl spec (StateT σ ProbComp) and let Rel : σ → σ → Prop be a relation on the handler state. Suppose:

• every query step transfers Rel: for Rel-related start states and any Rel-invariant continuation functional K, the per-query expected K agrees at the two states (hstep);
• the output functional F : γ → σ → ℝ≥0∞ is Rel-invariant (hF).

Then the run-level expected output ∑' z, Pr[= z | (simulateQ impl oa).run s] * F z.1 z.2 agrees at Rel-related start states s₁, s₂. The proof inducts on oa: at pure the output is the start state (hF applies); at a query bind the step's expected continuation functional is itself Rel-invariant by the inductive hypothesis, so hstep closes the step.

This is the generic value-substitution engine; a scheme discharges hstep by its per-query run shapes. See FiatShamirWithAbort.deferredDrawRead_run_count_dl_invariant for the worked instance (the recorded read-list multiplicity is invariant under the start drawn-list and bad-flag).