From ddb5ea5b5c431cafb1351963285fa33aa5a09804 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Sat, 2 Oct 2021 13:51:10 +0200
Subject: [PATCH 1/3] dynamic alloc/free

---
 theories/lang/ghost_state.v |  4 ++++
 theories/lang/lang.v        | 30 ++++++++++++++++++++++++++-
 theories/lang/lifting.v     | 41 +++++++++++++++++++++++++++++++++++++
 theories/lang/tactics.v     | 32 +++++++++++++++++++++++++----
 4 files changed, 102 insertions(+), 5 deletions(-)

diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v
index 52345829..e214350d 100644
--- a/theories/lang/ghost_state.v
+++ b/theories/lang/ghost_state.v
@@ -524,6 +524,10 @@ Section heap.
     by iDestruct (heap_mapsto_mbyte_agree with "[$]") as %->.
   Qed.
 
+  Lemma heap_mapsto_layout_has_layout l ly :
+    l ↦|ly| -∗ ⌜l `has_layout_loc` ly⌝.
+  Proof. iIntros "(% & % & % & ?)". done. Qed.
+
   Lemma heap_alloc_st l h v aid :
     l.1 = ProvAlloc (Some aid) →
     heap_range_free h l.2 (length v) →
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 46b80534..5658484f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -37,6 +37,7 @@ Inductive expr :=
 | Call (f : expr) (args : list expr)
 | Concat (es : list expr)
 | IfE (ot : op_type) (e1 e2 e3 : expr)
+| Alloc (ly : layout) (e : expr)
 | SkipE (e : expr)
 | StuckE (* stuck expression *)
 .
@@ -53,6 +54,7 @@ Lemma expr_ind (P : expr → Prop) :
   (∀ (f : expr) (args : list expr), P f → Forall P args → P (Call f args)) →
   (∀ (es : list expr), Forall P es → P (Concat es)) →
   (∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) →
+  (∀ (ly : layout) (e : expr), P e → P (Alloc ly e)) →
   (∀ (e : expr), P e → P (SkipE e)) →
   (P StuckE) →
   ∀ (e : expr), P e.
@@ -77,6 +79,7 @@ Inductive stmt :=
 (* m: map from values of e to indices into bs, def: default *)
 | Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
 | Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
+| Free (ly : layout) (e : expr) (s : stmt)
 | SkipS (s : stmt)
 | StuckS (* stuck statement *)
 | ExprS (e : expr) (s : stmt)
@@ -125,6 +128,7 @@ with rtexpr :=
 | RTCall (f : runtime_expr) (args : list runtime_expr)
 | RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
 | RTConcat (es : list runtime_expr)
+| RTAlloc (ly : layout) (e : runtime_expr)
 | RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr)
 | RTSkipE (e : runtime_expr)
 | RTStuckE
@@ -134,6 +138,7 @@ with rtstmt :=
 | RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt)
 | RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
 | RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt)
+| RTFree (ly : layout) (e : runtime_expr) (s : stmt)
 | RTSkipS (s : stmt)
 | RTStuckS
 | RTExprS (e : runtime_expr) (s : stmt)
@@ -151,6 +156,7 @@ Fixpoint to_rtexpr (e : expr) : runtime_expr :=
   | CAS ot e1 e2 e3 => RTCAS ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
   | Concat es => RTConcat (to_rtexpr <$> es)
   | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
+  | Alloc ly e => RTAlloc ly (to_rtexpr e)
   | SkipE e => RTSkipE (to_rtexpr e)
   | StuckE => RTStuckE
   end.
@@ -164,6 +170,7 @@ Definition to_rtstmt (rf : runtime_function) (s : stmt) : runtime_expr :=
   | IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2
   | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def
   | Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s
+  | Free ly e s => RTFree ly (to_rtexpr e) s
   | SkipS s => RTSkipS s
   | StuckS => RTStuckS
   | ExprS e s => RTExprS (to_rtexpr e) s
@@ -198,6 +205,7 @@ Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
   | CAS ly e1 e2 e3 => CAS ly (subst x v e1) (subst x v e2) (subst x v e3)
   | Concat el => Concat (subst x v <$> el)
   | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3)
+  | Alloc ly e => Alloc ly (subst x v e)
   | SkipE e => SkipE (subst x v e)
   | StuckE => StuckE
   end.
@@ -215,6 +223,7 @@ Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
   | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
   | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
   | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
+  | Free ly e s => Free ly (subst_l xs e) (subst_stmt xs s)
   | SkipS s => SkipS (subst_stmt xs s)
   | StuckS => StuckS
   | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
@@ -459,6 +468,14 @@ comparing pointers? (see lambda rust) *)
 | IfES v ot e1 e2 b σ:
     cast_to_bool ot v σ.(st_heap) = Some b →
     expr_step (IfE ot (Val v) e1 e2) σ [] (if b then e1 else e2) σ []
+| AllocS v l ly σ hs' :
+    has_layout_val v ly →
+    has_layout_loc l ly →
+    alloc_new_block σ.(st_heap) l v hs' →
+    expr_step (Alloc ly (Val v)) σ [] (Val (val_of_loc l)) {| st_heap := hs'; st_fntbl := σ.(st_fntbl) |} []
+| AllocFailS v ly σ :
+    has_layout_val v ly →
+    expr_step (Alloc ly (Val v)) σ [] AllocFailed σ []
 (* no rule for StuckE *)
 .
 
@@ -486,6 +503,11 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
 | ReturnS rf σ hs v:
     free_blocks σ.(st_heap) rf.(rf_locs) hs → (* Deallocate the stack. *)
     stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} []
+| FreeS ly v l s rf σ hs' :
+    val_to_loc v = Some l →
+    has_layout_loc l ly →
+    free_block σ.(st_heap) l ly hs' →
+    stmt_step (Free ly (Val v) s) rf σ [] (to_rtstmt rf s) {| st_fntbl := σ.(st_fntbl); st_heap := hs' |} []
 | SkipSS rf σ s :
     stmt_step (SkipS s) rf σ [] (to_rtstmt rf s) σ []
 | ExprSS rf σ s v:
@@ -514,7 +536,8 @@ Proof.
   all: repeat select (heap_at _ _ _ _ _) ltac:(fun H => destruct H as [?[?[??]]]).
   all: try (rewrite /heap_fmap/=; eapply heap_update_heap_state_invariant => //).
   all: try (unfold has_layout_val in *; by etransitivity).
-  repeat eapply alloc_new_blocks_invariant => //.
+  - repeat eapply alloc_new_blocks_invariant => //.
+  - eapply alloc_new_block_invariant => //.
 Qed.
 
 Lemma stmt_step_preserves_invariant s rf e σ1 σ2 κs efs:
@@ -529,6 +552,7 @@ Proof.
     match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
     by destruct o.
   - move => ??? _ Hfree Hinv. by eapply free_blocks_invariant.
+  - move => ??? _ _ ???? Hfree Hinv. by eapply free_block_invariant.
 Qed.
 
 Lemma runtime_step_preserves_invariant e1 e2 σ1 σ2 κs efs:
@@ -557,6 +581,7 @@ Inductive expr_ectx :=
 | CASRCtx (ot : op_type) (v1 v2 : val)
 | ConcatCtx (vs : list val) (es : list runtime_expr)
 | IfECtx (ot : op_type) (e2 e3 : runtime_expr)
+| AllocCtx (ly : layout)
 | SkipECtx
 .
 
@@ -575,6 +600,7 @@ Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr :=
   | CASRCtx ot v1 v2 => RTCAS ot (Val v1) (Val v2) e
   | ConcatCtx vs es => RTConcat ((Expr <$> (RTVal <$> vs)) ++ e :: es)
   | IfECtx ot e2 e3 => RTIfE ot e e2 e3
+  | AllocCtx ly => RTAlloc ly e
   | SkipECtx => RTSkipE e
   end.
 
@@ -584,6 +610,7 @@ Inductive stmt_ectx :=
 | AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt)
 | AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt)
 | ReturnCtx
+| FreeCtx (ly : layout) (s : stmt)
 | IfSCtx (ot : op_type) (s1 s2 : stmt)
 | SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
 | ExprSCtx (s : stmt)
@@ -594,6 +621,7 @@ Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt :=
   | AssignRCtx o ot e1 s => RTAssign o ot e1 e s
   | AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s
   | ReturnCtx => RTReturn e
