From 522e030492604245f84860e9d1691e96fe5d3027 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 May 2020 09:55:09 +0200
Subject: [PATCH] make heap store (option val) in preparation for deallocation

---
 theories/heap_lang/adequacy.v        |  8 ++---
 theories/heap_lang/lang.v            | 54 ++++++++++++++--------------
 theories/heap_lang/lib/atomic_heap.v |  2 +-
 theories/heap_lang/lifting.v         | 38 ++++++++++++++------
 theories/heap_lang/metatheory.v      | 14 ++++----
 theories/heap_lang/proph_erasure.v   | 53 ++++++++++++++-------------
 theories/heap_lang/total_adequacy.v  |  2 +-
 7 files changed, 95 insertions(+), 76 deletions(-)

diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 2b6366bb2..bce15e435 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -6,13 +6,13 @@ Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
-  heap_preG_heap :> gen_heapPreG loc val Σ;
-  heap_preG_inv_heap :> inv_heapPreG loc val Σ;
+  heap_preG_heap :> gen_heapPreG loc (option val) Σ;
+  heap_preG_inv_heap :> inv_heapPreG loc (option val) Σ;
   heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
 }.
 
 Definition heapΣ : gFunctors :=
-  #[invΣ; gen_heapΣ loc val; inv_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+  #[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val); proph_mapΣ proph_id (val * val)].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
@@ -22,7 +22,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
   iMod (gen_heap_init σ.(heap)) as (?) "Hh".
