Std.Do / mvcgen bridge for OracleComp

This module provides a proposition-level bridge on top of the quantitative WP in ProgramLogic.Unary.HoareTriple, with a Std.Do.WPMonad instance for .pure post-shape. The bridge is scoped to almost-sure correctness (= 1).

noncomputable def OracleComp.ProgramLogic.StdDo.wpProp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → Prop) : Prop

Proposition-level bridge from quantitative WP (= 1 threshold).

def OracleComp.ProgramLogic.StdDo.tripleProp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (pre : Prop) (oa : OracleComp spec α) (post : α → Prop) : Prop

Proposition-style triple alias used by the Std.Do bridge.

theorem OracleComp.ProgramLogic.StdDo.wpProp_iff_probEvent_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) : wpProp oa p ↔ probEvent oa p = 1

Adequacy bridge between wpProp and event probability = 1.

theorem OracleComp.ProgramLogic.StdDo.wpProp_iff_forall_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) : wpProp oa p ↔ ∀ x ∈ support oa, p x

Support-based characterization of almost-sure postconditions for OracleComp.

theorem OracleComp.ProgramLogic.StdDo.wpProp_pure {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (p : α → Prop) : wpProp (pure x) p ↔ p x

wpProp rule for pure.

theorem OracleComp.ProgramLogic.StdDo.wpProp_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (p : β → Prop) : wpProp (oa >>= ob) p ↔ wpProp oa fun (a : α) => wpProp (ob a) p

wpProp rule for bind.

@[implicit_reducible]

noncomputable instance OracleComp.ProgramLogic.StdDo.instWPOracleComp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] : Std.Do.WP (OracleComp spec) Std.Do.PostShape.pure

Std.Do WP instance for OracleComp, scoped to almost-sure correctness.

@[implicit_reducible]

noncomputable instance OracleComp.ProgramLogic.StdDo.instWPMonadOracleComp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] : Std.Do.WPMonad (OracleComp spec) Std.Do.PostShape.pure

Std.Do WPMonad instance for OracleComp under wpProp.

Support-based bridge for stateful transformers over OracleComp

The two lemmas below reduce Std.Do.Triple for StateT σ (OracleComp spec) and WriterT ω (OracleComp spec) to support-based statements about the underlying OracleComp distribution. They are the canonical "escape hatch" used whenever a handler proof needs to leave mvcgen (e.g. to perform a structural induction on OracleComp) without abandoning the Std.Do proof mode entirely.

theorem OracleComp.ProgramLogic.StdDo.triple_stateT_iff_forall_support {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ α : Type} (mx : StateT σ (OracleComp spec) α) (P : Std.Do.Assertion (Std.Do.PostShape.arg σ Std.Do.PostShape.pure)) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ Std.Do.PostShape.pure)) : ⦃P⦄ mx ⦃Q⦄ ↔ ∀ (s : σ), (P s).down → ∀ (a : α) (s' : σ), (a, s') ∈ support (mx.run s) → (Q.1 a s').down

Support characterization of Std.Do.Triple on StateT σ (OracleComp spec).

A triple ⦃P⦄ mx ⦃Q⦄ holds iff every outcome (a, s') in the support of mx.run s satisfies the postcondition Q.1 a s', whenever the starting state s satisfies the precondition P.

theorem OracleComp.ProgramLogic.StdDo.triple_writerT_iff_forall_support {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ω α : Type} [EmptyCollection ω] [Append ω] [LawfulAppend ω] (mx : WriterT ω (OracleComp spec) α) (P : Std.Do.Assertion (Std.Do.PostShape.arg ω Std.Do.PostShape.pure)) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ω Std.Do.PostShape.pure)) : ⦃P⦄ mx ⦃Q⦄ ↔ ∀ (s : ω), (P s).down → ∀ (a : α) (w : ω), (a, w) ∈ support mx.run → (Q.1 a (s ++ w)).down

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 always begins from ∅ and produces pairs (a, w), and the WP transformer defined in VCVio.ProgramLogic.Unary.WriterTBridge then prepends s via s ++ _ before applying the postcondition. This is why s appears only in Q.1 a (s ++ w) on the right-hand side.

theorem OracleComp.ProgramLogic.StdDo.triple_writerT_iff_forall_support_monoid {ι : Type} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ω α : Type} [Monoid ω] (mx : WriterT ω (OracleComp spec) α) (P : Std.Do.Assertion (Std.Do.PostShape.arg ω Std.Do.PostShape.pure)) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ω Std.Do.PostShape.pure)) : ⦃P⦄ mx ⦃Q⦄ ↔ ∀ (s : ω), (P s).down → ∀ (a : α) (w : ω), (a, w) ∈ support mx.run → (Q.1 a (s * w)).down