+  | FreeCtx ly s => RTFree ly e s
   | IfSCtx ot s1 s2 => RTIfS ot e s1 s2
   | SwitchCtx it m bs def => RTSwitch it e m bs def
   | ExprSCtx s => RTExprS e s
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index c6b9aafb..80ad9eb3 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -784,6 +784,26 @@ Proof.
   by iApply (wp_call_bind_ind []).
 Qed.
 
+Lemma wp_alloc E Φ (l : loc) ly (v : val) :
+  has_layout_val v ly →
+  ▷ (∀ l, l ↦ v -∗ freeable l (length v) -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗
+  WP (Alloc ly (Val v)) @ E {{ Φ }}.
+Proof.
+  iIntros (Hly) "Hwp".
+  iApply wp_lift_expr_step; first done.
+  iIntros (hs) "((%&Hhctx&Hactx)&Hfctx)/=".
+  iModIntro.
+  iSplit; first by eauto 10 using AllocFailS.
+  iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
+    (* Alloc failure case. *)
+    iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
+    iApply wp_alloc_failed.
+  }
+  iMod (heap_alloc_new_block_upd with "[$Hhctx $Hactx]") as "(Hctx & Hlv & Hlf)" => //.
+  iDestruct ("Hwp" with "Hlv Hlf [//]") as "Hpost".
+  iModIntro. iSplit => //.
+  iFrame "Hctx Hfctx". by iApply wp_value.
+Qed.
 End expr_lifting.
 
 (*** Lifting of statements *)
@@ -907,6 +927,27 @@ Proof.
   iSplit; first done. iFrame. by iApply "HWP".
 Qed.
 
