Simulation through WriterT Handlers #
Output-preservation lemmas for writer-instrumented query implementations.
theorem
QueryImpl.simulateQ_writerT_fst_map_run_eq_of_query
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
{ω : Type u}
[Monoid ω]
(implW : QueryImpl spec (WriterT ω m))
(impl : QueryImpl spec m)
(himpl : ∀ (t : spec.Domain), Prod.fst <$> (implW t).run = impl t)
(oa : OracleComp spec α)
:
A WriterT-valued handler preserves the output marginal of a whole
simulation as soon as it preserves the output marginal of each query.
This is the generic output-preservation principle for writer-style handler instrumentation. Specializations such as trace, cost, and counting handlers only need to prove the one-query hypothesis.
theorem
QueryImpl.simulateQ_writerT_append_fst_map_run_eq_of_query
{ι : Type u}
{spec : OracleSpec ι}
{α : Type u}
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
{ω : Type u}
[EmptyCollection ω]
[Append ω]
[LawfulAppend ω]
(implW : QueryImpl spec (WriterT ω m))
(impl : QueryImpl spec m)
(himpl : ∀ (t : spec.Domain), Prod.fst <$> (implW t).run = impl t)
(oa : OracleComp spec α)
:
Append-flavoured version of
QueryImpl.simulateQ_writerT_fst_map_run_eq_of_query.
This targets the WriterT instance that accumulates logs via ∅ and ++,
used by query logging.
theorem
OracleComp.fst_map_writerT_run_simulateQ
{ι : Type u}
{spec : OracleSpec ι}
{α ω : Type u}
[Monoid ω]
{so : QueryImpl spec (WriterT ω (OracleComp spec))}
(hso : ∀ (t : spec.Domain), Prod.fst <$> (so t).run = liftM (OracleSpec.query t))
(oa : OracleComp spec α)
:
Taking the first component of the WriterT output recovers the original computation, when the query implementation preserves the underlying oracle behavior (hso).
theorem
OracleComp.NeverFail_writerT_run_simulateQ_iff
{ι : Type u}
{spec : OracleSpec ι}
{α ω : Type u}
[Monoid ω]
[spec.Fintype]
[spec.Inhabited]
{so : QueryImpl spec (WriterT ω (OracleComp spec))}
(oa : OracleComp spec α)
: