diff --git a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean
index 953f65a1c..72f85ecc5 100644
--- a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean
+++ b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Bai, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.Instances.Lib.Invariants
@@ -37,17 +42,9 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F
   iintro !> %Φ ⟨#H, HP⟩ HQ
   wp_bind &landinsKnot _
   wp_rec
-  wp_bind ref(_)
-  wp_pures
-  iapply wp_alloc
-  iintro !> %r Hr
-  wp_pures
-  wp_bind (_ ← _)
-  iapply wp_store $$ Hr
-  iintro !> Hr
-  wp_pures
-  iapply wp_load $$ Hr
-  iintro !> Hr
+  wp_alloc r as Hr
+  wp_store
+  wp_load
   imod inv_alloc landinN ⊤ _ $$ Hr with #Hinv
   ihave HQ : ▷ (∀ u, Q u v1 -∗ Φ u) $$ [HQ]
   · inext; iexact HQ
@@ -58,8 +55,7 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F
   imod inv_acc $$ Hinv with ⟨Hr, Hcl⟩
   simp only [CoPset.subseteq_top]
   imodintro
-  iapply wp_load $$ Hr
-  iintro !> Hr
+  wp_load
   imod Hcl $$ Hr
   iapply H $$ [HP] [$]
   iframe HP
diff --git a/Iris/Iris/HeapLang/Lib/Quicksort.lean b/Iris/Iris/HeapLang/Lib/Quicksort.lean
index af85196f0..0d1f21909 100644
--- a/Iris/Iris/HeapLang/Lib/Quicksort.lean
+++ b/Iris/Iris/HeapLang/Lib/Quicksort.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros, Michael Sammler, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.HeapLang.PrimitiveLaws
@@ -115,9 +120,7 @@ theorem cons_spec x l ls Φ :
     WP hl(&cons #x &l) {{ Φ }} := by
   iintro Hl HΦ
   wp_rec; wp_pures
-  wp_bind ref(_)
-  iapply wp_alloc
-  iintro !> %l Hl
+  wp_alloc l
   wp_pures
   imodintro
   iapply HΦ
@@ -142,9 +145,7 @@ theorem append_spec l1 ls1 l2 ls2 Φ :
   | cons x xs =>
     icases isList_cons $$ Hl1 with ⟨%l, %tl, %heq, Hpt, Hl⟩
     subst heq; wp_pures
-    wp_bind !_
-    iapply wp_load $$ Hpt
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &append _ _
     iapply IH $$ Hl Hl2
@@ -177,9 +178,7 @@ theorem partition_spec x l ls Φ :
     dsimp only
     icases Hl with ⟨%_, %tl, %hl, Hpt, Hl⟩; subst hl
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ [$]
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &partition _ _
     iapply IH $$ Hl
@@ -231,9 +230,7 @@ theorem quicksort_spec l ls Φ :
     dsimp only
     icases Hl with ⟨%l, %tl, %heq, Hpt, Hl⟩; subst heq
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ [$]
-    iintro !> Hpt
+    wp_load
     wp_pures
     wp_bind &partition _ _
     iapply partition_spec $$ [$]
@@ -318,9 +315,7 @@ theorem wp_checkSorted (v vacc : Val) (l : List Int) (Φ : Val → IProp GF) :
     icases isList_cons $$ H with ⟨%loc, %tlv, %heq, Hpt, Htl⟩
     subst heq
     wp_pures
-    wp_bind !_
-    iapply wp_load $$ Hpt
-    iintro !> Hpt
+    wp_load
     rcases hinv with rfl | ⟨va, rfl, hva⟩
     · wp_pures
       iapply IH $$ %_ %tl %_ %((List.pairwise_cons.mp hsorted).2)
diff --git a/Iris/Iris/HeapLang/Lib/Spawn.lean b/Iris/Iris/HeapLang/Lib/Spawn.lean
index c8758eb27..da9241efa 100644
--- a/Iris/Iris/HeapLang/Lib/Spawn.lean
+++ b/Iris/Iris/HeapLang/Lib/Spawn.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Zongyuan Liu
+Authors: Zongyuan Liu, Klaus Kraßnitzer
 -/
 module
 
@@ -73,10 +73,7 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
       WP hl(&spawn &f) {{ Φ }} := by
   iintro !> %Φ Hf HΦ
   wp_rec
-  wp_bind ref(_)
-  wp_pures
-  iapply wp_alloc
-  iintro !> %l Hl
+  wp_alloc l as Hl
   imod token_alloc with ⟨%γ, Hγ⟩
   iapply fupd_wp
   imod inv_alloc N ⊤ (spawnInv γ l Ψ) $$ [Hl] with #Hinv
@@ -106,11 +103,10 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
   unfold spawnInv
   icases Hpt with ⟨%_, Hl, _⟩
   imodintro
-  iapply wp_store $$ Hl
-  iintro !> Hpt
+  wp_store
   iapply Hclose
   inext
-  iexists _; iframe Hpt
+  iexists _; iframe Hl
   iright; iexists v; isplit
   · itrivial
   · iframe
@@ -131,8 +127,7 @@ theorem join_spec (Ψ : Val → IProp GF) (l : Loc) :
   unfold spawnInv
   icases Hpt with ⟨%lv, Hl, Hcond⟩
   imodintro
-  iapply wp_load $$ Hl
-  iintro !> Hl
+  wp_load
   icases Hcond with (%Heq | ⟨%w, %Heq, (HΨw | Hγ')⟩) <;> subst Heq
   · imod Hclose $$ [Hl]
     · inext
diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean
index f632130c9..ecdca93da 100644
--- a/Iris/Iris/HeapLang/Lib/SpinLock.lean
+++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, ayhon, Klaus Kraßnitzer
+-/
 module
 
 public import Iris.HeapLang.Lib.Lock
@@ -85,8 +90,8 @@ theorem newlock_spec :
   iintro !> %Φ Hcont
   wp_rec
   imod token_alloc with ⟨%γ, Hγ⟩
-  iapply wp_alloc
-  iintro !> %l Hpt
+  wp_alloc l as Hpt
+  imodintro
   iapply Hcont
   iintro %R %E HR
   imod inv_alloc spinlockN E (lockInv γ l R) $$ [Hpt HR Hγ] with H
@@ -118,11 +123,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
   icases G1 with ⟨%b, Hpt, Hcond⟩
   cases b
   · simp only [Bool.false_eq_true, ↓reduceIte]
-    iapply wp_wand $$ [Hpt]
-    · iapply wp_cmpXchg_true rfl rfl $$ Hpt <;>
-        simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed]
-    iintro %v ⟨%Heq, Hpt⟩
-    subst Heq
+    wp_cmpxchg_suc
     imod G2 $$ [Hpt]
     · iexists true
       simp only [↓reduceIte]
@@ -134,11 +135,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
       simp only [↓reduceIte]
       iframe
   · simp only [↓reduceIte]
-    iapply wp_wand $$ [Hpt]
-    · iapply wp_cmpXchg_fail rfl rfl $$ Hpt <;>
-        simp [Val.compareSafe, Val.isUnboxed, BaseLit.isUnboxed]
-    iintro %v ⟨%Heq, Hpt⟩
-    subst Heq
+    wp_cmpxchg_fail
     imod G2 $$ [Hpt]
     · iexists true
       simp only [↓reduceIte]
@@ -187,8 +184,7 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) :
   unfold lockInv
   imodintro
   icases G1 with ⟨%b, Hpt, Hcond⟩
-  iapply wp_store $$ Hpt
-  iintro !> Hpt
+  wp_store
   imod G2 $$ [- Hcont]
   · inext
     iexists false
diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean
index f71882eb7..e13a0c2e0 100644
--- a/Iris/Iris/HeapLang/ProofMode.lean
+++ b/Iris/Iris/HeapLang/ProofMode.lean
@@ -1,12 +1,14 @@
 /-
-Copyright (c) 2026 Fernando Leal. All rights reserved.
+Copyright (c) 2026 Fernando Leal, Klaus Kraßnitzer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fernando Leal, Klaus Kraßnitzer
 -/
 module
 
 public import Iris.ProofMode
 public import Iris.HeapLang.Tactic
 public import Iris.HeapLang.Instances
+public import Iris.HeapLang.PrimitiveLaws
 public import Iris.ProgramLogic.WeakestPre
 public import Iris.ProgramLogic.Language
 public import Iris.ProgramLogic.EctxLanguage
@@ -206,7 +208,6 @@ public meta def iWpValueHead {u}
   {ehyps : Q($prop)}
   (hyps : Hyps bi ehyps)
   (ι : Q(IrisGS_gen $hlc Exp $GF))
-  (κ : Q(Wp $prop Exp Val Stuckness))
   (s : Q(Stuckness))
   (E : Q(CoPset))
   (e : Q(Exp))
@@ -215,6 +216,7 @@ public meta def iWpValueHead {u}
   (_hu : QuotedLevelDefEq u 0 := ⟨⟩)
   (_hprop : $prop =Q IProp $GF := ⟨⟩)
   (_hbi : $bi =Q UPred.instBIUPred := ⟨⟩)
+  (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def))
   (_hwp : $κ =Q wp.def := ⟨⟩) :
     ProofModeM (Option Q($ehyps ⊢ Wp.wp $s $E $e $Φ)) := do
   let ~q(ProgramLogic.ToVal.ofVal $v) := e
