Research proof index

run' projection corollary of withProgramming_empty_run_proj_eq.

Generic simulation triple: if every handler call handler t preserves an invariant I on the simulation state, then simulateQ handler oa preserves I for any oa : OracleComp spec α. The invariant-only form (same I as pre- and post-condition, independent of return value) is the most common case; stronger per-call specs can be derived by instantiat...

Support characterization of Std.Do.Triple on WriterT ω (OracleComp spec). A triple ⦃P⦄ mx ⦃Q⦄ over the writer log holds iff every outcome (a, w) in the support of mx.run satisfies Q.1 a (s ++ w) for every starting log s satisfying P. The starting log s threads through the WP interpretation itself, not through mx: WriterT.run mx alway...

If every oracle query in impl has the same evaluation distribution as the original query, then wp of the simulated computation equals wp of the original.

simulateQ cachingOracle only grows the cache: for any oa, if z ∈ support ((simulateQ cachingOracle oa).run cache₀) then cache₀ ≤ z.2.

If impl preserves Inv, then simulating any oracle computation with simulateQ impl preserves Inv on the final state (support-wise).