Redefine uninit. It is defined only for memory regions of size 1. Then, we...

Redefine uninit. It is defined only for memory regions of size 1. Then, we combine them using product.

theories/type.v

@@ -66,7 +66,7 @@ Program Coercion ty_of_st (st : simple_type) : type :=
      ty_own := st.(st_own);
 
      (* [st.(st_own) tid vl] needs to be outside of the fractured
-        borrow, otherwise I do not knwo how to prove the shr part of
+        borrow, otherwise I do not know how to prove the shr part of
         [lft_incl_ty_incl_shared_borrow]. *)
      ty_shr := λ κ tid _ l,
                (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
@@ -482,8 +482,8 @@ Section types.
       by iApply "Hclose'".
   Qed.
 
-  Program Definition uninit (n : nat) : type :=
-    {| st_size := n; st_own tid vl := (length vl = n)%I |}.
+  Program Definition uninit : type :=
+    {| st_size := 1; st_own tid vl := (length vl = 1%nat)%I |}.
   Next Obligation. done. Qed.
 
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=

theories/type_incl.v

@@ -180,32 +180,6 @@ Section ty_incl.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
 
-  Lemma ty_incl_uninit_split ρ n1 n2 :
-    ty_incl ρ (uninit (n1+n2)) (Π[uninit n1; uninit n2]).
-  Proof.
-    iIntros (tid) "_!>". iSplit; iIntros "!#*H".
-    - iDestruct "H" as %Hlen. iExists [take n1 vl; drop n1 vl].
-      repeat iSplit. by rewrite /= app_nil_r take_drop. done.
-      rewrite big_sepL_cons big_sepL_singleton. iSplit; iPureIntro.
-      apply take_length_le. lia. rewrite drop_length. lia.
-    - iSplit; last (iPureIntro; simpl; lia). iDestruct "H" as (vl) "[#Hf #Hlen]".
-      rewrite /= big_sepL_cons big_sepL_singleton. iSplit.
-      + iExists (take n1 vl). iSplit.
-        (* FIXME : cannot split the fractured borrow. *)
-        admit.
-        iNext. iDestruct "Hlen" as %Hlen. rewrite /= take_length_le //. lia.
-      + iExists (drop n1 vl). iSplit.
-        (* FIXME : cannot split the fractured borrow. *)
-        admit.
-        iNext. iDestruct "Hlen" as %Hlen. rewrite /= drop_length. iPureIntro. lia.
-  Admitted.
-
-  Lemma ty_incl_uninit_combine ρ n1 n2 :
-    ty_incl ρ (Π[uninit n1; uninit n2]) (uninit (n1+n2)).
-  Proof.
-  (* FIXME : idem : cannot combine the fractured borrow. *)
-  Admitted.
-
   Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
     Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (cont ρ1) (cont ρ2).

theories/typing.v

 From iris.program_logic Require Import hoare.
+From iris.base_logic Require Import big_op.
 From lrust Require Export type perm notation memcpy.
 From lrust Require Import perm_incl proofmode.
 
@@ -146,11 +147,20 @@ Section typing.
   Qed.
 
   Lemma typed_alloc ρ (n : nat):
-    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
+    0 < n → typed_step_ty ρ (Alloc #n) (own 1 (Π(replicate n uninit))).
   Proof.
-    iIntros (? tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
-    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame.
-    iExists _. iFrame. iPureIntro. by apply (inj Z.of_nat).
+    iIntros (Hn tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
+    iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iSplitL "H†".
+    - assert (ty_size (Π (replicate n uninit)) = n) as ->; last done.
+      clear. simpl. induction n. done. rewrite /= IHn //.
+    - 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".
+      + iExists []. rewrite big_sepL_nil. auto.
+      + iDestruct "IH" as (vll) "(% & % & ?)". subst. iExists ([_]::_). iSplit. done.
+        iSplit. iIntros "/=!%"; congruence.
+        rewrite /= big_sepL_cons. by iSplit.
   Qed.
 
   Lemma typed_free ty (ν : expr):
@@ -187,16 +197,26 @@ Section typing.
   Qed.
 
   Lemma consumes_move ty q:
-    consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q (uninit ty.(ty_size)))%P.
+    consumes ty (λ ν, ν ◁ own q ty)%P
+             (λ ν, ν ◁ own q (Π(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.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">%".
-      by rewrite ty.(ty_size_eq).
+    iAssert (▷ (length vl = ty_size ty))%I with "[#]" as ">Hlen".
+      by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
+    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitL "H†".
+    - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
+      clear. induction ty.(ty_size). done. simpl in *. congruence.
+    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
+      iInduction vl as [|v vl] "IH".
+      + iExists []. rewrite big_sepL_nil. auto.
+      + iDestruct "IH" as (vll) "(% & % & IH)". iExists ([v]::vll). iSplit; last iSplit.
+        * iIntros "!%/=". congruence.
+        * iIntros "!%/=". congruence.
+        * rewrite big_sepL_cons. iFrame "#". done.
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q: