From 57377e45f4f29b073986dbb50008e7775ad3967e Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 17 Mar 2022 23:33:57 +0900
Subject: [PATCH] Verify smallvec_pop
---
_CoqProject | 1 +
theories/typing/lib/smallvec/smallvec_pop.v | 146 ++++++++++++++++++++
2 files changed, 147 insertions(+)
create mode 100644 theories/typing/lib/smallvec/smallvec_pop.v
diff --git a/_CoqProject b/_CoqProject
index 01cb9313..0550d628 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -94,6 +94,7 @@ theories/typing/lib/smallvec/smallvec_basic.v
theories/typing/lib/smallvec/smallvec_slice.v
theories/typing/lib/smallvec/smallvec_index.v
theories/typing/lib/smallvec/smallvec_push.v
+theories/typing/lib/smallvec/smallvec_pop.v
# theories/typing/lib/fake_shared.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
diff --git a/theories/typing/lib/smallvec/smallvec_pop.v b/theories/typing/lib/smallvec/smallvec_pop.v
new file mode 100644
index 00000000..ff65b19c
--- /dev/null
+++ b/theories/typing/lib/smallvec/smallvec_pop.v
@@ -0,0 +1,146 @@
+From lrust.typing Require Export type.
+From lrust.typing Require Import array_util typing.
+From lrust.typing.lib Require Import option vec_util smallvec.smallvec.
+Set Default Proof Using "Type".
+
+Open Scope nat.
+Implicit Type 𝔄 𝔅: syn_type.
+
+Section smallvec_pop.
+ Context `{!typeG Σ}.
+
+ Definition smallvec_pop {𝔄} (ty: type 𝔄) : val :=
+ fn: ["v"] :=
+ let: "v'" := !"v" in delete [ #1; "v"];;
+ let: "len" := !("v'" +ₗ #2) in
+ let: "r" := new [ #(option_ty ty).(ty_size)] in
+ if: "len" ≤ #0 then
+ "r" <- #0;; return: ["r"]
+ else
+ let: "len'" := "len" - #1 in
+ "v'" +ₗ #2 <- "len'";; "r" <- #1;;
+ if: !"v'" then (* array mode *)
+ "r" +ₗ #1 <-{ty.(ty_size)} !("v'" +ₗ #4 +ₗ "len'" * #ty.(ty_size));;
+ return: ["r"]
+ else (* vector mode *)
+ "v'" +ₗ #3 <- !("v'" +ₗ #3) + #1;;
+ "r" +ₗ #1 <-{ty.(ty_size)} !(!("v'" +ₗ #1) +ₗ "len'" * #ty.(ty_size));;
+ return: ["r"].
+
+ Lemma smallvec_pop_type {𝔄} n (ty: type 𝔄) :
+ typed_val (smallvec_pop ty) (fn<α>(∅; &uniq{α} (smallvec n ty)) → option_ty ty)
+ (λ post '-[(al, al')], al' = removelast al → post (last_error al)).
+ Proof.
+ eapply type_fn; [apply _|]=> α ??[v[]]. simpl_subst.
+ iIntros (?[pπ[]]?) "#LFT TIME #PROPH #UNIQ #E Na L C /=[v _] #Obs".
+ rewrite tctx_hasty_val. iDestruct "v" as ([|]) "[_ v]"=>//.
+ case v as [[|v|]|]=>//. iDestruct "v" as "[(%vl & >↦ & [#LftIn uniq]) †]".
+ 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 (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.
+ 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.
+ wp_apply wp_new; [lia|done|]. iIntros (r) "[†r ↦r]".
+ rewrite Nat2Z.id/= heap_mapsto_vec_cons. iDestruct "↦r" as "[↦r ↦r']".
+ wp_let. wp_op. wp_if. case len as [|len]=>/=.
+ { wp_write. iMod ("ToBor" with "[↦₀ ↦₁ ↦₂ ↦₃ big Pc]") as "[Bor β]".
+ { iNext. iExists _, _. iFrame "⧖ Pc". rewrite split_mt_smallvec.
+ iExists _, _, _, _, _.
+ rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
+ by iFrame "↦₀ ↦₁ ↦₂ ↦₃ big". }
+ iMod ("ToL" with "β L") as "L".
+ iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty); #r ◁ box (option_ty ty)]
+ -[pπ; const None] with "[] LFT TIME PROPH UNIQ E Na L C [-] []").
+ - iApply type_jump; [solve_typing|solve_extract|solve_typing].
+ - rewrite/= !(tctx_hasty_val #_). iSplitR "↦r ↦r' †r".
+ { iExists _. iFrame "⧖ LftIn". iExists _, _. iFrame. iPureIntro.
+ split; [lia|done]. }
+ iSplitL; [|done]. iExists _. rewrite -freeable_sz_full. iFrame "⧖ †r".
+ iNext. rewrite /option_ty. setoid_rewrite mod_ty_own; [|apply _].
+ rewrite split_mt_sum. iExists 0%fin, (const ()). iSplit; [done|]. iFrame "↦r".
+ iSplitL. { iExists _. iFrame. iPureIntro. by rewrite/= repeat_length. }
+ iFrame. iExists []. rewrite heap_mapsto_vec_nil=>/=.
+ iSplit; [done|]. by iExists (const -[]).
+ - iApply proph_obs_impl; [|done]=> π. move: (equal_f Eq1 π)=>/=. clear.
+ inv_vec aπl. by case (pπ π)=>/= ??->. }
+ iMod (uniq_update with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
+ wp_op. wp_let. have ->: (S len - 1)%Z = len by lia. wp_op. do 2 wp_write.
+ wp_read. wp_if. set pπ' := λ π, (lapply (vinit aπl) π, π ξ). case b=>/=.
+ - iDestruct "big" as "[↦tys (%&% & ↦tl)]".
+ iDestruct (big_sepL_vinitlast with "↦tys") as "[↦tys (%& ↦last & ty)]"=>/=.
+ iDestruct (ty_size_eq with "ty") as %Lvl. do 4 wp_op. rewrite -Nat2Z.inj_mul.
+ wp_apply (wp_memcpy with "[$↦r' $↦last]"); [rewrite repeat_length; lia|lia|].
+ iIntros "[↦r' ↦last]". wp_seq.
+ iMod ("ToBor" with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tys ↦last ↦tl ⧖ Pc]") as "[Bor α]".
+ { 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 (_++_).
+ rewrite heap_mapsto_vec_app shift_loc_assoc -Z.add_assoc -Nat2Z.inj_add
+ -Lvl Nat.add_comm.
+ iFrame "↦last ↦tl". iPureIntro. rewrite app_length. lia. }
+ iMod ("ToL" with "α L") as "L".
+ iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty); #r ◁ box (option_ty ty)]
+ -[pπ'; Some ∘ _] with "[] LFT TIME PROPH UNIQ E Na L C [-] []").
+ + iApply type_jump; [solve_typing|solve_extract|solve_typing].
+ + rewrite/= !(tctx_hasty_val #_) right_id. iSplitL "Vo Bor".
+ * iExists _. iFrame "⧖ LftIn". iExists _, _. rewrite /uniq_body.
+ rewrite (proof_irrel (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ'))
+ (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ))). by iFrame.
+ * iExists _. rewrite -freeable_sz_full. iFrame "⧖ †r". iNext.
+ rewrite /option_ty. setoid_rewrite mod_ty_own; [|apply _].
+ rewrite split_mt_sum. iExists 1%fin, _. iSplit; [done|]. iFrame "↦r". iSplitR.
+ { iExists []. rewrite heap_mapsto_vec_nil left_id. iPureIntro=>/=.
+ move: ty.(ty_size)=> ?. lia. }
+ iExists _. iFrame "↦r'". iApply ty_own_depth_mono; [|done]. lia.
+ + iApply proph_obs_impl; [|done]=>/= π.
+ move: (equal_f Eq1 π) (equal_f Eq2 π)=>/=. clear. case (pπ π)=>/= ??->->.
+ have ->: last_error (lapply aπl π) = Some (vlast aπl π).
+ { 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_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.
+ do 2 wp_op. rewrite -Nat2Z.inj_mul.
+ wp_apply (wp_memcpy with "[$↦r' $↦last]"); [rewrite repeat_length; lia|lia|].
+ iIntros "[↦r' ↦last]". wp_seq.
+ iMod ("ToBor" with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tys ↦tl ↦last ↦ex † ⧖ Pc]") as "[Bor α]".
+ { 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. iPureIntro=>/=. lia. }
+ iMod ("ToL" with "α L") as "L".
+ iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty); #r ◁ box (option_ty ty)]
+ -[pπ'; Some ∘ _] with "[] LFT TIME PROPH UNIQ E Na L C [-] []").
+ + iApply type_jump; [solve_typing|solve_extract|solve_typing].
+ + rewrite/= !(tctx_hasty_val #_) right_id. iSplitL "Vo Bor".
+ * iExists _. iFrame "⧖ LftIn". iExists _, _. rewrite /uniq_body.
+ rewrite (proof_irrel (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ'))
+ (@prval_to_inh (listₛ 𝔄) (fst ∘ pπ))). by iFrame.
+ * iExists _. rewrite -freeable_sz_full. iFrame "⧖ †r". iNext.
+ rewrite /option_ty. setoid_rewrite mod_ty_own; [|apply _].
+ rewrite split_mt_sum. iExists 1%fin, _. iSplit; [done|]. iFrame "↦r". iSplitR.
+ { iExists []. rewrite heap_mapsto_vec_nil left_id. iPureIntro=>/=.
+ move: ty.(ty_size)=> ?. lia. }
+ iExists _. iFrame "↦r'". iApply ty_own_depth_mono; [|done]. lia.
+ + iApply proph_obs_impl; [|done]=>/= π.
+ move: (equal_f Eq1 π) (equal_f Eq2 π)=>/=. clear. case (pπ π)=>/= ??->->.
+ have ->: last_error (lapply aπl π) = Some (vlast aπl π).
+ { 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.
+ Qed.
+End smallvec_pop.
--
GitLab