Documentation

VCVio.OracleComp.QueryTracking.Tracing.Core

Trace instrumentation #

Writer-valued instrumentation records query-dependent observations before a handler runs, or response-dependent observations after a response returns. Projection recovers the original computation for any lawful base monad.

withTraceBefore: response-independent trace, recorded before handler #

@[reducible, inline]
abbrev QueryImpl.withTraceBefore {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) :
QueryImpl spec (WriterT ω m)

Wrap an oracle implementation so that each query records traceFn t in the writer ω before running the handler. The trace value depends only on the query. Failure in the base monad can discard the entire writer result.

Instances For
    theorem QueryImpl.withTraceBefore_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (t : spec.Domain) :
    so.withTraceBefore traceFn t = do tell (traceFn t) liftM (so t)
    theorem QueryImpl.fst_map_run_withTraceBefore {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (mx : OracleComp spec α) :
    @[simp]
    theorem QueryImpl.run_simulateQ_withTraceBefore_const_one {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] (so : QueryImpl spec m) (mx : OracleComp spec α) :
    (simulateQ (so.withTraceBefore fun (x : spec.Domain) => 1) mx).run = (fun (x : α) => (x, 1)) <$> simulateQ so mx

    When every query traces to the monoid identity 1, withTraceBefore is a no-op up to pairing with 1.

    theorem QueryImpl.support_fst_run_withTraceBefore {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] [MonadAttach m] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (mx : OracleComp spec α) :

    withTrace: response-dependent trace, recorded after handler #

    @[reducible, inline]
    abbrev QueryImpl.withTrace {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) :
    QueryImpl spec (WriterT ω m)

    Wrap an oracle implementation so that each query records traceFn t u in the writer ω after the handler returns response u. A handler failure skips the trace (the response never materialised).

    Instances For
      theorem QueryImpl.withTrace_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (t : spec.Domain) :
      so.withTrace traceFn t = do let u ← liftM (so t) tell (traceFn t u) pure u
      theorem QueryImpl.fst_map_run_withTrace {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (mx : OracleComp spec α) :
      Prod.fst <$> (simulateQ (so.withTrace traceFn) mx).run = simulateQ so mx
      @[simp]
      theorem QueryImpl.run_simulateQ_withTrace_const_one {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] (so : QueryImpl spec m) (mx : OracleComp spec α) :
      (simulateQ (so.withTrace fun (x : spec.Domain) (x_1 : spec.Range x) => 1) mx).run = (fun (x : α) => (x, 1)) <$> simulateQ so mx

      When every query/response pair traces to the monoid identity 1, withTrace is a no-op up to pairing with 1.

      theorem QueryImpl.support_fst_run_withTrace {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] [LawfulMonad m] [MonadAttach m] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (mx : OracleComp spec α) :

      withTraceAppendBefore: response-independent trace, recorded before #

      handler, accumulating via ∅ / ++

      @[reducible, inline]
      abbrev QueryImpl.withTraceAppendBefore {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) :
      QueryImpl spec (WriterT ω m)

      Append-flavoured analogue of withTraceBefore: each query records traceFn t in the writer ω before running the handler, and WriterT uses the [EmptyCollection ω] [Append ω] Monad instance (tell is a single push, bind concatenates with ++). The trace value depends only on the query. Failure in the base monad can discard the entire writer result.

      Instances For
        theorem QueryImpl.withTraceAppendBefore_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (t : spec.Domain) :
        so.withTraceAppendBefore traceFn t = do tell (traceFn t) liftM (so t)
        theorem QueryImpl.fst_map_run_withTraceAppendBefore {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] [LawfulAppend ω] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (mx : OracleComp spec α) :
        theorem QueryImpl.support_fst_run_withTraceAppendBefore {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] [LawfulAppend ω] [MonadAttach m] (so : QueryImpl spec m) (traceFn : spec.Domain → ω) (mx : OracleComp spec α) :

        withTraceAppend: response-dependent trace, recorded after handler, #

        accumulating via ∅ / ++

        @[reducible, inline]
        abbrev QueryImpl.withTraceAppend {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) :
        QueryImpl spec (WriterT ω m)

        Append-flavoured analogue of withTrace: each query records traceFn t u in the writer ω after the handler returns response u, using the [EmptyCollection ω] [Append ω] Monad (WriterT ω m) instance. A handler failure skips the trace (the response never materialised).

        Instances For
          theorem QueryImpl.withTraceAppend_apply {ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (t : spec.Domain) :
          so.withTraceAppend traceFn t = do let u ← liftM (so t) tell (traceFn t u) pure u
          theorem QueryImpl.fst_map_run_withTraceAppend {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] [LawfulAppend ω] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (mx : OracleComp spec α) :
          theorem QueryImpl.support_fst_run_withTraceAppend {ι : Type u} {spec : OracleSpec ι} {α : Type u} {m : Type u → Type v} [Monad m] {ω : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] [LawfulAppend ω] [MonadAttach m] (so : QueryImpl spec m) (traceFn : (t : spec.Domain) → spec.Range t → ω) (mx : OracleComp spec α) :