From 05fe05fcdad75b780986bada2ac4421e048507dd Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 7 Apr 2022 23:46:04 +0900
Subject: [PATCH] Model shr_slice and finish slice_basic.v

---
 _CoqProject                                   |   2 +-
 theories/typing/array_util.v                  |   9 ++
 theories/typing/examples/inc_vec.v            |   2 +-
 theories/typing/lib/slice/array_slice.v       |   2 +-
 theories/typing/lib/slice/iter.v              |  10 +-
 .../lib/slice/{uniq_slice.v => slice.v}       |  52 ++++++++-
 theories/typing/lib/slice/slice_basic.v       | 108 +++++++++++++-----
 theories/typing/lib/slice/slice_split.v       |   2 +-
 theories/typing/lib/smallvec/smallvec_slice.v |   2 +-
 theories/typing/lib/vec/vec_slice.v           |   2 +-
 10 files changed, 152 insertions(+), 39 deletions(-)
 rename theories/typing/lib/slice/{uniq_slice.v => slice.v} (72%)

diff --git a/_CoqProject b/_CoqProject
index 0550d628..603e4367 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -79,7 +79,7 @@ theories/typing/lib/option.v
 theories/typing/lib/list.v
 theories/typing/lib/maybe_uninit.v
 theories/typing/lib/vec_util.v
-theories/typing/lib/slice/uniq_slice.v
+theories/typing/lib/slice/slice.v
 theories/typing/lib/slice/slice_basic.v
 theories/typing/lib/slice/array_slice.v
 theories/typing/lib/slice/slice_split.v
diff --git a/theories/typing/array_util.v b/theories/typing/array_util.v
index 8efedefc..398bfbdc 100644
--- a/theories/typing/array_util.v
+++ b/theories/typing/array_util.v
@@ -192,4 +192,13 @@ Section array_util.
     iDestruct "tys" as "[ty tys]". setoid_rewrite <-shift_loc_assoc_nat.
     iSplitL "ty"; by [iApply "In"|iApply "IH"].
   Qed.