-  iMod (inv_heap_init loc val) as (?) ">Hi".
+  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iModIntro. iExists
     (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 0df1c4053..ee332ffbb 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -7,6 +7,8 @@ Set Default Proof Using "Type".
 
 (** heap_lang.  A fairly simple language used for common Iris examples.
 
+Noteworthy design choices:
+
 - This is a right-to-left evaluated language, like CakeML and OCaml.  The reason
   for this is that it makes curried functions usable: Given a WP for [f a b], we
   know that any effects [f] might have to not matter until after *both* [a] and
@@ -185,9 +187,9 @@ Definition vals_compare_safe (vl v1 : val) : Prop :=
   val_is_unboxed vl ∨ val_is_unboxed v1.
 Arguments vals_compare_safe !_ !_ /.
 
-(** The state: heaps of vals. *)
+(** The state: heaps of [option val]s, with [None] representing deallocated locations. *)
 Record state : Type := {
-  heap: gmap loc val;
+  heap: gmap loc (option val);
   used_proph_id: gset proph_id;
 }.
 
@@ -544,7 +546,7 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
     | _, _ => None
     end.
 
-Definition state_upd_heap (f: gmap loc val → gmap loc val) (σ: state) : state :=
+Definition state_upd_heap (f: gmap loc (option val) → gmap loc (option val)) (σ: state) : state :=
   {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
 Arguments state_upd_heap _ !_ /.
 
@@ -552,42 +554,42 @@ Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: sta
   {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
 Arguments state_upd_used_proph_id _ !_ /.
 
-Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val :=
+Fixpoint heap_array (l : loc) (vs : list val) : gmap loc (option val) :=
   match vs with
   | [] => ∅
-  | v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs'
+  | v :: vs' => {[l := Some v]} ∪ heap_array (l +ₗ 1) vs'
   end.
 
-Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
+Lemma heap_array_singleton l v : heap_array l [v] = {[l := Some v]}.
 Proof. by rewrite /heap_array right_id. Qed.
 
-Lemma heap_array_lookup l vs w k :
-  heap_array l vs !! k = Some w ↔
-  ∃ j, 0 ≤ j ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some w.
+Lemma heap_array_lookup l vs ow k :
+  heap_array l vs !! k = Some ow ↔
+  ∃ j w, 0 ≤ j ∧ k = l +ₗ j ∧ ow = Some w ∧ vs !! (Z.to_nat j) = Some w.
 Proof.
   revert k l; induction vs as [|v' vs IH]=> l' l /=.
   { rewrite lookup_empty. naive_solver lia. }
   rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
-  - intros [[-> ->] | (Hl & j & ? & -> & ?)].
-    { exists 0. rewrite loc_add_0. naive_solver lia. }
-    exists (1 + j). rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
-  - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
+  - intros [[-> ?] | (Hl & j & w & ? & -> & -> & ?)].
+    { eexists 0, _. rewrite loc_add_0. naive_solver lia. }
+    eexists (1 + j), _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
+  - intros (j & ? & ? & -> & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
     { rewrite loc_add_0; eauto. }
     right. split.
     { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
     assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
     { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
     rewrite Hj /= in Hil.
-    exists (j - 1). rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
+    eexists (j - 1), _. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
     auto with lia.
 Qed.
 
-Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) :
+Lemma heap_array_map_disjoint (h : gmap loc (option val)) (l : loc) (vs : list val) :
   (∀ i, (0 ≤ i) → (i < length vs) → h !! (l +ₗ i) = None) →
   (heap_array l vs) ##ₘ h.
 Proof.
   intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
-  intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
+  intros (j&?&?&->&?&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
   move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
 Qed.
 
@@ -596,7 +598,7 @@ Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
   state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
 
 Lemma state_init_heap_singleton l v σ :
-  state_init_heap l 1 v σ = state_upd_heap <[l:=v]> σ.
+  state_init_heap l 1 v σ = state_upd_heap <[l:=Some v]> σ.
 Proof.
   destruct σ as [h p]. rewrite /state_init_heap /=. f_equiv.
   rewrite right_id insert_union_singleton_l. done.
@@ -642,28 +644,28 @@ Inductive head_step : expr → state → list observation → expr → state →
                (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
                []
   | LoadS l v σ :
-     σ.(heap) !! l = Some v →
+     σ.(heap) !! l = Some $ Some v →
      head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
-  | StoreS l v σ :
-     is_Some (σ.(heap) !! l) →
-     head_step (Store (Val $ LitV $ LitLoc l) (Val v)) σ
+  | StoreS l v w σ :
+     σ.(heap) !! l = Some $ Some v →
+     head_step (Store (Val $ LitV $ LitLoc l) (Val w)) σ
                []
-               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
+               (Val $ LitV LitUnit) (state_upd_heap <[l:=Some w]> σ)
                []
   | CmpXchgS l v1 v2 vl σ b :
-     σ.(heap) !! l = Some vl →
+     σ.(heap) !! l = Some $ Some vl →
      (* Crucially, this compares the same way as [EqOp]! *)
      vals_compare_safe vl v1 →
      b = bool_decide (vl = v1) →
      head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
+               (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=Some v2]> σ else σ)
                []
   | FaaS l i1 i2 σ :
-     σ.(heap) !! l = Some (LitV (LitInt i1)) →
+     σ.(heap) !! l = Some $ Some (LitV (LitInt i1)) →
      head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
                []
-               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
+               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=Some $ LitV (LitInt (i1 + i2))]>σ)
                []
   | NewProphS σ p :
      p ∉ σ.(used_proph_id) →
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 7e847e369..0ce56eadd 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -137,4 +137,4 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
      cmpxchg_spec := primitive_cmpxchg_spec;
-     mapsto_agree := gen_heap.mapsto_agree  |}.
+     mapsto_agree := lifting.mapsto_agree |}.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 584d4a340..a5fb41562 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
-  heapG_gen_heapG :> gen_heapG loc val Σ;
-  heapG_inv_heapG :> inv_heapG loc val Σ;
+  heapG_gen_heapG :> gen_heapG loc (option val) Σ;
+  heapG_inv_heapG :> inv_heapG loc (option val) Σ;
   heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
 }.
 
@@ -23,19 +23,21 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 }.
 
 (** Override the notations so that scopes and coercions work out *)
-Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
+Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q (Some v%V))
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Notation "l ↦ v" :=
-  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
+Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l 1%Qp (Some v%V))
+  (at level 20) : bi_scope.
 Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
-Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
+Notation "l ↦□ I" :=
+  (inv_mapsto (L:=loc) (V:=option val) l (from_option I%stdpp%type False))
   (at level 20, format "l  ↦□  I") : bi_scope.
-Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
+Notation "l ↦_ I v" :=
+  (inv_mapsto_own (L:=loc) (V:=option val) l (Some v%V) (from_option I%stdpp%type False))
   (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
-Notation inv_heap_inv := (inv_heap_inv loc val).
+Notation inv_heap_inv := (inv_heap_inv loc (option val)).
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
@@ -257,6 +259,20 @@ Proof.
 Qed.
 
 (** Heap *)
+
+(** We need to adjust some [gen_heap] lemmas because of our value type
+being [option val]. *)
+
+Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
+Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
+
+Lemma mapsto_combine l q1 q2 v1 v2 :
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 + q2} v1 ∗ ⌜v1 = v2⌝.
+Proof.
+  iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
+  iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+Qed.
+
 (** The usable rules for [allocN] stated in terms of the [array] proposition
 are derived in te file [array]. *)
 Lemma heap_array_to_seq_meta l vs (n : nat) :
@@ -267,7 +283,7 @@ Proof.
   iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
-    intros (j&?&Hjl&_)%heap_array_lookup.
+    intros (j&w&?&Hjl&?&?)%heap_array_lookup.
     rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
   rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
@@ -276,14 +292,14 @@ Proof.
 Qed.
 
 Lemma heap_array_to_seq_mapsto l v (n : nat) :
-  ([∗ map] l' ↦ v ∈ heap_array l (replicate n v), l' ↦ v) -∗
+  ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.mapsto l' 1 ov) -∗
   [∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
 Proof.
   iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
   { done. }
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
-    intros (j&?&Hjl&_)%heap_array_lookup.
+    intros (j&w&?&Hjl&_)%heap_array_lookup.
     rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
   rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 0402c7eb7..51077ca0d 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -95,9 +95,9 @@ Qed.
 Lemma heap_closed_alloc σ l n w :
   0 < n →
   is_closed_val w →
-  map_Forall (λ _ v, is_closed_val v) (heap σ) →
+  map_Forall (λ _ v, from_option is_closed_val true v) (heap σ) →
   (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
-  map_Forall (λ _ v, is_closed_val v)
+  map_Forall (λ _ v, from_option is_closed_val true v)
              (heap_array l (replicate (Z.to_nat n) w) ∪ heap σ).
 Proof.
   intros Hn Hw Hσ Hl.
@@ -110,9 +110,9 @@ Proof.
     apply lookup_union_Some in Hix; last first.
     { eapply heap_array_map_disjoint;
         rewrite replicate_length Z2Nat.id; auto with lia. }
-    destruct Hix as [(?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
+    destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
                      [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
-    + rewrite !Z2Nat.id in Hlt; eauto with lia.
+    + simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
     + apply map_Forall_to_list in Hσ.
       by eapply Forall_lookup in Hσ; eauto; simpl in *.
   - apply map_Forall_to_list, Forall_forall.
@@ -122,10 +122,10 @@ Qed.
 (* The stepping relation preserves closedness *)
 Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
   is_closed_expr [] e1 →
-  map_Forall (λ _ v, is_closed_val v) σ1.(heap) →
+  map_Forall (λ _ v, from_option is_closed_val true v) σ1.(heap) →
   head_step e1 σ1 obs e2 σ2 es →
   is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
-  map_Forall (λ _ v, is_closed_val v) σ2.(heap).
+  map_Forall (λ _ v, from_option is_closed_val true v) σ2.(heap).
 Proof.
   intros Cl1 Clσ1 STEP.
   induction STEP; simpl in *; split_and!;
@@ -134,6 +134,8 @@ Proof.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
   - eapply bin_op_eval_closed; eauto; naive_solver.
   - by apply heap_closed_alloc.
+  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
+  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
   - case_match; try apply map_Forall_insert_2; by naive_solver.
 Qed.
 
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index 0aa6acf52..d4f8ca3f0 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -115,7 +115,8 @@ Definition erase_ectx (K : ectx heap_ectx_lang) : ectx heap_ectx_lang :=
 
 Definition erase_tp (tp : list expr) : list expr := erase_expr <$> tp.
 
-Definition erase_heap (h : gmap loc val) : gmap loc val := erase_val <$> h.
+Definition erase_heap (h : gmap loc (option val)) : gmap loc (option val) :=
+  (λ ov : option val, erase_val <$> ov) <$> h.
 
 Definition erase_state (σ : state) : state :=
   {| heap := erase_heap (heap σ); used_proph_id := ∅ |}.
@@ -189,17 +190,17 @@ Qed.
 Lemma lookup_erase_heap_None h l : erase_heap h !! l = None ↔ h !! l = None.
 Proof. rewrite lookup_fmap; by destruct (h !! l). Qed.
 
-Lemma lookup_erase_heap h l : erase_heap h !! l = erase_val <$> h !! l.
+Lemma lookup_erase_heap h l : erase_heap h !! l = (λ ov, erase_val <$> ov) <$> h !! l.
 Proof. by rewrite lookup_fmap. Qed.
 
 Lemma erase_heap_insert h l v :
-  erase_heap (<[l := v]> h) = <[l := erase_val v]> (erase_heap h).
+  erase_heap (<[l := Some v]> h) = <[l := Some $ erase_val v]> (erase_heap h).
 Proof.
   by rewrite /erase_heap fmap_insert.
 Qed.
 
-Lemma fmap_heap_array f l vs :
-  f <$> heap_array l vs = heap_array l (f <$> vs).
+Lemma fmap_heap_array (f : val → val) l vs :
+  (λ ov : option val, f <$> ov) <$> heap_array l vs = heap_array l (f <$> vs).
 Proof.
   revert l; induction vs as [|v vs IHvs]; intros l;
     first by rewrite /= fmap_empty.
@@ -247,41 +248,40 @@ Proof.
       rewrite ?erase_heap_insert /=; eauto using erase_state_init.
 Qed.
 Lemma erased_head_step_head_step_Load l σ v :
-  erase_heap (heap σ) !! l = Some v →
+  erase_heap (heap σ) !! l = Some (Some v) →
   head_steps_to_erasure_of (! #l) σ v (erase_state σ) [].
 Proof.
   intros Hl.
   rewrite lookup_erase_heap in Hl.
-  destruct (heap σ !! l) eqn:?; simplify_eq/=.
+  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
   eexists _, _, _, _; simpl; split; first econstructor; eauto.
 Qed.
 
-Lemma erased_head_step_head_step_Store l v σ :
-  is_Some (erase_heap (heap σ) !! l) →
-  head_steps_to_erasure_of (#l <- v) σ #()
-   {| heap := <[l:=erase_val v]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
+Lemma erased_head_step_head_step_Store l v w σ :
+  erase_heap (heap σ) !! l = Some (Some v) →
+  head_steps_to_erasure_of (#l <- w) σ #()
+   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
 Proof.
   intros Hl.
   rewrite lookup_erase_heap in Hl.
-  destruct (heap σ !! l) eqn:?; simplify_eq/=;
-           last by apply is_Some_None in Hl.
+  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
   eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
     by rewrite /state_upd_heap /erase_state /= erase_heap_insert.
 Qed.
 Lemma erased_head_step_head_step_CmpXchg l v w σ vl :
-  erase_heap (heap σ) !! l = Some vl →
+  erase_heap (heap σ) !! l = Some (Some vl) →
   vals_compare_safe vl (erase_val v) →
   head_steps_to_erasure_of
     (CmpXchg #l v w) σ
     (vl, #(bool_decide (vl = erase_val v)))%V
     (if bool_decide (vl = erase_val v)
-     then {| heap := <[l:=erase_val w]> (erase_heap (heap σ));
+     then {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ));
              used_proph_id := ∅ |}
      else erase_state σ) [].
 Proof.
   intros Hl Hvl.
   rewrite lookup_erase_heap in Hl.
-  destruct (heap σ !! l) as [u|] eqn:?; simplify_eq/=.
+  destruct (heap σ !! l) as [[u|]|] eqn:?; simplify_eq/=.
   rewrite -> vals_compare_safe_erase in Hvl.
   destruct (decide (u = v)) as [->|Hneq].
   - eexists _, _, _, _; simpl; split.
@@ -295,15 +295,15 @@ Proof.
     by rewrite erase_val_inj_iff.
 Qed.
 Lemma erased_head_step_head_step_FAA l n m σ :
-  erase_heap (heap σ) !! l = Some #n →
+  erase_heap (heap σ) !! l = Some (Some #n) →
   head_steps_to_erasure_of
     (FAA #l #m) σ #n
-    {| heap := <[l:= #(n + m)]> (erase_heap (heap σ));
+    {| heap := <[l:= Some #(n + m)]> (erase_heap (heap σ));
        used_proph_id := ∅ |} [].
 Proof.
   intros Hl.
   rewrite lookup_erase_heap in Hl.
-  destruct (heap σ !! l) as [[[]| | | |]|] eqn:?; simplify_eq/=.
+  destruct (heap σ !! l) as [[[[]| | | |]|]|] eqn:?; simplify_eq/=.
   repeat econstructor; first by eauto.
   by rewrite /state_upd_heap /erase_state /= erase_heap_insert.
 Qed.
@@ -615,7 +615,7 @@ Proof.
 Qed.
 
 Lemma head_step_erased_prim_step_CmpXchg v1 v2 σ l vl:
-  heap σ !! l = Some vl →
+  heap σ !! l = Some (Some vl) →
   vals_compare_safe vl v1 →
   ∃ e2' σ2' ef', prim_step (CmpXchg #l (erase_val v1)
                              (erase_val v2)) (erase_state σ) [] e2' σ2' ef'.
@@ -668,7 +668,7 @@ Proof.
 Qed.
 
 Lemma head_step_erased_prim_step_load σ l v:
-  heap σ !! l = Some v →
+  heap σ !! l = Some (Some v) →
   ∃ e2' σ2' ef', prim_step (! #l) (erase_state σ) [] e2' σ2' ef'.
 Proof.
   do 3 eexists; apply head_prim_step; econstructor.
@@ -676,17 +676,16 @@ Proof.
   by destruct lookup; simplify_eq.
 Qed.
 
-Lemma head_step_erased_prim_step_store σ l v:
-  is_Some (heap σ !! l) →
-  ∃ e2' σ2' ef', prim_step (#l <- erase_val v) (erase_state σ) [] e2' σ2' ef'.
+Lemma head_step_erased_prim_step_store σ l v w :
+  heap σ !! l = Some (Some v) →
+  ∃ e2' σ2' ef', prim_step (#l <- erase_val w) (erase_state σ) [] e2' σ2' ef'.
 Proof.
-  intros [w Hw].
-  do 3 eexists; apply head_prim_step; econstructor.
+  intros Hw. do 3 eexists; apply head_prim_step; econstructor.
   rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
 Qed.
 
 Lemma head_step_erased_prim_step_FAA σ l n n':
-  heap σ !! l = Some #n →
+  heap σ !! l = Some (Some #n) →
   ∃ e2' σ2' ef', prim_step (FAA #l #n') (erase_state σ) [] e2' σ2' ef'.
 Proof.
   intros Hl.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 346b024d2..8aa59f739 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -10,7 +10,7 @@ Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
   iMod (gen_heap_init σ.(heap)) as (?) "Hh".
-  iMod (inv_heap_init loc val) as (?) ">Hi".
+  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.
   iExists
-- 
GitLab