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)

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.

Equations
    Instances For
      source
      @[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
      source
      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
      source
      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.

      Equations
        Instances For
          source
          @[simp]
          theorem loggingOracle.probFailure_simulateQ {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) :
          Pr[⊥ | (simulateQ loggingOracle oa).run] = Pr[⊥ | oa]
          source
          @[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.

          Equations
            Instances For