From 9a80651100371603e2b13858f6df5aa20ec1ff4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 8 Apr 2022 15:59:51 +0900
Subject: [PATCH] Verify array/vec/smallvec_as_shr_slice
---
README.md | 2 +-
theories/typing/examples/inc_vec.v | 2 +-
theories/typing/lib/slice/array_slice.v | 27 +++++++++++++-
theories/typing/lib/smallvec/smallvec_slice.v | 37 ++++++++++++++++++-
theories/typing/lib/vec/vec_slice.v | 33 ++++++++++++++++-
5 files changed, 94 insertions(+), 7 deletions(-)
diff --git a/README.md b/README.md
index 8d4fe84b..c93882d2 100644
--- a/README.md
+++ b/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`** | | |
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index 16b5d83d..5f806925 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/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 ())).
diff --git a/theories/typing/lib/slice/array_slice.v b/theories/typing/lib/slice/array_slice.v
index 712b26c1..9e2cfcea 100644
--- a/theories/typing/lib/slice/array_slice.v
+++ b/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.
diff --git a/theories/typing/lib/smallvec/smallvec_slice.v b/theories/typing/lib/smallvec/smallvec_slice.v
index 84581cbc..40bab85c 100644
--- a/theories/typing/lib/smallvec/smallvec_slice.v
+++ b/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.
diff --git a/theories/typing/lib/vec/vec_slice.v b/theories/typing/lib/vec/vec_slice.v
index 9c95b9e4..dab19197 100644
--- a/theories/typing/lib/vec/vec_slice.v
+++ b/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.
--
GitLab