+Lemma wps_free Q Ψ s l ly :
+  l ↦|ly| -∗
+  freeable l (ly.(ly_size)) -∗
+  ▷ WPs s {{ Q, Ψ }} -∗
+  WPs (Free ly (val_of_loc l) s) {{ Q, Ψ }}.
+Proof.
+  iIntros "Hl Hf HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst.
+  iPoseProof (heap_mapsto_layout_has_layout with "Hl") as "%".
+  iApply wp_lift_stmt_step. iIntros (σ) "(Hhctx&Hfctx)".
+  iMod (heap_free_block_upd with "Hl Hf Hhctx") as (σ') "(%Hf & Hhctx)".
+  iModIntro. iSplit; first by eauto 10 using FreeS, val_to_of_loc.
+  iNext. iIntros (???? Hstep ?). inv_stmt_step. iModIntro.
+  iSplitR; first done.
+  match goal with
+  | H : val_to_loc _ = Some ?l |- _ => apply val_of_to_loc in H; injection H; intros <-; intros
+  end.
+  rewrite (free_block_inj σ.(st_heap) l ly hs' σ'); [ | done..].
+  iFrame.
+  by iApply "HWP".
+Qed.
+
 Lemma wps_skip Q Ψ s:
   (|={⊤}[∅]▷=> WPs s {{ Q, Ψ }}) -∗ WPs SkipS s {{ Q , Ψ }}.
 Proof.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 72bc68a7..1032e81d 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -18,6 +18,7 @@ Inductive expr :=
 | Call (f : expr) (args : list expr)
 | Concat (es : list expr)
 | IfE (op : op_type) (e1 e2 e3 : expr)
+| Alloc (ly : layout) (e : expr)
 | SkipE (e : expr)
 | StuckE
 (* new constructors *)
@@ -51,6 +52,7 @@ Lemma expr_ind (P : expr → Prop) :
   (∀ (f : expr) (args : list expr), P f → Forall P args → P (Call f args)) →
   (∀ (es : list expr), Forall P es → P (Concat es)) →
   (∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) →
+  (∀ (ly : layout) (e : expr), P e → P (Alloc ly e)) →
   (∀ (e : expr), P e → P (SkipE e)) →
   (P StuckE) →
   (∀ (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalAnd ot1 ot2 rit e1 e2)) →
@@ -69,17 +71,17 @@ Lemma expr_ind (P : expr → Prop) :
   (∀ (e : lang.expr), P (Expr e)) → ∀ (e : expr), P e.
 Proof.
   move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
-  fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro ?.
+  fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ??????????????? Hstruct Hmacro ?.
   9: {
     apply Hcall; [ |apply Forall_true => ?]; by apply: FIX.
   }
   9: {
     apply Hconcat. apply Forall_true => ?. by apply: FIX.
   }
-  23: {
+  24: {
     apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX.
   }
-  23: {
+  24: {
     apply Hmacro. apply Forall_true => ?. by apply: FIX.
   }
   all: auto.
@@ -98,6 +100,7 @@ Fixpoint to_expr (e : expr) : lang.expr :=
   | Call f args => lang.Call (to_expr f) (to_expr <$> args)
   | Concat es => lang.Concat (to_expr <$> es)
   | IfE ot e1 e2 e3 => lang.IfE ot (to_expr e1) (to_expr e2) (to_expr e3)
+  | Alloc ly e => lang.Alloc ly (to_expr e)
   | SkipE e => lang.SkipE (to_expr e)
   | StuckE => lang.StuckE
   | LogicalAnd ot1 ot2 rit e1 e2 => notation.LogicalAnd ot1 ot2 rit (to_expr e1) (to_expr e2)
@@ -175,6 +178,8 @@ Ltac of_expr e :=
     let e2 := of_expr e2 in
     let e3 := of_expr e3 in
     constr:(IfE ot e1 e2 e3)
+  | lang.Alloc ?ly ?e =>
+    let e := of_expr e in constr:(Alloc ly e)
   | lang.SkipE ?e =>
     let e := of_expr e in constr:(SkipE e)
   | lang.StuckE => constr:(StuckE e)
@@ -203,6 +208,7 @@ Inductive ectx_item :=
 | CallRCtx (f : val) (vl : list val) (el : list expr)
 | ConcatCtx (vs : list val) (es : list expr)
 | IfECtx (ot : op_type) (e2 e3 : expr)
+| AllocCtx (ly : layout)
 | SkipECtx
 (* new constructors *)
 | UseCtx (o : order) (ot : op_type)
@@ -231,6 +237,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CallRCtx f vl el => Call (Val f) ((Val <$> vl) ++ e :: el)
   | ConcatCtx vs es => Concat ((Val <$> vs) ++ e :: es)
   | IfECtx ot e2 e3 => IfE ot e e2 e3
+  | AllocCtx ly => Alloc ly e
   | SkipECtx => SkipE e
   | UseCtx o l => Use o l e
   | AddrOfCtx => AddrOf e
@@ -283,6 +290,9 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
   | IfE ot e1 e2 e3 =>
     if find_expr_fill e1 bind_val is Some (Ks, e') then
       Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e)
+  | Alloc ly e1 =>
+      if find_expr_fill e1 bind_val is Some (Ks, e') then
+        Some (Ks ++ [AllocCtx ly], e') else Some ([], e)
   | SkipE e1 =>
     if find_expr_fill e1 bind_val is Some (Ks, e') then
       Some (Ks ++ [SkipECtx], e') else Some ([], e)
@@ -333,6 +343,7 @@ Proof.
     apply: [lang.CallRCtx _ _ _]|
     apply: [lang.ConcatCtx _ _]|
     apply: [lang.IfECtx _ _ _]|
+    apply: [lang.AllocCtx _]|
     apply: [lang.SkipECtx]|
     apply: [lang.DerefCtx _ _]|
     apply: []|
@@ -342,7 +353,7 @@ Proof.
     apply: [lang.BinOpRCtx _ _ _ _]|
     apply: []|..
   ]).
-  move: K => [|||||||||||||||||n|||] * //=.
+  move: K => [||||||||||||||||||n|||] * //=.
   - (** Call *)
     do 2 f_equal.
     rewrite !fmap_app !fmap_cons. repeat f_equal; eauto.
@@ -370,6 +381,7 @@ Inductive stmt :=
 | IfS (ot : op_type) (e : expr) (s1 s2 : stmt)
 | Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
 | Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt)
+| Free (ly : layout) (e : expr) (s : stmt)
 | SkipS (s : stmt)
 | StuckS
 | ExprS (e : expr) (s : stmt)
@@ -387,6 +399,7 @@ Lemma stmt_ind (P : stmt → Prop):
   (∀ (ot : op_type) (e : expr) (s1 : stmt), P s1 → ∀ s2 : stmt, P s2 → P (IfS ot e s1 s2)) →
   (∀ (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt), P def → Forall P bs → P (Switch it e m bs def)) →
   (∀ (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt), P s → P (Assign o ot e1 e2 s)) →
+  (∀ (ly : layout) (e : expr) (s : stmt), P s → P (Free ly e s)) →
   (∀ s : stmt, P s → P (SkipS s)) →
   (P StuckS) →
   (∀ (e : expr) (s : stmt), P s → P (ExprS e s)) →
@@ -410,6 +423,7 @@ Fixpoint to_stmt (s : stmt) : lang.stmt :=
   | IfS ot e s1 s2 => (if{ot}: to_expr e then to_stmt s1 else to_stmt s2)%E
   | Switch it e m bs def => lang.Switch it (to_expr e) m (to_stmt <$> bs) (to_stmt def)
   | Assign o ot e1 e2 s => lang.Assign o ot (to_expr e1) (to_expr e2) (to_stmt s)
+  | Free ly e s => lang.Free ly (to_expr e) (to_stmt s)
   | SkipS s => lang.SkipS (to_stmt s)
   | StuckS => lang.StuckS
   | ExprS e s => lang.ExprS (to_expr e) (to_stmt s)
@@ -455,6 +469,10 @@ Ltac of_stmt s :=
     let e2 := of_expr e2 in
     let s := of_stmt s in
     constr:(Assign o ot e1 e2 s)
+  | lang.Free ?ly ?e ?s =>
+    let e := of_expr e in
+    let s := of_stmt s in
+    constr:(Free ly e s)
   | lang.SkipS ?s =>
     let s := of_stmt s in
     constr:(SkipS s)
@@ -474,6 +492,7 @@ Inductive stmt_ectx :=
 | SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
 | ExprSCtx (s : stmt)
 | AssertCtx (ot : op_type) (s : stmt)
+| FreeCtx (ly : layout) (s : stmt)
 .
 
 Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=
@@ -485,6 +504,7 @@ Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=
   | IfSCtx ot s1 s2 => IfS ot e s1 s2
   | SwitchCtx it m bs def => Switch it e m bs def
   | AssertCtx ot s => Assert ot e s
+  | FreeCtx ly s => Free ly e s
   end.
 
 Definition find_stmt_fill (s : stmt) : option (stmt_ectx * expr) :=
@@ -496,6 +516,7 @@ Definition find_stmt_fill (s : stmt) : option (stmt_ectx * expr) :=
   | Switch it e m bs def => if e is (Val v) then None else Some (SwitchCtx it m bs def, e)
   | Assign o ot e1 e2 s => if e2 is (Val v) then if e1 is (Val v) then None else Some (AssignLCtx o ot v s, e1) else Some (AssignRCtx o ot e1 s, e2)
   | Assert ot e s => if e is (Val v) then None else Some (AssertCtx ot s, e)
+  | Free ly e s => if e is (Val v) then None else Some (FreeCtx ly s, e)
   end.
 
 Lemma find_stmt_fill_correct s Ks e:
@@ -515,6 +536,7 @@ Proof.
   eexists ([StmtCtx (lang.SwitchCtx _ _ _ _) rf])|
   eexists ([StmtCtx (lang.ExprSCtx _) rf])|
   eexists ([StmtCtx (lang.IfSCtx _ _ _) rf])|
+  eexists ([StmtCtx (lang.FreeCtx _ _) rf])|
 ..] => //=.
 Qed.
 
@@ -532,6 +554,7 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr)  : expr :=
   | Call f args => Call (subst_l xs f) (subst_l xs <$> args)
   | Concat es => Concat (subst_l xs <$> es)
   | IfE ot e1 e2 e3 => IfE ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
+  | Alloc ly e => Alloc ly (subst_l xs e)
   | SkipE e => SkipE (subst_l xs e)
   | StuckE => StuckE
   | LogicalAnd ot1 ot2 rit e1 e2 => LogicalAnd ot1 ot2 rit (subst_l xs e1) (subst_l xs e2)
@@ -621,6 +644,7 @@ Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
   | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
   | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
   | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
+  | Free ly e s => Free ly (subst_l xs e) (subst_stmt xs s)
   | SkipS s => SkipS (subst_stmt xs s)
   | StuckS => StuckS
   | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
-- 
GitLab


From c61e4490bac1214ef20d9b8add1d2e709827bf4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 5 Oct 2021 18:21:51 +0200
Subject: [PATCH 2/3] alloc kind: either heap or stack allocations

---
 theories/lang/ghost_state.v  |  60 ++++++++++----------
 theories/lang/heap.v         | 104 +++++++++++++++++++----------------
 theories/lang/lang.v         |  10 ++--
 theories/lang/lifting.v      |   6 +-
 theories/typing/adequacy.v   |   8 +--
 tutorial/adequacy/adequacy.v |   2 +-
 6 files changed, 100 insertions(+), 90 deletions(-)

diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v
index e214350d..b62ffe2c 100644
--- a/theories/lang/ghost_state.v
+++ b/theories/lang/ghost_state.v
@@ -22,7 +22,7 @@ Definition heapUR : ucmra :=
 Class heapG Σ := HeapG {
   heap_heap_inG              :> inG Σ (authR heapUR);
   heap_heap_name             : gname;
-  heap_alloc_range_map_inG   :> ghost_mapG Σ alloc_id (Z * nat);
+  heap_alloc_range_map_inG   :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
   heap_alloc_range_map_name  : gname;
   heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
   heap_alloc_alive_map_name : gname;
@@ -39,10 +39,10 @@ Definition to_heap_cellR (hc : heap_cell) : heap_cellR :=
 Definition to_heapUR : heap → heapUR :=
   fmap to_heap_cellR.
 
-Definition to_alloc_rangeR (al : allocation) : (Z * nat) :=
-  (al.(al_start), al.(al_len)).
+Definition to_alloc_rangeR (al : allocation) : (Z * nat * alloc_kind) :=
+  (al.(al_start), al.(al_len), al.(al_kind)).
 
-Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat) :=
+Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat * alloc_kind) :=
   fmap to_alloc_rangeR.
 
 Definition to_alloc_alive_map : allocs → gmap alloc_id bool :=
@@ -156,8 +156,8 @@ Section definitions.
 
   (** * Freeable *)
 
-  Definition freeable_def (l : loc) (n : nat) : iProp Σ :=
-    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true |} ∗
+  Definition freeable_def (l : loc) (n : nat) (k : alloc_kind) : iProp Σ :=
+    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗
      alloc_alive id (DfracOwn 1) true.
   Definition freeable_aux : seal (@freeable_def). by eexists. Qed.
   Definition freeable := unseal freeable_aux.
@@ -247,13 +247,14 @@ Section alloc_range.
 
   Lemma alloc_range_mono id a1 a2 :
     alloc_same_range a1 a2 →
+    a1.(al_kind) = a2.(al_kind) →
     alloc_range id a1 -∗ alloc_range id a2.
-  Proof. destruct a1 as [???], a2 as [???] => -[/= <- <-]. by rewrite alloc_range_eq. Qed.
+  Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_range_eq. Qed.
 
   Lemma alloc_range_agree id a1 a2 :
     alloc_range id a1 -∗ alloc_range id a2 -∗ ⌜alloc_same_range a1 a2⌝.
   Proof.
-    destruct a1 as [???], a2 as [???]. rewrite alloc_range_eq /alloc_same_range.
+    destruct a1 as [????], a2 as [????]. rewrite alloc_range_eq /alloc_same_range.
     iIntros "H1 H2". by iDestruct (ghost_map_elem_agree with "H1 H2") as %[=->->].
   Qed.
 
@@ -280,20 +281,21 @@ Section alloc_range.
   Lemma alloc_range_lookup am id al :
     alloc_range_ctx am -∗
     alloc_range id al -∗
-    ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al'⌝.
+    ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al' ∧ al.(al_kind) = al'.(al_kind)⌝.
   Proof.
     rewrite alloc_range_eq. iIntros "Htbl Hf".
     iDestruct (ghost_map_lookup with "Htbl Hf") as %Hlookup.
-    iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[???][?[??]]].
+    iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[????][?[???]]].
     by eexists _.
   Qed.
 
   Lemma alloc_range_ctx_same_range am id al1 al2 :
     am !! id = Some al1 →
     alloc_same_range al1 al2 →
