Lazy Random Oracle #
The (lazy) random oracle samples a fresh uniform value on first query and caches the result
for future consistency. Same input always yields same output. State: QueryCache.
This is uniformSampleImpl.withCaching.
@[reducible, inline]
def
randomOracle
{ι : Type}
[DecidableEq ι]
{spec : OracleSpec ι}
[(t : spec.Domain) → SampleableType (spec.Range t)]
:
QueryImpl spec (StateT spec.QueryCache ProbComp)
The (lazy) random oracle: uniform sampling with caching.
On query t, returns the cached value if present, otherwise samples $ᵗ spec.Range t
uniformly and caches the result. This ensures consistency: same input → same output.
Instances For
theorem
randomOracle.apply_eq
{ι₀ : Type}
[DecidableEq ι₀]
{spec₀ : OracleSpec ι₀}
[(t : spec₀.Domain) → SampleableType (spec₀.Range t)]
(t : spec₀.Domain)
:
randomOracle t = do
let __do_lift ← get
match __do_lift t with
| some u => pure u
| none => do
let u ← liftM ($ᵗ spec₀.Range t)
modifyGet fun (cache : spec₀.QueryCache) => (u, cache.cacheQuery t u)