Program logic cutover phase 2 baseline

Author: quangvdao

ToMathlib/Control/Monad/Algebra.lean

@@ -114,3 +114,83 @@ theorem triple_bind [LawfulMonad m] {pre : l} {x : m α} {cut : α → l}
   exact le_trans hx (wp_mono x hf)
 
 end MAlgOrdered
+
+/-! ## Transformer lifting instances -/
+
+namespace MAlgOrdered
+
+variable {m : Type u → Type v} {l : Type u}
+variable [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l]
+
+/-- Lift an ordered monad algebra through `StateT`. -/
+noncomputable def instStateT (σ : Type u) :
+    MAlgOrdered (StateT σ m) (σ → l) where
+  μ x := fun s => MAlgOrdered.μ (x.run s >>= fun y => pure (y.1 y.2))
+  μ_pure x := by
+    funext s
+    simp [StateT.run_pure, MAlgOrdered.μ_pure]
+  μ_bind_mono f g hfg x := by
+    intro s
+    simp only [StateT.run_bind, bind_assoc]
+    exact MAlgOrdered.μ_bind_mono
+      (f := fun y => (f y.1).run y.2 >>= fun z => pure (z.1 z.2))
+      (g := fun y => (g y.1).run y.2 >>= fun z => pure (z.1 z.2))
+      (fun y => (hfg y.1) y.2)
+      (x.run s)
+
+attribute [instance] instStateT
+
+/-- Lift an ordered monad algebra through `ReaderT`. -/
+noncomputable def instReaderT (ρ : Type u) :
+    MAlgOrdered (ReaderT ρ m) (ρ → l) where
+  μ x := fun r => MAlgOrdered.μ (x.run r >>= fun q => pure (q r))
+  μ_pure x := by
+    funext r
+    simp [ReaderT.run_pure, MAlgOrdered.μ_pure]
+  μ_bind_mono f g hfg x := by
+    intro r
+    simp only [ReaderT.run_bind, bind_assoc]
+    exact MAlgOrdered.μ_bind_mono
+      (f := fun a => (f a).run r >>= fun q => pure (q r))
+      (g := fun a => (g a).run r >>= fun q => pure (q r))
+      (fun a => (hfg a) r)
+      (x.run r)
+
+attribute [instance] instReaderT
+
+/-- Lift an ordered monad algebra through `ExceptT` by interpreting exceptions as `⊥`. -/
+noncomputable def instExceptT (ε : Type u) :
+    MAlgOrdered (ExceptT ε m) l where
+  μ x := MAlgOrdered.μ <| (fun y : Except ε l =>
+    match y with
+    | Except.ok z => z
+    | Except.error _ => ⊥) <$> x.run
+  μ_pure x := by
+    simp [MAlgOrdered.μ_pure]
+  μ_bind_mono f g hfg x := by
+    let collapse : Except ε l → l := fun y =>
+      match y with
+      | Except.ok z => z
+      | Except.error _ => ⊥
+    simpa [ExceptT.run_bind, collapse] using
+      (MAlgOrdered.μ_bind_mono
+        (f := fun y => collapse <$>
+          (match y with
+          | Except.ok a => (f a).run
+          | Except.error e => pure (Except.error e)))
+        (g := fun y => collapse <$>
+          (match y with
+          | Except.ok a => (g a).run
+          | Except.error e => pure (Except.error e)))
+        (by
+          intro y
+          cases y with
+          | error e =>
+              simp [collapse, MAlgOrdered.μ_pure]
+          | ok a =>
+              simpa [collapse] using hfg a)
+        x.run)
+
+attribute [instance] instExceptT
+
+end MAlgOrdered

VCVio/ProgramLogic/Relational/Basic.lean

@@ -29,11 +29,36 @@ def PointwiseDom (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β)
 /-- Equality relation helper for same-type outputs. -/
 def EqRel (α : Type) : RelPost α α := fun x y => x = y
 