+    al1.(al_kind) = al2.(al_kind) →
     alloc_range_ctx am = alloc_range_ctx (<[id := al2]> am).
   Proof.
-    move => Hid [Heq1 Heq2].
+    move => Hid [Heq1 Heq2] Heq3.
     rewrite /alloc_range_ctx /to_alloc_range_map fmap_insert insert_id; first done.
     rewrite lookup_fmap Hid /=. destruct al1, al2; naive_solver.
   Qed.
@@ -387,7 +389,7 @@ Section loc_in_bounds.
   Proof.
     rewrite loc_in_bounds_eq.
     iIntros "Hb ((?&?&Hctx&?)&?)". iDestruct "Hb" as (id al ????) "Hb".
-    iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[??]]].
+    iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[[??]?]]].
     iExists id, al'. iPureIntro. unfold allocation_in_range, al_end in *.
     naive_solver lia.
   Qed.
@@ -564,7 +566,7 @@ Section heap.
     heap_ctx h ==∗
       heap_ctx (heap_alloc l.2 v id h) ∗
       l ↦ v ∗
-      freeable l (length v).
+      freeable l (length v) al.(al_kind).
   Proof.
     iIntros (Hid Hfree Hstart Hlen Hrange) "#Hr Hal Hctx".
     iMod (heap_alloc_st with "Hctx") as "[$ Hl]" => //.
@@ -843,11 +845,11 @@ End alloc_alive.
 Section alloc_new_blocks.
   Context `{!heapG Σ}.
 
-  Lemma heap_alloc_new_block_upd σ1 l v σ2:
-    alloc_new_block σ1 l v σ2 →
-    heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ l ↦ v ∗ freeable l (length v).
+  Lemma heap_alloc_new_block_upd σ1 l v kind σ2:
+    alloc_new_block σ1 kind l v σ2 →
+    heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ l ↦ v ∗ freeable l (length v) kind.
   Proof.
-    move => []; clear. move => σ l aid v alloc Haid ???; subst alloc.
+    move => []; clear. move => σ l aid kind v alloc Haid ???; subst alloc.
     iIntros "Hctx". iDestruct "Hctx" as (Hinv) "(Hhctx&Hrctx&Hsctx)".
     iMod (alloc_range_alloc  with "Hrctx") as "[$ #Hb]" => //.
     iMod (alloc_alive_alloc with "Hsctx") as "[$ Hs]" => //.
@@ -857,11 +859,11 @@ Section alloc_new_blocks.
     iModIntro. iFrame. iPureIntro. by eapply alloc_new_block_invariant.
   Qed.
 
-  Lemma heap_alloc_new_blocks_upd σ1 ls vs σ2:
-    alloc_new_blocks σ1 ls vs σ2 →
+  Lemma heap_alloc_new_blocks_upd σ1 ls vs kind σ2:
+    alloc_new_blocks σ1 kind ls vs σ2 →
     heap_state_ctx σ1 ==∗
       heap_state_ctx σ2 ∗
-      [∗ list] l; v ∈ ls; vs, l ↦ v ∗ freeable l (length v).
+      [∗ list] l; v ∈ ls; vs, l ↦ v ∗ freeable l (length v) kind.
   Proof.
     move => alloc.
     iInduction alloc as [σ|] "IH"; first by iIntros "$ !>". iIntros "Hσ".
@@ -873,27 +875,27 @@ End alloc_new_blocks.
 Section free_blocks.
   Context `{!heapG Σ}.
 
-  Lemma heap_free_block_upd σ1 l ly:
+  Lemma heap_free_block_upd σ1 l ly kind:
     l ↦|ly| -∗
-    freeable l (ly_size ly) -∗
-    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 l ly σ2⌝ ∗ heap_state_ctx σ2.
+    freeable l (ly_size ly) kind -∗
+    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 kind l ly σ2⌝ ∗ heap_state_ctx σ2.
   Proof.
     iIntros "Hl Hfree (Hinv&Hhctx&Hrctx&Hsctx)". iDestruct "Hinv" as %Hinv.
     rewrite freeable_eq. iDestruct "Hfree" as (aid Haid) "[#Hrange Hkill]".
     iDestruct "Hl" as (v Hv ?) "Hl".
-    iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[???] [??]].
-    iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[??]]]. simplify_eq/=.
+    iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[????k] [??]].
+    iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=.
     iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0) with "Hhctx Hl") as %? => //.
     iExists _. iSplitR. { iPureIntro. by econstructor. }
     iMod (heap_free_free with "Hhctx Hl") as "Hhctx". rewrite Hv. iFrame => /=.
-    iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true |}) with "Hsctx Hkill") as "[$ Hd]".
+    iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true; al_kind := k |}) with "Hsctx Hkill") as "[$ Hd]".
     erewrite alloc_range_ctx_same_range; [iFrame |done..].
     iPureIntro. eapply free_block_invariant => //. by eapply FreeBlock.
   Qed.
 
-  Lemma heap_free_blocks_upd ls σ1:
-    ([∗ list] l ∈ ls, l.1 ↦|l.2| ∗ freeable l.1 (ly_size l.2)) -∗
-    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_blocks σ1 ls σ2⌝ ∗ heap_state_ctx σ2.
+  Lemma heap_free_blocks_upd ls σ1 kind:
+    ([∗ list] l ∈ ls, l.1 ↦|l.2| ∗ freeable l.1 (ly_size l.2) kind ) -∗
+    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_blocks σ1 kind ls σ2⌝ ∗ heap_state_ctx σ2.
   Proof.
     iInduction ls as [|[l ly] ls] "IH" forall (σ1).
     { iIntros "_ ? !>". iExists σ1. iFrame. iPureIntro. by constructor. }
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 9aa9a70c..3411ac50 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -185,11 +185,17 @@ Qed.
 
 (** ** Representation of allocations. *)
 
+(** An allocation can either be a stack allocation or a heap allocation. *)
+Inductive alloc_kind : Set :=
+  | HeapAlloc
+  | StackAlloc.
+
 Record allocation :=
   Allocation {
-    al_start : Z;    (* First valid address. *)
-    al_len   : nat;  (* Number of allocated byte. *)
-    al_alive : bool; (* Is the allocation still alive. *)
+    al_start : Z;           (* First valid address. *)
+    al_len   : nat;         (* Number of allocated byte. *)
+    al_alive : bool;        (* Is the allocation still alive. *)
+    al_kind : alloc_kind;   (* On the heap or on the stack? *)
   }.
 
 Definition al_end (al : allocation) : Z :=
@@ -201,7 +207,7 @@ Definition alloc_same_range (al1 al2 : allocation) : Prop :=
   al1.(al_start) = al2.(al_start) ∧ al1.(al_len) = al2.(al_len).
 
 Definition killed (al : allocation) : allocation :=
-  {| al_start := al.(al_start); al_len := al.(al_len); al_alive := false; |}.
+  {| al_start := al.(al_start); al_len := al.(al_len); al_alive := false; al_kind := al.(al_kind) |}.
 
 (** Smallest allocatable address (we reserve 0 for NULL). *)
 Definition min_alloc_start : Z := 1.
@@ -262,6 +268,8 @@ Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. na
 Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop :=
   ∃ alloc, st.(hs_allocs) !! aid = Some alloc ∧ a ∈ alloc.
 
+Global Instance alloc_kind_eq_dec : EqDecision alloc_kind.
+Proof. solve_decision. Qed.
 Global Instance allocation_eq_dec : EqDecision (allocation).
 Proof. solve_decision. Qed.
 Global Instance alloc_id_alive_dec aid st : Decision (alloc_id_alive aid st).
@@ -474,57 +482,57 @@ Arguments mem_cast : simpl never.
 
 (** ** Allocation and deallocation. *)
 
-Inductive alloc_new_block : heap_state → loc → val → heap_state → Prop :=
-| AllocNewBlock σ l aid v:
-    let alloc := Allocation l.2 (length v) true in
+Inductive alloc_new_block : heap_state → alloc_kind → loc → val → heap_state → Prop :=
+| AllocNewBlock σ l aid kind v:
+    let alloc := Allocation l.2 (length v) true kind in
     l.1 = ProvAlloc (Some aid) →
     σ.(hs_allocs) !! aid = None →
     allocation_in_range alloc →
     heap_range_free σ.(hs_heap) l.2 (length v) →
