Fix build by indexing own by the full size and defining [freeable_sz].

Warning : splitting a own of a product only works if the list of types is non-empty.

theories/lang/new_delete.v

@@ -31,7 +31,7 @@ Section specs.
 
   Lemma wp_delete E (n:Z) l vl :
     ↑heapN ⊆ E → n = length vl →
-    {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ (▷ †l…(length vl) ∨ ⌜n = 0⌝) }}}
+    {{{ heap_ctx ∗ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
       delete [ #n; #l] @ E
     {{{ RET LitV LitUnit; True }}}.
   Proof.

theories/typing/own.v

+From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
@@ -13,7 +14,37 @@ Section own.
     {| st_size := 1; st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
   Next Obligation. done. Qed.
 
-  Program Definition own (q : Qp) (ty : type) :=
+  Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
+    match sz, n return _ with
+    | 0%nat, _ => True
+    | _, 0%nat => False
+    | sz, n => †{mk_Qp (sz / n) _}l…sz
+    end%I.
+  Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
+  Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
+  Proof. destruct sz, n; apply _. Qed.
+
+  Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ (†{1}l…n ∨ ⌜Z.of_nat n = 0⌝)%I.
+  Proof.
+    destruct n.
+    - iSplit; iIntros "H /="; auto.
+    - assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
+      rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= Qcmult_inv_r //.
+  Qed.
+
+  Lemma freeable_sz_split n sz1 sz2 l :
+    freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc l sz1) ⊣⊢
+                freeable_sz n (sz1 + sz2) l.
+  Proof.
+    destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
+    - by rewrite left_id shift_loc_0.
+    - by rewrite right_id Nat.add_0_r.
+    - iSplit. by iIntros "[[]?]". by iIntros "[]".
+    - rewrite heap_freeable_op_eq. f_equiv. apply Qp_eq.
+      rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
+  Qed.
+
+  Program Definition own (n : nat) (ty : type) :=
     {| ty_size := 1;
        ty_own tid vl :=
          (* We put a later in front of the †{q}, because we cannot use
@@ -23,7 +54,7 @@ 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) ∨ ⌜ty.(ty_size) = 0%nat⌝))%I;
+                   ▷ freeable_sz n ty.(ty_size) l)%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
             □ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
@@ -67,8 +98,8 @@ Section own.
       by iApply (ty.(ty_shr_mono) with "LFT Hκ").
   Qed.
 
-  Lemma ty_incl_own ρ ty1 ty2 q :
-    ty_incl ρ ty1 ty2 → ty_incl ρ (own q ty1) (own q ty2).
+  Lemma ty_incl_own n ty1 ty2 ρ :
+    ty_incl ρ ty1 ty2 → ty_incl ρ (own n ty1) (own n ty2).
   Proof.
     iIntros (Hincl tid) "#LFT H/=". iMod (Hincl with "LFT H") as "[#Howni #Hshri]".
     iModIntro. iSplit; iIntros "!#*H".
@@ -85,7 +116,7 @@ Section own.
   Qed.
 
   Lemma typed_new ρ (n : nat):
-    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own 1 (Π(replicate n uninit))).
+    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (Π(replicate n uninit))).
   Proof.
     iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
     iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
@@ -97,11 +128,11 @@ Section own.
       iExists [v], vl. iSplit. done. by iSplit.
     - 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.
+      by rewrite freeable_sz_full.
   Qed.
 
   Lemma typed_delete ty (ν : expr):
