Lazy Random Oracle Equals Eager Full-Table Sampling

For an oracle specification D →ₒ R with a single constant range R, running an OracleComp (D →ₒ R) α under the lazy random oracle (OracleSpec.randomOracle, i.e. uniformSampleImpl.withCaching) has the same output distribution as the eager strategy: sample a full answer table f : D → R uniformly, then evaluate the computation deterministically against f via evalWithAnswerFn.

The lazy oracle samples a fresh uniform value on first query and caches it for consistency, so caching only ever affects repeated queries. Since every fresh table entry is uniform and independent, lazily sampling on demand is distributionally identical to pre-sampling the whole table. The marginalization lemma evalDist_uniformSample_bind_update is the workhorse: it absorbs each fresh on-demand uniform draw into the pre-sampled table.

Main results

• evalDist_simulateQ_randomOracle_run'_eq_tableExtending: the generalized, cache-parametrized form, the induction vehicle.
• evalDist_simulateQ_randomOracle_run'_empty_eq_uniformTable: the empty-cache corollary — the lazy-vs-eager equivalence proper.

@[reducible]

def OracleComp.tableExtending {D R : Type} (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) : D → R

The total answer table obtained by overlaying a QueryCache on top of a full function table: cached entries take priority, uncached coordinates fall through to g.

theorem OracleComp.tableExtending_cacheQuery {D R : Type} [DecidableEq D] (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) (t : D) (u : R) : tableExtending (c.cacheQuery t u) g = Function.update (tableExtending c g) t u

Overlaying c.cacheQuery t u on g is the t-update of overlaying c on g.

theorem OracleComp.tableExtending_update_of_none {D R : Type} [DecidableEq D] (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) (g : D → R) {t : D} (hc : c t = none) (u : R) : Function.update (tableExtending c g) t u = tableExtending c (Function.update g t u)

When t is uncached, updating the overlaid table at t equals overlaying the cache on the updated full table.

theorem OracleComp.evalDist_uniformSample_bind_update_map {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (t : D) (ψ : (D → R) → α) : 𝒟[do let u ← $ᵗ R let g ← $ᵗ (D → R) pure (ψ (Function.update g t u))] = 𝒟[do let g ← $ᵗ (D → R) pure (ψ g)]

Marginalization, post-composed. For any continuation ψ : (D → R) → α, drawing a fresh uniform u, then a full uniform table g, and evaluating ψ on Function.update g t u has the same distribution as evaluating ψ on a directly drawn uniform table.

theorem OracleComp.evalDist_uniformSample_bind_update_two_map {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} {t₁ t₂ : D} (hne : t₁ ≠ t₂) (ψ : (D → R) → α) : 𝒟[do let u₁ ← $ᵗ R let u₂ ← $ᵗ R let g ← $ᵗ (D → R) pure (ψ (Function.update (Function.update g t₁ u₁) t₂ u₂))] = 𝒟[do let g ← $ᵗ (D → R) pure (ψ g)]

Two-cell marginalization, post-composed. For any continuation ψ : (D → R) → α and any two distinct coordinates t₁ ≠ t₂, drawing fresh independent uniforms u₁, u₂, then a full uniform table g, and evaluating ψ on the table with both coordinates overwritten yields the same distribution as evaluating ψ on a directly drawn uniform table.

This is the joint marginal independence at the coordinate pair (t₁, t₂): those two coordinates are jointly uniform and independent of the rest, so replacing them with fresh independent uniforms leaves the joint distribution unchanged. Two-cell analogue of evalDist_uniformSample_bind_update_map.

Used at the slot-positive case of the DC unlinkability reduction to marginalize the two cells ((tag, 0), n) (read by M) and ((tag, slotK), n) (read by S, with slotK ≠ 0) as independent uniforms, enabling the IH-rename closure without any per-step cacheBadReader charge.

theorem OracleComp.evalDist_simulateQ_randomOracle_run'_eq_tableExtending {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (oa : OracleComp (OracleSpec.ofFn fun (x : D) => R) α) (c : (OracleSpec.ofFn fun (x : D) => R).QueryCache) : 𝒟[(simulateQ OracleSpec.randomOracle oa).run' c] = 𝒟[do let g ← $ᵗ (D → R) pure (evalWithAnswerFn (QueryImpl.ofFn (tableExtending c g)) oa)]

Lazy random oracle equals eager full-table sampling — cache-parametrized form.

Running oa under the lazy random oracle starting from cache c yields the same output distribution as: sample a full table g : D → R uniformly, then evaluate oa deterministically against the table that overlays c on g.

This is the induction vehicle: the cache c is generalized so the query/bind step can recurse through cacheQuery.

theorem OracleComp.tableExtending_empty {D R : Type} (g : D → R) : tableExtending ∅ g = g

Overlaying the empty cache leaves a full table unchanged.

theorem OracleComp.evalDist_simulateQ_randomOracle_run'_empty_eq_uniformTable {D R : Type} [DecidableEq D] [Finite D] [Finite R] [Nonempty R] [SampleableType R] [SampleableType (D → R)] {α : Type} (oa : OracleComp (OracleSpec.ofFn fun (x : D) => R) α) : 𝒟[(simulateQ OracleSpec.randomOracle oa).run' ∅] = 𝒟[do let g ← $ᵗ (D → R) pure (evalWithAnswerFn (QueryImpl.ofFn g) oa)]

Lazy random oracle equals eager full-table sampling.

Running an OracleComp (D →ₒ R) α under the lazy random oracle from the empty cache yields the same output distribution as: sample a full answer table g : D → R uniformly, then evaluate the computation deterministically against g.

This is the empty-cache specialization of evalDist_simulateQ_randomOracle_run'_eq_tableExtending: the classic lazy-vs-eager-sampling equivalence. Lazy caching only affects repeated queries, and since each fresh table entry is uniform and independent, sampling on demand matches pre-sampling the whole table.