add lifting lemma and tactic for single-location Free

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,6 +145,7 @@ 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;

theories/heap_lang/lifting.v

@@ -348,6 +348,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.

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_load: not a 'wp'"
+  end.
+
 Tactic Notation "wp_load" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in