@@ -239,7 +241,7 @@ public meta def iWpValueHead {u}
 elab "wp_value_head" : tactic =>
   ProofModeM.runTacticWp fun mvar {bi, hyps, ι, s, E, e, Φ, hbi, ..} => do
     have : $bi =Q UPred.instBIUPred := hbi
-    let some pf ← iWpValueHead hyps ι q(wp.def) s E e Φ
+    let some pf ← iWpValueHead hyps ι s E e Φ
       | throwTacticEx `wp_value_head mvar s!"{e} is not a value"
     mvar.assign pf
 
@@ -275,7 +277,6 @@ public meta def iWpFinish {u}
   {ehyps : Q($prop)}
   (hyps : Hyps bi ehyps)
   (ι : Q(IrisGS_gen $hlc Exp $GF))
-  (κ : Q(Wp $prop Exp Val Stuckness))
   (s : Q(Stuckness))
   (E : Q(CoPset))
   (e : Q(Exp))
@@ -284,16 +285,17 @@ public meta def iWpFinish {u}
   (_hu : QuotedLevelDefEq u 0 := ⟨⟩)
   (_hprop : $prop =Q IProp $GF := ⟨⟩)
   (_hbi : $bi =Q UPred.instBIUPred := ⟨⟩)
+  (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def))
   (_hwp : $κ =Q wp.def := ⟨⟩) :
     ProofModeM (Q($ehyps ⊢ Wp.wp $s $E $e $Φ)) := do
   let ⟨e', pfeq⟩ ← iWpExprSimp e
-  let nextPf ← (← iWpValueHead hyps ι q(wp.def) s E e' Φ).getDM
+  let nextPf ← (← iWpValueHead hyps ι s E e' Φ).getDM
       (addBIGoal hyps q(Wp.wp $s $E $e' $Φ))
   return q(tac_wp_expr_simp $nextPf $pfeq)
 
 elab "wp_finish" : tactic =>
   ProofModeM.runTacticWp fun mvar {hyps, ι, s, E, e, Φ, ..} => do
-    let pf ← iWpFinish hyps ι q(wp.def) s E e Φ
+    let pf ← iWpFinish hyps ι s E e Φ
     mvar.assign pf
 
 public theorem tac_wp_bind [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e' : Exp} {Φ : Val → IProp GF}
@@ -343,7 +345,7 @@ public theorem tac_wp_pure [ι : IrisGS_gen hlc Exp GF] {Δ Δ'} {s : Stuckness}
   refine .trans (BI.laterN_mono _ H) ?_
   iintro $ !> -; itrivial
 
-elab "wp_pure " colGt ppSpace focus:hl_exp : tactic =>
+elab "wp_pure " colGt ppSpace focus:hl_exp:10 : tactic =>
   ProofModeM.runTacticWp fun mvar {hyps, ι, s, E, e, Φ, ..} => do
     let focus ← elabTermEnsuringTypeQ (← `(hl($focus))) q(HeapLang.Exp)
     trace[wp_pure] m!"Focusing with {focus}"
@@ -362,7 +364,7 @@ elab "wp_pure " colGt ppSpace focus:hl_exp : tactic =>
 
     let ⟨inner, .up _⟩ ← HeapLang.fillQ K e₂
 
-    let nextPf ← iWpFinish hyps' ι q(wp.def) s E inner Φ
+    let nextPf ← iWpFinish hyps' ι s E inner Φ
 
     let HΦ ← iSolveSidecondition q($φ) (failOnUnsolved := false)
 
