Logging Queries Made by a Computation

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 logging all the queries to the writer monad before forwarding the response.

@[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 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 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 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 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 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 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 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 loggingOracle (liftM (query t) >>= mx)).run = do let u ← liftM (query t) (fun (p : α × spec.QueryLog) => (p.1, ⟨t, u⟩ :: p.2)) <$> (simulateQ loggingOracle (mx u)).run

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

loggingOracle preserves IsTotalQueryBound: the query structure of (simulateQ loggingOracle oa).run is identical to that of oa (each query passes through unchanged, with only the writer log being appended).

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