From 7be89a06a93de12beadbbf8a3ae26b0fbb835685 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 27 Jul 2026 12:57:16 -0400
Subject: [PATCH 1/3] some quick examples

---
 Iris/Iris/HeapLang/Lib/Arith.lean   | 93 +++++++++++++++++++++++++++++
 Iris/Iris/HeapLang/Lib/Assert.lean  | 43 +++++++++++++
 Iris/Iris/HeapLang/Lib/Diverge.lean | 40 +++++++++++++
 Iris/Iris/HeapLang/Lib/Unwrap.lean  | 47 +++++++++++++++
 Iris/Iris/HeapLang/Syntax.lean      |  1 +
 5 files changed, 224 insertions(+)
 create mode 100644 Iris/Iris/HeapLang/Lib/Arith.lean
 create mode 100644 Iris/Iris/HeapLang/Lib/Assert.lean
 create mode 100644 Iris/Iris/HeapLang/Lib/Diverge.lean
 create mode 100644 Iris/Iris/HeapLang/Lib/Unwrap.lean

diff --git a/Iris/Iris/HeapLang/Lib/Arith.lean b/Iris/Iris/HeapLang/Lib/Arith.lean
new file mode 100644
index 000000000..f7186fdd4
--- /dev/null
+++ b/Iris/Iris/HeapLang/Lib/Arith.lean
@@ -0,0 +1,93 @@
+/-
+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 minimum]
+def minimum : Val := hl_val%
+  λ m n, if m < n then m else n
+
+@[rocq_alias 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 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
+    imodintro
+    rw [Int.min_eq_left (by omega)]
+    iexact HΦ
+  · rw [decide_eq_false h]
+    wp_pures
+    imodintro
+    rw [Int.min_eq_right (by omega)]
+    iexact HΦ
+
+@[rocq_alias 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]
+  iexact HΦ
+
+@[rocq_alias 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
+    imodintro
+    rw [Int.max_eq_right (by omega)]
+    iexact HΦ
+  · rw [decide_eq_false h]
+    wp_pures
+    imodintro
+    rw [Int.max_eq_left (by omega)]
+    iexact HΦ
+
+@[rocq_alias 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]
+  iexact HΦ
+
+end Spec
+
+end Arith
+end
diff --git a/Iris/Iris/HeapLang/Lib/Assert.lean b/Iris/Iris/HeapLang/Lib/Assert.lean
new file mode 100644
index 000000000..39c611e16
--- /dev/null
+++ b/Iris/Iris/HeapLang/Lib/Assert.lean
@@ -0,0 +1,43 @@
+/-
+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]
+
+@[rocq_alias 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, HΦ'⟩
+  subst Heq
+  wp_if
+  iapply fupd_intro
+  iexact HΦ'
+
+end Spec
+
+end Assert
+end
diff --git a/Iris/Iris/HeapLang/Lib/Diverge.lean b/Iris/Iris/HeapLang/Lib/Diverge.lean
new file mode 100644
index 000000000..ecde58f31
--- /dev/null
+++ b/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 diverge]
+def diverge : Val := hl_val%
+  rec diverge v := diverge v
+
+section Spec
+
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+@[rocq_alias 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
diff --git a/Iris/Iris/HeapLang/Lib/Unwrap.lean b/Iris/Iris/HeapLang/Lib/Unwrap.lean
new file mode 100644
index 000000000..8dffc0861
--- /dev/null
+++ b/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 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 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
diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean
index aa2c68027..d65e11130 100644
--- a/Iris/Iris/HeapLang/Syntax.lean
+++ b/Iris/Iris/HeapLang/Syntax.lean
@@ -237,6 +237,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 assert]
 def Exp.assert (e : Exp) := Exp.if e (.ofVal $ .lit .unit) Exp.stuck
 
 @[simp]

From 4bc786e4b8a05257d274cce4a9f3d0a8aba23481 Mon Sep 17 00:00:00 2001
From: Zongyuan Liu <liuzongyuan0505@gmail.com>
Date: Fri, 7 Aug 2026 16:11:20 +0200
Subject: [PATCH 2/3] Pass

---
 Iris/Iris/HeapLang/Lib.lean        |  4 ++++
 Iris/Iris/HeapLang/Lib/Arith.lean  | 16 ++++++----------
 Iris/Iris/HeapLang/Lib/Assert.lean |  8 +++-----
 3 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/Iris/Iris/HeapLang/Lib.lean b/Iris/Iris/HeapLang/Lib.lean
index e80bacdfa..5a790328f 100644
--- a/Iris/Iris/HeapLang/Lib.lean
+++ b/Iris/Iris/HeapLang/Lib.lean
@@ -1,8 +1,12 @@
 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.Lock
 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
diff --git a/Iris/Iris/HeapLang/Lib/Arith.lean b/Iris/Iris/HeapLang/Lib/Arith.lean
index f7186fdd4..dce9c6dee 100644
--- a/Iris/Iris/HeapLang/Lib/Arith.lean
+++ b/Iris/Iris/HeapLang/Lib/Arith.lean
@@ -41,14 +41,12 @@ theorem minimum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n :
   by_cases h : m < n
   · rw [decide_eq_true h]
     wp_pures
-    imodintro
     rw [Int.min_eq_left (by omega)]
-    iexact HΦ
+    itrivial
   · rw [decide_eq_false h]
     wp_pures
-    imodintro
     rw [Int.min_eq_right (by omega)]
-    iexact HΦ
+    itrivial
 
 @[rocq_alias minimum_spec_nat]
 theorem minimum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) :
@@ -57,7 +55,7 @@ theorem minimum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m
   iintro HΦ
   iapply minimum_spec
   rw [show min (↑m : Int) ↑n = ↑(min m n) by omega]
-  iexact HΦ
+  itrivial
 
 @[rocq_alias maximum_spec]
 theorem maximum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Int) :
@@ -69,14 +67,12 @@ theorem maximum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n :
   by_cases h : m < n
   · rw [decide_eq_true h]
     wp_pures
-    imodintro
     rw [Int.max_eq_right (by omega)]
-    iexact HΦ
+    itrivial
   · rw [decide_eq_false h]
     wp_pures
-    imodintro
     rw [Int.max_eq_left (by omega)]
-    iexact HΦ
+    itrivial
 
 @[rocq_alias maximum_spec_nat]
 theorem maximum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) :
@@ -85,7 +81,7 @@ theorem maximum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m
   iintro HΦ
   iapply maximum_spec
   rw [show max (↑m : Int) ↑n = ↑(max m n) by omega]
-  iexact HΦ
+  itrivial
 
 end Spec
 
diff --git a/Iris/Iris/HeapLang/Lib/Assert.lean b/Iris/Iris/HeapLang/Lib/Assert.lean
index 39c611e16..7e78f137c 100644
--- a/Iris/Iris/HeapLang/Lib/Assert.lean
+++ b/Iris/Iris/HeapLang/Lib/Assert.lean
@@ -23,6 +23,7 @@ section Spec
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
 
