diff --git a/Iris/Iris/HeapLang.lean b/Iris/Iris/HeapLang.lean
index 138791e1e..a2aca2461 100644
--- a/Iris/Iris/HeapLang.lean
+++ b/Iris/Iris/HeapLang.lean
@@ -4,6 +4,7 @@ public import Iris.HeapLang.Completeness
 public import Iris.HeapLang.Instances
 public import Iris.HeapLang.Linter
 public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Porting
 public import Iris.HeapLang.PrimitiveLaws
 public import Iris.HeapLang.ProofMode
 public import Iris.HeapLang.Semantics
diff --git a/Iris/Iris/HeapLang/Instances.lean b/Iris/Iris/HeapLang/Instances.lean
index 106d0dc85..fb3171e27 100644
--- a/Iris/Iris/HeapLang/Instances.lean
+++ b/Iris/Iris/HeapLang/Instances.lean
@@ -83,6 +83,7 @@ theorem mk_pure_prim_step {e1 e2 : Exp} (hstep : ∀ σ, BaseStep e1 σ [] e2 σ
   · exact ⟨e2, σ, [], BaseStep.ContextStep.intro (K := []) (hstep _)⟩
   · exact hpure (baseStep_of_primStep Hstep hsub)
 
+@[rocq_alias heap_lang.pure_if_true]
 instance instPureExecIfTrue: PureExec True 1 hl(if #true then &e1 else &e2) e1 where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -90,6 +91,7 @@ instance instPureExecIfTrue: PureExec True 1 hl(if #true then &e1 else &e2) e1 w
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_if_false]
 instance instPureExecIfFalse : PureExec True 1 hl(if #false then &e1 else &e2) e2 where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -97,6 +99,7 @@ instance instPureExecIfFalse : PureExec True 1 hl(if #false then &e1 else &e2) e
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_case_inl]
 instance instPureExecCaseInjl {v e1 e2} :
     PureExec True 1 (Exp.case hl(v(injl(&v))) e1 e2) (.app e1 (.ofVal v)) where
   pureExec _ := by
@@ -105,6 +108,7 @@ instance instPureExecCaseInjl {v e1 e2} :
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_case_inr]
 instance instPureExecCaseInjr {v e1 e2} :
     PureExec True 1 (Exp.case hl(v(injr(&v))) e1 e2) (.app e2 (.ofVal v)) where
   pureExec _ := by
@@ -113,6 +117,7 @@ instance instPureExecCaseInjr {v e1 e2} :
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_injlc]
 instance instPureExecInjl {v : Val} : PureExec True 1 hl(injl(&v)) hl(v(injl(&v)))  where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -120,6 +125,7 @@ instance instPureExecInjl {v : Val} : PureExec True 1 hl(injl(&v)) hl(v(injl(&v)
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_injrc]
 instance instPureExecInjr {v : Val} : PureExec True 1 hl(injr(&v)) hl(v(injr(&v)))  where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -127,6 +133,7 @@ instance instPureExecInjr {v : Val} : PureExec True 1 hl(injr(&v)) hl(v(injr(&v)
     · cases hs <;> simp
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_beta]
 instance instPureExecBeta {f x : Binder} {e : Exp} {v : Val} :
     PureExec True 1 hl(v(rec &f &x := &e) &v) ((e.subst f (.rec_ f x e)).subst x v) where
   pureExec _ := by
@@ -135,6 +142,7 @@ instance instPureExecBeta {f x : Binder} {e : Exp} {v : Val} :
     · cases hs <;> simp [*]
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_recc]
 instance instPureExecRec {f x e} :
     PureExec True 1 hl(rec &f &x := &e) hl(v(rec &f &x := &e)) where
   pureExec _ := by
@@ -143,6 +151,7 @@ instance instPureExecRec {f x e} :
     · cases hs <;> simp [*]
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_fst]
 instance instPureExecFst {v1 v2 : Val} : PureExec True 1 hl(fst(v((&v1, &v2)))) v1 where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -150,6 +159,7 @@ instance instPureExecFst {v1 v2 : Val} : PureExec True 1 hl(fst(v((&v1, &v2))))
     · cases hs <;> simp [*]
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_snd]
 instance instPureExecSnd {v1 v2 : Val} : PureExec True 1 hl(snd(v((&v1, &v2)))) v2 where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -157,6 +167,7 @@ instance instPureExecSnd {v1 v2 : Val} : PureExec True 1 hl(snd(v((&v1, &v2))))
     · cases hs <;> simp [*]
     · solve_subredex_values
 
+@[rocq_alias heap_lang.pure_pairc]
 instance instPureExecPair {v1 v2 : Val} : PureExec True 1 hl((&v1, &v2)) hl(v((&v1, &v2)))  where
   pureExec _ := by
     refine .once <| mk_pure_prim_step (fun _ => ?_) (fun hs => ?_) ?_
