Logging Queries Made by a Computation

QueryImpl.withLogging records every query/response pair ⟨t, u⟩ to a WriterT (QueryLog spec) writer layer. It is a response-dependent trace, defined as a specialisation of QueryImpl.withTraceAppend (see Tracing.lean): the log is appended after the underlying handler returns, so a handler failure leaves no log entry for the failed query.

We use the Append-flavoured withTraceAppend (rather than the Monoid flavoured withTrace) because QueryLog spec = List _ only carries an [EmptyCollection, Append, LawfulAppend] structure, not a Monoid. This matches the pre-existing Monad (WriterT (QueryLog spec) m) instance the rest of WriterTBridge / mvcgen infrastructure already targets.

noncomputable def QueryImpl.writerTMapBase {ι₀ ι₁ : Type u} {spec₀ : OracleSpec ι₀} {spec₁ : OracleSpec ι₁} {m₁ : Type u → Type v} [Monad m₁] {ω : Type u} (outer : QueryImpl spec₁ m₁) (inner : QueryImpl spec₀ (WriterT ω (OracleComp spec₁))) : QueryImpl spec₀ (WriterT ω m₁)

Push an outer oracle interpretation through the base monad of a WriterT-valued query implementation.

theorem QueryImpl.simulateQ_writerTMapBase_run {ι₀ ι₁ : Type u} {spec₀ : OracleSpec ι₀} {spec₁ : OracleSpec ι₁} {m₁ : Type u → Type v} [Monad m₁] {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m₁] [LawfulAppend ω] (outer : QueryImpl spec₁ m₁) (inner : QueryImpl spec₀ (WriterT ω (OracleComp spec₁))) {α : Type u} (oa : OracleComp spec₀ α) : simulateQ outer (simulateQ inner oa).run = (simulateQ (outer.writerTMapBase inner) oa).run

Running a WriterT handler and then interpreting its base oracle computations is the same as first mapping the handler's base through the outer interpreter.

def QueryImpl.withLogging {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) : QueryImpl spec (WriterT spec.QueryLog m)

Given that so implements the oracles in spec using the monad m, withLogging so gives the same implementation in the extension WriterT (QueryLog spec) m, by appending a single-entry log [⟨t, u⟩] after the handler returns response u.

This is the response-dependent specialisation of QueryImpl.withTraceAppend with the trace function fun t u => [⟨t, u⟩] (a single-element list, the free-monoid generator of QueryLog spec = List ((t : spec.Domain) × spec.Range t)).

theorem QueryImpl.withLogging_eq_withTraceAppend {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) : so.withLogging = so.withTraceAppend fun (t : spec.Domain) (u : spec.Range t) => [⟨t, u⟩]

@[simp]

theorem QueryImpl.withLogging_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] (so : QueryImpl spec m) (t : spec.Domain) : so.withLogging t = do let u ← liftM (so t) tell [⟨t, u⟩] pure u

theorem QueryImpl.fst_map_run_withLogging {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec m) (mx : OracleComp spec α) : Prod.fst <$> (simulateQ so.withLogging mx).run = simulateQ so mx

