Skip to content
Snippets Groups Projects
Commit 66454cde authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Modify split_mt_smallvec

parent 57377e45
No related tags found
No related merge requests found
Pipeline #63457 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/smallvec/smallvec.v
+ 7
− 10
View file @ 66454cde
......@@ -47,19 +47,19 @@ Section smallvec.
([∗ list] i ↦ aπ ∈ aπl, (l' +ₗ 4 +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) ∗
∃wl', ⌜k = (len * ty.(ty_size) + length wl')%nat⌝ ∗ (l' +ₗ 4 +ₗ[ty] len) ↦∗ wl'
else (* vector mode *)
∃wl, ⌜length wl = k⌝ ∗ (l' +ₗ 4) ↦∗ wl ∗ Φ l len ex aπl.
(∃wl, ⌜length wl = k⌝ ∗ (l' +ₗ 4) ↦∗ wl) ∗ Φ l len ex aπl.
Proof.
iSplit.
- iIntros "(%& ↦ & big)". iDestruct "big" as (b ?????(->&?&?)) "big".
iExists _, _, _, _, _. iSplit; [done|].
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
iDestruct "↦" as "($&$&$&$& ↦)". case b; [|iExists _; by iFrame].
iDestruct "big" as (??->) "tys/=".
iDestruct "↦" as "($&$&$&$& ↦)". case b=>/=; last first.
{ iFrame "big". iExists _. by iFrame. } iDestruct "big" as (??->) "tys/=".
iDestruct (big_sepL_ty_own_length with "tys") as %<-.
rewrite heap_mapsto_vec_app trans_big_sepL_mt_ty_own shift_loc_assoc.
iDestruct "↦" as "[? ↦ex]". iSplitR "↦ex"; iExists _; iFrame.
by rewrite -app_length.
- iDestruct 1 as (b ?????) "(↦hd & big)". case b.
- iDestruct 1 as (b ?????) "(↦hd & big)". case b=>/=.
+ rewrite trans_big_sepL_mt_ty_own.
iDestruct "big" as "[(%wll & ↦ar & tys) (%wl' &->& ↦ex)]".
iDestruct (big_sepL_ty_own_length with "tys") as %Eqsz.
......@@ -68,10 +68,10 @@ Section smallvec.
iDestruct "↦hd" as "($&$&$&$&_)". iFrame "↦ar ↦ex".
iExists true, _, _, _, _, _. iSplit; [by rewrite -app_length|].
iExists _, _. by iFrame.
+ iDestruct "big" as (?<-) "[↦tl ?]". iExists ([_;_;_;_]++_).
+ iDestruct "big" as "[(%&%&↦tl) ?]". iExists ([_;_;_;_]++_).
rewrite !heap_mapsto_vec_cons !shift_loc_assoc.
iDestruct "↦hd" as "($&$&$&$&_)". iFrame "↦tl".
iExists false, _, _, _, _, _. by iFrame.
iExists false, _, _, _, _, _=>/=. by iFrame.
Qed.
(* For simplicity, it always has the location and capacity *)
......@@ -123,9 +123,7 @@ Section smallvec.
iMod (ty_share_big_sepL with "LFT In Bor κ") as "Toshrs"; [done|].
iApply (step_fupdN_wand with "Toshrs"). iIntros "!> >[?$] !>".
iExists true, _, _, _, _. by iFrame.
- iMod (bor_exists with "LFT Bor") as (?) "Bor"; [done|].
iMod (bor_sep_persistent with "LFT Bor κ") as "(_ & Bor & κ)"; [done|].
iMod (bor_sep with "LFT Bor") as "[_ Bor]"; [done|].
- iMod (bor_sep with "LFT Bor") as "[_ Bor]"; [done|].
iMod (bor_sep with "LFT Bor") as "[Bor _]"; [done|].
iMod (ty_share_big_sepL with "LFT In Bor κ") as "Toshrs"; [done|].
iApply (step_fupdN_wand with "Toshrs"). iIntros "!> >[?$] !>".
......@@ -165,5 +163,4 @@ Section smallvec.
Global Instance smallvec_ne {𝔄} n : NonExpansive (@smallvec 𝔄 n).
Proof. solve_ne_type. Qed.
End smallvec.
theories/typing/lib/smallvec/smallvec_basic.v
+ 2
− 2
View file @ 66454cde
......@@ -158,8 +158,8 @@ Section smallvec_basic.
iApply ("C" $! [# #_] -[const ()] with "Na L [-Obs] Obs"). iSplit; [|done].
rewrite tctx_hasty_val. iExists _. iFrame "⧖". iSplit; [|done]. iNext.
iExists _. iFrame "↦". by rewrite unit_ty_own.
- iDestruct "big" as (? <-) "big". rewrite trans_big_sepL_mt_ty_own.
iDestruct "big" as "(↦tl & (%& ↦ar & tys) & (%& %Eq & ↦ex) & †')".
- rewrite trans_big_sepL_mt_ty_own.
iDestruct "big" as "((%&<-& ↦tl) & (%& ↦ar & tys) & (%& %Eq & ↦ex) & †')".
iDestruct (big_sepL_ty_own_length with "tys") as %Eq'.
do 2 (wp_op; wp_read). do 3 wp_op. wp_read.
rewrite -Nat2Z.inj_add -Nat2Z.inj_mul !Nat.mul_add_distr_r -Eq -Eq' -app_length.
......
theories/typing/lib/smallvec/smallvec_index.v
+ 3
− 4
View file @ 66454cde
......@@ -163,7 +163,7 @@ Section smallvec_index.
setoid_rewrite shift_loc_assoc. iSplitL "↦ty".
{ iStopProof. do 3 f_equiv. iApply ty_own_depth_mono. lia. }
iStopProof. do 6 f_equiv; [|iApply ty_own_depth_mono; lia]. do 2 f_equiv. lia.
- iDestruct "big" as (??) "(↦tl & ↦tys & ex†)". wp_read. wp_op. do 2 wp_read.
- iDestruct "big" as "(↦tl & ↦tys & ex†)". wp_read. wp_op. do 2 wp_read.
do 2 wp_op. wp_write. do 2 rewrite -{1}heap_mapsto_vec_singleton.
rewrite !freeable_sz_full. wp_bind (delete _).
iApply (wp_delete with "[$↦v $†v]"); [done|].
......@@ -219,9 +219,8 @@ Section smallvec_index.
by iApply proph_eqz_vinsert. }
rewrite split_mt_smallvec. iExists false, _, _, _, _=>/=.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
iFrame "↦₀ ↦₁ ↦₂ ↦₃ ex†". iSplit; [by rewrite vec_to_list_apply|].
iClear "#". iExists _. iFrame "↦tl". iSplit; [done|].
rewrite vinsert_backmid -big_sepL_vbackmid Eqi. iSplitL "↦tys".
iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tl ex†". iSplit; [by rewrite vec_to_list_apply|].
iClear "#". rewrite vinsert_backmid -big_sepL_vbackmid Eqi. iSplitL "↦tys".
{ iStopProof. do 6 f_equiv. iApply ty_own_depth_mono. lia. }
setoid_rewrite shift_loc_assoc. iSplitL "↦ty".
{ iStopProof. do 3 f_equiv. iApply ty_own_depth_mono. lia. }
......
theories/typing/lib/smallvec/smallvec_pop.v
+ 5
− 7
View file @ 66454cde
......@@ -42,8 +42,7 @@ Section smallvec_pop.
iDestruct "uniq" as (d ξi [? Eq2]) "[Vo Bor]". move: Eq2. set ξ := PrVar _ ξi=> Eq2.
iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
iMod (bor_acc with "LFT Bor α") as "[(%&%& #⧖ & Pc & big) ToBor]"; [done|].
wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-].
rewrite split_mt_smallvec.
wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-]. rewrite split_mt_smallvec.
iDestruct "big" as (?? len ex aπl Eq1) "(↦ & big)".
rewrite !heap_mapsto_vec_cons !shift_loc_assoc.
iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ & ↦₃ &_)". wp_op. wp_read. wp_let.
......@@ -106,7 +105,7 @@ Section smallvec_pop.
{ inv_vec aπl=> + aπl'. by elim aπl'=>/= *. }
have ->: removelast (lapply aπl π) = lapply (vinit aπl) π.
{ inv_vec aπl=> + aπl'. elim aπl'; [done|]=>/= *. by f_equal. } done.
- iDestruct "big" as (??) "(↦tl & ↦tys & (%&% & ↦ex) & †)".
- iDestruct "big" as "(↦tl & ↦tys & (%&% & ↦ex) & †)".
iDestruct (big_sepL_vinitlast with "↦tys") as "[↦tys (%& ↦last & ty)]"=>/=.
iDestruct (ty_size_eq with "ty") as %Lvl. do 2 wp_op. wp_read. wp_op.
wp_write. have ->: (ex + 1)%Z = S ex by lia. do 2 wp_op. wp_read.
......@@ -117,10 +116,9 @@ Section smallvec_pop.
{ iNext. iExists _, _. iFrame "⧖ Pc". rewrite split_mt_smallvec.
iExists _, _, _, _, _.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tys". iSplit; [done|]. iExists _. iFrame "↦tl".
iSplit; [done|]. have ->: len + S ex = S (len + ex) by lia. iFrame "†".
iExists (_++_). rewrite heap_mapsto_vec_app. iFrame "↦last".
rewrite shift_loc_assoc_nat app_length Nat.add_comm Lvl.
iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tl ↦tys". have ->: len + S ex = S (len + ex) by lia.
iFrame "†". iSplit; [done|]. iExists (_++_). rewrite heap_mapsto_vec_app.
iFrame "↦last". rewrite shift_loc_assoc_nat app_length Nat.add_comm Lvl.
iFrame. iPureIntro=>/=. lia. }
iMod ("ToL" with "α L") as "L".
iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty); #r ◁ box (option_ty ty)]
......
theories/typing/lib/smallvec/smallvec_push.v
+ 5
− 5
View file @ 66454cde
......@@ -35,7 +35,7 @@ Section smallvec_push.
rewrite split_mt_smallvec. iDestruct "big" as (b ? len ??->) "(↦ & big)".
rewrite heap_mapsto_vec_cons. iDestruct "↦" as "[↦₀ ↦']". wp_rec. wp_read.
wp_if. case b=>/=; last first.
{ iDestruct "big" as (??) "(↦tl & ↦tys & ↦ex & †)". wp_op.
{ iDestruct "big" as "((%&%& ↦tl) & ↦tys & ↦ex & †)". wp_op.
iApply (wp_vec_push_core with "[↦' ↦tys ↦ex † ↦x ty]").
{ iExists _, _. iFrame "↦' † ↦ex ↦tys". iExists _. iFrame. }
iIntros "!> (%&%& ↦' & ↦tys & ↦ex & † & ↦x)". iApply "ToΦ". iFrame "↦x".
......@@ -82,10 +82,10 @@ Section smallvec_push.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
iFrame "↦₀ ↦₁ ↦₂ ↦₃"=>/=. iSplit.
{ iPureIntro. fun_ext=> ?. by rewrite vec_to_list_snoc lapply_app. }
iExists (_++_). rewrite EqLen app_length heap_mapsto_vec_app shift_loc_assoc.
iFrame "↦o". rewrite Lwll. iFrame "↦tl". rewrite Nat.add_comm Nat.add_0_r.
iFrame "†". iSplit; [done|]. iSplitL; last first.
{ iExists []. by rewrite heap_mapsto_vec_nil. }
rewrite Nat.add_comm Nat.add_0_r. iFrame "†". iSplitL "↦o ↦tl".
{ iExists (_++_). rewrite EqLen app_length heap_mapsto_vec_app shift_loc_assoc.
iFrame "↦o". rewrite Lwll. by iFrame "↦tl". }
iSplitL; last first. { iExists []. by rewrite heap_mapsto_vec_nil. }
rewrite vec_to_list_snoc big_sepL_app big_sepL_singleton. iSplitL "tys ↦l".
+ rewrite trans_big_sepL_mt_ty_own. iExists _. iFrame "↦l". iStopProof.
do 3 f_equiv. apply ty_own_depth_mono. lia.
......
theories/typing/lib/smallvec/smallvec_slice.v
+ 2
− 3
View file @ 66454cde
......@@ -76,7 +76,7 @@ Section smallvec_slice.
iApply proph_eqz_constr. iApply (proph_eqz_prvars with "Eqzs"). }
rewrite split_mt_smallvec. iExists true, _, _, _, _=>/=.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc. by iFrame.
- iDestruct "big" as (??) "(↦tl & ↦tys & †)". wp_op. wp_read. wp_write. do 2 wp_seq.
- iDestruct "big" as "(↦tl & ↦tys & †)". wp_op. wp_read. wp_write. do 2 wp_seq.
iMod ("ToBor" $! (big_sepL _ _) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tl † ToPc] [↦tys Pcs]")
as "[Bor α]"; last first.
+ iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
......@@ -99,7 +99,6 @@ Section smallvec_slice.
{ iApply "ToPc". rewrite -!vec_to_list_apply.
iApply proph_eqz_constr. iApply (proph_eqz_prvars with "Eqzs"). }
rewrite split_mt_smallvec. iExists false, _, _, _, _=>/=.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
iFrame "↦₀ ↦₁ ↦₂ ↦₃ †". iSplit; [done|]. iExists _. by iFrame.
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc. by iFrame.
Qed.
End smallvec_slice.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment