Generic Trace Instrumentation for Query Implementations #
Two primitive ways to attach a writer-valued trace to a QueryImpl. Each
comes in two flavours, mirroring Mathlib's two Monad (WriterT ω M) instances:
[Monoid ω]flavour (withTrace/withTraceBefore): the trace lives in an arbitrary monoidωand accumulates via1and*. This is whatQueryImpl.withCost(CountingOracle.lean) uses, withω = QueryCount ι(pointwise additive monoid).[EmptyCollection ω] [Append ω]flavour (withTraceAppend/withTraceAppendBefore): the trace accumulates via∅and++, matching the Append-basedMonad (WriterT ω m)instance. This is whatQueryImpl.withLogging(LoggingOracle.lean) uses, withω = QueryLog spec(a list of query/response pairs).
The two flavours are mathematically the same (a free monoid view vs. an
append-list view), but they correspond to different Monad (WriterT ω m)
instances and Lean's resolver picks whichever one is unambiguously available.
We expose both so neither of QueryCount/QueryLog has to switch its
underlying writer interpretation.
For each flavour, "Before" emits traceFn t before running the handler
(so a handler failure still records the trace), while the bare version emits
traceFn t u after the handler returns response u (so a failure skips
the trace).
Concretely:
withCost = withTraceBefore(the cost ignores the response).withLogging so = withTraceAppend so (fun t u => [⟨t, u⟩])(the log records the response, hence "after" semantics).
The generic lemmas (output marginal, failure probability, NeverFail
equivalence, evalDist / support / probOutput bridges) flow downstream
automatically.
Connection to Control.Trace #
The trace function traceFn : (t : spec.Domain) → spec.Range t → ω is a curried
form of Idx spec.toPFunctor → ω, which is precisely
Control.Trace ω (Idx spec.toPFunctor). The Tracing API is therefore the
oracle-level counterpart of the abstract Control.Trace / PFunctor.Trace
infrastructure in ToMathlib.
withTraceBefore: response-independent trace, recorded before handler #
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, so a failure inside the handler still leaves the trace recorded.
Instances For
A "before"-style trace preserves failure probability for any base monad with
HasEvalSPMF: instrumenting with withTraceBefore does not change the
probability of failure.
When every query traces to the monoid identity 1, withTraceBefore is a
no-op up to pairing with 1.
evalDist / probOutput / support bridges for withTraceBefore #
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
An "after"-style trace preserves failure probability for any base monad with
HasEvalSPMF: instrumenting with withTrace 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.
When every query/response pair traces to the monoid identity 1,
withTrace is a no-op up to pairing with 1.
evalDist / probOutput / support bridges for withTrace #
withTraceAppendBefore: response-independent trace, recorded before #
handler, accumulating via ∅ / ++
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, so a failure inside the handler still leaves the trace recorded.
Instances For
evalDist / probOutput / support bridges for withTraceAppendBefore #
withTraceAppend: response-dependent trace, recorded after handler, #
accumulating via ∅ / ++
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).