Monoid-variant of triple_writerT_iff_forall_support.

For WriterT ω (OracleComp spec) where the log ω is a (multiplicative) monoid, a triple ⦃P⦄ mx ⦃Q⦄ 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. As in the Append-based variant, the starting log s threads through the WP interpretation (s * _), not through mx. This is the dual of the Append-based characterization and is what countingOracle / costOracle proofs use (where QueryCount ι = ι → ℕ has a Monoid instance but no Append).

theorem OracleComp.ProgramLogic.StdDo.Spec.query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) {Q : Std.Do.PostCond (spec.Range t) Std.Do.PostShape.pure} : ⦃⌜wpProp (liftM (OracleQuery.query t)) fun (a : spec.Range t) => (Q.1 a).down⌝⦄ liftM (OracleQuery.query t) ⦃Q⦄

Query specification for mspec/mvcgen in the .pure Std.Do view.

theorem OracleComp.ProgramLogic.StdDo.Spec.query_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (t : spec.Domain) {f : spec.Range t → OracleComp spec α} {Q : Std.Do.PostCond α Std.Do.PostShape.pure} : ⦃⌜wpProp (liftM (OracleQuery.query t) >>= f) fun (a : α) => (Q.1 a).down⌝⦄ (liftM (OracleQuery.query t) >>= f) ⦃Q⦄

Bind-chain specification shape for mspec/mvcgen in OracleComp do-blocks.

theorem OracleComp.ProgramLogic.StdDo.Spec.monadLift_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) {Q : Std.Do.PostCond (spec.Range t) Std.Do.PostShape.pure} : ⦃⌜wpProp (liftM (OracleQuery.query t)) fun (a : spec.Range t) => (Q.1 a).down⌝⦄ MonadLift.monadLift (OracleQuery.query t) ⦃Q⦄

Explicit-head spec for the MonadLift OracleQuery OracleComp-form of query.

When query t appears inside a do block, Lean's elaborator inserts a single MonadLift.monadLift _ (OracleQuery.query t) (no MonadLiftT wrapper). The ascription form (OracleComp.query t : OracleComp spec _) instead elaborates to liftM (instMonadLiftTOfMonadLift _ _) (OracleQuery.query t). The two are definitionally equal but syntactically distinct, and Lean.Elab.Tactic.Do.Spec.findSpec matches keys syntactically against a DiscrTree. This lemma re-states the content of Spec.query with the explicit MonadLift.monadLift head so mvcgen finds a match in do-block contexts. The two should be unified once core mvcgen normalizes liftM/MonadLiftT chains in its discrimination-tree key construction (upstream issue).

Architectural note: mvcgen for stateful handlers over OracleComp

Stateful handlers like cachingOracle (StateT) and loggingOracle (WriterT) are defined as QueryImpl spec (T (OracleComp spec)) for some state-tracking transformer T. mvcgen walks their bodies cleanly thanks to:

1. The low-priority MonadLift (OracleComp spec) (OracleComp superSpec) instance in Coercions/SubSpec.lean. By being lower priority than Lean's built-in reflexive MonadLiftT.refl, the self-lift case (spec = superSpec) is solved by MonadLiftT.refl rather than this parametric instance, and monadLift mx : OracleComp spec α reduces to id mx = mx definitionally. This is what Std.Do.Spec.UnfoldLift.monadLift_refl (a rfl-based lemma) needs in order to peel off the spurious self-lifts the parametric instance would otherwise leave behind around every nested oracle query. By being lower priority than the built-in MonadLift (OracleQuery superSpec) (OracleComp superSpec), single-query lifts also resolve via the standard "lift query then embed" path and avoid spurious walks through liftComp.

2. The Spec.monadLift_query lemma below, which provides a DiscrTree-friendly @[spec] keyed by the explicit MonadLift.monadLift _ (OracleQuery.query t) head that do-block elaboration produces. The plain Spec.query above keys on a different syntactic head and doesn't fire inside do blocks.

The first is now structural in VCVio with no special override needed. The second is a workaround for a discrimination-tree-key normalisation gap in upstream mvcgen and can be removed once Lean.Elab.Tactic.Do.Spec.findSpec and Lean.Elab.Tactic.Do.Attr.mkSpecTheorem canonicalise liftM/MonadLiftT chains.