diff --git a/theories/rust_typing/fixpoint.v b/theories/rust_typing/fixpoint.v
index d3b08e2c48ab112b1e56d926a6b53b8f06a5b7bd..dc766ef15c23144a8429ba49390ae961e43ff3d0 100644
--- a/theories/rust_typing/fixpoint.v
+++ b/theories/rust_typing/fixpoint.v
@@ -404,14 +404,14 @@ Section fixpoint.
intros n [][][Heq1 Heq2].
simpl in *. apply Heq1. }
apply _.
- - intros ? ? ? ? ? ? ? ? ? Hst. intros.
+ - intros ? ? ? ? ? ? ? ? Hst. intros.
rewrite /ty_shr/ty_own_val/= /F_ty_own_val_ty_shr_fixpoint/=.
eapply @limit_preserving.
{ eapply bi.limit_preserving_entails; first apply _.
intros n [][][Heq1 Heq2].
repeat f_equiv; simpl; [apply Heq2 | apply Heq1]. }
intros ?.
- eapply copy_shr_acc; [done | | done].
+ eapply copy_shr_acc; [ done |].
move: Hst. rewrite type_fixpoint_syn_type.
erewrite Fn_syn_type_const; done.
Qed.
diff --git a/theories/rust_typing/products.v b/theories/rust_typing/products.v
index 40e458afbc99292630085d602018799459d34781..b07c0dd0b411cafc9d1569434cace9dbf7e07737 100644
--- a/theories/rust_typing/products.v
+++ b/theories/rust_typing/products.v
@@ -1016,7 +1016,6 @@ Section copy.
length qs1 = length qs1' →
length vs1 = length fields1 →
rrust_ctx -∗
- na_own π (F ∖ shr_locsE l (fields_size fields1)) -∗
([∗ list] i↦ty;q ∈ pad_struct fields2 tys2 struct_make_uninit_type; qs2,
struct_own_el_shr π κ (length fields1 + i) all_fields l (projT2 ty).2 (projT2 ty).1 ∗ q.[κ]) -∗
@@ -1025,10 +1024,7 @@ Section copy.
) -∗
([∗ list] i ↦ v; '(q, q') ∈ vs1; (zip qs1 qs1'),
- na_own π (F ∖ shr_locsE l (fields_size (take (S i) all_fields))) -∗
- (▷ (l +ₗ offset_of_idx all_fields i) ↦{q'} v) ={E}=∗
- na_own π (F ∖ shr_locsE l (fields_size (take i all_fields) )) ∗ q.[κ]
- ) -∗
+ ▷ (l +ₗ offset_of_idx all_fields i) ↦{q'} v ={E}=∗ q.[κ]) -∗
|={E}=> ∃ qs2' vs2,
⌜length qs2' = length qs2⌠∗ ⌜length vs2 = length qs2⌠∗
@@ -1037,17 +1033,13 @@ Section copy.
struct_own_el_loc π q' v' i all_fields l (projT2 ty).2 (projT2 ty).1) ∗
(* if we give back the components, we get back the na token and lifetime tokens *)
([∗ list] i ↦ v; '(q, q') ∈ vs1 ++ vs2; (zip (qs1 ++ qs2) (qs1' ++ qs2')),
- na_own π (F ∖ shr_locsE l (fields_size (take (S i) all_fields))) -∗
- (▷ (l +ₗ offset_of_idx all_fields i) ↦{q'} v) ={E}=∗
- na_own π (F ∖ shr_locsE l (fields_size (take i all_fields))) ∗ q.[κ]
- ) ∗
+ ▷ (l +ₗ offset_of_idx all_fields i) ↦{q'} v ={E}=∗ q.[κ]
+ ).
(*(([∗ list] i ↦ ty; q ∈ pad_struct all_fields (tys1 ++ tys2) (λ ly : layout, existT (unit : Type) (uninit (UntypedSynType ly), # ())); qs1' ++ qs2',*)
(*▷ (l +ₗ offset_of_idx all_fields i) ↦{q}: ty_own_val (projT2 ty).1 π (projT2 ty).2) -∗*)
- (*na_own π (F ∖ shr_locsE l (fields_size all_fields)) ={E}=∗ na_own π F)*)
(*∗*)
- na_own π (F ∖ shr_locsE l (fields_size all_fields)).
Proof.
- iIntros (Hcopy ? Hf Hshr Hlen1 Hlen2 Hlen3 Hlen4 Hlen5) "#CTX Hna Hshr Hloc Hcl". subst all_fields.
+ iIntros (Hcopy ? Hf Hshr Hlen1 Hlen2 Hlen3 Hlen4 Hlen5) "#CTX Hshr Hloc Hcl". subst all_fields.
iInduction fields2 as [ | field2 fields2] "IH" forall (tys2 fields1 tys1 vs1 qs1 qs1' qs2 Hshr Hlen1 Hlen2 Hlen3 Hlen4 Hlen5 Hcopy); simpl.
{ destruct qs2; last done. iModIntro.
iExists [], []. simpl. destruct tys2; last done.
@@ -1066,19 +1058,10 @@ Section copy.
{ move: Hly1'. rewrite !lookup_app_r; [ | lia..].
rewrite !right_id !Nat.sub_diag. simpl. intros [= ->]; done. }
- iMod (copy_shr_acc with "CTX Hshr1 Hna Htok1") as "Ha".
+ iMod (copy_shr_acc with "CTX Hshr1 Htok1") as "Ha".
{ done. }
{ done. }
- { simpl. rewrite right_id.
- rewrite /offset_of_idx /fields_size.
- rewrite -!fmap_take.
- rewrite take_app.
- eapply shr_locsE_offset; last done.
- - lia.
- - rewrite /fields_size !fmap_app !sum_list_with_app. simpl. lia.
- }
- iDestruct "Ha" as "(>%Hlyl & %q2' & %v1 & Hna & (Hl & Hv) & Hlcl)".
- rewrite difference_difference_l_L.
+ iDestruct "Ha" as "(>%Hlyl & %q2' & %v1 & (Hl & Hv) & Hlcl)".
set (fields1' := fields1 ++ [(Some n, ly)]).
set (tys1' := tys1 ++ [ty2]).
set (vs1' := vs1 ++ [v1]).
@@ -1086,7 +1069,7 @@ Section copy.
set (qs1a' := qs1' ++ [q2']).
iPoseProof (ty_own_val_has_layout with "Hv") as "#Ha"; first done.
iDestruct "Ha" as ">%Hlyv".
- iSpecialize ("IH" $! tys2 fields1' tys1' vs1' qs1a qs1a' qs2 with "[] [] [] [] [] [] [] [Hna] [Hshr] [Hloc Hl Hv Hrfn Hsc] [Hcl Hlcl]").
+ iSpecialize ("IH" $! tys2 fields1' tys1' vs1' qs1a qs1a' qs2 with "[] [] [] [] [] [] [] [Hshr] [Hloc Hl Hv Hrfn Hsc] [Hcl Hlcl]").
{ subst fields1'. rewrite -app_assoc. done. }
{ iPureIntro. simpl in *. lia. }
{ iPureIntro. simpl in *. subst fields1' tys1'.
@@ -1096,10 +1079,6 @@ Section copy.
{ iPureIntro. subst qs1a qs1a'. rewrite !app_length/=. lia. }
{ iPureIntro. subst vs1' fields1'. rewrite !app_length/=. lia. }
{ done. }
- { rewrite /fields1'.
- iEval (rewrite /fields_size !fmap_app sum_list_with_app /= !Nat.add_0_r).
- iEval (rewrite /offset_of_idx -!fmap_take Nat.add_0_r take_app) in "Hna".
- rewrite shr_locsE_add. done. }
{ (* need to shift the indices etc *)
iPoseProof (big_sepL2_length with "Hshr") as "%Hlen7".
iApply (big_sepL2_wand with "Hshr"). iApply big_sepL2_intro; first done.
@@ -1129,18 +1108,11 @@ Section copy.
subst fields1'. rewrite -!app_assoc.
iApply (big_sepL2_app with "Hcl").
simpl. iSplitL; last done.
- iIntros "Hna Hl".
+ iIntros "Hl".
rewrite Hlen5.
- iMod ("Hlcl" with "[Hna] Hl") as "(Hna & $)".
- - iEval (rewrite /fields_size (app_assoc _ [_]) Nat.add_0_r) in "Hna".
- rewrite take_app'; first last. { rewrite app_length/=. lia. }
- rewrite !fmap_app sum_list_with_app /= Nat.add_0_r.
- rewrite shr_locsE_add.
- iEval (rewrite /offset_of_idx Nat.add_0_r -!fmap_take take_app).
- done.
- - iModIntro. iEval (rewrite /fields_size Nat.add_0_r take_app). done.
+ by iMod ("Hlcl" with "Hl") as "$".
}
- { iMod "IH" as "(%qs2' & %vs2 & % & % & Hl & Hcl & Hna)".
+ { iMod "IH" as "(%qs2' & %vs2 & % & % & Hl & Hcl)".
iModIntro. iExists (q2' :: qs2'), (v1 :: vs2).
rewrite /vs1'/qs1a'/= -!app_assoc /=. iFrame.
iPureIntro. split; lia.
@@ -1155,19 +1127,10 @@ Section copy.
{ move: Hly1'. rewrite !lookup_app_r; [ | lia..].
rewrite !right_id !Nat.sub_diag. simpl. intros [= ->]; done. }
- iMod (copy_shr_acc with "CTX Hshr1 Hna Htok1") as "Ha".
+ iMod (copy_shr_acc with "CTX Hshr1 Htok1") as "Ha".
{ done. }
{ done. }
- { simpl. rewrite right_id.
- rewrite /offset_of_idx /fields_size.
- rewrite -!fmap_take.
- rewrite take_app.
- eapply shr_locsE_offset; last done.
- - lia.
- - rewrite /fields_size !fmap_app !sum_list_with_app. simpl. lia.
- }
- iDestruct "Ha" as "(>%Hlyl & %q2' & %v1 & Hna & (Hl & Hv) & Hlcl)".
- rewrite difference_difference_l_L.
+ iDestruct "Ha" as "(>%Hlyl & %q2' & %v1 & (Hl & Hv) & Hlcl)".
set (fields1' := fields1 ++ [(None, ly)]).
(*set (tys1' := tys1 ++ [ty2]).*)
set (vs1' := vs1 ++ [v1]).
@@ -1175,7 +1138,7 @@ Section copy.
set (qs1a' := qs1' ++ [q2']).
iPoseProof (ty_own_val_has_layout with "Hv") as "#Ha"; first done.
iDestruct "Ha" as ">%Hlyv".
- iSpecialize ("IH" $! tys2 fields1' tys1 vs1' qs1a qs1a' qs2 with "[] [] [] [] [] [] [] [Hna] [Hshr] [Hloc Hl Hv Hrfn Hsc] [Hcl Hlcl]").
+ iSpecialize ("IH" $! tys2 fields1' tys1 vs1' qs1a qs1a' qs2 with "[] [] [] [] [] [] [] [Hshr] [Hloc Hl Hv Hrfn Hsc] [Hcl Hlcl]").
{ subst fields1'. rewrite -app_assoc. done. }
{ iPureIntro. simpl in *. lia. }
{ iPureIntro. simpl in *. subst fields1'.
@@ -1185,10 +1148,6 @@ Section copy.
{ iPureIntro. subst qs1a qs1a'. rewrite !app_length/=. lia. }
{ iPureIntro. subst vs1' fields1'. rewrite !app_length/=. lia. }
{ iPureIntro. done. }
- { rewrite /fields1'.
- iEval (rewrite /fields_size !fmap_app sum_list_with_app /= !Nat.add_0_r).
- iEval (rewrite /offset_of_idx -!fmap_take Nat.add_0_r take_app) in "Hna".
- rewrite shr_locsE_add. done. }
{ (* need to shift the indices etc *)
iPoseProof (big_sepL2_length with "Hshr") as "%Hlen7".
iApply (big_sepL2_wand with "Hshr"). iApply big_sepL2_intro; first done.
@@ -1217,18 +1176,11 @@ Section copy.
subst fields1'. rewrite -!app_assoc.
iApply (big_sepL2_app with "Hcl").
simpl. iSplitL; last done.
- iIntros "Hna Hl".
+ iIntros "Hl".
rewrite Hlen5.
- iMod ("Hlcl" with "[Hna] Hl") as "(Hna & $)".
- - iEval (rewrite /fields_size (app_assoc _ [_]) Nat.add_0_r) in "Hna".
- rewrite take_app'; first last. { rewrite app_length/=. lia. }
- rewrite !fmap_app sum_list_with_app /= Nat.add_0_r.
- rewrite shr_locsE_add.
- iEval (rewrite /offset_of_idx Nat.add_0_r -!fmap_take take_app).
- done.
- - iModIntro. iEval (rewrite /fields_size Nat.add_0_r take_app). done.
+ by iMod ("Hlcl" with "Hl") as "$".
}
- { iMod "IH" as "(%qs2' & %vs2 & % & % & Hl & Hcl & Hna)".
+ { iMod "IH" as "(%qs2' & %vs2 & % & % & Hl & Hcl)".
iModIntro. iExists (q2' :: qs2'), (v1 :: vs2).
rewrite /vs1'/qs1a'/= -!app_assoc /=. iFrame.
iPureIntro. split; lia.
@@ -1241,7 +1193,6 @@ Section copy.
shr_locsE l (fields_size fields + 1) ⊆ F →
length (named_fields fields) = length tys →
rrust_ctx -∗
- na_own π F -∗
([∗ list] i↦ty;q ∈ pad_struct fields tys struct_make_uninit_type; qs,
struct_own_el_shr π κ i fields l (projT2 ty).2 (projT2 ty).1 ∗ q.[κ]) -∗
|={E}=> ∃ qs' vs,
@@ -1251,37 +1202,18 @@ Section copy.
struct_own_el_loc π q' v' i fields l (projT2 ty).2 (projT2 ty).1) ∗
(* if we give back the components, we get back the na token and lifetime tokens *)
([∗ list] i ↦ v; '(q, q') ∈ vs; zip qs qs',
- na_own π (F ∖ shr_locsE l (fields_size (take (S i) fields))) -∗
- (▷ (l +ₗ offset_of_idx fields i) ↦{q'} v) ={E}=∗
- na_own π (F ∖ shr_locsE l (fields_size (take i fields))) ∗ q.[κ]
- ) ∗
- na_own π (F ∖ shr_locsE l (fields_size fields)).
+ (▷ (l +ₗ offset_of_idx fields i) ↦{q'} v) ={E}=∗ q.[κ]).
Proof.
- iIntros (????) "CTX Hna Hloc".
- iMod (struct_t_copy_ind _ [] qs [] [] [] tys [] fields fields with "CTX [Hna] Hloc [] []") as "Ha".
- { done. }
- { done. }
- { done. }
- { done. }
- { done. }
- { done. }
- { done. }
- { done. }
- { done. }
- { simpl. rewrite difference_empty_L. done. }
- { iNext. done. }
- { done. }
- simpl. done.
+ iIntros (????) "CTX Hloc".
+ iMod (struct_t_copy_ind _ [] qs [] [] [] tys [] fields fields with "CTX Hloc [] []") as "Ha"; try done.
+ by iNext.
Qed.
-
- Lemma struct_t_copy_acc π (tys : list (sigT (λ rt, type rt * place_rfn rt)%type)) fields q κ l E F :
+ Lemma struct_t_copy_acc π (tys : list (sigT (λ rt, type rt * place_rfn rt)%type)) fields q κ l E :
Forall (λ ty, Copyable (projT2 ty).1) tys →
lftE ∪ ↑shrN ⊆ E →
- shr_locsE l (fields_size fields + 1) ⊆ F →
length (named_fields fields) = length tys →
rrust_ctx -∗
- na_own π F -∗
q.[κ] -∗
([∗ list] i↦ty ∈ pad_struct fields tys struct_make_uninit_type, struct_own_el_shr π κ i fields l (projT2 ty).2 (projT2 ty).1) -∗
|={E}=> ∃ q' vs,
@@ -1290,14 +1222,11 @@ Section copy.
(▷ [∗ list] i ↦ ty; v' ∈ pad_struct fields tys struct_make_uninit_type; vs,
struct_own_el_loc π q' v' i fields l (projT2 ty).2 (projT2 ty).1) ∗
(* if we give back the components, we get back the na token and lifetime tokens *)
- (([∗ list] i ↦ v ∈ vs, (▷ (l +ₗ offset_of_idx fields i) ↦{q'} v)) -∗
- na_own π (F ∖ shr_locsE l (fields_size fields)) ={E}=∗
- na_own π F ∗ q.[κ]) ∗
- na_own π (F ∖ shr_locsE l (fields_size fields)).
+ (([∗ list] i ↦ v ∈ vs, (▷ (l +ₗ offset_of_idx fields i) ↦{q'} v)) ={E}=∗ q.[κ]).
Proof.
- iIntros (????) "#CTX Hna Htok Hloc".
+ iIntros (???) "#CTX Htok Hloc".
iPoseProof (Fractional_split_big_sepL (λ q, q.[κ])%I (length fields) with "Htok") as "(%qs & %Hlen_eq & Htoks & Htoks_cl)".
- iMod (struct_t_copy_ind' with "CTX Hna [Hloc Htoks]") as "(%qs' & %vs & %Hlen1 & %Hlen2 & Hloc & Hcl & Hna)"; [ done.. | | ].
+ iMod (struct_t_copy_ind' with "CTX [Hloc Htoks]") as "(%qs' & %vs & %Hlen1 & %Hlen2 & Hloc & Hcl)"; [ done.. | | ].
{ iApply big_sepL2_sep. iSplitL "Hloc".
1: iApply big_sepL_extend_r; last done.
2: iApply big_sepL_extend_l; last iApply "Htoks".
@@ -1333,8 +1262,7 @@ Section copy.
iModIntro. iExists q', vs. iFrame.
iSplitR. { iPureIntro. lia. }
-
- iIntros "Hloc Hna".
+ iIntros "Hloc".
iPoseProof (big_sepL2_length with "Hcl") as "%Hlen".
rewrite zip_with_length in Hlen.
iPoseProof (big_sepL2_to_zip with "Hcl") as "Hcl".
@@ -1353,30 +1281,28 @@ Section copy.
iPoseProof (big_sepL2_to_zip with "Hloc") as "Hloc".
iPoseProof (big_sepL_sep_2 with "Hcl Hloc") as "Hcl".
rewrite zip_assoc_l big_sepL_fmap.
- iAssert ([∗ list] i ↦ y ∈ qs, na_own π (F ∖ shr_locsE l (fields_size (take (S i) fields))) ={E}=∗ na_own π (F ∖ shr_locsE l (fields_size (take i fields))) ∗ (y).[κ])%I with "[Hcl]" as "Hcl".
+
+ iAssert ([∗ list] i ↦ y ∈ qs, True ={E}=∗ (y).[κ])%I with "[Hcl]" as "Hcl".
{ iApply big_sepL2_elim_l. iApply big_sepL2_from_zip; first last.
{ iApply (big_sepL2_elim_l). iApply big_sepL2_from_zip; first last.
{ iApply (big_sepL_wand with "Hcl").
iApply big_sepL_intro. iModIntro. iIntros (k [v [q1' q1]] Hlook) "Ha Hna"; simpl.
iDestruct "Ha" as "((Ha & Hcl) & Hl)".
iPoseProof ("Hcl" with "Hl") as "Hl".
- iApply ("Ha" with "Hna Hl"). }
+ iApply ("Ha" with "Hl"). }
rewrite zip_with_length. lia. }
lia. }
(* now collapse the whole sequence *)
- set (P i := (|={E}=> (na_own π (F ∖ shr_locsE l (fields_size (take i fields))) ∗ [∗ list] q ∈ (drop i qs), q.[κ]))%I).
- iPoseProof (big_sepL_eliminate_sequence_rev P with "Hcl [Hna] []") as "Ha".
- { iModIntro. rewrite drop_all. iSplitL; last done.
- assert (length qs = length fields) as -> by lia. rewrite firstn_all. iFrame.
- }
- { rewrite /P. iModIntro. iIntros (i q1 Hlook) ">(Hna & Htoks) Hvs".
- iMod ("Hvs" with "Hna") as "(Hna & Htok)".
- iFrame. erewrite (drop_S _ _ i); last done; simpl. by iFrame.
+ set (P i := (|={E}=> ([∗ list] q ∈ (drop i qs), q.[κ]))%I).
+ iPoseProof (big_sepL_eliminate_sequence_rev P with "Hcl [] []") as "Ha".
+ { iModIntro. rewrite drop_all. done. }
+ { rewrite /P. iModIntro. iIntros (i q1 Hlook) ">Htoks Hvs".
+ erewrite (drop_S _ _ i); last done; simpl. iFrame.
+ by iApply "Hvs".
}
- iMod "Ha" as "(Hna & Htoks)".
- iPoseProof ("Htoks_cl" with "Htoks") as "$".
- simpl. rewrite difference_empty_L. done.
+ iMod "Ha" as "Htoks".
+ by iPoseProof ("Htoks_cl" with "Htoks") as "$".
Qed.
Global Instance struct_t_copy {rts} (tys : hlist type rts) sls :
@@ -1384,14 +1310,14 @@ Section copy.
Copyable (struct_t sls tys).
Proof.
iIntros (Hcopy). split; first apply _.
- iIntros (κ π E F l ly r q ? Halg ?) "#CTX Hshr Hna Htok".
+ iIntros (κ π E l ly r q Halg ?) "#CTX Hshr Htok".
rewrite /ty_shr /=.
iDestruct "Hshr" as (sl) "(%Halg' & %Hlen & %Hly & #Hlb & #Hb)".
simpl in Halg.
specialize (use_struct_layout_alg_Some_inv _ _ Halg') as Halg2.
assert (ly = sl) as -> by by eapply syn_type_has_layout_inj.
iR.
- iMod (struct_t_copy_acc _ (hpzipl rts tys r) (sl_members sl) with "CTX Hna Htok Hb") as "(%q' & %vs & % & Hs & Hcl & Hna)".
+ iMod (struct_t_copy_acc _ (hpzipl rts tys r) (sl_members sl) with "CTX Htok Hb") as "(%q' & %vs & % & Hs & Hcl)".
{ clear -Hcopy. induction rts as [ | rt rts IH] in tys, r, Hcopy |-*; simpl.
- inv_hlist tys. destruct r. constructor.
- inv_hlist tys => ty tys. destruct r as [r1 r].
@@ -1399,7 +1325,6 @@ Section copy.
econstructor; first done. by apply IH.
}
{ done. }
- { done. }
{ rewrite hpzipl_length. rewrite named_fields_field_names_length. erewrite struct_layout_spec_has_layout_fields_length; done. }
(* now we need to pull the pointsto *)
@@ -1422,8 +1347,8 @@ Section copy.
{ iModIntro. iNext. rewrite fst_zip; last lia. iFrame. iExists _. iR. iR.
iSplitR. { iPureIntro. by apply mjoin_has_struct_layout. }
done. }
- iModIntro. iIntros "Hna Hpts".
- iApply ("Hcl" with "[Hpts]"); last done.
+ iModIntro. iIntros "Hpts".
+ iApply ("Hcl" with "[Hpts]").
iApply big_sepL_later. iNext. rewrite heap_mapsto_reshape_sl; last by apply mjoin_has_struct_layout.
iDestruct "Hpts" as "(_ & Hpts)". rewrite reshape_join; first done.
rewrite Forall2_fmap_r. eapply Forall2_impl; first done.
@@ -4149,4 +4074,3 @@ Section test.
*)
End test.
-
diff --git a/theories/rust_typing/program_rules.v b/theories/rust_typing/program_rules.v
index 4ff08f2effe0c309514c5582999e2f1036507bc3..e5814f28cc8eb165b5eb94dcd1dbe8f601898e24 100644
--- a/theories/rust_typing/program_rules.v
+++ b/theories/rust_typing/program_rules.v
@@ -2302,15 +2302,13 @@ Section typing.
(** [type_read_end] instance that does a copy *)
Lemma type_read_ofty_copy E L {rt} π (T : typed_read_end_cont_t rt) b2 bmin br l (ty : type rt) r ot `{!Copyable ty}:
- find_in_context FindNaOwn (λ '(π', mask),
- ⌜π' = π⌠∗ ⌜shrE ⊆ mask⌠∗
- (** We have to show that the type allows reads *)
- (⌜ty_has_op_type ty ot MCCopy⌠∗ ⌜lctx_bor_kind_alive E L b2⌠∗
- (** The place is left as-is *)
- ∀ v, na_own π mask -∗ T L v rt ty r rt (◠ty) (#r) (ResultWeak eq_refl)))
+ (** We have to show that the type allows reads *)
+ (⌜ty_has_op_type ty ot MCCopy⌠∗ ⌜lctx_bor_kind_alive E L b2⌠∗
+ (** The place is left as-is *)
+ ∀ v, T L v rt ty r rt (◠ty) (#r) (ResultWeak eq_refl))
⊢ typed_read_end π E L l (◠ty) (#r) b2 bmin br ot T.
Proof.
- iDestruct 1 as ([Ï€' mask]) "(Hna & -> & %Heq & (%Hot & %Hal & Hs))".
+ iIntros "(%Hot & %Hal & Hs)".
iIntros (F ???) "#CTX #HE HL".
destruct b2 as [ wl | | ]; simpl.
@@ -2331,22 +2329,23 @@ Section typing.
iR. iSplitR. { iApply typed_place_cond_refl. done. }
by iApply "Hs".
- - iIntros "Hincl0 #Hl".
+ - iIntros "_ #Hl".
simpl in Hal.
+
iPoseProof (ofty_ltype_acc_shared with "Hl") as "(%ly & %Halg & %Hly & Hlb & >Hl')"; first done.
+ assert (ly = ot_layout ot) as ->.
+ { specialize (ty_op_type_stable Hot) as ?. eapply syn_type_has_layout_inj; done. }
+
iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
iMod (lctx_lft_alive_tok_noend κ with "HE HL") as (q') "(Htok & HL & Hclose)"; [solve_ndisj | done | ].
- iMod (copy_shr_acc _ _ _ mask with "CTX Hl' [Hna] Htok") as "(>%Hly' & (%q'' & %v & Hna & (>Hll & #Hv) & Hclose_l))";
- [solve_ndisj | solve_ndisj | | | ].
- { etrans; last done. eapply shr_locsE_incl. }
- { done. }
+ iMod (copy_shr_acc with "CTX Hl' Htok") as "(>%Hly' & (%q'' & %v & (>Hll & #Hv) & Hclose_l))";
+ [solve_ndisj.. | done | ].
+
iDestruct (ty_own_val_has_layout with "Hv") as "#>%Hlyv"; first done.
iModIntro. iExists _, _, rt, _, _. iFrame "Hll Hv".
- assert (ly = ot_layout ot) as ->.
- { specialize (ty_op_type_stable Hot) as ?. eapply syn_type_has_layout_inj; done. }
iSplitR; first done. iSplitR; first done.
iApply logical_step_intro. iIntros (st) "Hll Hv'".
- iMod ("Hclose_l" with "Hna [Hv Hll]") as "[Hna Htok]".
+ iMod ("Hclose_l" with "[Hv Hll]") as "Htok".
{ eauto with iFrame. }
iMod ("Hclose" with "Htok HL") as "HL".
iPoseProof ("HL_cl" with "HL") as "HL".
@@ -2356,14 +2355,13 @@ Section typing.
iExists _, _, _, (ResultWeak eq_refl).
iFrame "Hl". iR.
- iSplitL "".
- 2: { iSpecialize ("Hs" with "[Hna]"); done. }
+ iSplitR "Hs"; last done.
iSplit.
{ iApply typed_place_cond_ty_refl_ofty. }
{ iApply typed_place_cond_rfn_refl. }
- - iIntros "Hincl0 Hl".
+ - iIntros "_ Hl".
simpl in Hal.
iPoseProof (llctx_interp_acc_noend with "HL") as "(HL & HL_cl)".
iMod (fupd_mask_subseteq lftE) as "HF_cl"; first done.
@@ -2386,8 +2384,7 @@ Section typing.
iExists _, _, _, (ResultWeak eq_refl).
iFrame; iR.
- iSplitL "".
- 2: { by iSpecialize ("Hs" with "Hna"). }
+ iSplitR "Hs"; last done.
iSplit.
{ iApply typed_place_cond_ty_refl_ofty. }
diff --git a/theories/rust_typing/shr_ref.v b/theories/rust_typing/shr_ref.v
index 5c919f41f4fb79e80089c11c91d62cc64a3231c4..78ec81ba65a6012f5f86f52ab5ae38c9f7da47c5 100644
--- a/theories/rust_typing/shr_ref.v
+++ b/theories/rust_typing/shr_ref.v
@@ -105,16 +105,14 @@ Section shr_ref.
Global Instance shr_ref_copyable {rt} (ty : type rt) κ : Copyable (shr_ref κ ty).
Proof.
constructor; first apply _.
- iIntros (κ' π E F l ly r ? ? Ha ?) "[LFT TIME] (%li & %ly' & %r' & %Hly' & % & % & #Hlb & #Hsc & #Hr & Hf & #Hown) Htok Hlft".
- iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
+ iIntros (κ' π E l ly r ? ? Ha) "[LFT TIME] (%li & %ly' & %r' & %Hly' & % & % & #Hlb & #Hsc & #Hr & Hf & #Hown) Hlft".
iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first solve_ndisj.
iModIntro.
assert (ly = void*) as ->. { injection Ha. done. }
iSplitR; first done.
iExists _, li. iDestruct "Hmt" as "[Hmt1 Hmt2]".
iSplitL "Hmt1". { iNext. iFrame "Hmt1". iExists li, ly', r'. iFrame "#". eauto. }
- iIntros "Htok2 Hmt1".
- iDestruct ("Htok" with "Htok2") as "$".
+ iIntros "Hmt1".
iApply "Hclose". iModIntro. rewrite -{3}(Qp.div_2 q').
iPoseProof (heap_mapsto_agree with "Hmt1 Hmt2") as "%Heq"; first done.
rewrite heap_mapsto_fractional. iFrame.
diff --git a/theories/rust_typing/type.v b/theories/rust_typing/type.v
index e6b1ad7ca438286bfd8c0445381c7fa91a26319f..3a8f5988cc471968c4872be30cf12e3005c66bfe 100644
--- a/theories/rust_typing/type.v
+++ b/theories/rust_typing/type.v
@@ -1762,17 +1762,15 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
Class Copyable `{!typeGS Σ} {rt} (ty : type rt) := {
copy_own_persistent π r v : Persistent (ty.(ty_own_val) π r v);
(* sharing predicates of copyable types should actually allow us to get a Copy out from below the reference *)
- copy_shr_acc κ π E F l ly r q :
+ copy_shr_acc κ π E l ly r q :
lftE ∪ ↑shrN ⊆ E →
syn_type_has_layout ty.(ty_syn_type) ly →
- shr_locsE l (ly.(ly_size) + 1) ⊆ F →
rrust_ctx -∗
ty.(ty_shr) κ π r l -∗
- na_own π F -∗ q.[κ] ={E}=∗
+ q.[κ] ={E}=∗
▷ ⌜l `has_layout_loc` ly⌠∗
- ∃ q' v, na_own π (F ∖ shr_locsE l ly.(ly_size)) ∗
- ▷ (l ↦{q'} v ∗ ty.(ty_own_val) π r v) ∗
- (na_own π (F ∖ shr_locsE l ly.(ly_size)) -∗ ▷l ↦{q'} v ={E}=∗ na_own π F ∗ q.[κ])
+ ∃ q' v, ▷ (l ↦{q'} v ∗ ty.(ty_own_val) π r v) ∗
+ (▷l ↦{q'} v ={E}=∗ q.[κ])
}.
#[export] Hint Mode Copyable - - + + : typeclass_instances.
#[export] Existing Instance copy_own_persistent.
@@ -1866,15 +1864,13 @@ Section copy.
#[export] Program Instance simple_type_copyable `{typeGS Σ} {rt} (st : simple_type rt) : Copyable st.
Next Obligation.
- iIntros (??? st κ π E F l ly r ? Hst ?). iIntros (?) "#(LFT & TIME & LLCTX) (%v & %ly' & Hf & #Hown & %Hst' & Hly) Htok Hlft".
+ iIntros (??? st κ π E l ly r ? Hst ?) "#(LFT & TIME & LLCTX) (%v & %ly' & Hf & #Hown & %Hst' & Hly) Hlft".
have: (ly' = ly); first by eapply syn_type_has_layout_inj. move => ?; subst ly'.
- iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first solve_ndisj.
iModIntro. iFrame "Hly". iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
iExists v.
iSplitL "Hmt1"; first by auto with iFrame.
- iIntros "Htok2 Hmt1".
- iDestruct ("Htok" with "Htok2") as "$".
+ iIntros "Hmt1".
iApply "Hclose". iModIntro. rewrite -{3}(Qp.div_2 q').
iPoseProof (heap_mapsto_agree with "Hmt1 Hmt2") as "%Heq"; first done.
rewrite heap_mapsto_fractional. iFrame.