Basic Constructions of Simulation Oracles #
This file defines a number of basic simulation oracles, as well as operations to combine them.
preInsert and postInsert #
The two main building blocks for instrumented QueryImpl values are preInsert and
postInsert. Both take a base QueryImpl spec m and a per-query side effect, and produce
a new QueryImpl spec n that wraps the base with that side effect:
preInsert so nxrunsnx tbefore the handlerso t. The side effect happens unconditionally, including when the handler later fails.postInsert so nxrunsnx t uafter the handler returns responseu, so the side effect can depend on the response and is skipped when the handler fails.
Both come with a complete generic theory, parametric in a projection
proj : ∀ {γ}, n γ → m γ that strips the instrumentation: proj_simulateQ_preInsert,
probFailure_proj_simulateQ_preInsert, NeverFail_proj_simulateQ_preInsert_iff,
evalDist_proj_simulateQ_preInsert, probOutput_proj_simulateQ_preInsert,
support_proj_simulateQ_preInsert, finSupport_proj_simulateQ_preInsert, and the
induction principle simulateQ_preInsert.induct (with postInsert analogues). Query-bound
transfer through these wrappers lives in QueryTracking/QueryBound.lean.
Most of the wrappers in QueryTracking/ (withTraceBefore, withTrace,
withTraceAppendBefore, withTraceAppend, withCost, withCounting, withAddCost,
withUnitCost, withLogging, appendInputLog) bottom out at these combinators. New
instrumentation should follow the same pattern when its shape is "for each query, run a
side effect and delegate" — wrappers whose control flow is conditional on external state
or the would-be response (cache-on-hit, seed fallback, budget gating) genuinely need a
custom QueryImpl and stay outside this hierarchy.
Given an implementation of spec in terms of a new set of oracles spec',
and an implementation of spec' in terms of arbitrary m, implement spec in terms of m.
Instances For
Given monads m and n with MonadLiftT m n, an implementation of spec in m,
and a computation nx in n for each query input, construct a new implementation
QueryImpl.preInsert so nx that calls nx on every query before the actual substitution so.
Note that nx is expected to have some side-effects, it's actual result is discarded.
Instances For
One-step characterisation of simulateQ (preInsert so nx) on a single query.
Induction principle for proj (simulateQ (so.preInsert nx) oa) parametric in a
motive OracleComp spec β → m β → Prop. The recursion structure of
proj_simulateQ_preInsert is exposed as two cases mirroring OracleComp.inductionOn:
in pure x the projected term reduces to pure x, and in query t >>= k it reduces
to so t >>= k' for some continuation k' u = proj (simulateQ (so.preInsert nx) (k u)).
Tagged @[elab_as_elim] so it is usable as induction oa using simulateQ_preInsert.induct.
Generic strip lemma: given a monad-morphism-style projection proj : ∀ {γ}, n γ → m γ
that preserves pure and bind and discards the inserted side effect on each query,
simulating with preInsert so nx and projecting back recovers simulateQ so. The proof
is the canonical use of simulateQ_preInsert.induct: the parametric motive is instantiated
to the equality with simulateQ so oa, leaving trivial cases.
A preInsert instrumentation preserves failure probability for any base monad with
[MonadLiftT m SPMF], given the projection bundle and its compatibility with failure
probabilities.
NeverFail biconditional companion of probFailure_proj_simulateQ_preInsert.
When nx is constantly pure x, preInsert so nx is the lift of so and the
resulting simulation equals the lifted underlying simulation. Generic analogue of the
run_simulateQ_withTraceBefore_const_one no-op identity.
evalDist / probOutput / support bridges for preInsert #
Given monads m and n with MonadLiftT m n, an implementation of spec in m,
and a computation nx in n for each query output, construct a new implementation
QueryImpl.postInsert so nx that calls nx on on the result of each substitution.
Note that nx is expected to have some side-effects, it's actual result is discarded.
Instances For
One-step characterisation of simulateQ (postInsert so nx) on a single query.
Induction principle for proj (simulateQ (so.postInsert nx) oa) parametric in a
motive OracleComp spec β → m β → Prop. The recursion structure of
proj_simulateQ_postInsert is exposed as two cases mirroring OracleComp.inductionOn:
in pure x the projected term reduces to pure x, and in query t >>= k it reduces
to so t >>= k' for some continuation k' u = proj (simulateQ (so.postInsert nx) (k u)).
Tagged @[elab_as_elim] so it is usable as induction oa using simulateQ_postInsert.induct.
Generic strip lemma: given a monad-morphism-style projection proj : ∀ {γ}, n γ → m γ
that preserves pure and bind and discards the inserted side effect on each query,
simulating with postInsert so nx and projecting back recovers simulateQ so. The proof
is the canonical use of simulateQ_postInsert.induct: the parametric motive is instantiated
to the equality with simulateQ so oa, leaving trivial cases.
A postInsert instrumentation preserves failure probability for any base monad with
[MonadLiftT m SPMF], given the projection bundle and its compatibility with failure
probabilities.
NeverFail biconditional companion of probFailure_proj_simulateQ_postInsert.
When nx is constantly pure x, postInsert so nx is the lift of so and the
resulting simulation equals the lifted underlying simulation. Generic analogue of the
run_simulateQ_withTrace_const_one no-op identity.