+-- TODO: use wp_smart_apply
 @[rocq_alias wp_assert]
 theorem wp_assert (E : CoPset) (Φ : Val → IProp GF) (e : Exp) :
     WP e @ E {{ v, ⌜v = hl_val(#true)⌝ ∧ ▷ Φ hl_val(#()) }} -∗
@@ -31,11 +32,8 @@ theorem wp_assert (E : CoPset) (Φ : Val → IProp GF) (e : Exp) :
   unfold Exp.assert
   wp_bind &e
   iapply wp_wand $$ HΦ
-  iintro %v ⟨%Heq, HΦ'⟩
-  subst Heq
-  wp_if
-  iapply fupd_intro
-  iexact HΦ'
+  iintro %v ⟨%Heq, _⟩ ; subst Heq
+  wp_if; itrivial
 
 end Spec
 

From 0dc08b61fafb34de190f9c9e4575e76df33baa4d Mon Sep 17 00:00:00 2001
From: Zongyuan Liu <liuzongyuan0505@gmail.com>
Date: Fri, 7 Aug 2026 16:16:39 +0200
Subject: [PATCH 3/3] Fix stale aliases

---
 Iris/Iris/HeapLang/Lib/Arith.lean   | 12 ++++++------
 Iris/Iris/HeapLang/Lib/Assert.lean  |  2 +-
 Iris/Iris/HeapLang/Lib/Diverge.lean |  4 ++--
 Iris/Iris/HeapLang/Lib/Unwrap.lean  |  4 ++--
 Iris/Iris/HeapLang/Syntax.lean      |  2 +-
 5 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/Iris/Iris/HeapLang/Lib/Arith.lean b/Iris/Iris/HeapLang/Lib/Arith.lean
index dce9c6dee..16e29949e 100644
--- a/Iris/Iris/HeapLang/Lib/Arith.lean
+++ b/Iris/Iris/HeapLang/Lib/Arith.lean
@@ -19,11 +19,11 @@ open BI Iris ProgramLogic
 
 namespace Arith
 
-@[rocq_alias minimum]
+@[rocq_alias heap_lang.minimum]
 def minimum : Val := hl_val%
   λ m n, if m < n then m else n
 
-@[rocq_alias maximum]
+@[rocq_alias heap_lang.maximum]
 def maximum : Val := hl_val%
   λ m n, if m < n then n else m
 
@@ -31,7 +31,7 @@ section Spec
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
 
-@[rocq_alias minimum_spec]
+@[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
@@ -48,7 +48,7 @@ theorem minimum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n :
     rw [Int.min_eq_right (by omega)]
     itrivial
 
-@[rocq_alias minimum_spec_nat]
+@[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
@@ -57,7 +57,7 @@ theorem minimum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m
   rw [show min (↑m : Int) ↑n = ↑(min m n) by omega]
   itrivial
 
-@[rocq_alias maximum_spec]
+@[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
@@ -74,7 +74,7 @@ theorem maximum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n :
     rw [Int.max_eq_left (by omega)]
     itrivial
 
-@[rocq_alias maximum_spec_nat]
+@[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
diff --git a/Iris/Iris/HeapLang/Lib/Assert.lean b/Iris/Iris/HeapLang/Lib/Assert.lean
index 7e78f137c..9b1982360 100644
--- a/Iris/Iris/HeapLang/Lib/Assert.lean
+++ b/Iris/Iris/HeapLang/Lib/Assert.lean
@@ -24,7 +24,7 @@ section Spec
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
 
 -- TODO: use wp_smart_apply
-@[rocq_alias wp_assert]
+@[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
diff --git a/Iris/Iris/HeapLang/Lib/Diverge.lean b/Iris/Iris/HeapLang/Lib/Diverge.lean
index ecde58f31..492a5135d 100644
--- a/Iris/Iris/HeapLang/Lib/Diverge.lean
+++ b/Iris/Iris/HeapLang/Lib/Diverge.lean
@@ -19,7 +19,7 @@ open BI Iris ProgramLogic
 
 namespace Diverge
 
-@[rocq_alias diverge]
+@[rocq_alias heap_lang.diverge]
 def diverge : Val := hl_val%
   rec diverge v := diverge v
 
@@ -27,7 +27,7 @@ section Spec
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
 
-@[rocq_alias wp_diverge]
+@[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
diff --git a/Iris/Iris/HeapLang/Lib/Unwrap.lean b/Iris/Iris/HeapLang/Lib/Unwrap.lean
index 8dffc0861..65bae9674 100644
--- a/Iris/Iris/HeapLang/Lib/Unwrap.lean
+++ b/Iris/Iris/HeapLang/Lib/Unwrap.lean
@@ -22,7 +22,7 @@ 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 unwrap]
+@[rocq_alias heap_lang.unwrap]
 def unwrap : Val := hl_val%
   λ o,
     match o with
@@ -33,7 +33,7 @@ section Spec
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
 
-@[rocq_alias unwrap_spec]
+@[rocq_alias heap_lang.unwrap_spec]
 theorem unwrap_spec (Φ : Val → IProp GF) (v : Val) :
     ▷ Φ v ⊢ WP hl(&unwrap v(some(&v))) {{ Φ }} := by
   iintro HΦ
diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean
index bb2511462..8b82bd62d 100644
--- a/Iris/Iris/HeapLang/Syntax.lean
+++ b/Iris/Iris/HeapLang/Syntax.lean
@@ -247,7 +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 assert]
+@[rocq_alias heap_lang.assert]
 def Exp.assert (e : Exp) := Exp.if e (.ofVal $ .lit .unit) Exp.stuck
 
 @[simp]