@@ -375,5 +377,467 @@ macro "wp_pures" : tactic => `(tactic| repeat wp_pure)
 
 macro "wp_rec" : tactic => `(tactic | (wp_bind _ _; iapply $(mkIdent `wp_rec):ident; rfl; imodintro; wp_finish))
 
+macro "wp_if" : tactic => `(tactic | wp_pure (if _ then _ else _))
+macro "wp_if_true" : tactic => `(tactic | wp_pure (if #true then _ else _))
+macro "wp_if_false" : tactic => `(tactic | wp_pure (if #false then _ else _))
+macro "wp_unop" : tactic => `(tactic | wp_pure (&(Exp.unop _ _)))
+macro "wp_binop" : tactic => `(tactic | wp_pure (&(Exp.binop _ _ _)))
+macro "wp_op" : tactic => `(tactic | first | wp_unop | wp_binop)
+macro "wp_lam" : tactic => `(tactic | wp_rec)
+macro "wp_let" : tactic => `(tactic | (wp_pure (rec _ &(.named _) := _); wp_lam))
+macro "wp_seq" : tactic => `(tactic | (wp_pure (rec _ _ := _); wp_lam))
+macro "wp_proj" : tactic => `(tactic | first | wp_pure (fst(_)) | wp_pure (snd(_)))
+macro "wp_case" : tactic => `(tactic | wp_pure (&(Exp.case _ _ _)))
+macro "wp_inj" : tactic => `(tactic | first | wp_pure (injl(_)) | wp_pure (injr(_)))
+macro "wp_pair" : tactic => `(tactic | wp_pure ((_, _)))
+macro "wp_closure" : tactic => `(tactic | wp_pure (rec &_ &_ := _))
+macro "wp_match" : tactic => `(tactic | (wp_case; wp_closure; wp_lam))
+
+/-! ## Tactic lemmas for the heap tactics -/
+
+/-- Helper lemma for the heap `tac_wp_*` lemmas. -/
+theorem tac_wp_heap_op [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' P P' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e : Exp} {r : Val} {Φ}
+    (hval : ProgramLogic.toVal e = none)
+    (hwp : ▷ P ⊢ WP e @ s ; E {{ v', ⌜v' = r⌝ ∗ P' }})
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ P)
+    (hcont : Δ'' ∗ P' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) r)) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K e) @ s ; E {{ Φ }} := by
+  refine hlater.trans ?_
+  refine .trans ?_ (wp_bind (ProgramLogic.fill K))
+  refine (later_mono hsplit.1).trans ?_
+  refine later_sep.1.trans ?_
+  refine (sep_mono .rfl hwp).trans ?_
+  refine (wp_frame_step_l' hval Std.LawfulSet.subset_refl).trans (wp_mono fun v' => ?_)
+  iintro ⟨HΔ, %hv, HP⟩
+  subst hv
+  iapply hcont
+  iframe
+
+public theorem tac_wp_alloc [ι : HeapLangGS hlc GF] {Δ Δ' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {v : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hcont : ∀ l : Loc, Δ' ∗ (l ↦ some v) ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#l))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(ref(&v))) @ s ; E {{ Φ }} := by
+  refine hlater.trans ?_
+  refine .trans ?_ (wp_bind (ProgramLogic.fill K))
+  refine .trans ?_ (wand_entails (wp_alloc v _))
+  exact later_mono <| forall_intro fun l => wand_intro (hcont l)
+
+public theorem tac_wp_free [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v))
+    (hcont : Δ'' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#()))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(free(#l))) @ s ; E {{ Φ }} :=
+  tac_wp_heap_op rfl wp_free hlater hsplit (sep_elim_left.trans hcont)
+
+public theorem tac_wp_load [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦{q} some v))
+    (hcont : Δ' ⊢ WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) v)) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(!v(#l))) @ s ; E {{ Φ }} := by
+  refine hlater.trans ?_
+  refine .trans ?_ (wp_bind (ProgramLogic.fill K))
+  iapply wand_apply (wand_entails (wp_load _))
+  refine .trans ?_ later_sep.1
+  refine later_mono ?_
+  refine hsplit.1.trans ?_
+  refine .trans sep_comm.mp ?_
+  exact sep_mono .rfl (wand_intro (hsplit.2.trans hcont))
+
+public theorem tac_wp_store [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v))
+    (hcont : Δ'' ∗ (l ↦ some v') ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#()))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(v(#l) ← &v')) @ s ; E {{ Φ }} := by
+  refine hlater.trans ?_
+  refine .trans ?_ (wp_bind (ProgramLogic.fill K))
+  iapply wand_apply (wand_entails (wp_store _))
+  refine .trans ?_ later_sep.1
+  refine later_mono ?_
+  refine hsplit.1.trans ?_
+  refine .trans sep_comm.mp ?_
+  exact sep_mono .rfl (wand_intro hcont)
+
+public theorem tac_wp_xchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v))
+    (hcont : Δ'' ∗ (l ↦ some v') ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) v)) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(xchg(#l, &v'))) @ s ; E {{ Φ }} :=
+  tac_wp_heap_op rfl wp_xchg hlater hsplit hcont
+
+public theorem tac_wp_cmpXchg_fail [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v v1 v2 : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦{q} some v))
+    (hne : v ≠ v1) (hsafe : v.compareSafe v1)
+    (hcont : Δ' ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #false)))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} :=
+  tac_wp_heap_op rfl (wp_cmpXchg_fail rfl rfl hsafe (decide_eq_false hne)) hlater hsplit
+    (hsplit.2.trans hcont)
+
+public theorem tac_wp_cmpXchg_suc [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v1 v2 : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v))
+    (heq : v = v1) (hsafe : v.compareSafe v1)
+    (hcont : Δ'' ∗ (l ↦ some v2) ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #true)))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} :=
+  tac_wp_heap_op rfl (wp_cmpXchg_true rfl rfl hsafe (decide_eq_true heq)) hlater hsplit hcont
+
+public theorem tac_wp_cmpXchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v1 v2 : Val} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some v))
+    (hsafe : v.compareSafe v1)
+    (hsuc : v = v1 → Δ'' ∗ (l ↦ some v2) ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #true)))) @ s ; E {{ Φ }})
+    (hfail : v ≠ v1 → Δ' ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val((&v, #false)))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(cmpXchg(v(#l), v(&v1), v(&v2)))) @ s ; E {{ Φ }} :=
+  if heq : v = v1 then tac_wp_cmpXchg_suc hlater hsplit heq hsafe (hsuc heq)
+  else tac_wp_cmpXchg_fail hlater hsplit heq hsafe (hfail heq)
+
+public theorem tac_wp_faa [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
+    {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {z1 z2 : Int} {Φ}
+    (hlater : Δ ⊢ ▷ Δ')
+    (hsplit : Δ' ⊣⊢ Δ'' ∗ (l ↦ some hl_val(#z1)))
+    (hcont : Δ'' ∗ (l ↦ some hl_val(#(z1 + z2))) ⊢
+      WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#z1))) @ s ; E {{ Φ }}) :
+    Δ ⊢ WP (ProgramLogic.fill K hl(faa(#l, #z2))) @ s ; E {{ Φ }} :=
+  tac_wp_heap_op rfl wp_faa hlater hsplit hcont
+
+-- TODO: port `tac_wp_allocN` once `array` and `wp_allocN` are ported
+
+/-! ## Shared machinery for the heap tactics -/
+
+/-- Epilogue shared by the keep/consume heap tactics: fill the result value `r` back into
+the evaluation context `K` and run `iWpFinish` over the continuation context `hyps`. Returns
+the continuation proof typed against `fill K (Exp.ofVal r)`, so the caller's `assign` matches
+the tac lemma's `hcont`. -/
+meta def finishHeapOp {u} {GF : Q(BundledGFunctors.{0, 0, 0})} {hlc : Q(HasLC)}
+    {prop : Q(Type u)} {bi : Q(BI $prop)} {ehyps : Q($prop)}
+    (hyps : Hyps bi ehyps) (ι : Q(IrisGS_gen $hlc Exp $GF))
+    (s : Q(Stuckness)) (E : Q(CoPset)) (K : Q(List ECtxItem)) (r : Q(Val)) (Φ : Q(Val → $prop))
+    (_hu : QuotedLevelDefEq u 0 := ⟨⟩) (_hprop : $prop =Q IProp $GF := ⟨⟩)
+    (κ : Q(Wp $prop Exp Val Stuckness) := q(wp.def)) (_hwp : $κ =Q wp.def := ⟨⟩) :
+    ProofModeM Q($ehyps ⊢ Wp.wp (self := $κ) $s $E (ProgramLogic.fill $K (Exp.ofVal $r)) $Φ) := do
+  let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal $r)
+  iWpFinish hyps ι s E inner Φ (κ := κ)
+
+/-- The points-to hypothesis located by `lookupPointsTo` for location `l`
+in the (later-stripped) context `eΔ'`, together with the pruned context `eΔ''`/`hyps''` and
+the splitting proof `pfSplit`, whose type is already recast to the `pointsTo` shape that the
+`tac_wp_*` lemmas expect. -/
+structure PointsToLookup {u : Level} {GF : Q(BundledGFunctors.{0, 0, 0})}
+    {hlc : Q(HasLC)} (hgs : Q(HeapLangGS $hlc $GF)) {prop : Q(Type u)} (bi : Q(BI $prop))
+    (eΔ' : Q($prop)) (l : Q(Loc)) (dq : Q(DFrac)) (hu : QuotedLevelDefEq u 0)
+    (hprop : $prop =Q IProp $GF) where
+  /-- The value stored at `l`. -/
+  v : Q(Val)
+  /-- The user-facing name of the found hypothesis. -/
+  name : Name
+  /-- The `IVarId` of the found hypothesis. -/
+  vid : IVarId
+  /-- The context with the points-to hypothesis removed. -/
+  eΔ'' : Q($prop)
+  hyps'' : @Hyps u prop bi eΔ''
+  /-- The split certificate, recast to the shape the `tac_wp_*` lemmas expect. -/
+  pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗ pointsTo $l $dq (some $v))
+
+/-- Locate and remove a spatial hypothesis `l ↦{dq} some v`.
+Reading operations pass a fresh metavariable, which the lookup assigns to whatever
+fraction is found and the lemmas' `↦{q}` implicit then picks up.
+Throws if no matching hypothesis exists. -/
+meta def lookupPointsTo {u} {GF : Q(BundledGFunctors.{0, 0, 0})} {hlc : Q(HasLC)}
+    {prop : Q(Type u)} {bi : Q(BI $prop)} {eΔ' : Q($prop)}
+    (tacName : Name) (mvar : MVarId) (hgs : Q(HeapLangGS $hlc $GF))
+    (hyps' : Hyps bi eΔ') (l : Q(Loc)) (dq : Q(DFrac))
+    (hu : QuotedLevelDefEq u 0 := ⟨⟩)
+    (hprop : $prop =Q IProp $GF := ⟨⟩) :
+    ProofModeM (@PointsToLookup u GF hlc hgs prop bi eΔ' l dq hu hprop) := do
+  let some ⟨⟨v, name, vid⟩, eΔ'', hyps'', _, _, _, _, pf⟩ ←
+      hyps'.removeG false fun name vid p ty => do
+        -- ignore intuitionistic hyps
+        if isTrue p then return none
+        have ty : Q(IProp $GF) := ty
+        -- destructure ty to get the location l', fraction dq' and stored value v
+        let ~q(pointsTo $l' $dq' (some $v)) := ty | return none
+        unless ← isDefEq l' l do return none
+        -- a literal `dq` rejects other fractions; a metavariable records the one found
+        unless ← isDefEq dq' dq do return none
+        return some ((v : Q(Val)), name, vid)
+    | throwTacticEx tacName mvar (if dq.isMVar
+        then m!"cannot find a points-to hypothesis for location {l}"
+        else m!"cannot find a full-ownership points-to hypothesis for location {l}")
+  trace[wp_heap.lookup] "found {name} : pointsTo {l} ({dq}) (some {v})"
+  have pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗ pointsTo $l $dq (some $v)) := pf
+  return { v, name, vid, eΔ'', hyps'', pfSplit }
+
+/-- The goal handed to a heap tactic by `ProofModeM.runTacticHeapWp`: `WpGoal` fields,
+plus the `HeapLangGS` instance `hgs` extracted from the goal's `IrisGS_gen`, and the
+context `hyps'`/`eΔ'` after stripping the WP's step modality, with `pfLater` witnessing
+the strip. -/
+structure HeapWpGoal extends WpGoal where
+  hgs : Q(HeapLangGS $hlc $GF)
+  {eΔ' : Q($prop)}
+  hyps' : @Hyps u prop bi eΔ'
+  pfLater : Q($ehyps ⊢ (modality_laterN 1).M $eΔ')
+  hι : $ι =Q @HeapLang $hlc $GF $hgs
+
+/-- Shared prologue for the heap tactics: run the tactic on a WP goal, check that it is a
+HeapLang WP (from the `HeapLangGS` instance), and strip the WP's step modality
+off the hypotheses. -/
+meta def runTacticHeapWp {α} (tacName : Name)
+    (k : MVarId → HeapWpGoal → ProofModeM α) : TacticM α := do
+  -- Rocq parity: every heap tactic first normalizes pure redexes
+  evalTactic (← `(tactic| wp_pures))
+  ProofModeM.runTacticWp fun mvar {hyps, GF, hlc, ι, s, E, e, Φ, hu, hprop, hbi, ..} => do
+    have ιQ : Q(IrisGS_gen $hlc Exp $GF) := ι
+    let ~q(@HeapLang _ _ $hgs) := ιQ
+      | throwTacticEx tacName mvar "the goal is not a HeapLang WP"
+    trace[wp_heap] "{tacName}: e = {e}"
+    -- currently specialized to later (no twp exists yet)
+    let ⟨_, hyps', pfLater⟩ ← iModAction hyps q(modality_laterN 1)
+    k mvar { hyps, ι, s, E, e, Φ, hu, hprop, hbi, hgs, hyps', pfLater, hι := ⟨⟩ }
+
+/-! ## The heap tactics -/
+
+elab "wp_load" : tactic =>
+  runTacticHeapWp `wp_load fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := l, K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.load (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure
+        return l
+      | throwTacticEx `wp_load mvar "cannot find a `load` redex"
+    trace[wp_heap.redex] "load {l}; K = {K}"
+
+    -- find `l ↦{dq} some v` in the spatial context and extract `dq`
+    let dq ← mkFreshExprMVarQ q(DFrac)
+    let ⟨v, _, _, _, _, pfSplit⟩ ← lookupPointsTo `wp_load mvar hgs hyps' l dq
+
+    -- fill the loaded value back into `K` and finish the continuation
+    -- (over `hyps'`: the points-to hypothesis is kept)
+    let pfCont ← finishHeapOp hyps' ι s E K v Φ
+
+    mvar.assign q(tac_wp_load (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+
+elab "wp_store" : tactic =>
+  runTacticHeapWp `wp_store fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, v'), K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.store (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure
+        return (l, v')
+      | throwTacticEx `wp_store mvar "cannot find a `store` redex"
+    trace[wp_heap.redex] "store {l} ← {v'}; K = {K}"
+
+    -- find and remove `l ↦ some v` (stores need full ownership)
+    let ⟨_, name, vid, _, hyps'', pfSplit⟩ ←
+      lookupPointsTo `wp_store mvar hgs hyps' l q(DFrac.own 1)
+
+    let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
+
+    let pfCont ← finishHeapOp hyps''' ι s E K q(hl_val(#())) Φ
+
+    mvar.assign q(tac_wp_store (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+
+elab "wp_xchg" : tactic =>
+  runTacticHeapWp `wp_xchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, v'), K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.xchg (Exp.ofVal (Val.lit (BaseLit.loc $l))) (Exp.ofVal $v')) := e' | failure
+        return (l, v')
+      | throwTacticEx `wp_xchg mvar "cannot find an `xchg` redex"
+    trace[wp_heap.redex] "xchg {l} ← {v'}; K = {K}"
+
+    -- find and remove `l ↦ some v` (xchg writes, so it needs full ownership)
+    let ⟨v, name, vid, _, hyps'', pfSplit⟩ ← lookupPointsTo `wp_xchg mvar hgs hyps' l q(DFrac.own 1)
+
+    let hyps''' := hyps''.add bi name vid q(false) q(pointsTo $l (DFrac.own 1) (some $v'))
+
+    let pfCont ← finishHeapOp hyps''' ι s E K v Φ
+
+    mvar.assign q(tac_wp_xchg (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+
+elab "wp_faa" : tactic =>
+  runTacticHeapWp `wp_faa fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, z2), K, ..} ← findECtx e fun e' => do
+        -- faa is only defined on integers
+        let ~q(Exp.faa (Exp.ofVal (Val.lit (BaseLit.loc $l)))
+            (Exp.ofVal (Val.lit (BaseLit.int $z2)))) := e' | failure
+        return (l, z2)
+      | throwTacticEx `wp_faa mvar "cannot find a `faa` redex"
+    trace[wp_heap.redex] "faa {l} += {z2}; K = {K}"
+
+    -- find and remove `l ↦ some v` (faa writes, so it needs full ownership)
+    let ⟨v, name, vid, eΔ'', hyps'', pfSplit⟩ ←
+      lookupPointsTo `wp_faa mvar hgs hyps' l q(DFrac.own 1)
+
+    -- check that the points-to value is an integer (FAA requirement)
+    let ~q(Val.lit (BaseLit.int $z1)) := v
+      | throwTacticEx `wp_faa mvar
+          m!"the points-to hypothesis for location {l} does not store an integer"
+    have pfSplit : Q($eΔ' ⊣⊢ $eΔ'' ∗
+      pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int $z1)))) := pfSplit
+
+    let hyps''' := hyps''.add bi name vid q(false)
+      q(pointsTo $l (DFrac.own 1) (some (Val.lit (BaseLit.int ($z1 + $z2)))))
+
+    let pfCont ← finishHeapOp hyps''' ι s E K q(Val.lit (BaseLit.int $z1)) Φ
+
+    mvar.assign q(tac_wp_faa (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+
+elab "wp_cmpxchg_suc" : tactic =>
+  runTacticHeapWp `wp_cmpxchg_suc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l)))
+            (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure
+        return (l, v1, v2)
+      | throwTacticEx `wp_cmpxchg_suc mvar "cannot find a `cmpXchg` redex"
+    trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}"
+
+    -- find and remove `l ↦ some v` (a successful cmpXchg writes, so full ownership)
+    let ⟨v, name, vid, _, hyps'', pfSplit⟩ ←
+      lookupPointsTo `wp_cmpxchg_suc mvar hgs hyps' l q(DFrac.own 1)
+
+    -- check safety, don't throw hard error to match Rocq behavior
+    let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false)
+
+    -- check equality, don't throw hard error to match Rocq behavior
+    let pfEq ← iSolveSidecondition q($v = $v1) (failOnUnsolved := false)
+
+    let hyps''' := hyps''.add bi name vid q(false)
+      q(pointsTo $l (DFrac.own 1) (some $v2))
+
+    let pfCont ← finishHeapOp hyps''' ι s E K
+      q(Val.pair $v (Val.lit (BaseLit.bool true))) Φ
+
+    mvar.assign
+      q(tac_wp_cmpXchg_suc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfEq $pfSafe $pfCont)
+
+elab "wp_cmpxchg_fail" : tactic =>
+  runTacticHeapWp `wp_cmpxchg_fail fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l)))
+            (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure
+        return (l, v1, v2)
+      | throwTacticEx `wp_cmpxchg_fail mvar "cannot find a `cmpXchg` redex"
+    trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}"
+
+    -- any fraction suffices for a failing compare (the points-to is only read)
+    let dq ← mkFreshExprMVarQ q(DFrac)
+    let ⟨v, _, _, _, _, pfSplit⟩ ← lookupPointsTo `wp_cmpxchg_fail mvar hgs hyps' l dq
+
+    -- check safety, don't throw hard error to match Rocq behavior
+    let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false)
+
+    -- check equality, don't throw hard error to match Rocq behavior
+    let pfNeq ← iSolveSidecondition q($v ≠ $v1) (failOnUnsolved := false)
+
+    let pfCont ← finishHeapOp hyps' ι s E K
+      q(Val.pair $v (Val.lit (BaseLit.bool false))) Φ
+
+    mvar.assign
+      q(tac_wp_cmpXchg_fail (ι := $hgs) (Δ' := $eΔ') (v2 := $v2)
+        $pfLater $pfSplit $pfNeq $pfSafe $pfCont)
+
+elab "wp_cmpxchg" " as " h1:binderIdent " | " h2:binderIdent : tactic =>
+  runTacticHeapWp `wp_cmpxchg fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := (l, v1, v2), K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.cmpXchg (Exp.ofVal (Val.lit (BaseLit.loc $l)))
+            (Exp.ofVal $v1) (Exp.ofVal $v2)) := e' | failure
+        return (l, v1, v2)
+      | throwTacticEx `wp_cmpxchg mvar "cannot find a `cmpXchg` redex"
+    trace[wp_heap.redex] "cmpXchg {l}: {v1} → {v2}; K = {K}"
+
+    -- find and remove `l ↦ some v` (the success branch writes, so full ownership)
+    let ⟨v, name, vid, eΔ'', hyps'', pfSplit⟩ ←
+      lookupPointsTo `wp_cmpxchg mvar hgs hyps' l q(DFrac.own 1)
+
+    let hypsSuc := hyps''.add bi name vid q(false)
+      q(pointsTo $l (DFrac.own 1) (some $v2))
+
+    -- check safety, don't throw hard error to match Rocq behavior
+    let pfSafe ← iSolveSidecondition q(($v).compareSafe $v1 = true) (failOnUnsolved := false)
+
+    let (sucName, _) ← getFreshName h1
+    let pfSuc : Q($v = $v1 → ($eΔ'' ∗ pointsTo $l (DFrac.own 1) (some $v2) ⊢
+      Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp)
+      (Val.pair $v (Val.lit (BaseLit.bool true))))) $Φ)) ←
+        Qq.withLocalDeclDQ sucName q($v = $v1) fun _h => do
+          let ⟨innerSuc, .up _⟩ ← HeapLang.fillQ K
+            q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool true))))
+          let pf ← iWpFinish hypsSuc ι s E innerSuc Φ
+          mkLambdaFVars #[_h] pf
+
+    let (failName, _) ← getFreshName h2
+    let pfFail : Q($v ≠ $v1 → $eΔ' ⊢
+      Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp)
+      (Val.pair $v (Val.lit (BaseLit.bool false))))) $Φ) ←
+        Qq.withLocalDeclDQ failName q($v ≠ $v1) fun _h => do
+          let ⟨innerFail, .up _⟩ ← HeapLang.fillQ K
+            q(Exp.ofVal (Val.pair $v (Val.lit (BaseLit.bool false))))
+          let pf ← iWpFinish hyps' ι s E innerFail Φ
+          mkLambdaFVars #[_h] pf
+
+    mvar.assign
+      q(tac_wp_cmpXchg (ι := $hgs) (Δ' := $eΔ') (v2 := $v2)
+        $pfLater $pfSplit $pfSafe $pfSuc $pfFail)
+
+elab "wp_free" : tactic =>
+  runTacticHeapWp `wp_free fun mvar {ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := l, K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.free (Exp.ofVal (Val.lit (BaseLit.loc $l)))) := e' | failure
+        return l
+      | throwTacticEx `wp_free mvar "cannot find a `free` redex"
+    trace[wp_heap.redex] "free {l}; K = {K}"
+
+    -- find and remove `l ↦ some v` (freeing needs full ownership); the continuation
+    -- runs over the pruned context `hyps''` since the points-to is consumed
+    let ⟨_, _, _, _, hyps'', pfSplit⟩ ← lookupPointsTo `wp_free mvar hgs hyps' l q(DFrac.own 1)
+
+    let pfCont ← finishHeapOp hyps'' ι s E K q(hl_val(#())) Φ
+
+    mvar.assign q(tac_wp_free (ι := $hgs) (Δ' := $eΔ') $pfLater $pfSplit $pfCont)
+
+
+elab "wp_alloc" ppSpace loc:binderIdent " as " hyp:binderIdent : tactic =>
+  runTacticHeapWp `wp_alloc fun mvar {bi, ι, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do
+    let some {result := v, K, ..} ← findECtx e fun e' => do
+        let ~q(Exp.allocN (Exp.ofVal (Val.lit (BaseLit.int 1)))
+            (Exp.ofVal $v)) := e' | failure
+        return v
+      | throwTacticEx `wp_alloc mvar "cannot find a `ref` alloc"
+    trace[wp_heap.redex] "ref {v}; K = {K}"
+
+    -- get location name from tactic call
+    let (locName, _) ← getFreshName loc
+
+    let pfCont : Q(∀ l : Loc, $eΔ' ∗ pointsTo l (DFrac.own 1) (some $v) ⊢
+        Wp.wp $s $E (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ←
+      Qq.withLocalDeclDQ locName q(Loc) fun l => do
+        let ⟨_, hyps''⟩ ← hyps'.addWithInfo bi hyp q(false)
+          q(pointsTo $l (DFrac.own 1) (some $v))
+
+        let ⟨inner, .up _⟩ ← HeapLang.fillQ K q(Exp.ofVal (Val.lit (BaseLit.loc $l)))
+        let pf ← iWpFinish hyps'' ι s E inner Φ
+        mkLambdaFVars #[l] pf
+
+    mvar.assign q(tac_wp_alloc (ι := $hgs) (Δ' := $eΔ') $pfLater $pfCont)
+
+macro "wp_alloc" ppSpace loc:binderIdent : tactic => `(tactic| wp_alloc $loc as _)
+
+-- Register the trace classes emitted by the tactics above; enables
+-- `set_option trace.wp_bind true` (and analogously for the others).
 initialize registerTraceClass `wp_bind
 initialize registerTraceClass `wp_pure
+initialize registerTraceClass `wp_heap
+initialize registerTraceClass `wp_heap.redex (inherited := true)
+initialize registerTraceClass `wp_heap.lookup (inherited := true)
diff --git a/Iris/Iris/Tests/HeapLang.lean b/Iris/Iris/Tests/HeapLang.lean
index af432f07a..2acd7f17e 100644
--- a/Iris/Iris/Tests/HeapLang.lean
+++ b/Iris/Iris/Tests/HeapLang.lean
@@ -2,4 +2,5 @@ module
 
 public import Iris.Tests.HeapLang.Notation
 public import Iris.Tests.HeapLang.WeakestPre
+public import Iris.Tests.HeapLang.HeapTactics
 public import Iris.Tests.HeapLang.Linter
diff --git a/Iris/Iris/Tests/HeapLang/HeapTactics.lean b/Iris/Iris/Tests/HeapLang/HeapTactics.lean
new file mode 100644
index 000000000..417057992
--- /dev/null
+++ b/Iris/Iris/Tests/HeapLang/HeapTactics.lean
@@ -0,0 +1,453 @@
+/-
+Copyright (c) 2026 Klaus Kraßnitzer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Klaus Kraßnitzer
+-/
+module
+
+public import Iris.BI
+public import Iris.Instances
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.ProofMode
+public import Iris.HeapLang.Instances
+public import Iris.ProgramLogic.WeakestPre
+
+/-! Tests for the heap-operation tactics (`wp_load`, ...). Unlike the tests in
+`Tests.HeapLang.WeakestPre`, these need the `IrisGS_gen` instance to be the one
+derived from `HeapLangGS`, so no generic `IrisGS_gen` variable is in scope. -/
+
+namespace Iris.HeapLang
+
+variable {hlc} {GF : BundledGFunctors} [ι : HeapLangGS hlc GF]
+variable {s : Stuckness} {E : CoPset} {Φ : Val → IProp GF}
+
+section wp_load
+
+example {l : Loc} {v : Val} :
+    (l ↦ some v) ∗ ((l ↦ some v) -∗ Φ v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by
+  iintro ⟨Hpt, HΦ⟩
+  wp_load
+  imodintro
+  iapply HΦ $$ Hpt
+
+-- with a ▷ on the points-to and the load inside an evaluation context
+example {l l' : Loc} :
+    ▷ (l ↦ some hl_val(#2)) ∗ ▷ (l' ↦ some hl_val(#3)) ⊢
+      WP hl(#1 + !v(#l)) @ s ; E {{ w, ⌜w = hl_val(#3)⌝ ∗ (l ↦ some hl_val(#2)) }} := by
+  iintro ⟨Hpt, Hpt'⟩
+  wp_load
+  wp_binop
+  imodintro
+  iframe Hpt
+  ipureintro
+  rfl
+
+-- `wp_load` accepts *fractional* ownership (where store/faa/free would reject)
+example {l : Loc} {dq : DFrac} {v : Val} :
+    (l ↦{dq} some v) ∗ ((l ↦{dq} some v) -∗ Φ v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by
+  iintro ⟨Hl, HΦ⟩
+  wp_load
+  imodintro
+  iapply HΦ $$ Hl
+
+/--
+error: Tactic `wp_load` failed: cannot find a points-to hypothesis for location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l l' : Loc
+v : Val
+⊢
+  ∗Hpt : l' ↦ some v
+  ⊢ WP hl(!#l) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l l' : Loc} {v : Val} :
+    (l' ↦ some v) ⊢ WP hl(!v(#l)) @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_load
+
+/--
+error: Tactic `wp_load` failed: cannot find a `load` redex
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+v v' : Val
+⊢
+  ∗Hpt : l ↦ some v
+  ⊢ WP hl(#l ← v(&v')) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {v v' : Val} :
+    (l ↦ some v) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_load
+
+end wp_load
+
+section wp_store
+
+example {l : Loc} {v v' : Val} :
+    (l ↦ some v) ∗ ((l ↦ some v') -∗ Φ hl_val(#())) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by
+  iintro ⟨Hpt, HΦ⟩
+  wp_store
+  imodintro
+  iapply HΦ $$ Hpt
+
+-- `wp_store` must pick the `l` points-to and leave the `l'` one untouched
+example {l l' : Loc} {v v' w : Val} :
+    (l ↦ some v) ∗ (l' ↦ some w) ⊢
+      WP hl(v(#l) ← &v') @ s ; E {{ _r, (l ↦ some v') ∗ (l' ↦ some w) }} := by
+  iintro ⟨Hl, Hl'⟩
+  wp_store
+  imodintro
+  iframe
+
+example {l : Loc} {v v' v'' : Val} :
+    (l ↦ some v) ⊢
+      WP hl(if #true then (v(#l) ← &v') else (v(#l) ← &v'')) @ s ; E
+        {{ _r, l ↦ some v' }} := by
+  iintro Hpt
+  wp_store
+  imodintro
+  iframe
+
+/--
+error: Tactic `wp_store` failed: cannot find a full-ownership points-to hypothesis for location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+dq : DFrac
+v v' : Val
+⊢
+  ∗Hpt : l ↦{dq} some v
+  ⊢ WP hl(#l ← v(&v')) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {dq : DFrac} {v v' : Val} :
+    (l ↦{dq} some v) ⊢ WP hl(v(#l) ← &v') @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_store
+
+end wp_store
+
+section wp_faa
+
+example {l : Loc} {z1 z2 : Int} :
+    (l ↦ some hl_val(#z1)) ∗ ((l ↦ some hl_val(#(z1 + z2))) -∗ Φ hl_val(#z1)) ⊢
+      WP hl(faa(#l, #z2)) @ s ; E {{ Φ }} := by
+  iintro ⟨Hpt, HΦ⟩
+  wp_faa
+  imodintro
+  iapply HΦ $$ Hpt
+
+-- `wp_faa` buried in an evaluation context (`#1 + •`), with a `▷` on the points-to
+example {l : Loc} {z : Int} :
+    ▷ (l ↦ some hl_val(#z)) ⊢
+      WP hl(#1 + faa(#l, #2)) @ s ; E
+        {{ w, ⌜w = hl_val(#((1 : Int) + z))⌝ ∗ l ↦ some hl_val(#(z + (2 : Int))) }} := by
+  iintro Hl
+  wp_faa
+  wp_binop
+  imodintro
+  iframe
+  ipureintro
+  rfl
+
+-- `wp_faa` failing: writes need full ownership, fractional is rejected
+/--
+error: Tactic `wp_faa` failed: cannot find a full-ownership points-to hypothesis for location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+dq : DFrac
+z : Int
+⊢
+  ∗Hpt : l ↦{dq} some hl_val(#z)
+  ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {dq : DFrac} {z : Int} :
+    (l ↦{dq} some hl_val(#z)) ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_faa
+
+-- `wp_faa` failing: the stored value must be an integer literal
+/--
+error: Tactic `wp_faa` failed: the points-to hypothesis for location l does not store an integer
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+v : Val
+⊢
+  ∗Hpt : l ↦ some v
+  ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {v : Val} :
+    (l ↦ some v) ⊢ WP hl(faa(#l, #1)) @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_faa
+
+end wp_faa
+
+section wp_xchg
+
+-- `xchg` returns the old value and stores the new one
+example {l : Loc} {v v' : Val} :
+    (l ↦ some v) ∗ ((l ↦ some v') -∗ Φ v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ Φ }} := by
+  iintro ⟨Hpt, HΦ⟩
+  wp_xchg
+  imodintro
+  iapply HΦ $$ Hpt
+
+-- `wp_xchg` under a `▷`, returning the old value
+example {l : Loc} {v v' : Val} :
+    ▷ (l ↦ some v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ w, ⌜w = v⌝ ∗ l ↦ some v' }} := by
+  iintro Hl
+  wp_xchg
+  imodintro
+  iframe
+  ipureintro
+  rfl
+
+-- `wp_xchg` failing: writes need full ownership, fractional is rejected
+/--
+error: Tactic `wp_xchg` failed: cannot find a full-ownership points-to hypothesis for location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+dq : DFrac
+v v' : Val
+⊢
+  ∗Hpt : l ↦{dq} some v
+  ⊢ WP hl(xchg(#l, v(&v'))) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {dq : DFrac} {v v' : Val} :
+    (l ↦{dq} some v) ⊢ WP hl(xchg(#l, &v')) @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_xchg
+
+end wp_xchg
+
+section wp_free
+
+-- `free` consumes the points-to (its resource is gone in the continuation)
+example {l : Loc} {v : Val} :
+    (l ↦ some v) ∗ Φ hl_val(#()) ⊢ WP hl(free(#l)) @ s ; E {{ Φ }} := by
+  iintro ⟨Hpt, HΦ⟩
+  wp_free
+  imodintro
+  iexact HΦ
+
+-- `wp_free` on a `▷`-wrapped points-to, among several; the survivor stays
+example {l l' : Loc} {v w : Val} :
+    ▷ (l ↦ some v) ∗ (l' ↦ some w) ⊢
+      WP hl(free(#l)) @ s ; E {{ _r, l' ↦ some w }} := by
+  iintro ⟨Hl, Hl'⟩
+  wp_free
+  imodintro
+  iframe
+
+-- `wp_free` failing: deallocation needs full ownership, fractional is rejected
+/--
+error: Tactic `wp_free` failed: cannot find a full-ownership points-to hypothesis for location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+dq : DFrac
+v : Val
+⊢
+  ∗Hpt : l ↦{dq} some v
+  ⊢ WP hl(free(#l)) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {dq : DFrac} {v : Val} :
+    (l ↦{dq} some v) ⊢ WP hl(free(#l)) @ s ; E {{ Φ }} := by
+  iintro Hpt
+  wp_free
+
+end wp_free
+
+section wp_alloc
+
+-- `alloc` produces a fresh `l ↦ some v`; `wp_alloc l as Hl` names both
+example {v : Val} :
+    ⊢ WP hl(ref(&v)) @ s ; E {{ w, ∃ l : Loc, ⌜w = hl_val(#l)⌝ ∗ l ↦ some v }} := by
+  wp_alloc l as Hl
+  imodintro
+  iexists l
+  isplit
+  · ipureintro; rfl
+  · iexact Hl
+
+-- anonymous variant: `wp_alloc l` auto-names the points-to; `iframe` picks it up
+example {v : Val} :
+    ⊢ WP hl(ref(&v)) @ s ; E {{ w, ∃ l : Loc, ⌜w = hl_val(#l)⌝ ∗ l ↦ some v }} := by
+  wp_alloc l
+  imodintro
+  iexists l
+  iframe
+  ipureintro
+  rfl
+
+end wp_alloc
+
+section wp_cmpxchg_suc
+
+-- concrete equal values: the `v = v1` and `compareSafe` side conditions are
+-- discharged automatically, the slot is updated to `v2`, result is `(v, #true)`
+example {l : Loc} {v2 : Val} :
+    ▷ (l ↦ some hl_val(#1)) ⊢
+      WP hl(cmpXchg(v(#l), v(#1), &v2)) @ s ; E
+        {{ w, ⌜w = hl_val((#1, #true))⌝ ∗ l ↦ some v2 }} := by
+  iintro Hl
+  wp_cmpxchg_suc
+  imodintro
+  iframe
+  ipureintro
+  rfl
+
+-- `wp_cmpxchg_suc` failing: a successful CAS writes, so fractional is rejected
+/--
+error: Tactic `wp_cmpxchg_suc` failed: cannot find a full-ownership points-to hypothesis for
+location l
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ : Val → IProp GF
+l : Loc
+dq : DFrac
+v2 : Val
+⊢
+  ∗Hl : l ↦{dq} some hl_val(#1)
+  ⊢ WP hl(cmpXchg(#l, #1, v(&v2))) @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {l : Loc} {dq : DFrac} {v2 : Val} :
+    (l ↦{dq} some hl_val(#1)) ⊢
+      WP hl(cmpXchg(v(#l), v(#1), &v2)) @ s ; E {{ Φ }} := by
+  iintro Hl
+  wp_cmpxchg_suc
+
+end wp_cmpxchg_suc
+
+section wp_cmpxchg_fail
+
+-- distinct concrete values with *fractional* ownership: the points-to is only
+-- read and kept at its fraction; result is `(v, #false)`. Both side conditions
+-- (`≠` and `compareSafe`) are discharged automatically for concrete values.
+example {l : Loc} {dq : DFrac} {v2 : Val} :
+    ▷ (l ↦{dq} some hl_val(#1)) ⊢
+      WP hl(cmpXchg(v(#l), v(#2), &v2)) @ s ; E
+        {{ w, ⌜w = hl_val((#1, #false))⌝ ∗ l ↦{dq} some hl_val(#1) }} := by
+  iintro Hl
+  wp_cmpxchg_fail
+  imodintro
+  iframe
+  ipureintro
+  rfl
+
+end wp_cmpxchg_fail
+
+section wp_cmpxchg
+
+-- symbolic compare value: both continuations appear as goals, with the
+-- (dis)equality introduced into the Lean context under the given names;
+-- `compareSafe` is discharged since the stored value is an unboxed literal
+example {l : Loc} {v1 : Val} :
+    ▷ (l ↦ some hl_val(#1)) ⊢
+      WP hl(cmpXchg(v(#l), &v1, v(#7))) @ s ; E
+        {{ w, (⌜w = hl_val((#1, #true))⌝ ∗ l ↦ some hl_val(#7)) ∨
+              (⌜w = hl_val((#1, #false))⌝ ∗ l ↦ some hl_val(#1)) }} := by
+  iintro Hl
+  wp_cmpxchg as Heq | Hne
+  · imodintro
+    ileft
+    iframe
+    ipureintro
+    rfl
+  · imodintro
+    iright
+    iframe
+    ipureintro
+    rfl
+
+end wp_cmpxchg
+
+section goal_shape
+
+-- heap tactics reject WPs over a non-HeapLang `IrisGS_gen` instance
+/--
+error: Tactic `wp_load` failed: the goal is not a HeapLang WP
+
+hlc : HasLC
+GF : BundledGFunctors
+ι : HeapLangGS hlc GF
+s : Stuckness
+E : CoPset
+Φ✝ : Val → IProp GF
+hlc' : HasLC
+GF' : BundledGFunctors
+inst✝ : IrisGS_gen hlc' Exp GF'
+e : Exp
+Φ : Val → IProp GF'
+⊢
+  ⊢ WP e @ s ; E {{ Φ }}
+-/
+#guard_msgs (whitespace := lax) in
+example {hlc'} {GF' : BundledGFunctors} [IrisGS_gen hlc' Exp GF']
+    {e : Exp} {Φ : Val → IProp GF'} :
+    ⊢ WP e @ s ; E {{ Φ }} := by
+  wp_load
+
+-- heap tactics reject goals that are not WPs at all
+/--
+error: The goal P must be a WP
+-/
+#guard_msgs (whitespace := lax) in
+example {P : IProp GF} : P ⊢ P := by
+  iintro HP
+  wp_load
+
+end goal_shape
+
+end Iris.HeapLang
diff --git a/Iris/Iris/Tests/HeapLang/WeakestPre.lean b/Iris/Iris/Tests/HeapLang/WeakestPre.lean
index ffd2e2ef0..62477bfb5 100644
--- a/Iris/Iris/Tests/HeapLang/WeakestPre.lean
+++ b/Iris/Iris/Tests/HeapLang/WeakestPre.lean
@@ -1,6 +1,7 @@
 /-
-Copyright (c) 2026 Fernando Leal. All rights reserved.
+Copyright (c) 2026 Fernando Leal, Klaus Kraßnitzer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fernando Leal, Klaus Kraßnitzer
 -/
 module
 
@@ -224,6 +225,568 @@ n : Int
 example (n : Int) : ⊢@{IProp GF} WP hl((#1 * #2 <<< #3 ≤ #n + (#1 &&& #2 ^^^ #3)) = #true) {{ v, ⌜v = hl_val(#true)⌝ }} := by
   wp_pures
 
+end wp_pure
 
+section pure_tactics
 
-end wp_pure
+variable {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+section wp_lam
+
+def addOne : Val := hl_val% λ x, x + #1
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(v(λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_lam
+
+/--
+error: iapply: cannot apply WP hl(v(&?_) v(&?_)) @ ?_ ; ?_ {{ ?_ }} to WP hl(let x := #1; (x + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl((λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_lam
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(&addOne #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_lam
+
+/--
+error: iapply: cannot apply WP hl(v(&?_) v(&?_)) @ ?_ ; ?_ {{ ?_ }} to WP hl(v(&addOne) (#1 + #1)) {{ v, ⌜v = hl_val(#3)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(&addOne (#1 + #1)) {{ v, ⌜v = hl_val(#3)⌝ }} := by
+  wp_lam
+
+end wp_lam
+
+section wp_let
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_let
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(let x := #1; x + #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_let
+
+end wp_let
+
+section wp_seq
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_seq
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(let x := #1; x) {{ v, ⌜v = hl_val(#1)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(let x := #1; x) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_seq
+
+end wp_seq
+
+section wp_closure
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1 + #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_closure
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((v(λ x, (x + #1))) #1) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl((λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_closure
+
+end wp_closure
+
+section wp_if
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_if
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #2)) {{ v, ⌜v = hl_val(#3)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by
+  wp_if
+
+end wp_if
+
+section wp_if_true
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_if_true
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_if_true
+
+end wp_if_true
+
+section wp_if_false
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_if_false
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_if_false
+
+end wp_if_false
+
+section wp_proj
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(fst(v((#1, #2)))) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_proj
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }} := by
+  wp_proj
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(snd(v((#1, #2)))) {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_proj
+
+end wp_proj
+
+section wp_inj
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(injr((#1 + #1))) {{ v, ⌜v = hl_val(injr(#2))⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(injr(#1 + #1)) {{ v, ⌜v = hl_val(injr(#2))⌝ }} := by
+  wp_inj
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(injr(#1)) = hl_val(injr(#1))⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(injr(#1)) {{ v, ⌜v = hl_val(injr(#1))⌝ }} := by
+  wp_inj
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(injl(#1)) = hl_val(injl(#1))⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(injl(#1)) {{ v, ⌜v = hl_val(injl(#1))⌝ }} := by
+  wp_inj
+
+end wp_inj
+
+section wp_pair
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val((#1, #2)) = hl_val((#1, #2))⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }} := by
+  wp_pair
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(((#1 + #1), #2)) {{ v, ⌜v = hl_val((#2, #2))⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl((#1 + #1, #2)) {{ v, ⌜v = hl_val((#2, #2))⌝ }} := by
+  wp_pair
+
+end wp_pair
+
+section wp_unop
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #2)) {{ v, ⌜v = hl_val(#3)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by
+  wp_unop
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#!true) = hl_val(#false)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by
+  wp_unop
+
+end wp_unop
+
+section wp_binop
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#(1 + 2)) = hl_val(#3)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by
+  wp_binop
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((~#true)) {{ v, ⌜v = hl_val(#false)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by
+  wp_binop
+
+end wp_binop
+
+section wp_op
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#!true) = hl_val(#false)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by
+  wp_op
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_op
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ |={⊤}=> ⌜hl_val(#(1 + 2)) = hl_val(#3)⌝
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by
+  wp_op
+
+end wp_op
+
+section wp_case
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(match injl(#1) with | injl(x) => (x + #1) | injr(y) => y) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF}
+    WP hl(match injl(#1) with | injl(x) => x + #1 | injr(y) => y)
+      {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_case
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(let x := #1; (x + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF}
+    WP hl(match v(injl(#1)) with | injl(x) => x + #1 | injr(y) => y)
+      {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_case
+
+end wp_case
+
+section wp_match
+
+/--
+error: unsolved goals
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF}
+    WP hl(match v(injl(#1)) with | injl(x) => x + #1 | injr(y) => y)
+      {{ v, ⌜v = hl_val(#2)⌝ }} := by
+  wp_match
+
+/--
+error: Tactic `wp_pure` failed: Cannot find expression to evaluate
+
+hlc : HasLC
+GF✝ : BundledGFunctors
+ι : IrisGS_gen hlc Exp GF✝
+GF : BundledGFunctors
+inst✝ : HeapLangGS hlc GF
+⊢ ⏎
+  ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }}
+-/
+#guard_msgs in
+example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by
+  wp_match
+
+end wp_match
+
+end pure_tactics