@@ -165,6 +176,7 @@ instance instPureExecPair {v1 v2 : Val} : PureExec True 1 hl((&v1, &v2)) hl(v((&
     · solve_subredex_values
 
 set_option synthInstance.checkSynthOrder false in
+@[rocq_alias heap_lang.pure_unop]
 instance instPureExecUnOp {op : UnOp} {v v' : Val} :
     PureExec (op.eval v = some v') 1 (Exp.unop op (.ofVal v)) (.ofVal v') where
   pureExec h := by
@@ -174,6 +186,7 @@ instance instPureExecUnOp {op : UnOp} {v v' : Val} :
     · solve_subredex_values
 
 set_option synthInstance.checkSynthOrder false in
+@[rocq_alias heap_lang.pure_binop]
 instance instPureExecBinOp {op : BinOp} {v1 v2 v' : Val} :
     PureExec (op.eval v1 v2 = some v') 1
       (Exp.binop op (.ofVal v1) (.ofVal v2)) (.ofVal v') where
@@ -184,6 +197,7 @@ instance instPureExecBinOp {op : BinOp} {v1 v2 v' : Val} :
     · solve_subredex_values
 
 -- higher priority than the generic binop instance
+@[rocq_alias heap_lang.pure_eqop]
 instance (priority := default + 10) instPureExecEqOp {v1 v2 : Val} :
     PureExec (v1.compareSafe v2) 1
       (Exp.binop .eq (.ofVal v1) (.ofVal v2)) (.ofVal (.lit (.bool (v1 == v2)))) where
@@ -193,36 +207,47 @@ instance (priority := default + 10) instPureExecEqOp {v1 v2 : Val} :
     · cases hs <;> simp_all [BinOp.eval]
     · solve_subredex_values
 
+@[rocq_alias heap_lang.load_atomic]
 instance instAtomicLoad {s} {v : Val} : Atomic s hl(!&v) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.store_atomic]
 instance instAtomicStore {s} {v1 v2 : Val} : Atomic s hl(&v1 ← &v2) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.fst_atomic]
 instance instAtomicFst {s} {v1 : Val} : Atomic s hl(fst(&v1)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.snd_atomic]
 instance instAtomicSnd {s} {v1 : Val} : Atomic s hl(snd(&v1)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.alloc_atomic]
 instance instAtomicAllocN {s} {v1 v2 : Val} : Atomic s hl(allocn(&v1, &v2)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.free_atomic]
 instance instAtomicFree {s} {v : Val} : Atomic s hl(free(&v)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.xchg_atomic]
 instance instAtomicXchg {s} {v1 v2 : Val} : Atomic s hl(xchg(&v1, &v2)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.faa_atomic]
 instance instAtomicFaa {s} {v1 v2 : Val} : Atomic s hl(faa(&v1, &v2)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.fork_atomic]
 instance instAtomicFork {s} {e : Exp} : Atomic s hl(fork(&e)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.new_proph_atomic]
 instance instAtomicNewProph {s} : Atomic s (State := State) Exp.newProph where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
+@[rocq_alias heap_lang.cmpxchg_atomic]
 instance instAtomicCmpXChg {s} {v1 v2 v3 : Val} : Atomic s hl(cmpXchg(&v1, &v2, &v3)) where
   atomic {σ obs e' σ' eₜ} Hstep := by solve_atomic Hstep
 
@@ -278,6 +303,7 @@ theorem base_step_more_proph_ids {e : Exp} {σ : State} {κs : List Observation}
   | cmpXchgS _ _ _ _ _ b _ _ _ => cases b <;> intro _ hx <;> exact hx
   | _ => intro _ hx; exact hx
 
+@[rocq_alias heap_lang.step_resolve]
 theorem step_resolve {e : Exp} {vp vt : Val} {σ₁ σ₂ : State} {κ : List Observation} {e₂ : Exp} {efs : List Exp}
     [hatom : Atomic .StronglyAtomic e]
     (hprim : PrimStep.primStep (Exp.resolve e (.val vp) (.val vt), σ₁) κ (e₂, σ₂, efs)) :
@@ -318,6 +344,7 @@ theorem step_resolve_decompose {e : Exp} {p : ProphId} {w : Val} {σ₁ σ₂ :
   match step_resolve hstep with
   | .resolveS _ v_n _ _ _ _ κs_n _ hb _ => ⟨κs_n, v_n, rfl, rfl, hb⟩
 
+@[rocq_alias heap_lang.resolve_reducible]
 theorem resolve_reducible {e : Exp} {σ : State} {p : ProphId} {v : Val}
     [hatom : Atomic .StronglyAtomic e] (hred : BaseStep.Reducible (e, σ))
     (hin : σ.usedProphId.contains p) :
@@ -348,6 +375,7 @@ theorem prim_step_more_proph_ids {e : Exp} {σ : State} {κs : List Observation}
 /-- `resolve e &vp &vt` is atomic whenever its subexpression `e` is strongly
 atomic: any step of the whole expression is a `resolveS` base step, which runs
 `e` to a value and produces a value. Mirrors `resolve_atomic` in Rocq. -/
+@[rocq_alias heap_lang.resolve_atomic]
 instance instAtomicResolve {s} {e : Exp} {vp vt : Val} [hatom : Atomic .StronglyAtomic e] :
     Atomic s (Exp.resolve e (.val vp) (.val vt)) where
   atomic {σ obs e' σ' eₜ} Hstep := by
diff --git a/Iris/Iris/HeapLang/Lib/Lock.lean b/Iris/Iris/HeapLang/Lib/Lock.lean
index d87a1e1f1..8bd8bb970 100644
--- a/Iris/Iris/HeapLang/Lib/Lock.lean
+++ b/Iris/Iris/HeapLang/Lib/Lock.lean
@@ -10,6 +10,7 @@ open BI
 
 @[expose] public section
 
+@[rocq_alias heap_lang.lock]
 class Lock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where
   newlock : Val
   acquire : Val
@@ -57,6 +58,7 @@ instance instPersistentLockIsLock  γ v R : Persistent (lk.isLock N γ v R) :=
 instance instTimelessLockLocked  γ : Timeless (lk.locked N γ) :=
   lk.locked_timeless γ
 
+@[rocq_alias heap_lang.is_lock_contractive]
 theorem isLock_contractive γ v : OFE.Contractive (lk.isLock N γ v) := by
   rw [contractive_internalEq (PROP := IProp GF)]
   iintro %x₁ %x₂ #HEQ
@@ -80,6 +82,9 @@ instance is_lock_ne γ v : OFE.NonExpansive (lk.isLock N γ v) :=
   letI _ := isLock_contractive N γ v
   OFE.ne_of_contractive _
 
+#rocq_ignore heap_lang.is_lock_proper "OFE is Leibniz; use equality"
+
+@[rocq_alias heap_lang.newlock_spec]
 theorem newlock_spec R :
     ⊢ □ ∀ (Φ : Val → IProp GF),
     R -∗ (∀ (v : Val) (γ : lk.name), lk.isLock N γ v R -∗ Φ v) -∗
diff --git a/Iris/Iris/HeapLang/Lib/Par.lean b/Iris/Iris/HeapLang/Lib/Par.lean
index 94996d760..82e99ccf7 100644
--- a/Iris/Iris/HeapLang/Lib/Par.lean
+++ b/Iris/Iris/HeapLang/Lib/Par.lean
@@ -18,8 +18,10 @@ open BI Iris ProgramLogic Spawn
 
 namespace Par
 
+@[rocq_alias heap_lang.parN]
 def parN : Namespace := ndot nroot "par"
 
+@[rocq_alias heap_lang.par]
 def par : Val := hl_val%
   λ e1 e2,
     let handle := &spawn e1;
@@ -37,6 +39,7 @@ section Specs
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [SpawnG GF]
 
+@[rocq_alias heap_lang.par_spec]
 theorem par_spec (Ψ1 Ψ2 : Val → IProp GF) (f1 f2 : Val) (Φ : Val → IProp GF) :
     ⊢ WP hl(&f1 #()) {{ Ψ1 }} -∗
       WP hl(&f2 #()) {{ Ψ2 }} -∗
@@ -60,6 +63,7 @@ theorem par_spec (Ψ1 Ψ2 : Val → IProp GF) (f1 f2 : Val) (Φ : Val → IProp
   wp_pures
   iexact HΦ
 
+@[rocq_alias heap_lang.wp_par]
 theorem wp_par (Ψ1 Ψ2 : Val → IProp GF) (e1 e2 : Exp) (Φ : Val → IProp GF) :
     ⊢ WP hl(&e1) {{ Ψ1 }} -∗
       WP hl(&e2) {{ Ψ2 }} -∗
diff --git a/Iris/Iris/HeapLang/Lib/Spawn.lean b/Iris/Iris/HeapLang/Lib/Spawn.lean
index 27bc366e7..358463e0a 100644
--- a/Iris/Iris/HeapLang/Lib/Spawn.lean
+++ b/Iris/Iris/HeapLang/Lib/Spawn.lean
@@ -19,32 +19,41 @@ open BI Iris ProgramLogic
 
 namespace Spawn
 
+@[rocq_alias heap_lang.spawn]
 def spawn : Val := hl_val%
   λ f,
     let c := ref(none());
     fork(c ← some(f #()));
     c
 
+@[rocq_alias heap_lang.join]
 def join : Val := hl_val%
   rec join c :=
     match !c with
     | some(x) => x
     | none() => join c
 
+@[rocq_alias heap_lang.spawnG]
 abbrev SpawnG (GF : BundledGFunctors) := TokenG GF
 
+#rocq_ignore heap_lang.«spawnΣ» "Superseded by the `SpawnG` typeclass on `BundledGFunctors`."
+#rocq_ignore heap_lang.«subG_spawnΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 section Predicates
 
 variable [HeapLangGS hlc GF] [SpawnG GF] (N : Namespace)
 
+@[rocq_alias heap_lang.spawn_inv]
 def spawnInv (γ : GName) (l : Loc) (Ψ : Val → IProp GF) : IProp GF := iprop%
   ∃ lv : Val, (l ↦ some lv) ∗
     (⌜lv = hl_val(none())⌝ ∨
      ∃ w : Val, ⌜lv = hl_val(some(&w))⌝ ∗ (Ψ w ∨ token γ))
 
+@[rocq_alias heap_lang.join_handle]
 def joinHandle (l : Loc) (Ψ : Val → IProp GF) : IProp GF := iprop%
   ∃ γ : GName, token γ ∗ inv N (spawnInv γ l Ψ)
 
+@[rocq_alias heap_lang.spawn_inv_ne]
 instance spawnInv_ne (γ : GName) (l : Loc) :
     OFE.NonExpansive (spawnInv γ l : (Val → IProp GF) → _) where
   ne _ _ _ HΨ :=
@@ -53,6 +62,7 @@ instance spawnInv_ne (γ : GName) (l : Loc) :
         or_ne.ne .rfl <| exists_ne fun w =>
           sep_ne.ne .rfl <| or_ne.ne (HΨ w) .rfl
 
+@[rocq_alias heap_lang.join_handle_ne]
 instance joinHandle_ne (l : Loc) :
     OFE.NonExpansive (joinHandle N l : (Val → IProp GF) → _) where
   ne _ _ _ HΨ :=
@@ -66,6 +76,7 @@ section Specs
 
 variable [HeapLangGS hlc GF] [SpawnG GF] (N : Namespace)
 
+@[rocq_alias heap_lang.spawn_spec]
 theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
     ⊢ □ ∀ (Φ : Val → IProp GF),
       WP hl(&f #()) {{ Ψ }} -∗
@@ -111,6 +122,7 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) :
   · itrivial
   · iframe
 
+@[rocq_alias heap_lang.join_spec]
 theorem join_spec (Ψ : Val → IProp GF) (l : Loc) :
     ⊢ □ ∀ (Φ : Val → IProp GF),
       joinHandle N l Ψ -∗
diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean
index f634739c3..fe09e668a 100644
--- a/Iris/Iris/HeapLang/Lib/SpinLock.lean
+++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean
@@ -20,31 +20,42 @@ open BI Iris ProgramLogic
 
 namespace SpinLock
 
+@[rocq_alias heap_lang.newlock]
 def newlock : Val := hl_val(
   λ _, ref(#false))
+@[rocq_alias heap_lang.try_acquire]
 def tryAcquire : Val := hl_val(
   λ l, snd(cmpXchg(l, #false, #true)))
+@[rocq_alias heap_lang.acquire]
 def acquire : Val := hl_val(
   rec acquire l :=
     if (&tryAcquire l)
       then #()
       else acquire l)
+@[rocq_alias heap_lang.release]
 def release : Val := hl_val(
   λ l, l ← #false)
 
+@[rocq_alias heap_lang.spin_lockG]
 abbrev SpinLockG (GF : BundledGFunctors) := TokenG GF
 
+#rocq_ignore heap_lang.«spin_lockΣ» "Superseded by the `SpinLockG` typeclass on `BundledGFunctors`."
+#rocq_ignore heap_lang.«subG_spin_lockΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 def spinlockN : Namespace := ndot nroot "spinlock"
 
 section Predicates
 
 variable [HeapLangGS hlc GF] [SpinLockG GF]
 
+@[rocq_alias heap_lang.locked]
 def locked (γ : GName) : IProp GF := token γ
 
+@[rocq_alias heap_lang.lock_inv]
 def lockInv (γ : GName) (l : Loc) (R : IProp GF) : IProp GF := iprop%
   ∃ b : Bool, (l ↦ some hl_val(#b)) ∗ (if b then True else locked γ ∗ R)
 
+@[rocq_alias heap_lang.is_lock]
 def isLock (γ : GName) (lk : Val) (R : IProp GF) : IProp GF := iprop%
   ∃ l : Loc, ⌜lk = Val.lit (.loc l)⌝ ∧ inv spinlockN (lockInv γ l R)
 
@@ -54,9 +65,11 @@ instance instIsLockPersistent (γ : GName) (lk : Val) (R : IProp GF) : Persisten
 instance instLockedTimeless (γ : GName) : Timeless (locked (GF := GF) γ) := by
   unfold locked; infer_instance
 
+@[rocq_alias heap_lang.locked_exclusive]
 theorem instLockedExclusive (γ : GName) : locked γ ∗ locked γ ⊢@{IProp GF} False :=
   token_exclusive γ
 
+@[rocq_alias heap_lang.is_lock_iff]
 theorem is_lock_iff (γ : GName) (lk : Val) (R₁ R₂ : IProp GF) :
     isLock γ lk R₁ ⊢ (▷ □ (R₁ ∗-∗ R₂)) -∗ isLock γ lk R₂ := by
   unfold isLock lockInv
@@ -83,6 +96,7 @@ section Specs
 
 variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [SpinLockG GF]
 
+@[rocq_alias heap_lang.newlock_spec_delay_init]
 theorem newlock_spec :
   ⊢ □ ∀ (Φ : Val → IProp GF),
     (∀ (v : Val) (γ : GName), (∀ R E, R ={E}=∗ isLock γ v R) -∗ Φ v) -∗
@@ -104,6 +118,7 @@ theorem newlock_spec :
   iframe
   itrivial
 
+@[rocq_alias heap_lang.try_acquire_spec]
 theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
     ⊢ □ ∀ (Φ : Val → IProp GF),
     isLock γ lk R -∗
@@ -147,6 +162,7 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
       simp only [Bool.false_eq_true, ↓reduceIte]
       itrivial
 
+@[rocq_alias heap_lang.acquire_spec]
 theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
   ⊢ □ ∀ (Φ : Val → IProp GF),
     isLock γ lk R -∗
@@ -168,6 +184,7 @@ theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) :
     simp only [if_pos]
     iframe
 
+@[rocq_alias heap_lang.release_spec]
 theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) :
   ⊢ □ ∀ (Φ : Val → IProp GF),
     isLock γ lk R ∗ (locked γ ∗ R) -∗
@@ -196,7 +213,7 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) :
 
 end Specs
 
-@[implicit_reducible]
+@[implicit_reducible, rocq_alias heap_lang.spin_lock]
 def instLock [HeapLangGS hlc GF] : Lock GF where
   newlock := newlock
   acquire := acquire
diff --git a/Iris/Iris/HeapLang/Porting.lean b/Iris/Iris/HeapLang/Porting.lean
new file mode 100644
index 000000000..e7e160657
--- /dev/null
+++ b/Iris/Iris/HeapLang/Porting.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+import Iris.Std.RocqPorting
+
+/-!
+# HeapLang porting bookkeeping
+
+File-level `#rocq_ignore_file` entries for `iris_heap_lang/`. Per-definition
+`@[rocq_alias]` and `#rocq_ignore` entries live next to the declarations they
+describe; only whole-file decisions are recorded here.
+-/
+
+#rocq_ignore_file heap_lang "pretty.v"
+  "Rocq-specific pretty printing; Lean prints HeapLang via the delaborators in Notation.lean"
diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean
index 6157337ad..52cbeac1a 100644
--- a/Iris/Iris/HeapLang/PrimitiveLaws.lean
+++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean
@@ -22,6 +22,7 @@ section HeapLangGS
 
 abbrev ProphMapF := fun V => Std.ExtTreeMap ProphId V compare
 
+@[rocq_alias heap_lang.heapGpreS]
 class HeapLangGpreS (hlc : outParam HasLC) (GF : BundledGFunctors) extends InvGpreS GF where
   heap_pre : genHeapPreS Loc (Option Val) GF HeapF
   proph_pre : prophMapPreS ProphId (Val × Val) GF ProphMapF
@@ -29,6 +30,31 @@ class HeapLangGpreS (hlc : outParam HasLC) (GF : BundledGFunctors) extends InvGp
 attribute [reducible, instance] HeapLangGpreS.heap_pre
 attribute [reducible, instance] HeapLangGpreS.proph_pre
 
+#rocq_ignore heap_lang.«heapΣ» "Superseded by the `HeapLangGpreS` typeclass on `BundledGFunctors`."
+#rocq_ignore heap_lang.subG_heapGpreS "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
+/-! ### The heap_lang points-to assertion
+The HeapLang points-to assertion is taken from `gen_heap`. -/
+
+attribute [rocq_alias heap_lang.pointsto] pointsTo
+attribute [rocq_alias heap_lang.pointsto_timeless] instTimelessPointsTo
+attribute [rocq_alias heap_lang.pointsto_fractional] instFractionalPointsTo
+attribute [rocq_alias heap_lang.pointsto_as_fractional] instAsFractionalPointsTo
+attribute [rocq_alias heap_lang.pointsto_valid] pointsTo_cmraValid
+attribute [rocq_alias heap_lang.pointsto_valid_2] pointsTo_op_cmraValid
+attribute [rocq_alias heap_lang.pointsto_agree] pointsTo_agree
+attribute [rocq_alias heap_lang.pointsto_combine] pointsTo_combine
+attribute [rocq_alias heap_lang.pointsto_frac_ne] pointsTo_frac_ne
+attribute [rocq_alias heap_lang.pointsto_ne] pointsTo_ne
+attribute [rocq_alias heap_lang.pointsto_persist] pointsTo_persist
+attribute [rocq_alias heap_lang.pointsto_unpersist] pointsTo_unpersist
+attribute [rocq_alias heap_lang.pointsto_persistent] instPersistentPointsTo
+
+#rocq_ignore heap_lang.pointsto_def "Rocq sealing auxiliary definition."
+#rocq_ignore heap_lang.pointsto_aux "Rocq sealing auxiliary definition."
+#rocq_ignore heap_lang.pointsto_unseal "Rocq unsealing lemma."
+
+@[rocq_alias heap_lang.heapGS_gen]
 class HeapLangGS (hlc : outParam HasLC) (GF : BundledGFunctors) where
   -- not an instance on purpose to avoid diamonds with IrisGS_gen
   [invGS : InvGS_gen hlc GF]
@@ -50,6 +76,7 @@ theorem prophMapInterp_nil_append [HeapLangGS hlc GF] (κs : List Observation)
     (ps : Std.ExtTreeSet ProphId) : prophMapInterp ([] ++ κs) ps ⊣⊢ prophMapInterp κs ps :=
   .rfl
 
+@[rocq_alias heap_lang.heapGS_irisGS]
 instance HeapLang [HeapLangGS hlc GF] : IrisGS_gen hlc Exp GF where
   invGS := HeapLangGS.invGS
   numLatersPerStep n := 0
@@ -99,6 +126,7 @@ end HeapLangGS
 
 section Adequacy
 
+@[rocq_alias heap_lang.heap_adequacy]
 theorem heap_adequacy [HeapLangGpreS .hasLC GF] (e : Exp) σ (φ : Val → Prop)
     (Hwp : ∀ [HeapLangGS .hasLC GF], ⊢@{IProp GF} (WP e {{ v, ⌜φ v⌝ }})) :
     adequate .NotStuck e σ (fun v _ => φ v) := by
@@ -146,6 +174,7 @@ theorem wp_rec {f x : Binder} {e : Exp} {vf v : Val}
   dsimp only [Nat.repeat]
   iintro !> !> !> -; iframe
 
+@[rocq_alias heap_lang.wp_fork]
 theorem wp_fork {e : Exp} :
     ▷ Φ (hl_val(#())) -∗
     ▷ WP e @ s; ⊤ {{ _v, True }} -∗
@@ -174,6 +203,7 @@ theorem wp_fork {e : Exp} :
   · iapply BI.BigSepL.bigSepL_singleton
     iframe Hwp
 
+@[rocq_alias heap_lang.wp_fork_fupd]
 theorem wp_fork_fupd {e : Exp} :
     (▷ |={E}=> (WP e @ s; ⊤ {{ _v, True }} ∗ Φ (hl_val(#())))) ⊢
       WP hl(fork(&e)) @ s; E {{ Φ }} := by
@@ -202,6 +232,7 @@ theorem wp_fork_fupd {e : Exp} :
   · iapply BI.BigSepL.bigSepL_singleton
     iframe Hwp
 
+@[rocq_alias heap_lang.wp_alloc]
 theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) :
     ▷ (∀ l : Loc, l ↦ some v -∗ Φ (.lit $ .loc l)) -∗
     WP hl(ref(&v)) @ s; E {{ Φ }} := by
@@ -240,6 +271,7 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) :
   isplit; ipureintro; rfl
   iapply HΦ $$ [$]
 
+@[rocq_alias heap_lang.wp_load]
 theorem wp_load {l : Loc} {q} {v : Val} Φ :
     ▷ l ↦{q} some v -∗
     ▷ (l ↦{q} some v -∗ Φ v) -∗
@@ -274,6 +306,7 @@ theorem wp_load {l : Loc} {q} {v : Val} Φ :
   · ipureintro; simp [toVal]; rfl
   · iapply HΦ $$ [$]
 
+@[rocq_alias heap_lang.wp_store]
 theorem wp_store {l : Loc} {v v' : Val} Φ :
     ▷ l ↦ some v' -∗
     ▷ (l ↦ some v -∗ Φ hl_val(#())) -∗
@@ -312,6 +345,7 @@ theorem wp_store {l : Loc} {v v' : Val} Φ :
   · ipureintro; rfl
   · iapply HΦ $$ [$]
 
+@[rocq_alias heap_lang.wp_cmpxchg_fail]
 theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v2 : Val}
     (Heq1 : toVal e1 = .some v1) (Heq2 : toVal e2 = .some v2) (Heq3 : v'.compareSafe v1)
     (Heq4 : decide (v' = v1) = false) :
@@ -355,6 +389,7 @@ theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp
   ipureintro
   simp
 
+@[rocq_alias heap_lang.wp_cmpxchg_suc]
 theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v2 : Val}
     (Heq1 : toVal e1 = .some v1) (Heq2 : toVal e2 = .some v2) (Heq3 : v'.compareSafe v1)
     (Heq4 : decide (v' = v1) = true) :
@@ -400,6 +435,7 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v
   ipureintro; simp [toVal]
   rfl
 
+@[rocq_alias heap_lang.wp_free]
 theorem wp_free {l : Loc} {v : Val} :
     ▷ (l ↦ some v) ⊢ WP hl(free(#l)) @ s; E {{ v'', ⌜v'' = hl_val(#())⌝ ∗ l ↦ none }} := by
   iintro >Hpt
@@ -434,6 +470,7 @@ theorem wp_free {l : Loc} {v : Val} :
   simp [toVal]
   rfl
 
+@[rocq_alias heap_lang.wp_xchg]
 theorem wp_xchg {l : Loc} {v w : Val} :
     ▷ (l ↦ some v) ⊢ WP hl(xchg(#l, &w)) @ s; E {{ v'', ⌜v'' = v⌝ ∗ l ↦ some w }} := by
   iintro >Hpt
@@ -469,6 +506,7 @@ theorem wp_xchg {l : Loc} {v w : Val} :
   iframe Hpt
   ipureintro; simp [toVal]; rfl
 
+@[rocq_alias heap_lang.wp_faa]
 theorem wp_faa {l : Loc} {i1 i2 : Int} :
     ▷ (l ↦ some hl_val(#i1))
     ⊢ WP hl(faa(#l, #i2)) @ s; E {{ v'', ⌜v'' = hl_val(#i1)⌝ ∗ l ↦ some hl_val(#(i1 + i2)) }} := by
@@ -506,6 +544,7 @@ theorem wp_faa {l : Loc} {i1 i2 : Int} :
   iframe Hpt
   ipureintro; simp [toVal]; rfl
 
+@[rocq_alias heap_lang.wp_new_proph]
 theorem wp_new_proph Φ :
     (∀ p pvs, proph p pvs -∗ Φ (.lit (.prophecy p))) -∗
     WP hl(newProph()) @ s; E {{ Φ }} := by
@@ -543,6 +582,7 @@ theorem wp_new_proph Φ :
     iapply HΦ $$ [$]
   · simp only [Algebra.BigOpL.bigOpL_nil]; itrivial
 
+@[rocq_alias heap_lang.wp_resolve_strong]
 theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)}
     (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none) :
     proph p pvs -∗
@@ -609,6 +649,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val ×
     iapply wp_value'
     iapply HΦ $$ %pvs'' %hpvs'_eq Hele
 
+@[rocq_alias heap_lang.wp_resolve]
 theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)}
     (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none := by decide) :
     proph p pvs -∗
@@ -623,6 +664,7 @@ theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)}
   iframe Hp
   iexact Hcont
 
+@[rocq_alias heap_lang.wp_resolve_proph]
 theorem wp_resolve_proph {p : ProphId} {w : Val} {pvs : List (Val × Val)} :
     proph p pvs -∗
     (∀ pvs', ⌜pvs = (hl_val(#()), w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ hl_val(#())) -∗
diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean
index 6c3b9c110..03229249a 100644
--- a/Iris/Iris/HeapLang/ProofMode.lean
+++ b/Iris/Iris/HeapLang/ProofMode.lean
@@ -190,11 +190,13 @@ public meta def ProofModeM.runTacticWp {α} (tacName : Name) (k : MVarId → WpG
       | throwIPMError "The goal {goal} must be a WP"
     k mvar {hyps, ι, s, E, e, Φ, hu:=⟨⟩, hprop:=⟨⟩, hbi:=⟨⟩ }
 
+@[rocq_alias heap_lang.tac_wp_value]
 public theorem tac_wp_value [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {v : Val} {Φ : Val → IProp GF}
   (H : Δ ⊢ |={E}=> Φ v) :
   (Δ ⊢ WP (v : Exp) @ s ; E {{ Φ }}) :=
   H.trans (wp_value_fupd ⟨rfl⟩).2
 
+@[rocq_alias heap_lang.tac_wp_value_nofupd]
 public theorem tac_wp_value_nofupd [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {v : Val} {Φ : Val → IProp GF}
   (H : Δ ⊢ Φ v) :
   (Δ ⊢ WP (v : Exp) @ s ; E {{ Φ }}) :=
@@ -258,6 +260,7 @@ public meta def iWpExprSimp (e : Q(Exp)) :
   let ⟨res, _⟩ ← Meta.simp e simpctx (simprocs:=#[procs])
   return ⟨res.expr, ← res.getProof' e⟩
 
+@[rocq_alias heap_lang.tac_wp_expr_eval]
 public theorem tac_wp_expr_simp [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {e e' : Exp} {Φ : Val → IProp GF}
   (h : Δ ⊢ WP e' @ s ; E {{ Φ }})
   (heq : e = e') :
@@ -298,6 +301,7 @@ elab "wp_finish" : tactic =>
     let pf ← iWpFinish hyps ι s E e Φ
     mvar.assign pf
 
+@[rocq_alias heap_lang.tac_wp_bind]
 public theorem tac_wp_bind [ι : IrisGS_gen hlc Exp GF] {Δ} {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e' : Exp} {Φ : Val → IProp GF}
   (H : Δ ⊢ WP e' @ s ; E {{ v, WP (ProgramLogic.fill K (Exp.ofVal (Expr:=Exp) v)) @ s; E {{ Φ }} }}) :
     (Δ ⊢ WP (ProgramLogic.fill K e') @ s ; E {{ Φ }}) :=
@@ -331,6 +335,7 @@ elab "wp_bind" colGt ppSpace focus:hl_exp:10 : tactic =>
       let pf ← addBIGoal hyps q(Wp.wp $s $E $e' $Φ')
       mvar.assign q(tac_wp_bind $pf)
 
+@[rocq_alias heap_lang.tac_wp_pure]
 public theorem tac_wp_pure [ι : IrisGS_gen hlc Exp GF] {Δ Δ'} {s : Stuckness} {E : CoPset} {K : List ECtxItem} {e₁ e₂ : Exp} {φ : Prop} {n : Nat} {Φ : Val → IProp GF} :
     ProgramLogic.Language.PureExec φ n e₁ e₂ →
     φ →
@@ -447,6 +452,7 @@ theorem tac_wp_heap_op [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' P P' : IProp GF}
   iapply hcont
   iframe
 
+@[rocq_alias heap_lang.tac_wp_alloc]
 public theorem tac_wp_alloc [ι : HeapLangGS hlc GF] {Δ Δ' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {v : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -458,6 +464,7 @@ public theorem tac_wp_alloc [ι : HeapLangGS hlc GF] {Δ Δ' : IProp GF}
   refine .trans ?_ (wand_entails (wp_alloc v _))
   exact later_mono <| forall_intro fun l => wand_intro (hcont l)
 
+@[rocq_alias heap_lang.tac_wp_free]
 public theorem tac_wp_free [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -466,6 +473,7 @@ public theorem tac_wp_free [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     Δ ⊢ WP (ProgramLogic.fill K hl(free(#l))) @ s ; E {{ Φ }} :=
   tac_wp_heap_op rfl wp_free hlater hsplit (sep_elim_left.trans hcont)
 
+@[rocq_alias heap_lang.tac_wp_load]
 public theorem tac_wp_load [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} {p : Bool}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -479,6 +487,7 @@ public theorem tac_wp_load [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} {p
   refine later_mono ?_
   exact (lookup_split hsplit).trans (sep_mono .rfl (wand_mono .rfl hcont))
 
+@[rocq_alias heap_lang.tac_wp_store]
 public theorem tac_wp_store [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -495,6 +504,7 @@ public theorem tac_wp_store [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
   refine .trans sep_comm.mp ?_
   exact sep_mono .rfl (wand_intro hcont)
 
+@[rocq_alias heap_lang.tac_wp_xchg]
 public theorem tac_wp_xchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v' : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -504,6 +514,7 @@ public theorem tac_wp_xchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     Δ ⊢ WP (ProgramLogic.fill K hl(xchg(#l, &v'))) @ s ; E {{ Φ }} :=
   tac_wp_heap_op rfl wp_xchg hlater hsplit hcont
 
+@[rocq_alias heap_lang.tac_wp_cmpxchg_fail]
 public theorem tac_wp_cmpXchg_fail [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} {p : Bool}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {q} {v v1 v2 : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -524,6 +535,7 @@ public theorem tac_wp_cmpXchg_fail [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp
   iapply hcont
   iapply Hrestore $$ HP
 
+@[rocq_alias heap_lang.tac_wp_cmpxchg_suc]
 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 : Δ ⊢ ▷ Δ')
@@ -534,6 +546,7 @@ public theorem tac_wp_cmpXchg_suc [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp
     Δ ⊢ 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
 
+@[rocq_alias heap_lang.tac_wp_cmpxchg]
 public theorem tac_wp_cmpXchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {v v1 v2 : Val} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
@@ -547,6 +560,7 @@ public theorem tac_wp_cmpXchg [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
   if heq : v = v1 then tac_wp_cmpXchg_suc hlater hsplit heq hsafe (hsuc heq)
   else tac_wp_cmpXchg_fail (p := false) hlater hsplit heq hsafe (hfail heq)
 
+@[rocq_alias heap_lang.tac_wp_faa]
 public theorem tac_wp_faa [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF}
     {s : Stuckness} {E : CoPset} {K : List ECtxItem} {l : Loc} {z1 z2 : Int} {Φ}
     (hlater : Δ ⊢ ▷ Δ')
diff --git a/Iris/Iris/HeapLang/Semantics.lean b/Iris/Iris/HeapLang/Semantics.lean
index faed75d25..ff1c16fea 100644
--- a/Iris/Iris/HeapLang/Semantics.lean
+++ b/Iris/Iris/HeapLang/Semantics.lean
@@ -19,6 +19,7 @@ namespace Iris.HeapLang
 
 open Std
 
+@[rocq_alias heap_lang.heap_lang.ectx_item]
 inductive ECtxItem where
   | appL (v2 : Val)
   | appR (e1 : Exp)
@@ -51,6 +52,7 @@ inductive ECtxItem where
   | resolveR (e0 e1 : Exp)
   deriving Inhabited, Repr, DecidableEq
 
+@[rocq_alias heap_lang.heap_lang.fill_item]
 def ECtxItem.fill (Ki : ECtxItem) (e : Exp) : Exp :=
   match Ki with
   | .appL v2        => .app e (.ofVal v2)
@@ -83,19 +85,25 @@ def ECtxItem.fill (Ki : ECtxItem) (e : Exp) : Exp :=
   | .resolveM e0 v2   => .resolve e0 e (.ofVal v2)
   | .resolveR e0 e1   => .resolve e0 e1 e
 
+@[rocq_alias heap_lang.heap_lang.state]
 structure State where
   heap : Std.ExtTreeMap Loc (Option Val)
   usedProphId : Std.ExtTreeSet ProphId
 
 instance : Inhabited State := ⟨.empty, .empty⟩
 
+attribute [rocq_alias heap_lang.heap_lang.state_inhabited] instInhabitedState
+
+@[rocq_alias heap_lang.heap_lang.observation]
 abbrev Observation := ProphId × (Val × Val)
 
+@[rocq_alias heap_lang.heap_lang.un_op_eval]
 def UnOp.eval : UnOp → Val → Option Val
   | .neg,   .lit (.bool b) => some (.lit (.bool (!b)))
   | .minus, .lit (.int n)  => some (.lit (.int (-n)))
   | _,      _              => none
 
+@[rocq_alias heap_lang.heap_lang.bin_op_eval]
 def BinOp.eval : BinOp → Val → Val → Option Val
   | .plus,   .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 + n2)))
   | .minus,  .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 - n2)))
@@ -119,6 +127,7 @@ def BinOp.eval : BinOp → Val → Val → Option Val
 
 abbrev HeapF := fun V => Std.ExtTreeMap Loc V compare
 
+@[rocq_alias heap_lang.heap_lang.state_init_heap]
 abbrev State.initHeap (σ : State) (l : Loc) (n : Int) (v : Option Val) : State :=
   { σ with heap := (List.range n.toNat).foldl
             (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) σ.heap }
@@ -202,6 +211,7 @@ theorem State.initHeap_self {σ : State} {l : Loc} {v : Option Val}
   simp only [State.initHeap, Int.toNat_one, List.range_one, List.foldl_cons, List.foldl_nil,
     Int.cast_ofNat_Int, hl, hins]
 
+@[rocq_alias heap_lang.heap_lang.base_step]
 inductive BaseStep : Exp → State → List Observation → Exp → State → List Exp → Prop where
   | recS (f x : Binder) (e : Exp) (σ : State) :
       BaseStep (.rec_ f x e) σ [] (.ofVal (.rec_ f x e)) σ []
diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean
index 8b82bd62d..bb2a8a87b 100644
--- a/Iris/Iris/HeapLang/Syntax.lean
+++ b/Iris/Iris/HeapLang/Syntax.lean
@@ -42,9 +42,25 @@ instance : Std.LawfulEqOrd Loc where
     intros l₁ l₂; unfold compare; unfold instOrdLoc; simp;
     intros h; ext; assumption
 
+attribute [rocq_alias heap_lang.Loc.eq_spec] Loc.ext_iff
+
+@[rocq_alias heap_lang.Loc.add]
 instance : HAdd Loc Int Loc where
   hAdd l i := ⟨l.n + i⟩
 
+-- Rocq's `Loc` carries a `Prop`-valued order `Loc.le`/`Loc.lt` together with its
+-- decidability and order-theoretic properties. `Loc` has no `LE`/`LT` instance here:
+-- comparison goes through `Ord Loc` above, and the order itself is the `Int` order
+-- on the `Loc.n` field, so all of these are `Int` facts.
+#rocq_ignore heap_lang.Loc.le "Use the `Int` order on `Loc.n`; comparison is the `Ord Loc` instance."
+#rocq_ignore heap_lang.Loc.lt "Use the `Int` order on `Loc.n`; comparison is the `Ord Loc` instance."
+#rocq_ignore heap_lang.Loc.le_dec "Decidable via the `Int` order on `Loc.n`."
+#rocq_ignore heap_lang.Loc.lt_dec "Decidable via the `Int` order on `Loc.n`."
+#rocq_ignore heap_lang.Loc.le_po "Follows from the `Int` order on `Loc.n`, with `Loc.ext_iff` for antisymmetry."
+#rocq_ignore heap_lang.Loc.le_total "Follows from the `Int` order on `Loc.n`."
+#rocq_ignore heap_lang.Loc.le_ngt "Follows from the `Int` order on `Loc.n`."
+#rocq_ignore heap_lang.Loc.le_lteq "Follows from the `Int` order on `Loc.n`, with `Loc.ext_iff`."
+
 instance : Zero Loc where
   zero := ⟨0⟩
 
@@ -93,12 +109,16 @@ inductive BaseLit where
   | prophecy (p : ProphId)
 deriving Inhabited, Repr, DecidableEq
 
+attribute [rocq_alias heap_lang.heap_lang.base_lit_eq_dec] instDecidableEqBaseLit
+
 @[rocq_alias heap_lang.heap_lang.un_op]
 inductive UnOp where
   | neg
   | minus
 deriving Inhabited, Repr, DecidableEq
 
+attribute [rocq_alias heap_lang.heap_lang.un_op_eq_dec] instDecidableEqUnOp
+
 @[rocq_alias heap_lang.heap_lang.bin_op]
 inductive BinOp where
   /- We use "tdiv" and "tmod" instead of "div" and "mod" to
@@ -111,6 +131,8 @@ inductive BinOp where
   | offset /- pointer offset -/
 deriving Inhabited, Repr, DecidableEq
 
+attribute [rocq_alias heap_lang.heap_lang.bin_op_eq_dec] instDecidableEqBinOp
+
 mutual
   @[rocq_alias heap_lang.heap_lang.expr]
   inductive Exp : Type where
@@ -157,6 +179,11 @@ mutual
   deriving Inhabited, Repr, DecidableEq
 end
 
+attribute [rocq_alias heap_lang.heap_lang.expr_eq_dec] instDecidableEqExp
+attribute [rocq_alias heap_lang.heap_lang.val_eq_dec] instDecidableEqVal
+attribute [rocq_alias heap_lang.heap_lang.expr_inhabited] instInhabitedExp
+attribute [rocq_alias heap_lang.heap_lang.val_inhabited] instInhabitedVal
+
 def Exp.isVal : Exp → Bool
   | .val _ => true
   | _ => false
@@ -197,6 +224,7 @@ instance : Coe Unit BaseLit where
 
 attribute [coe] BaseLit.int BaseLit.bool BaseLit.loc BaseLit.prophecy
 
+@[rocq_alias heap_lang.heap_lang.subst]
 def Exp.substStr (x : String) (v : Val) (e : Exp) : Exp :=
   match e with
   | .val _ => e
@@ -223,22 +251,30 @@ def Exp.substStr (x : String) (v : Val) (e : Exp) : Exp :=
   | .newProph => .newProph
   | .resolve e₀ e₁ e₂ => .resolve (e₀.substStr x v) (e₁.substStr x v) (e₂.substStr x v)
 
+@[rocq_alias heap_lang.heap_lang.subst']
 def Exp.subst (x : Binder) (v : Val) (e : Exp) : Exp :=
   if let .named x := x then Exp.substStr x v e else e
 
+@[rocq_alias heap_lang.heap_lang.lit_is_unboxed]
 def BaseLit.isUnboxed : BaseLit → Bool
   | .prophecy _ | .poison => false
   | _ => true
 
+@[rocq_alias heap_lang.heap_lang.val_is_unboxed]
 def Val.isUnboxed : Val → Bool
   | .lit l => l.isUnboxed
   | .injL (.lit l) => l.isUnboxed
   | .injR (.lit l) => l.isUnboxed
   | _ => false
 
+@[rocq_alias heap_lang.heap_lang.vals_compare_safe]
 def Val.compareSafe (v1 v2 : Val) : Bool :=
   v1.isUnboxed || v2.isUnboxed
 
+-- Rocq states unboxedness as a `Prop` and derives decidability; here it is `Bool`-valued.
+#rocq_ignore heap_lang.heap_lang.lit_is_unboxed_dec "`BaseLit.isUnboxed` is `Bool`-valued; decidability is definitional."
+#rocq_ignore heap_lang.heap_lang.val_is_unboxed_dec "`Val.isUnboxed` is `Bool`-valued; decidability is definitional."
+
 section Derived
 def Exp.stuck : Exp := Exp.app (.ofVal $ .lit $ .int 0) (.ofVal $ .lit $ .int 0)