feat: add Triple.observe

src/Std/Do/Triple/Basic.lean

@@ -110,4 +110,21 @@ for `Q₁`, then `mp x h₁ h₂` is a proof for `Q₂` about `x`.
 theorem mp [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ (Q₁ →ₚ Q₂)) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
   Triple.iff.mpr <| SPred.and_mono (Triple.iff.mp h₁) (Triple.iff.mp h₂) |>.trans ((wp x).conjunctive Q₁ (Q₁ →ₚ Q₂)).mpr |>.trans ((wp x).mono _ _ PostCond.and_imp)
 
+/--
+Observes a fact `Q` about the state by running a stateless program `obs`, then carries `Q` into the
+proof of `prog`. A triple for `prog` follows from a triple for `obs` that assumes the postcondition
+`Q` of the specification `h` and establishes the goal `wp⟦prog⟧ Post`. This requires `obs` to be
+*stateless*: the premise `hp` states that its successful runs leave the state unchanged.
+-/
+theorem observe [WP m ps] {α β : Type u} {obs : m α} {prog : m β}
+    {Pre : Assertion ps} {Q : PostCond α ps} {Post : PostCond β ps}
+    (hp : ∀ C : Assertion ps, wp⟦obs⟧ (PostCond.noThrow fun _ => C) ⊢ₛ C)
+    (h : Triple obs Pre Q)
+    (hgoal : Triple obs Pre (Q →ₚ PostCond.noThrow fun _ => wp⟦prog⟧ Post)) :
+    Triple prog Pre Post :=
+  Triple.of_entails_wp <|
+    (Triple.entails_wp_of_pre_post (Triple.mp obs h hgoal) SPred.and_self.mpr
+      (PostCond.entails.mk (fun _ => SPred.and_elim_r) (ExceptConds.and_elim_right _ _))).trans
+    (hp (wp⟦prog⟧ Post))
+
 end Triple

tests/elab/doLogicTests.lean

@@ -829,3 +829,83 @@ theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
   mvcgen
   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
   all_goals grind
+
+/-! ### The partial correctness trick
+
+Specifications are written in the object language as boolean monadic predicates. A triple
+hypothesis is consumed by observing its program via `Triple.observe`
+and stepping through it with `mvcgen`. -/
+
+namespace PartialCorrectnessTrick
+
+inductive RustError where
+  | rustPanic
+  | integerOverflow
+
+abbrev RustM := Except RustError
+
+/-- A boolean monadic predicate holds when it returns `true` without throwing. -/
+abbrev RustM.holds (p : RustM Bool) : Prop := ⦃⌜True⌝⦄ p ⦃⇓ r => ⌜r⌝⦄
+
+/-- Running an `Except` program and discarding its result preserves any goal. -/
+theorem wp_const (p : RustM α) (C : Assertion (.except RustError .pure)) :
+    wp⟦p⟧ (⇓ _ => C) ⊢ₛ C := by
+  cases p with
+  | ok a => exact SPred.entails.refl _
+  | error e => exact SPred.false_elim
+
+namespace Unfoldable
+
+def panicAdd (x y : Nat) : RustM Nat := do
+  if (x + y) ≤ 100 then pure (x + y) else Except.error .integerOverflow
+
+def pre (x : Nat) : RustM Bool := do
+  if x ≤ 10 then
+    pure ((← panicAdd x 10) == 15)
+  else
+    pure false
+
+def f (x : Nat) : RustM Nat := do
+  panicAdd x 5
+
+def post (x : Nat) (res : Nat) : RustM Bool := do
+  pure (res == 10)
+
+example (x : Nat) :
+    (pre x).holds → ⦃⌜True⌝⦄ f x ⦃⇓ res => ⌜(post x res).holds⌝⦄ := by
+  intro h
+  apply Triple.observe (wp_const (pre x)) h
+  mvcgen [pre, panicAdd] <;> try grind
+  intro hx
+  mvcgen [f, post, panicAdd] <;> try grind
+  mvcgen [post] <;> grind
+
+end Unfoldable
+
+namespace Opaque
+
+opaque g : Nat → RustM Nat
+
+def pre (x : Nat) : RustM Bool := do pure (x == (← g 0))
+
+def f (x : Nat) : RustM Nat := pure (x + 1)
+
+def post (x : Nat) (res : Nat) : RustM Bool := do pure (res - 1 == (← g 0))
+
+/-- Partial-correctness self-specification: if `p` succeeds with `r`, then `p = .ok r`. -/
+theorem self_spec (p : RustM α) : ⦃⌜True⌝⦄ p ⦃⇓? r => ⌜p = .ok r⌝⦄ := by
+  cases p with
+  | ok a => exact Triple.pure a (by simp)
+  | error e => apply Triple.of_entails_wp; intro _; exact True.intro
+
+example (x : Nat) :
+    (pre x).holds → ⦃⌜True⌝⦄ f x ⦃⇓ res => ⌜(post x res).holds⌝⦄ := by
+  intro h
+  apply Triple.observe (wp_const (pre x)) h
+  have hg := self_spec (g 0)
+  mvcgen [pre, hg, f] <;> try grind
+  simp
+
+end Opaque
+
+end PartialCorrectnessTrick