diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index 9fac5a079f7614478700433a1221659f3fce9cc0..6761a22dbf5f3473b1d1a1f8225cacb010e05466 100644
--- a/theories/typing/lib/smallvec/smallvec_push.v
+++ b/theories/typing/lib/smallvec/smallvec_push.v
@@ -1,168 +1,140 @@
From lrust.typing Require Export type.
From lrust.typing Require Import array_util typing.
-From lrust.typing.lib.smallvec Require Import smallvec.
-From lrust.typing.lib.vec Require Import vec_pushpop vec.
+From lrust.typing.lib Require Import vec_util smallvec.smallvec.
Set Default Proof Using "Type".
Implicit Type 𝔄 𝔅: syn_type.
-
Section smallvec_push.
- Context `{!typeG Σ}.
-
- (*
- check the tag,
- if its an array and there's room, store it there
- otherwise, push to the vector
- *)
- Definition smallvec_push {𝔄} (ty: type 𝔄) (n : nat ) : val :=
- fn: ["self"; "v"] :=
- let: "self'" := !"self" in delete [ #1; "self"];;
- let: "tag" := !"self'" in
- withcont: "push":
- if: "tag" then (* array mode *)
- let: "len" := !("self'" +ₗ #2) in
- if: ( "len" + #1) ≤ #n then
- "self'" +ₗ #4 +ₗ "len" * #ty.(ty_size) <-{ty_size ty} !"v";;
- ("self'" +ₗ #2) <- "len" + #1;;
- let: "r" := new [ #0] in return: ["r"]
- else (* ruh-roh gotta allocate a vector and copy everything over*)
- 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" []
- (* vector mode *)
- cont: "push" [] :=
- let: "vec_push" := vec_push ty in
- let: "vec" := new [ #1] in
- "vec" <- "self'" +ₗ #1;;
- letcall: "r" := "vec_push" ["vec"; "v"] in
- return: ["r"] .
+ Context `{!typeG Σ}.
-(* useful to force type inverence to choose the correct type for vπ' *)
-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_core {𝔄} (n: nat) (ty: type 𝔄) : val :=
+ rec: BAnon ["v"; "x"] :=
+ if: !"v" then (* array mode *)
+ let: "len" := !("v" +ₗ #2) in "v" +ₗ #2 <- "len" + #1;;
+ if: "len" + #1 ≤ #n then
+ "v" +ₗ #4 +ₗ "len" * #ty.(ty_size) <-{ty.(ty_size)} !"x"
+ else
+ let: "l" := new [("len" + #1) * #ty.(ty_size)] in
+ memcpy ["l"; "len" * #ty.(ty_size); "v" +ₗ #4];;
+ "l" +ₗ "len" * #ty.(ty_size) <-{ty.(ty_size)} !"x";;
+ "v" <- #false;; "v" +ₗ #1 <- "l";; "v" +ₗ #3 <- #0
+ else (* vector mode *)
+ vec_push_core ty ["v" +ₗ #1; "x"].
-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 ()).
+ Lemma wp_smallvec_push_core {𝔄} n (ty: type 𝔄) (v x: loc) alπ bπ du dx tid E :
+ {{{
+ v ↦∗: (smallvec n ty).(ty_own) alπ du tid ∗ x ↦∗: ty.(ty_own) bπ dx tid
+ }}} smallvec_push_core n ty [ #v; #x] @ E {{{ RET #☠;
+ v ↦∗: (smallvec n ty).(ty_own) (λ π, alπ π ++ [bπ π]) (du `max` dx) tid ∗
+ x ↦∗len ty.(ty_size)
+ }}}.
Proof.
- eapply type_fn; [apply _|]=> α ϝ k [v[x[]]]. simpl_subst.
- iIntros (tid (vπ & aπ &[]) ?) "#LFT #TIME #PROPH #UNIQ #E Na L C /=(v & x &_) #Obs".
- rewrite tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//.
- case v as [[|v|]|]=>//. iDestruct "v" as "[(%vl & >↦ & [#LftIn uniq]) †]".
+ iIntros (?) "[big (%& ↦x & ty)] ToΦ". iDestruct (ty_size_eq with "ty") as %?.
+ 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.
+ iApply (wp_vec_push_core with "[↦' ↦tys ↦ex † ↦x ty]").
+ { iExists _, _. iFrame "↦' † ↦ex ↦tys". iExists _. iFrame. }
+ iIntros "!> (%&%& ↦' & ↦tys & ↦ex & † & ↦x)". iApply "ToΦ". iFrame "↦x".
+ rewrite split_mt_smallvec. iExists false, _, _, _, _. iFrame "↦tys ↦ex †".
+ iDestruct (heap_mapsto_vec_cons with "[$↦₀ $↦']") as "$".
+ iSplitR; last first. { iExists _. by iFrame. } iPureIntro. fun_ext=> ?.
+ by rewrite vec_to_list_snoc lapply_app. }
+ rewrite !heap_mapsto_vec_cons !shift_loc_assoc. iDestruct "↦'" as "(↦₁ & ↦₂ & ↦₃ &_)".
+ iDestruct "big" as "[↦tys (%wl & %EqLen & ↦tl)]".
+ wp_op. wp_read. wp_let. do 2 wp_op. wp_write. have ->: (len + 1)%Z = S len by lia.
+ do 2 wp_op. wp_if. case Cmp: (bool_decide _).
+ - move: Cmp=>/bool_decide_eq_true ?. do 3 wp_op. rewrite -Nat2Z.inj_mul.
+ have Lwl: length wl = ty.(ty_size) + (n - S len) * ty.(ty_size).
+ { rewrite Nat.mul_sub_distr_r Nat.add_sub_assoc; [lia|].
+ apply Nat.mul_le_mono_r. lia. }
+ move: (app_length_ex wl _ _ Lwl)=> [?[?[->[Lul ?]]]].
+ rewrite heap_mapsto_vec_app Lul !shift_loc_assoc. iDestruct "↦tl" as "[↦new ↦tl]".
+ iApply (wp_memcpy with "[$↦new $↦x]"); [lia..|]. iIntros "!> [↦new ↦x]".
+ iApply "ToΦ". iSplitR "↦x"; last first. { iExists _. by iFrame. }
+ rewrite split_mt_smallvec. iExists _, _, _, _, (vsnoc _ _).
+ rewrite !heap_mapsto_vec_cons !shift_loc_assoc heap_mapsto_vec_nil.
+ iFrame "↦₀ ↦₁ ↦₂ ↦₃"=>/=. iSplit.
+ { iPureIntro. fun_ext=> ?. by rewrite vec_to_list_snoc lapply_app. }
+ iSplitR "↦tl"; last first.
+ { have ->: ∀sz, (4 + (len * sz)%nat + sz = 4 + (sz + len * sz)%nat)%Z by lia.
+ iExists _. iFrame "↦tl". iPureIntro. lia. }
+ rewrite vec_to_list_snoc big_sepL_app big_sepL_singleton. iSplitL "↦tys".
+ + iStopProof. do 6 f_equiv. apply ty_own_depth_mono. lia.
+ + iExists _. iSplitL "↦new".
+ * rewrite vec_to_list_length Nat.add_0_r shift_loc_assoc. iFrame.
+ * iApply ty_own_depth_mono; [|done]. lia.
+ - do 2 wp_op. wp_bind (new _). iApply wp_new; [lia|done|]. iIntros "!>% [† ↦l]".
+ have ->: ∀sz: nat, ((len + 1) * sz)%Z = len * sz + sz by lia.
+ rewrite Nat2Z.id. wp_let. do 2 wp_op. wp_bind (memcpy _).
+ rewrite repeat_app heap_mapsto_vec_app. iDestruct "↦l" as "[↦l ↦new]".
+ rewrite repeat_length trans_big_sepL_mt_ty_own. iDestruct "↦tys" as (?) "[↦o tys]".
+ iDestruct (big_sepL_ty_own_length with "tys") as %Lwll.
+ iApply (wp_memcpy with "[$↦l $↦o]"); [rewrite repeat_length; lia|lia|].
+ iIntros "!>[↦l ↦o]". wp_seq. do 2 wp_op. rewrite -Nat2Z.inj_mul. wp_bind (memcpy _).
+ iApply (wp_memcpy with "[$↦new $↦x]"); [by rewrite repeat_length|lia|].
+ iIntros "!>[↦new ↦x]". wp_seq. wp_write. do 2 (wp_op; wp_write). iApply "ToΦ".
+ iSplitR "↦x"; last first. { iExists _. by iFrame. }
+ rewrite split_mt_smallvec. iExists _, _, _, 0, (vsnoc _ _).
+ 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 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.
+ + iExists _. rewrite Nat.add_0_r vec_to_list_length. iFrame "↦new".
+ iApply ty_own_depth_mono; [|done]. lia.
+ Qed.
+
+ Definition smallvec_push {𝔄} n (ty: type 𝔄) : val :=
+ fn: ["v"; "x"] :=
+ let: "v'" := !"v" in delete [ #1; "v"];;
+ smallvec_push_core n ty ["v'"; "x"];;
+ delete [ #ty.(ty_size); "x"];;
+ let: "r" := new [ #0] in return: ["r"].
+
+ Lemma smallvec_push_type {𝔄} n (ty: type 𝔄) :
+ typed_val (smallvec_push n ty) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ())
+ (λ post '-[(al, al'); a], al' = al ++ [a] → post ()).
+Proof.
+ eapply type_fn; [apply _|]=> α ??[v[x[]]]. simpl_subst.
+ iIntros (?(pπ & bπ &[])?) "#LFT #TIME #PROPH #UNIQ #E Na L C /=(v & x &_) #Obs".
+ rewrite !tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//.
+ case v as [[|v|]|]=>//. iDestruct "v" as "[(%vl & >↦v & [#LftIn uniq]) †v]".
case vl as [|[[|v'|]|][]]; try by iDestruct "uniq" as ">[]".
- rewrite heap_mapsto_vec_singleton. wp_read. wp_let. wp_bind (delete _).
- rewrite -heap_mapsto_vec_singleton freeable_sz_full.
- iApply (wp_delete with "[$↦ $†]"); [done|]. iIntros "!>_".
- iDestruct "uniq" as (du ξi [? Eq2]) "[Vo Bor]". move: Eq2. set ξ := PrVar _ ξi=> Eq2.
+ iDestruct "x" as ([|dx]) "[⧖x x]"=>//. case x as [[|x|]|]=>//=.
+ iDestruct "x" as "[↦ty †x]". rewrite heap_mapsto_vec_singleton. wp_read.
+ iDestruct "uniq" as (du ξ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_cons with "LFT Bor α") as "[(%&%& #⧖u & Pc & ↦vec) ToBor]"; [done|].
- set bor_body := (∃ vπ' d', ⧖(S d') ∗ .PC[ξ] vπ' d' ∗ (∃ vl : list val, v' ↦∗ vl ∗ ty_own (smallvec n ty) vπ' d' tid vl))%I.
+ iMod (bor_acc with "LFT Bor α") as "[(%&%& ⧖u & Pc & ↦sv) ToBor]"; [done|].
wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-].
- 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 "(↦₀ & ↦l & ↦len & ↦ex)".
- wp_read. wp_let. set push := (rec: "push" _ := _)%E.
- iAssert ( v' ↦ #false -∗ (v' +ₗ 1) ↦∗: ty_own (vec_ty ty) (fst ∘ vπ) (S du) tid -∗
- (∃ wl : list val, ⌜length wl = (n * ty_size ty)%nat⌝ ∗ (v' +ₗ 4) ↦∗ wl) -∗
- .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 "↦₀ ↦vec ↦tl Pc Vo C Na ToL Tx ToBor". rewrite /push. wp_rec.
- 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]=>//=; [by iMod ("Hvec") as "?"|]. iNext.
- iDestruct "Hvec" as (????) "([-> %] & ?)". iDestruct "↦tl" as (?) "(% & ↦tl)".
- iCombine "↦₀ v1" as "↦v". iCombine "↦v ↦tl" as "↦v".
- rewrite -heap_mapsto_vec_cons -heap_mapsto_vec_app.
- iExists _. iFrame. iExists false, _, _, _, _, _. by iFrame. }
- { iExists (fst ∘ vπ), (S du). iFrame "# Pc".
- iDestruct "↦vec" as (vl) "(? & v)". iExists vl. iFrame.
- iDestruct "v" as (????) "(? & ? & ?)". iExists _, _, _, _. iFrame. }
- iMod ("ToL" with "tok") as "L".
- iAssert (tctx_elt_interp tid (#v' +ₗ #1 ◁ &uniq{α} (vec_ty ty)) vπ ) with "[o Vo]" as "te".
- { iExists _, _. iFrame "# ∗". iSplitR; [done|]. iExists _, ξi. by iFrame. }
- iApply (type_type +[_; _] -[_; _] with "[] LFT TIME PROPH UNIQ E Na L C [$Tx $te]").
- - iApply type_val; [apply vec_push_type|]. intro_subst.
- iApply type_new; [done|]. intro_subst. iApply type_assign; [solve_typing..|].
- iApply (type_letcall α); [solve_typing|solve_extract|solve_typing|]. intro_subst.
- iApply type_jump; [solve_typing| solve_extract| solve_typing].
- - by iApply (proph_obs_impl with "Obs").
- }
- 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. do 2 wp_op. wp_if. case_eq (bool_decide (len + 1 ≤ n)%Z) => LenN.
- { iClear "push". assert (len + 1 ≤ n). { case_bool_decide; lia. }
- rewrite tctx_hasty_val. iDestruct "x" as ([|dx]) "[⧖x x]"=>//. case x as [[|x|]|]=>//.
- do 3 wp_op. wp_bind (_ <-{_} !_)%E. iApply (wp_persistent_time_receipt with "TIME ⧖x"); [done|].
- assert (length tl = ty_size ty + (n - len - 1) * ty_size ty) as Len.
- { rewrite -Nat.sub_add_distr Nat.mul_sub_distr_r Nat.add_sub_assoc; [lia|]. by apply Nat.mul_le_mono_r. }
- move: {Len}(app_length_ex tl _ _ Len)=> [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.
- iApply (wp_memcpy with "[$↦ $↦x]") ; [lia..|].
- 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 "ty_vec".
- { iExists vl. rewrite vec_to_list_length. iFrame. iApply (ty_own_depth_mono with "[$]"); lia. }
- iMod (uniq_update ξ (fst ∘ vπ') with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
- iMod ("ToBor" $! bor_body with "[] [Pc ↦₀ ↦l ↦len ty_vec Z ↦tl ↦ex]") as "[? tok]".
- { by iIntros "!> $". }
- { iExists _, (S d). iFrame "# ∗". iCombine "↦₀ ↦l ↦len ↦ex" as "↦v" .
- rewrite -shift_loc_assoc Nat2Z.inj_add Nat2Z.inj_mul -!shift_loc_assoc -!heap_mapsto_vec_cons.
- rewrite split_mt_smallvec. 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"; [by rewrite !Nat2Z.inj_add Nat2Z.inj_succ Nat2Z.inj_0 Z.one_succ|].
- rewrite vec_to_list_app. iSplitL "ty_vec Z".
- { rewrite big_sepL_snoc Nat2Z.inj_mul. iFrame. iNext. iClear "#". iStopProof. do 6 f_equiv. apply ty_own_depth_mono. lia. }
- iExists z. rewrite shift_loc_assoc !Nat2Z.inj_mul -Z.mul_succ_l -Z.add_1_r.
- rewrite Nat2Z.inj_add Nat2Z.inj_succ Nat2Z.inj_0 -Z.one_succ. iFrame.
- iPureIntro. rewrite K -Nat.mul_add_distr_r -Nat.sub_add_distr Nat.add_sub_assoc; lia.
- }
- iMod ("ToL" with "tok L") as "L".
- 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 "⧖ LftIn". iExists (S d), ξi.
- rewrite /uniq_body /bor_body /vπ' /ξ (proof_irrel (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ)) (prval_to_inh (𝔄 := listₛ _) (fst ∘ vπ'))).
- iSplitR. iSplit; [done|]. iPureIntro. fun_ext => ? //=. iFrame.
- - 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_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.
- 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 "[$] [tys †' ↦' ↦l ↦ex ↦ε ↦len] [↦tl ↦] [$] [$] [$] [$] [ToL L] [$] ToBor").
- { iExists [_; _; _]. iClear "push". rewrite !heap_mapsto_vec_cons -!shift_loc_assoc. iFrame.
- iExists _, _, 0,_. iSplitR; [done|].
- rewrite trans_big_sepL_mt_ty_own Nat.add_0_r Nat2Z.id. iFrame. iSplitL.
- - iExists _. iFrame.
- - iExists []. rewrite heap_mapsto_vec_nil //=. }
- { iExists (concat wll ++ tl). rewrite heap_mapsto_vec_app app_length Len -!shift_loc_assoc. by iFrame. }
- { iIntros. iApply ("ToL" with "[$] [$]"). } } }
- { iDestruct "↦tys" as (wl) "(% & ↦tl & proph & a)".
- iApply ( "push" with "[$] [↦l ↦len ↦ex proph a] [↦tl] [$] [$] [$] [$] [ToL L] [$] ToBor").
- { iExists [_; _; _]. rewrite !heap_mapsto_vec_cons -!shift_loc_assoc. iFrame. iExists _, _, _, _. by iFrame. }
- { iExists wl. by iFrame. }
- { iIntros "?". iApply ("ToL" with "[$] [$]"). }
- }
+ wp_bind (delete _). rewrite -heap_mapsto_vec_singleton freeable_sz_full.
+ iApply (wp_delete with "[$↦v $†v]"); [done|]. iCombine "⧖u ⧖x" as "#⧖".
+ iIntros "!>_". wp_seq. wp_bind (smallvec_push_core _ _ _).
+ iApply (wp_smallvec_push_core with "[$↦sv $↦ty]").
+ iIntros "!>[↦sv (%& %Lvl & ↦x)]". wp_seq. rewrite freeable_sz_full.
+ wp_bind (delete _). iApply (wp_delete with "[$↦x †x]"); [lia|by rewrite Lvl|].
+ iIntros "!>_". wp_seq. set pπ' := λ π, ((pπ π).1 ++ [bπ π], π ξ).
+ iMod (uniq_update with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
+ iMod ("ToBor" with "[Pc ↦sv]") as "[Bor α]". { iExists _, _. iFrame "⧖ Pc ↦sv". }
+ iMod ("ToL" with "α L") as "L".
+ iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty)] -[pπ']
+ 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 "⧖ LftIn". iExists _, _. rewrite /uniq_body.
+ rewrite (proof_irrel (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ'))
+ (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ))). by iFrame.
+ - iApply proph_obs_impl; [|done]=>/= π. move: (equal_f Eq2 π)=>/=.
+ by case (pπ π)=>/= ??->.
Qed.
-End smallvec_push.
\ No newline at end of file
+End smallvec_push.