Documentation

VCVio.OracleComp.QueryTracking.RandomOracle.Eager

Eager Random Oracle #

The eager random oracle serves answers from a pre-generated QuerySeed, consuming values sequentially and falling back to fresh uniform sampling when exhausted. Different calls to the same oracle consume different seed values. State: QuerySeed.

This gives INDEPENDENT samples (each call consumes a different seed value), unlike randomOracle which gives CONSISTENT samples (same input → same output via caching). When averaged over a uniformly sampled seed, the eager version matches the fresh independent-query semantics of evalDist.

source
@[reducible, inline]
def eagerRandomOracle {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [(t : spec.Domain) → SampleableType (spec.Range t)] :
QueryImpl spec (StateT spec.QuerySeed ProbComp)

The eager random oracle: serves answers from a pre-generated QuerySeed, consuming seed values sequentially and falling back to fresh uniform sampling when exhausted.

Concretely, on query t:

  • If seed t is non-empty, return the head and advance to the tail.
  • If seed t is empty, sample $ᵗ spec.Range t uniformly and leave the seed unchanged.

Important: This gives INDEPENDENT samples (each call consumes a different seed value), unlike randomOracle which gives CONSISTENT samples (same input → same output via caching). The two models agree when no oracle index is queried more than once.

This is definitionally equal to uniformSampleImpl.withPregen (from SeededOracle.lean).

Instances For
    source
    theorem eagerRandomOracle.apply_eq {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} [(t : spec₀.Domain) → SampleableType (spec₀.Range t)] (t : spec₀.Domain) :
    eagerRandomOracle t = StateT.mk fun (seed : spec₀.QuerySeed) => match seed t with | u :: us => pure (u, Function.update seed t us) | [] => (fun (x : spec₀.Range t) => (x, seed)) <$> ($ᵗ spec₀.Range t)
    source
    theorem eagerRandomOracle.evalDist_simulateQ_run'_empty {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} [(t : spec₀.Domain) → SampleableType (spec₀.Range t)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) :
    evalDist ((simulateQ eagerRandomOracle oa).run' ∅) = evalDist oa

    With an empty seed, the eager random oracle reduces to uniformSampleImpl: every query falls through to fresh uniform sampling with no state change. This is a faithful simulation (preserves evalDist).

    source
    theorem eagerRandomOracle_evalDist_generateSeed_bind {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} [(t : spec₀.Domain) → SampleableType (spec₀.Range t)] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (qc : ι₀ → ℕ) (js : List ι₀) :
    (evalDist do let seed ← OracleComp.generateSeed spec₀ qc js (simulateQ eagerRandomOracle oa).run' seed) = evalDist oa

    The eager random oracle, averaged over a uniformly sampled seed, matches the fresh independent-query semantics of evalDist. This is because the pre-sampled seed values are i.i.d. uniform, exactly matching fresh oracle queries.

    This is the analog of seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run' but for eagerRandomOracle (which falls back to ProbComp rather than OracleComp spec).