Caching Queries Made by a Computation

This file defines a modifier QueryImpl.withCaching that modifies a query implementation to cache results to return to the same query in the future.

We also define cachingOracle, which caches queries to the oracles in spec, querying fresh values from spec if no cached value exists.

def QueryImpl.withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) : QueryImpl spec (StateT spec.QueryCache m)

Modify a query implementation to cache previous call and return that output in the future.

@[simp]

theorem QueryImpl.withCaching_apply {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (t : spec.Domain) : so.withCaching t = do let __do_lift ← get match __do_lift t with | some u => pure u | none => do let u ← liftM (so t) modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery t u)

theorem QueryImpl.withCaching_cache_le {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSet m] (so : QueryImpl spec m) (t : spec.Domain) (cache₀ : spec.QueryCache) (z : spec.Range t × spec.QueryCache) (hz : z ∈ support ((so.withCaching t).run cache₀)) : cache₀ ≤ z.2

Running withCaching at state cache produces a result whose cache is ≥ cache. On a cache hit the state is unchanged; on a miss a single entry is added.

theorem QueryImpl.PreservesInv.withCaching_le {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] [spec₀.DecidableEq] (so : QueryImpl spec₀ ProbComp) (cache₀ : spec₀.QueryCache) : so.withCaching.PreservesInv fun (x : spec₀.QueryCache) => cache₀ ≤ x

withCaching preserves the invariant (cache₀ ≤ ·) (the cache only grows).

@[reducible, inline]

def cachingOracle {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} : QueryImpl spec (StateT spec.QueryCache (OracleComp spec))

Oracle for caching queries to the oracles in spec, querying fresh values if needed.

theorem cachingOracle.apply_eq {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (t : spec.Domain) : cachingOracle t = do let __do_lift ← get match __do_lift t with | some u => pure u | none => do let u ← liftM (OracleQuery.query t) modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery t u)

@[simp]

theorem cachingOracle.probFailure_run_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (cache : spec₀.QueryCache) : Pr[⊥ | (simulateQ cachingOracle oa).run cache] = Pr[⊥ | oa]

Trivially true via probFailure_eq_zero since both sides are OracleComp computations. A generic withCaching version for arbitrary base monads would require a separate argument because caching changes the oracle semantics (cache hits skip the underlying oracle call).

@[simp]

theorem cachingOracle.NeverFail_run_simulateQ_iff {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (cache : spec₀.QueryCache) : NeverFail ((simulateQ cachingOracle oa).run cache) ↔ NeverFail oa

Trivially true via probFailure_eq_zero; see probFailure_run_simulateQ.

@[simp]

theorem cachingOracle.simulateQ_query {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (t : spec.Domain) : simulateQ cachingOracle (liftM (OracleQuery.query t)) = cachingOracle t

def withCacheOverlay {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (cache : spec.QueryCache) (oa : OracleComp spec α) : OracleComp spec α

Run an OracleComp with a QueryCache as a priority layer over the real oracle. Cached entries are returned directly (no oracle query), misses fall through to the real oracle and get cached for subsequent lookups within the same computation.

This is the fundamental "programmable random oracle" primitive: pre-fill the cache with programmed entries, then run the computation. Concretely:

withCacheOverlay cache oa = StateT.run' (simulateQ cachingOracle oa) cache

Key properties:

• withCacheOverlay ∅ oa deduplicates queries but is otherwise equivalent to oa.
• withCacheOverlay cache (query t) returns v without an external query when cache t = some v, and queries the real oracle when cache t = none.

TODO: generalize FiatShamir.runtime to runtimeWithCache cache with runtime = runtimeWithCache ∅, deriving randomOracle evaluation from withCacheOverlay + evalDist.

@[simp]

theorem withCacheOverlay_pure {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (cache : spec.QueryCache) (a : α) : withCacheOverlay cache (pure a) = pure a

theorem withCacheOverlay_query_hit {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (cache : spec.QueryCache) (t : spec.Domain) (v : spec.Range t) (hv : cache t = some v) : withCacheOverlay cache (liftM (OracleQuery.query t)) = pure v

theorem withCacheOverlay_query_miss {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (cache : spec.QueryCache) (t : spec.Domain) (hv : cache t = none) : withCacheOverlay cache (liftM (OracleQuery.query t)) = liftM (OracleQuery.query t)

theorem OracleComp.simulateQ_cachingOracle_cache_le {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) (cache₀ : spec.QueryCache) (z : α × spec.QueryCache) (hmem : z ∈ support ((simulateQ cachingOracle oa).run cache₀)) : cache₀ ≤ z.2

simulateQ cachingOracle only grows the cache: for any oa, if z ∈ support ((simulateQ cachingOracle oa).run cache₀) then cache₀ ≤ z.2.

theorem OracleComp.cachingOracle_query_caches {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (t : spec.Domain) (cache₀ : spec.QueryCache) (v : spec.Range t) (cache₁ : spec.QueryCache) (hmem : (v, cache₁) ∈ support ((cachingOracle t).run cache₀)) : cache₁ t = some v

After running cachingOracle on a single query at t, the resulting cache maps t to the returned value.