Verify array/vec/smallvec_as_shr_slice

README.md

@@ -93,7 +93,7 @@ The filenames are spread across `theories/typing/examples`, `theories/typing`, `
 | `pop`               | `vec_pushpop.v`   | `vec_pop_type`           |
 | `index_mut`         | `vec_index.v`     | `vec_index_uniq_type`    |
 | **`IterMut`**       |                   |                          |
-| `iter_mut`          | `vec_slice.v`     | `vec_as_slice_uniq_type` |
+| `iter_mut`          | `vec_slice.v`     | `vec_as_uniq_slice_type` |
 | `next`              | `iter.v`          | `iter_uniq_next_type`    |
 | `inc_vec`           | `inc_vec.v`       | `inc_vec_type`           |
 | **`Cell`**          |                   |                          |

theories/typing/examples/inc_vec.v

@@ -40,7 +40,7 @@ Section code.
       (λ post '-[(v, v')], v' = map (λ e, e + 5) v → post ()).
   Proof.
     eapply type_fn; [apply _|]=>/= α ϝ ret [v[]]. simpl_subst. via_tr_impl.
-    { iApply type_val; [apply (vec_as_slice_uniq_type int)|]. intro_subst.
+    { iApply type_val; [apply (vec_as_uniq_slice_type int)|]. intro_subst.
       iApply type_letcall; [solve_typing|solve_extract|solve_typing|..].
       iIntros (iter). simpl_subst.
       iApply (type_cont [] (λ _, +[iter ◁ _]) (λ (post : ()%ST → _) _, post ())).

theories/typing/lib/slice/array_slice.v

@@ -15,8 +15,31 @@ Section array_slice.
       "r" <- "a";; "r" +ₗ #1 <- #n;;
       return: ["r"].
 
+  (* Rust's [T; n]::as_slice *)
+  Lemma array_as_shr_slice_type {𝔄} n (ty: type 𝔄) :
+    typed_val (array_as_slice n) (fn<α>(∅; &shr{α} [ty;^ n]) → shr_slice α ty)
+      (λ post '-[al], post al).
+  Proof.
+    eapply type_fn; [apply _|]=>/= α ??[ba[]]. simpl_subst.
+    iIntros (?(vπ &[])?) "#LFT #TIME #PROPH UNIQ E Na L C /=[ba _] #Obs".
+    rewrite tctx_hasty_val. iDestruct "ba" as ([|d]) "[#⧖ box]"=>//.
+    case ba as [[|ba|]|]=>//=. rewrite split_mt_ptr.
+    case d as [|]; [by iDestruct "box" as "[>[] _]"|]=>/=.
+    iDestruct "box" as "[(%& ↦ & tys) †]". wp_read. wp_let.
+    rewrite freeable_sz_full -heap_mapsto_vec_singleton.
+    wp_apply (wp_delete with "[$↦ $†]"); [done|]. iIntros "_". wp_seq.
+    wp_apply wp_new; [done..|]. iIntros (?) "[† ↦]". wp_let.
+    rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+    iDestruct "↦" as "[↦ ↦']". wp_write. wp_op. wp_write. do 2 wp_seq.
+    rewrite cctx_interp_singleton.
+    iApply ("C" $! [# #_] -[_] with "Na L [-] Obs"). iSplit; [|done].
+    rewrite tctx_hasty_val. iExists (S _). rewrite/= split_mt_shr_slice.
+    rewrite freeable_sz_full. iFrame "⧖ †". iNext. iExists _, _, _. iFrame.
+    iPureIntro. by rewrite -vec_to_list_apply vapply_funsep.
+  Qed.
+
   (* Rust's [T; n]::as_mut_slice *)
-  Lemma array_as_slice_uniq_type {𝔄} n (ty: type 𝔄) :
+  Lemma array_as_uniq_slice_type {𝔄} n (ty: type 𝔄) :
     typed_val (array_as_slice n) (fn<α>(∅; &uniq{α} [ty;^ n]) → uniq_slice α ty)
       (λ post '-[(al, al')], length al' = length al → post (zip al al')).
   Proof.
@@ -25,7 +48,7 @@ Section array_slice.
     rewrite tctx_hasty_val. iDestruct "ba" as ([|]) "[#⧖ box]"=>//.
     case ba as [[|ba|]|]=>//=. rewrite split_mt_uniq_bor.
     iDestruct "box" as "[(#In &%&%& %ξi &>[% %Eq2]& ↦ba & Vo & Bor) †ba]".
-    wp_read. wp_seq. rewrite freeable_sz_full -heap_mapsto_vec_singleton.
+    wp_read. wp_let. rewrite freeable_sz_full -heap_mapsto_vec_singleton.
     wp_apply (wp_delete with "[$↦ba $†ba]"); [done|]. iIntros "_".
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     iMod (bor_acc_cons with "LFT Bor α") as "[big ToBor]"; [done|]. wp_seq.

theories/typing/lib/smallvec/smallvec_slice.v

@@ -17,7 +17,42 @@ Section smallvec_slice.
       else
         "r" <- !("v" +ₗ #1);; return: ["r"].
 
-  Lemma smallvec_as_slice_uniq_type {𝔄} n (ty: type 𝔄) :
+  (* Rust's SmallVec::as_slice *)
+  Lemma smallvec_as_shr_slice_type {𝔄} n (ty: type 𝔄) :
+    typed_val smallvec_as_slice (fn<α>(∅; &shr{α} (smallvec n ty)) → shr_slice α ty)
+      (λ post '-[al], post al).
+  Proof.
+    eapply type_fn; [apply _|]=>/= α ??[bv[]]. simpl_subst.
+    iIntros (?(vπ &[])?) "#LFT #TIME #PROPH #UNIQ E Na L C /=[bv _] #Obs".
+    rewrite tctx_hasty_val. iDestruct "bv" as ([|d]) "[⧖ box]"=>//.
+    case bv as [[|bv|]|]=>//=. rewrite split_mt_ptr.
+    case d as [|d]; [by iDestruct "box" as "[>[] _]"|]=>/=.
+    iDestruct "box" as "[(%& ↦ & big) †]". wp_read. wp_let.
+    rewrite freeable_sz_full -heap_mapsto_vec_singleton.
+    wp_apply (wp_delete with "[$↦ $†]"); [done|]. iIntros "_". wp_seq.
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_let.
+    iDestruct "big" as (b ????->) "[Bor tys]".
+    iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Bor α") as (?) "[>↦ Cls]"; [done|].
+    rewrite !heap_mapsto_vec_cons !heap_mapsto_vec_nil shift_loc_assoc.
+    iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ & ↦₃ &_)". iDestruct "↦r" as "(↦r & ↦r' &_)".
+    do 2 wp_op. wp_read. wp_write. wp_read. wp_if. case b; wp_op.
+    - wp_write. do 2 wp_seq. iMod ("Cls" with "[$↦₀ $↦₁ $↦₂ $↦₃]") as "α".
+      iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
+      iApply ("C" $! [# #_] -[_] with "Na L [-] Obs"). iSplit; [|done].
+      rewrite tctx_hasty_val. iExists (S _). rewrite/= split_mt_shr_slice.
+      rewrite freeable_sz_full. iFrame "⧖ †r". iNext. iExists _, _, _.
+      iSplit; [done|]. by iFrame.
+    - wp_read. wp_write. do 2 wp_seq. iMod ("Cls" with "[$↦₀ $↦₁ $↦₂ $↦₃]") as "α".
+      iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
+      iApply ("C" $! [# #_] -[_] with "Na L [-] Obs"). iSplit; [|done].
+      rewrite tctx_hasty_val. iExists (S _). rewrite/= split_mt_shr_slice.
+      rewrite freeable_sz_full. iFrame "⧖ †r". iNext. iExists _, _, _.
+      iSplit; [done|]. by iFrame.
+  Qed.
+
+  (* Rust's SmallVec::as_mut_slice *)
+  Lemma smallvec_as_uniq_slice_type {𝔄} n (ty: type 𝔄) :
     typed_val smallvec_as_slice (fn<α>(∅; &uniq{α} (smallvec n ty)) → uniq_slice α ty)
       (λ post '-[(al, al')], length al' = length al → post (zip al al')).
   Proof.

theories/typing/lib/vec/vec_slice.v

@@ -15,8 +15,37 @@ Section vec_slice.
       "r" <- !"v";; "r" +ₗ #1 <- !("v" +ₗ #1);;
       return: ["r"].
 
-  (* Rust's Vec::as_slice_mut *)
-  Lemma vec_as_slice_uniq_type {𝔄} (ty: type 𝔄) :
+  (* Rust's Vec::as_slice *)
+  Lemma vec_as_shr_slice_type {𝔄} (ty: type 𝔄) :
+    typed_val vec_as_slice (fn<α>(∅; &shr{α} (vec_ty ty)) → shr_slice α ty)
+      (λ post '-[al], post al).
+  Proof.
+    eapply type_fn; [apply _|]=>/= α ??[bv[]]. simpl_subst.
+    iIntros (?(vπ &[])?) "#LFT #TIME #PROPH #UNIQ E Na L C /=[bv _] #Obs".
+    rewrite tctx_hasty_val. iDestruct "bv" as ([|d]) "[⧖ box]"=>//.
+    case bv as [[|bv|]|]=>//=. rewrite split_mt_ptr.
+    case d as [|d]; [by iDestruct "box" as "[>[] _]"|]=>/=.
+    iDestruct "box" as "[(%& ↦ & big) †]". wp_read. wp_let.
+    case d as [|d]; [done|]. iDestruct "big" as (????->) "[Bor tys]".
+    rewrite freeable_sz_full -heap_mapsto_vec_singleton.
+    wp_apply (wp_delete with "[$↦ $†]"); [done|]. iIntros "_". wp_seq.
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_let.
+    iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
+    iMod (frac_bor_acc with "LFT Bor α") as (?) "[>↦ Cls]"; [done|].
+    rewrite !heap_mapsto_vec_cons !heap_mapsto_vec_nil.
+    iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ &_)". iDestruct "↦r" as "(↦r & ↦r' &_)".
+    wp_read. wp_write. do 2 wp_op. wp_read. wp_write. do 2 wp_seq.
+    iMod ("Cls" with "[$↦₀ $↦₁ $↦₂]") as "α".
+    iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
+    iApply ("C" $! [# #_] -[_] with "Na L [-] Obs"). iSplit; [|done].
+    rewrite tctx_hasty_val. iExists (S _). rewrite/= split_mt_shr_slice.
+    rewrite freeable_sz_full. iFrame "⧖ †r". iNext. iExists _, _, _.
+    iSplit; [done|]. iFrame "↦r ↦r'". iClear "#". iStopProof.
+    do 3 f_equiv. apply ty_shr_depth_mono. lia.
+  Qed.
+
+  (* Rust's Vec::as_mut_slice *)
+  Lemma vec_as_uniq_slice_type {𝔄} (ty: type 𝔄) :
     typed_val vec_as_slice (fn<α>(∅; &uniq{α} (vec_ty ty)) → uniq_slice α ty)
       (λ post '-[(al, al')], length al' = length al → post (zip al al')).
   Proof.