-    alloc_new_block σ l v {|
+    alloc_new_block σ kind l v {|
       hs_heap   := heap_alloc l.2 v aid σ.(hs_heap);
       hs_allocs := <[aid := alloc]> σ.(hs_allocs);
     |}.
 
-Inductive alloc_new_blocks : heap_state → list loc → list val → heap_state → Prop :=
-| AllocNewBlock_nil σ :
-    alloc_new_blocks σ [] [] σ
-| AllocNewBlock_cons σ σ' σ'' l v ls vs :
-    alloc_new_block σ l v σ' →
-    alloc_new_blocks σ' ls vs σ'' →
-    alloc_new_blocks σ (l :: ls) (v :: vs) σ''.
-
-Inductive free_block : heap_state → loc → layout → heap_state → Prop :=
-| FreeBlock σ l aid ly v:
-    let al_alive := Allocation l.2 ly.(ly_size) true  in
-    let al_dead  := Allocation l.2 ly.(ly_size) false in
+Inductive alloc_new_blocks : heap_state → alloc_kind → list loc → list val → heap_state → Prop :=
+| AllocNewBlock_nil σ kind :
+    alloc_new_blocks σ kind [] [] σ
+| AllocNewBlock_cons σ σ' σ'' l v ls kind vs :
+    alloc_new_block σ kind l v σ' →
+    alloc_new_blocks σ' kind ls vs σ'' →
+    alloc_new_blocks σ kind (l :: ls) (v :: vs) σ''.
+
+Inductive free_block : heap_state → alloc_kind → loc → layout → heap_state → Prop :=
+| FreeBlock σ l aid ly kind v:
+    let al_alive := Allocation l.2 ly.(ly_size) true  kind in
+    let al_dead  := Allocation l.2 ly.(ly_size) false kind in
     l.1 = ProvAlloc (Some aid) →
     σ.(hs_allocs) !! aid = Some al_alive →
     length v = ly.(ly_size) →
     heap_lookup_loc l v (λ st, st = RSt 0%nat) σ.(hs_heap) →
-    free_block σ l ly {|
+    free_block σ kind l ly {|
       hs_heap   := heap_free l.2 ly.(ly_size) σ.(hs_heap);
       hs_allocs := <[aid := al_dead]> σ.(hs_allocs);
     |}.
 
-Inductive free_blocks : heap_state → list (loc * layout) → heap_state → Prop :=
-| FreeBlocks_nil σ :
-    free_blocks σ [] σ
-| FreeBlocks_cons σ σ' σ'' l ly ls :
-    free_block σ l ly σ' →
-    free_blocks σ' ls σ'' →
-    free_blocks σ ((l, ly) :: ls) σ''.
+Inductive free_blocks : heap_state → alloc_kind → list (loc * layout) → heap_state → Prop :=
+| FreeBlocks_nil σ kind :
+    free_blocks σ kind [] σ
+| FreeBlocks_cons σ σ' σ'' l ly kind ls :
+    free_block σ kind l ly σ' →
+    free_blocks σ' kind ls σ'' →
+    free_blocks σ kind ((l, ly) :: ls) σ''.
 
-Lemma free_block_inj hs l ly hs1 hs2:
-  free_block hs l ly hs1 → free_block hs l ly hs2 → hs1 = hs2.
+Lemma free_block_inj hs l ly kind hs1 hs2:
+  free_block hs kind l ly hs1 → free_block hs kind l ly hs2 → hs1 = hs2.
 Proof. destruct l. inversion 1; simplify_eq. by inversion 1; simplify_eq/=. Qed.
 
-Lemma free_blocks_inj hs1 hs2 hs ls:
-  free_blocks hs ls hs1 → free_blocks hs ls hs2 → hs1 = hs2.
+Lemma free_blocks_inj hs1 hs2 hs kind ls:
+  free_blocks hs kind ls hs1 → free_blocks hs kind ls hs2 → hs1 = hs2.
 Proof.
   move Heq: {1}(hs) => hs' Hb.
-  elim: Hb hs Heq. { move => ?? ->. by inversion 1. }
-  move => ?????? Hb1 ? IH ??.
+  elim: Hb hs Heq. { move => ??? ->. by inversion 1. }
+  move => ??????? Hb1 ? IH ??.
   inversion 1; simplify_eq. apply: IH; [|done].
   by apply: free_block_inj.
 Qed.
@@ -580,25 +588,25 @@ Definition heap_state_invariant (st : heap_state) : Prop :=
 
 (** ** Lemmas about the heap state invariant. *)
 
-Lemma heap_state_alloc_alive_free_disjoint σ id a n b alloc:
+Lemma heap_state_alloc_alive_free_disjoint σ id a n b kind alloc:
   heap_state_alloc_alive_in_heap σ →
   alloc_id_alive id σ →
   heap_range_free σ.(hs_heap) a n →
   σ.(hs_allocs) !! id = Some alloc →
-  Allocation a n b ## alloc.
+  Allocation a n b kind ## alloc.
 Proof.
   move => Hin_heap Halive Hfree Hal p Hp1 Hp2.
   apply (Hin_heap _ _ Hal Halive) in Hp2 as [? Hp2].
   rewrite Hfree in Hp2; first done. apply Hp1.
 Qed.
 
-Lemma alloc_new_block_invariant σ1 σ2 l v :
-  alloc_new_block σ1 l v σ2 →
+Lemma alloc_new_block_invariant σ1 σ2 l v kind :
+  alloc_new_block σ1 kind l v σ2 →
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
   move => []; clear.
-  move => σ1 l aid v alloc Haid Hfresh Halloc Hrange H.
+  move => σ1 l aid kind v alloc Haid Hfresh Halloc Hrange H.
   destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!.
   - move => a [id??] /= Ha. destruct (decide (aid = id)) as [->|Hne].
     + exists alloc. split => /=; first by rewrite lookup_insert.
@@ -650,22 +658,22 @@ Proof.
       eapply (Hi5 _ _ Hal); [by eexists | done |..].
 Qed.
 
-Lemma alloc_new_blocks_invariant σ1 σ2 ls vs :
-  alloc_new_blocks σ1 ls vs σ2 →
+Lemma alloc_new_blocks_invariant σ1 σ2 ls vs kind :
+  alloc_new_blocks σ1 kind ls vs σ2 →
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
-  elim => [] // ??????? Hb Hbs IH H.
+  elim => [] // ???????? Hb Hbs IH H.
   apply IH. by eapply alloc_new_block_invariant.
 Qed.
 
-Lemma free_block_invariant σ1 σ2 l ly:
-  free_block σ1 l ly σ2 →
+Lemma free_block_invariant σ1 σ2 l ly kind :
+  free_block σ1 kind l ly σ2 →
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
   move => []; clear.
-  move => σ l aid ly v al_a al_d Haid Hal_a Hlen Hlookup H.
+  move => σ l aid ly kind v al_a al_d Haid Hal_a Hlen Hlookup H.
   destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!.
   - move => a hc /= Hhc.
     assert (¬ (l.2 ≤ a < l.2 + length v)) as Hnot_in.
@@ -712,12 +720,12 @@ Proof.
     erewrite elem_of_disjoint in Hdisj. by eapply Hdisj.
 Qed.
 
-Lemma free_blocks_invariant σ1 σ2 ls:
-  free_blocks σ1 ls σ2 →
+Lemma free_blocks_invariant σ1 σ2 ls kind :
+  free_blocks σ1 kind ls σ2 →
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
-  elim => [] // ?????? Hb Hbs IH H.
+  elim => [] // ??????? Hb Hbs IH H.
   apply IH. by eapply free_block_invariant.
 Qed.
 
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 5658484f..c48b93ea 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -446,9 +446,9 @@ comparing pointers? (see lambda rust) *)
     Forall2 has_layout_loc lsa fn.(f_args).*2 →
     Forall2 has_layout_loc lsv fn.(f_local_vars).*2 →
     (* initialize the local vars to poison *)
-    alloc_new_blocks σ.(st_heap) lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' →
+    alloc_new_blocks σ.(st_heap) StackAlloc lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' →
     (* initialize the arguments with the supplied values *)
-    alloc_new_blocks hs' lsa vs hs'' →
+    alloc_new_blocks hs' StackAlloc lsa vs hs'' →
     (* add used blocks allocations  *)
     rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} →
     expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) {| st_heap := hs''; st_fntbl := σ.(st_fntbl)|} []
