diff --git a/theories/caesium/layout.v b/theories/caesium/layout.v
index bca95401d6ed4f8d978f0bec5eed988cc967461a..e16dc43f73726f4289f4e54cd3d6f0087088a9c5 100644
--- a/theories/caesium/layout.v
+++ b/theories/caesium/layout.v
@@ -113,6 +113,10 @@ Lemma ly_size_mk_array_layout (n : nat) ly :
Proof.
rewrite /mk_array_layout /ly_mult /ly_size //.
Qed.
+Lemma ly_align_mk_array_layout ly n :
+ ly_align (mk_array_layout ly n) = ly_align ly.
+Proof. done. Qed.
+
(*** Lemmas about [layout] *)
diff --git a/theories/caesium/lifting.v b/theories/caesium/lifting.v
index 63b1ae58a02734f6030b1c3b8be867c08fc7de03..f63e1f44f628340119af0010b8f6ac84e3723fc3 100644
--- a/theories/caesium/lifting.v
+++ b/theories/caesium/lifting.v
@@ -364,6 +364,23 @@ Section logical_steps.
iIntros "HP". rewrite /maybe_logical_step.
destruct b; first iApply logical_step_intro; eauto.
Qed.
+
+ Lemma maybe_logical_step_fupd step F P :
+ maybe_logical_step step F (|={F}=> P) -∗
+ maybe_logical_step step F P.
+ Proof.
+ destruct step; simpl.
+ - iApply logical_step_fupd.
+ - rewrite fupd_trans; auto.
+ Qed.
+
+ Lemma maybe_logical_step_compose (E : coPset) step (P Q : iProp Σ) :
+ maybe_logical_step step E P -∗ maybe_logical_step step E (P -∗ Q) -∗ maybe_logical_step step E Q.
+ Proof.
+ iIntros "Ha Hb". destruct step; simpl.
+ - iApply (logical_step_compose with "Ha Hb").
+ - iMod "Ha". iMod "Hb". by iApply "Hb".
+ Qed.
End logical_steps.
(*** General lifting lemmas *)
diff --git a/theories/caesium/struct.v b/theories/caesium/struct.v
index dd15d992787368e0d33de0003dbf24dae6d020ab..4ebf560388ebc7e37261d443571893eda86bbd0c 100644
--- a/theories/caesium/struct.v
+++ b/theories/caesium/struct.v
@@ -222,6 +222,31 @@ Proof.
eapply IH; done.
Qed.
+Lemma pad_struct_lookup_Some_Some {A} s l f k (x : A) n ly :
+ length l = length (field_names s) →
+ pad_struct s l f !! k = Some x →
+ s !! k = Some (Some n, ly) →
+ l !! field_idx_of_idx s k = Some x.
+Proof.
+ intros Hlen Hlook1 Hlook2.
+ apply pad_struct_lookup_Some in Hlook1; last done.
+ destruct Hlook1 as (n' & ly' & Hlooka & Hlook1).
+ rewrite Hlook2 in Hlooka. injection Hlooka as [= <- <-].
+ destruct Hlook1 as [(_ & ?) | (? & _)]; naive_solver.
+Qed.
+Lemma pad_struct_lookup_Some_None {A} s l f k (x : A) ly :
+ length l = length (field_names s) →
+ pad_struct s l f !! k = Some x →
+ s !! k = Some (None, ly) →
+ x = f ly.
+Proof.
+ intros Hlen Hlook1 Hlook2.
+ apply pad_struct_lookup_Some in Hlook1; last done.
+ destruct Hlook1 as (n' & ly' & Hlooka & Hlook1).
+ rewrite Hlook2 in Hlooka. injection Hlooka as [= <- <-].
+ destruct Hlook1 as [(? & ?) | (? & ?)]; naive_solver.
+Qed.
+
Lemma pad_struct_insert_field {A} s (l : list A) f i j n x :
index_of s n = Some j →
field_index_of s n = Some i →
diff --git a/theories/caesium/time.v b/theories/caesium/time.v
index 2f8807acd0d91149e2ef54b48d955dee491b290f..835449f2a5e288f5a87fe4ae97edb2f7d1244543 100644
--- a/theories/caesium/time.v
+++ b/theories/caesium/time.v
@@ -105,6 +105,10 @@ Section time.
Global Instance additive_time_receipt_into_sep n m : IntoSep atime (n + m) atime n atime m.
Proof. rewrite /IntoSep. by rewrite additive_time_receipt_sep. Qed.
+ Lemma additive_time_receipt_succ n :
+ atime (S n) ⊣⊢ atime 1 ∗ atime n.
+ Proof. by rewrite -additive_time_receipt_sep. Qed.
+
Lemma persistent_time_receipt_0 : ⊢ |==> ptime 0.
Proof. rewrite /persistent_time_receipt. apply own_unit. Qed.
Lemma additive_time_receipt_0 : ⊢ |==> atime 0.
diff --git a/theories/caesium/val.v b/theories/caesium/val.v
index 96c3b5b1c8d0ea143c42946280bd3a6ec9329290..cec1c8c982b241fd265abdad86c713dc0f9b24f0 100644
--- a/theories/caesium/val.v
+++ b/theories/caesium/val.v
@@ -376,6 +376,13 @@ Lemma i2v_bool_Some b it:
val_to_Z (i2v (bool_to_Z b) it) it = Some (bool_to_Z b).
Proof. apply: val_to_of_Z. apply val_of_Z_bool. Qed.
+Lemma val_of_bool_i2v b :
+ val_of_bool b = i2v (bool_to_Z b) u8.
+Proof.
+ apply val_of_bool_iff_val_of_Z.
+ apply val_of_Z_bool.
+Qed.
+
Definition val_to_Z_ot (v : val) (ot : op_type) : option Z :=
match ot with
diff --git a/theories/rust_typing/arrays.v b/theories/rust_typing/arrays.v
index a363edf144515eb1d410b7eb3b1d453456f42e68..db9989fd128c8ae7bce13d4142d70a92972de7b7 100644
--- a/theories/rust_typing/arrays.v
+++ b/theories/rust_typing/arrays.v
@@ -668,7 +668,7 @@ Section subltype.
iIntros (Hst) "#Hel".
iModIntro. iIntros (Ï€ l) "Ha".
rewrite !ltype_own_array_unfold /array_ltype_own.
- iDestruct "Ha" as "(%ly & %Halg & %Hsz & %Hly & Hlb & ? & ? & Hrfn & Ha)".
+ iDestruct "Ha" as "(%ly & %Halg & %Hsz & %Hly & Hlb & ? & Hrfn & Ha)".
iExists ly. iSplitR. { rewrite -Hst. done. }
iR. iR. iFrame.
iMod "Ha". iModIntro.
@@ -969,6 +969,12 @@ Section lemmas.
iIntros (Hst). iPureIntro. simp_ltypes. rewrite Hst. done.
Qed.
+ Lemma typed_place_cond_rfn_lift_array {rt} (rs rs' : list (place_rfn rt)) k :
+ ([∗ list] ty1;ty2 ∈ rs; rs', typed_place_cond_rfn k ty1 ty2) ⊢@{iProp Σ} typed_place_cond_rfn k (#rs) (#rs').
+ Proof. iIntros "Ha". destruct k; done. Qed.
+
+
+
Lemma array_ltype_acc_owned' {rt} F π (def : type rt) (len : nat) (lts : list (nat * ltype rt)) (rs : list (place_rfn rt)) l wl :
lftE ⊆ F →
l â—â‚—[Ï€, Owned wl] #rs @ ArrayLtype def len lts -∗
@@ -987,7 +993,6 @@ Section lemmas.
={F}=∗
l â—â‚—[Ï€, Owned wl] #rs' @ ArrayLtype def' len lts').
Proof.
- (* TODO *)
iIntros (?) "Hb". rewrite ltype_own_array_unfold /array_ltype_own.
iDestruct "Hb" as "(%ly & %Hst & % & %Hly & #Hlb & Hcred & %r' & <- & <- & Hb)".
iExists ly. iR. iR. iR. iR.
@@ -1063,7 +1068,180 @@ Section lemmas.
*)
Qed.
- (* TODO: uniq access *)
+ Local Lemma typed_place_cond_ty_uniq_core_eq_array {rt} (def : type rt) (def' : type rt) lts lts' len κ γ :
+ ([∗ list] ty1; ty2 ∈ interpret_iml (◠def)%I len lts; interpret_iml (◠def')%I len lts', typed_place_cond_ty (Uniq κ γ) ty1 ty2) -∗
+ ([∗ list] ty1; ty2 ∈ interpret_iml (◠def)%I len lts; interpret_iml (◠def')%I len lts', ∀ b' r, ltype_eq b' r r (ltype_core ty1) (ltype_core ty2)).
+ Proof.
+ iIntros "Hcond". iApply (big_sepL2_impl with "Hcond").
+ iModIntro. iIntros (? lt1 lt2 Hlook1 Hlook2).
+ iApply typed_place_cond_ty_uniq_core_eq.
+ Qed.
+ Local Lemma typed_place_cond_ty_uniq_unblockable_array {rt} (def : type rt) (def' : type rt) lts lts' len κ γ :
+ ([∗ list] ty1; ty2 ∈ interpret_iml (◠def)%I len lts; interpret_iml (◠def')%I len lts', typed_place_cond_ty (Uniq κ γ) ty1 ty2) -∗
+ ([∗ list] ty1; ty2 ∈ interpret_iml (◠def)%I len lts; interpret_iml (◠def')%I len lts', imp_unblockable [κ] ty2).
+ Proof.
+ iIntros "Hcond". iApply (big_sepL2_impl with "Hcond").
+ iModIntro. iIntros (? lt1 lt2 Hlook1 Hlook2).
+ iApply typed_place_cond_ty_uniq_unblockable.
+ Qed.
+
+ Local Lemma array_acc_uniq_elems_unblock π l {rt} len (def def' : type rt) ly lts lts' (rs : list (place_rfn rt)) κ γ :
+ syn_type_has_layout (ty_syn_type def) ly →
+ ty_syn_type def = ty_syn_type def' →
+ ([∗ list] ty1;ty2 ∈ interpret_iml (◠def) len lts; interpret_iml (◠def')%I len lts', typed_place_cond_ty (Uniq κ γ) ty1 ty2) -∗
+ [†κ] -∗
+ (|={lftE}=> [∗ list] i↦lt;r0 ∈ interpret_iml (â— def') len lts';rs, ⌜ ltype_st lt = ty_syn_type def⌠∗ (l offset{ly}â‚— i) â—â‚—[ Ï€, Owned false] r0 @ lt) -∗
+ |={lftE}=> [∗ list] i↦lt;r0 ∈ interpret_iml (â— def) len lts;rs, ⌜ ltype_st lt = ty_syn_type def⌠∗ (l offset{ly}â‚— i) â—â‚—[ Ï€, Owned false] r0 @ ltype_core lt.
+ Proof.
+ iIntros (Hst Hst_eq) "#Hcond #Hdead >Hb". iApply big_sepL2_fupd.
+ iPoseProof (big_sepL2_length with "Hb") as "%Hlen2". rewrite interpret_iml_length in Hlen2.
+ iPoseProof (big_sepL2_to_zip with "Hb") as "Hb".
+ iApply big_sepL2_from_zip. { rewrite interpret_iml_length. done. }
+ iPoseProof (big_sepL_extend_r with "Hb") as "Hb"; first last.
+ { iApply big_sepL2_elim_l. iApply (big_sepL2_impl with "Hb").
+ iModIntro. iIntros (? [lt1 r1] [lt2 r2] Hlook1 Hlook2).
+ simpl. iIntros "(%Hst1 & Hl)".
+ apply lookup_zip in Hlook1 as (Hlook1 & Hlook1').
+ apply lookup_zip in Hlook2 as (Hlook2 & Hlook2'). simpl in *.
+ assert (r1 = r2) as -> by naive_solver.
+ iPoseProof (typed_place_cond_ty_uniq_core_eq_array _ _ _ _ _ κ γ with "Hcond") as "Heq".
+ iPoseProof (typed_place_cond_ty_uniq_unblockable_array _ _ _ _ _ κ γ with "Hcond") as "Hub".
+ iPoseProof (big_sepL2_lookup with "Heq") as "Heq1"; [ done.. | ].
+ iPoseProof (big_sepL2_lookup with "Hub") as "Hub1"; [ done.. | ].
+ iMod (imp_unblockable_use with "Hub1 [] Hl") as "Hl"; first done.
+ { iFrame "Hdead"; done. }
+ iDestruct ("Heq1" $! (Owned _) _) as "((%Hst1' & #Heq1' & _) & (_ & #Heq2 & _))".
+ iMod ("Heq2" with "Hl") as "Hl".
+ rewrite !ltype_core_syn_type_eq in Hst1'.
+ rewrite -Hst1. eauto with iFrame.
+ }
+ rewrite !zip_length !interpret_iml_length//.
+ Qed.
+ Local Lemma array_acc_uniq_elems_core_eq π l {rt} len (def def' : type rt) ly lts lts' (rs : list (place_rfn rt)) :
+ syn_type_has_layout (ty_syn_type def) ly →
+ ty_syn_type def = ty_syn_type def' →
+ ([∗ list] ty1;ty2 ∈ interpret_iml (◠def) len lts; interpret_iml (◠def')%I len lts', ∀ b' r, ltype_eq b' r r (ltype_core ty1) (ltype_core ty2)) -∗
+ (|={lftE}=> [∗ list] i↦lt;r0 ∈ interpret_iml (â— def) len lts;rs, ⌜ ltype_st lt = ty_syn_type def⌠∗ (l offset{ly}â‚— i) â—â‚—[ Ï€, Owned false] r0 @ ltype_core lt) -∗
+ |={lftE}=> [∗ list] i↦lt;r0 ∈ interpret_iml (â— def') len lts';rs, ⌜ ltype_st lt = ty_syn_type def⌠∗ (l offset{ly}â‚— i) â—â‚—[ Ï€, Owned false] r0 @ ltype_core lt.
+ Proof.
+ iIntros (Hst Hst_eq) "#Heq >Hb". iApply big_sepL2_fupd.
+ iPoseProof (big_sepL2_length with "Hb") as "%Hlen2". rewrite interpret_iml_length in Hlen2.
+ iPoseProof (big_sepL2_to_zip with "Hb") as "Hb".
+ iApply big_sepL2_from_zip. { rewrite interpret_iml_length. done. }
+ iPoseProof (big_sepL_extend_r with "Hb") as "Hb"; first last.
+ { iApply big_sepL2_elim_l. iApply (big_sepL2_impl with "Hb").
+ iModIntro. iIntros (? [lt1 r1] [lt2 r2] Hlook1 Hlook2).
+ simpl. iIntros "(%Hst1 & Hl)".
+ apply lookup_zip in Hlook1 as (Hlook1 & Hlook1').
+ apply lookup_zip in Hlook2 as (Hlook2 & Hlook2'). simpl in *.
+ assert (r1 = r2) as -> by naive_solver.
+ iPoseProof (big_sepL2_lookup with "Heq") as "Heq1"; [ done.. | ].
+ iDestruct ("Heq1" $! (Owned _) _) as "((%Hst1' & #Heq1' & _) & (_ & #Heq2 & _))".
+ iMod ("Heq1'" with "Hl") as "Hl".
+ rewrite !ltype_core_syn_type_eq in Hst1'.
+ rewrite -Hst1. eauto with iFrame.
+ }
+ rewrite !zip_length !interpret_iml_length//.
+ Qed.
+
+ Lemma array_ltype_acc_uniq {rt} F π (def : type rt) (len : nat) (lts : list (nat * ltype rt)) (rs : list (place_rfn rt)) l R q κ γ :
+ lftE ⊆ F →
+ rrust_ctx -∗
+ q.[κ] -∗
+ (q.[κ] ={lftE}=∗ R) -∗
+ l â—â‚—[Ï€, Uniq κ γ] #rs @ ArrayLtype def len lts -∗
+ ∃ ly, ⌜syn_type_has_layout def.(ty_syn_type) ly⌠∗
+ ⌜l `has_layout_loc` (mk_array_layout ly len)⌠∗
+ ⌜(ly_size ly * len ≤ max_int isize_t)%Z⌠∗
+ (*⌜Forall (λ '(i, _), i < len) lts⌠∗*)
+ loc_in_bounds l 0 (ly.(ly_size) * len) ∗ |={F}=>
+ ([∗ list] i↦lt;r0 ∈ interpret_iml (â— def) len lts;rs, ⌜ltype_st lt = ty_syn_type def⌠∗ (l offset{ly}â‚— i) â—â‚—[Ï€, Owned false] r0 @ lt) ∗
+ logical_step F
+ (∀ (def' : type rt) (lts' : list (nat * ltype rt)) (rs' : list (place_rfn rt)) bmin,
+ ⌜ty_syn_type def = ty_syn_type def'⌠-∗
+ ⌜len = length rs'⌠-∗
+ bmin ⊑ₖ Uniq κ γ -∗
+ ([∗ list] ty1; ty2 ∈ interpret_iml (◠def) len lts; interpret_iml (◠def') len lts', typed_place_cond_ty (bmin) (ty1) (ty2)) -∗
+ ([∗ list] r1; r2 ∈ rs; rs', typed_place_cond_rfn (bmin) (r1) (r2)) -∗
+ (* new ownership *)
+ ([∗ list] i↦lt;r0 ∈ interpret_iml (â— def') len lts';rs', ⌜ltype_st lt = ty_syn_type def'⌠∗ (l offset{ly}â‚— i) â—â‚—[Ï€, Owned false] r0 @ lt)
+ ={F}=∗
+ l â—â‚—[Ï€, Uniq κ γ] #rs' @ ArrayLtype def' len lts' ∗
+ R ∗
+ typed_place_cond (Uniq κ γ ⊓ₖ bmin) (ArrayLtype def len lts) (ArrayLtype def' len lts') (#rs) (#rs')
+ ).
+ Proof.
+ (* TODO *)
+ iIntros (?) "#(LFT & TIME & LLCTX) Htok Htokcl Hb". rewrite ltype_own_array_unfold /array_ltype_own.
+ iDestruct "Hb" as "(%ly & %Hst & % & %Hly & #Hlb & Hcred & Hrfn & Hb)".
+ iExists ly. iR. iR. iR. iR.
+ iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
+ iMod "Hb".
+ iMod (pinned_bor_acc_strong lftE with "LFT Hb Htok") as "(%κ'' & #Hincl & Hb & _ & Hb_cl)"; first done.
+ iMod "Hcl_F" as "_".
+ iDestruct "Hcred" as "((Hcred1 & Hcred) & Hat)".
+ iApply (lc_fupd_add_later with "Hcred1"). iNext.
+ iDestruct "Hb" as "(%r' & Hauth & %Hlen & Hb)".
+ iPoseProof (gvar_agree with "Hauth Hrfn") as "#->".
+ iMod (fupd_mask_mono with "Hb") as "Hb"; first done.
+ iModIntro. iFrame.
+ iApply (logical_step_intro_atime with "Hat").
+ iIntros "Hcred' Hat".
+ iModIntro.
+ (* close with updated type *)
+ iIntros (def' lts' rs' bmin Hst_eq Hlen_eq) "#Hincl' #Hcond_ty #Hcond_rfn Hb".
+ iMod (gvar_update rs' with "Hauth Hrfn") as "(Hauth & Hrfn)".
+ set (V := (∃ r', gvar_auth γ r' ∗ ⌜length r' = len⌠∗ (|={lftE}=> [∗ list] i↦lt;r0 ∈ interpret_iml (◠def') len lts';r', ⌜ltype_st lt = ty_syn_type def⌠∗ ltype_own lt (Owned false) π r0 (l offset{ly}ₗ i)))%I).
+ iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
+ iDestruct "Hcred" as "(Hcred1 & Hcred)".
+ iMod ("Hb_cl" $! V with "[] Hcred1 [Hauth Hb]") as "(Hb & Htok)".
+ { iNext. iIntros "(%r' & Hauth & %Hlen' & Hb) Hdead".
+ iModIntro. iNext. iExists r'. iFrame "Hauth". iR.
+ iMod (lft_incl_dead with "Hincl Hdead") as "Hdead"; first done.
+ setoid_rewrite ltype_own_core_equiv.
+ iApply (array_acc_uniq_elems_unblock with "[Hcond_ty] Hdead Hb").
+ { done. } { done. }
+ iApply (big_sepL2_impl with "Hcond_ty").
+ iModIntro. iIntros (? [] [] ? ?).
+ iApply typed_place_cond_ty_incl. done.
+ }
+ { iModIntro. rewrite /V. iExists rs'. iFrame. rewrite Hst_eq. eauto 8 with iFrame. }
+ iMod ("Htokcl" with "Htok") as "$".
+ iMod "Hcl_F" as "_".
+ iModIntro.
+ (* TODO maybe donate the leftover credits *)
+ iSplitL.
+ { rewrite ltype_own_array_unfold /array_ltype_own.
+ iExists ly. iFrame. rewrite -Hst_eq. do 4 iR.
+ iPoseProof (pinned_bor_shorten with "Hincl Hb") as "Hb".
+ iModIntro. subst V.
+ (* need to adapt the pinned part, too *)
+ iApply (pinned_bor_iff with "[] [] Hb").
+ { iNext. iModIntro. eauto. }
+ iNext. iModIntro.
+ setoid_rewrite ltype_own_core_equiv.
+
+ iAssert ([∗ list] ty1;ty2 ∈ interpret_iml (◠def) len lts; interpret_iml (◠def') len lts', typed_place_cond_ty (Uniq κ γ) ty1 ty2)%I with "[Hcond_ty]" as "Ha".
+ { iApply (big_sepL2_impl with "Hcond_ty"). iModIntro. iIntros (k ? ? ? ?). by iApply typed_place_cond_ty_incl. }
+ iSplit.
+ - iIntros "(%r' & Hauth & ? & Hb)". iExists r'. iFrame. iMod "Hb".
+ iApply (array_acc_uniq_elems_core_eq with "[] Hb"). { done. } { done. }
+ iApply typed_place_cond_ty_uniq_core_eq_array. done.
+ - iIntros "(%r' & Hauth & ? & Hb)". iExists r'. iFrame. iMod "Hb".
+ rewrite Hst_eq. iApply (array_acc_uniq_elems_core_eq with "[] Hb").
+ { rewrite -Hst_eq. done. } { done. }
+ iPoseProof (typed_place_cond_ty_uniq_core_eq_array with "Ha") as "Hb".
+ iApply big_sepL2_flip. iApply (big_sepL2_impl with "Hb").
+ iModIntro. iIntros (? ? ? ? ?) "Heq" => /=.
+ iIntros (??). iApply ltype_eq_sym. iApply "Heq".
+ }
+ iApply (typed_place_cond_incl bmin).
+ { iApply bor_kind_incl_glb; first done. iApply bor_kind_incl_refl. }
+ iSplit.
+ + iApply (array_ltype_place_cond_ty _ _ with "Hcond_ty"); last done.
+ apply place_access_rt_rel_refl.
+ + by iApply (typed_place_cond_rfn_lift_array).
+ Qed.
Lemma array_ltype_acc_shared {rt} F π (def : type rt) (len : nat) (lts : list (nat * ltype rt)) (rs : list (place_rfn rt)) l κ :
lftE ⊆ F →
@@ -1099,19 +1277,85 @@ Section lemmas.
iExists _. iR. iR. iModIntro. by iFrame "Hb''".
}
iIntros (bmin) "Hcond".
- iSplitL; first last.
- { destruct bmin;done. }
+ iSplitL; first last.
+ { destruct bmin;done. }
(*last iApply typed_place_cond_rfn_refl.*)
iApply array_ltype_place_cond_ty.
- apply place_access_rt_rel_refl.
- done.
- done.
Qed.
+
+ Lemma array_val_from_uninit π v st1 st2 ly1 ly2 len :
+ syn_type_has_layout st1 ly1 →
+ syn_type_has_layout st2 ly2 →
+ ly_size ly1 = ly_size ly2 * len →
+ v â—áµ¥{ Ï€} .@ uninit st1 -∗
+ v â—áµ¥{ Ï€} replicate len (# ()) @ array_t (uninit st2) len.
+ Proof.
+ intros Hst1 Hst2 Hly.
+ rewrite /ty_own_val/=.
+ iDestruct 1 as "(%ly0 & %Hly0 & %Hlyv0 & _)".
+ assert (ly0 = ly1) as ->. { by eapply syn_type_has_layout_inj. }
+ (*assert (ly0 = ly1) as -> by by eapply syn_type_has_layout_inj.*)
+ iExists _. iR.
+ iSplitR. { iPureIntro. apply (use_layout_alg_size) in Hst1. lia. }
+ rewrite replicate_length. iR.
+ iSplitR. { rewrite /has_layout_val/mk_array_layout/ly_mult /= -Hly /=. done. }
+ iApply big_sepL2_intro.
+ { rewrite reshape_length !replicate_length//. }
+ iModIntro. iIntros (k ?? Hlook1 Hlook2).
+ apply lookup_replicate in Hlook1 as (-> & ?).
+ iExists _. iR.
+ rewrite uninit_own_spec.
+ iExists _. iR.
+ iPureIntro. rewrite /has_layout_val.
+ apply elem_of_list_lookup_2 in Hlook2.
+ apply reshape_replicate_elem_length in Hlook2; first done.
+ rewrite Hlyv0. lia.
+ Qed.
End lemmas.
Section rules.
Context `{!typeGS Σ}.
+ Local Lemma typed_place_cond_ty_array_lift {rt} (def : type rt) len bmin i lts (lt1 lt2 : ltype rt) :
+ interpret_iml (◠def)%I len lts !! i = Some lt1 →
+ ([∗ list] κ ∈ concat ((λ '(_, lt), ltype_blocked_lfts lt) <$> lts), bor_kind_outlives bmin κ) -∗
+ typed_place_cond_ty bmin lt1 lt2 -∗
+ [∗ list] lt1;lt2 ∈ interpret_iml (◠def) len lts;<[i:= lt2]> (interpret_iml (◠def) len lts), typed_place_cond_ty bmin lt1 lt2.
+ Proof.
+ iIntros (Hlook) "#Houtl Hcond".
+ rewrite -{1}(list_insert_id (interpret_iml _ _ _) i lt1); last done.
+ rewrite (big_sepL2_insert _ _ _ _ _ (λ _ lt1 lt2, typed_place_cond_ty bmin lt1 lt2) 0); cycle 1.
+ { by eapply lookup_lt_Some. }
+ { by eapply lookup_lt_Some. }
+ iFrame. iApply big_sepL2_intro; first done.
+ iModIntro. iIntros (k lt1' lt2' Hlook' ?). case_decide; first done.
+ assert (lt1' = lt2') as -> by congruence.
+ apply lookup_interpret_iml_Some_inv in Hlook' as (? & [-> | Hel]).
+ { iApply typed_place_cond_ty_refl_ofty. }
+ apply elem_of_list_lookup_1 in Hel as (k' & Hlook2).
+ iApply typed_place_cond_ty_refl.
+ iPoseProof (big_sepL_concat_lookup _ _ k' with "Houtl") as "Ha".
+ { rewrite list_lookup_fmap Hlook2. done. }
+ done.
+ Qed.
+ Local Lemma typed_place_cond_rfn_array_lift {rt} (rs : list (place_rfn rt)) ri1 ri2 i bmin :
+ rs !! i = Some ri1 → ⊢@{iProp Σ}
+ typed_place_cond_rfn bmin ri1 ri2 -∗
+ [∗ list] r1;r2 ∈ rs;<[i:=ri2]> rs, typed_place_cond_rfn bmin r1 r2.
+ Proof.
+ iIntros (Hlook) "Hcond".
+ specialize (lookup_lt_Some _ _ _ Hlook) as Hlt.
+ rewrite -{1}(list_insert_id rs i ri1); last done.
+ rewrite (big_sepL2_insert _ _ _ _ _ (λ _ r1 r2, _) 0); [ | lia..].
+ iSplitL; first done.
+ iApply big_sepL2_intro; first done. iModIntro.
+ iIntros (? r1 r2 ??). case_decide; first done.
+ assert (r1 = r2) as -> by congruence. destruct bmin; done.
+ Qed.
+
(** ** typed_place *)
Lemma typed_place_array_owned π E L {rt rtv} (def : type rt) (lts : list (nat * ltype rt)) (len : nat) (rs : list (place_rfn rt)) wl bmin ly l it v (tyv : type rtv) (i : rtv) P T :
(∃ i',
@@ -1190,28 +1434,8 @@ Section rules.
iModIntro.
iDestruct "Hcond" as "(Hcond & Hcond_rfn)".
iApply ("Hcondv" with "[Hcond] [Hcond_rfn] []").
- - simpl.
- rewrite -{1}(list_insert_id (interpret_iml _ _ _) i lti); last done.
- rewrite (big_sepL2_insert _ _ _ _ _ (λ _ lt1 lt2, typed_place_cond_ty bmin lt1 lt2) 0); cycle 1.
- { rewrite interpret_iml_length. lia. }
- { rewrite interpret_iml_length. lia. }
- iFrame. iApply big_sepL2_intro; first done.
- iModIntro. iIntros (k lt1 lt2 Hlook ?). case_decide; first done.
- assert (lt1 = lt2) as -> by congruence.
- apply lookup_interpret_iml_Some_inv in Hlook as (? & [-> | Hel]).
- { iApply typed_place_cond_ty_refl_ofty. }
- apply elem_of_list_lookup_1 in Hel as (k' & Hlook).
- iApply typed_place_cond_ty_refl.
- iPoseProof (big_sepL_concat_lookup _ _ k' with "Houtl") as "Ha".
- { rewrite list_lookup_fmap Hlook. done. }
- done.
- - rewrite -{1}(list_insert_id rs i ri); last done.
- rewrite (big_sepL2_insert _ _ _ _ _ (λ _ r1 r2, _) 0); [ | lia..].
- iSplitL; first done.
- iApply big_sepL2_intro; first done. iModIntro.
- iIntros (? r1 r2 ??). case_decide; first done.
- assert (r1 = r2) as -> by congruence. destruct bmin; done.
- (*iApply typed_place_cond_rfn_refl.*)
+ - iApply typed_place_cond_ty_array_lift; done.
+ - iApply typed_place_cond_rfn_array_lift; done.
- iPureIntro. apply place_access_rt_rel_refl.
Qed.
Global Instance typed_place_array_owned_inst π E L {rt rtv} (def : type rt) (lts : list (nat * ltype rt)) (len : nat) (rs : list (place_rfn rt)) wl bmin ly l it v (tyv : type rtv) (i : rtv) P :
@@ -1230,7 +1454,7 @@ Section rules.
⌜interpret_iml (◠def) len lts !! Z.to_nat i' = Some lt⌠-∗
⌜rs !! Z.to_nat i' = Some r⌠-∗
(* sidecondition for other components *)
- ⌜Forall (lctx_bor_kind_outlives E L1 bmin) (concat ((λ '(_, lt), ltype_blocked_lfts lt) <$> (lts)))⌠∗
+ ⌜Forall (lctx_bor_kind_outlives E L2 bmin) (concat ((λ '(_, lt), ltype_blocked_lfts lt) <$> (lts)))⌠∗
typed_place π E L2 (l offsetst{ty_syn_type def}ₗ i') lt r bmin (Owned false) P (λ L3 κs' li bi bmin2 rti ltyi ri strong weak,
T L3 (κs ++ κs') li bi bmin2 rti ltyi ri None
(fmap (λ weak, mk_weak
@@ -1240,39 +1464,175 @@ Section rules.
) weak)))))
⊢ typed_place π E L l (ArrayLtype def len lts) (#rs) bmin (Uniq κ γ) (BinOpPCtx (PtrOffsetOp ly) (IntOp it) v rtv tyv i :: P) T.
Proof.
- (* TODO *)
- Admitted.
+ rewrite /lctx_lft_alive_count_goal.
+ iIntros "(%i' & %Hst & HT)".
+ iIntros (????) "#CTX #HE HL #Hincl Hl Hcont".
+ simpl. iIntros "Hv".
+ iApply fupd_wp.
+ iMod ("HT" with "[] [] CTX HE HL Hv") as "(%L' & %R2 & >(Hi & R2) & HL & HT)"; [done.. | ].
+ iDestruct ("HT" with "R2") as "(% & % & HT)".
+ iDestruct "HT" as "(%κs & %L1 & %Hal & HT)".
+ iMod (fupd_mask_subseteq lftE) as "HclF"; first done.
+ iMod (lctx_lft_alive_count_tok with "HE HL") as "(%q & Htok & Hcltok & HL)"; [done.. | ].
+ iPoseProof (array_ltype_acc_uniq with "CTX Htok Hcltok Hl") as "(%ly' & %Hst' & %Hly & %Hsz & #Hlb & Hb)"; first done.
+ assert (ly' = ly) as -> by by eapply syn_type_has_layout_inj.
+ iMod "HclF" as "_".
+ iMod (fupd_mask_mono with "Hb") as "(Hb & Hcl)"; first done.
+ iEval (rewrite /ty_own_val/=) in "Hi".
+ iDestruct "Hi" as "(%Hi & %Hiz)".
+ iDestruct "CTX" as "(LFT & TIME & LLCTX)".
+ iApply (wp_logical_step with "TIME Hcl"); [done.. | ].
+ iApply wp_ptr_offset.
+ { eapply val_to_of_loc. }
+ { done. }
+ { rewrite /elem_of/int_elem_of_it. split; last nia.
+ specialize (min_int_le_0 isize_t). lia. }
+ { iPoseProof (loc_in_bounds_array_offset _ _ (Z.to_nat i') with "Hlb") as "Hlb'"; first lia.
+ rewrite Z2Nat.id; last done.
+ iApply loc_in_bounds_shorten_suf; last done. lia. }
+ { iApply loc_in_bounds_shorten_suf; last done. lia. }
+ iModIntro. iNext. iIntros "Hcred Hcl".
+ iModIntro. iExists _. iR.
+ iPoseProof (big_sepL2_length with "Hb") as "%Hlen_eq".
+ rewrite interpret_iml_length in Hlen_eq.
+ clear i. set (i := Z.to_nat i').
+ destruct (lookup_lt_is_Some_2 (interpret_iml (â— def) len lts)%I i) as (lti & Hlook_lti).
+ { rewrite interpret_iml_length. lia. }
+ destruct (lookup_lt_is_Some_2 rs i) as (ri & Hlook_ri).
+ { lia. }
+ iPoseProof ("HT" $! lti ri with "[//] [//]") as "(%Houtl & HT)".
+ iPoseProof (lctx_bor_kind_outlives_all_use with "[//] HE HL") as "#Houtl".
+ iPoseProof (big_sepL2_insert_acc with "Hb") as "((%Hsti & Hb) & Hcl_b)"; [done | done | ].
+ iPoseProof ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL") as "Hc".
+ rewrite /OffsetLocSt/use_layout_alg' Hst/=.
+ rewrite /offset_loc.
+ iApply ("Hc" with "[] [Hb]").
+ { destruct bmin; done. }
+ { subst i. rewrite Z2Nat.id//. }
+ iIntros (L2 κs' l2 b2 bmin0 rti ltyi ri' strong weak) "#Hincl1 Hi Hc".
+ iApply ("Hcont" with "[//] Hi").
+ iSplitR; first done. destruct weak as [ weak | ]; last done.
+ simpl. iIntros (ltyi2 ri2 bmin') "#Hincl2 Hi Hcond".
+ iDestruct "Hc" as "(_ & Hc)".
+ iMod ("Hc" with "[//] Hi Hcond") as "(Hi & #Hcond & Htoks & HR)".
+ iPoseProof (typed_place_cond_syn_type_eq with "Hcond") as "%Hsteq".
+ iPoseProof ("Hcl_b" with "[Hi]") as "Hb".
+ { rewrite /i Z2Nat.id; last done. iFrame. rewrite -Hsteq//. }
+ rewrite insert_interpret_iml.
+ iMod ("Hcl" with "[//] [] [] [] [] Hb") as "(Hb & ? & Hcondv)".
+ { rewrite insert_length //. }
+ { iApply "Hincl". }
+ { iApply typed_place_cond_ty_array_lift; [done.. | ].
+ iDestruct "Hcond" as "($ & _)". }
+ { iApply typed_place_cond_rfn_array_lift; first done.
+ iDestruct "Hcond" as "(_ & $)". }
+ { rewrite llft_elt_toks_app. iFrame.
+ iApply typed_place_cond_incl; last done.
+ iApply bor_kind_min_incl_r. }
+ Qed.
Global Instance typed_place_array_uniq_inst π E L {rt rtv} (def : type rt) (lts : list (nat * ltype rt)) (len : nat) (rs : list (place_rfn rt)) κ γ bmin ly l it v (tyv : type rtv) (i : rtv) P :
TypedPlace E L π l (ArrayLtype def len lts) (#rs) bmin (Uniq κ γ) (BinOpPCtx (PtrOffsetOp ly) (IntOp it) v rtv tyv i :: P) | 30 :=
λ T, i2p (typed_place_array_uniq π E L def lts len rs κ γ bmin ly l it v tyv i P T).
- (* TODO this is a problem, because we can only get strong below OpenedLtype etc.
-
- *)
+ (* TODO this is a problem, because we can only get strong below OpenedLtype etc. *)
Lemma typed_place_array_shared π E L {rt rtv} (def : type rt) (lts : list (nat * ltype rt)) (len : nat) (rs : list (place_rfn rt)) κ bmin ly l it v (tyv : type rtv) (i : rtv) P T :
(∃ i',
⌜syn_type_has_layout (ty_syn_type def) ly⌠∗
subsume_full E L false (v â—áµ¥{Ï€} i @ tyv) (v â—áµ¥{Ï€} i' @ int it) (λ L1 R2, R2 -∗
⌜(0 ≤ i')%Z⌠∗ ⌜(i' < len)%Z⌠∗
(* get lifetime token *)
- li_tactic (lctx_lft_alive_count_goal E L1 κ) (λ '(κs, L2),
+ (*li_tactic (lctx_lft_alive_count_goal E L1 κ) (λ '(κs, L2),*)
∀ lt r,
(* relies on Lithium's built-in simplification of lookups. *)
⌜interpret_iml (◠def) len lts !! Z.to_nat i' = Some lt⌠-∗
⌜rs !! Z.to_nat i' = Some r⌠-∗
(* sidecondition for other components *)
⌜Forall (lctx_bor_kind_outlives E L1 bmin) (concat ((λ '(_, lt), ltype_blocked_lfts lt) <$> (lts)))⌠∗
- typed_place π E L2 (l offsetst{ty_syn_type def}ₗ i') lt r bmin (Owned false) P (λ L3 κs' li bi bmin2 rti ltyi ri strong weak,
- T L3 (κs ++ κs') li bi bmin2 rti ltyi ri None
+ typed_place π E L1 (l offsetst{ty_syn_type def}ₗ i') lt r bmin (Shared κ) P (λ L3 κs' li bi bmin2 rti ltyi ri strong weak,
+ T L3 (κs') li bi bmin2 rti ltyi ri None
(fmap (λ weak, mk_weak
(λ lti2 ri2, ArrayLtype def len ((Z.to_nat i', weak.(weak_lt) lti2 ri2) :: lts))
(λ ri, #(<[Z.to_nat i' := weak.(weak_rfn) ri]> rs))
(weak.(weak_R))
- ) weak)))))
+ ) weak))))
⊢ typed_place π E L l (ArrayLtype def len lts) (#rs) bmin (Shared κ) (BinOpPCtx (PtrOffsetOp ly) (IntOp it) v rtv tyv i :: P) T.
Proof.
- (* TODO *)
- Admitted.
+ iIntros "(%i' & %Hst & HT)".
+ iIntros (????) "#CTX #HE HL #Hincl Hl Hcont".
+ simpl. iIntros "Hv".
+ iApply fupd_wp.
+ iMod ("HT" with "[] [] CTX HE HL Hv") as "(%L' & %R2 & >(Hi & R2) & HL & HT)"; [done.. | ].
+ iDestruct ("HT" with "R2") as "(% & % & HT)".
+ iMod (fupd_mask_subseteq F) as "HclF"; first done.
+ iPoseProof (array_ltype_acc_shared with "Hl") as "(%ly' & %Hst' & %Hly & %Hsz & #Hlb & >(Hb & Hcl))"; first done.
+ assert (ly' = ly) as -> by by eapply syn_type_has_layout_inj.
+ iMod "HclF" as "_".
+ iEval (rewrite /ty_own_val/=) in "Hi".
+ iDestruct "Hi" as "(%Hi & %Hiz)".
+ iDestruct "CTX" as "(LFT & TIME & LLCTX)".
+ iApply wp_fupd.
+ iApply wp_ptr_offset.
+ { eapply val_to_of_loc. }
+ { done. }
+ { rewrite /elem_of/int_elem_of_it. split; last nia.
+ specialize (min_int_le_0 isize_t). lia. }
+ { iPoseProof (loc_in_bounds_array_offset _ _ (Z.to_nat i') with "Hlb") as "Hlb'"; first lia.
+ rewrite Z2Nat.id; last done.
+ iApply loc_in_bounds_shorten_suf; last done. lia. }
+ { iApply loc_in_bounds_shorten_suf; last done. lia. }
+ iModIntro. iNext. iIntros "Hcred".
+ iModIntro. iExists _. iR.
+ iPoseProof (big_sepL2_length with "Hb") as "%Hlen_eq".
+ rewrite interpret_iml_length in Hlen_eq.
+ clear i. set (i := Z.to_nat i').
+ destruct (lookup_lt_is_Some_2 (interpret_iml (â— def) len lts)%I i) as (lti & Hlook_lti).
+ { rewrite interpret_iml_length. lia. }
+ destruct (lookup_lt_is_Some_2 rs i) as (ri & Hlook_ri).
+ { lia. }
+ iPoseProof ("HT" $! lti ri with "[//] [//]") as "(%Houtl & HT)".
+ iPoseProof (lctx_bor_kind_outlives_all_use with "[//] HE HL") as "#Houtl".
+ iPoseProof (big_sepL2_insert_acc with "Hb") as "((%Hsti & Hb) & Hcl_b)"; [done | done | ].
+ iPoseProof ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL") as "Hc".
+ rewrite /OffsetLocSt/use_layout_alg' Hst/=.
+ rewrite /offset_loc.
+ iApply ("Hc" with "[] [Hb]").
+ { destruct bmin; done. }
+ { subst i. rewrite Z2Nat.id//. }
+ iIntros (L2 κs l2 b2 bmin0 rti ltyi ri' strong weak) "#Hincl1 Hi Hc".
+ iApply ("Hcont" with "[//] Hi").
+ iSplitR; first done. destruct weak as [ weak | ]; last done.
+ simpl. iIntros (ltyi2 ri2 bmin') "#Hincl2 Hi Hcond".
+ iDestruct "Hc" as "(_ & Hc)".
+ iMod ("Hc" with "[//] Hi Hcond") as "(Hi & Hcond & Htoks & HR)".
+ iPoseProof (typed_place_cond_syn_type_eq with "Hcond") as "%Hsteq".
+ iPoseProof ("Hcl_b" with "[Hi]") as "Hb".
+ { rewrite /i Z2Nat.id; last done. iFrame. rewrite -Hsteq//. }
+ rewrite insert_interpret_iml.
+ iMod ("Hcl" with "[] [] Hb") as "(Hb & Hcondv)".
+ { done. }
+ { rewrite insert_length //. }
+ (*{ iPureIntro. rewrite Forall_cons. split; first lia. done. }*)
+ iFrame.
+ iModIntro.
+ iDestruct "Hcond" as "(Hcond & Hcond_rfn)".
+ iApply "Hcondv".
+ simpl.
+
+ rewrite -{1}(list_insert_id (interpret_iml _ _ _) i lti); last done.
+ rewrite (big_sepL2_insert _ _ _ _ _ (λ _ lt1 lt2, typed_place_cond_ty bmin lt1 lt2) 0); cycle 1.
+ { rewrite interpret_iml_length. lia. }
+ { rewrite interpret_iml_length. lia. }
+ iFrame. iApply big_sepL2_intro; first done.
+ iModIntro. iIntros (k lt1 lt2 Hlook ?). case_decide; first done.
+ assert (lt1 = lt2) as -> by congruence.
+ apply lookup_interpret_iml_Some_inv in Hlook as (? & [-> | Hel]).
+ { iApply typed_place_cond_ty_refl_ofty. }
+ apply elem_of_list_lookup_1 in Hel as (k' & Hlook).
+ iApply typed_place_cond_ty_refl.
+ iPoseProof (big_sepL_concat_lookup _ _ k' with "Houtl") as "Ha".
+ { rewrite list_lookup_fmap Hlook. done. }
+ done.
+ Qed.
Global Instance typed_place_array_shared_inst π E L {rt rtv} (def : type rt) (lts : list (nat * ltype rt)) (len : nat) (rs : list (place_rfn rt)) κ bmin ly l it v (tyv : type rtv) (i : rtv) P :
TypedPlace E L π l (ArrayLtype def len lts) (#rs) bmin (Shared κ) (BinOpPCtx (PtrOffsetOp ly) (IntOp it) v rtv tyv i :: P) | 30 :=
λ T, i2p (typed_place_array_shared π E L def lts len rs κ bmin ly l it v tyv i P T).
@@ -1498,6 +1858,27 @@ Section rules.
SubLtype E L k rs1 rs2 (ArrayLtype def1 len1 lts1) (ArrayLtype def2 len2 lts2) | 9 :=
λ T, i2p (weak_subltype_array_evar_lts E L def1 def2 len1 len2 lts1 lts2 rs1 rs2 k T).
+ Local Lemma weak_subltype_array_helper {rt1 rt2} (def1 : type rt1) (def2 : type rt2) len1 (lts1 : list (nat * ltype rt1)) (lts2 : list (nat * ltype rt2)) rs1 rs2 b1 :
+ length rs2 = len1 → length rs1 = len1 →
+ ([∗ list] i↦a;b ∈ interpret_iml (◠def1) len1 lts1; interpret_iml (◠def2) len1 lts2, ∃ (r1 : place_rfn rt1) (r2 : place_rfn rt2), ⌜rs1 !! i = Some r1⌠∗ ⌜rs2 !! i = Some r2⌠∗ ltype_incl b1 r1 r2 a b) -∗
+ [∗ list] lt1;lt2 ∈ zip (interpret_iml (◠def1) len1 lts1) rs1; zip (interpret_iml (◠def2) len1 lts2) rs2, ltype_incl b1 lt1.2 lt2.2 lt1.1 lt2.1.
+ Proof.
+ iIntros (??) "Ha".
+ iPoseProof (big_sepL2_to_zip with "Ha") as "Ha".
+ iPoseProof (big_sepL_extend_r (zip rs1 rs2) with "Ha") as "Ha".
+ { rewrite !zip_length !interpret_iml_length. lia. }
+ iApply big_sepL2_from_zip. { rewrite !zip_length !interpret_iml_length. lia. }
+ rewrite zip_assoc_l [zip rs1 (zip _ _)]zip_assoc_r [zip rs1 (interpret_iml _ _ _)]zip_flip.
+ rewrite !zip_fmap_l !zip_fmap_r. rewrite !zip_assoc_l !zip_fmap_r.
+ rewrite zip_assoc_r -!list_fmap_compose big_sepL_fmap.
+ iApply big_sepL2_to_zip'.
+ iApply (big_sepL2_impl with "Ha").
+ iModIntro. iIntros (k [lt1 lt2] [r1 r2] Hlook1 Hlook2); simpl.
+ iIntros "(%r1' & %r2' & %Hlook1' & %Hlook2' & Hincl)".
+ apply lookup_zip in Hlook2 as (Hlook21 & Hlook22).
+ assert (r1' = r1) as -> by naive_solver. assert (r2' = r2) as -> by naive_solver.
+ done.
+ Qed.
Lemma weak_subltype_array_owned_in E L {rt1 rt2} (def1 : type rt1) (def2 : type rt2) len1 len2 (lts1 : list (nat * ltype rt1)) (lts2 : list (nat * ltype rt2)) rs1 rs2 wl T :
(⌜len1 = len2⌠∗
∃ rs2', ⌜rs2 = #rs2'⌠∗
@@ -1512,8 +1893,9 @@ Section rules.
iApply array_ltype_incl_owned_in; first done.
simpl. iIntros (?). rewrite interpret_iml_length.
iSpecialize ("Ha" with "[] []"). { iPureIntro. lia. } {iPureIntro. lia. }
- iR.
- Admitted.
+ iR. setoid_rewrite Nat.add_0_r.
+ iApply weak_subltype_array_helper; done.
+ Qed.
Global Instance weak_subltype_array_owned_in_inst E L {rt1 rt2} (def1 : type rt1) (def2 : type rt2) len1 len2 (lts1 : list (nat * ltype rt1)) (lts2 : list (nat * ltype rt2)) rs1 rs2 wl :
SubLtype E L (Owned wl) #rs1 rs2 (ArrayLtype def1 len1 lts1) (ArrayLtype def2 len2 lts2) |10 :=
λ T, i2p (weak_subltype_array_owned_in E L def1 def2 len1 len2 lts1 lts2 rs1 rs2 wl T).
@@ -1549,8 +1931,9 @@ Section rules.
iApply array_ltype_incl_shared_in; first done.
simpl. iIntros (?). rewrite interpret_iml_length.
iSpecialize ("Ha" with "[] []"). { iPureIntro. lia. } {iPureIntro. lia. }
- iR.
- Admitted.
+ iR. setoid_rewrite Nat.add_0_r.
+ iApply weak_subltype_array_helper; done.
+ Qed.
Global Instance weak_subltype_array_shared_in_inst E L {rt1 rt2} (def1 : type rt1) (def2 : type rt2) len1 len2 (lts1 : list (nat * ltype rt1)) (lts2 : list (nat * ltype rt2)) rs1 rs2 κ :
SubLtype E L (Shared κ) #rs1 rs2 (ArrayLtype def1 len1 lts1) (ArrayLtype def2 len2 lts2) |10 :=
λ T, i2p (weak_subltype_array_shared_in E L def1 def2 len1 len2 lts1 lts2 rs1 rs2 κ T).
@@ -1788,6 +2171,7 @@ Section rules.
MutEqLtype E L (â— array_t def1 len1)%I (ArrayLtype def2 len2 lts2) | 14 :=
λ T, i2p (mut_eqltype_array_ofty_l E L def1 def2 len1 len2 lts2 T).
+
(** Owned subtype for initialization *)
Lemma owned_subtype_uninit_array π E L pers {rt} (ty : type rt) (st : syn_type) len r2 T :
li_tactic (compute_layout_goal st) (λ ly1,
@@ -1816,25 +2200,10 @@ Section rules.
done.
- simpl; done.
- iIntros (v) "Hun".
- iApply "Hv".
- rewrite /ty_own_val/=.
- iDestruct "Hun" as "(%ly0 & %Hly0 & %Hlyv0 & _)".
- assert (ly0 = ly1) as -> by by eapply syn_type_has_layout_inj.
- iExists _. iR.
- iSplitR. { iPureIntro. apply (use_layout_alg_size) in Hly0. lia. }
- rewrite replicate_length. iR.
- iSplitR. { rewrite /has_layout_val/mk_array_layout/ly_mult /= -Hszeq. done. }
- iApply big_sepL2_intro.
- { rewrite reshape_length !replicate_length//. }
- iModIntro. iIntros (k ?? Hlook1 Hlook2).
- apply lookup_replicate in Hlook1 as (-> & ?).
- iExists _. iR.
- rewrite uninit_own_spec.
- iExists _. iR.
- iPureIntro. rewrite /has_layout_val.
- apply elem_of_list_lookup_2 in Hlook2.
- apply reshape_replicate_elem_length in Hlook2; first done.
- rewrite Hlyv0. lia.
+ iApply "Hv". iApply array_val_from_uninit; last done.
+ + done.
+ + done.
+ + lia.
Qed.
Global Instance owned_subtype_uninit_array_inst π E L pers {rt} (ty : type rt) st len r2 :
OwnedSubtype π E L pers () r2 (uninit st) (array_t ty len) :=
@@ -2194,36 +2563,168 @@ End rules.
Section value.
Context `{!typeGS Σ}.
+
+ Lemma value_t_untyped_to_array' π v vs n ly ly' :
+ ly_size ly' = ly_size ly * n →
+ syn_type_has_layout (UntypedSynType ly) ly →
+ v â—áµ¥{Ï€} vs @ value_t (UntypedSynType ly') -∗
+ v â—áµ¥{Ï€} (fmap (M:=list) PlaceIn $ reshape (replicate n (ly_size ly)) vs) @ (array_t (value_t (UntypedSynType ly)) n).
+ Proof.
+ iIntros (Hsz ?) "Hv". rewrite /ty_own_val/=.
+ iDestruct "Hv" as "(%ot & %Hot & %Hmv & %Hv & %Hst)".
+ apply use_op_alg_untyped_inv in Hot as ->.
+ simpl in *.
+ apply is_memcast_val_untyped_inv in Hmv as <-.
+ apply (syn_type_has_layout_untyped_inv) in Hst as (_ & Hwf & Hsz' & Hal).
+ iExists ly.
+ iSplitR. { done. }
+ iSplitR. { iPureIntro. rewrite Hsz in Hsz'. lia. }
+ iSplitR. { rewrite fmap_length reshape_length replicate_length //. }
+ iSplitR. { rewrite /has_layout_val /mk_array_layout /ly_mult /= Hv Hsz. done. }
+ iApply big_sepL2_intro.
+ { rewrite fmap_length reshape_length !replicate_length//. }
+ iModIntro. iIntros (k ?? Hlook1 Hlook2).
+ rewrite list_lookup_fmap in Hlook1.
+ rewrite Hlook2 in Hlook1. simpl in Hlook1. injection Hlook1 as [= <-].
+ iExists _. iR.
+ iExists (UntypedOp ly).
+ simpl.
+ iSplitR. { iPureIntro. apply use_op_alg_untyped; done. }
+ iSplitR. { iPureIntro. by left. }
+ iSplitR. {
+ destruct (decide (ly_size ly = 0)) as [Hzero | ].
+ - (* size is 0 *)
+ rewrite Hzero reshape_replicate_0 in Hlook2.
+ apply lookup_replicate_1 in Hlook2 as (-> & ?).
+ rewrite /has_layout_val Hzero //.
+ - rewrite sublist_lookup_reshape in Hlook2.
+ { rewrite sublist_lookup_Some' in Hlook2. destruct Hlook2 as (-> & ?).
+ iPureIntro. rewrite /has_layout_val take_length drop_length. lia. }
+ { lia. }
+ { rewrite Hv. lia. }
+ }
+ iPureIntro. done.
+ Qed.
Lemma value_t_untyped_to_array π v vs n ly :
+ syn_type_has_layout (UntypedSynType ly) ly →
v â—áµ¥{Ï€} vs @ value_t (UntypedSynType (mk_array_layout ly n)) -∗
v â—áµ¥{Ï€} (fmap (M:=list) PlaceIn $ reshape (replicate n (ly_size ly)) vs) @ (array_t (value_t (UntypedSynType ly)) n).
Proof.
- Admitted.
+ iIntros (?) "Hv".
+ iApply (value_t_untyped_to_array' with "Hv").
+ - done.
+ - done.
+ Qed.
+
+ Lemma value_t_untyped_from_array' π v vs (vs' : list val) vs'' n ly ly' :
+ ly' = mk_array_layout ly n →
+ vs = fmap PlaceIn vs' →
+ vs'' = (mjoin vs') →
+ v â—áµ¥{Ï€} vs @ (array_t (value_t (UntypedSynType ly)) n) -∗
+ v â—áµ¥{Ï€} vs'' @ value_t (UntypedSynType ly').
+ Proof.
+ iIntros (-> -> ->) "Hv".
+ rewrite /ty_own_val/=.
+ iDestruct "Hv" as "(%ly'' & %Hst & %Hsz & <- & %Hv & Hl)".
+ apply syn_type_has_layout_untyped_inv in Hst as (-> & Hwf & Hsz' & Hal).
+ rewrite fmap_length. rewrite fmap_length in Hv.
+ iExists (UntypedOp (mk_array_layout ly (length vs'))).
+ iSplitR. { iPureIntro. apply use_op_alg_untyped; done. }
+
+ rewrite big_sepL2_fmap_l.
+ (* have: agreement between the values *)
+ iSplitL. {
+ iAssert ([∗ list] x1; x2 ∈ vs'; (reshape (replicate (length vs') (ly_size ly)) v), ⌜x1 = x2⌠∗ ⌜x1 `has_layout_val` lyâŒ)%I with "[Hl]" as "Hl".
+ { iApply (big_sepL2_impl with "Hl"). iModIntro.
+ iIntros (? v1 v2 _ _) "(%v3 & -> & Ha)".
+ rewrite {1}/ty_own_val/=.
+ iDestruct "Ha" as "(%ot & %Hot & %Hv1 & ? & ?)".
+ apply use_op_alg_untyped_inv in Hot as ->.
+ apply is_memcast_val_untyped_inv in Hv1 as ->.
+ simpl. iFrame. done. }
+ rewrite big_sepL2_sep. iDestruct "Hl" as "(Hl1 & Hl)".
+ iPoseProof (big_sepL2_Forall2 with "Hl1") as "%Hl1".
+ apply Forall2_eq in Hl1 as ->.
+ iClear "Hl1". rewrite big_sepL2_elim_r.
+ rewrite reshape_length replicate_length.
+ rewrite join_reshape.
+ - iPureIntro. left. done.
+ - rewrite sum_list_replicate Hv ly_size_mk_array_layout.
+ lia. }
+ iSplitR. { iPureIntro. rewrite /has_layout_val Hv /= //. }
+ iPureIntro.
+ apply syn_type_has_layout_untyped.
+ - done.
+ - by apply array_layout_wf.
+ - rewrite ly_size_mk_array_layout.
+ move: Hsz. rewrite fmap_length. lia.
+ - rewrite /ly_align_in_bounds ly_align_mk_array_layout //.
+ Qed.
Lemma value_t_untyped_from_array π v vs n ly :
+ length vs = n * ly_size ly →
v â—áµ¥{Ï€} (fmap (M:=list) PlaceIn $ reshape (replicate n (ly_size ly)) vs) @ (array_t (value_t (UntypedSynType ly)) n) -∗
v â—áµ¥{Ï€} vs @ value_t (UntypedSynType (mk_array_layout ly n)).
Proof.
- Admitted.
+ iIntros (?) "Hv". iApply value_t_untyped_from_array'; last done.
+ - done.
+ - done.
+ - rewrite join_reshape; first done.
+ rewrite sum_list_replicate. lia.
+ Qed.
Lemma ofty_value_t_untyped_to_array π l vs ly n :
+ syn_type_has_layout (UntypedSynType ly) ly →
(l â—â‚—[Ï€, Owned false] #vs @ â— value_t (UntypedSynType (mk_array_layout ly n)))%I -∗
l â—â‚—[Ï€, Owned false] #(fmap (M:=list) PlaceIn $ reshape (replicate n (ly_size ly)) vs) @ â— (array_t (value_t (UntypedSynType ly)) n).
Proof.
- Admitted.
+ iIntros (?) "Ha".
+ iPoseProof (ltype_own_has_layout with "Ha") as "(%ly' & %Hst & %Hly)".
+ simp_ltypes in Hst. simpl in Hst.
+ apply syn_type_has_layout_untyped_inv in Hst as (-> & Hwf & Hsz & Hal).
+ iApply (ofty_mono_ly_strong_in with "[] [] Ha").
+ - simpl. apply syn_type_has_layout_untyped; done.
+ - simpl. apply (syn_type_has_layout_array _ _ ly); first done; first last.
+ { move: Hsz. rewrite ly_size_mk_array_layout. lia. }
+ done.
+ - done.
+ - done.
+ - iIntros (v) "Ha".
+ iApply value_t_untyped_to_array; first done. done.
+ - simpl. eauto.
+ Qed.
+ Lemma ofty_value_t_untyped_from_array' π l (vs : list (place_rfn val)) (vs' : list val) (vs'' : val) ly ly' n :
+ ly' = mk_array_layout ly n →
+ vs = fmap PlaceIn vs' →
+ vs'' = (mjoin vs') →
+ (l â—â‚—[Ï€, Owned false] #vs @ â— (array_t (value_t (UntypedSynType ly)) n))%I -∗
+ (l â—â‚—[Ï€, Owned false] #vs'' @ â— value_t (UntypedSynType ly'))%I.
+ Proof.
+ iIntros (???) "Ha".
+ iPoseProof (ltype_own_has_layout with "Ha") as "(%ly1 & %Hst & %Hly)".
+ simp_ltypes in Hst. simpl in Hst.
+ specialize (syn_type_has_layout_array_inv _ _ _ Hst) as (ly2 & Hst' & -> & Hsz).
+ specialize (syn_type_has_layout_untyped_inv _ _ Hst') as (-> & ? & ? & ?).
+ iApply (ofty_mono_ly_strong_in with "[] [] Ha").
+ - simpl. apply (syn_type_has_layout_array _ _ ly); [done.. | ].
+ move: Hsz. rewrite ly_size_mk_array_layout. lia.
+ - simpl. subst ly'. eapply syn_type_has_layout_make_untyped; done.
+ - done.
+ - subst ly'. done.
+ - iIntros (v) "Ha".
+ iApply value_t_untyped_from_array'; done.
+ - simpl. eauto.
+ Qed.
Lemma ofty_value_t_untyped_from_array π l vs ly n :
+ length vs = n * ly_size ly →
(l â—â‚—[Ï€, Owned false] #(fmap (M:=list) PlaceIn $ reshape (replicate n (ly_size ly)) vs) @ â— (array_t (value_t (UntypedSynType ly)) n))%I -∗
(l â—â‚—[Ï€, Owned false] #vs @ â— value_t (UntypedSynType (mk_array_layout ly n)))%I.
Proof.
- Admitted.
+ iIntros (?) "Hv". iApply ofty_value_t_untyped_from_array'; last done.
+ - done.
+ - done.
+ - rewrite join_reshape; first done. rewrite sum_list_replicate. lia.
+ Qed.
- Lemma ofty_value_t_has_length F π l v st ly :
- lftE ⊆ F →
- syn_type_has_layout st ly →
- l â—â‚—[Ï€, Owned false] #v @ (â— value_t st)%I ={F}=∗
- ⌜length v = ly_size ly⌠∗ l â—â‚—[Ï€, Owned false] #v @ (â— value_t st)%I.
- Proof.
- iIntros (? Hst) "Hl".
- Admitted.
End value.
diff --git a/theories/rust_typing/box.v b/theories/rust_typing/box.v
index f255832ab8bc24128ae5adf020abfc197e9d22df..d49ded54fec8aa639113118e6db96b8205d4f127 100644
--- a/theories/rust_typing/box.v
+++ b/theories/rust_typing/box.v
@@ -321,7 +321,7 @@ Section unfold.
Proof.
iModIntro. iIntros (Ï€ l).
rewrite ltype_own_box_unfold /box_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
- iIntros "(%ly & Halg & Hly & Hlb & Hcred & Hat & Hrfn & Hb)". iExists ly.
+ iIntros "(%ly & Halg & Hly & Hlb & (Hcred & Hat) & Hrfn & Hb)". iExists ly.
iFrame "∗". iMod "Hb". iModIntro.
setoid_rewrite ltype_own_core_equiv. simp_ltypes.
iApply (pinned_bor_iff' with "[] Hb").
@@ -350,7 +350,7 @@ Section unfold.
Proof.
iModIntro. iIntros (Ï€ l).
rewrite ltype_own_box_unfold /box_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
- iIntros "(%ly & Halg & Hly & Hsc & Hlb & Hcred & Hat & Hrfn & Hb)".
+ iIntros "(%ly & Halg & Hly & Hsc & Hlb & (Hcred & Hat) & Hrfn & Hb)".
iExists ly. iFrame. iMod "Hb". iModIntro.
(* same proof as above *)
setoid_rewrite ltype_own_core_equiv. simp_ltypes.
@@ -506,7 +506,7 @@ Section rules.
.
Proof.
iIntros (?) "#(LFT & TIME & LLCTX) Hκ HR Hb". rewrite ltype_own_box_unfold /box_ltype_own.
- iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hlb & Hcred & Hat & Hrfn & Hb)".
+ iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hlb & (Hcred & Hat) & Hrfn & Hb)".
injection Halg as <-. iFrame "#%".
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
iMod "Hb".
@@ -602,27 +602,38 @@ Section rules.
lftE ⊆ F →
rrust_ctx -∗
q.[κ] -∗
- l â—â‚—[Ï€, Shared κ] r @ BoxLtype lt -∗
+ l â—â‚—[Ï€, Shared κ] #r @ BoxLtype lt -∗
⌜l `has_layout_loc` void*⌠∗ loc_in_bounds l 0 (ly_size void*) ∗ |={F}=>
- ∃ (l' : loc) r' q, place_rfn_interp_shared r r' ∗ l ↦{q} l' ∗ (|={F}â–·=> l' â—â‚—[Ï€, Shared κ] r' @ lt) ∗
- (∀ lt',
- l ↦{q} l' -∗
- l' â—â‚—[Ï€, Shared κ] r @ lt' -∗
- l â—â‚—[Ï€, Shared κ] PlaceIn r' @ BoxLtype lt ∗
+ ∃ (l' : loc) q', l ↦{q'} l' ∗ (|={F}â–·=> l' â—â‚—[Ï€, Shared κ] r @ lt) ∗
+ (∀ (lt' : ltype rt) r',
+ l ↦{q'} l' -∗
+ l' â—â‚—[Ï€, Shared κ] r' @ lt' -∗ |={F}=>
+ l â—â‚—[Ï€, Shared κ] #r' @ BoxLtype lt' ∗
q.[κ] ∗
- (∀ bmin,
+ (∀ bmin,
bmin ⊑ₖ Shared κ -∗
- typed_place_cond bmin lt lt r' r' ={F}=∗
- typed_place_cond bmin (BoxLtype lt) (BoxLtype lt) (#r') (#r'))).
+ typed_place_cond bmin lt lt' r r' ={F}=∗
+ typed_place_cond bmin (BoxLtype lt) (BoxLtype lt') #r #r')).
Proof.
- iIntros (?) "#CTX Hκ Hb". rewrite {1}ltype_own_box_unfold /box_ltype_own.
- iDestruct "Hb" as "(%ly & %Hst & %Hly & #Hlb & %r' & Hrfn & #Hb)".
+ iIntros (?) "#(LFT & TIME & LLCTX) Hκ Hb". rewrite {1}ltype_own_box_unfold /box_ltype_own.
+ iDestruct "Hb" as "(%ly & %Hst & %Hly & #Hlb & %r' & -> & #Hb)".
apply syn_type_has_layout_ptr_inv in Hst. subst ly.
iR. iR.
- iMod (fupd_mask_mono with "Hb") as "(%li & Hf & Hl)"; first done.
-
- (* TODO *)
- Abort.
+ iMod (fupd_mask_mono with "Hb") as "(%li & #Hf & #Hl)"; first done.
+ iMod (frac_bor_acc with "LFT Hf Hκ") as "(%q' & >Hpts & Hclf)"; first done.
+ iModIntro. iExists _, _. iFrame.
+ iSplitR. { iApply step_fupd_intro; first done. auto. }
+ iIntros (lt' r'') "Hpts #Hl'".
+ iMod ("Hclf" with "Hpts") as "Htok".
+ iFrame. iSplitL.
+ { iModIntro. rewrite ltype_own_box_unfold /box_ltype_own. iExists void*. iFrame "% #".
+ iR. iExists _. iR. iModIntro. iModIntro. iExists _. iFrame "#". }
+ iModIntro. iIntros (bmin) "Hincl Hcond".
+ iDestruct "Hcond" as "(Hcond_ty & Hcond_rfn)".
+ iModIntro. iSplit.
+ + iApply box_ltype_place_cond_ty; done.
+ + destruct bmin; done.
+ Qed.
(** Place access *)
(* Needs to have lower priority than the id instance *)
@@ -745,20 +756,55 @@ Section rules.
Global Instance typed_place_box_uniq_inst {rto} π E L (lt2 : ltype rto) bmin0 r l κ' γ' P :
TypedPlace E L π l (BoxLtype lt2) (PlaceIn r) bmin0 (Uniq κ' γ') (DerefPCtx Na1Ord PtrOp true :: P) | 30 := λ T, i2p (typed_place_box_uniq π E L lt2 P l r κ' γ' bmin0 T).
- (*
- Lemma typed_place_box_shared {rto} π E L (lt2 : ltype rto) P l r κ' bmin0
- (T : llctx → list lft → loc → bor_kind → bor_kind → ∀ rti, ltype rti → place_rfn rti → (ltype rti → ltype ((place_rfn rto))) → (place_rfn rti → place_rfn ((place_rfn rto))) → (ltype rti → place_rfn rti → iProp Σ) → iProp Σ) :
+ Lemma typed_place_box_shared {rto} π E L (lt2 : ltype rto) P l r κ' bmin0 (T : place_cont_t (place_rfn rto)) :
li_tactic (lctx_lft_alive_count_goal E L κ') (λ '(κs, L'),
- (∀ l', typed_place π E L' l' lt2 r (bmin0) (Owned true) P
- (λ L'' κs' l2 b2 bmin rti tyli ri (tylp : ltype rti → ltype rto) (rctx : place_rfn rti → place_rfn rto) R,
- T L'' (κs ++ κs') l2 b2 (Shared κ' ⊓ₖ bmin) rti tyli ri (BoxLtype ∘ tylp) (λ (r : place_rfn rti), PlaceIn (rctx r)) R))) -∗
- typed_place π E L l (BoxLtype lt2) (PlaceIn r) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp :: P) T.
+ (∀ l', typed_place π E L' l' lt2 r (bmin0) (Shared κ') P
+ (λ L'' κs' l2 b2 bmin rti tyli ri strong weak,
+ T L'' (κs ++ κs') l2 b2 (Shared κ' ⊓ₖ bmin) rti tyli ri
+ (* strong branch: fold to ShadowedLtype *)
+ (* TODO *)
+ None
+ (* weak branch: just keep the Box *)
+ (fmap (λ weak, mk_weak (λ lti2 ri2, BoxLtype (weak.(weak_lt) lti2 ri2)) (λ (r : place_rfn rti), PlaceIn (weak.(weak_rfn) r)) weak.(weak_R)) weak))))
+ ⊢ typed_place π E L l (BoxLtype lt2) (PlaceIn r) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp true :: P) T.
Proof.
- (* TODO *)
- Admitted.
+ rewrite /lctx_lft_alive_count_goal.
+ iIntros "(%κs & %L2 & %Hal & HT)".
+ iIntros (Φ F ??). iIntros "#(LFT & TIME & LLCTX) #HE HL #Hincl0 HP HΦ/=".
+ (* get a token *)
+ iApply fupd_wp. iMod (fupd_mask_subseteq lftE) as "HclF"; first done.
+ iMod (lctx_lft_alive_count_tok lftE with "HE HL") as (q) "(Hκ' & Hclκ' & HL)"; [done.. | ].
+ iMod "HclF" as "_". iMod (fupd_mask_subseteq F) as "HclF"; first done.
+ iPoseProof (box_ltype_acc_shared F with "[$LFT $TIME $LLCTX] Hκ' HP") as "(%Hly & Hlb & Hb)"; [done.. | ].
+ iMod "Hb" as "(%l' & %q' & Hl & Hb & Hcl)". iMod "Hb".
+ iMod "HclF" as "_".
+ iModIntro.
+ iApply wp_fupd.
+ iApply (wp_deref with "Hl") => //; [solve_ndisj | by apply val_to_of_loc | ].
+ iNext.
+ iIntros (st) "Hl Hcred".
+ iExists l'. iMod (fupd_mask_mono with "Hb") as "Hb"; first done.
+ iSplitR. { iPureIntro. unfold mem_cast. rewrite val_to_of_loc. done. }
+ iApply ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL [] Hb"). { destruct bmin0; done. }
+ iModIntro. iIntros (L'' κs' l2 b2 bmin rti tyli ri strong weak) "#Hincl1 Hb Hs".
+ iApply ("HΦ" $! _ _ _ _ (Shared κ' ⊓ₖ bmin) _ _ _ _ _ with "[Hincl1] Hb").
+ { iApply bor_kind_incl_trans; last iApply "Hincl1". iApply bor_kind_min_incl_r. }
+ simpl. iSplit.
+ - (* strong update *)
+ done.
+ - (* weak update *)
+ destruct weak as [ weak | ]; last done.
+ iDestruct "Hs" as "(_ & Hs)".
+ iIntros (ltyi2 ri2 bmin') "#Hincl2 Hl2 Hcond".
+ iMod ("Hs" with "[Hincl2] Hl2 Hcond") as "(Hb & Hcond & ? & HR)".
+ { iApply bor_kind_incl_trans; first iApply "Hincl2". iApply bor_kind_min_incl_r. }
+ iMod ("Hcl" with "Hl Hb") as "(Hb & Hκ' & Hcond')".
+ iMod (fupd_mask_mono with "(Hclκ' Hκ')") as "?"; first done.
+ rewrite llft_elt_toks_app. iFrame.
+ cbn. iApply "Hcond'"; last done. done.
+ Qed.
Global Instance typed_place_box_shared_inst {rto} π E L (lt2 : ltype rto) bmin0 r l κ' P :
- TypedPlace E L π l (BoxLtype lt2) (PlaceIn r) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp :: P) | 30 := λ T, i2p (typed_place_box_shared π E L lt2 P l r κ' bmin0 T).
- *)
+ TypedPlace E L π l (BoxLtype lt2) (#r) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp true :: P) | 30 := λ T, i2p (typed_place_box_shared π E L lt2 P l r κ' bmin0 T).
Lemma stratify_ltype_box_Owned {rt} `{Inhabited rt} π E L mu mdu ma {M} (ml : M) l (lt : ltype rt) (r : (place_rfn rt)) wl
@@ -858,7 +904,16 @@ Section rules.
end)
⊢ resolve_ghost π E L rm lb l (BoxLtype lt) (Owned wl) (PlaceGhost γ) T.
Proof.
- Admitted.
+ iIntros "Ha" (???) "#CTX #HE HL Hl".
+ iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+ - rewrite ltype_own_box_unfold /box_ltype_own.
+ iDestruct "Hl" as "(%ly & ? & ? & ? & ? & % & Hinterp & ?)".
+ simpl. iPoseProof (gvar_pobs_agree_2 with "Hinterp HObs") as "#<-".
+ iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+ iL. rewrite ltype_own_box_unfold /box_ltype_own.
+ iExists _. iFrame. iExists _. iR. by iFrame.
+ - iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro. by iFrame.
+ Qed.
Global Instance resolve_ghost_box_owned_inst {rt} π E L l (lt : ltype rt) γ wl rm lb :
ResolveGhost π E L rm lb l (BoxLtype lt) (Owned wl) (PlaceGhost γ) | 7 := λ T, i2p (resolve_ghost_box_Owned π E L l lt γ wl rm lb T).
@@ -870,10 +925,41 @@ Section rules.
end)
⊢ resolve_ghost π E L rm lb l (BoxLtype lt) (Uniq κ γ') (PlaceGhost γ) T.
Proof.
- Admitted.
+ iIntros "Ha" (???) "#CTX #HE HL Hl".
+ iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+ - rewrite ltype_own_box_unfold /box_ltype_own.
+ iDestruct "Hl" as "(%ly & ? & ? & ? & ? & Hinterp & ?)".
+ simpl.
+ iPoseProof (Rel2_use_pobs with "HObs Hinterp") as "(%r2 & Hobs & ->)".
+ iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+ iL. rewrite ltype_own_box_unfold /box_ltype_own.
+ iExists _. iFrame. done.
+ - iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro. by iFrame.
+ Qed.
Global Instance resolve_ghost_box_uniq_inst {rt} π E L l (lt : ltype rt) γ κ γ' rm lb :
ResolveGhost π E L rm lb l (BoxLtype lt) (Uniq κ γ') (PlaceGhost γ) | 7 := λ T, i2p (resolve_ghost_box_Uniq π E L l lt γ rm lb κ γ' T).
+ Lemma resolve_ghost_box_shared {rt} π E L l (lt : ltype rt) γ rm lb κ T :
+ find_observation (place_rfn rt) γ FindObsModeDirect (λ or,
+ match or with
+ | None => ⌜rm = ResolveTry⌠∗ T L (PlaceGhost γ) True false
+ | Some r => T L (#r) True true
+ end)
+ ⊢ resolve_ghost π E L rm lb l (BoxLtype lt) (Shared κ) (PlaceGhost γ) T.
+ Proof.
+ iIntros "Ha" (???) "#CTX #HE HL Hl".
+ iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+ - rewrite ltype_own_box_unfold /box_ltype_own.
+ iDestruct "Hl" as "(%ly & ? & ? & ? & % & Hinterp & ?)".
+ simpl. iPoseProof (gvar_pobs_agree_2 with "Hinterp HObs") as "#<-".
+ iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+ iL. rewrite ltype_own_box_unfold /box_ltype_own.
+ iExists _. iFrame. iExists _. iR. by iFrame.
+ - iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro. by iFrame.
+ Qed.
+ Global Instance resolve_ghost_box_shared_inst {rt} π E L l (lt : ltype rt) γ κ rm lb :
+ ResolveGhost π E L rm lb l (BoxLtype lt) (Shared κ) (PlaceGhost γ) | 7 := λ T, i2p (resolve_ghost_box_shared π E L l lt γ rm lb κ T).
+
(** cast_ltype *)
Lemma cast_ltype_to_type_box E L {rt} `{Inhabited rt} (lt : ltype rt) T :
cast_ltype_to_type E L lt (λ ty, T (box ty))
diff --git a/theories/rust_typing/existentials.v b/theories/rust_typing/existentials.v
index d1f586b3d0977180b14263e3e54461e417859ffb..0350d07c1ad3bfba535e60a003ee42d97ccec188 100644
--- a/theories/rust_typing/existentials.v
+++ b/theories/rust_typing/existentials.v
@@ -281,7 +281,7 @@ Section open.
Can we generalize? *)
iIntros (?) "#(LFT & TIME & LLCTX) Htok Hcl_tok Hb".
rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & Hcred & Hat & Hrfn & Hb)".
+ iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & (Hcred & Hat) & Hrfn & Hb)".
iMod (fupd_mask_mono with "Hb") as "Hb"; first done.
iDestruct "Hcred" as "(Hcred1 & Hcred)".
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
diff --git a/theories/rust_typing/gvar_refinement.v b/theories/rust_typing/gvar_refinement.v
index 4dac3c9080ddadda258572deea2ef6ec19147a6d..a12d12911456bbf2f7eb3a40ec04df72289ddaf2 100644
--- a/theories/rust_typing/gvar_refinement.v
+++ b/theories/rust_typing/gvar_refinement.v
@@ -155,7 +155,7 @@ End sigma.
Potentially, that even works as a general abstraction in the gvar interface.
*)
Section ghost_variables.
- Context `{ghost_varG Σ RT} {T : Type}.
+ Context `{!ghost_varG Σ RT} {T : Type}.
Implicit Types (γ : gname) (t : T).
Definition gvar_auth γ t := ghost_var γ (DfracOwn (1/2)) (RT_into t).
@@ -235,6 +235,8 @@ Section ghost_variables.
Global Instance Rel2_timeless γ1 γ2 R : Timeless (Rel2 γ1 γ2 R).
Proof. apply _. Qed.
-
- (* TODO: define Rel, etc. *)
End ghost_variables.
+
+Lemma gvar_update_strong `{!ghost_varG Σ RT} {T1 T2 : Type} {γ} {t1 t2 : T1} (t : T2) :
+ gvar_auth γ t1 -∗ gvar_obs γ t2 ==∗ gvar_auth γ t ∗ gvar_obs γ t.
+Proof. iApply ghost_var_update_halves. Qed.
diff --git a/theories/rust_typing/lft_contexts.v b/theories/rust_typing/lft_contexts.v
index add8113bead66533756b35e48cd6df58c30ff219..b70232caae044b091a3b3613415f248c07a19d26 100644
--- a/theories/rust_typing/lft_contexts.v
+++ b/theories/rust_typing/lft_contexts.v
@@ -529,6 +529,18 @@ Section lft_contexts.
by iApply "Hincl".
Qed.
+ Lemma big_sepL_lft_incl_incl κs κ :
+ elctx_interp E -∗ llctx_interp L -∗
+ ([∗ list] κ' ∈ κs, ⌜lctx_lft_incl κ' κâŒ) -∗
+ ([∗ list] κ' ∈ κs, κ' ⊑ κ).
+ Proof.
+ iIntros "#HE HL #Hincl".
+ iInduction κs as [ | κ' κs] "IH"; first done.
+ simpl. iDestruct "Hincl" as "(%Hincl & Hincl)".
+ iPoseProof (lctx_lft_incl_incl with "HL HE") as "#$"; first apply Hincl.
+ iApply ("IH" with "Hincl HL").
+ Qed.
+
(* Lifetime aliveness *)
Definition lctx_lft_alive (κ : lft) : Prop :=
(* the proof must not use any information about the counts *)
@@ -1254,6 +1266,20 @@ Section lft_contexts.
Proof.
iIntros (Hel) "Hall". iApply (big_sepL_elem_of with "Hall"). done.
Qed.
+
+ Lemma lft_dead_list_nil :
+ lft_dead_list [] ⊣⊢ True.
+ Proof. done. Qed.
+ Lemma lft_dead_list_cons κ κs :
+ lft_dead_list (κ :: κs) ⊣⊢ [†κ] ∗ lft_dead_list κs.
+ Proof. done. Qed.
+ Lemma lft_dead_list_app κs1 κs2 :
+ lft_dead_list (κs1 ++ κs2) ⊣⊢ lft_dead_list κs1 ∗ lft_dead_list κs2.
+ Proof.
+ induction κs1 as [ | κ κs1 IH]; simpl.
+ { rewrite lft_dead_list_nil left_id. eauto. }
+ rewrite lft_dead_list_cons IH. rewrite bi.sep_assoc //.
+ Qed.
End lft_contexts.
Arguments lft_dead_list : simpl never.
diff --git a/theories/rust_typing/ltype_rules.v b/theories/rust_typing/ltype_rules.v
index abad0ae6605ad295e2d6ce83c5907fa526929887..714a58bc7451f1038acd2ead35fc4736dfe4312d 100644
--- a/theories/rust_typing/ltype_rules.v
+++ b/theories/rust_typing/ltype_rules.v
@@ -20,7 +20,7 @@ Proof.
by iApply ty_shr_mono.
+ rewrite /lty_of_ty_own.
iDestruct "Hincl" as "(Hincl & ->)".
- iIntros "(%ly & Hst & Hly & Hsc & Hlb & Hcred & Hat & Hrfn & Hb)". iExists ly. iFrame.
+ iIntros "(%ly & Hst & Hly & Hsc & Hlb & Hcred & Hrfn & Hb)". iExists ly. iFrame.
iMod "Hb". iModIntro. iApply pinned_bor_shorten; done.
Qed.
Local Lemma alias_mono `{!typeGS Σ} rt st p b1 b2 π r l :
@@ -49,7 +49,7 @@ Proof.
iApply lft_intersect_mono; last done. iApply lft_incl_refl.
+ iDestruct "Hincl" as "(Hincl & ->)".
rewrite !ltype_own_mut_ref_unfold /mut_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame. iMod "Hb". by iApply pinned_bor_shorten.
Qed.
Local Lemma shrltype_mono `{!typeGS Σ} {rt} (lt : ltype rt) π κ :
@@ -68,7 +68,7 @@ Proof.
done.
+ iDestruct "Hincl" as "(Hincl & ->)".
rewrite !ltype_own_shr_ref_unfold /shr_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame. iMod "Hb". by iApply pinned_bor_shorten.
Qed.
Local Lemma box_ltype_mono `{!typeGS Σ} {rt} (lt : ltype rt) π :
@@ -87,7 +87,7 @@ Proof.
iNext. iApply IH; last done. done.
+ iDestruct "Hincl" as "(Hincl & ->)".
rewrite !ltype_own_box_unfold /box_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame. iMod "Hb". by iApply pinned_bor_shorten.
Qed.
Local Lemma owned_ptr_ltype_mono `{!typeGS Σ} {rt} (lt : ltype rt) (ls : bool) π :
@@ -106,7 +106,7 @@ Proof.
iNext. iApply IH; last done. done.
+ iDestruct "Hincl" as "(Hincl & ->)".
rewrite !ltype_own_owned_ptr_unfold /owned_ptr_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame. iMod "Hb". by iApply pinned_bor_shorten.
Qed.
Local Lemma struct_ltype_mono `{!typeGS Σ} {rts} (lts : hlist ltype rts) sls π :
@@ -134,7 +134,7 @@ Proof.
rewrite /UninitLtype !ltype_own_ofty_unfold. by iApply (lty_of_ty_mono with "[] Hb").
+ iDestruct "Hincl" as "(Hincl & ->)".
rewrite !ltype_own_struct_unfold /struct_ltype_own.
- iIntros "(%sl & ? & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%sl & ? & ? & ? & ? & ? & ? & Hb)".
iExists sl. iFrame. iMod "Hb".
by iApply pinned_bor_shorten.
Qed.
@@ -155,7 +155,7 @@ Proof.
by eapply elem_of_list_lookup_2.
+ rewrite !ltype_own_array_unfold /array_ltype_own.
iDestruct "Hincl" as "(Hincl & ->)".
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro. iApply pinned_bor_shorten; done.
Qed.
@@ -478,7 +478,7 @@ Section subtype.
Proof.
iIntros "#Heq". iModIntro.
iIntros (Ï€ l). rewrite !ltype_own_owned_ptr_unfold /owned_ptr_ltype_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & Hobs & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & Hobs & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro.
iApply (pinned_bor_iff with "[] [] Hb").
@@ -774,13 +774,13 @@ Section accessors.
l â—â‚—[Ï€, Uniq κ γ] #(r2) @ OpenedLtype (â—ty2) (â—ty) (â—ty) (λ r1 r1', ⌜r1 = r1'âŒ) (λ _ _, R))).
Proof.
iIntros (?) "#(LFT & TIME & LLCTX) Htok HclR Hb". rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & Hcred & Hat & Hobs & Hb)".
+ iDestruct "Hb" as "(%ly & %Halg & %Hly & #Hsc & #Hlb & Hcred & Hobs & Hb)".
iExists ly. iFrame "%#".
iMod (fupd_mask_subseteq lftE) as "HF_cl"; first done.
iMod "Hb" as "Hb".
iMod (pinned_bor_acc_strong lftE with "LFT Hb Htok") as "(%κ' & #Hinclκ & Hb & Hvcl & Hcl)"; first done.
iMod "HF_cl" as "_".
- iDestruct "Hcred" as "[Hcred1 Hcred]".
+ iDestruct "Hcred" as "([Hcred1 Hcred] & Hat)".
iApply (lc_fupd_add_later with "Hcred1"); iNext.
iDestruct "Hb" as "(%r' & Hauth & Hb)".
iMod (fupd_mask_mono lftE with "Hb") as "(%v & Hl & Hv)"; first done.
@@ -918,7 +918,7 @@ Section open.
Proof.
iIntros (? κ γ π r l q κs ?) "#(LFT & TIME & LLCTX) Htok Hcl_tok Hb".
rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly & % & % & #? & #? & (Hcred1 & Hcred) & Hat & Hrfn & Hb)".
+ iDestruct "Hb" as "(%ly & % & % & #? & #? & ((Hcred1 & Hcred) & Hat) & Hrfn & Hb)".
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
iMod "Hb".
iMod (pinned_bor_acc_strong lftE with "LFT Hb Htok") as "(%κ' & #Hincl & Hb & ? & Hcl_b)"; first done.
diff --git a/theories/rust_typing/ltypes.v b/theories/rust_typing/ltypes.v
index e525d1e8851ea99913d6e8eae84982c80ca00f24..a47832f7b043830c6e5559416d3d281e22fc5c2a 100644
--- a/theories/rust_typing/ltypes.v
+++ b/theories/rust_typing/ltypes.v
@@ -407,6 +407,18 @@ Proof.
iApply (Hincl with "HL HE").
Qed.
+Lemma lctx_bor_kind_incl_use E L b1 b2 :
+ lctx_bor_kind_incl E L b1 b2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ b1 ⊑ₖ b2.
+Proof.
+ iIntros (Hincl) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ by iPoseProof (Hincl with "HL HE") as "Ha".
+Qed.
+
+
(** Outliving *)
Definition bor_kind_outlives (b : bor_kind) (κ : lft) : iProp Σ :=
match b with
@@ -481,6 +493,17 @@ Qed.
Definition lctx_bor_kind_direct_incl (E : elctx) (L : llctx) b b' : Prop :=
∀ qL, llctx_interp_noend L qL -∗ □ (elctx_interp E -∗ b ⊑ₛₖ b').
+Lemma lctx_bor_kind_direct_incl_use E L b1 b2 :
+ lctx_bor_kind_direct_incl E L b1 b2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ b1 ⊑ₛₖ b2.
+Proof.
+ iIntros (Hincl) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ by iPoseProof (Hincl with "HL HE") as "Ha".
+Qed.
+
End ltype.
Infix "⊑ₖ" := bor_kind_incl (at level 70) : bi_scope.
@@ -1095,6 +1118,7 @@ Section ltype_def.
Definition UninitLty st := OfTyLty (uninit st).
Definition maybe_creds (wl : bool) := (if wl then £ num_cred ∗ atime 1 else True)%I.
+ Definition have_creds : iProp Σ := £ num_cred ∗ atime 1.
Definition lty_of_ty_own {rt} (ty : type rt) k π (r : place_rfn rt) l :=
(∃ ly : layout, ⌜syn_type_has_layout ty.(ty_syn_type) ly⌠∗ ⌜l `has_layout_loc` ly⌠∗
@@ -1108,7 +1132,7 @@ Section ltype_def.
As such, this is really needed for contractiveness/making working with rec types possible. *)
▷?(wl)|={lftE}=> ∃ v, l ↦ v ∗ ty.(ty_own_val) π r' v
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
(* Note: need an update inside the borrow over the recursive thing to get the unfolding equation for products
(as products need an update there)
@@ -1245,7 +1269,7 @@ Section ltype_def.
freeable_nz l' ly'.(ly_size) 1 HeapAlloc ∗
lty_own_pre core lt (Owned true) π r' l'
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
(* TODO can we remove the update here? *)
|={lftE}=> &pin{κ}
@@ -1291,7 +1315,7 @@ Section ltype_def.
⌜l' `has_layout_loc` ly'⌠∗
lty_own_pre core lt (Owned ls) π r' l'
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
|={lftE}=> &pin{κ}
[∃ (r' : place_rfn (lty_rt lt)) (l' : loc),
@@ -1335,7 +1359,7 @@ Section ltype_def.
(* TODO layout requirements on l' here? *)
▷?wl |={lftE}=> ∃ l' : loc , l ↦ l' ∗ (lty_own_pre core lt (Uniq κ γ) π r' l')
| Uniq κ' γ' =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ' ∗
|={lftE}=> &pin{κ'}
[∃ (r' : (place_rfn (lty_rt lt)) * gname),
@@ -1371,7 +1395,7 @@ Section ltype_def.
▷?wl |={lftE}=> ∃ (l' : loc), l ↦ l' ∗
lty_own_pre core lt (Shared κ) π r' l'
| Uniq κ' γ' =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ' ∗
|={lftE}=> &pin{κ'}(∃ (r' : place_rfn (lty_rt lt)), gvar_auth γ' r' ∗
|={lftE}=> ∃ (l' : loc), l ↦ l' ∗ lty_own_pre core lt (Shared κ) π r' l')
@@ -1403,7 +1427,7 @@ Section ltype_def.
∃ ly, ⌜snd <$> sl.(sl_members) !! i = Some ly⌠∗ ⌜syn_type_has_layout (lty_st (projT1 ty)) ly⌠∗
lty_own_pre core (projT1 ty) (Owned false) π (projT2 ty) (l +ₗ Z.of_nat (offset_of_idx sl.(sl_members) i)))
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
(* We change the ownership to Owned false, because we can't push the borrow down in this formulation of products.
The cost of this is that we need an update here (to get congruence rules for ltype_eq),
@@ -1453,7 +1477,7 @@ Section ltype_def.
⌜lty_st ty.1 = ty_syn_type def⌠∗
lty_own_pre core ty.1 (Owned false) π (rew <-Heq in ty.2) (offset_loc l ly i))
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
|={lftE}=> &pin{κ}
[∃ r' : list (place_rfn rt), gvar_auth γ r' ∗ ⌜length r' = len⌠∗ |={lftE}=>
@@ -1897,7 +1921,7 @@ Section ltype_def.
do 2 f_equiv.
all: setoid_rewrite big_sepL_P_eq.
all: simpl.
- 3: do 3 f_equiv;
+ 3: do 2 f_equiv;
[move : r; simpl; rewrite <-Heq; done | do 2 f_equiv].
1: f_equiv.
all: iSplit.
@@ -2084,7 +2108,7 @@ Section ltype_def.
do 2 f_equiv.
all: simpl.
all: setoid_rewrite big_sepL_P_eq.
- 3: do 3 f_equiv;
+ 3: do 2 f_equiv;
[move : r; rewrite <-Heq; done | do 2 f_equiv].
1: f_equiv.
all: iSplit.
@@ -2620,7 +2644,7 @@ Section ltype_def.
freeable_nz l' ly'.(ly_size) 1 HeapAlloc ∗
rec _ lt (Owned true) π r' l'
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
(* TODO can we remove the update here? *)
|={lftE}=> &pin{κ}
@@ -2668,7 +2692,7 @@ Section ltype_def.
⌜l' `has_layout_loc` ly'⌠∗
rec _ lt (Owned ls) π r' l'
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
|={lftE}=> &pin{κ}
[∃ (r' : place_rfn rt) (l' : loc),
@@ -2710,7 +2734,7 @@ Section ltype_def.
▷?wl|={lftE}=> ∃ (l' : loc), l ↦ l' ∗
rec _ lt (Shared κ) π r' l'
| Uniq κ' γ' =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ' ∗
|={lftE}=> &pin{κ'}(∃ (r' : place_rfn rt), gvar_auth γ' r' ∗ |={lftE}=> ∃ (l' : loc), l ↦ l' ∗ rec _ lt (Shared κ) π r' l')
| Shared κ' =>
@@ -2740,7 +2764,7 @@ Section ltype_def.
(* TODO layout requirements on l' here? *)
▷?wl|={lftE}=> ∃ l' : loc , l ↦ l' ∗ (rec _ lt (Uniq κ γ) π r' l')
| Uniq κ' γ' =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ' ∗
|={lftE}=> &pin{κ'}
[∃ (r' : (place_rfn rt) * gname),
@@ -2787,7 +2811,7 @@ Section ltype_def.
∃ ly, ⌜snd <$> sl.(sl_members) !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
rec _ (projT2 ty).1 (Owned false) π (projT2 ty).2 (l +ₗ Z.of_nat (offset_of_idx sl.(sl_members) i))
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
(* We change the ownership to Owned false, because we can't push the borrow down in this formulation of products.
The cost of this is that we need an update here (to get congruence rules for ltype_eq),
@@ -2834,7 +2858,7 @@ Section ltype_def.
[∗ list] i ↦ lt; r0 ∈ (interpret_iml (OfTy def) len lts); r',
⌜ltype_st lt = ty_syn_type def⌠∗ rec _ lt (Owned false) π r0 (offset_loc l ly i)
| Uniq κ γ =>
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
place_rfn_interp_mut r γ ∗
|={lftE}=> &pin{κ}
[∃ r' : list (place_rfn rt), gvar_auth γ r' ∗ ⌜length r' = len⌠∗ |={lftE}=>
@@ -3350,7 +3374,7 @@ Section ltype_def.
do 2 f_equiv. rewrite big_sepL_P_eq.
rewrite -OfTy_ltype_lty interpret_iml_fmap ArrayLtype_big_sepL_fmap //.
rewrite interpret_iml_length//.
- - do 7 f_equiv. all: f_equiv; first done.
+ - do 6 f_equiv. all: f_equiv; first done.
all: apply sep_equiv_proper => Hlen.
all: repeat f_equiv; rewrite big_sepL_P_eq.
all: rewrite -OfTy_ltype_lty interpret_iml_fmap ArrayLtype_big_sepL_fmap//.
@@ -4141,17 +4165,17 @@ Section ltype_def.
intros ? Hdeinit.
induction lt using lty_induction; simpl; try done.
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & ? & ? & Hcred & ? & $ & Hl)".
+ by iIntros "(%ly & %Halg & %Hly & ? & ? & Hcred & $ & Hl)".
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & Hlb & Hcred & ? & $ & Hb)".
+ by iIntros "(%ly & %Halg & %Hly & Hlb & Hcred & $ & Hb)".
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & $ & Hb)".
+ by iIntros "(%ly & %Halg & %Hly & ? & Hcred & $ & Hb)".
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & $ & Hb)".
+ by iIntros "(%ly & %Halg & %Hly & ? & Hcred & $ & Hb)".
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & $ & Hb)".
+ by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & $ & Hb)".
- rewrite /lty_own. simp lty_own_pre.
- by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & $ & Hb)".
+ by iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & $ & Hb)".
- rewrite /lty_own. simp lty_own_pre.
iDestruct 1 as "(%el & %rty & ? & ? & ? & ? & ? & [])".
- rewrite /lty_own. simp lty_own_pre.
@@ -4216,25 +4240,25 @@ Section ltype_def.
iIntros "(%ly & %Halg & %Hly & ? & Hlb & (%r' & -> & Hobs & Hb))". injection Hdeinit as <-.
iModIntro. iIntros (??). simpl. by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
- iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & Hr & Hb)".
+ iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & Hr & Hb)".
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre.
- iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & Hb)". injection Hdeinit as <-.
+ iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & Hb)". injection Hdeinit as <-.
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre.
- iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & Hb)". injection Hdeinit as <-.
+ iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & Hb)". injection Hdeinit as <-.
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
- iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & ? & Hb)".
+ iIntros "(%ly & %Halg & %Hly & ? & Hcred & ? & Hb)".
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
- iIntros "(%ly & %Halg & ? & ? & ? & ? & ? & _)".
+ iIntros "(%ly & %Halg & ? & ? & ? & ? & _)".
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
- iIntros "(%ly & %Halg & ? & ? & ? & ? & ? & ? & _)".
+ iIntros "(%ly & %Halg & ? & ? & ? & ? & ? & _)".
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
- iIntros "(%ly & %Halg & ? & ? & ? & ? & ? & ? & _)".
+ iIntros "(%ly & %Halg & ? & ? & ? & ? & ? & _)".
iModIntro. iIntros (??). by iFrame.
- rewrite /lty_own. simp lty_own_pre. injection Hdeinit as <-.
iIntros "(%el & %rty & ? & ? & ? & ? & ? & [])".
@@ -4417,6 +4441,201 @@ Definition full_subltype `{!typeGS Σ} (E : elctx) (L : llctx) {rt} (lt1 : ltype
#[export]
Instance: Params (@full_subltype) 5 := {}.
+Lemma ltype_incl'_use `{!typeGS Σ} {rt1 rt2} F (lt1 : ltype rt1) (lt2 : ltype rt2) l π b r1 r2 :
+ lftE ⊆ F →
+ ltype_incl' b r1 r2 lt1 lt2 -∗
+ l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗
+ l â—â‚—[Ï€, b] r2 @ lt2.
+Proof.
+ iIntros (?) "#Hincl Hl".
+ iMod (fupd_mask_subseteq lftE) as "Hcl"; first done.
+ destruct b.
+ - iMod ("Hincl" with "Hl") as "$". by iMod "Hcl".
+ - iMod "Hcl". iModIntro. by iApply "Hincl".
+ - iMod "Hcl". iModIntro. by iApply "Hincl".
+Qed.
+Lemma ltype_incl_use `{!typeGS Σ} {rt1 rt2} π F b r1 r2 l (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ lftE ⊆ F →
+ ltype_incl b r1 r2 lt1 lt2 -∗
+ l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2.
+Proof.
+ iIntros (?) "Hincl Ha".
+ iDestruct "Hincl" as "(_ & #Hincl & _)".
+ destruct b.
+ - iApply (fupd_mask_mono with "(Hincl Ha)"); done.
+ - by iApply "Hincl".
+ - by iApply "Hincl".
+Qed.
+Lemma ltype_incl_use_core `{!typeGS Σ} {rt1 rt2} π F b r1 r2 l (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ lftE ⊆ F →
+ ltype_incl b r1 r2 lt1 lt2 -∗
+ l â—â‚—[Ï€, b] r1 @ ltype_core lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ ltype_core lt2.
+Proof.
+ iIntros (?) "Hincl Ha".
+ iDestruct "Hincl" as "(_ & _ & #Hincl)".
+ destruct b.
+ - iApply (fupd_mask_mono with "(Hincl Ha)"); done.
+ - by iApply "Hincl".
+ - by iApply "Hincl".
+Qed.
+
+
+Section accessors.
+ Context `{!typeGS Σ}.
+ Lemma subltype_use {rt1 rt2} F E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ lftE ⊆ F →
+ subltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ â–¡ ∀ Ï€ l, l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2.
+ Proof.
+ iIntros (? Hsubt) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
+ iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
+ iModIntro. iIntros (Ï€ l). iApply ltype_incl_use; done.
+ Qed.
+ Lemma subltype_use_core {rt1 rt2} F E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ lftE ⊆ F →
+ subltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ â–¡ ∀ Ï€ l, l â—â‚—[Ï€, b] r1 @ ltype_core lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ ltype_core lt2.
+ Proof.
+ iIntros (? Hsubt) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
+ iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
+ iModIntro. iIntros (Ï€ l). iApply ltype_incl_use_core; done.
+ Qed.
+
+ Lemma subltype_acc {rt1 rt2} E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ subltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ltype_incl b r1 r2 lt1 lt2.
+ Proof.
+ iIntros (Hsubt) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
+ iPoseProof (Hsubt with "HL CTX HE") as "#Hincl". done.
+ Qed.
+ Lemma full_subltype_acc E L {rt} (lt1 lt2 : ltype rt) :
+ full_subltype E L lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ∀ b r, ltype_incl b r r lt1 lt2.
+ Proof.
+ iIntros (Hsubt) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
+ iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
+ iIntros (b r). iApply "Hincl".
+ Qed.
+
+ Lemma eqltype_use_noend F E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) qL l π :
+ lftE ⊆ F →
+ eqltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp_noend L qL -∗
+ (l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2) ∗
+ llctx_interp_noend L qL.
+ Proof.
+ iIntros (? Hunfold) "#CTX #HE HL".
+ iPoseProof (Hunfold with "HL CTX HE") as "#Hll". iFrame.
+ iIntros "Hl".
+ iDestruct "Hll" as "((_ & #Ha & _) & _)".
+ destruct b.
+ - iMod (fupd_mask_subseteq lftE) as "Hcl"; first solve_ndisj.
+ iMod ("Ha" with "Hl") as "$". by iMod "Hcl" as "_".
+ - by iApply "Ha".
+ - by iApply "Ha".
+ Qed.
+ Lemma eqltype_use F E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) l π :
+ lftE ⊆ F →
+ eqltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ (l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2) ∗
+ llctx_interp L.
+ Proof.
+ iIntros (? Hunfold) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ iPoseProof (eqltype_use_noend with "CTX HE HL") as "($ & HL)"; [done.. | ].
+ by iApply "HL_cl".
+ Qed.
+ Lemma eqltype_acc E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ eqltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ltype_eq b r1 r2 lt1 lt2.
+ Proof.
+ iIntros (Heq) "CTX HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ iApply (Heq with "HL CTX HE").
+ Qed.
+ Lemma full_eqltype_acc E L {rt} (lt1 lt2 : ltype rt) :
+ full_eqltype E L lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ∀ b r, ltype_eq b r r lt1 lt2.
+ Proof.
+ iIntros (Heq) "CTX HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ iApply (Heq with "HL CTX HE").
+ Qed.
+
+ Lemma all_ltype_eq_alt {rt} b (lt1 lt2 : ltype rt) :
+ (∀ r, ltype_eq b r r lt1 lt2) ⊣⊢ (∀ r, ltype_incl b r r lt1 lt2) ∧ (∀ r, ltype_incl b r r lt2 lt1).
+ Proof.
+ iSplit.
+ - iIntros "#Ha". iSplit; iIntros (r); iSpecialize ("Ha" $! r); iDestruct "Ha" as "[Ha Hb]"; done.
+ - iIntros "#[Ha Hb]". iIntros (r). iSplit; done.
+ Qed.
+ Lemma full_eqltype_use F π E L {rt} b r (lt1 lt2 : ltype rt) l :
+ lftE ⊆ F →
+ full_eqltype E L lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ (l â—â‚—[ Ï€, b] r @ lt1 ={F}=∗ l â—â‚—[ Ï€, b] r @ lt2) ∗
+ llctx_interp L.
+ Proof.
+ iIntros (? Heq) "#CTX #HE HL".
+ iPoseProof (full_eqltype_acc with "CTX HE HL") as "#Heq"; [done | ].
+ iFrame. iIntros "Hl". iDestruct ("Heq" $! _ _) as "[Hincl _]".
+ by iApply (ltype_incl_use with "Hincl Hl").
+ Qed.
+
+ Lemma eqltype_syn_type_eq_noend E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) qL :
+ eqltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp_noend L qL -∗
+ ⌜ltype_st lt1 = ltype_st lt2âŒ.
+ Proof.
+ iIntros (Hunfold) "#CTX #HE HL".
+ iPoseProof (Hunfold with "HL CTX HE") as "#Hll".
+ iDestruct "Hll" as "((#$ & _) & _)".
+ Qed.
+ Lemma eqltype_syn_type_eq E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
+ eqltype E L b r1 r2 lt1 lt2 →
+ rrust_ctx -∗
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ⌜ltype_st lt1 = ltype_st lt2âŒ.
+ Proof.
+ iIntros (Hunfold) "#CTX #HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
+ iPoseProof (eqltype_syn_type_eq_noend with "CTX HE HL") as "#$".
+ done.
+ Qed.
+End accessors.
+
Section eqltype.
Context `{!typeGS Σ}.
@@ -4711,7 +4930,7 @@ Section eqltype.
simpl. simp_ltypes. rewrite -bi.persistent_sep_dup.
iModIntro. iIntros (Ï€ l) "Hb".
rewrite !ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly & Hst & ? & Hsc & Hlb & ? & ? & Hrfn & Hb)".
+ iDestruct "Hb" as "(%ly & Hst & ? & Hsc & Hlb & ? & Hrfn & Hb)".
iExists ly. iFrame. rewrite Hst. iFrame.
iSplitL "Hsc"; first by iApply "Hsceq".
@@ -4912,7 +5131,7 @@ Section blocked.
- iIntros (κ0 γ' π r l) "#Hdead Hb".
rewrite ltype_own_core_equiv /=. simp_ltypes.
rewrite !ltype_own_mut_ref_unfold /mut_ltype_own.
- iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro. iModIntro.
(*rewrite ltype_core_syn_type_eq.*)
@@ -4943,7 +5162,7 @@ Section blocked.
- iIntros (κ0 γ' π r l) "#Hdead Hb".
rewrite ltype_own_core_equiv /=. simp_ltypes.
rewrite !ltype_own_shr_ref_unfold /shr_ltype_own.
- iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro. iModIntro.
(*rewrite ltype_core_syn_type_eq.*)
@@ -4978,7 +5197,7 @@ Section blocked.
- iIntros (κ' γ' π r l) "#Hdead Hb".
rewrite ltype_own_core_equiv /=. simp_ltypes.
rewrite !ltype_own_box_unfold /box_ltype_own.
- iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iDestruct "Hb" as "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro. rewrite ltype_core_syn_type_eq.
setoid_rewrite ltype_own_core_core.
@@ -5071,21 +5290,6 @@ Section blocked.
rewrite -ltype_own_core_equiv. iApply ("Ha2" with "Hdead Hb").
Qed.
- (* TODO: move *)
- Lemma lft_dead_list_nil :
- lft_dead_list [] ⊣⊢ True.
- Proof. done. Qed.
- Lemma lft_dead_list_cons κ κs :
- lft_dead_list (κ :: κs) ⊣⊢ [†κ] ∗ lft_dead_list κs.
- Proof. done. Qed.
- Lemma lft_dead_list_app κs1 κs2 :
- lft_dead_list (κs1 ++ κs2) ⊣⊢ lft_dead_list κs1 ∗ lft_dead_list κs2.
- Proof.
- induction κs1 as [ | κ κs1 IH]; simpl.
- { rewrite lft_dead_list_nil left_id. eauto. }
- rewrite lft_dead_list_cons IH. rewrite bi.sep_assoc //.
- Qed.
-
(** Once all the blocked lifetimes are dead, every ltype is unblockable to its core. *)
Lemma imp_unblockable_blocked_dead {rt} (lt : ltype rt) :
⊢ imp_unblockable (ltype_blocked_lfts lt) lt.
@@ -5167,22 +5371,30 @@ Section blocked.
iApply ofty_imp_unblockable.
Qed.
+ Lemma imp_unblockable_use π F κs {rt} (lt : ltype rt) (r : place_rfn rt) l bk :
+ lftE ⊆ F →
+ imp_unblockable κs lt -∗
+ lft_dead_list κs -∗
+ l â—â‚—[Ï€, bk] r @ lt ={F}=∗ l â—â‚—[Ï€, bk] r @ ltype_core lt.
+ Proof.
+ iIntros (?) "(#Hub_uniq & #Hub_owned) Hdead Hl".
+ destruct bk.
+ - iMod (fupd_mask_mono with "(Hub_owned Hdead Hl)") as "Hl"; first done.
+ rewrite ltype_own_core_equiv. done.
+ - iApply (ltype_own_shared_to_core with "Hl").
+ - iMod (fupd_mask_mono with "(Hub_uniq Hdead Hl)") as "Hl"; first done.
+ rewrite ltype_own_core_equiv. done.
+ Qed.
+
Lemma unblock_blocked {rt} E κ π l b (ty : type rt) r :
lftE ⊆ E →
[†κ] -∗
l â—â‚—[Ï€, b] r @ (BlockedLtype ty κ) ={E}=∗ l â—â‚—[Ï€, b] r @ (â— ty)%I.
Proof.
iIntros (?) "Hdead Hl".
- iPoseProof (blocked_imp_unblockable ty κ) as "#(Ha1 & Ha2)".
- destruct b.
- - iMod (fupd_mask_subseteq lftE) as "Hcl"; first done.
- iMod ("Ha2" with "[$Hdead //] Hl") as "Hl".
- rewrite ltype_own_core_equiv. simp_ltypes. iMod "Hcl". simpl. done.
- - rewrite ltype_own_blocked_unfold /blocked_lty_own.
- iDestruct "Hl" as "(% & _ & _ & _ & _ & [])".
- - iPoseProof ("Ha1" with "[$Hdead //] Hl") as "Hl".
- rewrite ltype_own_core_equiv. simp_ltypes.
- iApply (fupd_mask_mono with "Hl"). done.
+ iPoseProof (blocked_imp_unblockable ty κ) as "Ha".
+ iMod (imp_unblockable_use with "Ha [$Hdead//] Hl") as "Hb"; first done.
+ simp_ltypes. done.
Qed.
Lemma unblock_shrblocked {rt} E κ π l b (ty : type rt) r :
lftE ⊆ E →
@@ -5190,16 +5402,9 @@ Section blocked.
l â—â‚—[Ï€, b] r @ (ShrBlockedLtype ty κ) ={E}=∗ l â—â‚—[Ï€, b] r @ (â— ty)%I.
Proof.
iIntros (?) "Hdead Hl".
- iPoseProof (shr_blocked_imp_unblockable ty κ) as "#(Ha1 & Ha2)".
- destruct b.
- - iMod (fupd_mask_subseteq lftE) as "Hcl"; first done.
- iMod ("Ha2" with "[$Hdead //] Hl") as "Hl".
- rewrite ltype_own_core_equiv. simp_ltypes. iMod "Hcl". simpl. done.
- - rewrite ltype_own_shrblocked_unfold /shr_blocked_lty_own.
- iDestruct "Hl" as "(% & _ & _ & _ & _ & % & _ & [])".
- - iPoseProof ("Ha1" with "[$Hdead //] Hl") as "Hl".
- rewrite ltype_own_core_equiv. simp_ltypes.
- iApply (fupd_mask_mono with "Hl"). done.
+ iPoseProof (shr_blocked_imp_unblockable ty κ) as "Ha".
+ iMod (imp_unblockable_use with "Ha [$Hdead//] Hl") as "Hb"; first done.
+ simp_ltypes. done.
Qed.
Lemma unblock_coreable {rt} F π (lt_full : ltype rt) r κs l b :
lftE ⊆ F →
@@ -5207,15 +5412,9 @@ Section blocked.
l â—â‚—[Ï€, b] r @ CoreableLtype κs lt_full ={F}=∗
l â—â‚—[Ï€, b] r @ ltype_core lt_full.
Proof.
- iIntros (?) "#Hdead Hl".
- rewrite ltype_own_coreable_unfold /coreable_ltype_own.
- iDestruct "Hl" as "(%ly & %Halg & %Hly & #Hlb & Hl)".
- destruct b.
- - iMod (fupd_mask_mono with "(Hl Hdead)") as "Hb"; first done.
- rewrite ltype_own_core_equiv. done.
- - rewrite ltype_own_core_equiv. done.
- - iDestruct "Hl" as "(Hrfn & Hl)".
- iMod (fupd_mask_mono with "(Hl Hdead Hrfn)") as "Hb"; first done.
- rewrite ltype_own_core_equiv. done.
+ iIntros (?) "Hdead Hl".
+ iPoseProof (coreable_ltype_imp_unblockable lt_full κs) as "Ha".
+ iMod (imp_unblockable_use with "Ha [$Hdead//] Hl") as "Hb"; first done.
+ simp_ltypes. done.
Qed.
End blocked.
diff --git a/theories/rust_typing/memcasts.v b/theories/rust_typing/memcasts.v
index 3718f54433d87f63723f47203163977cda1873a7..f1fdbc1e0ca4bb7fa48cfc9f53e88f6299794feb 100644
--- a/theories/rust_typing/memcasts.v
+++ b/theories/rust_typing/memcasts.v
@@ -169,6 +169,22 @@ Proof.
rewrite /has_layout_val mem_cast_length //.
Qed.
+Lemma is_memcast_val_has_layout_val v v' ot ly :
+ is_memcast_val v ot v' →
+ v `has_layout_val` ly →
+ v' `has_layout_val` ly.
+Proof.
+ intros [-> | (st & ->)] Hb; first done.
+ by apply has_layout_val_mem_cast.
+Qed.
+Lemma is_memcast_val_length v v' ot :
+ is_memcast_val v ot v' →
+ length v = length v'.
+Proof.
+ intros [-> | (st & ->)]; first done.
+ rewrite mem_cast_length//.
+Qed.
+
(* Q:
does the syntactical type alone determine the memcast_compat_type?
diff --git a/theories/rust_typing/products.v b/theories/rust_typing/products.v
index a7f896072b1b034777a67299106768f0ce9814bf..0902d7621c323ec4d9e845c66b63e0a52ce30670 100644
--- a/theories/rust_typing/products.v
+++ b/theories/rust_typing/products.v
@@ -124,36 +124,6 @@ Global Hint Unfold unit_t : tyunfold.
Section structs.
Context `{!typeGS Σ}.
- (* TODO move *)
- Lemma big_sepL_extend_l {A B} (l' : list B) (l : list A) Φ :
- length l' = length l →
- ([∗ list] i ↦ x ∈ l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ y; x ∈ l'; l, Φ i x).
- Proof.
- iIntros (?) "Ha". iApply big_sepL2_const_sepL_r. iFrame. done.
- Qed.
- Lemma big_sepL_extend_r {A B} (l' : list B) (l : list A) Φ :
- length l' = length l →
- ([∗ list] i ↦ x ∈ l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x; y ∈ l; l', Φ i x).
- Proof.
- iIntros (?) "Ha". iApply big_sepL2_const_sepL_l. iFrame. done.
- Qed.
- Lemma big_sepL2_elim_l {A B} (l' : list B) (l : list A) Φ :
- ([∗ list] i ↦ y; x ∈ l'; l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x ∈ l, Φ i x).
- Proof.
- iIntros "Ha". rewrite big_sepL2_const_sepL_r. iDestruct "Ha" as "(_ & $)".
- Qed.
- Lemma big_sepL2_elim_r {A B} (l' : list B) (l : list A) Φ :
- ([∗ list] i ↦ x; y ∈ l; l', Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x ∈ l, Φ i x).
- Proof.
- iIntros "Ha". rewrite big_sepL2_const_sepL_l. iDestruct "Ha" as "(_ & $)".
- Qed.
- Lemma big_sepL2_sep_1 {A B} (l1 : list A) (l2 : list B) Φ Ψ :
- ⊢@{iProp Σ}
- ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
- ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2) -∗
- ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2).
- Proof. iIntros "Ha Hb". iApply big_sepL2_sep. iFrame. Qed.
-
Polymorphic Definition zip_to_rtype (rt : list Type) (tys : hlist type rt) :=
(fmap (λ x, mk_rtype (projT2 x)) (hzipl rt tys)).
@@ -552,7 +522,7 @@ Section structs.
end. done.
+ unfold struct_make_uninit_type in *.
match goal with | H : existT _ _ = existT _ _ |- _ => rename H into Heq end.
- injection Heq => Heq1 Heq2 ?. subst.
+ injection Heq => Heq1 Heq2 ?. subst.
apply existT_inj in Heq1. apply existT_inj in Heq2. subst.
iSplitR; first done. iSplitR; first done.
iExists _; iPureIntro. split; first done.
@@ -1628,7 +1598,7 @@ Section subltype.
iModIntro.
iIntros (Ï€ l).
rewrite !ltype_own_struct_unfold /struct_ltype_own.
- iIntros "(%sl & %Halg & %Hlen & %Hly & Hlb & ? & ? & Hrfn & Hb)".
+ iIntros "(%sl & %Halg & %Hlen & %Hly & Hlb & ? & Hrfn & Hb)".
iExists sl. iSplitR; first done. iSplitR; first done.
iSplitR; first done. iFrame.
iMod "Hb". iModIntro. iApply (pinned_bor_iff with "[] [] Hb").
@@ -1778,13 +1748,13 @@ Section unfold.
assert (sl' = sl) as ->. { by eapply struct_layout_spec_has_layout_inj. }
rewrite hpzipl_hmap.
set (f := (λ '(existT x (a, b)), existT x (◠a, b))%I).
- rewrite (pad_struct_ext _ _ _ (λ ly, f (existT (unit : Type) (uninit (UntypedSynType ly), PlaceIn ())))); last done.
+ rewrite (pad_struct_ext _ _ _ (λ ly, f (struct_make_uninit_type ly))); last done.
rewrite pad_struct_fmap big_sepL_fmap.
rewrite /struct_own_el_val heap_mapsto_reshape_sl; last done.
iDestruct "Hl" as "(_ & Hl)".
iPoseProof (big_sepL2_sep_sepL_l with "[$Hl $Hb]") as "Ha".
- iAssert ([∗ list] k↦ _;y ∈ reshape (ly_size <$> (sl_members sl).*2) v; pad_struct (sl_members sl) (hpzipl rts tys r') (λ ly : layout, existT (unit : Type) (uninit (UntypedSynType ly), PlaceIn ())), |={lftE}=> ∃ ly : layout, ⌜snd <$> sl_members sl !! k = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 (f y)).1) ly⌠∗ ltype_own (projT2 (f y)).1 (Owned false) π (projT2 (f y)).2 (l +ₗ offset_of_idx (sl_members sl) k))%I with "[-]" as "Hs"; first last.
+ iAssert ([∗ list] k↦ _;y ∈ reshape (ly_size <$> (sl_members sl).*2) v; pad_struct (sl_members sl) (hpzipl rts tys r') struct_make_uninit_type, |={lftE}=> ∃ ly : layout, ⌜snd <$> sl_members sl !! k = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 (f y)).1) ly⌠∗ ltype_own (projT2 (f y)).1 (Owned false) π (projT2 (f y)).2 (l +ₗ offset_of_idx (sl_members sl) k))%I with "[-]" as "Hs"; first last.
{ rewrite big_sepL2_const_sepL_r. rewrite big_sepL_fupd. iDestruct "Hs" as "[_ $]". }
iApply (big_sepL2_wand with "Ha").
@@ -1818,7 +1788,7 @@ Section unfold.
rewrite hpzipl_hmap.
set (f := (λ '(existT x (a, b)), existT x (◠a, b))%I).
- rewrite (pad_struct_ext _ _ _ (λ ly, f (existT (unit : Type) (uninit (UntypedSynType ly), PlaceIn ())))); last done.
+ rewrite (pad_struct_ext _ _ _ (λ ly, f $ struct_make_uninit_type ly)); last done.
rewrite pad_struct_fmap big_sepL_fmap.
iModIntro. iApply (big_sepL_wand with "Hb").
iApply big_sepL_intro. iIntros "!>" (k [rt0 [ty0 r0]] Hlook).
@@ -1843,7 +1813,7 @@ Section unfold.
(∃ r' : plist place_rfn rts, gvar_auth γ r' ∗
(|={lftE}=> ∃ v : val, l ↦ v ∗ v â—áµ¥{ Ï€} r' @ struct_t sls tys)) ↔
(∃ r' : plist place_rfn rts, gvar_auth γ r' ∗ (|={lftE}=>
- [∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts ((λ X : Type, OfTy) +<$> tys) r') (λ ly : layout, existT (unit : Type) (UninitLtype (UntypedSynType ly), PlaceIn ())),
+ [∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts ((λ X : Type, OfTy) +<$> tys) r') struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗
⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
(l +â‚— offset_of_idx (sl_members sl) i) â—â‚—[ Ï€, Owned wl] (projT2 ty).2 @ if b then ltype_core (projT2 ty).1 else (projT2 ty).1)).
@@ -1856,7 +1826,7 @@ Section unfold.
assert (sl' = sl) as ->. { by eapply struct_layout_spec_has_layout_inj. }
rewrite hpzipl_hmap.
set (f := (λ '(existT x (a, b)), existT x (◠a, b))%I).
- rewrite (pad_struct_ext _ _ _ (λ ly, f (existT (unit : Type) (uninit (UntypedSynType ly), PlaceIn ())))); last done.
+ rewrite (pad_struct_ext _ _ _ (λ ly, f $ struct_make_uninit_type ly)); last done.
rewrite pad_struct_fmap big_sepL_fmap.
rewrite heap_mapsto_reshape_sl; last done. iDestruct "Hl" as "(_ & Hl)".
iPoseProof (big_sepL2_sep_sepL_l with "[$Hl $Hb]") as "Ha".
@@ -1987,7 +1957,7 @@ Section unfold.
⊢ ltype_incl' (Uniq κ γ) r r (◠(struct_t sls tys))%I (StructLtype (hmap (λ _, OfTy) tys) sls).
Proof.
iModIntro. iIntros (Ï€ l). rewrite ltype_own_struct_unfold ltype_own_ofty_unfold /lty_of_ty_own /struct_ltype_own.
- iIntros "(%ly & %Hst & %Hly & %Hsc & #Hlb & Hrfn & ? & ? & Hb)". simpl in Hst.
+ iIntros "(%ly & %Hst & %Hly & %Hsc & #Hlb & Hrfn & ? & Hb)". simpl in Hst.
apply use_layout_alg_struct_Some_inv in Hst as (sl & Hst & ->).
iExists sl. iSplitR; first done.
(* NOTE: here we really need the ty_sidecond; we would not be able to just extract this info out from under the borrow! *)
@@ -2156,7 +2126,7 @@ Section unfold.
rewrite -big_sepL_fupd.
rewrite hpzipl_hmap.
set (f := (λ '(existT x (a, b)), existT x (◠a, b))%I).
- rewrite (pad_struct_ext _ _ _ (λ ly, f (existT (unit : Type) (uninit (UntypedSynType ly), PlaceIn ())))); last done.
+ rewrite (pad_struct_ext _ _ _ (λ ly, f $ struct_make_uninit_type ly)); last done.
rewrite pad_struct_fmap big_sepL_fmap.
iApply (big_sepL_wand with "Hb").
iApply big_sepL_intro. iIntros "!>" (k [rt0 [ty0 r0]] Hlook).
@@ -2171,7 +2141,7 @@ Section unfold.
⊢ ltype_incl' (Uniq κ γ) r r (StructLtype (hmap (λ _, OfTy) tys) sls) (◠(struct_t sls tys))%I.
Proof.
iModIntro. iIntros (Ï€ l). rewrite ltype_own_struct_unfold ltype_own_ofty_unfold /lty_of_ty_own /struct_ltype_own.
- iIntros "(%sl & %Hst & %Hlen & %Hly & #Hlb & Hrfn & ? & ? & Hb)".
+ iIntros "(%sl & %Hst & %Hlen & %Hly & #Hlb & Hrfn & ? & Hb)".
iExists sl.
iSplitR. { iPureIntro. eapply use_struct_layout_alg_Some_inv; done. }
iSplitR; first done.
@@ -2368,6 +2338,215 @@ Section lemmas.
*)
Abort.
+ (*Lemma idx_of_to_field_idx : *)
+ (*i < *)
+ (*idx_of_field_idx fields (field_idx_of_idx fields i) = i.*)
+
+ (* TODO move *)
+ Local Lemma pad_struct_focus' {A} (els : list A) fields (make_uninit : layout → A) (Φ : nat → A → iProp Σ) (i0 : nat) :
+ length els = length (named_fields fields) →
+ ([∗ list] i ↦ x ∈ pad_struct fields els make_uninit, Φ (i + i0) x) -∗
+ (* get just the named fields *)
+ ([∗ list] i ↦ x ∈ els, ∃ j ly n, ⌜fields !! j = Some (Some n, ly)⌠∗ ⌜named_fields fields !! (i)%nat = Some (n, ly)⌠∗ Φ (j + i0) x) ∗
+ (* if we return the named fields, we can get back the whole thing *)
+ (∀ els',
+ ⌜length els' = length els⌠-∗
+
+ ([∗ list] i ↦ x ∈ els', ∃ j ly n, ⌜fields !! j = Some (Some n, ly)⌠∗ ⌜named_fields fields !! (i + i0)%nat = Some (n, ly)⌠∗ Φ (j + i0) x) -∗
+
+ ([∗ list] i ↦ x ∈ pad_struct fields els' make_uninit, Φ (i + i0) x)).
+ Proof.
+
+ (* What do we need to piece it together?
+ basically I should be able to go via uniqueness of names I guess
+
+ (* TODO *)
+ *)
+
+ iIntros (Hlen) "Ha".
+ iInduction fields as [ | [n ly] fields] "IH" forall (els Hlen i0); simpl.
+ { simpl in Hlen. destruct els; last done. simpl. iR. iIntros (els' Hlen').
+ destruct els'; last done. eauto. }
+ destruct n as [ n | ]; simpl.
+ - simpl in Hlen. destruct els as [ | el els]; first done; simpl in *.
+ iDestruct "Ha" as "(Ha & Hb)".
+ iPoseProof ("IH" $! els with "[] [Hb]") as "(Hb & Hcl)".
+ { iPureIntro. lia. }
+ { setoid_rewrite <-Nat.add_succ_r. iApply "Hb". }
+ iSplitL "Ha Hb".
+ { (* show the split *)
+ iSplitL "Ha".
+ { iExists 0, _, _. iR. iR. done. }
+ iApply (big_sepL_impl with "Hb"). iModIntro. iIntros (k x Hlook).
+ iIntros "(%j & % & % & %Hlook1 & %Hlook2 & Ha)".
+ iExists (S j), _, _. simpl. iR. iR. rewrite Nat.add_succ_r. done. }
+ (* show that we can shift back *)
+ iIntros (els' Hlen') "Ha".
+ destruct els' as [ | el' els']; first done. simpl.
+ iDestruct "Ha" as "((%j & % & % & % & % & Ha) & Hb)".
+ (* now we have these elements back *)
+ iPoseProof ("Hcl" $! els' with "[] [Hb]") as "Hb".
+ { iPureIntro. simpl in *. lia. }
+ { iApply (big_sepL_impl with "Hb"). iModIntro. iIntros (k x Hlook).
+ iIntros "(%j' & % & % & %Hlook1 & %Hlook2 & Ha)".
+ destruct j'.
+ { simpl in *. injection Hlook1 as [= [= <-] <-].
+ (*iExists (S j'), _, _. i*)
+
+ (*iExists (S j'), _, _. *)
+ Admitted.
+ Lemma pad_struct_focus {A} (els : list A) fields (make_uninit : layout → A) (Φ : nat → A → iProp Σ) :
+ length els = length (named_fields fields) →
+ ([∗ list] i ↦ x ∈ pad_struct fields els make_uninit, Φ i x) -∗
+ ([∗ list] i ↦ x ∈ els, ∃ j ly n, ⌜fields !! j = Some (Some n, ly)⌠∗ ⌜named_fields fields !! i = Some (n, ly)⌠∗ Φ j x) ∗
+ (∀ els',
+ ⌜length els' = length els⌠-∗
+ ([∗ list] i ↦ x ∈ els', ∃ j ly n, ⌜fields !! j = Some (Some n, ly)⌠∗ ⌜named_fields fields !! i = Some (n, ly)⌠∗ Φ j x) -∗
+ ([∗ list] i ↦ x ∈ pad_struct fields els' make_uninit, Φ i x)).
+ Proof.
+ iIntros (?) "Ha".
+ iPoseProof (pad_struct_focus' els fields make_uninit Φ 0 with "[Ha]") as "Ha".
+ { done. }
+ { setoid_rewrite Nat.add_0_r. done. }
+ setoid_rewrite Nat.add_0_r. done.
+ Qed.
+
+
+ (* TODO ; move + upstream *)
+ Lemma list_lookup_omap_Some {A B} (l : list A) (f : A → option B) x y i :
+ l !! i = Some x →
+ f x = Some y →
+ ∃ j, omap f l !! j = Some y.
+ Proof.
+ induction l as [ | h l IH] in i |-*; simpl; first done.
+ destruct i as [ | i]; simpl.
+ - intros [= ->] -> => /=.
+ by exists 0.
+ - intros Hlook Ha. destruct (IH _ Hlook Ha) as (j & Hlook').
+ destruct (f h) as [Hx | ].
+ + exists (S j). naive_solver.
+ + naive_solver.
+ Qed.
+
+ (* TODO move *)
+ Lemma sl_index_of_lookup sl n i :
+ index_of (sl_members sl) n = Some i ↔ (∃ ly : layout, sl.(sl_members) !! i = Some (Some n, ly)).
+ Proof.
+ rewrite index_of_lookup.
+ split; first naive_solver.
+ intros (ly & Hsl). exists ly. split; first done.
+ intros j (n' & ly') Hlook Hlt.
+ simpl. destruct n' as [ n' | ]; last naive_solver.
+ intros [= ->].
+ move: Hsl Hlook.
+ assert (NoDup (field_names (sl_members sl))) as Hnd.
+ { specialize (sl_nodup sl). case_bool_decide; naive_solver. }
+ move: Hnd. generalize (sl_members sl) as fields. clear sl.
+ induction fields as [ | [n1 ly1] fields IH] in i, j, Hlt |-*; simpl.
+ { naive_solver. }
+ destruct n1 as [ n1 | ].
+ - (* named head *)
+ rewrite NoDup_cons. intros [Hnel Hnd].
+ destruct i as [ | i].
+ { simpl. intros [= [= ->] ->]. destruct j; lia. }
+ simpl. destruct j as [ | j]; simpl.
+ { intros Ha [= [= ->] ->].
+ apply Hnel. apply elem_of_list_omap.
+ eexists (_, _); split; last done.
+ by eapply elem_of_list_lookup_2. }
+ { eapply IH; last done. lia. }
+ - intros Hnd.
+ destruct i as [ | i]; first done.
+ simpl. destruct j as [ | j]; simpl; first done.
+ eapply IH; last done. lia.
+ Qed.
+ Lemma sl_index_of_lookup_1 sl i n :
+ index_of sl.(sl_members) n = Some i →
+ ∃ ly, sl.(sl_members) !! i = Some (Some n, ly).
+ Proof.
+ intros Ha. apply sl_index_of_lookup. eauto.
+ Qed.
+ Lemma sl_index_of_lookup_2 sl i n ly :
+ sl.(sl_members) !! i = Some (Some n, ly) →
+ index_of sl.(sl_members) n = Some i.
+ Proof.
+ intros Ha. apply sl_index_of_lookup. eauto.
+ Qed.
+
+ (** Focus the initialized fields of a struct, disregarding the padding fields *)
+ Lemma struct_ltype_focus_components π {rts : list Type} (lts : hlist ltype rts) (rs : plist place_rfn rts) sls sl k l :
+ length rts = length (sls_fields sls) →
+ struct_layout_spec_has_layout sls sl →
+ ([∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts lts rs) struct_make_uninit_ltype,
+ ∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗
+ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
+ (l +â‚— offset_of_idx (sl_members sl) i) â—â‚—[ Ï€, k] (projT2 ty).2 @ (projT2 ty).1) -∗
+ (* we get access to the named fields *)
+ ([∗ list] i↦p ∈ hpzipl rts lts rs, let 'existT rt (lt, r) := p in ∃ (name : var_name) (st : syn_type), ⌜sls_fields sls !! i = Some (name, st)⌠∗ l atst{sls}â‚— name â—â‚—[ Ï€, k] r @ lt) ∗
+ (* we can update the named fields: *)
+ (∀ (rts' : list Type) (lts' : hlist ltype rts') rs',
+ (* syn types need to be the same *)
+ ⌜length rts = length rts'⌠-∗
+ (⌜Forall2 (λ p p2, let 'existT rt (lt, _) := p in let 'existT rt' (lt', _) := p2 in ltype_st lt = ltype_st lt') (hpzipl rts lts rs) (hpzipl rts' lts' rs')âŒ) -∗
+ (* ownership *)
+ ([∗ list] i↦p ∈ hpzipl rts' lts' rs', let 'existT rt (lt, r) := p in ∃ (name : var_name) (st : syn_type), ⌜sls_fields sls !! i = Some (name, st)⌠∗ l atst{sls}â‚— name â—â‚—[ Ï€, k] r @ lt) -∗
+ (* we get back the full struct ownership *)
+ ([∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts' lts' rs') struct_make_uninit_ltype,
+ ∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗
+ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
+ (l +â‚— offset_of_idx (sl_members sl) i) â—â‚—[ Ï€, k] (projT2 ty).2 @ (projT2 ty).1)).
+ Proof.
+ iIntros (Hlen Halg) "Hl".
+ iPoseProof (pad_struct_focus with "Hl") as "(Hl & Hl_cl)".
+ { rewrite hpzipl_length. rewrite named_fields_field_names_length (struct_layout_spec_has_layout_fields_length sls); done. }
+ (* remember the layouts *)
+ iAssert ([∗ list] i↦x ∈ hpzipl rts lts rs, ∃ (ly : layout) (n : string), ⌜named_fields (sl_members sl) !! i = Some (n, ly)⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 x).1) lyâŒ)%I with "[Hl]" as "%Hly_agree".
+ { iApply (big_sepL_impl with "Hl").
+ iModIntro. iIntros (j [rt [lt r]] Hlook).
+ iIntros "(%j' & %ly & %n & %Hmem & %Hnamed & %ly' & %Hmem' & %Hst & Hl)".
+ rewrite Hmem in Hmem'. simpl in *. injection Hmem' as <-.
+ specialize (struct_layout_spec_has_layout_alt_2 _ _ Halg) as Halg2.
+ eapply Forall2_lookup_r in Halg2; last done.
+ destruct Halg2 as ([n' st'] & Hfields & Hst' & <-).
+ rewrite Hnamed. iExists _, _. done. }
+
+ iSplitL "Hl".
+ { iApply (big_sepL_impl with "Hl").
+ iModIntro. iIntros (j [rt [lt r]] Hlook).
+ iIntros "(%j' & %ly & %n & %Hmem & %Hnamed & %ly' & %Hmem' & %Hst & Hl)".
+ rewrite Hmem in Hmem'. simpl in *. injection Hmem' as <-.
+ specialize (struct_layout_spec_has_layout_alt_2 _ _ Halg) as Halg2.
+ eapply Forall2_lookup_r in Halg2; last done.
+ destruct Halg2 as ([n' st'] & Hfields & Hst' & <-).
+ iExists _, _. rewrite /GetMemberLocSt.
+ rewrite /use_struct_layout_alg'.
+ iR. rewrite Halg. simpl.
+ rewrite /offset_of.
+ erewrite sl_index_of_lookup_2; last done.
+ done. }
+ iIntros (rts' lts' rs') "%Hlen_eq %Hst Hb".
+ iApply "Hl_cl". { rewrite !hpzipl_length//. }
+
+ iApply (big_sepL_impl with "Hb").
+ iModIntro. iIntros (ka [rt [lt r]] Hlook) "(%n & %st & %Hst' & Hl)".
+ simpl.
+ specialize (struct_layout_spec_has_layout_lookup sls sl n _ _ Halg Hst') as Hidx.
+ specialize (struct_layout_spec_has_layout_alt_2 _ _ Halg) as Halg2.
+ eapply Forall2_lookup_l in Halg2 as ([n' ly'] & Hlook' & Hly); last done.
+ simpl in Hly. destruct Hly as (Hly & ->).
+ specialize (named_fields_lookup_1 _ _ _ _ Hlook') as (ka' & Hlook'').
+
+ eapply Forall2_lookup_r in Hst; last done.
+ destruct Hst as ([rt' [lt' r']] & Hlook2 & Hst).
+ rewrite -Hst.
+ eapply Hly_agree in Hlook2 as (ly2 & n2 & Hlook2 & Hst2).
+ simpl in *. rewrite Hlook' in Hlook2. injection Hlook2 as [= <- <-].
+ iExists ka', ly', n. iR. iR.
+ iExists _. rewrite Hlook''. iR. iR.
+ rewrite /GetMemberLocSt /use_struct_layout_alg' Halg /=.
+ rewrite /offset_of. erewrite sl_index_of_lookup_2; done.
+ Qed.
+
End lemmas.
Section rules.
@@ -2440,7 +2619,7 @@ Section rules.
iIntros "_". done.
Qed.
- Lemma typed_place_cond_rfn_lift_struct {rts} (rs rs' : plist place_rfn rts) k :
+ Lemma typed_place_cond_rfn_lift_struct {rts} (rs rs' : plist place_rfn rts) k :
([∗ list] ty1;ty2 ∈ pzipl rts rs;pzipl rts rs', typed_place_cond_rfn k (projT2 ty1) (projT2 ty2)) ⊢@{iProp Σ} typed_place_cond_rfn k (#rs) (#rs').
Proof.
iIntros "Ha". destruct k; done.
@@ -2460,6 +2639,24 @@ Section rules.
*)
Qed.
+ Lemma typed_place_cond_struct_lift {rts rts'} (lts : hlist ltype rts) (lts' : hlist ltype rts') r r' sls bmin:
+ ([∗ list] ty1; ty2 ∈ hzipl rts lts; hzipl rts' lts', typed_place_cond_ty bmin (projT2 ty1) (projT2 ty2)) -∗
+ ([∗ list] ty1; ty2 ∈ pzipl rts r; pzipl rts' r', typed_place_cond_rfn bmin (projT2 ty1) (projT2 ty2)) -∗
+ ⌜Forall2 (place_access_rt_rel bmin) rts rts'⌠-∗
+ typed_place_cond bmin (StructLtype lts sls) (StructLtype lts' sls) (#r) (#r').
+ Proof.
+ iIntros "Hcond_ty Hcond_rfn %Hrt".
+ rewrite /typed_place_cond.
+ iSplitL "Hcond_ty".
+ { iApply struct_ltype_place_cond_ty; done. }
+ destruct bmin; simpl; [done | | done].
+ assert (rts = rts') as <-.
+ { clear -Hrt. rewrite /place_access_rt_rel in Hrt.
+ induction rts as [ | ?? IH] in rts', Hrt |-*; destruct rts' as [ | ??]; inversion Hrt; try done.
+ subst. f_equiv. by eapply IH. }
+ done.
+ Qed.
+
Lemma struct_ltype_acc_owned {rts} F π (lts : hlist ltype rts) (r : plist place_rfn rts) l sls wl :
lftE ⊆ F →
l â—â‚—[Ï€, Owned wl] #r @ StructLtype lts sls -∗
@@ -2477,12 +2674,7 @@ Section rules.
([∗ list] i ↦ ty ∈ pad_struct (sl_members sl) (hpzipl rts' lts' r') struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
(l +â‚— offset_of_idx sl.(sl_members) i) â—â‚—[Ï€, Owned false] (projT2 ty).2 @ (projT2 ty).1) ={F}=∗
- l â—â‚—[Ï€, Owned wl] #r' @ StructLtype lts' sls ∗
- (* place condition, if required *)
- (∀ bmin, ([∗ list] ty1; ty2 ∈ hzipl rts lts; hzipl rts' lts', typed_place_cond_ty bmin (projT2 ty1) (projT2 ty2)) -∗
- ([∗ list] ty1; ty2 ∈ pzipl rts r; pzipl rts' r', typed_place_cond_rfn bmin (projT2 ty1) (projT2 ty2)) -∗
- ⌜Forall2 (place_access_rt_rel bmin) rts rts'⌠-∗
- typed_place_cond bmin (StructLtype lts sls) (StructLtype lts' sls) (#r) (#r'))).
+ l â—â‚—[Ï€, Owned wl] #r' @ StructLtype lts' sls).
Proof.
iIntros (?) "Hb". rewrite ltype_own_struct_unfold /struct_ltype_own.
iDestruct "Hb" as "(%sl & %Halg & %Hlen & %Hly & #Hlb & Hcred & %r' & -> & Hb)".
@@ -2491,78 +2683,44 @@ Section rules.
iModIntro. iFrame.
iApply (logical_step_intro_maybe with "Hat"). iIntros "Hcred' !>".
iIntros (rts' lts' r) "%Hlen_eq Hb".
- iSplitL "Hb Hcred'".
- { rewrite ltype_own_struct_unfold /struct_ltype_own.
- iExists sl. rewrite Hlen_eq. iFrame "%#∗".
- iExists r. iSplitR; first done. iModIntro. done. }
- iModIntro.
- iIntros (bmin) "Hcond_ty Hcond_rfn %Hrt".
- rewrite /typed_place_cond.
- iSplitL "Hcond_ty".
- { iApply struct_ltype_place_cond_ty; done. }
- destruct bmin; simpl; [done | | done].
- assert (rts = rts') as <-.
- { clear -Hrt. rewrite /place_access_rt_rel in Hrt.
- induction rts as [ | ?? IH] in rts', Hrt |-*; destruct rts' as [ | ??]; inversion Hrt; try done.
- subst. f_equiv. by eapply IH. }
- done.
- (*
- iExists eq_refl. iClear "Hlb Hcred". clear.
- iInduction rts as [ | rt rts IH] "IH".
- - destruct r, r'. done.
- - destruct r as [r0 r], r' as [r0' r'].
- simpl. iDestruct "Hcond_rfn" as "(Hh & Hcond_rfn)".
- iDestruct ("IH" with "Hcond_rfn") as "%Heq". injection Heq as <-.
- iDestruct "Hh" as "(%Heq & %Heq2)".
- rewrite -Heq2. rewrite (UIP_refl _ _ Heq). done.
- *)
+ rewrite ltype_own_struct_unfold /struct_ltype_own.
+ iExists sl. rewrite Hlen_eq. iFrame "%#∗".
+ iExists r. iSplitR; first done. iModIntro. done.
Qed.
Definition sigT_ltype_core : (sigT (λ rt, ltype rt * place_rfn rt)%type) → (sigT (λ rt, ltype rt * place_rfn rt)%type) := λ '(existT _ (lt, r)), existT _ (ltype_core lt, r).
- Local Lemma pad_struct_pull_core {rts} (lts : hlist ltype rts) (rs : plist place_rfn rts) fields (Φ : nat → (sigT (λ rt, ltype rt * place_rfn rt)%type) → iProp Σ) :
+ Local Lemma pad_struct_pull_core {rts} (lts : hlist ltype rts) (rs : plist place_rfn rts) fields (Φ : nat → (sigT (λ rt, ltype rt * place_rfn rt)%type) → iProp Σ) :
([∗ list] i↦ty ∈ pad_struct fields (hpzipl rts (@ltype_core Σ typeGS0 +<$> lts) rs) struct_make_uninit_ltype, Φ i ty)%I ⊣⊢
([∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts rs) struct_make_uninit_ltype, Φ i (sigT_ltype_core ty))%I.
Proof.
- rewrite hpzipl_hmap.
+ rewrite hpzipl_hmap.
rewrite (pad_struct_ext _ _ _ (λ ly, sigT_ltype_core (struct_make_uninit_ltype ly))); first last.
- { intros ly. simpl. rewrite ltype_core_uninit. reflexivity. }
+ { intros ly. simpl. rewrite ltype_core_uninit. reflexivity. }
rewrite (pad_struct_fmap _ _ _ sigT_ltype_core) big_sepL_fmap.
done.
Qed.
- Lemma ltype_core_sigT_ltype_core_idemp ty :
+ Lemma ltype_core_sigT_ltype_core_idemp ty :
ltype_core ((projT2 $ sigT_ltype_core ty).1) = (projT2 $ sigT_ltype_core ty).1.
Proof.
destruct ty as [? []]; simpl. rewrite ltype_core_idemp //.
Qed.
- Lemma ltype_st_sigT_ltype_core ty :
+ Lemma ltype_st_sigT_ltype_core ty :
ltype_st ((projT2 $ sigT_ltype_core ty).1) = ltype_st (projT2 ty).1.
Proof.
destruct ty as [? []]; simpl. rewrite ltype_core_syn_type_eq //.
Qed.
- Lemma typed_place_cond_ty_uniq_core_eq {rt} (lt1 lt2 : ltype rt) κ γ :
- typed_place_cond_ty (Uniq κ γ) lt1 lt2 -∗ ∀ b r, ltype_eq b r r (ltype_core lt1) (ltype_core lt2).
- Proof.
- iIntros "(%Heq & Ha & _)". rewrite (UIP_refl _ _ Heq). done.
- Qed.
- Lemma typed_place_cond_ty_uniq_unblockable {rt1 rt2} (lt1 : ltype rt1) (lt2 : ltype rt2) κ γ :
- typed_place_cond_ty (Uniq κ γ) lt1 lt2 -∗ imp_unblockable [κ] lt2.
- Proof.
- iIntros "(%Heq & _ & Ha)". done.
- Qed.
- Lemma typed_place_cond_ty_uniq_core_eq_big {rts} (lts1 : hlist ltype rts) (lts2 : hlist ltype rts) κ γ :
+ Local Lemma typed_place_cond_ty_uniq_core_eq_struct {rts} (lts1 : hlist ltype rts) (lts2 : hlist ltype rts) κ γ :
([∗ list] ty1; ty2 ∈ hzipl rts lts1; hzipl rts lts2, typed_place_cond_ty (Uniq κ γ) (projT2 ty1) (projT2 ty2)) -∗
([∗ list] ty ∈ hzipl2 rts lts1 lts2, ∀ b' r, ltype_eq b' r r (ltype_core (projT2 ty).1) (ltype_core (projT2 ty).2)).
Proof.
iIntros "Hcond".
iPoseProof (big_sepL2_to_zip with "Hcond") as "Hcond".
rewrite zip_hzipl_hzipl2 big_sepL_fmap.
- iApply (big_sepL_impl with "Hcond").
- iModIntro. iIntros (? [rt [lt1 lt2]] Hlook).
- simpl. iIntros "(%Heq & Heq & _)". rewrite (UIP_refl _ _ Heq).
- done.
+ iApply (big_sepL_impl with "Hcond"). iModIntro. iIntros (? [rt [lt1 lt2]] Hlook).
+ iApply typed_place_cond_ty_uniq_core_eq.
Qed.
- Lemma typed_place_cond_ty_uniq_unblockable_big {rts} (lts1 : hlist ltype rts) (lts2 : hlist ltype rts) κ γ :
+ Local Lemma typed_place_cond_ty_uniq_unblockable_struct {rts} (lts1 : hlist ltype rts) (lts2 : hlist ltype rts) κ γ :
([∗ list] ty1; ty2 ∈ hzipl rts lts1; hzipl rts lts2, typed_place_cond_ty (Uniq κ γ) (projT2 ty1) (projT2 ty2)) -∗
([∗ list] ty ∈ hzipl2 rts lts1 lts2, imp_unblockable [κ] (projT2 ty).2).
Proof.
@@ -2571,61 +2729,61 @@ Section rules.
rewrite zip_hzipl_hzipl2 big_sepL_fmap.
iApply (big_sepL_impl with "Hcond").
iModIntro. iIntros (? [rt [lt1 lt2]] Hlook).
- simpl. iIntros "(%Heq & _ & Hub)". done.
+ iApply typed_place_cond_ty_uniq_unblockable.
Qed.
Local Lemma struct_acc_uniq_elems_core π l {rts} (lts lts' : hlist ltype rts) (rs : plist place_rfn rts) fields :
length (field_names fields) = length rts →
([∗ list] ty ∈ hzipl2 rts lts lts', ∀ b' r, ltype_eq b' r r (ltype_core (projT2 ty).1) (ltype_core (projT2 ty).2)) -∗
- ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts rs) struct_make_uninit_ltype,
+ ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts rs) struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> fields !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗ (l +â‚— offset_of_idx fields i) â—â‚—[ Ï€, Owned false] (projT2 ty).2 @ ltype_core (projT2 ty).1)) -∗
- ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts' rs) struct_make_uninit_ltype,
+ ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts' rs) struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> fields !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗ (l +â‚— offset_of_idx fields i) â—â‚—[ Ï€, Owned false] (projT2 ty).2 @ ltype_core (projT2 ty).1)).
Proof.
iIntros (Ha) "#Hcond >Hb". iApply big_sepL_fupd.
- iApply big_sepL2_elim_l.
- iPoseProof (big_sepL_extend_r with "Hb") as "Hb"; first last.
- { iApply (big_sepL2_impl with "Hb").
- iModIntro. iIntros (? [? []] [? []] Hlook1 Hlook2).
- simpl. iIntros "(%ly & ? & ? & Hl)".
- apply pad_struct_lookup_Some in Hlook1 as (n & ly1 & Hlook & Hlook1); first last.
+ iApply big_sepL2_elim_l.
+ iPoseProof (big_sepL_extend_r with "Hb") as "Hb"; first last.
+ { iApply (big_sepL2_impl with "Hb").
+ iModIntro. iIntros (? [? []] [? []] Hlook1 Hlook2).
+ simpl. iIntros "(%ly & ? & ? & Hl)".
+ apply pad_struct_lookup_Some in Hlook1 as (n & ly1 & Hlook & Hlook1); first last.
+ { rewrite hpzipl_length Ha. lia. }
+ destruct Hlook1 as [(? & Hlook1) | (-> & Hlook1)].
+ - apply hpzipl_lookup_inv_hzipl_pzipl in Hlook1 as (Hlook1 & Hlook1').
+ destruct n; last done.
+ eapply pad_struct_lookup_Some_Some in Hlook2; cycle -2.
{ rewrite hpzipl_length Ha. lia. }
- destruct Hlook1 as [(? & Hlook1) | (-> & Hlook1)].
- - apply hpzipl_lookup_inv_hzipl_pzipl in Hlook1 as (Hlook1 & Hlook1').
- destruct n; last done.
- eapply pad_struct_lookup_Some_Some in Hlook2; cycle -2.
- { rewrite hpzipl_length Ha. lia. }
- { done. }
- apply hpzipl_lookup_inv_hzipl_pzipl in Hlook2 as (Hlook2 & Hlook2').
- rewrite Hlook1' in Hlook2'. injection Hlook2' => Heq1 ?. subst.
- apply existT_inj in Heq1 as ->.
- iPoseProof (big_sepL_lookup with "Hcond")as "Heq".
- { apply hzipl_hzipl2_lookup; done. }
- (*iPoseProof (typed_place_cond_ty_incl _ (Uniq κ γ) with "Hincl_k Hcond'") as "Hcond''".*)
- iDestruct ("Heq" $! (Owned _) _) as "((%Hst1 & #Heq1 & _) & (_ & #Heq2 & _))".
- (*setoid_rewrite ltype_own_core_equiv. *)
- iPoseProof ("Heq1" with "Hl") as "Hb".
- simpl in Hst1. rewrite !ltype_core_syn_type_eq in Hst1.
- iMod "Hb". iModIntro. rewrite Hst1. cbn. eauto with iFrame.
- - injection Hlook1 => Hlook1_1 Hlook1_2 ?. subst.
- apply existT_inj in Hlook1_2. apply existT_inj in Hlook1_1. subst.
- eapply pad_struct_lookup_Some_None in Hlook2; cycle 1.
- { rewrite hpzipl_length Ha. lia. }
- { done. }
- injection Hlook2 => Hlook2_1 Hlook2_2 ?. subst.
- apply existT_inj in Hlook2_1. apply existT_inj in Hlook2_2. subst.
- eauto with iFrame.
- }
- rewrite !pad_struct_length //.
+ { done. }
+ apply hpzipl_lookup_inv_hzipl_pzipl in Hlook2 as (Hlook2 & Hlook2').
+ rewrite Hlook1' in Hlook2'. injection Hlook2' => Heq1 ?. subst.
+ apply existT_inj in Heq1 as ->.
+ iPoseProof (big_sepL_lookup with "Hcond")as "Heq".
+ { apply hzipl_hzipl2_lookup; done. }
+ (*iPoseProof (typed_place_cond_ty_incl _ (Uniq κ γ) with "Hincl_k Hcond'") as "Hcond''".*)
+ iDestruct ("Heq" $! (Owned _) _) as "((%Hst1 & #Heq1 & _) & (_ & #Heq2 & _))".
+ (*setoid_rewrite ltype_own_core_equiv. *)
+ iPoseProof ("Heq1" with "Hl") as "Hb".
+ simpl in Hst1. rewrite !ltype_core_syn_type_eq in Hst1.
+ iMod "Hb". iModIntro. rewrite Hst1. cbn. eauto with iFrame.
+ - injection Hlook1 => Hlook1_1 Hlook1_2 ?. subst.
+ apply existT_inj in Hlook1_2. apply existT_inj in Hlook1_1. subst.
+ eapply pad_struct_lookup_Some_None in Hlook2; cycle 1.
+ { rewrite hpzipl_length Ha. lia. }
+ { done. }
+ injection Hlook2 => Hlook2_1 Hlook2_2 ?. subst.
+ apply existT_inj in Hlook2_1. apply existT_inj in Hlook2_2. subst.
+ eauto with iFrame.
+ }
+ rewrite !pad_struct_length //.
Qed.
Local Lemma struct_acc_uniq_elems_unblock π l {rts} (lts lts' : hlist ltype rts) (rs : plist place_rfn rts) fields κ γ :
length (field_names fields) = length rts →
([∗ list] ty1;ty2 ∈ hzipl rts lts;hzipl rts lts', typed_place_cond_ty (Uniq κ γ) (projT2 ty1) (projT2 ty2)) -∗
[†κ] -∗
- ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts' rs) struct_make_uninit_ltype,
+ ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts' rs) struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> fields !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗ (l +â‚— offset_of_idx fields i) â—â‚—[ Ï€, Owned false] (projT2 ty).2 @ (projT2 ty).1)) -∗
- ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts rs) struct_make_uninit_ltype,
+ ((|={lftE}=> [∗ list] i↦ty ∈ pad_struct fields (hpzipl rts lts rs) struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> fields !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗ (l +â‚— offset_of_idx fields i) â—â‚—[ Ï€, Owned false] (projT2 ty).2 @ ltype_core (projT2 ty).1)).
Proof.
iIntros (Ha) "#Hcond #Hdead >Hb". iApply big_sepL_fupd.
@@ -2643,33 +2801,33 @@ Section rules.
{ rewrite hpzipl_length Ha. lia. }
{ done. }
apply hpzipl_lookup_inv_hzipl_pzipl in Hlook2 as (Hlook2 & Hlook2').
- rewrite Hlook1' in Hlook2'. injection Hlook2' => Heq1 ?. subst.
+ rewrite Hlook1' in Hlook2'. injection Hlook2' => Heq1 ?. subst.
apply existT_inj in Heq1 as ->.
- iPoseProof (typed_place_cond_ty_uniq_core_eq_big _ _ κ γ with "Hcond") as "Heq".
- iPoseProof (typed_place_cond_ty_uniq_unblockable_big _ _ κ γ with "Hcond") as "Hub".
+ iPoseProof (typed_place_cond_ty_uniq_core_eq_struct _ _ κ γ with "Hcond") as "Heq".
+ iPoseProof (typed_place_cond_ty_uniq_unblockable_struct _ _ κ γ with "Hcond") as "Hub".
iPoseProof (big_sepL_lookup with "Heq") as "Heq1".
{ apply hzipl_hzipl2_lookup; done. }
iPoseProof (big_sepL_lookup with "Hub") as "Hub1".
- { apply hzipl_hzipl2_lookup; done. }
+ { apply hzipl_hzipl2_lookup; done. }
cbn.
iMod (imp_unblockable_use with "Hub1 [] Hl") as "Hl"; first done.
{ iFrame "Hdead"; done. }
iDestruct ("Heq1" $! (Owned _) _) as "((%Hst1 & #Heq1' & _) & (_ & #Heq2 & _))".
iMod ("Heq2" with "Hl") as "Hl".
- rewrite !ltype_core_syn_type_eq in Hst1.
- rewrite -Hst1.
+ rewrite !ltype_core_syn_type_eq in Hst1.
+ rewrite -Hst1.
eauto with iFrame.
- injection Hlook1 => Hlook1_1 Hlook1_2 ?. subst.
apply existT_inj in Hlook1_2. apply existT_inj in Hlook1_1. subst.
eapply pad_struct_lookup_Some_None in Hlook2; cycle 1.
{ rewrite hpzipl_length Ha. lia. }
- { done. }
- injection Hlook2 => Hlook2_1 Hlook2_2 ?. subst.
+ { done. }
+ injection Hlook2 => Hlook2_1 Hlook2_2 ?. subst.
apply existT_inj in Hlook2_1. apply existT_inj in Hlook2_2. subst.
setoid_rewrite ltype_core_uninit. eauto with iFrame.
- }
- rewrite !pad_struct_length //.
+ }
+ rewrite !pad_struct_length //.
Qed.
Lemma struct_ltype_acc_uniq {rts} F π (lts : hlist ltype rts) (r : plist place_rfn rts) l sls κ γ q R :
@@ -2694,7 +2852,7 @@ Section rules.
(l +â‚— offset_of_idx sl.(sl_members) i) â—â‚—[Ï€, Owned false] (projT2 ty).2 @ (projT2 ty).1) -∗
([∗ list] ty1; ty2 ∈ hzipl rts lts; hzipl rts lts', typed_place_cond_ty (bmin) (projT2 ty1) (projT2 ty2)) -∗
([∗ list] ty1; ty2 ∈ pzipl rts r; pzipl rts r', typed_place_cond_rfn (bmin) (projT2 ty1) (projT2 ty2)) ={F}=∗
- l â—â‚—[Ï€, Uniq κ γ] PlaceIn r' @ StructLtype lts' sls ∗
+ l â—â‚—[Ï€, Uniq κ γ] #r' @ StructLtype lts' sls ∗
R ∗
typed_place_cond (Uniq κ γ ⊓ₖ bmin) (StructLtype lts sls) (StructLtype lts' sls) (PlaceIn r) (PlaceIn r')) ∧
((* strong access, go to OpenedLtype *)
@@ -2709,7 +2867,7 @@ Section rules.
(λ ri ri', ⌜ri = ri'âŒ) (λ _ _, R))).
Proof.
iIntros (?) "#(LFT & TIME & LLCTX) Hκ HR Hb". rewrite ltype_own_struct_unfold /struct_ltype_own.
- iDestruct "Hb" as "(%sl & %Halg & %Hlen & %Hly & #Hlb & Hcred & Hat & Hrfn & Hb)".
+ iDestruct "Hb" as "(%sl & %Halg & %Hlen & %Hly & #Hlb & (Hcred & Hat) & Hrfn & Hb)".
iExists sl. iFrame "#%".
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
iMod "Hb".
@@ -2729,7 +2887,7 @@ Section rules.
- (* close *)
iIntros (bmin lts' rs') "#Hincl_k Hl #Hcond #Hrcond".
iMod (gvar_update rs' with "Hauth Hrfn") as "(Hauth & Hrfn)".
- set (V := (∃ r', gvar_auth γ r' ∗
+ set (V := (∃ r', gvar_auth γ r' ∗
(|={lftE}=> [∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts lts' r') struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗ ltype_own (projT2 ty).1 (Owned false) π (projT2 ty).2 (l +ₗ offset_of_idx (sl_members sl) i)))%I).
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
@@ -2740,7 +2898,7 @@ Section rules.
iModIntro. iNext. iExists r'. iFrame "Hauth".
rewrite Hlen in Ha. clear -Ha.
iMod (lft_incl_dead with "Hincl Hdead") as "Hdead"; first done.
- setoid_rewrite ltype_own_core_equiv.
+ setoid_rewrite ltype_own_core_equiv.
iApply (struct_acc_uniq_elems_unblock with "[Hcond] Hdead Hb").
{ done. }
iApply (big_sepL2_impl with "Hcond").
@@ -2765,17 +2923,17 @@ Section rules.
iAssert ([∗ list] ty1;ty2 ∈ hzipl rts lts;hzipl rts lts', typed_place_cond_ty (Uniq κ γ) (projT2 ty1) (projT2 ty2))%I with "[Hcond]" as "Ha".
{ iApply (big_sepL2_impl with "Hcond"). iModIntro. iIntros (k [] [] ? ?). by iApply typed_place_cond_ty_incl. }
iSplit.
- - iIntros "(%r' & Hauth & Hb)". iExists r'. iFrame. iMod "Hb".
+ - iIntros "(%r' & Hauth & Hb)". iExists r'. iFrame. iMod "Hb".
iApply (struct_acc_uniq_elems_core with "[] Hb"); [ lia | ].
- iApply typed_place_cond_ty_uniq_core_eq_big.
+ iApply typed_place_cond_ty_uniq_core_eq_struct.
iApply (big_sepL2_impl with "Hcond").
iModIntro. iIntros (? [] [] ? ?). iApply (typed_place_cond_ty_incl with "Hincl_k").
- - iIntros "(%r' & Hauth & Hb)". iExists r'. iFrame. iMod "Hb".
+ - iIntros "(%r' & Hauth & Hb)". iExists r'. iFrame. iMod "Hb".
iApply (struct_acc_uniq_elems_core with "[] Hb"); [ lia | ].
rewrite hzipl2_swap big_sepL_fmap.
- iPoseProof (typed_place_cond_ty_uniq_core_eq_big with "Ha") as "Hb".
+ iPoseProof (typed_place_cond_ty_uniq_core_eq_struct with "Ha") as "Hb".
iApply (big_sepL_impl with "Hb").
- iModIntro. iIntros (? [? []] ?) "Heq" => /=.
+ iModIntro. iIntros (? [? []] ?) "Heq" => /=.
iIntros (??). iApply ltype_eq_sym. iApply "Heq".
}
iApply (typed_place_cond_incl bmin).
@@ -2792,18 +2950,18 @@ Section rules.
{ iModIntro. iIntros (?) "Hauth Hc". simp_ltypes.
rewrite ltype_own_struct_unfold /struct_ltype_own.
iExists _. iFrame. iDestruct "Hc" as ">(%sl' & %Hsl' & _ & _ & _ & _ & %r' & -> & >Hb)".
- assert (sl' = sl) as ->. { rewrite Halg in Hsl'. injection Hsl' as ->. done. }
- iModIntro. setoid_rewrite ltype_own_core_equiv.
+ assert (sl' = sl) as ->. { rewrite Halg in Hsl'. injection Hsl' as ->. done. }
+ iModIntro. setoid_rewrite ltype_own_core_equiv.
rewrite pad_struct_pull_core. iApply (big_sepL_impl with "Hb").
iModIntro. iIntros (? [? []] ?). simpl. rewrite ltype_core_syn_type_eq. eauto. }
{ iIntros (?) "Hobs Hat Hcred Hp". simp_ltypes.
rewrite ltype_own_struct_unfold /struct_ltype_own.
- setoid_rewrite ltype_own_core_equiv.
+ setoid_rewrite ltype_own_core_equiv.
iModIntro. iExists sl. iFrame "% ∗". iR.
iModIntro.
setoid_rewrite pad_struct_pull_core.
- setoid_rewrite ltype_core_sigT_ltype_core_idemp.
+ setoid_rewrite ltype_core_sigT_ltype_core_idemp.
setoid_rewrite ltype_st_sigT_ltype_core.
iApply (pinned_bor_iff with "[] [] Hp").
- iNext. iModIntro. iSplit.
@@ -2819,7 +2977,6 @@ Section rules.
iExists rs'. iR. iModIntro. iFrame. }
Qed.
- (* TODO
Lemma struct_ltype_acc_shared {rts} F π (lts : hlist ltype rts) (r : plist place_rfn rts) l sls κ :
lftE ⊆ F →
l â—â‚—[Ï€, Shared κ] #r @ StructLtype lts sls -∗
@@ -2829,53 +2986,32 @@ Section rules.
([∗ list] i ↦ ty ∈ pad_struct (sl_members sl) (hpzipl rts lts r) struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
(l +â‚— offset_of_idx sl.(sl_members) i) â—â‚—[Ï€, Shared κ] (projT2 ty).2 @ (projT2 ty).1) ∗
-
- logical_step F
(∀ rts' (lts' : hlist ltype rts') (r' : plist place_rfn rts'),
(* the number of fields should remain equal *)
⌜length rts' = length rts⌠-∗
(* new ownership *)
([∗ list] i ↦ ty ∈ pad_struct (sl_members sl) (hpzipl rts' lts' r') struct_make_uninit_ltype,
∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗ ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
- (l +â‚— offset_of_idx sl.(sl_members) i) â—â‚—[Ï€, Owned false] (projT2 ty).2 @ (projT2 ty).1) ={F}=∗
- l â—â‚—[Ï€, Owned wl] #r' @ StructLtype lts' sls ∗
- (* place condition, if required *)
- (∀ bmin, ([∗ list] ty1; ty2 ∈ hzipl rts lts; hzipl rts' lts', typed_place_cond_ty bmin (projT2 ty1) (projT2 ty2)) -∗
- ([∗ list] ty1; ty2 ∈ pzipl rts r; pzipl rts' r', typed_place_cond_rfn bmin (projT2 ty1) (projT2 ty2)) -∗
- ⌜Forall2 (place_access_rt_rel bmin) rts rts'⌠-∗
- typed_place_cond bmin (StructLtype lts sls) (StructLtype lts' sls) (#r) (#r'))).
+ (l +â‚— offset_of_idx sl.(sl_members) i) â—â‚—[Ï€, Shared κ] (projT2 ty).2 @ (projT2 ty).1) ={F}=∗
+ l â—â‚—[Ï€, Shared κ] #r' @ StructLtype lts' sls).
Proof.
- *)
+ iIntros (?) "Hb". rewrite ltype_own_struct_unfold /struct_ltype_own.
+ iDestruct "Hb" as "(%sl & %Halg & %Hlen & %Hly & #Hlb & %r' & -> & #Hb)".
+ iExists sl. iFrame "#%". iMod (fupd_mask_mono with "Hb") as "Hb'"; first done.
+ iModIntro. iFrame.
+ iIntros (rts' lts' r) "%Hlen_eq #Hb'".
+ rewrite ltype_own_struct_unfold /struct_ltype_own.
+ iExists sl. rewrite Hlen_eq. iFrame "%#∗".
+ iExists r. iSplitR; first done. iModIntro. done.
+ Qed.
(** Place lemmas for products *)
(* NOTE: these lemmas require sideconditions for the unaffected components of the product that state that we can keep blocked subplaces blocked because the outer bor_kinds outlive the the blocking lifetimes.
It would be good if we could remove this sidecondition with a smarter setup of ltypes... TODO
But it's not clear that that is possible: We can arbitrarily shorten the lifetime of outer things -- then at the later point we just don't knwo anymore that really the lender expects it back at a later point.
-
-
*)
-
- (* TODO maybe need some simplification mechanism here, given that hlist_insert_id/plist_insert_id will not nicely compute due to the eqcasts?
- In practice, the eqcast should be a reflexivity cast, we just need to use UIP_refl to get it to simplify.
- Ideas:
- - have a tactic hint for simplifying it.
- + probably this is simplest. Maybe make it a general purpose simplification tactic, i.e. integrate the map simplification stuff that I already have?
- + problem: this is in a continuation, so we can't concretely simplify yet.
- Rather: need to do that at clients of typed_place.
- Or: do that at users of place types, i.e. SimplifyHypPlace. Have an external instance that just computes. However, that is difficult with descending into.
- Also, getting a reasonable progress indicator for that is difficult.
-
- simplify_term {T} (t : T)
- Can we make this extensible?
- Can we phrase the removal of the eqcast via a tc instance?
-
- - augment Lithium directly with support for doing this stuff. Seems hard though. Ask Michael if he thinks this is sensible?
- - some type class instances in Lithium I could use? Need to understand Lithium's infrastructure for simplification better first. Ask Michael?
- -
- *)
-
- Local Lemma struct_lift_place_cond_ty_homo {rts} (lts : hlist ltype rts) i (lto lto' : ltype (lnth (unit : Type) rts i)) bmin0 :
+ Local Lemma struct_lift_place_cond_ty_homo {rts} (lts : hlist ltype rts) i (lto lto' : ltype (lnth (unit : Type) rts i)) bmin0 :
hnth (UninitLtype UnitSynType) lts i = lto →
i < length rts →
([∗ list] κ0 ∈ concat ((λ X : Type, ltype_blocked_lfts) +c<$> lts), bor_kind_outlives bmin0 κ0) -∗
@@ -2901,7 +3037,7 @@ Section rules.
{ eapply hcmap_lookup_hzipl. done. }
simpl. done.
Qed.
- Local Lemma struct_lift_place_cond_rfn_homo {rts} (rs : plist place_rfn rts) i (ro ro' : place_rfn (lnth (unit : Type) rts i)) bmin0 :
+ Local Lemma struct_lift_place_cond_rfn_homo {rts} (rs : plist place_rfn rts) i (ro ro' : place_rfn (lnth (unit : Type) rts i)) bmin0 :
pnth (#tt) rs i = ro →
i < length rts →
⊢@{iProp Σ} typed_place_cond_rfn bmin0 ro ro' -∗
@@ -2990,7 +3126,7 @@ Section rules.
iPoseProof ("Hc_close" with "Hb1 []") as "Hb".
{ rewrite -Hst2. done. }
iFrame.
- iMod ("Hcl" with "[] Hb") as "(Hb & _)".
+ iMod ("Hcl" with "[] Hb") as "Hb".
{ rewrite insert_length //. }
iFrame. iPureIntro. done.
- (* weak *)
@@ -3002,11 +3138,11 @@ Section rules.
iPoseProof ("Hc_close" with "Hb1") as "Hb".
iFrame "HL HR".
iDestruct "Hcond" as "(#Hcond_ty & Hcond_rfn)".
- iMod ("Hcl" with "[] [Hb]") as "(Hb & Hcond)".
+ iMod ("Hcl" with "[] [Hb]") as "Hb".
{ done. }
{ iApply "Hb". iPoseProof (typed_place_cond_ty_syn_type_eq with "Hcond_ty") as "<-". done. }
iFrame "Hb".
- iApply ("Hcond" with "[] [Hcond_rfn] []").
+ iApply (typed_place_cond_struct_lift with "[] [Hcond_rfn] []").
+ iApply (struct_lift_place_cond_ty_homo with "Houtl Hcond_ty"); [done | lia].
+ iApply (struct_lift_place_cond_rfn_homo with "Hcond_rfn"); [done | lia].
+ iPureIntro. clear. induction rts; simpl; first done.
@@ -3101,10 +3237,10 @@ Section rules.
iMod ("Hcl" with "[] [Hb] [] [] ") as "(Hb & Htoks & Hcond)".
{ done. }
{ iApply "Hb". iPoseProof (typed_place_cond_ty_syn_type_eq with "Hcond_ty") as "<-". done. }
- { iApply (struct_lift_place_cond_ty_homo with "Houtl Hcond_ty"); [done | lia]. }
+ { iApply (struct_lift_place_cond_ty_homo with "Houtl Hcond_ty"); [done | lia]. }
{ iApply (struct_lift_place_cond_rfn_homo with "Hcond_rfn"); [done | lia]. }
iFrame "Hb".
- rewrite llft_elt_toks_app. iFrame.
+ rewrite llft_elt_toks_app. iFrame.
iApply typed_place_cond_incl; last done.
iApply bor_kind_min_incl_r.
Qed.
@@ -3116,33 +3252,81 @@ Section rules.
(T : place_cont_t (plist place_rfn rts)) :
((* sidecondition for other components *)
⌜Forall (lctx_bor_kind_outlives E L bmin0) (concat ((λ _, ltype_blocked_lfts) +c<$> lts))⌠∗
- (* get lifetime token *)
- li_tactic (lctx_lft_alive_count_goal E L κ) (λ '(κs, L'),
(* recursively check place *)
(∃ i, ⌜sls_field_index_of sls.(sls_fields) f = Some i⌠∗
∃ lto (ro : place_rfn (lnth (unit : Type) rts i)),
⌜hnth (UninitLtype UnitSynType) lts i = lto⌠∗
⌜pnth (#tt) r i = ro⌠∗
typed_place π E L (l atst{sls}ₗ f) lto ro bmin0 (Shared κ) P
- (λ L' κs' l1 b2 bmin rti ltyi ri strong weak,
- T L' (κs ++ κs') l1 b2 bmin rti ltyi ri
- (* this should not require wrapping by Shadowed *)
- (fmap (λ strong, mk_strong
- (λ rt', plist place_rfn (<[i := strong.(strong_rt) rt']> rts))
- (λ rt' lt' r', StructLtype (hlist_insert rts lts i _ (strong.(strong_lt) _ lt' r')) sls)
- (λ rt' (r' : place_rfn rt'), #(plist_insert rts r i _ (strong.(strong_rfn) _ r')))
- strong.(strong_R)) strong)
+ (λ L' κs l1 b2 bmin rti ltyi ri strong weak,
+ T L' κs l1 b2 bmin rti ltyi ri
+ None (* TODO *)
+ (*(fmap (λ strong, mk_strong*)
+ (*(λ rt', plist place_rfn (<[i := strong.(strong_rt) rt']> rts))*)
+ (*(λ rt' lt' r', StructLtype (hlist_insert rts lts i _ (strong.(strong_lt) _ lt' r')) sls)*)
+ (*(λ rt' (r' : place_rfn rt'), #(plist_insert rts r i _ (strong.(strong_rfn) _ r')))*)
+ (*strong.(strong_R)) strong)*)
(fmap (λ weak, mk_weak
(λ lti2 ri2, StructLtype (hlist_insert_id (unit : Type) rts lts i (weak.(weak_lt) lti2 ri2)) sls)
(λ (r' : place_rfn rti), #(plist_insert_id (unit : Type) rts r i (weak.(weak_rfn) r')))
- weak.(weak_R)) weak)))))
+ weak.(weak_R)) weak))))
⊢ typed_place π E L l (StructLtype lts sls) (#r) bmin0 (Shared κ) (GetMemberPCtx sls f :: P) T.
Proof.
+ iIntros "(% & %i & %Hfield & %lto & %ro & %Hlto & %Hro & Hp)".
+ iIntros (Φ F ??) "#(LFT & TIME & LLCTX) #HE HL #Hincl0 Hl HΦ/=".
+ iPoseProof (struct_ltype_acc_shared F with "Hl") as "(%sl & %Halg & %Hly & %Hmem & #Hlb & Hb)"; first done.
+ iApply fupd_wp.
+ iMod (fupd_mask_mono with "Hb") as "(Hb & Hcl)"; first done.
+ iPoseProof (lctx_bor_kind_outlives_all_use with "[//] HE HL") as "#Houtl".
- (* TODO *)
- Admitted.
+ eapply (sls_field_index_of_lookup) in Hfield as (ly & Hfield).
+ assert (i < length rts)%nat. { rewrite -Hmem. eapply lookup_lt_Some. done. }
+ (* Note: if we later on want to allow the struct alg to change order of fields, then we need to change pad_struct (or use something else here), because it currently relies on the order of the types and the order of the sl members matching up *)
+ assert (field_index_of (sl_members sl) f = Some i) as Hfield'.
+ { eapply struct_layout_spec_has_layout_lookup; done. }
+ (*iApply (wp_logical_step with "TIME Hcl"); [done | solve_ndisj.. | ].*)
+ iApply (wp_get_member).
+ { apply val_to_of_loc. }
+ { done. }
+ { by eapply field_index_of_to_index_of. }
+ { done. }
+ iModIntro. iNext. iIntros "Hcred". iExists _. iR.
+ iPoseProof (focus_struct_component with "Hb") as "(%Heq & %ly' & %Hst & Hb & Hc_close)".
+ { done. }
+ { eapply (hnth_pnth_hpzipl_lookup _ (unit : Type) (UninitLtype UnitSynType) (PlaceIn ())); [ | done..].
+ eapply field_index_of_leq in Hfield'.
+ erewrite struct_layout_spec_has_layout_fields_length in Hfield'; last done. lia. }
+ assert (l at{sl}â‚— f = l atst{sls}â‚— f) as Hleq.
+ { rewrite /GetMemberLocSt /use_struct_layout_alg' Halg //. }
+ rewrite Hleq.
+ iApply ("Hp" with "[//] [//] [$LFT $TIME $LLCTX] HE HL Hincl0 [Hb]").
+ { rewrite -Hlto -Hro. done. }
+ iIntros (L' κs l2 b2 bmin rti ltyi ri strong weak) "#Hincl1 Hli Hcont".
+ iApply ("HΦ" $! _ _ _ _ _ _ _ _ _ _ with "Hincl1 Hli").
+ simpl. iSplit.
+ - (* strong *)
+ done.
+ - (* weak *)
+ destruct weak as [ weak | ]; last done.
+ iDestruct "Hcont" as "[_ Hcont]".
+ iIntros (ltyi2 ri2 bmin') "#Hincl2 Hli Hcond".
+ iMod ("Hcont" $! _ _ bmin' with "Hincl2 Hli Hcond") as "(Hb1 & Hcond & HL & HR)".
+ simpl. iDestruct "Hc_close" as "[_ Hc_close]".
+ iPoseProof ("Hc_close" with "Hb1") as "Hb".
+ iFrame "HL HR".
+ iDestruct "Hcond" as "(#Hcond_ty & Hcond_rfn)".
+ iMod ("Hcl" with "[] [Hb]") as "Hb".
+ { done. }
+ { iApply "Hb". iPoseProof (typed_place_cond_ty_syn_type_eq with "Hcond_ty") as "<-". done. }
+ iFrame "Hb".
+ iApply (typed_place_cond_struct_lift with "[] [Hcond_rfn] []").
+ + iApply (struct_lift_place_cond_ty_homo with "Houtl Hcond_ty"); [done | lia].
+ + iApply (struct_lift_place_cond_rfn_homo with "Hcond_rfn"); [done | lia].
+ + iPureIntro. clear. induction rts; simpl; first done.
+ constructor; first apply place_access_rt_rel_refl. done.
+ Qed.
Global Instance typed_place_struct_shared_inst π E L {rts} (lts : hlist ltype rts) (r : plist place_rfn rts) sls κ bmin0 f l P :
- TypedPlace E L π l (StructLtype lts sls) (PlaceIn r) bmin0 (Shared κ) (GetMemberPCtx sls f :: P) | 30 :=
+ TypedPlace E L π l (StructLtype lts sls) #r bmin0 (Shared κ) (GetMemberPCtx sls f :: P) | 30 :=
λ T, i2p (typed_place_struct_shared lts π E L r sls f κ bmin0 P l T).
Definition stratify_ltype_struct_iter_cont_t := llctx → iProp Σ → ∀ rts' : list Type, hlist ltype rts' → plist place_rfn rts' → iProp Σ.
@@ -3251,51 +3435,8 @@ Section rules.
However, at least these won't need typeclasses I guess, just need to extend the liRJudgment tactics.
*)
-
(* TODO: stratification instance for StructLtype with optional refolding *)
- (** Focus the initialized fields of a struct, disregarding the padding fields *)
- Lemma struct_ltype_focus_components π {rts : list Type} (lts : hlist ltype rts) (rs : plist place_rfn rts) sls sl k l :
- struct_layout_spec_has_layout sls sl →
- ([∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts lts rs) (λ ly : layout, existT (unit : Type) (UninitLtype (UntypedSynType ly), # ())),
- ∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗
- ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
- (l +â‚— offset_of_idx (sl_members sl) i) â—â‚—[ Ï€, k] (projT2 ty).2 @ (projT2 ty).1) -∗
- ([∗ list] i↦p ∈ hpzipl rts lts rs, let 'existT rt (lt, r) := p in ∃ (name : var_name) (st : syn_type), ⌜sls_fields sls !! i = Some (name, st)⌠∗ l atst{sls}â‚— name â—â‚—[ Ï€, k] r @ lt) ∗
- (∀ (rts' : list Type) (lts' : hlist ltype rts') rs',
- ([∗ list] p;p2 ∈ hpzipl rts lts rs;hpzipl rts' lts' rs', let 'existT rt (lt, _) := p in let 'existT rt' (lt', _) := p2 in ⌜ltype_st lt = ltype_st lt'âŒ) -∗
- ([∗ list] i↦p ∈ hpzipl rts' lts' rs', let 'existT rt (lt, r) := p in ∃ (name : var_name) (st : syn_type), ⌜sls_fields sls !! i = Some (name, st)⌠∗ l atst{sls}â‚— name â—â‚—[ Ï€, k] r @ lt) -∗
- ([∗ list] i↦ty ∈ pad_struct (sl_members sl) (hpzipl rts' lts' rs') (λ ly : layout, existT (unit : Type) (UninitLtype (UntypedSynType ly), # ())),
- ∃ ly : layout, ⌜snd <$> sl_members sl !! i = Some ly⌠∗
- ⌜syn_type_has_layout (ltype_st (projT2 ty).1) ly⌠∗
- (l +â‚— offset_of_idx (sl_members sl) i) â—â‚—[ Ï€, k] (projT2 ty).2 @ (projT2 ty).1)).
- Proof.
- (*
- iIntros (Halg) "Hl".
- iInduction rts as [ | rt rts] "IH"; inv_hlist lts; [ destruct rs | destruct rs as [r rs]]; simpl.
- { iR. iIntros (rts' lts' rs') "Hl'".
- iPoseProof (big_sepL2_length with "Hl'") as "%Hlen".
- rewrite hpzipl_length in Hlen. destruct rts'; last done.
- inv_hlist lts'. destruct rs'. simpl. iIntros "_".
- iFrame. }
- intros lt lts. simpl.
- rewrite pad_struct_cons
- *)
-
- (*
- clear -Hleneq. iInduction rts as [ | rt rts] "IH" forall (rts' lts' rs' i Hleneq); simpl; destruct rts' as [ | rt' rts']; try done;
- inv_hlist lts; inv_hlist lts'.
- { destruct rs, rs'; done. }
- intros lt' lts' lt lts.
- destruct rs as [r rs], rs' as [r' rs']; simpl.
- iDestruct "Ha" as "(Ha1 & Ha)".
- iDestruct "Hst" as "(%Hst & Hst)".
- iPoseProof ("IH" with "[] [Ha] Hst") as "?".
- { simpl in *. iPureIntro. lia. }
- {
- *)
- (* NOTE: need to generalize lemma about the initial index i in the induction to get sls stuff through *)
- Admitted.
Lemma stratify_ltype_struct_owned {rts} π E L mu mdu ma {M} (m : M) l (lts : hlist ltype rts) (rs : plist place_rfn rts) sls wl T :
stratify_ltype_struct_iter π E L mu mdu ma m l 0 sls lts rs (Owned false) (λ L2 R2 rts' lts' rs',
@@ -3306,7 +3447,7 @@ Section rules.
rewrite ltype_own_struct_unfold /struct_ltype_own.
iDestruct "Hl" as "(%sl & %Halg & %Hlen & %Hly & Hlb & Hcreds & %r' & <- & Hl)".
iMod (maybe_use_credit with "Hcreds Hl") as "(Hcred & Hat & Hl)"; first done.
- iPoseProof (struct_ltype_focus_components with "Hl") as "(Hl & Hlcl)"; first done.
+ iPoseProof (struct_ltype_focus_components with "Hl") as "(Hl & Hlcl)"; [done | done | ].
iMod ("HT" with "[//] [//] CTX HE HL [//] [] [] [Hl]") as "(%L2 & %R2 & %rts' & %lts' & %rs' & %Hleneq & Hst & Hstep & HL & HT)".
{ iPureIntro. lia. }
{ rewrite Hlen. done. }
@@ -3316,7 +3457,9 @@ Section rules.
iApply (logical_step_compose with "Hstep").
iApply (logical_step_intro_maybe with "Hat").
iIntros "Hcred2 !> (Ha & $)".
- iPoseProof ("Hlcl" $! rts' lts' rs' with "Hst [Ha]") as "Hl".
+ iPoseProof ("Hlcl" $! rts' lts' rs' with "[//] [Hst] [Ha]") as "Hl".
+ { iApply big_sepL2_Forall2.
+ iApply (big_sepL2_impl with "Hst"). iModIntro. iIntros (? [? []] [? []] ? ?); done. }
{ iApply (big_sepL_mono with "Ha"). intros ? [? []] ?. rewrite Nat.add_0_r. eauto. }
iModIntro.
rewrite ltype_own_struct_unfold /struct_ltype_own.
@@ -3343,7 +3486,7 @@ Section rules.
λ T, i2p (stratify_ltype_ofty_struct π E L mu ma ml l tys r sls b T).
(* needs to have lower priority than the id instance *)
- Lemma place_ofty_struct {rts} π E L l (tys : hlist type rts) (r : place_rfn (plist place_rfn rts)) sls bmin0 b P T :
+ Lemma typed_place_ofty_struct {rts} π E L l (tys : hlist type rts) (r : place_rfn (plist place_rfn rts)) sls bmin0 b P T :
typed_place π E L l (StructLtype (hmap (λ _, OfTy) tys) sls) r bmin0 b P T
⊢ typed_place π E L l (◠(struct_t sls tys)) r bmin0 b P T.
Proof.
@@ -3353,7 +3496,7 @@ Section rules.
Qed.
Global Instance typed_place_ofty_struct_inst {rts} π E L l (tys : hlist type rts) (r : place_rfn (plist place_rfn rts)) sls bmin0 b P :
TypedPlace E L π l (◠(struct_t sls tys))%I r bmin0 b P | 30 :=
- λ T, i2p (place_ofty_struct π E L l tys r sls bmin0 b P T).
+ λ T, i2p (typed_place_ofty_struct π E L l tys r sls bmin0 b P T).
(** Subtyping *)
(* TODO replace foldr with relate_hlist *)
diff --git a/theories/rust_typing/program_rules.v b/theories/rust_typing/program_rules.v
index 10b7da77db4dea3e9e26cbf11a312447fa49887c..5648160b6a21d4f8349c428b85aa5ba1be1a9f50 100644
--- a/theories/rust_typing/program_rules.v
+++ b/theories/rust_typing/program_rules.v
@@ -4,20 +4,6 @@ From refinedrust Require Import ltype_rules.
From caesium Require Import lang proofmode derived lifting.
Set Default Proof Using "Type".
- (* TODO move *)
- Lemma big_sepL_lft_incl_incl `{!typeGS Σ} E L κs κ :
- elctx_interp E -∗ llctx_interp L -∗
- ([∗ list] κ' ∈ κs, ⌜lctx_lft_incl E L κ' κâŒ) -∗
- ([∗ list] κ' ∈ κs, κ' ⊑ κ).
- Proof.
- iIntros "#HE HL #Hincl".
- iInduction κs as [ | κ' κs] "IH"; first done.
- simpl. iDestruct "Hincl" as "(%Hincl & Hincl)".
- iPoseProof (lctx_lft_incl_incl with "HL HE") as "#$"; first apply Hincl.
- iApply ("IH" with "Hincl HL").
- Qed.
-
-
Section typing.
Context `{typeGS Σ}.
(* NOTE: find_in_context instances should always have a sep conj in their premise, even if the LHS is just [True].
@@ -949,7 +935,7 @@ Section typing.
iIntros "HT". iIntros (F ??) "#CTX #HE HL Hl".
iMod ("HT" with "[//]") as "HT". iDestruct "HT" as "[(%r & Hobs & HT) | (-> & HT)]".
- rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hl" as "(%ly & ? & ? & ? & ? & ? & ? & Hrfn & Hb)".
+ iDestruct "Hl" as "(%ly & ? & ? & ? & ? & ? & Hrfn & Hb)".
iDestruct "Hrfn" as "(%v1 & %v2 & Hauth & Hobs' & %HR)".
iPoseProof (gvar_pobs_agree_2 with "Hauth Hobs") as "->".
simpl. subst.
diff --git a/theories/rust_typing/programs.v b/theories/rust_typing/programs.v
index 7d39f8a1908650503c9ff49458bd039c23933e97..278a00457e72a5207f7be63d0aca256177d00a92 100644
--- a/theories/rust_typing/programs.v
+++ b/theories/rust_typing/programs.v
@@ -4,340 +4,6 @@ From caesium Require Import lang proofmode derived lifting.
Set Default Proof Using "Type".
-
-
- (* TODO move *)
- Definition option_combine {A B} (a : option A) (b : option B) : option (A * B) :=
- match a, b with
- | Some a, Some b => Some (a, b)
- | _, _ => None
- end.
- Lemma option_combine_Some {A B} (a : option A) (b : option B) c :
- option_combine a b = Some c →
- ∃ a' b', a = Some a' ∧ b = Some b' ∧ c = (a', b').
- Proof.
- rewrite /option_combine. destruct a, b; naive_solver.
- Qed.
- Lemma option_combine_None {A B} (a : option A) (b : option B) :
- option_combine a b = None →
- a = None ∨ b = None.
- Proof.
- rewrite /option_combine. destruct a, b; naive_solver.
- Qed.
-
-
-
-(* TODO move *)
-Lemma val_of_bool_i2v b :
- val_of_bool b = i2v (bool_to_Z b) u8.
-Proof.
- apply val_of_bool_iff_val_of_Z.
- apply val_of_Z_bool.
-Qed.
-
-(* TODO: move *)
-Lemma lctx_bor_kind_incl_use `{!typeGS Σ} E L b1 b2 :
- lctx_bor_kind_incl E L b1 b2 →
- elctx_interp E -∗
- llctx_interp L -∗
- b1 ⊑ₖ b2.
-Proof.
- iIntros (Hincl) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- by iPoseProof (Hincl with "HL HE") as "Ha".
-Qed.
-
-Lemma lctx_bor_kind_direct_incl_use `{!typeGS Σ} E L b1 b2 :
- lctx_bor_kind_direct_incl E L b1 b2 →
- elctx_interp E -∗
- llctx_interp L -∗
- b1 ⊑ₛₖ b2.
-Proof.
- iIntros (Hincl) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- by iPoseProof (Hincl with "HL HE") as "Ha".
-Qed.
-
-(* TODO move *)
-Lemma subtype_acc `{!typeGS Σ} E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) :
- subtype E L r1 r2 ty1 ty2 →
- elctx_interp E -∗
- llctx_interp L -∗
- type_incl r1 r2 ty1 ty2.
-Proof.
- iIntros (Hsub) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
- iPoseProof (Hsub with "HL HE") as "#Hincl". done.
-Qed.
-Lemma full_subtype_acc `{!typeGS Σ} E L {rt} (ty1 : type rt) (ty2 : type rt) :
- full_subtype E L ty1 ty2 →
- elctx_interp E -∗
- llctx_interp L -∗
- ∀ r, type_incl r r ty1 ty2.
-Proof.
- iIntros (Hsub) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
- iIntros (?). iPoseProof (Hsub with "HL HE") as "#Hincl". done.
-Qed.
-Lemma full_subtype_acc_noend `{!typeGS Σ} E L {rt} (ty1 : type rt) (ty2 : type rt) qL :
- full_subtype E L ty1 ty2 →
- elctx_interp E -∗
- llctx_interp_noend L qL -∗
- ∀ r, type_incl r r ty1 ty2.
-Proof.
- iIntros (Hsub) "HE HL".
- iIntros (?). iPoseProof (Hsub with "HL HE") as "#Hincl". done.
-Qed.
-
-Lemma eqtype_acc `{!typeGS Σ} E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) :
- eqtype E L r1 r2 ty1 ty2 →
- elctx_interp E -∗
- llctx_interp L -∗
- type_incl r1 r2 ty1 ty2 ∗ type_incl r2 r1 ty2 ty1.
-Proof.
- iIntros ([Hsub1 Hsub2]) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
- iPoseProof (Hsub1 with "HL HE") as "#Hincl1".
- iPoseProof (Hsub2 with "HL HE") as "#Hincl2".
- iFrame "#".
-Qed.
-Lemma eqtype_acc_noend `{!typeGS Σ} E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) qL :
- eqtype E L r1 r2 ty1 ty2 →
- elctx_interp E -∗
- llctx_interp_noend L qL -∗
- type_incl r1 r2 ty1 ty2 ∗ type_incl r2 r1 ty2 ty1.
-Proof.
- iIntros ([Hsub1 Hsub2]) "HE HL".
- iPoseProof (Hsub1 with "HL HE") as "#Hincl1".
- iPoseProof (Hsub2 with "HL HE") as "#Hincl2".
- iFrame "#".
-Qed.
-Lemma full_eqtype_acc `{!typeGS Σ} E L {rt} (ty1 : type rt) (ty2 : type rt) :
- full_eqtype E L ty1 ty2 →
- elctx_interp E -∗
- llctx_interp L -∗
- ∀ r, type_incl r r ty1 ty2 ∗ type_incl r r ty2 ty1.
-Proof.
- iIntros (Heq) "HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
- iIntros (r). destruct (Heq r) as [Hsub1 Hsub2].
- iPoseProof (Hsub1 with "HL HE") as "#$".
- iPoseProof (Hsub2 with "HL HE") as "#$".
-Qed.
-Lemma full_eqtype_acc_noend `{!typeGS Σ} E L {rt} (ty1 : type rt) (ty2 : type rt) qL :
- full_eqtype E L ty1 ty2 →
- elctx_interp E -∗
- llctx_interp_noend L qL -∗
- ∀ r, type_incl r r ty1 ty2 ∗ type_incl r r ty2 ty1.
-Proof.
- iIntros (Heq) "HE HL".
- iIntros (r). destruct (Heq r) as [Hsub1 Hsub2].
- iPoseProof (Hsub1 with "HL HE") as "#$".
- iPoseProof (Hsub2 with "HL HE") as "#$".
-Qed.
-
-(* TODO move *)
-Lemma ltype_incl'_use `{!typeGS Σ} {rt1 rt2} F (lt1 : ltype rt1) (lt2 : ltype rt2) l π b r1 r2 :
- lftE ⊆ F →
- ltype_incl' b r1 r2 lt1 lt2 -∗
- l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗
- l â—â‚—[Ï€, b] r2 @ lt2.
-Proof.
- iIntros (?) "#Hincl Hl".
- iMod (fupd_mask_subseteq lftE) as "Hcl"; first done.
- destruct b.
- - iMod ("Hincl" with "Hl") as "$". by iMod "Hcl".
- - iMod "Hcl". iModIntro. by iApply "Hincl".
- - iMod "Hcl". iModIntro. by iApply "Hincl".
-Qed.
-Lemma ltype_incl_use `{!typeGS Σ} {rt1 rt2} π F b r1 r2 l (lt1 : ltype rt1) (lt2 : ltype rt2) :
- lftE ⊆ F →
- ltype_incl b r1 r2 lt1 lt2 -∗
- l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2.
-Proof.
- iIntros (?) "Hincl Ha".
- iDestruct "Hincl" as "(_ & #Hincl & _)".
- destruct b.
- - iApply (fupd_mask_mono with "(Hincl Ha)"); done.
- - by iApply "Hincl".
- - by iApply "Hincl".
-Qed.
-Lemma ltype_incl_use_core `{!typeGS Σ} {rt1 rt2} π F b r1 r2 l (lt1 : ltype rt1) (lt2 : ltype rt2) :
- lftE ⊆ F →
- ltype_incl b r1 r2 lt1 lt2 -∗
- l â—â‚—[Ï€, b] r1 @ ltype_core lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ ltype_core lt2.
-Proof.
- iIntros (?) "Hincl Ha".
- iDestruct "Hincl" as "(_ & _ & #Hincl)".
- destruct b.
- - iApply (fupd_mask_mono with "(Hincl Ha)"); done.
- - by iApply "Hincl".
- - by iApply "Hincl".
-Qed.
-
-
-(* TODO move *)
-Section subltype.
- Context `{!typeGS Σ}.
- Lemma subltype_use {rt1 rt2} F E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
- lftE ⊆ F →
- subltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- â–¡ ∀ Ï€ l, l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2.
- Proof.
- iIntros (? Hsubt) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
- iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
- iModIntro. iIntros (Ï€ l). iApply ltype_incl_use; done.
- Qed.
- Lemma subltype_use_core {rt1 rt2} F E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
- lftE ⊆ F →
- subltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- â–¡ ∀ Ï€ l, l â—â‚—[Ï€, b] r1 @ ltype_core lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ ltype_core lt2.
- Proof.
- iIntros (? Hsubt) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
- iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
- iModIntro. iIntros (Ï€ l). iApply ltype_incl_use_core; done.
- Qed.
-
- Lemma subltype_acc {rt1 rt2} E L b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
- subltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- ltype_incl b r1 r2 lt1 lt2.
- Proof.
- iIntros (Hsubt) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
- iPoseProof (Hsubt with "HL CTX HE") as "#Hincl". done.
- Qed.
- Lemma full_subltype_acc E L {rt} (lt1 lt2 : ltype rt) :
- full_subltype E L lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- ∀ b r, ltype_incl b r r lt1 lt2.
- Proof.
- iIntros (Hsubt) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & _)".
- iPoseProof (Hsubt with "HL CTX HE") as "#Hincl".
- iIntros (b r). iApply "Hincl".
- Qed.
-End subltype.
-
-
-(* TODO move *)
-Section eqltype.
- Context `{!typeGS Σ}.
- Lemma eqltype_use_noend F E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) qL l π :
- lftE ⊆ F →
- eqltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp_noend L qL -∗
- (l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2) ∗
- llctx_interp_noend L qL.
- Proof.
- iIntros (? Hunfold) "#CTX #HE HL".
- iPoseProof (Hunfold with "HL CTX HE") as "#Hll". iFrame.
- iIntros "Hl".
- iDestruct "Hll" as "((_ & #Ha & _) & _)".
- destruct b.
- - iMod (fupd_mask_subseteq lftE) as "Hcl"; first solve_ndisj.
- iMod ("Ha" with "Hl") as "$". by iMod "Hcl" as "_".
- - by iApply "Ha".
- - by iApply "Ha".
- Qed.
- Lemma eqltype_use F E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) l π :
- lftE ⊆ F →
- eqltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- (l â—â‚—[Ï€, b] r1 @ lt1 ={F}=∗ l â—â‚—[Ï€, b] r2 @ lt2) ∗
- llctx_interp L.
- Proof.
- iIntros (? Hunfold) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- iPoseProof (eqltype_use_noend with "CTX HE HL") as "($ & HL)"; [done.. | ].
- by iApply "HL_cl".
- Qed.
- Lemma eqltype_acc E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
- eqltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- ltype_eq b r1 r2 lt1 lt2.
- Proof.
- iIntros (Heq) "CTX HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- iApply (Heq with "HL CTX HE").
- Qed.
- Lemma full_eqltype_acc E L {rt} (lt1 lt2 : ltype rt) :
- full_eqltype E L lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- ∀ b r, ltype_eq b r r lt1 lt2.
- Proof.
- iIntros (Heq) "CTX HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- iApply (Heq with "HL CTX HE").
- Qed.
-
- Lemma all_ltype_eq_alt {rt} b (lt1 lt2 : ltype rt) :
- (∀ r, ltype_eq b r r lt1 lt2) ⊣⊢ (∀ r, ltype_incl b r r lt1 lt2) ∧ (∀ r, ltype_incl b r r lt2 lt1).
- Proof.
- iSplit.
- - iIntros "#Ha". iSplit; iIntros (r); iSpecialize ("Ha" $! r); iDestruct "Ha" as "[Ha Hb]"; done.
- - iIntros "#[Ha Hb]". iIntros (r). iSplit; done.
- Qed.
- Lemma full_eqltype_use F π E L {rt} b r (lt1 lt2 : ltype rt) l :
- lftE ⊆ F →
- full_eqltype E L lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- (l â—â‚—[ Ï€, b] r @ lt1 ={F}=∗ l â—â‚—[ Ï€, b] r @ lt2) ∗
- llctx_interp L.
- Proof.
- iIntros (? Heq) "#CTX #HE HL".
- iPoseProof (full_eqltype_acc with "CTX HE HL") as "#Heq"; [done | ].
- iFrame. iIntros "Hl". iDestruct ("Heq" $! _ _) as "[Hincl _]".
- by iApply (ltype_incl_use with "Hincl Hl").
- Qed.
-
- Lemma eqltype_syn_type_eq_noend E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) qL :
- eqltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp_noend L qL -∗
- ⌜ltype_st lt1 = ltype_st lt2âŒ.
- Proof.
- iIntros (Hunfold) "#CTX #HE HL".
- iPoseProof (Hunfold with "HL CTX HE") as "#Hll".
- iDestruct "Hll" as "((#$ & _) & _)".
- Qed.
- Lemma eqltype_syn_type_eq E L {rt1 rt2} b r1 r2 (lt1 : ltype rt1) (lt2 : ltype rt2) :
- eqltype E L b r1 r2 lt1 lt2 →
- rrust_ctx -∗
- elctx_interp E -∗
- llctx_interp L -∗
- ⌜ltype_st lt1 = ltype_st lt2âŒ.
- Proof.
- iIntros (Hunfold) "#CTX #HE HL".
- iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
- iPoseProof (eqltype_syn_type_eq_noend with "CTX HE HL") as "#$".
- done.
- Qed.
-End eqltype.
-
Section named_lfts.
Context `{typeGS Σ}.
(** [named_lfts] is a construct used by the automation to map annotated lifetime names to concrete Coq names.
@@ -438,12 +104,6 @@ Section credits.
iApply ("Hcl" $! 1%nat).
Qed.
-
- (* TODO move *)
- Lemma additive_time_receipt_succ n :
- atime (S n) ⊣⊢ atime 1 ∗ atime n.
- Proof. by rewrite -additive_time_receipt_sep. Qed.
-
Lemma credit_store_borrow_receipt (n m : nat) :
credit_store n m -∗
atime 1 ∗ (atime 1 -∗ credit_store n m).
@@ -499,20 +159,29 @@ Section credits.
rewrite -Nat.add_succ_r. rewrite additive_time_receipt_sep. iFrame.
Qed.
- (* TODO move *)
- Lemma lc_split_le (m n : nat) :
- m ≤ n →
- £ n -∗ £ m ∗ £ (n - m).
- Proof.
- intros ?. replace n with (m + (n - m))%nat by lia.
- replace (m + (n - m) - m)%nat with (n - m)%nat by lia.
- rewrite lc_split. auto.
- Qed.
End credits.
Section option_map.
Context `{!typeGS Σ}.
+ Definition option_combine {A B} (a : option A) (b : option B) : option (A * B) :=
+ match a, b with
+ | Some a, Some b => Some (a, b)
+ | _, _ => None
+ end.
+ Lemma option_combine_Some {A B} (a : option A) (b : option B) c :
+ option_combine a b = Some c →
+ ∃ a' b', a = Some a' ∧ b = Some b' ∧ c = (a', b').
+ Proof.
+ rewrite /option_combine. destruct a, b; naive_solver.
+ Qed.
+ Lemma option_combine_None {A B} (a : option A) (b : option B) :
+ option_combine a b = None →
+ a = None ∨ b = None.
+ Proof.
+ rewrite /option_combine. destruct a, b; naive_solver.
+ Qed.
+
Definition typed_option_map {A R} (o : option A) (Φ : A → (R → iProp Σ) → iProp Σ) (d : R) (T : R → iProp Σ) :=
match o with
| Some o => Φ o T
@@ -1340,7 +1009,7 @@ Section judgments.
Proof.
iIntros "Huniq". iSplit.
+ by iApply typed_place_cond_ty_refl.
- + destruct b => //.
+ + destruct b => //.
(*iExists eq_refl. done.*)
Qed.
@@ -1369,6 +1038,17 @@ Section judgments.
iIntros "(Ha & _)". by iApply typed_place_cond_ty_syn_type_eq.
Qed.
+ Lemma typed_place_cond_ty_uniq_core_eq {rt} (lt1 lt2 : ltype rt) κ γ :
+ typed_place_cond_ty (Uniq κ γ) lt1 lt2 -∗ ∀ b r, ltype_eq b r r (ltype_core lt1) (ltype_core lt2).
+ Proof.
+ iIntros "(%Heq & Ha & _)". rewrite (UIP_refl _ _ Heq). done.
+ Qed.
+ Lemma typed_place_cond_ty_uniq_unblockable {rt1 rt2} (lt1 : ltype rt1) (lt2 : ltype rt2) κ γ :
+ typed_place_cond_ty (Uniq κ γ) lt1 lt2 -∗ imp_unblockable [κ] lt2.
+ Proof.
+ iIntros "(%Heq & _ & Ha)". done.
+ Qed.
+
(* controls conditions on refinement type changes *)
Definition place_access_rt_rel (bmin : bor_kind) (rt1 rt2 : Type) :=
match bmin with
@@ -1390,7 +1070,7 @@ Section judgments.
Lemma typed_place_cond_rfn_refl b {rt} (r : place_rfn rt) :
⊢ typed_place_cond_rfn b r r.
Proof.
- destruct b => //.
+ destruct b => //.
(*iExists eq_refl. done.*)
Qed.
@@ -2232,15 +1912,6 @@ Section judgments.
Class ProveWithSubtype (E : elctx) (L : llctx) (step : bool) (pm : ProofMode) (P : iProp Σ) : Type :=
prove_with_subtype_proof T : iProp_to_Prop (prove_with_subtype E L step pm P T).
- (* TODO: move *)
- Lemma maybe_logical_step_compose (E : coPset) step (P Q : iProp Σ) :
- maybe_logical_step step E P -∗ maybe_logical_step step E (P -∗ Q) -∗ maybe_logical_step step E Q.
- Proof.
- iIntros "Ha Hb". destruct step; simpl.
- - iApply (logical_step_compose with "Ha Hb").
- - iMod "Ha". iMod "Hb". by iApply "Hb".
- Qed.
-
Lemma prove_with_subtype_sep E L step pm P1 P2 T :
prove_with_subtype E L step pm P1 (λ L' κs R1, prove_with_subtype E L' step pm P2 (λ L'' κs2 R2, T L'' (κs ++ κs2) (R1 ∗ R2)))
⊢ prove_with_subtype E L step pm (P1 ∗ P2) T.
@@ -2274,21 +1945,6 @@ Section judgments.
Global Instance prove_with_subtype_exists_inst {X} E L step pm (Φ : X → iProp Σ) : ProveWithSubtype E L step pm (∃ x, Φ x) :=
λ T, i2p (prove_with_subtype_exists E L step pm Φ T).
- (* TODO move *)
- Lemma imp_unblockable_use π F κs {rt} (lt : ltype rt) (r : place_rfn rt) l bk :
- lftE ⊆ F →
- imp_unblockable κs lt -∗
- lft_dead_list κs -∗
- l â—â‚—[Ï€, bk] r @ lt ={F}=∗ l â—â‚—[Ï€, bk] r @ ltype_core lt.
- Proof.
- iIntros (?) "(#Hub_uniq & #Hub_owned) Hdead Hl".
- destruct bk.
- - iMod (fupd_mask_mono with "(Hub_owned Hdead Hl)") as "Hl"; first done.
- rewrite ltype_own_core_equiv. done.
- - iApply (ltype_own_shared_to_core with "Hl").
- - iMod (fupd_mask_mono with "(Hub_uniq Hdead Hl)") as "Hl"; first done.
- rewrite ltype_own_core_equiv. done.
- Qed.
(** For ofty location ownership, we have special handling to stratify first, if possible.
This only happens in the [ProveWithStratify] proof mode though, because we sometimes directly want to get into [Subsume]. *)
@@ -2703,23 +2359,6 @@ Section judgments.
iSplitR; last done. by iRight.
Qed.
- (*
- match option_combine upd weak with
- | Some (Heq, weak) =>
- l â—â‚—[Ï€, b] (weak.(weak_rfn) (rew <- Heq in r2)) @ (weak.(weak_lt) (rew <- Heq in lt2)) -∗
- weak.(weak_R) (rew <- Heq in lt2) (rew <- Heq in r2) -∗
- introduce_with_hooks E L (R_weak ∗ R) T
- | None =>
- match strong with
- | Some strong =>
- l â—â‚—[Ï€, b] (strong.(strong_rfn) rti2 r2) @ (strong.(strong_lt) rti2 lt2) -∗
- strong.(strong_R) rti2 lt2 r2 -∗
- introduce_with_hooks E L R T
- | _ => False
- end
- end.
- *)
-
(** ** Read judgments *)
(* In a given lifetime context, we can read from [e], in the process determining that [e] reads from a location [l] and getting a value typed at a type [ty] with a layout compatible with [ot], and afterwards, the remaining [T L' v ty' r'] needs to be proved, where [ty'] is the new type of the read value and [v] is the read value.
diff --git a/theories/rust_typing/references.v b/theories/rust_typing/references.v
index aaf7433d413c6d7d45a2a9f60cc266fe263e0f82..e4385966a9124e52181b68b2e33dae3e6b759242 100644
--- a/theories/rust_typing/references.v
+++ b/theories/rust_typing/references.v
@@ -22,7 +22,7 @@ Section mut_ref.
loc_in_bounds l 0 ly.(ly_size) ∗
inner.(ty_sidecond) ∗
place_rfn_interp_mut r γ ∗
- £ num_cred ∗ atime 1 ∗
+ have_creds ∗
|={lftE}=> &pin{κ} (∃ r' : rt, gvar_auth γ r' ∗ |={lftE}=> l ↦: inner.(ty_own_val) π r'))%I;
ty_has_op_type ot mt := is_ptr_ot ot;
@@ -120,7 +120,6 @@ Section mut_ref.
iMod (bor_sep with "LFT Hb") as "(Ha & Hb)"; first solve_ndisj.
iMod (bor_persistent with "LFT Ha Htok_κ'") as "(>#Hsc & Htok_κ')"; first solve_ndisj.
iMod (bor_sep with "LFT Hb") as "(Hobs & Hb)"; first solve_ndisj.
- rewrite bi.sep_assoc.
iMod (bor_sep with "LFT Hb") as "(Hcred & Hb)"; first solve_ndisj.
iDestruct "Htok_κ'" as "(Htok_κ' & Htokc)".
iMod (bor_acc with "LFT Hcred Htokc") as "(>(Hcred & Hat) & Hclos_c)"; first solve_ndisj.
@@ -192,7 +191,7 @@ Section mut_ref.
iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Next Obligation.
- iIntros (??[r γ]???) "(%l & %ly & -> & _ & _ & _ & _ & Hrfn & Hcred & Hat & _)".
+ iIntros (??[r γ]???) "(%l & %ly & -> & _ & _ & _ & _ & Hrfn & Hcred & _)".
iApply fupd_logical_step. destruct r as [ r | γ'].
- iMod (gvar_obs_persist with "Hrfn") as "?".
iApply logical_step_intro. by iFrame.
@@ -221,7 +220,7 @@ Section subtype.
v â—áµ¥{Ï€} r @ mut_ref ty2 κ1.
Proof.
destruct r as [r γ].
- iIntros "#Hincl #Ht12 #Ht21 (%l & %ly & -> & ? & Hly & Hlb & Hsc & Hobs & ? & ? & Hb)".
+ iIntros "#Hincl #Ht12 #Ht21 (%l & %ly & -> & ? & Hly & Hlb & Hsc & Hobs & ? & Hb)".
iDestruct ("Ht12" $! inhabitant) as "(%Hst & #Hsceq & _)".
(*iDestruct "Ht21" as "(_ & _ & #Hv21 & #Hs21)".*)
iExists l, ly. iFrame. iSplitR; first done.
@@ -435,7 +434,7 @@ Section subltype.
Proof.
iIntros "#Heq #Hincl1 #Hincl2". iModIntro.
iIntros (Ï€ l). rewrite !ltype_own_mut_ref_unfold /mut_ltype_own /=.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)".
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)".
iExists ly. iFrame.
iMod "Hb". iModIntro. iApply (pinned_bor_iff with "[] [] Hb").
+ iNext. iModIntro. iSplit.
@@ -539,7 +538,7 @@ Section ltype_agree.
iMod "Hb" as "(%l' & Hl & Hb)".
iExists l'. iFrame.
rewrite ltype_own_ofty_unfold /lty_of_ty_own.
- iDestruct "Hb" as "(%ly' & ? & ? & Hsc & Hlb' & ? & ? & Hrfn' & Hb)".
+ iDestruct "Hb" as "(%ly' & ? & ? & Hsc & Hlb' & ? & Hrfn' & Hb)".
iExists l'. iFrame. iExists ly'. iSplitR; first done. iFrame "∗". done.
Qed.
Lemma mut_ref_unfold_1_uniq κ κ' γ r :
@@ -547,17 +546,17 @@ Section ltype_agree.
Proof.
iModIntro.
iIntros (Ï€ l). rewrite ltype_own_mut_ref_unfold /mut_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
- iIntros "(%ly & ? & %Hly & ? & ? & ? & ? & Hb)". iExists ly. iFrame "∗". iSplitR; first done.
+ iIntros "(%ly & ? & %Hly & ? & ? & ? & Hb)". iExists ly. iFrame "∗". iSplitR; first done.
iMod "Hb". iModIntro.
setoid_rewrite ltype_own_core_equiv. simp_ltypes.
iApply (pinned_bor_iff' with "[] Hb").
iNext. iModIntro. iSplit.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame. iMod "Hb" as "(%l' & Hl & Hb)".
iExists l'. iFrame. rewrite ltype_own_ofty_unfold /lty_of_ty_own. destruct r' as [r' γ'].
- iDestruct "Hb" as "(%ly' & Hst' & Hly' & Hsc & Hlb & ? & ? & Hrfn & >Hb)".
+ iDestruct "Hb" as "(%ly' & Hst' & Hly' & Hsc & Hlb & ? & Hrfn & >Hb)".
iModIntro. iExists l', ly'. iFrame "∗". iSplitR; first done. by iFrame.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame. iMod "Hb" as "(%v & Hl & Hb)". destruct r' as [r' γ'].
- iDestruct "Hb" as "(%l' & %ly' & -> & ? & ? & Hlb & Hsc & Hrfn & ? & ? & >Hb)".
+ iDestruct "Hb" as "(%l' & %ly' & -> & ? & ? & Hlb & Hsc & Hrfn & ? & >Hb)".
iExists _. iFrame. rewrite ltype_own_ofty_unfold /lty_of_ty_own.
iModIntro. iExists ly'. iFrame. done.
Qed.
@@ -598,7 +597,7 @@ Section ltype_agree.
iIntros "(%ly & ? & ? & _ & #Hlb & ? & %r' & Hrfn & Hb)". destruct r' as [r' γ'].
(*iApply except_0_if_intro.*)
iModIntro. iExists ly. iFrame "∗ #". iExists γ', r'. iFrame. iNext.
- iMod "Hb" as "(%v & Hl & %l' & %ly' & -> & ? & ? & #Hlb' & Hsc & ? & ? & Hrfn' & >Hb)".
+ iMod "Hb" as "(%v & Hl & %l' & %ly' & -> & ? & ? & #Hlb' & Hsc & ? & Hrfn' & >Hb)".
iExists _. iFrame. rewrite ltype_own_ofty_unfold /lty_of_ty_own. iExists ly'. iFrame "∗ #". done.
Qed.
Lemma mut_ref_unfold_2_uniq κ κ' γ r :
@@ -606,18 +605,18 @@ Section ltype_agree.
Proof.
iModIntro.
iIntros (Ï€ l). rewrite ltype_own_mut_ref_unfold /mut_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
- iIntros "(%ly & ? & ? & _ & Hlb & ? & ? & Hrfn & Hb)". iExists ly. iFrame "∗". iMod "Hb".
+ iIntros "(%ly & ? & ? & _ & Hlb & ? & Hrfn & Hb)". iExists ly. iFrame "∗". iMod "Hb".
iModIntro.
setoid_rewrite ltype_own_core_equiv. simp_ltypes.
iApply (pinned_bor_iff' with "[] Hb").
iNext. iModIntro. iSplit.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame. iMod "Hb" as "(%v & Hl & Hb)". destruct r' as [r' γ'].
- iDestruct "Hb" as "(%l' & %ly' & -> & ? & ? & Hlb & Hsc & Hrfn & ? & ? & >Hb)".
+ iDestruct "Hb" as "(%l' & %ly' & -> & ? & ? & Hlb & Hsc & Hrfn & ? & >Hb)".
iExists _. iFrame. rewrite ltype_own_ofty_unfold /lty_of_ty_own.
iModIntro. iExists ly'. iFrame. done.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame. iMod "Hb" as "(%l' & Hl & Hb)".
iExists l'. iFrame. rewrite ltype_own_ofty_unfold /lty_of_ty_own. destruct r' as [r' γ'].
- iDestruct "Hb" as "(%ly' & Hst' & Hly' & Hsc & Hlb & ? & ? & Hrfn & >Hb)".
+ iDestruct "Hb" as "(%ly' & Hst' & Hly' & Hsc & Hlb & ? & Hrfn & >Hb)".
iModIntro. iExists l', ly'. iFrame "∗". iSplitR; first done. by iFrame.
Qed.
Lemma mut_ref_unfold_2_shared κ κ' r :
@@ -690,12 +689,12 @@ Section rules.
iMod (maybe_use_credit with "Hcreds Hb") as "(Hcreds & Hat & Hb)"; first done.
iDestruct "Hb" as "(%v & Hl & Hb)".
rewrite /ty_own_val/=.
- iDestruct "Hb" as "(% & % & -> & ? & ? & ? & ? & Hb & Hcred' & Hat' & ?)".
+ iDestruct "Hb" as "(% & % & -> & ? & ? & ? & ? & Hb & Hcred' & ?)".
iFrame.
iSplitR. { simp_ltypes. done. }
rewrite ltype_own_ofty_unfold /lty_of_ty_own.
iExists _. simpl. iFrame. iR. iR.
- iSplitL "Hcred' Hat'". { destruct wl; last done. by iFrame. }
+ iSplitL "Hcred'". { destruct wl; last done. by iFrame. }
iExists _. iR. iModIntro. iModIntro. iModIntro.
iExists _. iFrame. rewrite uninit_own_spec. iExists _. iR.
iPureIntro. eapply syn_type_has_layout_ptr_inv in Hst. subst.
@@ -726,17 +725,17 @@ Section rules.
Lemma mut_ltype_acc_owned {rt} F π (lt : ltype rt) (r : place_rfn rt) l κ' γ' wl :
lftE ⊆ F →
rrust_ctx -∗
- l â—â‚—[Ï€, Owned wl] PlaceIn (r, γ') @ MutLtype lt κ' -∗
+ l â—â‚—[Ï€, Owned wl] #(r, γ') @ MutLtype lt κ' -∗
⌜l `has_layout_loc` void*⌠∗ loc_in_bounds l 0 (ly_size void*) ∗ |={F}=>
∃ l' : loc, l ↦ l' ∗ l' â—â‚—[Ï€, Uniq κ' γ'] r @ lt ∗
logical_step F
(∀ bmin rt' (lt2 : ltype rt') r2,
l ↦ l' -∗
l' â—â‚—[Ï€, Uniq κ' γ'] r2 @ lt2 ={F}=∗
- l â—â‚—[Ï€, Owned wl] PlaceIn (r2, γ') @ MutLtype lt2 κ' ∗
+ l â—â‚—[Ï€, Owned wl] #(r2, γ') @ MutLtype lt2 κ' ∗
(typed_place_cond bmin lt lt2 r r2 -∗
⌜place_access_rt_rel bmin rt rt'⌠-∗
- typed_place_cond bmin (MutLtype lt κ') (MutLtype lt2 κ') (PlaceIn (r, γ')) (PlaceIn (r2, γ')))).
+ typed_place_cond bmin (MutLtype lt κ') (MutLtype lt2 κ') (#(r, γ')) (#(r2, γ')))).
Proof.
iIntros (?) "#[LFT TIME] HP".
rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
@@ -764,7 +763,7 @@ Section rules.
rrust_ctx -∗
q.[κ] -∗
(q.[κ] ={lftE}=∗ R) -∗
- l â—â‚—[Ï€, Uniq κ γ] PlaceIn (r, γ') @ MutLtype lt κ' -∗
+ l â—â‚—[Ï€, Uniq κ γ] #(r, γ') @ MutLtype lt κ' -∗
⌜l `has_layout_loc` void*⌠∗ loc_in_bounds l 0 (ly_size void*) ∗ |={F}=>
∃ l' : loc, l ↦ l' ∗ (l' â—â‚—[Ï€, Uniq κ' γ'] r @ lt) ∗
logical_step F
@@ -787,7 +786,7 @@ Section rules.
Proof.
iIntros (?) "#[LFT TIME] Hκ HR HP".
rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
- iDestruct "HP" as "(%ly & %Halg & %Hly & #Hlb & Hcred & Hat & Hrfn & Hb)".
+ iDestruct "HP" as "(%ly & %Halg & %Hly & #Hlb & (Hcred & Hat) & Hrfn & Hb)".
injection Halg as <-. iFrame "Hlb". iSplitR; first done.
iMod (fupd_mask_subseteq lftE) as "Hcl_F"; first done.
@@ -877,13 +876,48 @@ Section rules.
iExists _, r2. iR. iNext. iModIntro. eauto with iFrame. }
Qed.
- (* TODO : shared *)
-
+ Lemma mut_ltype_acc_shared {rt} F π (lt : ltype rt) r l q κ κ' γ :
+ lftE ⊆ F →
+ rrust_ctx -∗
+ q.[κ] -∗
+ l â—â‚—[Ï€, Shared κ] #(r, γ) @ MutLtype lt κ' -∗
+ ⌜l `has_layout_loc` void*⌠∗ loc_in_bounds l 0 (ly_size void*) ∗ |={F}=>
+ ∃ (l' : loc) q', l ↦{q'} l' ∗ (|={F}â–·=> l' â—â‚—[Ï€, Shared (κ' ⊓ κ)] r @ lt) ∗
+ (∀ (lt' : ltype rt) r',
+ l ↦{q'} l' -∗
+ l' â—â‚—[Ï€, Shared (κ' ⊓ κ)] r' @ lt' -∗ |={F}=>
+ l â—â‚—[Ï€, Shared κ] #(r', γ) @ MutLtype lt' κ' ∗
+ q.[κ] ∗
+ (∀ bmin,
+ bmin ⊑ₖ Shared κ -∗
+ typed_place_cond bmin lt lt' r r' ={F}=∗
+ typed_place_cond bmin (MutLtype lt κ') (MutLtype lt' κ') #(r, γ) #(r', γ))).
+ Proof.
+ iIntros (?) "#(LFT & TIME & LLCTX) Hκ Hb". rewrite {1}ltype_own_mut_ref_unfold /mut_ltype_own.
+ iDestruct "Hb" as "(%ly & %Hst & %Hly & #Hlb & %r' & %γ' & %Ha & #Hb)".
+ injection Ha as <- <-.
+ apply syn_type_has_layout_ptr_inv in Hst. subst ly.
+ iR. iR.
+ iMod (fupd_mask_mono with "Hb") as "(%li & #Hf & #Hl)"; first done.
+ iMod (frac_bor_acc with "LFT Hf Hκ") as "(%q' & >Hpts & Hclf)"; first done.
+ iModIntro. iExists _, _. iFrame.
+ iSplitR. { iApply step_fupd_intro; first done. auto. }
+ iIntros (lt' r'') "Hpts #Hl'".
+ iMod ("Hclf" with "Hpts") as "Htok".
+ iFrame. iSplitL.
+ { iModIntro. rewrite ltype_own_mut_ref_unfold /mut_ltype_own. iExists void*. iFrame "% #".
+ iR. iExists _, _. iR. iModIntro. iModIntro. iExists _. iFrame "#". }
+ iModIntro. iIntros (bmin) "Hincl Hcond".
+ iDestruct "Hcond" as "(Hcond_ty & Hcond_rfn)".
+ iModIntro. iSplit.
+ + iApply mut_ltype_place_cond_ty; done.
+ + destruct bmin; simpl; done.
+ Qed.
(** Place *)
(* This needs to have a lower priority than the id instances, because we do not want to unfold when P = []. *)
- Lemma place_ofty_mut {rt} `{Inhabited rt} π E L l (ty : type rt) κ (r : place_rfn (place_rfn rt * gname)) bmin0 b P T :
+ Lemma typed_place_ofty_mut {rt} `{Inhabited rt} π E L l (ty : type rt) κ (r : place_rfn (place_rfn rt * gname)) bmin0 b P T :
typed_place π E L l (MutLtype (◠ty) κ) r bmin0 b P T
⊢ typed_place π E L l (◠(mut_ref ty κ)) r bmin0 b P T.
Proof.
@@ -892,7 +926,7 @@ Section rules.
iApply ltype_eq_sym. iApply mut_ref_unfold.
Qed.
Global Instance typed_place_ofty_mut_inst {rt} `{Inhabited rt} π E L l (ty : type rt) κ (r : place_rfn (place_rfn rt * gname)) bmin0 b P :
- TypedPlace E L π l (◠(mut_ref ty κ))%I r bmin0 b P | 30 := λ T, i2p (place_ofty_mut π E L l ty κ r bmin0 b P T).
+ TypedPlace E L π l (◠(mut_ref ty κ))%I r bmin0 b P | 30 := λ T, i2p (typed_place_ofty_mut π E L l ty κ r bmin0 b P T).
Lemma typed_place_mut_owned {rto} π κ (lt2 : ltype rto) P E L γ l r wl bmin0
(T : place_cont_t ((place_rfn rto) * gname)) :
@@ -1008,23 +1042,60 @@ Section rules.
Global Instance typed_place_mut_uniq_inst {rto} E L π κ κ' γ γ' (lt2 : ltype rto) bmin0 r l P :
TypedPlace E L π l (MutLtype lt2 κ) (#(r, γ)) bmin0 (Uniq κ' γ') (DerefPCtx Na1Ord PtrOp true :: P) | 30 := λ T, i2p (typed_place_mut_uniq π E L lt2 P l r κ γ κ' γ' bmin0 T).
- (* TODO: shared. can also do strong updates due to ShadowedLtype
- Lemma place_mut_shared {rto} π E L κ κ' (lt2 : ltype rto) P γ l bmin0 r
- (T : llctx → list lft → loc → bor_kind → bor_kind → ∀ rti, ltype rti → place_rfn rti → (ltype rti → ltype (place_rfn rto * gname)) → (place_rfn rti → place_rfn ((place_rfn rto) * gname)) → (ltype rti → place_rfn rti → iProp Σ) → iProp Σ) :
- (* get lifetime token *)
+ Lemma typed_place_mut_shared {rto} π E L (lt2 : ltype rto) P l r κ γ κ' bmin0 (T : place_cont_t (place_rfn rto * gname)) :
li_tactic (lctx_lft_alive_count_goal E L κ') (λ '(κs, L'),
- (* recursively check the place *)
- (∀ l', typed_place π E L' l' lt2 r (Uniq κ γ ⊓ₖ bmin0) (Uniq κ γ) P
- (λ L'' κs' l2 b2 bmin rti tyli ri (tylp : ltype rti → ltype rto) (rctx : place_rfn rti → place_rfn rto) R,
- T L'' (κs ++ κs') l2 b2 (Shared κ' ⊓ₖ bmin) rti tyli ri ((λ lt, MutLtype lt κ) ∘ tylp) (λ (r : place_rfn rti), PlaceIn (rctx r, γ)) R))) -∗
- typed_place π E L l (MutLtype lt2 κ) (#(r, γ)) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp :: P) T.
+ (∀ l', typed_place π E L' l' lt2 r (Shared (κ ⊓ κ') ⊓ₖ bmin0) (Shared (κ ⊓ κ')) P
+ (λ L'' κs' l2 b2 bmin rti tyli ri strong weak,
+ T L'' (κs ++ κs') l2 b2 (Shared κ' ⊓ₖ bmin) rti tyli ri
+ (* strong branch: fold to ShadowedLtype *)
+ None (* TODO *)
+ (*(fmap (λ strong, mk_strong (λ rti, (place_rfn (strong.(strong_rt) rti) * gname)%type)*)
+ (*(λ rti2 ltyi2 ri2,*)
+ (*OpenedLtype (MutLtype (strong.(strong_lt) _ ltyi2 ri2) κ) (MutLtype lt2 κ) (MutLtype lt2 κ) (λ r1 r1', ⌜r1 = r1'âŒ) (λ _ _, llft_elt_toks κs))*)
+ (*(λ rti2 ri2, #((strong.(strong_rfn) _ ri2), γ))*)
+ (*strong.(strong_R)) strong)*)
+ (* weak branch: just keep the MutLtype *)
+ (fmap (λ weak, mk_weak (λ lti' ri', MutLtype (weak.(weak_lt) lti' ri') κ) (λ (r : place_rfn rti), #(weak.(weak_rfn) r, γ)) weak.(weak_R)) weak))))
+ ⊢ typed_place π E L l (MutLtype lt2 κ) #(r, γ) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp true :: P) T.
Proof.
- (* TODO *)
- Admitted.
+ rewrite /lctx_lft_alive_count_goal.
+ iIntros "(%κs & %L2 & %Hal & HT)".
+ iIntros (Φ F ??). iIntros "#(LFT & TIME & LLCTX) #HE HL #Hincl0 HP HΦ/=".
+ (* get a token *)
+ iApply fupd_wp. iMod (fupd_mask_subseteq lftE) as "HclF"; first done.
+ iMod (lctx_lft_alive_count_tok lftE with "HE HL") as (q) "(Hκ' & Hclκ' & HL)"; [done.. | ].
+ iMod "HclF" as "_". iMod (fupd_mask_subseteq F) as "HclF"; first done.
+ iPoseProof (mut_ltype_acc_shared F with "[$LFT $TIME $LLCTX] Hκ' HP") as "(%Hly & Hlb & Hb)"; [done.. | ].
+ iMod "Hb" as "(%l' & %q' & Hl & >Hb & Hcl)". iMod "HclF" as "_".
+ iModIntro. iApply wp_fupd. iApply (wp_deref with "Hl") => //; [solve_ndisj | by apply val_to_of_loc | ].
+ iNext.
+ iIntros (st) "Hl Hcred". iMod (fupd_mask_mono with "Hb") as "#Hb"; first done.
+ iExists l'.
+ iSplitR. { iPureIntro. unfold mem_cast. rewrite val_to_of_loc. done. }
+ iApply ("HT" with "[//] [//] [$LFT $TIME $LLCTX] HE HL [] Hb"). { iApply bor_kind_min_incl_l. }
+ iModIntro. iIntros (L'' κs' l2 b2 bmin rti tyli ri strong weak) "#Hincl1 Hb' Hs".
+ iApply ("HΦ" $! _ _ _ _ (Shared κ' ⊓ₖ bmin) _ _ _ _ _ with "[Hincl1] Hb'").
+ { iApply bor_kind_incl_trans; last iApply "Hincl1". iApply bor_kind_min_incl_r. }
+ simpl. iSplit.
+ - (* strong update *)
+ done.
+ - (* weak update *)
+ destruct weak as [ weak | ]; last done.
+ iDestruct "Hs" as "(_ & Hs)".
+ iIntros (ltyi2 ri2 bmin') "#Hincl2 Hl2 Hcond".
+ iMod ("Hs" with "[Hincl2] Hl2 Hcond") as "(Hb' & Hcond & ? & HR)".
+ { iApply bor_kind_incl_trans; first iApply "Hincl2". iApply bor_kind_min_incl_r. }
+ simpl.
+ iMod ("Hcl" with "Hl Hb'") as "(Hb' & Hκ' & Hcond')".
+ iFrame. rewrite llft_elt_toks_app.
+ iMod (fupd_mask_mono with "(Hclκ' Hκ')") as "?"; first done.
+ iFrame. iApply "Hcond'".
+ + done.
+ + iApply typed_place_cond_incl; last done.
+ iApply bor_kind_min_incl_r.
+ Qed.
Global Instance typed_place_mut_shared_inst {rto} E L π κ κ' γ (lt2 : ltype rto) bmin0 r l P :
- TypedPlace E L π l (MutLtype lt2 κ) (PlaceIn (r, γ)) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp :: P) | 30 := λ T, i2p (place_mut_shared π E L κ κ' lt2 P γ l bmin0 r T).
- *)
-
+ TypedPlace E L π l (MutLtype lt2 κ) (#(r, γ)) bmin0 (Shared κ') (DerefPCtx Na1Ord PtrOp true :: P) | 30 := λ T, i2p (typed_place_mut_shared π E L lt2 P l r κ γ κ' bmin0 T).
(** Stratification *)
Lemma stratify_ltype_mut_owned {rt} π E L mu mdu ma {M} (ml : M) l (lt : ltype rt) κ (r : (place_rfn rt)) wl γ
@@ -1201,7 +1272,7 @@ Section rules.
find_observation (place_rfn rt * gname) γ FindObsModeDirect (λ or,
match or with
| None => ⌜rm = ResolveTry⌠∗ T L (PlaceGhost γ) True false
- | Some r => T L (PlaceIn $ r) True true
+ | Some r => T L #r True true
end)
⊢ resolve_ghost π E L rm lb l (MutLtype lt κ) (Owned wl) (PlaceGhost γ) T.
Proof.
@@ -1224,7 +1295,7 @@ Section rules.
find_observation (place_rfn rt * gname) γ FindObsModeDirect (λ or,
match or with
| None => ⌜rm = ResolveTry⌠∗ T L (PlaceGhost γ) True false
- | Some r => T L (PlaceIn $ r) True true
+ | Some r => T L #r True true
end)
⊢ resolve_ghost π E L rm lb l (MutLtype lt κ) (Uniq κ' γ') (PlaceGhost γ) T.
Proof.
@@ -1232,10 +1303,9 @@ Section rules.
iIntros "HT". iIntros (F ??) "#CTX #HE HL Hb".
iMod ("HT" with "[//]") as "HT". iDestruct "HT" as "[(%r & Hobs & HT) | (-> & HT)]".
- rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
- iDestruct "Hb" as "(%ly & %Hst & %Hly & ? & ? & ? & Hrfn & ?)".
+ iDestruct "Hb" as "(%ly & %Hst & %Hly & ? & ? & Hrfn & ?)".
simpl.
- iDestruct "Hrfn" as "(%r0 & %r1 & Ha1 & Ha2 & %Heq)".
- iPoseProof (gvar_pobs_agree_2 with "Ha1 Hobs") as "%". subst.
+ iPoseProof (Rel2_use_pobs with "Hobs Hrfn") as "(%r2 & Hobs & ->)".
iModIntro. iExists _, _, _,_. iFrame. iApply maybe_logical_step_intro.
iL. rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
iExists _. iFrame. done.
@@ -1244,6 +1314,29 @@ Section rules.
Global Instance resolve_ghost_mut_uniq_inst {rt} π E L l (lt : ltype rt) κ γ κ' γ' rm lb :
ResolveGhost π E L rm lb l (MutLtype lt κ) (Uniq κ' γ') (PlaceGhost γ) | 7 := λ T, i2p (resolve_ghost_mut_Uniq π E L l lt γ rm lb κ κ' γ' T).
+ Lemma resolve_ghost_mut_shared {rt} π E L l (lt : ltype rt) γ rm lb κ κ' T :
+ find_observation (place_rfn rt * gname) γ FindObsModeDirect (λ or,
+ match or with
+ | None => ⌜rm = ResolveTry⌠∗ T L (PlaceGhost γ) True false
+ | Some r => T L #r True true
+ end)
+ ⊢ resolve_ghost π E L rm lb l (MutLtype lt κ) (Shared κ') (PlaceGhost γ) T.
+ Proof.
+ rewrite /FindOptGvarPobs /=.
+ iIntros "HT". iIntros (F ??) "#CTX #HE HL Hb".
+ iMod ("HT" with "[//]") as "HT". iDestruct "HT" as "[(%r & Hobs & HT) | (-> & HT)]".
+ - rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
+ iDestruct "Hb" as "(%ly & %Hst & %Hly & ? & %γ0 & %r'& Hrfn & ?)".
+ simpl.
+ iPoseProof (gvar_pobs_agree_2 with "Hrfn Hobs") as "%Heq". subst r.
+ iModIntro. iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+ iL. rewrite ltype_own_mut_ref_unfold /mut_ltype_own.
+ iExists _. iFrame. do 2 iR. iExists _, _. iR. iFrame.
+ - iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro. by iFrame.
+ Qed.
+ Global Instance resolve_ghost_mut_shared_inst {rt} π E L l (lt : ltype rt) κ γ κ' rm lb :
+ ResolveGhost π E L rm lb l (MutLtype lt κ) (Shared κ') (PlaceGhost γ) | 7 := λ T, i2p (resolve_ghost_mut_shared π E L l lt γ rm lb κ κ' T).
+
(** cast_ltype *)
Lemma cast_ltype_to_type_mut E L {rt} `{Inhabited rt} (lt : ltype rt) κ T :
cast_ltype_to_type E L lt (λ ty, T (mut_ref ty κ))
@@ -1866,7 +1959,7 @@ Section subltype.
Proof.
iIntros "#Heq #Hincl1 #Hincl2". iModIntro.
iIntros (Ï€ l). rewrite !ltype_own_shr_ref_unfold /shr_ltype_own.
- iIntros "(%ly & ? & ? & Hlb & ? & ? & Hrfn & Hb)".
+ iIntros "(%ly & ? & ? & Hlb & ? & Hrfn & Hb)".
iExists ly. iFrame. rewrite -?Hly_eq. iFrame.
iMod "Hb". iModIntro. iApply (pinned_bor_iff with "[] [] Hb").
+ iNext. iModIntro. iSplit.
@@ -1986,7 +2079,7 @@ Section ltype_agree.
⊢ ltype_incl' (Uniq κ' γ) r r (ShrLtype (◠ty) κ) (◠(shr_ref ty κ)).
Proof.
iModIntro. iIntros (Ï€ l). rewrite ltype_own_shr_ref_unfold /shr_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
- iIntros "(%ly & ? & ? & ? & ? & ? & ? & Hb)". iExists ly. iFrame. iMod "Hb". iModIntro.
+ iIntros "(%ly & ? & ? & ? & ? & ? & Hb)". iExists ly. iFrame. iMod "Hb". iModIntro.
iApply (pinned_bor_iff' with "[] Hb").
iNext. iModIntro. iSplit.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame.
@@ -2046,7 +2139,7 @@ Section ltype_agree.
Proof.
iModIntro. iIntros (Ï€ l). rewrite ltype_own_shr_ref_unfold /shr_ltype_own ltype_own_ofty_unfold /lty_of_ty_own.
(* same proof as above essentially *)
- iIntros "(%ly & ? & ? & Hsc & ? & ? & ? & ? & Hb)". iExists ly. iFrame. iMod "Hb". iModIntro.
+ iIntros "(%ly & ? & ? & Hsc & ? & ? & ? & Hb)". iExists ly. iFrame. iMod "Hb". iModIntro.
iApply (pinned_bor_iff' with "[] Hb").
iNext. iModIntro. iSplit.
* iIntros "(%r' & Hauth & Hb)". iExists _. iFrame.
diff --git a/theories/rust_typing/shims.v b/theories/rust_typing/shims.v
index 8069d64b819bfbcc8b9167cab70d0cf7a424c5b8..2fbc066a5231ec3047096cd470cf7ce669ad7413 100644
--- a/theories/rust_typing/shims.v
+++ b/theories/rust_typing/shims.v
@@ -255,7 +255,9 @@ Proof.
(* turn it into arrays *)
iPoseProof (ofty_value_t_untyped_to_array with "Hs") as "Hs".
+ { by eapply syn_type_has_layout_make_untyped. }
iPoseProof (ofty_value_t_untyped_to_array with "Ht") as "Ht".
+ { by eapply syn_type_has_layout_make_untyped. }
iModIntro.
set (loop_inv := (λ (E : elctx) (L : llctx),
@@ -280,7 +282,9 @@ Proof.
assert (take i (reshape (replicate len (ly_size T_st_ly)) v_s) ++ drop i (reshape (replicate len (ly_size T_st_ly)) v_t) = (reshape (replicate len (ly_size T_st_ly)) (take (i * ly_size T_st_ly) v_s ++ drop (i * ly_size T_st_ly) v_t))) as ->.
{ shelve. }
iPoseProof (ofty_value_t_untyped_from_array with "Hs") as "Hs".
+ { rewrite Hlen_s ly_size_mk_array_layout. lia. }
iPoseProof (ofty_value_t_untyped_from_array with "Ht") as "Ht".
+ { rewrite app_length take_length drop_length. rewrite Hlen_t Hlen_s !ly_size_mk_array_layout. lia. }
iApply typed_stmt_annot_skip.
repeat liRStep; liShow.
diff --git a/theories/rust_typing/type.v b/theories/rust_typing/type.v
index c7f9610430941263ee7157aafcbf0cec544cfd75..84e4dd0582cd38ee5579c513d95ad74f7ac24ef1 100644
--- a/theories/rust_typing/type.v
+++ b/theories/rust_typing/type.v
@@ -742,21 +742,35 @@ Section subtyping.
intros ??????. by eapply subtype_trans.
Qed.
- (*
- Lemma full_subtype_Forall2_llctx E L {rt} (tys1 tys2 : list (type rt)) qL :
- Forall2 (full_subtype E L) tys1 tys2 →
- llctx_interp_noend L qL -∗ (elctx_interp E -∗
- [∗ list] tys ∈ (zip tys1 tys2), ∀ r, type_incl r r (tys.1) (tys.2)).
+ Lemma subtype_acc E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) :
+ subtype E L r1 r2 ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ type_incl r1 r2 ty1 ty2.
Proof.
- iIntros (Htys) "HL #HE".
- iAssert ([∗ list] tys ∈ zip tys1 tys2,
- □ (llctx_interp_noend L qL -∗ ∀ r, type_incl r r (tys.1) (tys.2)))%I as "#Htys".
- { iApply big_sepL_forall. iIntros (k [ty1 ty2] Hlookup).
- move:Htys => /Forall2_Forall /Forall_forall=>Htys.
- iIntros "!> HL" (r).
- iApply (Htys (ty1, ty2) with "HL"); first by exact: elem_of_list_lookup_2. done. }
+ iIntros (Hsub) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
+ iPoseProof (Hsub with "HL HE") as "#Hincl". done.
+ Qed.
+ Lemma full_subtype_acc E L {rt} (ty1 : type rt) (ty2 : type rt) :
+ full_subtype E L ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ∀ r, type_incl r r ty1 ty2.
+ Proof.
+ iIntros (Hsub) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
+ iIntros (?). iPoseProof (Hsub with "HL HE") as "#Hincl". done.
+ Qed.
+ Lemma full_subtype_acc_noend E L {rt} (ty1 : type rt) (ty2 : type rt) qL :
+ full_subtype E L ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp_noend L qL -∗
+ ∀ r, type_incl r r ty1 ty2.
+ Proof.
+ iIntros (Hsub) "HE HL".
+ iIntros (?). iPoseProof (Hsub with "HL HE") as "#Hincl". done.
Qed.
- *)
Lemma equiv_full_subtype E L {rt} (ty1 ty2 : type rt) : ty1 ≡ ty2 → full_subtype E L ty1 ty2.
Proof. unfold subtype=>EQ ? ?. setoid_rewrite EQ. apply subtype_refl. Qed.
@@ -889,4 +903,53 @@ Section subtyping.
Proof.
iIntros (Heq r). destruct (Heq r) as [Ha Hb]. done.
Qed.
+
+ Lemma eqtype_acc E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) :
+ eqtype E L r1 r2 ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ type_incl r1 r2 ty1 ty2 ∗ type_incl r2 r1 ty2 ty1.
+ Proof.
+ iIntros ([Hsub1 Hsub2]) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
+ iPoseProof (Hsub1 with "HL HE") as "#Hincl1".
+ iPoseProof (Hsub2 with "HL HE") as "#Hincl2".
+ iFrame "#".
+ Qed.
+ Lemma eqtype_acc_noend E L {rt1 rt2} r1 r2 (ty1 : type rt1) (ty2 : type rt2) qL :
+ eqtype E L r1 r2 ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp_noend L qL -∗
+ type_incl r1 r2 ty1 ty2 ∗ type_incl r2 r1 ty2 ty1.
+ Proof.
+ iIntros ([Hsub1 Hsub2]) "HE HL".
+ iPoseProof (Hsub1 with "HL HE") as "#Hincl1".
+ iPoseProof (Hsub2 with "HL HE") as "#Hincl2".
+ iFrame "#".
+ Qed.
+ Lemma full_eqtype_acc E L {rt} (ty1 : type rt) (ty2 : type rt) :
+ full_eqtype E L ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp L -∗
+ ∀ r, type_incl r r ty1 ty2 ∗ type_incl r r ty2 ty1.
+ Proof.
+ iIntros (Heq) "HE HL".
+ iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & Hcl_L)".
+ iIntros (r). destruct (Heq r) as [Hsub1 Hsub2].
+ iPoseProof (Hsub1 with "HL HE") as "#$".
+ iPoseProof (Hsub2 with "HL HE") as "#$".
+ Qed.
+ Lemma full_eqtype_acc_noend E L {rt} (ty1 : type rt) (ty2 : type rt) qL :
+ full_eqtype E L ty1 ty2 →
+ elctx_interp E -∗
+ llctx_interp_noend L qL -∗
+ ∀ r, type_incl r r ty1 ty2 ∗ type_incl r r ty2 ty1.
+ Proof.
+ iIntros (Heq) "HE HL".
+ iIntros (r). destruct (Heq r) as [Hsub1 Hsub2].
+ iPoseProof (Hsub1 with "HL HE") as "#$".
+ iPoseProof (Hsub2 with "HL HE") as "#$".
+ Qed.
+
+
End subtyping.
diff --git a/theories/rust_typing/util.v b/theories/rust_typing/util.v
index 613cff7005f46cc1e30dd2a3acbfcf75fe4de9e7..20a2ee8c0f8e3b81fa4de16476ff91fe0bae4319 100644
--- a/theories/rust_typing/util.v
+++ b/theories/rust_typing/util.v
@@ -145,6 +145,13 @@ Proof.
rewrite drop_length. lia.
Qed.
+Lemma reshape_replicate_0 {A} (xs : list A) n :
+ reshape (replicate n 0) xs = replicate n [].
+Proof.
+ induction n as [ | n IH]; simpl; first done.
+ rewrite take_0 drop_0. f_equiv. apply IH.
+Qed.
+
Section Forall.
(** Recursive version of Forall, to make it computational and eligible for recursive definitions. *)
Context {X} (P : X → Prop).
@@ -189,6 +196,15 @@ Proof.
- intros Hel i x Hlook%elem_of_list_lookup_2. eauto.
Qed.
+Lemma Forall2_eq {A} (l1 l2 : list A) :
+ Forall2 eq l1 l2 → l1 = l2.
+Proof.
+ induction l1 as [ | x1 l1 IH] in l2 |-*; simpl.
+ { intros ->%Forall2_nil_inv_l. done. }
+ intros (y1 & l2' & -> & Hf & ->)%Forall2_cons_inv_l.
+ f_equiv. by apply IH.
+Qed.
+
Lemma and_proper (A B C : Prop) :
(A → B ↔ C) →
(A ∧ B) ↔ (A ∧ C).
@@ -546,6 +562,14 @@ Lemma big_sepL2_to_zip {Σ} {A B} (l1 : list A) (l2 : list B) (Φ : _ → _ →
Proof.
rewrite big_sepL2_alt. iIntros "(_ & $)".
Qed.
+(* goal-directed version *)
+Lemma big_sepL2_to_zip' {Σ} {A B} (l1 : list A) (l2 : list B) (Φ : _ → _ → iProp Σ) :
+ ([∗ list] i ↦ x; y ∈ l1; l2, Φ i (x, y)) ⊢
+ [∗ list] i ↦ x ∈ zip l1 l2, Φ i x.
+Proof.
+ rewrite big_sepL2_alt. iIntros "(_ & Ha)".
+ setoid_rewrite <-surjective_pairing. done.
+Qed.
Local Lemma big_sepL2_later' {Σ} {A B} (l1 : list A) (l2 : list B) (Φ : _ → _ → _ → iProp Σ) n :
length l1 = length l2 →
@@ -583,6 +607,35 @@ Proof.
iModIntro. iIntros (? [? [? ?]] ?); simpl. eauto.
Qed.
+Lemma big_sepL_extend_l {Σ} {A B} (l' : list B) (l : list A) Φ :
+ length l' = length l →
+ ([∗ list] i ↦ x ∈ l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ y; x ∈ l'; l, Φ i x).
+Proof.
+ iIntros (?) "Ha". iApply big_sepL2_const_sepL_r. iFrame. done.
+Qed.
+Lemma big_sepL_extend_r {Σ} {A B} (l' : list B) (l : list A) Φ :
+ length l' = length l →
+ ([∗ list] i ↦ x ∈ l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x; y ∈ l; l', Φ i x).
+Proof.
+ iIntros (?) "Ha". iApply big_sepL2_const_sepL_l. iFrame. done.
+Qed.
+Lemma big_sepL2_elim_l {Σ} {A B} (l' : list B) (l : list A) Φ :
+ ([∗ list] i ↦ y; x ∈ l'; l, Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x ∈ l, Φ i x).
+Proof.
+ iIntros "Ha". rewrite big_sepL2_const_sepL_r. iDestruct "Ha" as "(_ & $)".
+Qed.
+Lemma big_sepL2_elim_r {Σ} {A B} (l' : list B) (l : list A) Φ :
+ ([∗ list] i ↦ x; y ∈ l; l', Φ i x) ⊢@{iProp Σ} ([∗ list] i ↦ x ∈ l, Φ i x).
+Proof.
+ iIntros "Ha". rewrite big_sepL2_const_sepL_l. iDestruct "Ha" as "(_ & $)".
+Qed.
+Lemma big_sepL2_sep_1 {Σ} {A B} (l1 : list A) (l2 : list B) Φ Ψ :
+ ⊢@{iProp Σ}
+ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
+ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2) -∗
+ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2).
+Proof. iIntros "Ha Hb". iApply big_sepL2_sep. iFrame. Qed.
+
(** ** General Iris/BI things *)
Lemma sep_ne_proper {Σ} (A : Prop) (B C : iProp Σ) n :
(A → B ≡{n}≡ C) →
@@ -746,6 +799,15 @@ Proof.
- rewrite !left_id. iApply (fupd_mask_mono with "HP"); done.
Qed.
+Lemma lc_split_le (m n : nat) :
+ m ≤ n →
+ £ n -∗ £ m ∗ £ (n - m).
+Proof.
+ intros ?. replace n with (m + (n - m))%nat by lia.
+ replace (m + (n - m) - m)%nat with (n - m)%nat by lia.
+ rewrite lc_split. auto.
+Qed.
+
Lemma maybe_later_mono (P : iProp Σ) b : ▷?b P -∗ ▷ P.
Proof.
iIntros "P". by iPoseProof (bi.laterN_le _ 1 with "P") as "P"; first (destruct b; simpl; lia).
diff --git a/theories/rust_typing/value.v b/theories/rust_typing/value.v
index ad79ab129a06db6842a55c094e642529cfa4fd8c..d744a28f956e9f733fa5409a9e93021d5a0f1739 100644
--- a/theories/rust_typing/value.v
+++ b/theories/rust_typing/value.v
@@ -446,28 +446,29 @@ Section value.
- rewrite /layout_wf/ly_align/u8/=. apply Z.divide_1_l.
- done.
Qed.
- Lemma value_t_untyped_length π v v1 ly :
- v â—áµ¥{Ï€} v1 @ value_t (UntypedSynType ly) -∗
+
+ Lemma value_t_has_length π v v1 st ly :
+ syn_type_has_layout st ly →
+ v â—áµ¥{Ï€} v1 @ value_t st -∗
⌜length v1 = ly_size ly⌠∗ ⌜length v = ly_size lyâŒ.
Proof.
rewrite /ty_own_val/=.
iDestruct 1 as "(%ot & %Hot & %Hmc & %Hly & %Hst)".
- apply use_op_alg_untyped_inv in Hot as ->.
- apply syn_type_has_layout_untyped_inv in Hst as (<- & ? & ?).
- apply is_memcast_val_untyped_inv in Hmc as ->.
- rewrite /has_layout_val in Hly. simpl in *.
- done.
+ assert (ly = ot_layout ot) as -> by by eapply syn_type_has_layout_inj.
+ iL. iPureIntro. apply is_memcast_val_length in Hmc as ->; done.
Qed.
- Lemma ofty_value_t_untyped_length F π l ly v1 :
+ Lemma ofty_value_t_has_length F π l st ly v1 :
lftE ⊆ F →
- l â—â‚—[Ï€, Owned false] #v1 @ (â— value_t (UntypedSynType ly)) ={F}=∗
- ⌜length v1 = ly_size ly⌠∗ l â—â‚—[Ï€, Owned false] #v1 @ (â— value_t (UntypedSynType ly)).
+ syn_type_has_layout st ly →
+ l â—â‚—[Ï€, Owned false] #v1 @ (â— value_t st) ={F}=∗
+ ⌜length v1 = ly_size ly⌠∗ l â—â‚—[Ï€, Owned false] #v1 @ (â— value_t st).
Proof.
- iIntros (?) "Hl".
+ iIntros (??) "Hl".
rewrite ltype_own_ofty_unfold/lty_of_ty_own.
iDestruct "Hl" as "(%ly' & % & % & ? & ? & ? & %r' & <- & Hb)".
iMod (fupd_mask_mono with "Hb") as "(%v & Hl & Hv)"; first done.
- iPoseProof (value_t_untyped_length with "Hv") as "(% & %)".
+ iPoseProof (value_t_has_length with "Hv") as "(% & %)"; first done.
+ assert (ly' = ly) as -> by by eapply syn_type_has_layout_inj.
iR. iModIntro. iExists _. iFrame. iR. iR. iExists _. iR.
iModIntro. eauto with iFrame.
Qed.
@@ -482,23 +483,33 @@ Section value.
Proof.
iIntros (? Hn ?).
rewrite /offset_loc.
- assert (ly_size (mk_array_layout ly k) = ly_size ly * k)%nat as Heq. {
- rewrite /mk_array_layout/ly_mult{1}/ly_size. lia. }
- rewrite -Nat2Z.inj_mul. rewrite -{3}Heq.
- iIntros "Hl". iMod (ofty_value_t_untyped_length with "Hl") as "(%Hlen & Hl)"; first done.
+ rewrite -Nat2Z.inj_mul -{3}(ly_size_mk_array_layout k ly).
+ iIntros "Hl".
+ iPoseProof (ltype_own_has_layout with "Hl") as "(%lyv & %Hstly & %Hlyl)".
+ simp_ltypes in Hstly. simpl in Hstly.
+ iMod (ofty_value_t_has_length with "Hl") as "(%Hlen & Hl)"; [done.. | ].
simpl in *.
iApply (ofty_value_t_split_adjacent with "Hl").
- done.
- simpl. lia.
- simpl. lia.
- - simpl. rewrite /mk_array_layout/ly_mult/ly_size/=. lia.
+ - simpl. rewrite !ly_size_mk_array_layout. lia.
- rewrite take_drop//.
- rewrite take_length. simpl.
- rewrite Heq. rewrite Hlen.
- rewrite /mk_array_layout/ly_mult{2}/ly_size. lia.
+ apply syn_type_has_layout_untyped_inv in Hstly as (-> & ? & ? & ?).
+ rewrite Hlen !ly_size_mk_array_layout. lia.
- by apply array_layout_wf.
- by apply array_layout_wf.
Qed.
+
+ Lemma value_t_has_layout π st v vs :
+ v â—áµ¥{Ï€} vs @ value_t st -∗
+ ∃ ly, ⌜syn_type_has_layout st ly⌠∗ ⌜v `has_layout_val` lyâŒ.
+ Proof.
+ rewrite /ty_own_val.
+ iDestruct 1 as "(%ot & %Hot & %Hmv & %Hv & %Hst)".
+ iExists (ot_layout ot). iR. done.
+ Qed.
End value.
Global Hint Unfold value_t : tyunfold.
@@ -508,15 +519,6 @@ Global Typeclasses Opaque value_t.
Section rules.
Context `{!typeGS Σ}.
- (* TODO move *)
- Lemma maybe_logical_step_fupd step F P :
- maybe_logical_step step F (|={F}=> P) -∗
- maybe_logical_step step F P.
- Proof.
- destruct step; simpl.
- - iApply logical_step_fupd.
- - rewrite fupd_trans; auto.
- Qed.
(** *** instances for types that are not value -- these have lower priority than the the value-specific versions below *)
(** by default, we go to UntypedSynType, and can later on specialize if needed by subsumption (we cannot go the other way around due to memcast compatibility) *)