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] [HasEvalSPMF m] (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 HasEvalSPMF, 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] [HasEvalSPMF m] (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.

@[simp]

theorem QueryImpl.appendInputLog_apply {κ : Type} {loggedSpec : OracleSpec κ} {m₀ : Type → Type v} [Monad m₀] (so : QueryImpl loggedSpec m₀) (t : loggedSpec.Domain) : so.appendInputLog t = do let inputs ← get let u ← liftM (so t) set (inputs ++ [t]) pure u

@[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.Fintype] [spec.Inhabited] (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.Fintype] [spec.Inhabited] (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.Fintype] [spec.Inhabited] (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.Fintype] [spec.Inhabited] (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

Bidirectional query-bound transfer for loggingOracle / withLogging

The writer log overlay leaves the underlying query structure untouched, so all three query-bound flavors transfer biconditionally via fst_map_run_simulateQ / QueryImpl.fst_map_run_withLogging and isXQueryBound_iff_of_map_eq.

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 ι} {α : 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 ι'} (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 ι} {α : 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 ι'} (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.Fintype] [spec.Inhabited] {α : 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.