feat: Pure examples from HeapLang/Lib

Iris/Iris/HeapLang/Lib.lean

@@ -1,5 +1,8 @@
 module
 
+public import Iris.HeapLang.Lib.Arith
+public import Iris.HeapLang.Lib.Assert
+public import Iris.HeapLang.Lib.Diverge
 public import Iris.HeapLang.Lib.LandinsKnot
 public import Iris.HeapLang.Lib.LazyCoin
 public import Iris.HeapLang.Lib.Lock
@@ -8,3 +11,4 @@ public import Iris.HeapLang.Lib.Par
 public import Iris.HeapLang.Lib.Quicksort
 public import Iris.HeapLang.Lib.Spawn
 public import Iris.HeapLang.Lib.SpinLock
+public import Iris.HeapLang.Lib.Unwrap

Iris/Iris/HeapLang/Lib/Arith.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Instances
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.HeapLang.ProofMode
+
+namespace Iris.HeapLang
+
+open BI Iris ProgramLogic
+
+@[expose] public section
+
+namespace Arith
+
+@[rocq_alias heap_lang.minimum]
+def minimum : Val := hl_val%
+  λ m n, if m < n then m else n
+
+@[rocq_alias heap_lang.maximum]
+def maximum : Val := hl_val%
+  λ m n, if m < n then n else m
+
+section Spec
+
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+@[rocq_alias heap_lang.minimum_spec]
+theorem minimum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Int) :
+    ▷ Φ (Val.lit (.int (min m n))) -∗
+    WP hl(&minimum #m #n) @ s; E {{ Φ }} := by
+  iintro HΦ
+  wp_lam
+  wp_pures
+  by_cases h : m < n
+  · rw [decide_eq_true h]
+    wp_pures
+    rw [Int.min_eq_left (by omega)]
+    itrivial
+  · rw [decide_eq_false h]
+    wp_pures
+    rw [Int.min_eq_right (by omega)]
+    itrivial
+
+@[rocq_alias heap_lang.minimum_spec_nat]
+theorem minimum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) :
+    ▷ Φ (Val.lit (.int (Int.ofNat (min m n)))) -∗
+    WP hl(&minimum #m #n) @ s; E {{ Φ }} := by
+  iintro HΦ
+  iapply minimum_spec
+  rw [show min (↑m : Int) ↑n = ↑(min m n) by omega]
+  itrivial
+
+@[rocq_alias heap_lang.maximum_spec]
+theorem maximum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Int) :
+    ▷ Φ (Val.lit (.int (max m n))) -∗
+    WP hl(&maximum #m #n) @ s; E {{ Φ }} := by
+  iintro HΦ
+  wp_lam
+  wp_pures
+  by_cases h : m < n
+  · rw [decide_eq_true h]
+    wp_pures
+    rw [Int.max_eq_right (by omega)]
+    itrivial
+  · rw [decide_eq_false h]
+    wp_pures
+    rw [Int.max_eq_left (by omega)]
+    itrivial
+
+@[rocq_alias heap_lang.maximum_spec_nat]
+theorem maximum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) :
+    ▷ Φ (Val.lit (.int (Int.ofNat (max m n)))) -∗
+    WP hl(&maximum #m #n) @ s; E {{ Φ }} := by
+  iintro HΦ
+  iapply maximum_spec
+  rw [show max (↑m : Int) ↑n = ↑(max m n) by omega]
+  itrivial
+
+end Spec
+
+end Arith
+end

Iris/Iris/HeapLang/Lib/Assert.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Instances
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.HeapLang.ProofMode
+
+namespace Iris.HeapLang
+
+open BI Iris ProgramLogic
+
+@[expose] public section
+
+namespace Assert
+
+section Spec
+
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+-- TODO: use wp_smart_apply
+@[rocq_alias heap_lang.wp_assert]
+theorem wp_assert (E : CoPset) (Φ : Val → IProp GF) (e : Exp) :
+    WP e @ E {{ v, ⌜v = hl_val(#true)⌝ ∧ ▷ Φ hl_val(#()) }} -∗
+    WP hl(assert(&e)) @ E {{ Φ }} := by
+  iintro HΦ
+  unfold Exp.assert
+  wp_bind &e
+  iapply wp_wand $$ HΦ
+  iintro %v ⟨%Heq, _⟩ ; subst Heq
+  wp_if; itrivial
+
+end Spec
+
+end Assert
+end

Iris/Iris/HeapLang/Lib/Diverge.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Instances
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.HeapLang.ProofMode
+
+namespace Iris.HeapLang
+
+open BI Iris ProgramLogic
+
+@[expose] public section
+
+namespace Diverge
+
+@[rocq_alias heap_lang.diverge]
+def diverge : Val := hl_val%
+  rec diverge v := diverge v
+
+section Spec
+
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+@[rocq_alias heap_lang.wp_diverge]
+theorem wp_diverge (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (v : Val) :
+    ⊢ WP hl(&diverge &v) @ s; E {{ Φ }} := by
+  iloeb as IH
+  wp_lam
+  iapply IH
+
+end Spec
+
+end Diverge
+end

Iris/Iris/HeapLang/Lib/Unwrap.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Instances
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.HeapLang.ProofMode
+public import Iris.HeapLang.Lib.Assert
+
+namespace Iris.HeapLang
+
+open BI Iris ProgramLogic
+
+@[expose] public section
+
+namespace Unwrap
+
+/-- `unwrap o` unsafely asserts that `o` is `some v` and returns `v`. The
+`none` case is unreachable (it aborts via `assert`). -/
+@[rocq_alias heap_lang.unwrap]
+def unwrap : Val := hl_val%
+  λ o,
+    match o with
+    | none() => assert(#false)
+    | some(v) => v
+
+section Spec
+
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+@[rocq_alias heap_lang.unwrap_spec]
+theorem unwrap_spec (Φ : Val → IProp GF) (v : Val) :
+    ▷ Φ v ⊢ WP hl(&unwrap v(some(&v))) {{ Φ }} := by
+  iintro HΦ
+  wp_lam
+  wp_pures
+  iapply HΦ
+
+end Spec
+
+end Unwrap
+end

Iris/Iris/HeapLang/Syntax.lean

@@ -247,6 +247,7 @@ theorem Exp.stuck_subst {x v} : Exp.substStr x v Exp.stuck = Exp.stuck := by
   simp [Exp.stuck, Exp.substStr]
   simp only [substStr, ofVal]
 
+@[rocq_alias heap_lang.assert]
 def Exp.assert (e : Exp) := Exp.if e (.ofVal $ .lit .unit) Exp.stuck
 
 @[simp]