-    typed_step (ν ◁ own 1 ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
+    typed_step (ν ◁ own ty.(ty_size) ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
   Proof.
     iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
     iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
@@ -110,13 +141,12 @@ Section own.
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
     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.
+    rewrite freeable_sz_full. by iFrame.
   Qed.
 
-  Lemma update_strong ty1 ty2 q:
+  Lemma update_strong ty1 ty2 n:
     ty1.(ty_size) = ty2.(ty_size) →
-    update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
+    update ty1 (λ ν, ν ◁ own n ty2)%P (λ ν, ν ◁ own n ty1)%P.
   Proof.
     iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "H◁").
     iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
@@ -127,8 +157,8 @@ Section own.
     iExists _. iSplit. done. iFrame. iExists _. iFrame.
   Qed.
 
-  Lemma consumes_copy_own ty q:
-    Copy ty → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
+  Lemma consumes_copy_own ty n:
+    Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
   Proof.
     iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
     iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
@@ -140,9 +170,9 @@ Section own.
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
-  Lemma consumes_move ty q:
-    consumes ty (λ ν, ν ◁ own q ty)%P
-             (λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
+  Lemma consumes_move ty n:
+    consumes ty (λ ν, ν ◁ own n ty)%P
+             (λ ν, ν ◁ own n (Π(replicate ty.(ty_size) uninit)))%P.
   Proof.
     iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
     iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.

theories/typing/product_split.v

@@ -13,17 +13,17 @@ Section product_split.
     | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
     end.
 
-  Lemma perm_split_own_prod2 ty1 ty2 (q1 q2 : Qp) ν :
-    ν ◁ own (q1 + q2) (product2 ty1 ty2) ⇔
-      ν ◁ own q1 ty1 ∗ ν +ₗ #ty1.(ty_size) ◁ own q2 ty2.
+  Lemma perm_split_own_prod2 ty1 ty2 n ν :
+    ν ◁ own n (product2 ty1 ty2) ⇔
+      ν ◁ own n ty1 ∗ ν +ₗ #ty1.(ty_size) ◁ own n ty2.
   Proof.
     rewrite /has_type /own /sep /=.
     destruct (eval_expr ν) as [[[]|?]|]; last first; split; iIntros (tid) "_ H/=";
       (try by iDestruct "H" as "[_ []]"); (try by iDestruct "H" as (l) "[% _]").
     { by auto. }
-    - iDestruct "H" as (l') "(EQ & H & H†)". iDestruct "EQ" as %[=<-].
-      iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)".
-      subst. rewrite heap_mapsto_vec_app -heap_freeable_op_eq.
+    - iDestruct "H" as (l') "(EQ & H & >H†)". iDestruct "EQ" as %[=<-].
+      iDestruct "H" as (vl) "[>H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)".
+      subst. rewrite heap_mapsto_vec_app -freeable_sz_split.
       iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
       iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
       { iNext. by iApply ty_size_eq. }
@@ -33,7 +33,7 @@ Section product_split.
     - iDestruct "H" as "[H1 H2]".
       iDestruct "H1" as (l') "(EQ & H↦1 & H†1)". iDestruct "EQ" as %[=<-].
       iDestruct "H2" as (l') "(EQ & H↦2 & H†2)". iDestruct "EQ" as %[=<-].
-      iExists l. iSplitR. done. rewrite -heap_freeable_op_eq. iFrame.
+      iExists l. iSplitR. done. rewrite -freeable_sz_split. iFrame.
       iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
       iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
       iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
@@ -41,49 +41,32 @@ Section product_split.
       iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
   Qed.
 
-  Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) ν :
-    length tyl = length ql →
-    foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
-    ν ◁ own q (Π tyl) ⇔
+  Lemma perm_split_own_prod tyl n ν :
+    tyl ≠ [] →
+    ν ◁ own n (Π tyl) ⇔
       foldr (λ qtyoffs acc,
-             ν +ₗ #(qtyoffs.2.2:nat) ◁ own (qtyoffs.1) (qtyoffs.2.1) ∗ acc)
-            ⊤ (combine ql (combine_offs tyl 0)).
+             ν +ₗ #(qtyoffs.2:nat) ◁ own n (qtyoffs.1) ∗ acc)
+            ⊤ (combine_offs tyl 0).
   Proof.
-    revert q tyl ν. induction ql as [|q0 [|q1 ql] IH]=>q tyl ν Hlen Hq.
-    { destruct q. intros. simpl in *. by subst. }
-    - destruct tyl as [|ty0 [|ty1 tyl]]; try done. simpl in *.
-      assert (q0 = q) as ->. { apply Qp_eq. by rewrite -Hq Qcplus_0_r. }
-      rewrite /has_type /sep /=.
+    intros ?. revert ν. rewrite /product /=. induction tyl as [|ty tyl IH]=>ν. done.
+    rewrite /= perm_split_own_prod2. destruct tyl.
+    - rewrite /has_type /sep /=.
       destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
-        (try by iDestruct "H" as "[[] _]"); (try by iDestruct "H" as (l) "[% _]");
-        (try by auto); rewrite (shift_loc_0 l) Nat.add_0_r.
-      + iSplitL; last done. iExists _. iSplitR. done.
-        iDestruct "H" as (l') "[Heq [H↦ H†]]". iDestruct "Heq" as %[=<-].
-        iDestruct "H↦" as (vl) "[H↦ H]".
-        iDestruct "H" as (vl1 vl2) "(>% & Hown & >%)". subst.
-        rewrite app_nil_r. iFrame. iExists _. by iFrame.
-      + iExists l. iSplitR. done.
-        iDestruct "H" as "[H _]". iDestruct "H" as (l') "[Heq [H↦ H†]]".
-        iDestruct "Heq" as %[=<-]. iFrame. iDestruct "H↦" as (vl) "[H↦ Hown]".
-        iExists vl. iFrame. iExists vl, []. iFrame. rewrite app_nil_r. auto.
-    - destruct tyl as [|ty0 tyl]. done.
-      assert (Hpos : (0 < foldr (λ (q : Qp) acc, (q + acc)%Qc) 0%Qc (q1 :: ql))%Qc).
-      { apply Qcplus_pos_nonneg. apply Qp_prf. clear. induction ql. done.
-        apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. }
-      assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq.
-      injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
-      set (q1l := q1::ql). cbn[combine_offs combine foldr]. apply perm_sep_proper.
+        (try by iDestruct "H" as "[_ []]"); (try by iDestruct "H" as "[[] _]");
+      rewrite shift_loc_0; iDestruct "H" as "[$ _]"; [done|].
+      iExists _. iSplitL. done. iSplitL; iIntros "!>!>"; last done.
+      iExists []. rewrite heap_mapsto_vec_nil. auto.
+    - rewrite IH //. f_equiv.
       + rewrite /has_type /sep /=.
         destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
-        (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
-        (try by auto); by rewrite shift_loc_0.
-      + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
-        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //=.
-        apply perm_sep_proper.
+          (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
+          (try by auto); rewrite (shift_loc_0 l) //.
+      + clear. change (ty_size ty) with (0+ty_size ty)%nat at 2. generalize 0%nat.
+        induction (t :: tyl) as [|ty' tyl' IH]=>offs //=. apply perm_sep_proper.
         * rewrite /has_type /sep /=.
           destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
           (try by iDestruct "H" as "[]"); [|]; by rewrite shift_loc_assoc_nat (comm plus).
-        * etrans. apply IHl. by injection Hlen. do 3 f_equiv. lia.
+        * etrans. apply IH. do 2 f_equiv. lia.
   Qed.
 
   Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :