diff --git a/CHANGELOG.md b/CHANGELOG.md
index d9dda024277d5ae9097d786793cb706a6e689168..beddcceeeea37ca1fca4186b1d6c68a2c7b4bb1b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,8 +23,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 **Changes in heap_lang:**
 
+* Added support for deallocation of locations via the `Free` operation.
 * Added a fraction to the heap_lang `array` assertion.
-* Added array_copy library for copying and cloning arrays.
+* Added `lib.array` module for deallocating, copying and cloning arrays.
 * Added the ghost state for "invariant locations" to `heapG`.  This affects the
   statement of `heap_adequacy`, which is now responsible for initializing the
   "invariant locations" invariant.
diff --git a/_CoqProject b/_CoqProject
index 894e7004117ad53b1f2bcaf1c067f5142ca5e24e..aa95ee16316aa7da30fe22d61a7809e17239e31b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -125,7 +125,7 @@ theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
 theories/heap_lang/lib/diverge.v
 theories/heap_lang/lib/arith.v
-theories/heap_lang/lib/array_copy.v
+theories/heap_lang/lib/array.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 8d19418d3e9f263a36b63e9848174f844e820406..9fb599d4c42e6e27ba56f5f3866a577a28e7a963 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -113,6 +113,15 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  I : val → Prop
+  Heq : ∀ v : val, I v ↔ I #true
+  ============================
+  ⊢ l ↦□ (λ _ : val, I #true)
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 6b88e361c6150d1fec7b32d21c915a084d817de0..efed8387ea57a950617af6781fabef9ea8e46f84 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -218,15 +218,35 @@ Section tests.
     iIntros "[$ _]". (* splits the fraction, not the app *)
   Qed.
 
+
+  Lemma test_wp_free l v :
+    {{{ l ↦ v }}} Free #l {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
+  Qed.
+
+  Lemma test_twp_free l v :
+    [[{ l ↦ v }]] Free #l [[{ RET #(); True }]].
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
+  Qed.
 End tests.
 
-Section notation_tests.
+Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
   Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
-End notation_tests.
+
+  (* Make sure [setoid_rewrite] works. *)
+  Lemma inv_mapsto_setoid_rewrite (l : loc) (I : val → Prop) :
+    (∀ v, I v ↔ I #true) →
+    ⊢ l ↦□ (λ v, I v).
+  Proof.
+    iIntros (Heq). setoid_rewrite Heq. Show.
+  Abort.
+End inv_mapsto_tests.
 
 Section printing_tests.
   Context `{!heapG Σ}.
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 20311ce9739af67bdf5f4bc4fb3b31a11c914809..230ce99431a926d5e84ff2d78df2d298696b4c58 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -14,11 +14,10 @@ it is that they are reading in that case. In that extreme case, the invariant
 may just be [True].
 
 Since invariant locations cannot be deallocated, they only make sense when
-modelling languages with garbage collection.  Note that heap_lang does not
-actually have explicit dealloaction. However, the proof rules we provide for
-heap operations currently are conservative in the sense that they do not expose
-this fact.  By making "invariant" locations a separate assertion, we can keep
-all the other proofs that do not need it conservative.  *)
+modeling languages with garbage collection.  HeapLang can be used to model
+either language by choosing whether or not to use the [Free] operation.  By
+using a separate assertion [inv_mapsto_own] for "invariant" locations, we can
+keep all the other proofs that do not need it conservative.  *)
 
 Definition inv_heapN: namespace := nroot .@ "inv_heap".
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 2b6366bb2ab2e2e66b6d56402474eb130768903d..bce15e435908cceec9018bb8ff1fb6cf07ee72d5 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 0df1c405306fb06b5b91fc8ebc849041a0bab73f..4d821594cc685c12968115fc6ea32470ae6bdf48 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -7,12 +7,21 @@ 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
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
   useless unless the user let-expands [b].
 
+- Even after deallocating a location, the heap remembers that these locations
+  were previously allocated and makes sure they do not get reused. This is
+  necessary to ensure soundness of the [meta] feature provided by [gen_heap].
+  Also, unlike in languages like C, allocated and deallocated "blocks" do not
+  have to match up: you can allocate a large array of locations and then
+  deallocate a hole out of it in the middle.
+
 - For prophecy variables, we annotate the reduction steps with an "observation"
   and tweak adequacy such that WP knows all future observations. There is
   another possible choice: Use non-deterministic choice when creating a prophecy
@@ -100,6 +109,7 @@ Inductive expr :=
   | Fork (e : expr)
   (* Heap *)
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
+  | Free (e : expr)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
@@ -185,9 +195,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;
 }.
 
@@ -233,6 +243,8 @@ Proof.
      | Fork e, Fork e' => cast_if (decide (e = e'))
      | AllocN e1 e2, AllocN e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | Free e, Free e' =>
+        cast_if (decide (e = e'))
      | Load e, Load e' => cast_if (decide (e = e'))
      | Store e1 e2, Store e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
@@ -316,12 +328,13 @@ Proof.
      | Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
      | Fork e => GenNode 12 [go e]
      | AllocN e1 e2 => GenNode 13 [go e1; go e2]
-     | Load e => GenNode 14 [go e]
-     | Store e1 e2 => GenNode 15 [go e1; go e2]
-     | CmpXchg e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
-     | FAA e1 e2 => GenNode 17 [go e1; go e2]
-     | NewProph => GenNode 18 []
-     | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
+     | Free e => GenNode 14 [go e]
+     | Load e => GenNode 15 [go e]
+     | Store e1 e2 => GenNode 16 [go e1; go e2]
+     | CmpXchg e0 e1 e2 => GenNode 17 [go e0; go e1; go e2]
+     | FAA e1 e2 => GenNode 18 [go e1; go e2]
+     | NewProph => GenNode 19 []
+     | Resolve e0 e1 e2 => GenNode 20 [go e0; go e1; go e2]
      end
    with gov v :=
      match v with
@@ -351,12 +364,13 @@ Proof.
      | GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
      | GenNode 12 [e] => Fork (go e)
      | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
-     | GenNode 14 [e] => Load (go e)
-     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
-     | GenNode 16 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
-     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
-     | GenNode 18 [] => NewProph
-     | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
+     | GenNode 14 [e] => Free (go e)
+     | GenNode 15 [e] => Load (go e)
+     | GenNode 16 [e1; e2] => Store (go e1) (go e2)
+     | GenNode 17 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
+     | GenNode 18 [e1; e2] => FAA (go e1) (go e2)
+     | GenNode 19 [] => NewProph
+     | GenNode 20 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
      | _ => Val $ LitV LitUnit (* dummy *)
      end
    with gov v :=
@@ -371,7 +385,7 @@ Proof.
    for go).
  refine (inj_countable' enc dec _).
  refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- - destruct e as [v| | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
+ - destruct e as [v| | | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
      [exact (gov v)|done..].
  - destruct v; by f_equal.
 Qed.
@@ -405,6 +419,7 @@ Inductive ectx_item :=
   | CaseCtx (e1 : expr) (e2 : expr)
   | AllocNLCtx (v2 : val)
   | AllocNRCtx (e1 : expr)
+  | FreeCtx
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
@@ -441,6 +456,7 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocNLCtx v2 => AllocN e (Val v2)
   | AllocNRCtx e1 => AllocN e1 e
+  | FreeCtx => Free e
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
@@ -473,6 +489,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
   | Fork e => Fork (subst x v e)
   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
+  | Free e => Free (subst x v e)
   | Load e => Load (subst x v e)
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
@@ -544,7 +561,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 +569,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 & w & ? & -> & -> & 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&w&?&->&?&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
   move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
 Qed.
 
@@ -596,7 +613,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.
@@ -641,29 +658,35 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
                []
+  | FreeS l v σ :
+     σ.(heap) !! l = Some $ Some v →
+     head_step (Free (Val $ LitV $ LitLoc l)) σ
+               []
+               (Val $ LitV LitUnit) (state_upd_heap <[l:=None]> σ)
+               []
   | 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/array_copy.v b/theories/heap_lang/lib/array.v
similarity index 65%
rename from theories/heap_lang/lib/array_copy.v
rename to theories/heap_lang/lib/array.v
index 1125d22bc496ae33af00267d42c04562bd9310e5..364c806d40ebfd99d70afc81161e86847a6f7332 100644
--- a/theories/heap_lang/lib/array_copy.v
+++ b/theories/heap_lang/lib/array.v
@@ -4,18 +4,28 @@ From iris.heap_lang Require Export lang array.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
-(** Implement [array_copy_to], a function which copies to an array in-place.
+(** Provides some array utilities:
 
-Using [array_copy_to] we also implement [array_clone], which allocates a fresh
-array and copies to it. *)
+* [array_free], to deallocate an entire array in one go.
+* [array_copy_to], a function which copies to an array in-place.
+* Using [array_copy_to] we also implement [array_clone], which allocates a fresh
+array and copies to it.
 
-Definition array_copy_to: val :=
+*)
+
+Definition array_free : val :=
+  rec: "freeN" "ptr" "n" :=
+    if: "n" ≤ #0 then #()
+    else Free "ptr";;
+         "freeN" ("ptr" +â‚— #1) ("n" - #1).
+
+Definition array_copy_to : val :=
   rec: "array_copy_to" "dst" "src" "n" :=
     if: "n" ≤ #0 then #()
     else "dst" <- !"src";;
          "array_copy_to" ("dst" +â‚— #1) ("src" +â‚— #1) ("n" - #1).
 
-Definition array_clone: val :=
+Definition array_clone : val :=
   λ: "src" "n",
     let: "dst" := AllocN "n" #() in
     array_copy_to "dst" "src" "n";;
@@ -24,7 +34,25 @@ Definition array_clone: val :=
 Section proof.
   Context `{!heapG Σ}.
 
-  Theorem twp_array_copy_to stk E (dst src: loc) vdst vsrc q (n:Z) :
+  Lemma twp_array_free s E l vs (n : Z) :
+    n = length vs →
+    [[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
+  Proof.
+    iIntros (Hlen Φ) "Hl HΦ".
+    iInduction vs as [|v vs] "IH" forall (l n Hlen); subst n; wp_rec; wp_pures.
+    { iApply "HΦ". done. }
+    iDestruct (array_cons with "Hl") as "[Hv Hl]".
+    wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
+  Qed.
+  Lemma wp_array_free s E l vs (n : Z) :
+    n = length vs →
+    {{{ l ↦∗ vs }}} array_free #l #n @ s; E {{{ RET #(); True }}}.
+  Proof.
+    iIntros (? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
+    iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  Qed.
+
+  Theorem twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
     [[{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }]]
       array_copy_to #dst #src #n @ stk; E
@@ -41,7 +69,7 @@ Section proof.
     iIntros "[Hvdst Hvsrc]".
     iApply "HΦ"; by iFrame.
   Qed.
-  Theorem wp_array_copy_to stk E (dst src: loc) vdst vsrc q (n:Z) :
+  Theorem wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
     {{{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }}}
       array_copy_to #dst #src #n @ stk; E
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 7e847e3698bc62afe2a5fd9ed71e5a1386659370..6a762620f87bea32bbe36bda152b90e8911d6cd0 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -9,6 +9,7 @@ Set Default Proof Using "Type".
 Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
+  free : val;
   load : val;
   store : val;
   cmpxchg : val;
@@ -23,6 +24,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- operation specs -- *)
   alloc_spec (v : val) :
     {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
+  free_spec (l : loc) (v : val) :
+    {{{ mapsto l 1 v }}} free #l {{{ l, RET #l; True }}};
   load_spec (l : loc) :
     ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (w : val) :
@@ -81,6 +84,8 @@ End derived.
 (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
 Definition primitive_alloc : val :=
   λ: "v", ref "v".
+Definition primitive_free : val :=
+  λ: "v", Free "v".
 Definition primitive_load : val :=
   λ: "l", !"l".
 Definition primitive_store : val :=
@@ -97,6 +102,12 @@ Section proof.
     iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done.
   Qed.
 
+  Lemma primitive_free_spec (l : loc) (v : val) :
+    {{{ l ↦ v }}} primitive_free #l {{{ l, RET #l; True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_lam. wp_free. iApply "HΦ". done.
+  Qed.
+
   Lemma primitive_load_spec (l : loc) :
     ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
     <<< l ↦{q} v, RET v >>>.
@@ -134,7 +145,8 @@ End proof.
      (using [Explicit Instance]). *)
 Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
   {| alloc_spec := primitive_alloc_spec;
+     free_spec := primitive_free_spec;
      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 584d4a340de71e560c1d41e298352475380c52eb..5cb0b05685e4be5b742e7cbcfee673669be313f3 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) Σ;
 }.
 
@@ -22,20 +22,35 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
   fork_post _ := True%I;
 }.
 
-(** Override the notations so that scopes and coercions work out *)
-Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
+(** Since we use an [option val] instance of [gen_heap], we need to overwrite
+the notations.  That also helps for scopes and coercions. *)
+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)
+(** Same for [gen_inv_heap], except that these are higher-order notations so to
+make setoid rewriting in the predicate [I] work we need actual definitions
+here. *)
+Section definitions.
+  Context `{!heapG Σ}.
+  Definition inv_mapsto_own (l : loc) (v : val) (I : val → Prop) : iProp Σ :=
+    inv_mapsto_own l (Some v) (from_option I False).
+  Definition inv_mapsto (l : loc) (I : val → Prop) : iProp Σ :=
+    inv_mapsto l (from_option I False).
+End definitions.
+
+Instance: Params (@inv_mapsto_own) 4 := {}.
+Instance: Params (@inv_mapsto) 3 := {}.
+
+Notation inv_heap_inv := (inv_heap_inv loc (option val)).
+Notation "l ↦□ I" := (inv_mapsto l I%stdpp%type)
   (at level 20, format "l  ↦□  I") : bi_scope.
-Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
-  (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
-Notation inv_heap_inv := (inv_heap_inv loc val).
+Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
+  (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
 (** 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 +272,81 @@ Proof.
 Qed.
 
 (** Heap *)
+
+(** We need to adjust the [gen_heap] and [gen_inv_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.
+
+Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
+Proof. apply mapsto_valid. Qed.
+Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
+Proof. apply mapsto_valid_2. Qed.
+Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+  ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Proof. apply mapsto_mapsto_ne. Qed.
+
+Global Instance inv_mapsto_own_proper l v :
+  Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).
+Proof.
+  intros I1 I2 HI. rewrite /inv_mapsto_own. f_equiv=>-[w|]; last done.
+  simpl. apply HI.
+Qed.
+Global Instance inv_mapsto_proper l :
+  Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto l).
+Proof.
+  intros I1 I2 HI. rewrite /inv_mapsto. f_equiv=>-[w|]; last done.
+  simpl. apply HI.
+Qed.
+
+Lemma make_inv_mapsto l v (I : val → Prop) E :
+  ↑inv_heapN ⊆ E →
+  I v →
+  inv_heap_inv -∗ l ↦ v ={E}=∗ l ↦_I v.
+Proof. iIntros (??) "#HI Hl". iApply make_inv_mapsto; done. Qed.
+Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦□ I.
+Proof. apply inv_mapsto_own_inv. Qed.
+
+Lemma inv_mapsto_own_acc_strong E :
+  ↑inv_heapN ⊆ E →
+  inv_heap_inv ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦_I v -∗
+    (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
+      inv_mapsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
+Proof.
+  iIntros (?) "#Hinv".
+  iMod (inv_mapsto_own_acc_strong with "Hinv") as "Hacc"; first done.
+  iIntros "!>" (l v I) "Hl". iDestruct ("Hacc" with "Hl") as "(% & Hl & Hclose)".
+  iFrame "%∗". iIntros (w) "% Hl". iApply "Hclose"; done.
+Qed.
+
+Lemma inv_mapsto_own_acc E l v I:
+  ↑inv_heapN ⊆ E →
+  inv_heap_inv -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
+    (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
+Proof.
+  iIntros (?) "#Hinv Hl".
+  iMod (inv_mapsto_own_acc with "Hinv Hl") as "(% & Hl & Hclose)"; first done.
+  iFrame "%∗". iIntros "!>" (w) "% Hl". iApply "Hclose"; done.
+Qed.
+
+Lemma inv_mapsto_acc l I E :
+  ↑inv_heapN ⊆ E →
+  inv_heap_inv -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
+Proof.
+  iIntros (?) "#Hinv Hl".
+  iMod (inv_mapsto_acc with "Hinv Hl") as ([v|]) "(% & Hl & Hclose)"; [done| |done].
+  iIntros "!>". iExists (v). 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 +357,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 +366,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.
@@ -332,6 +422,24 @@ Proof.
   iApply twp_alloc; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
 Qed.
 
+Lemma twp_free s E l v :
+  [[{ l ↦ v }]] Free (Val $ LitV $ LitLoc l) @ s; E
+  [[{ RET LitV LitUnit; True }]].
+Proof.
+  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
+Qed.
+Lemma wp_free s E l v :
+  {{{ ▷ l ↦ v }}} Free (Val $ LitV (LitLoc l)) @ s; E
+  {{{ RET LitV LitUnit; True }}}.
+Proof.
+  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iApply (twp_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+Qed.
+
 Lemma twp_load s E l q v :
   [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
 Proof.
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 0402c7eb7881058fefcaf0a73a16e8bcd02c1858..0859f72697bf77ceb005cfa330cc3431dc39d39a 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -10,7 +10,7 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
   | Val v => is_closed_val v
   | Var x => bool_decide (x ∈ X)
   | Rec f x e => is_closed_expr (f :b: x :b: X) e
-  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
      is_closed_expr X e
   | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
@@ -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.
 
@@ -154,6 +156,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | Fork e => Fork (subst_map vs e)
   | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
+  | Free e => Free (subst_map vs e)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index cb9c1a2afbd6c7d4dc53cc9d3de4dfb3fa557c33..dea83e0950224b0f60fe1ef108635fdbdaa5045b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -237,6 +237,32 @@ Proof.
   apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
 Qed.
 
+Lemma tac_wp_free Δ Δ' Δ'' s E i K l v Φ :
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  envs_delete false i false Δ' = Δ'' →
+  envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ? Hlk <- Hfin.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
+  apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
+Qed.
+Lemma tac_twp_free Δ Δ' s E i K l v Φ :
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
+  envs_delete false i false Δ = Δ' →
+  envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E [{ Φ }]).
+Proof.
+  rewrite envs_entails_eq=> Hlk <- Hfin.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_free.
+  rewrite envs_lookup_split //; simpl.
+  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
+  apply sep_mono_r, wand_intro_r. rewrite right_id //.
+Qed.
+
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
@@ -492,6 +518,30 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
 Tactic Notation "wp_alloc" ident(l) :=
   wp_alloc l as "?".
 
+Tactic Notation "wp_free" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_free: cannot find" l "↦ ?" in
+  wp_pures;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free _ _ _ _ _ _ K))
+      |fail 1 "wp_free: cannot find 'Free' in" e];
+    [iSolveTC
+    |solve_mapsto ()
+    |pm_reflexivity
+    |wp_finish]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_free _ _ _ _ _ K))
+      |fail 1 "wp_free: cannot find 'Free' in" e];
+    [solve_mapsto ()
+    |pm_reflexivity
+    |wp_finish]
+  | _ => fail "wp_free: not a 'wp'"
+  end.
+
 Tactic Notation "wp_load" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index 0aa6acf52ae0fa375ff96a0cd09da2bb3caadc28..ca5671830b9c4ee7e80cfa383c4266d50a99de73 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -40,6 +40,7 @@ Fixpoint erase_expr (e : expr) : expr :=
   | Case e0 e1 e2 => Case (erase_expr e0) (erase_expr e1) (erase_expr e2)
   | Fork e => Fork (erase_expr e)
   | AllocN e1 e2 => AllocN (erase_expr e1) (erase_expr e2)
+  | Free e => Free (erase_expr e)
   | Load e => Load (erase_expr e)
   | Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
   | CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
@@ -93,6 +94,7 @@ Fixpoint erase_ectx_item (Ki : ectx_item) : list ectx_item :=
   | CaseCtx e1 e2 => [CaseCtx (erase_expr e1) (erase_expr e2)]
   | AllocNLCtx v2 => [AllocNLCtx (erase_val v2)]
   | AllocNRCtx e1 => [AllocNRCtx (erase_expr e1)]
+  | FreeCtx => [FreeCtx]
   | LoadCtx => [LoadCtx]
   | StoreLCtx v2 => [StoreLCtx (erase_val v2)]
   | StoreRCtx e1 => [StoreRCtx (erase_expr e1)]
@@ -115,7 +117,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 +192,22 @@ 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).
+Lemma erase_heap_insert_Some h l v :
+  erase_heap (<[l := Some v]> h) = <[l := Some $ erase_val v]> (erase_heap h).
+Proof.
+  by rewrite /erase_heap fmap_insert.
+Qed.
+Lemma erase_heap_insert_None h l v :
+  erase_heap (<[l := None]> h) = <[l := None]> (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.
@@ -246,48 +254,57 @@ Proof.
     first econstructor; try setoid_rewrite <- lookup_erase_heap_None;
       rewrite ?erase_heap_insert /=; eauto using erase_state_init.
 Qed.
+Lemma erased_head_step_head_step_Free l v σ :
+  erase_heap (heap σ) !! l = Some (Some v) →
+  head_steps_to_erasure_of (Free #l) σ #()
+   {| heap := <[l:=None]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
+Proof.
+  intros Hl.
+  rewrite lookup_erase_heap in Hl.
+  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
+  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
+  rewrite /state_upd_heap /erase_state /= erase_heap_insert_None //.
+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.
+  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
 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.
     { econstructor; eauto. }
     rewrite !bool_decide_eq_true_2; eauto using erase_val_inj_iff; [].
-    rewrite -?erase_heap_insert.
+    rewrite -?erase_heap_insert_Some.
     split_and!; auto.
   - eexists _, _, _, _; simpl; split.
     { econstructor; eauto. }
@@ -295,17 +312,17 @@ 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.
+  by rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some.
 Qed.
 
 (** When the erased program makes a head step, so does the original program. *)
@@ -329,6 +346,7 @@ Proof.
   eauto using erased_head_step_head_step_rec,
     erased_head_step_head_step_NewProph,
     erased_head_step_head_step_AllocN,
+    erased_head_step_head_step_Free,
     erased_head_step_head_step_Load,
     erased_head_step_head_step_Store,
     erased_head_step_head_step_CmpXchg,
@@ -615,7 +633,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'.
@@ -667,8 +685,16 @@ Proof.
   intros; rewrite lookup_erase_heap_None; eauto.
 Qed.
 
+Lemma head_step_erased_prim_step_free σ l v :
+  heap σ !! l = Some (Some v) →
+  ∃ e2' σ2' ef', prim_step (Free #l) (erase_state σ) [] e2' σ2' ef'.
+Proof.
+  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_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 +702,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.
@@ -709,6 +734,7 @@ Proof.
                 head_step_erased_prim_step_un_op,
                 head_step_erased_prim_step_bin_op,
                 head_step_erased_prim_step_allocN,
+                head_step_erased_prim_step_free,
                 head_step_erased_prim_step_load,
                 head_step_erased_prim_step_store,
                 head_step_erased_prim_step_FAA;
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 368f202fe40127e70e64b10c6bf0bf755bef4cab..c3325b8dd09014e4bd41247f0d138379b93c37b7 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -32,6 +32,7 @@ Ltac reshape_expr e tac :=
     | Case ?e0 ?e1 ?e2                => add_item (CaseCtx e1 e2) vs K e0
     | AllocN ?e (Val ?v)              => add_item (AllocNLCtx v) vs K e
     | AllocN ?e1 ?e2                  => add_item (AllocNRCtx e1) vs K e2
+    | Free ?e                         => add_item FreeCtx vs K e
     | Load ?e                         => add_item LoadCtx vs K e
     | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
     | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 346b024d2abdd439457b38ac2ca2ff42ba5b6e48..8aa59f739f02b93d25b6a25c87847cb1aa6b39ee 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