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 (HasQuery.query t) fun (a : spec.Range t) => (Q.1 a).down⌝⦄ HasQuery.query t ⦃Q⦄

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

The bare query here resolves to HasQuery.query (m := OracleComp spec), which unfolds to liftM (OracleSpec.query t).

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 (HasQuery.query t >>= f) fun (a : α) => (Q.1 a).down⌝⦄ (HasQuery.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 (HasQuery.query t) fun (a : spec.Range t) => (Q.1 a).down⌝⦄ MonadLift.monadLift (OracleSpec.query t) ⦃Q⦄

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

When query t appears inside a do block via MonadLift, Lean's elaborator inserts a single MonadLift.monadLift _ (OracleSpec.query t) (no MonadLiftT wrapper). The HasQuery.query form (the bare query after the ergonomic cutover) instead elaborates via MonadLiftT. 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.

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 _ (OracleSpec.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.