Skip to content
Snippets Groups Projects
Commit f0f30002 authored by Xavier Denis's avatar Xavier Denis
Browse files

100

parent 954f6757
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/smallvec/smallvec_push.v
+ 161
− 96
View file @ f0f30002
......@@ -28,7 +28,10 @@ Section smallvev_push.
("self'" +ₗ #2) <- "len" + #1;;
let: "r" := new [ #0] in return: ["r"]
else (* ruh-roh gotta allocate a vector and copy everything over*)
("self'" +ₗ #1) <- ("self'" +ₗ #4);;
let: "l'" := new [("len") * #ty.(ty_size)] in
memcpy ["l'"; "len" * #ty.(ty_size); "self'" +ₗ #4];;
("self'" +ₗ #1) <- ("l'");;
("self'" +ₗ #3) <- #0;;
"self'" <- #false;; "push" []
else
"push" []
......@@ -42,11 +45,16 @@ Section smallvev_push.
.
Definition bor_cnts {𝔄} (ty: type 𝔄) (vπ: proph 𝔄) (ξi: positive) (d: nat)
(tid: thread_id) (l: loc) : iProp Σ :=
let ξ := PrVar (𝔄 ↾ prval_to_inh vπ) ξi in
(∃vπ' d', ⧖(S d') ∗ .PC[ξ] vπ' d' ∗ l ↦∗: ty.(ty_own) vπ' d' tid).
Definition smallvec_push_type {𝔄} (ty: type 𝔄) (n : nat ) :
typed_val (smallvec_push ty n) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ())
(λ post '-[(al, al'); a], al' = al ++ [a] → post ()).
Proof.
eapply type_fn; [apply _|]=> α ??[v[x[]]]. simpl_subst.
eapply type_fn; [apply _|]=> α ? k [v[x[]]]. simpl_subst.
{
......@@ -54,10 +62,8 @@ Section smallvev_push.
rewrite tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//.
case v as [[|v|]|]=>//. iDestruct "v" as "[(%vl & >↦ & [#LftIn uniq]) †]".
case vl as [|[[|v'|]|][]]; try by iDestruct "uniq" as ">[]".
(* iDestruct "x" as ([|dx]) "[⧖x x]"=>//. case x as [[|x|]|]=>//. *)
rewrite heap_mapsto_vec_singleton. wp_read. wp_let. wp_bind (delete _).
rewrite -heap_mapsto_vec_singleton freeable_sz_full.
(* iApply (wp_persistent_time_receipt with "TIME ⧖x"); [done|]. *)
iApply (wp_delete with "[$↦ $†]"); [done|].
iIntros "!>_".
(* iIntros "!>_ ⧖x". *)
......@@ -70,7 +76,7 @@ Section smallvev_push.
rewrite split_mt_smallvec. case du as [|du]=>//.
iDestruct "↦vec" as (tag ? len ex aπl Eq1) "(↦ & ↦tys)".
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iDestruct "↦" as "(↦₀ & ? & ↦len & ↦v)".
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iDestruct "↦" as "(↦₀ & ↦l & ↦len & ↦ex)".
wp_read. wp_let.
......@@ -78,149 +84,208 @@ Section smallvev_push.
iAssert (
v' ↦ #false -∗
(∃ wl' : list val,
⌜(n * ty_size ty)%nat =
(len * ty_size ty + length wl')%nat⌝
∗ (v' +ₗ 4 +ₗ[ty] len) ↦∗ wl') -∗
(* (∃ vl : list val, (v' +ₗ 1) ↦∗ vl ∗ ty_own (vec_ty ty) vπ' (S du) tid vl) -∗ *)
(cctx_interp tid postπ _) -∗
(∃ wl : list val, ⌜length wl = (n * ty_size ty)%nat⌝ ∗ (v' +ₗ 4) ↦∗ wl) -∗
(v' +ₗ 1) ↦∗: ty_own (vec_ty ty) (fst ∘ vπ) (S du) tid -∗
.PC[ξ] (fst ∘ vπ) (S du) -∗
.VO[ξ] (fst ∘ vπ) (S du) -∗
(cctx_interp tid postπ [k ◁cont{[_], (λ v : vec val 1, +[vhd v ◁ box ()])} tr_ret]) -∗
na_own tid ⊤ -∗
(q'.[α] ={⊤}=∗ llctx_interp [_ ⊑ₗ []] 1)%I -∗
tctx_elt_interp tid (x ◁ box ty) aπ -∗
(∀ Q : iPropI Σ, ▷ (▷ Q ={↑lft_userN}=∗ ▷ bor_body) -∗ ▷ Q ={⊤}=∗ &{α} Q ∗ q'.[α]) -∗
WP push [] {{ _, cont_postcondition }})%I with "[]" as "push".
{
iIntros "/= ↦₀ ↦tl C Na ToL Tx ToBor".
(* rewrite !heap_mapsto_vec_cons. iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ &_)". *)
iIntros "↦₀ ↦tl ↦vec Pc Vo C Na ToL Tx ToBor".
rewrite /push. wp_rec.
iMod ("ToBor" $! (∃ (vπ' : proph _) d', ((v' +ₗ 1) ↦∗: (vec_ty ty).(ty_own) vπ' d' tid) ∗ .PC[ξ] vπ' d' ∗ ⧖ (S d'))%I
with "[↦₀ ↦tl] []") as "[? tok]".
{ iIntros "!> Hvec". iDestruct "Hvec" as (vπ' d') "(Hvals & ? & ?)". rewrite /bor_body.
(* iMod ("ToBor" $! (∃ (vπ' : _) d', ((v' +ₗ 1) ↦∗: (vec_ty ty).(ty_own) vπ' d' tid) ∗ .PC[ξ] vπ' d' ∗ ⧖ (S d'))%I *)
iMod ("ToBor" $! (bor_cnts (vec_ty ty) (fst ∘ vπ) ξi (S du) _ (v' +ₗ 1))
with "[↦₀ ↦tl] [↦vec Pc]") as "[o tok]".
{ iIntros "!> Hvec". rewrite /bor_cnts. iDestruct "Hvec" as (vπ' d') "(? & ? & Hvals)". rewrite /bor_body.
iExists vπ', d'. iFrame. iDestruct "Hvals" as (vl) "(>v1 & Hvec)".
case d' as [|d]=>//; [admit|]. (*trivial false in left case*)
case d' as [|d]=>//=; [by iMod ("Hvec") as "?"|].
iModIntro. iNext. (*provs wrong, forgot how to eliminate modalities *)
iDestruct "Hvec" as (l' len' ex' aπl') "([-> %] & ?)".
iCombine "↦₀ v1" as "v0".
rewrite -heap_mapsto_vec_cons.
iDestruct "↦tl" as (?) "(% & ↦tl)".
iCombine "v0 ↦tl" as "v0".
rewrite -heap_mapsto_vec_cons -heap_mapsto_vec_app.
(* iCombine "v0 ↦tl" as "v0".
rewrite -heap_mapsto_vec_app. *)
iExists _. iFrame. iExists false. simpl.
*)
(* rewrite -heap_mapsto_vec_cons. *)
(* rewrite -heap_mapsto_vec_app. *)
iExists _. iFrame.
iExists false, l', len', ex', _, aπl'.
simpl. iFrame. done.
} {admit. }
} {
iExists (fst ∘ vπ), (S du). iFrame "# Pc".
iDestruct "↦vec" as (vl) "(? & v)". iExists vl.
iFrame. iDestruct "v" as (x' l' e p) "(? & ? & ?)".
iExists x', l', e, p. iFrame. }
iMod ("ToL" with "tok") as "L".
(* with "[↦₀ ↦tl] [↦v ↦vec Pc ]") as "[o tok]". *)
iAssert (tctx_elt_interp tid (#v' +ₗ #1 ◁ &uniq{α} (vec_ty ty)) vπ ) with "[]" as "te".
{ admit. }
iAssert (tctx_elt_interp tid (#v' +ₗ #1 ◁ &uniq{α} (vec_ty ty)) vπ ) with "[o Vo]" as "te".
{ iExists #(v' +ₗ 1),( S (S du)).
iFrame "# ∗". iSplitR;[done|].
iExists (S du), ξi. rewrite /uniq_body. iFrame. iSplitR; [done|].
iFrame. done. }
iApply (type_val (ℭ := ()) (𝔅l := [(listₛ 𝔄 * listₛ 𝔄)%ST;𝔄]) _ _
(fn<α>(∅; &uniq{α} (vec_ty ty), ty) → ()) +[_; _] _ _ _ _ _
(λ p '(-[Φ; a; b]), Φ p -[a; b]) $! _ _ -[vπ;aπ]
with "LFT TIME PROPH UNIQ E Na L C [] [Obs]"). apply vec_push_type.
admit.
admit.
Unshelve.
[$] [Obs]").
with "LFT TIME PROPH UNIQ E Na L C [$] [Obs]"). apply vec_push_type.
iExact "Obs".
Unshelve. constructor. done. constructor. done.
intro_subst.
via_tr_impl.
iApply type_new; [done|]. intro_subst.
iApply type_assign.
solve_typing.
solve_typing.
solve_typing.
iApply (type_letcall α);[solve_typing|solve_extract|solve_typing|..]. intro_subst.
iApply type_jump. solve_typing. solve_extract. solve_typing.
move => ? [? [? [? []]]] //=.
}
rewrite /=. rewrite -shift_loc_assoc -!heap_mapsto_vec_cons.
iDestruct "↦tys" as (?) "(% & ↦tl & ↦vec)".
(* rewrite /=. rewrite -shift_loc_assoc -!heap_mapsto_vec_cons. *)
(* iDestruct "↦tys" as (?) "(% & ↦tl & ↦vec)". *)
}
(* } *)
rewrite /push. wp_let. wp_if. case tag.
{ iDestruct "↦tys" as "(Z & ↦vec)". iDestruct "↦vec" as (tl) "(% & ↦tl)".
set vπ' := λ π, (lapply (vsnoc aπl aπ) π, π ξ).
wp_op. wp_read. wp_let. wp_op. wp_op. wp_if. case_eq (bool_decide (len + 1 ≤ n)%Z) => ?.
wp_op. wp_read. wp_let. wp_op. wp_op. wp_if. case_eq (bool_decide (len + 1 ≤ n)%Z) => LenN.
{
iClear "push".
rewrite tctx_hasty_val. iDestruct "x" as ([|dx]) "[⧖x x]"=>//. case x as [[|x|]|]=>//.
(* iCombine "⧖u ⧖x" as "#⧖"=>/=. set d := S du `max` dx. *)
(* assert ( ∃ d', d = S d') as [d' Hd'].
{ subst d. case dx => //=[//=|?]; [by exists du| by eexists (du `max` _)]. } *)
(* rewrite Hd'. *)
wp_op. wp_op. wp_op. wp_bind (_ <-{_} !_)%E.
iApply (wp_persistent_time_receipt with "TIME ⧖x"); [done|].
(* move: (lookup_lt_is_Some_2 aπl len) => [lia|]. *)
assert (length tl = ty_size ty + (n - len) * ty_size ty) by admit.
move: {H1}(app_length_ex tl _ _ H1)=> [vl'[?[->[Len ?]]]].
assert (length tl = ty_size ty + (n - len - 1) * ty_size ty).
{ simpl.
assert (len + 1 ≤ n).
{ case_bool_decide; lia. }
rewrite -Nat.sub_add_distr Nat.mul_sub_distr_r.
rewrite Nat.add_sub_assoc. lia.
by apply Nat.mul_le_mono_r.
}
move: {H1}(app_length_ex tl _ _ H1)=> [vl'[z[->[Len K]]]].
rewrite heap_mapsto_vec_app shift_loc_assoc_nat Len -Nat2Z.inj_mul.
iDestruct "↦tl" as "[↦ ↦tl]".
iDestruct "x" as "[(%& ↦x & ty) †x]".
iDestruct (ty_size_eq with "ty") as %Sz. rewrite freeable_sz_full.
iDestruct (ty_size_eq with "ty") as %Sz.
(* rewrite freeable_sz_full. *)
iApply (wp_memcpy with "[$↦ $↦x]") ; [lia..|].
iIntros "!> [↦ ↦x]". wp_seq. wp_op. wp_op. wp_write.
iIntros "!> [↦ ↦x] ⧖x".
iCombine "⧖u ⧖x" as "#⧖"=>/=. set d := du `max` dx.
wp_seq. wp_op. wp_op. wp_write.
iAssert (∃ vl, (v' +ₗ 4 +ₗ[ty] (length aπl)) ↦∗ vl ∗ ty_own ty aπ ( d) tid vl)%I with "[ty ↦]" as "zz".
{ iExists vl. rewrite vec_to_list_length. iFrame. iApply (ty_own_depth_mono with "[$]"). lia. }
(* iCombine "Z zz" as "Z". rewrite -big_sepL_snoc. *)
iMod (uniq_update ξ (fst ∘ vπ') with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
iMod ("ToBor" $! bor_body with "[] [Pc ↦₀ ↦l ↦len zz Z ↦tl ↦ex]") as "[? tok]".
{ by iIntros "!> $". }
{ rewrite /bor_body. iNext. iExists _, (S d). iFrame "# ∗".
iCombine "↦₀ ↦l ↦len ↦ex" as "↦v" .
rewrite -shift_loc_assoc.
rewrite Nat2Z.inj_add Nat2Z.inj_mul -!shift_loc_assoc .
rewrite -!heap_mapsto_vec_cons.
epose proof (split_mt_smallvec ty ((n * ty_size ty)%nat) v' tid (S d) (fst ∘ vπ')).
rewrite H1.
clear H1.
iExists true, l, _, ex, (aπl +++ [#aπ]). iFrame. iSplitR.
{ iPureIntro. fun_ext. rewrite /vπ' /= => ?. rewrite vec_to_list_app vec_to_list_snoc lapply_app //=. }
iSplitL "↦v". rewrite !Nat2Z.inj_add. rewrite (_ : #(len + 1%nat) = #(len + 1)). iFrame.
{ rewrite Nat2Z.inj_succ Nat2Z.inj_0 Z.one_succ //=. }
iMod ("ToBor" $! (∃ (vπ' : proph _) d', (v' ↦∗: (smallvec n ty).(ty_own) vπ' d' tid) ∗ .PC[ξ] vπ' d' ∗ ⧖ (S d'))%I with "[] []") as "[? tok]".
{ admit. } { admit. }
simpl. iFrame. simpl.
rewrite vec_to_list_app /=.
iSplitL "zz Z".
{ rewrite big_sepL_snoc Nat2Z.inj_mul. iFrame.
iClear "#". iStopProof. do 6 f_equiv. apply ty_own_depth_mono. lia.
}
iFrame. iExists z.
iFrame. rewrite shift_loc_assoc Nat2Z.inj_mul.
iClear "#".
rewrite -Z.mul_succ_l -Z.add_1_r. simpl. iFrame.
rewrite Nat2Z.inj_mul Nat2Z.inj_add Nat2Z.inj_succ Nat2Z.inj_0 -Z.one_succ.
iFrame.
iPureIntro. rewrite K. rewrite -Nat.mul_add_distr_r.
(* assert ( n > len). lia. admit. *)
rewrite -Nat.sub_add_distr.
rewrite Nat.add_sub_assoc. lia. clear push.
case_bool_decide; lia.
}
iMod ("ToL" with "tok L") as "L".
(* wp_bind (new _). *)
(* iApply wp_new. done. done. iIntros "!>" (?) "[†' ↦']". wp_let. *)
iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty)] -[vπ'] with "[] LFT TIME PROPH UNIQ E Na L C [-] []").
- iApply type_new; [done|]. intro_subst.
iApply type_jump; [solve_typing|solve_extract|solve_typing].
- rewrite/= right_id (tctx_hasty_val #_). iExists _.
iFrame "⧖u LftIn". iExists _, _. rewrite /uniq_body.
iFrame "⧖ LftIn". iExists (S d), ξi. rewrite /uniq_body.
iFrame.
iSplitR. iSplit; [done|]. iPureIntro.
fun_ext. rewrite /= /ξ(proof_irrel (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ)) (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ'))) => ? //=.
subst ξ. subst bor_body.
rewrite (proof_irrel (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ)) (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ'))).
iFrame.
(* rewrite (proof_irrel (@prval_to_inh (listₛ 𝔄) (fst ∘ vπ'))
(@prval_to_inh (listₛ 𝔄) (fst ∘ vπ))). by iFrame. *)
admit.
- iApply proph_obs_impl;[|done] => π //=.
move: (equal_f Eq1 π) (equal_f Eq2 π)=>/=. case (vπ π)=>/= ??->-> Imp Eq.
apply Imp. move: Eq. by rewrite vec_to_list_snoc lapply_app.
}
{ wp_op. wp_op. wp_write. wp_write.
iApply ( "push" with "[] ToBor"). admit.
{ wp_op. wp_bind (new _). iApply wp_new; [lia| done|].
iIntros "!>" (?) "[†' ↦']". wp_let. wp_op. wp_op. wp_bind (memcpy _).
rewrite trans_big_sepL_mt_ty_own.
iDestruct "Z" as (?) "[↦ tys]".
iDestruct (big_sepL_ty_own_length with "tys") as %Len.
(* plus_0_r Nat2Z.id Nat.mul_add_distr_r *)
(* repeat_app heap_mapsto_vec_app. *)
iApply (wp_memcpy with "[$↦' $↦]"); [rewrite repeat_length; lia|lia|].
iIntros "!>[↦' ↦]". wp_seq. wp_op. rewrite -Nat2Z.inj_mul.
wp_write. wp_op. iDestruct "↦ex" as "(↦ex & ↦ε)". rewrite !shift_loc_assoc. wp_write.
wp_write.
iApply ( "push" with "[$] [↦tl ↦] [tys †' ↦' ↦l ↦ex ↦ε ↦len] [$] [$] [$] [$] [ToL L] [$] ToBor").
{ iExists (concat wll ++ tl). iFrame. rewrite heap_mapsto_vec_app app_length Len -!shift_loc_assoc. by iFrame. }
{ iExists [_; _; _]. iClear "push".
iCombine "↦l ↦len ↦ex ↦ε" as "↦v'". rewrite -!shift_loc_assoc -!heap_mapsto_vec_cons.
iFrame. iExists _, _, 0,_.
iSplitR; [done|].
iSplitL "tys ↦'". rewrite trans_big_sepL_mt_ty_own.
iNext. iExists wll. iFrame. iSplitR. iExists []. rewrite heap_mapsto_vec_nil //=.
by rewrite Nat.add_0_r Nat2Z.id.
}
{ iIntros. iApply ("ToL" with "[$] [$]"). }
}
}
{ iApply ("push" with "[] ToBor"). admit.
}
rewrite /=. rewrite -shift_loc_assoc -!heap_mapsto_vec_cons.
iDestruct "↦tys" as (?) "(% & ↦tl & ↦vec)".
iMod ("ToBor" $! (∃ (vπ' : proph _) d', ((v' +ₗ 1) ↦∗: (vec_ty ty).(ty_own) vπ' d' tid) ∗ .PC[ξ] vπ' d' ∗ ⧖ (S d'))%I with "[↦₀ ↦tl] [↦v ↦vec Pc ]") as "[o tok]".
- iIntros "!> Hvec". iDestruct "Hvec" as (vπ' d') "(Hvals & ? & ?)".
iExists vπ', d'. iFrame. iDestruct "Hvals" as (vl) "(>v1 & Hvec)".
case d' as [|d]=>//; [admit|]. (*trivial false in left case*)
iModIntro. iNext. (*provs wrong, forgot how to eliminate modalities *)
iDestruct "Hvec" as (l' len' ex' aπl') "([-> %] & ?)".
iCombine "↦₀ v1" as "v0".
rewrite -heap_mapsto_vec_cons.
iCombine "v0 ↦tl" as "v0".
rewrite -heap_mapsto_vec_app.
iExists _. iFrame.
iExists false, l', len', ex', _, aπl'.
simpl. iFrame. done.
- iExists (fst ∘ vπ), (S du). iFrame "# Pc".
iDestruct "↦vec" as "(? & e & ?)".
iDestruct "e" as (?) "?".
iExists _. iFrame. simpl.
iExists l, len, ex, aπl. iFrame. iSplitR;[done|]. iExists vl. done.
- iMod ("ToL" with "tok L") as "L".
iAssert (tctx_elt_interp tid (#v' +ₗ #1 ◁ &uniq{α} (vec_ty ty)) vπ ) with "[o ⧖u Vo]" as "te".
{ iExists #(v' +ₗ 1),( S (S du)).
iFrame "# ∗". iSplitR;[done|].
iExists (S du), ξi. rewrite /uniq_body. iFrame. iSplitR; [done|].
subst ξ. simpl.
admit.
}
rewrite -/(tctx_interp _ +[_ ◁ &uniq{_} (vec_ty _)] -[vπ]).
iApply (type_val (ℭ := ()) (𝔅l := [(listₛ 𝔄 * listₛ 𝔄)%ST;𝔄]) _ _ (fn<α>(∅; &uniq{α} (vec_ty ty), ty) → ()) +[_; _] _ _ _ _ _ (λ p '(-[Φ; a; b]), Φ p -[a; b]) $! _ _ -[vπ;aπ] with "LFT TIME PROPH UNIQ E Na L C [$] [Obs]").
apply vec_push_type. simpl. iExact "Obs".
Unshelve.
intro_subst. via_tr_impl.
iApply type_new; [done|]. intro_subst.
iApply type_assign.
solve_typing.
solve_typing.
solve_typing.
iApply (type_letcall α);[solve_typing|solve_extract|solve_typing|..]. intro_subst.
iApply type_jump. solve_typing. solve_extract. solve_typing.
move => ? [? [? [? []]]] //=.
}
{ simpl.
iDestruct "↦tys" as (wl) "(% & ↦tl & proph & a)".
iApply ( "push" with "[$] [↦tl] [↦l ↦len ↦ex proph a] [$] [$] [$] [$] [ToL L] [$] ToBor").
{ iExists wl. by iFrame. }
{ iExists [_; _; _]. iCombine "↦l ↦len ↦ex" as "↦v". rewrite -shift_loc_assoc -!heap_mapsto_vec_cons.
iFrame. iExists _, _, _, _. by iFrame. }
{ iIntros "?". iApply ("ToL" with "[$] [$]"). }
}
}
wp_read.
Qed.
End smallvec_push.
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment