Oracle-Aware Unary WP Rules

This file connects the quantitative weakest precondition (wp) to simulateQ, providing rules that let program logic proofs pass through oracle simulation boundaries.

Main results

• wp_simulateQ_eq: If an oracle implementation preserves distributions, then wp is preserved.
• wp_liftComp: Lifting a computation to a larger oracle spec preserves wp.
• wp_simulateQ_run'_eq: Stateful oracle implementations that preserve distributions preserve wp.

theorem OracleComp.ProgramLogic.wp_simulateQ_eq {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (impl : QueryImpl spec (OracleComp spec)) (hImpl : ∀ (t : spec.Domain), evalDist (impl t) = evalDist (liftM (query t))) (oa : OracleComp spec α) (post : α → ENNReal) : wp (simulateQ impl oa) post = wp oa post

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.

theorem OracleComp.ProgramLogic.wp_liftComp {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {ι' : Type u_2} {superSpec : OracleSpec ι'} [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) (post : α → ENNReal) : wp (mx.liftComp superSpec) post = wp mx post

Lifting a computation to a larger oracle spec via liftComp preserves wp.

theorem OracleComp.ProgramLogic.wp_simulateQ_run'_eq {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (impl : QueryImpl spec (StateT σ (OracleComp spec))) (hImpl : ∀ (t : spec.Domain) (s : σ), evalDist ((impl t).run' s) = OptionT.lift (PMF.uniformOfFintype (spec.Range t))) (oa : OracleComp spec α) (s : σ) (post : α → ENNReal) : wp ((simulateQ impl oa).run' s) post = wp oa post

If a stateful oracle implementation preserves distributions (each query produces a uniform distribution after discarding state), then wp of simulateQ ... run' equals wp of the original computation.