Combined Caching + Logging Handlers

This file packages the concrete "cache plus append-log" handlers that are useful in proof developments but should live below ProgramLogic.

QueryImpl.withCachingTraceAppend is the generic transformer: it threads a QueryCache spec × ω state, reuses cached answers on hits, falls back to the underlying implementation on misses, and appends a response-dependent trace to the second state component after every query.

QueryImpl.withCachingLogging and OracleSpec.cachingLoggingOracle are the canonical specializations to QueryLog spec.

def QueryImpl.withCachingTraceAppend {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [DecidableEq ι] {ω : Type u} [Append ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) : QueryImpl spec (StateT (spec.QueryCache × ω) m)

Cache responses in the first state component and append a response-dependent trace to the second state component after every query.

On a cache hit, the underlying handler is not consulted; the cached answer is returned directly and the trace still records the observed (query, response) pair. On a cache miss, the underlying handler supplies the answer, which is then installed in the cache before the trace is appended.

@[simp]

theorem QueryImpl.withCachingTraceAppend_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [DecidableEq ι] {ω : Type u} [Append ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (t : spec.Domain) : so.withCachingTraceAppend traceFn t = StateT.mk fun (s : spec.QueryCache × ω) => match s.1 t with | some u => pure (u, s.1, s.2 ++ traceFn t u) | none => (fun (p : spec.Range t × ω) => (p.1, s.1.cacheQuery t p.1, p.2)) <$> (fun (u : spec.Range t) => (u, s.2 ++ traceFn t u)) <$> so t

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

Specialization of withCachingTraceAppend to the canonical query log QueryLog spec.

@[simp]

theorem QueryImpl.withCachingLogging_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [DecidableEq ι] (so : QueryImpl spec m) (t : spec.Domain) : so.withCachingLogging t = StateT.mk fun (s : spec.QueryCache × spec.QueryLog) => match s.1 t with | some u => pure (u, s.1, s.2 ++ [⟨t, u⟩]) | none => (fun (p : spec.Range t × spec.QueryLog) => (p.1, s.1.cacheQuery t p.1, p.2)) <$> (fun (u : spec.Range t) => (u, s.2 ++ [⟨t, u⟩])) <$> so t

Forward-direction query bounds for withCachingTraceAppend

The trace overlay does not change the underlying query count, so the withCaching bounds transfer through withCachingAux_run_proj_eq via isQueryBound_iff_of_map_eq.

theorem QueryImpl.isTotalQueryBound_run_simulateQ_withCachingTraceAppend {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {ω : Type u} [EmptyCollection ω] [Append ω] {α : Type u} [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec)) (traceFn : (t : spec.Domain) → spec.Range t → ω) {oa : OracleComp spec α} {n : ℕ} (h : oa.IsTotalQueryBound n) (hstep : ∀ (t : spec.Domain), (so t).IsTotalQueryBound 1) (s : spec.QueryCache × ω) : ((simulateQ (so.withCachingTraceAppend traceFn) oa).run s).IsTotalQueryBound n

theorem QueryImpl.isQueryBoundP_run_simulateQ_withCachingTraceAppend {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {ω : Type u} [EmptyCollection ω] [Append ω] {α ι' : Type u} {spec' : OracleSpec ι'} [LawfulAppend ω] (so : QueryImpl spec (OracleComp spec')) (traceFn : (t : spec.Domain) → spec.Range t → ω) {oa : OracleComp spec α} {p : ι → Prop} [DecidablePred p] {q : ι' → Prop} [DecidablePred q] {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) (s : spec.QueryCache × ω) : ((simulateQ (so.withCachingTraceAppend traceFn) oa).run s).IsQueryBoundP q n

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

Canonical combined caching + logging oracle over OracleComp spec.

@[simp]

theorem cachingLoggingOracle.apply_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [spec.DecidableEq] (t : spec.Domain) : OracleSpec.cachingLoggingOracle t = do let __discr ← get match __discr with | (cache, trace) => match cache t with | some u => modifyGet fun (x : spec.QueryCache × spec.QueryLog) => (u, cache, trace ++ [⟨t, u⟩]) | none => do let u ← liftM (query t) modifyGet fun (x : spec.QueryCache × spec.QueryLog) => (u, cache.cacheQuery t u, trace ++ [⟨t, u⟩])

theorem cachingLoggingOracle.fst_map_run_simulateQ {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [spec.DecidableEq] {α : Type u} (oa : OracleComp spec α) (s : spec.QueryCache × spec.QueryLog) : Prod.map id Prod.fst <$> (simulateQ OracleSpec.cachingLoggingOracle oa).run s = (simulateQ OracleSpec.cachingOracle oa).run s.1

Projecting away the log component recovers the ordinary caching semantics.

@[simp]

theorem cachingLoggingOracle.run'_simulateQ_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] [spec.DecidableEq] {α : Type u} (oa : OracleComp spec α) (s : spec.QueryCache × spec.QueryLog) : (simulateQ OracleSpec.cachingLoggingOracle oa).run' s = (simulateQ OracleSpec.cachingOracle oa).run' s.1

Output-only projection corollary of fst_map_run_simulateQ.

Forward-direction query bounds

The log overlay does not change the underlying query count, so the cachingOracle bounds transfer through fst_map_run_simulateQ via isQueryBound_iff_of_map_eq.

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

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

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