Simulation through WriterT Handlers

Combinators and output-preservation lemmas for writer-instrumented query implementations. The combinators here mirror the StateT/ReaderT versions in SimSemantics/StateT/Basic.lean and SimSemantics/ReaderT/Basic.lean.

def QueryImpl.parallelWriterT {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type (max u_3 u_4) → Type u_5} [Functor m] {ω₁ ω₂ : Type (max u_3 u_4)} [Monoid ω₁] [Monoid ω₂] (impl₁ : QueryImpl spec₁ (WriterT ω₁ m)) (impl₂ : QueryImpl spec₂ (WriterT ω₂ m)) : QueryImpl (spec₁ + spec₂) (WriterT (ω₁ × ω₂) m)

Given implementations for oracles in spec₁ and spec₂ in terms of writer monads for two different log monoids ω₁ and ω₂, implement the combined set spec₁ + spec₂ in terms of the product monoid ω₁ × ω₂. Each side leaves the other component at the identity.

def QueryImpl.sigmaWriterT {τ : Type} [DecidableEq τ] {ι : τ → Type u_1} {spec : (t : τ) → OracleSpec (ι t)} {m : Type (max u_2 u_3) → Type u_4} [Functor m] {ω : τ → Type (max u_2 u_3)} [(t : τ) → Monoid (ω t)] (impl : (t : τ) → QueryImpl (spec t) (WriterT (ω t) m)) : QueryImpl (OracleSpec.sigma spec) (WriterT ((t : τ) → ω t) m)

Indexed version of QueryImpl.parallelWriterT. Each query for index t writes into the t-th component of the pi-product (t : τ) → ω t, leaving every other component at the identity. Note that m cannot vary with t.

def QueryImpl.flattenWriterT {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] {ω₁ ω₂ : Type u} [Monoid ω₂] (impl : QueryImpl spec (WriterT ω₁ (WriterT ω₂ m))) : QueryImpl spec (WriterT (ω₁ × ω₂) m)

Reassociate a nested writer transformer into one product log.

The outer log is the first component of the product; the inner/base log is the second. This is the writer-transformer analogue of flattenStateT. Requires [Monoid ω₂] to lift the inner writer's run; the resulting WriterT (ω₁ × ω₂) m carries both logs as a product.

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 α) : Prod.fst <$> (simulateQ so oa).run = oa

Taking the first component of the WriterT output recovers the original computation, when the query implementation preserves the underlying oracle behavior (hso).

theorem OracleComp.probFailure_writerT_run_simulateQ {ι : Type u} {spec : OracleSpec ι} {α ω : Type u} [Monoid ω] [spec.IsUniformSpec] {so : QueryImpl spec (WriterT ω (OracleComp spec))} (oa : OracleComp spec α) : Pr[⊥ | (simulateQ so oa).run] = Pr[⊥ | oa]

theorem OracleComp.NeverFail_writerT_run_simulateQ_iff {ι : Type u} {spec : OracleSpec ι} {α ω : Type u} [Monoid ω] [spec.IsUniformSpec] {so : QueryImpl spec (WriterT ω (OracleComp spec))} (oa : OracleComp spec α) : NeverFail (simulateQ so oa).run ↔ NeverFail oa