Documentation

VCVio.OracleComp.QueryTracking.LoggingOracle

Logging Queries Made by a Computation #

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

Add logging to an existing query implementation, using StateT to extend the final monad.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem QueryImpl.withLogging_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {α : Type u} (so : QueryImpl spec m) (q : spec.OracleQuery α) :
    so.withLogging.impl q = do let x ← liftM (so.impl q) tell (OracleSpec.QueryLog.singleton q x) pure x
    source
    def loggingOracle {ι : Type u} {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.

    Equations
    Instances For
      source
      @[simp]
      theorem loggingOracle.apply_eq {ι : Type u} {spec : OracleSpec ι} {α : Type u} (q : spec.OracleQuery α) :
      loggingOracle.impl q = do let u ← liftM q tell (OracleSpec.QueryLog.singleton q u) pure u
      source
      @[simp]
      theorem loggingOracle.fst_map_run_simulateQ {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      Prod.fst <$> (OracleComp.simulateQ loggingOracle oa).run = oa

      Taking only the main output after logging queries is the original compuation.

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

      Throwing away the query log after simulation looks like running the original computation.

      source
      @[simp]
      theorem loggingOracle.probFailure_run_simulateQ {ι : Type u} {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] (oa : OracleComp spec α) :
      [⊥|(OracleComp.simulateQ loggingOracle oa).run] = [⊥|oa]
      source
      @[simp]
      theorem loggingOracle.neverFails_run_simulateQ_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      (OracleComp.simulateQ loggingOracle oa).run.neverFails ↔ oa.neverFails
      source
      theorem loggingOracle.neverFails_simulateQ {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) :
      oa.neverFails → (OracleComp.simulateQ loggingOracle oa).run.neverFails

      Alias of the reverse direction of loggingOracle.neverFails_run_simulateQ_iff.