theorem QueryImpl.probFailure_run_simulateQ_withLogging {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (so : QueryImpl spec m) (mx : OracleComp spec α) : Pr[⊥ | (simulateQ so.withLogging mx).run] = Pr[⊥ | simulateQ so mx]

Logging preserves failure probability: for any base monad m with MonadLiftT m SPMF, wrapping an oracle implementation with withLogging does not change the probability of failure. When m = OracleComp spec, both sides are 0 (trivially true). When m can genuinely fail (e.g. OptionT (OracleComp spec)), this is a non-trivial faithfulness property.

theorem QueryImpl.NeverFail_run_simulateQ_withLogging_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (so : QueryImpl spec m) (mx : OracleComp spec α) : NeverFail (simulateQ so.withLogging mx).run ↔ NeverFail (simulateQ so mx)

def QueryImpl.appendInputLog {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] (so : QueryImpl loggedSpec m₀) : QueryImpl loggedSpec (StateT (List loggedSpec.Domain) m₀)

Run an implementation and append each queried input to a StateT list.

This is the state-transformer analogue of withLogging when only the query inputs are needed: responses are returned exactly as in the base implementation, while the state records the input sequence in order.

Defined as the response-independent preInsert instrumentation that appends the queried input t to the state list before delegating to so.

theorem QueryImpl.appendInputLog_eq_preInsert {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] (so : QueryImpl loggedSpec m₀) : so.appendInputLog = so.preInsert fun (t : loggedSpec.Domain) => modify fun (x : List loggedSpec.Domain) => x ++ [t]

@[simp]

theorem QueryImpl.appendInputLog_apply {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] [LawfulMonad m₀] (so : QueryImpl loggedSpec m₀) (t : loggedSpec.Domain) : so.appendInputLog t = do modify fun (x : List loggedSpec.Domain) => x ++ [t] liftM (so t)

@[simp]

theorem QueryImpl.run_withLogging_apply {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] [LawfulMonad m₀] (so : QueryImpl loggedSpec m₀) (t : loggedSpec.Domain) : (so.withLogging t).run = do let u ← so t pure (u, [⟨t, u⟩])

theorem QueryImpl.run_appendInputLog_apply {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] [LawfulMonad m₀] (so : QueryImpl loggedSpec m₀) (t : loggedSpec.Domain) (inputs : List loggedSpec.Domain) : (so.appendInputLog t).run inputs = do let u ← so t pure (u, inputs ++ [t])

theorem QueryImpl.map_run_withLogging_inputs_eq_run_appendInputLog {ι₀ : Type} {spec₀ : OracleSpec ι₀} {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] [LawfulMonad m₀] [HasQuery spec₀ m₀] {α' : Type} (so : QueryImpl loggedSpec m₀) (oa : OracleComp (spec₀ + loggedSpec) α') (initialInputs : List loggedSpec.Domain) : have baseW := liftTarget (WriterT loggedSpec.QueryLog m₀) HasQuery.toQueryImpl; have implW := baseW + so.withLogging; have baseS := liftTarget (StateT (List loggedSpec.Domain) m₀) HasQuery.toQueryImpl; have implAppend := baseS + so.appendInputLog; (fun (z : α' × loggedSpec.QueryLog) => (z.1, initialInputs ++ List.map (fun (e : (t : loggedSpec.Domain) × loggedSpec.Range t) => e.fst) z.2)) <$> (simulateQ implW oa).run = (simulateQ implAppend oa).run initialInputs

A WriterT query log can be replayed as a StateT input log.

For computations over a sum spec + loggedSpec, this theorem compares two implementations:

• left queries in spec are forwarded unchanged;
• right queries in loggedSpec are either handled with withLogging, producing a QueryLog loggedSpec, or with appendInputLog, appending just the queried inputs to a state list.

Mapping the WriterT result to (output, initialInputs ++ loggedInputs) yields exactly the same base-monad computation as running the StateT implementation from initialInputs.

def OracleSpec.loggingOracle {ι : Type (max u_1 u_2)} {spec : OracleSpec ι} : QueryImpl spec (WriterT spec.QueryLog (OracleComp spec))

Simulation oracle for tracking the quries in a QueryLog, without modifying the actual behavior of the oracle. Requires decidable equality of the indexing set to determine which list to update when queries come in.

@[simp]

theorem loggingOracle.probFailure_simulateQ {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.IsUniformSpec] (oa : OracleComp spec α) : Pr[⊥ | (simulateQ OracleSpec.loggingOracle oa).run] = Pr[⊥ | oa]

Specialization of QueryImpl.probFailure_run_simulateQ_withLogging to loggingOracle.

@[simp]

theorem loggingOracle.fst_map_run_simulateQ {ι : Type} {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) : Prod.fst <$> (simulateQ OracleSpec.loggingOracle oa).run = oa

@[simp]

theorem loggingOracle.run_simulateQ_bind_fst {ι : Type} {spec : OracleSpec ι} {α β : Type} (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (do let x ← (simulateQ OracleSpec.loggingOracle oa).run ob x.1) = oa >>= ob

@[simp]

theorem loggingOracle.NeverFail_run_simulateQ_iff {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.IsUniformSpec] (oa : OracleComp spec α) : NeverFail (simulateQ OracleSpec.loggingOracle oa).run ↔ NeverFail oa

Specialization of QueryImpl.NeverFail_run_simulateQ_withLogging_iff to loggingOracle.

@[simp]

theorem loggingOracle.probEvent_fst_run_simulateQ {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.IsUniformSpec] (oa : OracleComp spec α) (p : α → Prop) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => p z.1) = probEvent oa p

@[simp]

theorem loggingOracle.probOutput_fst_map_run_simulateQ {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : Pr[= x | Prod.fst <$> (simulateQ OracleSpec.loggingOracle oa).run] = Pr[= x | oa]

theorem OracleComp.run_simulateQ_loggingOracle_query_bind {ι : Type} {spec : OracleSpec ι} {α : Type} (t : spec.Domain) (mx : spec.Range t → OracleComp spec α) : (simulateQ OracleSpec.loggingOracle (liftM (OracleSpec.query t) >>= mx)).run = do let u ← liftM (OracleSpec.query t) (fun (p : α × spec.QueryLog) => (p.1, ⟨t, u⟩ :: p.2)) <$> (simulateQ OracleSpec.loggingOracle (mx u)).run

theorem OracleComp.isTotalQueryBound_run_simulateQ_loggingOracle_iff {ι : Type} {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (n : ℕ) : (simulateQ OracleSpec.loggingOracle oa).run.IsTotalQueryBound n ↔ oa.IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_loggingOracle_iff {ι : Type} {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} (oa : OracleComp spec α) (p : ι → Prop) [DecidablePred p] (n : ℕ) : (simulateQ OracleSpec.loggingOracle oa).run.IsQueryBoundP p n ↔ oa.IsQueryBoundP p n

theorem OracleComp.isTotalQueryBound_run_simulateQ_withLogging_iff {ι : Type} {spec : OracleSpec ι} {ι' : Type} {spec' : OracleSpec ι'} (so : QueryImpl spec (OracleComp spec')) {α : Type} (mx : OracleComp spec α) (n : ℕ) : (simulateQ so.withLogging mx).run.IsTotalQueryBound n ↔ (simulateQ so mx).IsTotalQueryBound n

theorem OracleComp.isQueryBoundP_run_simulateQ_withLogging_iff {ι : Type} {spec : OracleSpec ι} {ι' : Type} {spec' : OracleSpec ι'} [spec'.IsUniformSpec] (so : QueryImpl spec (OracleComp spec')) {α : Type} (mx : OracleComp spec α) (q : ι' → Prop) [DecidablePred q] (n : ℕ) : (simulateQ so.withLogging mx).run.IsQueryBoundP q n ↔ (simulateQ so mx).IsQueryBoundP q n

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_loggingOracle_iff {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} (oa : OracleComp spec α) (qb : ι → ℕ) : (simulateQ OracleSpec.loggingOracle oa).run.IsPerIndexQueryBound qb ↔ oa.IsPerIndexQueryBound qb

theorem OracleComp.isPerIndexQueryBound_run_simulateQ_withLogging_iff {ι : Type} {spec : OracleSpec ι} {ι' : Type} [DecidableEq ι'] {spec' : OracleSpec ι'} [spec'.IsUniformSpec] (so : QueryImpl spec (OracleComp spec')) {α : Type} (mx : OracleComp spec α) (qb : ι' → ℕ) : (simulateQ so.withLogging mx).run.IsPerIndexQueryBound qb ↔ (simulateQ so mx).IsPerIndexQueryBound qb

theorem OracleComp.log_length_le_of_mem_support_run_simulateQ {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] [spec.IsUniformSpec] {α : Type} {oa : OracleComp spec α} {n : ℕ} (hbound : oa.IsTotalQueryBound n) {z : α × spec.QueryLog} (hz : z ∈ support (simulateQ OracleSpec.loggingOracle oa).run) : List.length z.2 ≤ n

A total query bound controls the length of every loggingOracle trace in support: if oa makes at most n queries, then every support point of (simulateQ loggingOracle oa).run has log length at most n.

@[reducible]

def OracleComp.withQueryLog {ι : Type u_1} {spec : OracleSpec ι} {α : Type u_1} (mx : OracleComp spec α) : OracleComp spec (α × spec.QueryLog)

Add a query log to a computation using a logging oracle.

theorem OracleComp.withQueryLog_bind {ι : Type} {spec : OracleSpec ι} {α β : Type} (mx : OracleComp spec α) (my : α → OracleComp spec β) : (mx >>= my).withQueryLog = do let p ← mx.withQueryLog (Prod.map id fun (x : spec.QueryLog) => p.2 ++ x) <$> (my p.1).withQueryLog

withQueryLog distributes over bind: the combined log is the concatenation of the prefix's log and the continuation's log.

@[simp]

theorem OracleComp.withQueryLog_pure {ι : Type} {spec : OracleSpec ι} {α : Type} (x : α) : (pure x).withQueryLog = pure (x, [])

withQueryLog of pure x produces (x, []) — no oracle queries, empty log.

theorem OracleComp.withQueryLog_query {ι : Type} {spec : OracleSpec ι} (t : spec.Domain) : (liftM (OracleSpec.query t)).withQueryLog = do let u ← liftM (OracleSpec.query t) pure (u, [⟨t, u⟩])

withQueryLog of a single query t produces (u, [⟨t, u⟩]) where u is the oracle response: one query, one log entry.

@[simp]

theorem OracleComp.probEvent_withQueryLog {ι : Type} {oSpec : OracleSpec ι} [oSpec.IsUniformSpec] {α : Type} (oa : OracleComp oSpec α) (p : α → Prop) : probEvent oa.withQueryLog (p ∘ Prod.fst) = probEvent oa p

For any computation oa and predicate p, the probability of p holding on the output equals the probability of p ∘ Prod.fst holding on the output of oa.withQueryLog.

theorem OracleComp.withQueryLog_self_log_eq {ι : Type} {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) {v : α} {l₁ l₂ : spec.QueryLog} (hmem : ((v, l₁), l₂) ∈ support oa.withQueryLog.withQueryLog) : l₁ = l₂

Self-log fixed point. The two log layers produced by oa.withQueryLog.withQueryLog agree on every support point: simulating the logging oracle over oa.withQueryLog records exactly the queries that the inner withQueryLog already recorded, since withQueryLog does not add new queries to the underlying OracleComp.