feat: Intial annotations for HeapLang

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

Iris/Iris/HeapLang/Instances.lean

@@ -83,20 +83,23 @@ 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 => ?_) ?_
     · constructor
     · 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 => ?_) ?_
     · constructor
     · 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,20 +117,23 @@ 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 => ?_) ?_
     · constructor
     · 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 => ?_) ?_
     · constructor
     · 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,20 +151,23 @@ 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 => ?_) ?_
     · constructor <;> simp
     · 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 => ?_) ?_
     · constructor <;> simp
     · 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

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) -∗

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 }} -∗

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 Ψ -∗