+/-! A minimal relational triple skeleton (coupling-ready API surface). -/
+
+/-- Minimal relational triple skeleton for two computations and a relational postcondition. -/
+def RelTriple (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β)
+    (post : RelPost α β) : Prop :=
+  PointwiseDom oa ob post
+
 @[simp]
 lemma pointwiseDom_refl (oa : OracleComp spec₁ α) :
     PointwiseDom (spec₁ := spec₁) (spec₂ := spec₁) oa oa (EqRel α) := by
   intro x y hxy
   subst hxy
   exact le_rfl
 
+@[simp]
+lemma relTriple_refl (oa : OracleComp spec₁ α) :
+    RelTriple (spec₁ := spec₁) (spec₂ := spec₁) oa oa (EqRel α) :=
+  pointwiseDom_refl (spec₁ := spec₁) oa
+
+lemma pointwiseDom_post_mono {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β}
+    {post post' : RelPost α β}
+    (h : PointwiseDom oa ob post) (hpost : ∀ ⦃x y⦄, post' x y → post x y) :
+    PointwiseDom oa ob post' := by
+  intro x y hxy
+  exact h (hpost hxy)
+
+lemma relTriple_post_mono {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β}
+    {post post' : RelPost α β}
+    (h : RelTriple oa ob post) (hpost : ∀ ⦃x y⦄, post' x y → post x y) :
+    RelTriple oa ob post' :=
+  pointwiseDom_post_mono h hpost
+
 end OracleComp.ProgramLogic.Relational

VCVio/ProgramLogic/Unary/Examples.lean

@@ -36,3 +36,33 @@ example (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
   probEvent_eq_wp_indicator (spec := spec) oa p
 
 end OracleComp.ProgramLogic
+
+namespace MAlgOrdered
+
+open MAlgOrdered
+
+universe v
+
+variable {m : Type u → Type v} {L : Type u}
+variable [Monad m] [LawfulMonad m] [CompleteLattice L] [MAlgOrdered m L]
+variable {α β σ ρ ε : Type u}
+
+example (x : StateT σ m α) (f : α → StateT σ m β) (post : β → σ → L) :
+    MAlgOrdered.wp (m := StateT σ m) (l := σ → L) (x >>= f) post =
+      MAlgOrdered.wp (m := StateT σ m) (l := σ → L) x
+        (fun a => MAlgOrdered.wp (m := StateT σ m) (l := σ → L) (f a) post) := by
+  simpa using (MAlgOrdered.wp_bind (m := StateT σ m) (l := σ → L) x f post)
+
+example (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (post : β → ρ → L) :
+    MAlgOrdered.wp (m := ReaderT ρ m) (l := ρ → L) (x >>= f) post =
+      MAlgOrdered.wp (m := ReaderT ρ m) (l := ρ → L) x
+        (fun a => MAlgOrdered.wp (m := ReaderT ρ m) (l := ρ → L) (f a) post) := by
+  simpa using (MAlgOrdered.wp_bind (m := ReaderT ρ m) (l := ρ → L) x f post)
+
+example (x : ExceptT ε m α) (f : α → ExceptT ε m β) (post : β → L) :
+    MAlgOrdered.wp (m := ExceptT ε m) (l := L) (x >>= f) post =
+      MAlgOrdered.wp (m := ExceptT ε m) (l := L) x
+        (fun a => MAlgOrdered.wp (m := ExceptT ε m) (l := L) (f a) post) := by
+  simpa using (MAlgOrdered.wp_bind (m := ExceptT ε m) (l := L) x f post)
+
+end MAlgOrdered

VCVio/ProgramLogic/Unary/HoareTriple.lean

@@ -25,6 +25,13 @@ variable {ι : Type u} {spec : OracleSpec ι}
 variable [spec.Fintype] [spec.Inhabited]
 variable {α β : Type}
 
+/-! ## API contract
+
+- This unary quantitative interface is instantiated for `OracleComp spec`.
+- Probability/evaluation assumptions are `[spec.Fintype]` and `[spec.Inhabited]`.
+- The quantitative codomain is fixed to `ℝ≥0∞`.
+-/
+
 /-- Expectation-style algebra for oracle computations returning `ℝ≥0∞`. -/
 noncomputable def μ (oa : OracleComp spec ℝ≥0∞) : ℝ≥0∞ :=
   ∑' x, Pr[= x | oa] * x