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_run_some {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec m) {t : spec.Domain} {cache : spec.QueryCache} {u : spec.Range t} (hcache : cache t = some u) : (so.withCaching t).run cache = pure (u, cache)

theorem QueryImpl.withCaching_run_none {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec m) {t : spec.Domain} {cache : spec.QueryCache} (hcache : cache t = none) : (so.withCaching t).run cache = (fun (u : spec.Range t) => (u, cache.cacheQuery t u)) <$> so t

Caching with auxiliary state

def QueryImpl.withCachingAux {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {Q : Type w} {m' : Type (max u w) → Type v} [Monad m'] (hit : (t : spec.Domain) → spec.Range t → spec.QueryCache → Q → Q) (miss : (t : spec.Domain) → spec.QueryCache → Q → m' (spec.Range t × Q)) : QueryImpl spec (StateT (spec.QueryCache × Q) m')

Cache responses while threading an auxiliary state component.

The cache is consulted first. On a hit, the cached response is returned and the auxiliary state is updated by hit. On a miss, miss produces both the response and the next auxiliary state; the response is then installed in the cache.

@[simp]

theorem QueryImpl.withCachingAux_apply {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {Q : Type w} {m' : Type (max u w) → Type v} [Monad m'] (hit : (t : spec.Domain) → spec.Range t → spec.QueryCache → Q → Q) (miss : (t : spec.Domain) → spec.QueryCache → Q → m' (spec.Range t × Q)) (t : spec.Domain) (s : spec.QueryCache × Q) : (withCachingAux hit miss t).run s = match s.1 t with | some u => pure (u, s.1, hit t u s.1 s.2) | none => (fun (p : spec.Range t × Q) => (p.1, s.1.cacheQuery t p.1, p.2)) <$> miss t s.1 s.2

theorem QueryImpl.withCachingAux_run_proj_eq {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {Q : Type u} [LawfulMonad m] (base : QueryImpl spec m) (hit : (t : spec.Domain) → spec.Range t → spec.QueryCache → Q → Q) (miss : (t : spec.Domain) → spec.QueryCache → Q → m (spec.Range t × Q)) (hmiss : ∀ (t : spec.Domain) (cache : spec.QueryCache) (q : Q), Prod.fst <$> miss t cache q = base t) {α : Type u} (oa : OracleComp spec α) (cache : spec.QueryCache) (q : Q) : Prod.map id Prod.fst <$> (simulateQ (withCachingAux hit miss) oa).run (cache, q) = (simulateQ base.withCaching oa).run cache

Projecting away the auxiliary state of withCachingAux recovers ordinary caching whenever the miss handler has the same output marginal as the base implementation.

theorem QueryImpl.withCachingAux_run'_eq {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {Q : Type u} [LawfulMonad m] (base : QueryImpl spec m) (hit : (t : spec.Domain) → spec.Range t → spec.QueryCache → Q → Q) (miss : (t : spec.Domain) → spec.QueryCache → Q → m (spec.Range t × Q)) (hmiss : ∀ (t : spec.Domain) (cache : spec.QueryCache) (q : Q), Prod.fst <$> miss t cache q = base t) {α : Type u} (oa : OracleComp spec α) (cache : spec.QueryCache) (q : Q) : (simulateQ (withCachingAux hit miss) oa).run' (cache, q) = (simulateQ base.withCaching oa).run' cache

Output-only corollary of withCachingAux_run_proj_eq.

theorem QueryImpl.withCachingAux_aux_inv_of_mem {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {Q : Type w} {m' : Type (max u w) → Type v} [Monad m'] [LawfulMonad m'] [HasEvalSet m'] (hit : (t : spec.Domain) → spec.Range t → spec.QueryCache → Q → Q) (miss : (t : spec.Domain) → spec.QueryCache → Q → m' (spec.Range t × Q)) (inv : Q → Prop) (hhit : ∀ (t : spec.Domain) (u : spec.Range t) (cache : spec.QueryCache) (q : Q), inv q → inv (hit t u cache q)) (hmiss : ∀ (t : spec.Domain) (cache : spec.QueryCache) (q : Q), inv q → ∀ p ∈ support (miss t cache q), inv p.2) {t : spec.Domain} {cache : spec.QueryCache} {q : Q} {z : spec.Range t × spec.QueryCache × Q} (hq : inv q) (hz : z ∈ support ((withCachingAux hit miss t).run (cache, q))) : inv z.2.2

One-step invariant preservation for the auxiliary component of withCachingAux.

theorem QueryImpl.PreservesInv.withCachingAux_aux {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} {Q₀ : Type} (hit : (t : spec₀.Domain) → spec₀.Range t → spec₀.QueryCache → Q₀ → Q₀) (miss : (t : spec₀.Domain) → spec₀.QueryCache → Q₀ → ProbComp (spec₀.Range t × Q₀)) (inv : Q₀ → Prop) (hhit : ∀ (t : spec₀.Domain) (u : spec₀.Range t) (cache : spec₀.QueryCache) (q : Q₀), inv q → inv (hit t u cache q)) (hmiss : ∀ (t : spec₀.Domain) (cache : spec₀.QueryCache) (q : Q₀), inv q → ∀ p ∈ support (miss t cache q), inv p.2) : (withCachingAux hit miss).PreservesInv fun (s : spec₀.QueryCache × Q₀) => inv s.2

A withCachingAux handler preserves an invariant on its auxiliary component when both hit and miss auxiliary updates preserve it.

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).

Forward query bounds for withCaching

A wrapped step makes ≤ 1 underlying query (zero on a hit, one on a miss), so any bound on so t transfers to (so.withCaching t).run cache.

theorem QueryImpl.isQueryBoundP_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (t : spec.Domain) {p : ι' → Prop} [DecidablePred p] {n : ℕ} (h : (so t).IsQueryBoundP p n) (cache : spec.QueryCache) : ((so.withCaching t).run cache).IsQueryBoundP p n

theorem QueryImpl.isTotalQueryBound_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) (t : spec.Domain) {n : ℕ} (h : (so t).IsTotalQueryBound n) (cache : spec.QueryCache) : ((so.withCaching t).run cache).IsTotalQueryBound n

theorem QueryImpl.isPerIndexQueryBound_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (so : QueryImpl spec (OracleComp spec)) (t : spec.Domain) {qb : ι → ℕ} (h : (so t).IsPerIndexQueryBound qb) (cache : spec.QueryCache) : ((so.withCaching t).run cache).IsPerIndexQueryBound qb

Parametric simulateQ lifts for withCaching

theorem OracleComp.IsQueryBoundP.simulateQ_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {α : Type u} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] (so : QueryImpl spec (OracleComp spec')) {oa : OracleComp spec α} {n : ℕ} (h : oa.IsQueryBoundP p n) (hstep_p : ∀ (t : ι), p t → (so t).IsQueryBoundP q 1) (hstep_np : ∀ (t : ι), ¬p t → (so t).IsQueryBoundP q 0) (cache : spec.QueryCache) : ((simulateQ so.withCaching oa).run cache).IsQueryBoundP q n

theorem OracleComp.IsTotalQueryBound.simulateQ_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {ι' : Type u} {spec' : OracleSpec ι'} {α : Type u} (so : QueryImpl spec (OracleComp spec')) {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain), (so t).IsTotalQueryBound 1) (cache : spec.QueryCache) : ((simulateQ so.withCaching oa).run cache).IsTotalQueryBound n

theorem OracleComp.IsPerIndexQueryBound.simulateQ_run_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α : Type u} (so : QueryImpl spec (OracleComp spec)) {oa : OracleComp spec α} {qb : ι → ℕ} (h : oa.IsPerIndexQueryBound qb) (hstep : ∀ (t : spec.Domain), (so t).IsPerIndexQueryBound (Function.update 0 t 1)) (cache : spec.QueryCache) : ((simulateQ so.withCaching oa).run cache).IsPerIndexQueryBound qb

@[reducible, inline]

def OracleSpec.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.eq_withCaching {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} : OracleSpec.cachingOracle = (QueryImpl.ofLift spec (OracleComp spec)).withCaching

Definitional unfold of cachingOracle as caching wrapped around the lifting handler.

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

theorem cachingOracle.run_some {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {t : spec.Domain} {cache : spec.QueryCache} {u : spec.Range t} (h : cache t = some u) : (OracleSpec.cachingOracle t).run cache = pure (u, cache)

Cache hit: cachingOracle t returns the stored value without an underlying query.

theorem cachingOracle.run_none {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {t : spec.Domain} {cache : spec.QueryCache} (h : cache t = none) : (OracleSpec.cachingOracle t).run cache = (fun (u : spec.Range t) => (u, cache.cacheQuery t u)) <$> liftM (OracleSpec.query t)

Cache miss: cachingOracle t issues a single underlying query t and stores it.

@[simp]

theorem cachingOracle.probFailure_run_simulateQ {ι₀ : Type} {spec₀ : OracleSpec ι₀} [DecidableEq ι₀] [spec₀.Fintype] [spec₀.Inhabited] {α : Type} (oa : OracleComp spec₀ α) (cache : spec₀.QueryCache) : Pr[⊥ | (simulateQ OracleSpec.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 OracleSpec.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 OracleSpec.cachingOracle (liftM (OracleSpec.query t)) = OracleSpec.cachingOracle t

Forward query bounds for cachingOracle

Forward only — the reverse fails because cache hits strictly reduce the simulated count.

theorem cachingOracle.isTotalQueryBound_run_simulateQ {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} {α : Type} {oa : OracleComp spec₀ α} {n : ℕ} (h : oa.IsTotalQueryBound n) (cache : spec₀.QueryCache) : ((simulateQ OracleSpec.cachingOracle oa).run cache).IsTotalQueryBound n

theorem cachingOracle.isQueryBoundP_run_simulateQ {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} {α : Type} {oa : OracleComp spec₀ α} {p : ι₀ → Prop} [DecidablePred p] {n : ℕ} (h : oa.IsQueryBoundP p n) (cache : spec₀.QueryCache) : ((simulateQ OracleSpec.cachingOracle oa).run cache).IsQueryBoundP p n

theorem cachingOracle.isPerIndexQueryBound_run_simulateQ {ι₀ : Type} [DecidableEq ι₀] {spec₀ : OracleSpec ι₀} {α : Type} {oa : OracleComp spec₀ α} {qb : ι₀ → ℕ} (h : oa.IsPerIndexQueryBound qb) (cache : spec₀.QueryCache) : ((simulateQ OracleSpec.cachingOracle oa).run cache).IsPerIndexQueryBound qb

def OracleSpec.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.

The cache-parametric runtime built on top of this combinator lives in VCVio.CryptoFoundations.FiatShamir.Sigma as FiatShamir.runtimeWithCache cache, with FiatShamir.runtime defined as runtimeWithCache ∅.

@[simp]

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

theorem withCacheOverlay_bind {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α β : Type u} (cache : spec.QueryCache) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : OracleSpec.withCacheOverlay cache (oa >>= ob) = do let p ← (simulateQ OracleSpec.cachingOracle oa).run cache OracleSpec.withCacheOverlay p.2 (ob p.1)

theorem withCacheOverlay_map {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α β : Type u} (cache : spec.QueryCache) (f : α → β) (oa : OracleComp spec α) : OracleSpec.withCacheOverlay cache (f <$> oa) = f <$> OracleSpec.withCacheOverlay cache oa

theorem withCacheOverlay_bind_pure {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} {α β : Type u} (cache : spec.QueryCache) (oa : OracleComp spec α) (f : α → β) : (OracleSpec.withCacheOverlay cache do let x ← oa pure (f x)) = f <$> OracleSpec.withCacheOverlay cache oa

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

theorem withCacheOverlay_query_miss {ι : Type u} [DecidableEq ι] {spec : OracleSpec ι} (cache : spec.QueryCache) (t : spec.Domain) (hv : cache t = none) : OracleSpec.withCacheOverlay cache (liftM (OracleSpec.query t)) = liftM (OracleSpec.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 OracleSpec.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 ((OracleSpec.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.