@@ -471,7 +471,7 @@ comparing pointers? (see lambda rust) *)
 | AllocS v l ly σ hs' :
     has_layout_val v ly →
     has_layout_loc l ly →
-    alloc_new_block σ.(st_heap) l v hs' →
+    alloc_new_block σ.(st_heap) HeapAlloc l v hs' →
     expr_step (Alloc ly (Val v)) σ [] (Val (val_of_loc l)) {| st_heap := hs'; st_fntbl := σ.(st_fntbl) |} []
 | AllocFailS v ly σ :
     has_layout_val v ly →
@@ -501,12 +501,12 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
     rf.(rf_fn).(f_code) !! b = Some s →
     stmt_step (Goto b) rf σ [] (to_rtstmt rf s) σ []
 | ReturnS rf σ hs v:
-    free_blocks σ.(st_heap) rf.(rf_locs) hs → (* Deallocate the stack. *)
+    free_blocks σ.(st_heap) StackAlloc rf.(rf_locs) hs → (* Deallocate the stack. *)
     stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} []
 | FreeS ly v l s rf σ hs' :
     val_to_loc v = Some l →
     has_layout_loc l ly →
-    free_block σ.(st_heap) l ly hs' →
+    free_block σ.(st_heap) HeapAlloc l ly hs' →
     stmt_step (Free ly (Val v) s) rf σ [] (to_rtstmt rf s) {| st_fntbl := σ.(st_fntbl); st_heap := hs' |} []
 | SkipSS rf σ s :
     stmt_step (SkipS s) rf σ [] (to_rtstmt rf s) σ []
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 80ad9eb3..d816e90e 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -786,7 +786,7 @@ Qed.
 
 Lemma wp_alloc E Φ (l : loc) ly (v : val) :
   has_layout_val v ly →
-  ▷ (∀ l, l ↦ v -∗ freeable l (length v) -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗
+  ▷ (∀ l, l ↦ v -∗ freeable l (length v) HeapAlloc -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗
   WP (Alloc ly (Val v)) @ E {{ Φ }}.
 Proof.
   iIntros (Hly) "Hwp".
@@ -929,7 +929,7 @@ Qed.
 
 Lemma wps_free Q Ψ s l ly :
   l ↦|ly| -∗
-  freeable l (ly.(ly_size)) -∗
+  freeable l (ly.(ly_size)) HeapAlloc -∗
   ▷ WPs s {{ Q, Ψ }} -∗
   WPs (Free ly (val_of_loc l) s) {{ Q, Ψ }}.
 Proof.
@@ -943,7 +943,7 @@ Proof.
   match goal with
   | H : val_to_loc _ = Some ?l |- _ => apply val_of_to_loc in H; injection H; intros <-; intros
   end.
-  rewrite (free_block_inj σ.(st_heap) l ly hs' σ'); [ | done..].
+  rewrite (free_block_inj σ.(st_heap) l ly HeapAlloc hs' σ'); [ | done..].
   iFrame.
   by iApply "HWP".
 Qed.
diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 0b8d670f..54fb1002 100644
--- a/theories/typing/adequacy.v
+++ b/theories/typing/adequacy.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
 Class typePreG Σ := PreTypeG {
   type_invG                      :> invGpreS Σ;
   type_heap_heap_inG             :> inG Σ (authR heapUR);
-  type_heap_alloc_range_map_inG  :> ghost_mapG Σ alloc_id (Z * nat);
+  type_heap_alloc_range_map_inG  :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
   type_heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
   type_heap_fntbl_inG            :> ghost_mapG Σ addr function;
 }.
@@ -18,7 +18,7 @@ Class typePreG Σ := PreTypeG {
 Definition typeΣ : gFunctors :=
   #[invΣ;
    GFunctor (constRF (authR heapUR));
-   ghost_mapΣ alloc_id (Z * nat);
+   ghost_mapΣ alloc_id (Z * nat * alloc_kind);
    ghost_mapΣ alloc_id bool;
    ghost_mapΣ addr function].
 Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
@@ -38,7 +38,7 @@ Definition main_type `{!typeG Σ} (P : iProp Σ) :=
 
 (** * The main adequacy lemma *)
 Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap addr function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ:
-  alloc_new_blocks initial_heap_state gls gvs hs →
+  alloc_new_blocks initial_heap_state StackAlloc gls gvs hs →
   σ = {| st_heap := hs; st_fntbl := fns; |} →
   (∀ {HtypeG : typeG Σ}, ∃ gl gt,
   let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in
@@ -53,7 +53,7 @@ Proof.
   iMod (own_alloc (● h ⋅ ◯ h)) as (γh) "[Hh _]" => //.
   { apply auth_both_valid_discrete. split => //. }
   iMod (ghost_map_alloc fns) as (γf) "[Hf Hfm]".
-  iMod (ghost_map_alloc_empty (V:=(Z * nat))) as (γr) "Hr".
+  iMod (ghost_map_alloc_empty (V:=(Z * nat * alloc_kind))) as (γr) "Hr".
   iMod (ghost_map_alloc_empty (V:=bool)) as (γs) "Hs".
   set (HheapG := HeapG _ _ γh _ γr _ γs _ γf).
   set (HrefinedCG := RefinedCG _ _ HheapG).
diff --git a/tutorial/adequacy/adequacy.v b/tutorial/adequacy/adequacy.v
index 403eb7c6..1afe2511 100644
--- a/tutorial/adequacy/adequacy.v
+++ b/tutorial/adequacy/adequacy.v
@@ -85,7 +85,7 @@ Section adequate.
     loc_allocator_state `has_layout_loc` struct_alloc_state →
     loc_initialized `has_layout_loc` struct_latch →
     (* TODO: Should we try to show that this assumption is provable? *)
-    alloc_new_blocks initial_heap_state initial_heap_locs initial_heap_values hs →
+    alloc_new_blocks initial_heap_state StackAlloc initial_heap_locs initial_heap_values hs →
     σ = {| st_heap := hs; st_fntbl := fn_lists_to_fns function_addrs functions; |} →
     NoDup function_addrs →
     nsteps (Λ := c_lang) n (initial_prog <$> [(fn_loc addr_main); (fn_loc addr_main2)], σ) κs (t2, σ2) →
-- 
GitLab


From e465823879c4e1fa585e83e74fdf1a66e33aa995 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 6 Oct 2021 10:10:41 +0200
Subject: [PATCH 3/3] incorporate suggestions

---
 theories/lang/ghost_state.v  | 106 +++++++++++++++++------------------
 theories/lang/heap.v         |   3 +-
 theories/typing/adequacy.v   |   6 +-
 tutorial/adequacy/adequacy.v |   2 +-
 4 files changed, 59 insertions(+), 58 deletions(-)

diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v
index b62ffe2c..bf092de6 100644
--- a/theories/lang/ghost_state.v
+++ b/theories/lang/ghost_state.v
@@ -22,8 +22,8 @@ Definition heapUR : ucmra :=
 Class heapG Σ := HeapG {
   heap_heap_inG              :> inG Σ (authR heapUR);
   heap_heap_name             : gname;
-  heap_alloc_range_map_inG   :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
-  heap_alloc_range_map_name  : gname;
+  heap_alloc_meta_map_inG   :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
+  heap_alloc_meta_map_name  : gname;
   heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
   heap_alloc_alive_map_name : gname;
   heap_fntbl_inG             :> ghost_mapG Σ addr function;
@@ -39,11 +39,11 @@ Definition to_heap_cellR (hc : heap_cell) : heap_cellR :=
 Definition to_heapUR : heap → heapUR :=
   fmap to_heap_cellR.
 
-Definition to_alloc_rangeR (al : allocation) : (Z * nat * alloc_kind) :=
+Definition to_alloc_metaR (al : allocation) : (Z * nat * alloc_kind) :=
   (al.(al_start), al.(al_len), al.(al_kind)).
 
-Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat * alloc_kind) :=
-  fmap to_alloc_rangeR.
+Definition to_alloc_meta_map : allocs → gmap alloc_id (Z * nat * alloc_kind) :=
+  fmap to_alloc_metaR.
 
 Definition to_alloc_alive_map : allocs → gmap alloc_id bool :=
   fmap al_alive.
@@ -53,20 +53,20 @@ Section definitions.
 
   (** * Allocation stuff. *)
 
-  (** [alloc_range id al] persistently records the information that allocation
+  (** [alloc_meta id al] persistently records the information that allocation
   with identifier [id] has a range corresponding to that of [a]. *)
-  Definition alloc_range_def (id : alloc_id) (al : allocation) : iProp Σ :=
-    id ↪[ heap_alloc_range_map_name ]□ to_alloc_rangeR al.
-  Definition alloc_range_aux : seal (@alloc_range_def). by eexists. Qed.
-  Definition alloc_range := unseal alloc_range_aux.
-  Definition alloc_range_eq : @alloc_range = @alloc_range_def :=
-    seal_eq alloc_range_aux.
+  Definition alloc_meta_def (id : alloc_id) (al : allocation) : iProp Σ :=
+    id ↪[ heap_alloc_meta_map_name ]□ to_alloc_metaR al.
+  Definition alloc_meta_aux : seal (@alloc_meta_def). by eexists. Qed.
+  Definition alloc_meta := unseal alloc_meta_aux.
+  Definition alloc_meta_eq : @alloc_meta = @alloc_meta_def :=
+    seal_eq alloc_meta_aux.
 
-  Global Instance allocs_range_pers id al : Persistent (alloc_range id al).
-  Proof. rewrite alloc_range_eq. by apply _. Qed.
+  Global Instance allocs_range_pers id al : Persistent (alloc_meta id al).
+  Proof. rewrite alloc_meta_eq. by apply _. Qed.
 
-  Global Instance allocs_range_tl id al : Timeless (alloc_range id al).
-  Proof. rewrite alloc_range_eq. by apply _. Qed.
+  Global Instance allocs_range_tl id al : Timeless (alloc_meta id al).
+  Proof. rewrite alloc_meta_eq. by apply _. Qed.
 
   (** [loc_in_bounds l n] persistently records the information that location
   [l] and any of its positive offset up to [n] (included) are in range of the
@@ -75,7 +75,7 @@ Section definitions.
   Definition loc_in_bounds_def (l : loc) (n : nat) : iProp Σ :=
     ∃ (id : alloc_id) (al : allocation),
       ⌜l.1 = ProvAlloc (Some id)⌝ ∗ ⌜al.(al_start) ≤ l.2⌝ ∗ ⌜l.2 + n ≤ al_end al⌝ ∗
-      ⌜allocation_in_range al⌝ ∗ alloc_range id al.
+      ⌜allocation_in_range al⌝ ∗ alloc_meta id al.
   Definition loc_in_bounds_aux : seal (@loc_in_bounds_def). by eexists. Qed.
   Definition loc_in_bounds := unseal loc_in_bounds_aux.
   Definition loc_in_bounds_eq : @loc_in_bounds = @loc_in_bounds_def :=
@@ -157,7 +157,7 @@ Section definitions.
   (** * Freeable *)
 
   Definition freeable_def (l : loc) (n : nat) (k : alloc_kind) : iProp Σ :=
-    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗
+    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_meta id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗
      alloc_alive id (DfracOwn 1) true.
   Definition freeable_aux : seal (@freeable_def). by eexists. Qed.
   Definition freeable := unseal freeable_aux.
@@ -169,8 +169,8 @@ Section definitions.
   Definition heap_ctx (h : heap) : iProp Σ :=
     own heap_heap_name (● to_heapUR h).
 
-  Definition alloc_range_ctx (ub : allocs) : iProp Σ :=
-    ghost_map_auth heap_alloc_range_map_name 1 (to_alloc_range_map ub).
+  Definition alloc_meta_ctx (ub : allocs) : iProp Σ :=
+    ghost_map_auth heap_alloc_meta_map_name 1 (to_alloc_meta_map ub).
 
   Definition alloc_alive_ctx (ub : allocs) : iProp Σ :=
     ghost_map_auth heap_alloc_alive_map_name 1 (to_alloc_alive_map ub).
@@ -181,7 +181,7 @@ Section definitions.
   Definition heap_state_ctx (st : heap_state) : iProp Σ :=
     ⌜heap_state_invariant st⌝ ∗
     heap_ctx st.(hs_heap) ∗
-    alloc_range_ctx st.(hs_allocs) ∗
+    alloc_meta_ctx st.(hs_allocs) ∗
     alloc_alive_ctx st.(hs_allocs).
 
   Definition state_ctx (σ:state) : iProp Σ :=
@@ -241,70 +241,70 @@ Section fntbl.
   Qed.
 End fntbl.
 
-Section alloc_range.
+Section alloc_meta.
   Context `{!heapG Σ}.
   Implicit Types am : allocs.
 
-  Lemma alloc_range_mono id a1 a2 :
+  Lemma alloc_meta_mono id a1 a2 :
     alloc_same_range a1 a2 →
     a1.(al_kind) = a2.(al_kind) →
-    alloc_range id a1 -∗ alloc_range id a2.
-  Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_range_eq. Qed.
+    alloc_meta id a1 -∗ alloc_meta id a2.
+  Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_meta_eq. Qed.
 
-  Lemma alloc_range_agree id a1 a2 :
-    alloc_range id a1 -∗ alloc_range id a2 -∗ ⌜alloc_same_range a1 a2⌝.
+  Lemma alloc_meta_agree id a1 a2 :
+    alloc_meta id a1 -∗ alloc_meta id a2 -∗ ⌜alloc_same_range a1 a2⌝.
   Proof.
-    destruct a1 as [????], a2 as [????]. rewrite alloc_range_eq /alloc_same_range.
+    destruct a1 as [????], a2 as [????]. rewrite alloc_meta_eq /alloc_same_range.
     iIntros "H1 H2". by iDestruct (ghost_map_elem_agree with "H1 H2") as %[=->->].
   Qed.
 
-  Lemma alloc_range_alloc am id al :
+  Lemma alloc_meta_alloc am id al :
     am !! id = None →
-    alloc_range_ctx am ==∗
-    alloc_range_ctx (<[id := al]> am) ∗ alloc_range id al.
+    alloc_meta_ctx am ==∗
+    alloc_meta_ctx (<[id := al]> am) ∗ alloc_meta id al.
   Proof.
-    move => Hid. rewrite alloc_range_eq. iIntros "Hctx".
+    move => Hid. rewrite alloc_meta_eq. iIntros "Hctx".
     iMod (ghost_map_insert_persist with "Hctx") as "[? $]". { by rewrite lookup_fmap fmap_None. }
     by rewrite -fmap_insert.
   Qed.
 
-  Lemma alloc_range_to_loc_in_bounds l id (n : nat) al:
+  Lemma alloc_meta_to_loc_in_bounds l id (n : nat) al:
     l.1 = ProvAlloc (Some id) →
     al.(al_start) ≤ l.2 ∧ l.2 + n ≤ al_end al →
     allocation_in_range al →
-    alloc_range id al -∗ loc_in_bounds l n.
+    alloc_meta id al -∗ loc_in_bounds l n.
   Proof.
     iIntros (?[??]?) "Hr". rewrite loc_in_bounds_eq.
     iExists id, al. by iFrame "Hr".
   Qed.
 
-  Lemma alloc_range_lookup am id al :
-    alloc_range_ctx am -∗
-    alloc_range id al -∗
+  Lemma alloc_meta_lookup am id al :
+    alloc_meta_ctx am -∗
+    alloc_meta id al -∗
     ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al' ∧ al.(al_kind) = al'.(al_kind)⌝.
   Proof.
-    rewrite alloc_range_eq. iIntros "Htbl Hf".
+    rewrite alloc_meta_eq. iIntros "Htbl Hf".
     iDestruct (ghost_map_lookup with "Htbl Hf") as %Hlookup.
     iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[????][?[???]]].
     by eexists _.
   Qed.
 
-  Lemma alloc_range_ctx_same_range am id al1 al2 :
+  Lemma alloc_meta_ctx_same_range am id al1 al2 :
     am !! id = Some al1 →
     alloc_same_range al1 al2 →
     al1.(al_kind) = al2.(al_kind) →
-    alloc_range_ctx am = alloc_range_ctx (<[id := al2]> am).
+    alloc_meta_ctx am = alloc_meta_ctx (<[id := al2]> am).
   Proof.
     move => Hid [Heq1 Heq2] Heq3.
-    rewrite /alloc_range_ctx /to_alloc_range_map fmap_insert insert_id; first done.
+    rewrite /alloc_meta_ctx /to_alloc_meta_map fmap_insert insert_id; first done.
     rewrite lookup_fmap Hid /=. destruct al1, al2; naive_solver.
   Qed.
 
-  Lemma alloc_range_ctx_killed am id al :
+  Lemma alloc_meta_ctx_killed am id al :
     am !! id = Some al →
-    alloc_range_ctx am = alloc_range_ctx (<[id := killed al]> am).
-  Proof. move => ?. by apply: alloc_range_ctx_same_range. Qed.
-End alloc_range.
+    alloc_meta_ctx am = alloc_meta_ctx (<[id := killed al]> am).
+  Proof. move => ?. by apply: alloc_meta_ctx_same_range. Qed.
+End alloc_meta.
 
 Section alloc_alive.
   Context `{!heapG Σ}.
@@ -351,7 +351,7 @@ Section loc_in_bounds.
       iDestruct "H2" as (?? Hl2 ? Hend ?) "#H2".
       move: Hl1 Hl2 => /= Hl1 Hl2. iExists id, al.
       destruct l. unfold al_end in *. simpl in *. simplify_eq.
-      iDestruct (alloc_range_agree with "H2 H1") as %[? <-].
+      iDestruct (alloc_meta_agree with "H2 H1") as %[? <-].
       iFrame "H1". iPureIntro. rewrite /shift_loc /= in Hend. naive_solver lia.
     - iIntros "H". iDestruct "H" as (id al ????) "#H".
       iSplit; iExists id, al; iFrame "H"; iPureIntro; split_and! => //=; lia.
@@ -389,7 +389,7 @@ Section loc_in_bounds.
   Proof.
     rewrite loc_in_bounds_eq.
     iIntros "Hb ((?&?&Hctx&?)&?)". iDestruct "Hb" as (id al ????) "Hb".
-    iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[[??]?]]].
+    iDestruct (alloc_meta_lookup with "Hctx Hb") as %[al' [?[[??]?]]].
     iExists id, al'. iPureIntro. unfold allocation_in_range, al_end in *.
     naive_solver lia.
   Qed.
@@ -561,7 +561,7 @@ Section heap.
     al.(al_start) = l.2 →
     al.(al_len) = length v →
     allocation_in_range al →
-    alloc_range id al -∗
+    alloc_meta id al -∗
     alloc_alive id (DfracOwn 1) true -∗
     heap_ctx h ==∗
       heap_ctx (heap_alloc l.2 v id h) ∗
@@ -574,7 +574,7 @@ Section heap.
     rewrite heap_mapsto_mbyte_eq /heap_mapsto_mbyte_def.
     iSplitR "Hal"; last first; last iSplit.
     - rewrite freeable_eq. iExists id. iFrame. iSplit => //.
-      by iApply (alloc_range_mono with "Hr").
+      by iApply (alloc_meta_mono with "Hr").
     - rewrite loc_in_bounds_eq. iExists id, al. iFrame "Hr".
       rewrite /al_end. iPureIntro. naive_solver lia.
     - iApply (big_sepL_impl with "Hl").
@@ -851,9 +851,9 @@ Section alloc_new_blocks.
   Proof.
     move => []; clear. move => σ l aid kind v alloc Haid ???; subst alloc.
     iIntros "Hctx". iDestruct "Hctx" as (Hinv) "(Hhctx&Hrctx&Hsctx)".
-    iMod (alloc_range_alloc  with "Hrctx") as "[$ #Hb]" => //.
+    iMod (alloc_meta_alloc  with "Hrctx") as "[$ #Hb]" => //.
     iMod (alloc_alive_alloc with "Hsctx") as "[$ Hs]" => //.
-    iDestruct (alloc_range_to_loc_in_bounds l aid (length v) with "[Hb]")
+    iDestruct (alloc_meta_to_loc_in_bounds l aid (length v) with "[Hb]")
       as "#Hinb" => //; [done|..].
     iMod (heap_alloc with "Hb Hs Hhctx") as "[Hhctx [Hv Hal]]" => //.
     iModIntro. iFrame. iPureIntro. by eapply alloc_new_block_invariant.
@@ -884,12 +884,12 @@ Section free_blocks.
     rewrite freeable_eq. iDestruct "Hfree" as (aid Haid) "[#Hrange Hkill]".
     iDestruct "Hl" as (v Hv ?) "Hl".
     iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[????k] [??]].
-    iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=.
+    iDestruct (alloc_meta_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=.
     iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0) with "Hhctx Hl") as %? => //.
     iExists _. iSplitR. { iPureIntro. by econstructor. }
     iMod (heap_free_free with "Hhctx Hl") as "Hhctx". rewrite Hv. iFrame => /=.
     iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true; al_kind := k |}) with "Hsctx Hkill") as "[$ Hd]".
-    erewrite alloc_range_ctx_same_range; [iFrame |done..].
+    erewrite alloc_meta_ctx_same_range; [iFrame |done..].
     iPureIntro. eapply free_block_invariant => //. by eapply FreeBlock.
   Qed.
 
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 3411ac50..274a26d5 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -188,7 +188,8 @@ Qed.
 (** An allocation can either be a stack allocation or a heap allocation. *)
 Inductive alloc_kind : Set :=
   | HeapAlloc
-  | StackAlloc.
+  | StackAlloc 
+  | GlobalAlloc.
 
 Record allocation :=
   Allocation {
diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 54fb1002..eb010ef0 100644
--- a/theories/typing/adequacy.v
+++ b/theories/typing/adequacy.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
 Class typePreG Σ := PreTypeG {
   type_invG                      :> invGpreS Σ;
   type_heap_heap_inG             :> inG Σ (authR heapUR);
-  type_heap_alloc_range_map_inG  :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
+  type_heap_alloc_meta_map_inG  :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind);
   type_heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
   type_heap_fntbl_inG            :> ghost_mapG Σ addr function;
 }.
@@ -38,7 +38,7 @@ Definition main_type `{!typeG Σ} (P : iProp Σ) :=
 
 (** * The main adequacy lemma *)
 Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap addr function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ:
-  alloc_new_blocks initial_heap_state StackAlloc gls gvs hs →
+  alloc_new_blocks initial_heap_state GlobalAlloc gls gvs hs →
   σ = {| st_heap := hs; st_fntbl := fns; |} →
   (∀ {HtypeG : typeG Σ}, ∃ gl gt,
   let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in
@@ -62,7 +62,7 @@ Proof.
   set (Hglobals := {| global_locs := gl; global_initialized_types := gt; |}).
   move => Hwp.
   iMod (heap_alloc_new_blocks_upd with "[Hh Hr Hs]") as "[Hctx Hmt]" => //. {
-    rewrite /heap_state_ctx /alloc_range_ctx /to_alloc_range_map /alloc_alive_ctx /to_alloc_alive_map !fmap_empty.
+    rewrite /heap_state_ctx /alloc_meta_ctx /to_alloc_meta_map /alloc_alive_ctx /to_alloc_alive_map !fmap_empty.
     by iFrame.
   }
   rewrite big_sepL2_sep. iDestruct "Hmt" as "[Hmt Hfree]".
diff --git a/tutorial/adequacy/adequacy.v b/tutorial/adequacy/adequacy.v
index 1afe2511..28b747d9 100644
--- a/tutorial/adequacy/adequacy.v
+++ b/tutorial/adequacy/adequacy.v
@@ -85,7 +85,7 @@ Section adequate.
     loc_allocator_state `has_layout_loc` struct_alloc_state →
     loc_initialized `has_layout_loc` struct_latch →
     (* TODO: Should we try to show that this assumption is provable? *)
-    alloc_new_blocks initial_heap_state StackAlloc initial_heap_locs initial_heap_values hs →
+    alloc_new_blocks initial_heap_state GlobalAlloc initial_heap_locs initial_heap_values hs →
     σ = {| st_heap := hs; st_fntbl := fn_lists_to_fns function_addrs functions; |} →
     NoDup function_addrs →
     nsteps (Λ := c_lang) n (initial_prog <$> [(fn_loc addr_main); (fn_loc addr_main2)], σ) κs (t2, σ2) →
-- 
GitLab