[new] and [delete] : thin wrappers around Alloc and Free, to allow 0-size allocations.

_CoqProject

@@ -17,6 +17,7 @@ theories/lang/heap.v
 theories/lang/lang.v
 theories/lang/lifting.v
 theories/lang/memcpy.v
+theories/lang/new_delete.v
 theories/lang/notation.v
 theories/lang/proofmode.v
 theories/lang/races.v

theories/lang/new_delete.v

+From iris.base_logic.lib Require Import namespaces.
+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode.
+
+Definition new : val :=
+  λ: ["n"],
+    if: "n" ≤ #0 then #((42%positive, 1337):loc)
+    else Alloc "n".
+Opaque new.
+
+Definition delete : val :=
+  λ: ["n"; "loc"],
+    if: "n" ≤ #0 then #()
+    else Free "n" "loc".
+Opaque delete.
+
+Section specs.
+  Context `{heapG Σ}.
+
+  Lemma wp_new E n:
+    ↑heapN ⊆ E → 0 ≤ n →
+    {{{ heap_ctx }}} new [ #n ] @ E
+    {{{ l vl, RET LitV $ LitLoc l;
+        ⌜n = length vl⌝ ∗ (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ vl }}}.
+  Proof.
+    iIntros (? ? Φ) "#Hinv HΦ". wp_lam. wp_op; intros ?.
+    - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
+      rewrite heap_mapsto_vec_nil. auto.
+    - wp_if. wp_alloc l vl as "H↦" "H†". iApply  "HΦ". iFrame. auto.
+  Qed.
+
+  Lemma wp_delete E (n:Z) l vl :
+    ↑heapN ⊆ E → n = length vl →
+    {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ (▷ †l…(length vl) ∨ ⌜n = 0⌝) }}}
+      delete [ #n; #l] @ E
+    {{{ RET LitV LitUnit; True }}}.
+  Proof.
+    iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
+      wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
+  Qed.
+End specs.
\ No newline at end of file

theories/typing/own.v

 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.lang Require Export new_delete.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_incl typing product.
 
@@ -21,7 +22,8 @@ Section own.
 
             Since this assertion is timeless, this should not cause
             problems. *)
-         (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
+         (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗
+                   ▷ (†{q}l…ty.(ty_size) ∨ ⌜ty.(ty_size) = 0%nat⌝))%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
             □ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
@@ -82,29 +84,34 @@ Section own.
       iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
   Qed.
 
-  Lemma typed_alloc ρ (n : nat):
-    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (Π(replicate n uninit))).
+  Lemma typed_new ρ (n : nat):
+    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own 1 (Π(replicate n uninit))).
   Proof.
-    iIntros (Hn tid) "!#(#HEAP&_&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
-    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitR "H†".
+    iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
+    iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
+    rewrite Nat2Z.id. iSplitR "H†".
     - iExists vl. iFrame.
       match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
       clear Hn. apply (inj Z.of_nat) in Hlen. subst.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate n uninit)) = n) as ->; last done.
-      clear. simpl. induction n. done. rewrite /= IHn //.
+    - assert (ty_size (Π (replicate n uninit)) = n) as ->.
+      { clear. induction n; rewrite //= IHn //. }
+      iDestruct "H†" as "[?|%]". by auto. rewrite (inj Z.of_nat n 0%nat); auto.
   Qed.
 
-  Lemma typed_free ty (ν : expr):
-    typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
+  Lemma typed_delete ty (ν : expr):
+    typed_step (ν ◁ own 1 ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
   Proof.
     iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
     iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
     rewrite has_type_value.
     iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
-    rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
+    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
+    iApply (wp_delete with "[-]"); try by auto.
+    iFrame "∗#". iDestruct "H†" as "[?|Hlen]". by auto.
+    iDestruct "Hlen" as %->. auto.
   Qed.
 
   Lemma update_strong ty1 ty2 q:
@@ -151,4 +158,4 @@ Section own.
     - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
       clear. induction ty.(ty_size). done. by apply (f_equal S).
   Qed.
-End own.
\ No newline at end of file
+End own.