+
+  Lemma big_sepL_ty_shr_lft_mono {𝔄} (ty: type 𝔄) aπl d κ κ' tid l :
+    κ' ⊑ κ -∗ ([∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ tid (l +ₗ[ty] i)) -∗
+    [∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ' tid (l +ₗ[ty] i).
+  Proof.
+    iIntros "#? tys". iInduction aπl as [|] "IH" forall (l); [done|]=>/=.
+    iDestruct "tys" as "[ty tys]". setoid_rewrite <-shift_loc_assoc_nat.
+    iSplitL "ty"; by [iApply ty_shr_lft_mono|iApply "IH"].
+  Qed.
 End array_util.
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index c65eb0c4..16b5d83d 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/theories/typing/examples/inc_vec.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.vec Require Import vec vec_slice.
-From lrust.typing.lib.slice Require Import uniq_slice iter.
+From lrust.typing.lib.slice Require Import slice iter.
 Set Default Proof Using "Type".
 
 Section code.
diff --git a/theories/typing/lib/slice/array_slice.v b/theories/typing/lib/slice/array_slice.v
index 0529ef1a..712b26c1 100644
--- a/theories/typing/lib/slice/array_slice.v
+++ b/theories/typing/lib/slice/array_slice.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import uniq_array_util typing.
-From lrust.typing.lib Require Import slice.uniq_slice.
+From lrust.typing.lib Require Import slice.slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
diff --git a/theories/typing/lib/slice/iter.v b/theories/typing/lib/slice/iter.v
index 42c8ef13..4d6bc33e 100644
--- a/theories/typing/lib/slice/iter.v
+++ b/theories/typing/lib/slice/iter.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing uniq_array_util lib.option.
-From lrust.typing.lib.slice Require Import uniq_slice.
+From lrust.typing.lib.slice Require Import slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄: syn_type.
@@ -8,7 +8,13 @@ Implicit Type 𝔄: syn_type.
 Section iter.
   Context `{!typeG Σ}.
 
-  (** We model the unique iterator the same as the unique slice *)
+  (** For simplicity, we model the shared and unique iterators
+    the same as the shared and unique slices *)
+
+  (* Rust's Iter<'a, T> *)
+  Definition iter_shr {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ 𝔄) :=
+    shr_slice κ ty.
+
   (* Rust's IterMut<'a, T> *)
   Definition iter_uniq {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ (𝔄 * 𝔄)) :=
     uniq_slice κ ty.
diff --git a/theories/typing/lib/slice/uniq_slice.v b/theories/typing/lib/slice/slice.v
similarity index 72%
rename from theories/typing/lib/slice/uniq_slice.v
rename to theories/typing/lib/slice/slice.v
index 75038913..c83945ab 100644
--- a/theories/typing/lib/slice/uniq_slice.v
+++ b/theories/typing/lib/slice/slice.v
@@ -4,9 +4,57 @@ Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
 
-Section uniq_slice.
+Section slice.
   Context `{!typeG Σ}.
 
+  Lemma split_mt_shr_slice {A} φ Φ l' d q :
+    (l' ↦∗{q}: (λ vl, [S(d') := d]
+      ∃(l: loc) (n: nat) (aπl: A n),
+        ⌜vl = [ #l; #n] ∧ φ n aπl⌝ ∗ Φ l n d' aπl)) ⊣⊢
+    [S(d') := d] ∃(l: loc) (n: nat) (aπl: A n),
+      ⌜φ n aπl⌝ ∗ l' ↦{q} #l ∗ (l' +ₗ 1) ↦{q} #n ∗ Φ l n d' aπl.
+  Proof.
+    iSplit.
+    - iIntros "(%& ↦ & big)". case d; [done|]=>/= ?.
+      iDestruct "big" as (???[->?]) "?". iExists _, _, _.
+      rewrite !heap_mapsto_vec_cons. iDestruct "↦" as "($&$&_)". by iFrame.
+    - iIntros "big". case d; [done|]=>/= ?.
+      iDestruct "big" as (????) "(↦ & ↦' & ?)". iExists [_;_].
+      rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil. iFrame "↦ ↦'".
+      iExists _, _, _. by iFrame.
+  Qed.
+
+  (* Rust's &'a [T] *)
+  Program Definition shr_slice {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ 𝔄) := {|
+    st_size := 2;  st_lfts := κ :: ty.(ty_lfts);  st_E := ty.(ty_E) ++ ty_outlives_E ty κ;
+    st_own (alπ: proph (listₛ 𝔄)) d tid vl := [S(d') := d]
+      ∃(l: loc) (n: nat) (aπl: vec (proph 𝔄) n),
+        ⌜vl = [ #l; #n] ∧ alπ = lapply aπl⌝ ∗
+        [∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d' κ tid (l +ₗ[ty] i);
+  |}%I.
+  Next Obligation.
+    iIntros (????[|]??) "big"; [done|]. by iDestruct "big" as (???[->_]) "_".
+  Qed.
+  Next Obligation.
+    move=> ???[|?][|?]*/=; try (by iIntros); [lia|]=>/=. do 10 f_equiv.
+    apply ty_shr_depth_mono. lia.
+  Qed.
+  Next Obligation.
+    move=> ?????[|?]*/=; [by iIntros|].
+    iIntros "#LFT #? (%&%&%&[->->]& #tys) κ' !>/=".
+    iDestruct (ty_shr_proph_big_sepL with "LFT [] [] tys κ'") as "Upd"; first done.
+    { iApply lft_incl_trans; by [|iApply lft_intersect_incl_l]. }
+    { iApply lft_incl_trans; by [|iApply lft_intersect_incl_r]. }
+    iApply (step_fupdN_wand with "Upd"). iNext. iMod 1 as (ξl q ?) "[ξl Upd]".
+    iModIntro. iExists ξl, q. iSplit.
+    { iPureIntro. rewrite -vec_to_list_apply. by apply proph_dep_constr. }
+    iIntros "{$ξl}ξl". iMod ("Upd" with "ξl") as "$". iModIntro.
+    iExists _, _, _. by iSplit.
+  Qed.
+
+  Global Instance shr_slice_ne {𝔄} κ : NonExpansive (@shr_slice 𝔄 κ).
+  Proof. rewrite /shr_slice. solve_ne_type. Qed.
+
   Lemma split_mt_uniq_slice {A} P Ψ Φ l' q :
     (l' ↦∗{q}: (λ vl, P ∗
       ∃(l: loc) (n d': nat) (aπξil: A n),
@@ -106,4 +154,4 @@ Section uniq_slice.
 
   Global Instance uniq_slice_ne {𝔄} κ : NonExpansive (@uniq_slice 𝔄 κ).
   Proof. rewrite /uniq_slice /uniq_body. solve_ne_type. Qed.
-End uniq_slice.
+End slice.
diff --git a/theories/typing/lib/slice/slice_basic.v b/theories/typing/lib/slice/slice_basic.v
index 4e8d5f1a..9574c97b 100644
--- a/theories/typing/lib/slice/slice_basic.v
+++ b/theories/typing/lib/slice/slice_basic.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing uniq_array_util.
-From lrust.typing.lib.slice Require Import uniq_slice.
+From lrust.typing.lib.slice Require Import slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
@@ -8,6 +8,59 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section slice_basic.
   Context `{!typeG Σ}.
 
+  (* shr_slice *)
+
+  Global Instance shr_slice_type_contractive {𝔄} κ :
+    TypeContractive (shr_slice (𝔄:=𝔄) κ).
+  Proof.
+    split; [by apply (type_lft_morphism_add_one κ)|done| |].
+    - move=> > EqSz */=. rewrite EqSz. by do 12 f_equiv.
+    - move=> > EqSz */=. rewrite EqSz. do 16 (f_contractive || f_equiv). by simpl in *.
+  Qed.
+
+  Global Instance shr_slice_send {𝔄} κ (ty: type 𝔄) : Sync ty → Send (shr_slice κ ty).
+  Proof. move=> >/=. by do 12 f_equiv. Qed.
+
+  Lemma shr_slice_resolve {𝔄} κ (ty: type 𝔄) E L : resolve E L (shr_slice κ ty) (const True).
+  Proof. apply resolve_just. Qed.
+
+  Lemma shr_slice_real {𝔄 𝔅} κ (ty: type 𝔄) E L (f: _ → 𝔅) :
+    lctx_lft_alive E L κ → real E L ty f →
+    real (𝔅:=listₛ _) E L (shr_slice κ ty) (map f).
+  Proof.
+    move=> ??. apply simple_type_real=>/=.
+    iIntros (???[|]???) "LFT E L big"; [done|]=>/=.
+    iDestruct "big" as (???[->->]) "tys".
+    iMod (real_big_sepL_ty_shr with "LFT E L tys") as "Upd"; [done..|].
+    iIntros "!>!>!>". iApply (step_fupdN_wand with "Upd").
+    iIntros ">((%bl & %Eq)&$& tys) !>". iSplit.
+    { iPureIntro. exists bl. fun_ext=> π. move: (equal_f Eq π)=>/= <-.
+      by rewrite -vec_to_list_apply vec_to_list_map. }
+    iExists _, _, _. by iSplit.
+  Qed.
+
+  Lemma shr_slice_subtype {𝔄 𝔅} κ κ' ty ty' (f: 𝔄 → 𝔅) E L :
+    lctx_lft_incl E L κ' κ → subtype E L ty ty' f →
+    subtype E L (shr_slice κ ty) (shr_slice κ' ty') (map f).
+  Proof.
+    move=> Lft Sub. apply subtype_simple_type=>/=. iIntros (?) "L".
+    iDestruct (Lft with "L") as "#Lft". iDestruct (Sub with "L") as "#Sub".
+    iIntros "!> E". iDestruct ("Lft" with "E") as "#?".
+    iDestruct ("Sub" with "E") as "#(%&?&_& #?)". iSplit; [done|].
+    iSplit; [by iApply lft_intersect_mono|]. iIntros (?[|]??) "big /="; [done|].
+    iDestruct "big" as (?? aπl[->->]) "tys". iExists _, _, _.
+    have ?: ∀(aπl: vec (proph 𝔄) _), map f ∘ lapply aπl = lapply (vmap (f ∘.) aπl).
+    { move=> ?. elim; [done|]=> ??? IH. fun_ext=>/= ?. f_equal. apply (equal_f IH). }
+    iSplit; [done|]. iApply incl_big_sepL_ty_shr; [done..|].
+    by iApply big_sepL_ty_shr_lft_mono.
+  Qed.
+  Lemma shr_slice_eqtype {𝔄 𝔅} κ κ' ty ty' (f: 𝔄 → 𝔅) g E L :
+    lctx_lft_eq E L κ' κ → eqtype E L ty ty' f g →
+    eqtype E L (shr_slice κ ty) (shr_slice κ' ty') (map f) (map g).
+  Proof. move=> [??][??]. split; (apply shr_slice_subtype; by [|split]). Qed.
+
+  (* uniq_slice *)
+
   Global Instance uniq_slice_type_contractive {𝔄} κ :
     TypeContractive (uniq_slice (𝔄:=𝔄) κ).
   Proof.
@@ -81,40 +134,37 @@ Section slice_basic.
     eqtype E L (uniq_slice κ ty) (uniq_slice κ' ty') id id.
   Proof. move=> [??][??]. split; (apply uniq_slice_subtype; by [|split]). Qed.
 
+  (* methods *)
+
   Definition slice_len: val :=
-    fn: ["bs"] :=
-      let: "s" := !"bs" in delete [ #1; "bs"];;
-      letalloc: "r" <- !("s" +ₗ #1) in
-      return: ["r"].
+    fn: ["s"] :=
+      let: "l" := !("s" +ₗ #1) in delete [ #2; "s"];;
+      letalloc: "r" <- "l" in return: ["r"].
 
   (* Rust's [T]::len *)
-  Lemma uniq_slice_len_type {𝔄} (ty: type 𝔄) :
-    typed_val slice_len (fn<(α, β)>(∅; &shr{β} (uniq_slice α ty)) → int)
-      (λ post '-[aal], post (length aal)).
+  Lemma shr_slice_len_type {𝔄} (ty: type 𝔄) :
+    typed_val slice_len (fn<α>(∅; shr_slice α ty) → int)
+      (λ post '-[al], post (length al)).
   Proof.
-    eapply type_fn; [apply _|]. move=>/= [α β]??[b[]]. simpl_subst.
-    iIntros (?[?[]]?) "LFT _ _ _ E Na L C /=[bs _] #Obs".
-    rewrite tctx_hasty_val. iDestruct "bs" as ([|d]) "[⧖ box]"=>//.
-    case b as [[]|]=>//=. rewrite split_mt_ptr.
-    case d as [|d]; first by iDestruct "box" as "[>[] _]".
-    iDestruct "box" as "[(%& >↦bs  & slice) †bs]". wp_read. wp_let.
-    rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-    wp_apply (wp_delete with "[$↦bs $†bs]"); [done|]. iIntros "_". wp_seq.
-    case d as [|]=>//. iDestruct "slice" as (???? [Eq1 ?]) "[Bor _]".
-    iMod (lctx_lft_alive_tok β with "E L") as (?) "(β & L & ToL)"; [solve_typing..|].
-    iMod (frac_bor_acc with "LFT Bor β") as (?) "[(↦₀ & ↦₁ & ↦₂) Toα]"; [done|].
-    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_let. wp_op. wp_read.
-    rewrite heap_mapsto_vec_singleton. wp_write. do 2 wp_seq.
-    iMod ("Toα" with "[$↦₀ $↦₁ $↦₂]") as "β". iMod ("ToL" with "β L") as "L".
-    rewrite cctx_interp_singleton. iApply ("C" $! [# #_] -[_] with "Na L [-] []").
-    - rewrite/= right_id (tctx_hasty_val #_) -freeable_sz_full. iExists _.
-      iFrame "⧖ †r". iNext. iExists [_]. rewrite heap_mapsto_vec_singleton.
-      iFrame "↦r". by iExists _.
+    eapply type_fn; [apply _|]. move=>/= α ??[b[]]. simpl_subst.
+    iIntros (?[?[]]?) "LFT TIME PROPH UNIQ E Na L C /=[bs _] #Obs".
+    rewrite tctx_hasty_val. iDestruct "bs" as ([|d]) "[#⧖ box]"=>//.
+    case b as [[]|]=>//=. iDestruct "box" as "[sl †]". rewrite split_mt_shr_slice.
+    case d as [|d]; first by iDestruct "sl" as ">[]". wp_op.
+    iDestruct "sl" as (? n ?->) "(↦ & ↦' &_)". wp_read. wp_let.
+    rewrite freeable_sz_full. wp_apply (wp_delete [_;_] with "[$† ↦ ↦']"); [done| |].
+    { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+    iIntros "_". wp_seq.
+    iApply (type_type +[#n ◁ int] -[const (n: Zₛ)]
+      with "[] LFT TIME PROPH UNIQ E Na L C [] []").
+    - iApply type_letalloc_1; [solve_extract|done|]. intro_subst.
+      iApply type_jump; [solve_typing|solve_extract|solve_typing].
+    - iSplit; [|done]. rewrite (tctx_hasty_val #n)/=. iExists _.
+      iFrame "⧖". by iExists n.
     - iApply proph_obs_eq; [|done]=>/= π. f_equal.
-      rewrite -(map_length fst). move: (equal_f Eq1 π)=> /= ->.
       by rewrite -vec_to_list_apply vec_to_list_length.
   Qed.
 End slice_basic.
 
-Global Hint Resolve uniq_slice_resolve uniq_slice_real
-  uniq_slice_subtype uniq_slice_eqtype : lrust_typing.
+Global Hint Resolve shr_slice_resolve shr_slice_real shr_slice_subtype shr_slice_eqtype
+  uniq_slice_resolve uniq_slice_real uniq_slice_subtype uniq_slice_eqtype : lrust_typing.
diff --git a/theories/typing/lib/slice/slice_split.v b/theories/typing/lib/slice/slice_split.v
index 3e91d84b..e3d854d0 100644
--- a/theories/typing/lib/slice/slice_split.v
+++ b/theories/typing/lib/slice/slice_split.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import uniq_array_util typing.
-From lrust.typing.lib Require Import slice.uniq_slice.
+From lrust.typing.lib Require Import slice.slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
diff --git a/theories/typing/lib/smallvec/smallvec_slice.v b/theories/typing/lib/smallvec/smallvec_slice.v
index b392e8dc..84581cbc 100644
--- a/theories/typing/lib/smallvec/smallvec_slice.v
+++ b/theories/typing/lib/smallvec/smallvec_slice.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import uniq_array_util typing.
-From lrust.typing.lib Require Import smallvec.smallvec slice.uniq_slice.
+From lrust.typing.lib Require Import smallvec.smallvec slice.slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
diff --git a/theories/typing/lib/vec/vec_slice.v b/theories/typing/lib/vec/vec_slice.v
index d19b8bdc..9c95b9e4 100644
--- a/theories/typing/lib/vec/vec_slice.v
+++ b/theories/typing/lib/vec/vec_slice.v
@@ -1,6 +1,6 @@
 From lrust.typing Require Export type.
 From lrust.typing Require Import uniq_array_util typing.
-From lrust.typing.lib Require Import vec.vec slice.uniq_slice.
+From lrust.typing.lib Require Import vec.vec slice.slice.
 Set Default Proof Using "Type".
 
 Implicit Type 𝔄 𝔅: syn_type.
-- 
GitLab