diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 9847b59736cd98165c20eaf1dcf39abc149658ad..1120df37d63dea894022dff37cb9d1fe6eb7fa69 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2024-02-06.0.66d2e339") | (= "dev") }
+ "coq-iris" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 5b4e7d9d56547f38225f88ea70562aa92aeb1826..c50a56d4d76870d04804b2681f83cddeb88e5644 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -189,7 +189,7 @@ Section arc.
iMod (own_alloc ((â— (Some $ Cinl ((1/2)%Qp, xH, None), O) â‹…
â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
as (γ) "[H◠H◯]"; first by apply auth_both_valid_discrete.
- iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
+ iFrame. iApply inv_alloc. iExists _. iFrame.
rewrite Qp.div_2. auto.
Qed.
@@ -314,7 +314,7 @@ Section arc.
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ (1%nat)). }
iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
- { iExists _. iFrame. iExists _.
+ { iExists _. iFrame.
rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- destruct wlock.
@@ -407,7 +407,7 @@ Section arc.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid. rewrite /= -Heq comm_L.
by apply Qp.add_le_mono_l, Qp.div_le. }
- iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
+ iFrame. iApply "Hclose1". iExists _. iFrame.
rewrite /= [xH â‹… _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
Qp.div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
@@ -529,7 +529,7 @@ Section arc.
iMod (own_update_2 _ _ _ _ with "Hâ— Hown") as "Hâ—".
{ apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_".
- { iExists _. iFrame. iExists (q + q'')%Qp. iCombine "HP1 HP1'" as "$".
+ { iExists _. iCombine "HP1 HP1'" as "HP". iFrame "Hâ—". iFrame.
iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index e2777f892571510e1d4cb86bc9ce8c70260ce518..40cd71babe0f85db77c1b1d16ee8b09fd8b1eb83 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -90,7 +90,7 @@ Proof.
auto. }
iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
iMod ("Hclose" with "[-HΦ]").
- - iNext. iRight. iExists true. iFrame. iExists _. iFrame.
+ - iNext. iRight. iExists true. iFrame.
- iModIntro. wp_seq. by iApply "HΦ".
Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 945816ce2d4a65d06c6eabf5d9aaa3683faec8d2..93f6474431db6f04c63ea77d32bc672a27a6c9ac 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -140,13 +140,12 @@ Proof.
first solve_ndisj.
{ by rewrite lookup_insert. }
iFrame.
- iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later.
- iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame.
- iExists _. iFrame.
+ iApply "Hclose'". iFrame. rewrite big_sepS_later.
+ iApply "Hclose''". iLeft. iFrame "% ∗".
rewrite insert_insert -(fmap_insert _ _ _ Bor_in) insert_id //.
- iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
iMod ("Hclose'" with "[-Hbor]") as "_".
- + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ + iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†"); first done. iFrame.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
@@ -175,7 +174,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iExists κ''. iFrame "#". iIntros "!> %Q HvsQ HQ". clear -HE.
+ iExists κ''. iFrame "Hle". iIntros "!> %Q HvsQ HQ". clear -HE.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -208,11 +207,11 @@ Proof.
- by rewrite big_sepM_delete.
- by rewrite -fmap_None -lookup_fmap fmap_delete. }
iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
- { iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
- iLeft. iFrame "%". iExists _, _. iFrame. }
+ { iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
+ iLeft. iFrame "% ∗". }
iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
- iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
- iExists Q. rewrite -(bi.iff_refl emp). auto.
+ iSplit; first by iApply lft_incl_refl. iFrame.
+ iExists Q. rewrite -(bi.iff_refl emp). eauto.
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hbor")
as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
@@ -238,7 +237,7 @@ Proof.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- - iLeft. iExists (i.1). iFrame "#".
+ - iLeft. iFrame "Hle".
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
unfold lft_bor_alive, idx_bor_own.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
@@ -261,18 +260,18 @@ Proof.
-fmap_None -lookup_fmap fmap_delete //. }
rewrite own_bor_op. iDestruct "Hown" as "[Hâ— Hâ—¯]".
iMod ("Hclose'" with "[- Hâ—¯]"); last first.
- { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
- iExists j. iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
- iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
- iLeft. iFrame "%". iExists _, _. iFrame. iNext.
+ { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
+ iFrame "Hs' ∗". rewrite -(bi.iff_refl emp). auto. }
+ iFrame. rewrite big_sepS_later. iApply "Hclose''".
+ iLeft. iFrame "%". iExists _, _.
rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
- iExists _. iFrame "Hbox Hâ—".
+ iFrame.
rewrite big_sepM_insert; last first.
{ by rewrite -fmap_None -lookup_fmap fmap_delete. }
by rewrite big_sepM_delete.
- iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
iMod ("Hclose'" with "[-Hbor]") as "_".
- + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ + iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†") as "$"; first done.
iApply fupd_mask_subseteq; first solve_ndisj.
Qed.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 310bcc8396b8da1b4f567115fe2a67884d8381f8..84949761aad28a44a71dbfd749f6d24404f7ea3a 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -42,8 +42,8 @@ Proof.
simpl. iFrame. }
iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
iSplitL "HBâ—¯ HsliceB".
- + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
- iExists P. rewrite -(bi.iff_refl emp). auto.
+ + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iFrame.
+ rewrite -(bi.iff_refl emp). auto.
+ clear -HE. iIntros "!> H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iDestruct ("HIlookup" with "HI") as %Hκ.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 4541525e5ffd095614ed952f1adbe7ab9b9de723..72e655f4eedd659768c774fa188b386deff62d17 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -50,14 +50,12 @@ Proof.
-fmap_None -lookup_fmap fmap_delete //. }
rewrite !own_bor_op. iDestruct "Hbor" as "[[Hâ— Hâ—¯2] Hâ—¯1]".
iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
- iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
+ { rewrite /bor /raw_bor /idx_bor_own. iFrame "#∗". by rewrite -(bi.iff_refl emp). }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
- iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
- iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
- iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
- rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox Hâ—".
+ { rewrite /bor /raw_bor /idx_bor_own. iFrame "#∗". by rewrite -(bi.iff_refl emp). }
+ iApply "Hclose". iFrame. rewrite big_sepS_later.
+ iApply "Hclose'". iLeft.
+ rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "%∗".
rewrite !big_sepM_insert /=.
+ by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
+ by rewrite -fmap_None -lookup_fmap fmap_delete.
@@ -66,9 +64,9 @@ Proof.
iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor2]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
- { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
- iRight. iSplit; last by auto. iExists _. iFrame. }
- unfold bor. iSplitL "Hbor1"; iExists _; eauto.
+ { iFrame. rewrite big_sepS_later. iApply "Hclose'".
+ iRight. by iFrame. }
+ unfold bor. by iFrame "#∗".
Qed.
Lemma bor_combine E κ P Q :
@@ -119,12 +117,11 @@ Proof.
rewrite own_bor_op. iDestruct "Hbor" as "[Hâ— Hâ—¯]".
iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
- iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
- iExists γ. iFrame. iExists _. iFrame. iNext. iModIntro.
+ iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2"). iFrame. iNext. iModIntro.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
- iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
- iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
- rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox Hâ—".
+ iApply "Hclose". iFrame. rewrite big_sepS_later.
+ iApply "Hclose'". iLeft.
+ rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "%∗".
rewrite !big_sepM_insert /=.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=; last first.
@@ -134,8 +131,8 @@ Proof.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
iMod ("Hclose" with "[-Hbor]") as "_".
- { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
- iRight. iSplit; last by auto. iExists _. iFrame. }
- unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
+ { iFrame. rewrite big_sepS_later. iApply "Hclose'".
+ iRight. by iFrame. }
+ unfold bor. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
Qed.
End borrow.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 2b3b0f4bc87ae962b09c1fa8a8e160f3bb94966b..3405d59a847828305cbe4bc60f0c316031a2ef5f 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -443,8 +443,7 @@ Proof.
rewrite /bor /raw_bor /idx_bor /bor_idx. iSplit.
- iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
iExists (κ', s). by iFrame.
- - iDestruct 1 as ([κ' s]) "[[??]?]".
- iExists κ'. iFrame. iExists s. by iFrame.
+ - iDestruct 1 as ([κ' s]) "[[??]?]". iFrame.
Qed.
Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 47b7e97f4b812d39e58d4cfb87a7d6d0900ec6ee..4712bfc6821985103be57730f655b98d21d60da3 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -362,10 +362,9 @@ Section arc.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lrc â— box (arc ty)]
with "[] LFT HE Hna HL Hk [>-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦"; first by iExists _; rewrite ->uninit_own; auto.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame "∗%".
iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
- rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
+ rewrite freeable_sz_full_S. by iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -405,7 +404,7 @@ Section arc.
iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
- { rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
+ { rewrite freeable_sz_full_S. iFrame.
by rewrite vec_to_list_length. }
iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!> Hν".
iDestruct (lft_tok_dead with "Hν H†") as "[]". }
@@ -793,8 +792,8 @@ Section arc.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (option ty) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
- by rewrite tctx_hasty_val. }
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+ rewrite tctx_hasty_val. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -828,8 +827,8 @@ Section arc.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (uninit 0) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
- by rewrite tctx_hasty_val. }
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+ rewrite tctx_hasty_val. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -894,7 +893,7 @@ Section arc.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
- -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+ -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame.
iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
rewrite app_length drop_length. lia. }
iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 4cbc56fcc9de78bd094c9a04995cf45d2122b475..ce5730cb6b0fe77b18aa5ca06231c4162e2348e8 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -130,12 +130,11 @@ Section brandedvec.
iMod (frac_bor_acc with "LFT Hmem Hlft") as (q') "[>Hmt Hclose]"; first solve_ndisj.
iDestruct "Hmt" as "[Hmt1 Hmt2]".
iModIntro. iExists _.
- iSplitL "Hmt1".
- { iExists [_]. iNext. iFrame. iExists _. eauto with iFrame. }
+ iSplitL "Hmt1"; first by simpl; iFrame "∗#".
iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[>Hmt1 #Hown']".
iDestruct ("Htok" with "Htok2") as "$".
iAssert (â–· ⌜1 = length vl'âŒ)%I as ">%".
- { iNext. iDestruct (ty_size_eq with "Hown'") as %->. done. }
+ { iNext. by iDestruct ("Hown'") as "[%x [Hown' ->]]". }
destruct vl' as [|v' vl']; first done.
destruct vl' as [|]; last first. { simpl in *. lia. }
rewrite !heap_pointsto_vec_singleton.
@@ -201,10 +200,7 @@ Section typing.
iSplitR; first done.
simpl.
rewrite freeable_sz_full.
- iFrame.
- iExists 0%nat.
- iSplitL; last done.
- iExists γ; iSplitR; by eauto. }
+ by iFrame "#∗". }
iMod ("Hn'" with "[%]") as (α) "[Hn Htok]"; [solve_typing..|].
wp_let.
iMod (lctx_lft_alive_tok Ï with "HE HL")
@@ -399,11 +395,7 @@ Section typing.
iMod ("Hclose'" with "[H↦ Hidx Hown]") as "[Hn Hβ]".
{ iExists (#(n+1)::nil).
rewrite heap_pointsto_vec_singleton.
- iFrame "∗".
- iIntros "!>".
- iExists (n + 1)%nat.
- iSplitL; last by (iPureIntro; do 3 f_equal; lia).
- iExists γ. eauto with iFrame.
+ iFrame "#∗". iPureIntro; do 3 f_equal; lia.
}
iMod ("Hclose" with "Hβ HL") as "HL".
iApply (type_type _ _ _ [ r â— box (uninit 1); #n â— brandidx _]
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 3405077ee74781787d59a31269114efde0135fb8..2bf7a723865cd5342334be4d6ce1b33226a593fa 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -223,9 +223,7 @@ Section typing.
[c ◠box (&shr{α}(cell ty)); #x ◠box (uninit ty.(ty_size)); #r ◠box ty]
with "[] LFT HE Htl HL HC"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
- iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
- - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
- - iFrame. iExists _. iFrame. }
+ iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†"; by iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 1cd696e9ec46a4984a1fbb867aa5439cf60d1534..62f928cb772eafaa5364bafc81a4a013068c87d1 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -143,9 +143,8 @@ Section ghostcell.
iIntros (?????) "#Hκ H".
iDestruct "H" as (γ) "[#? H]".
iDestruct "H" as (κ'') "[? ?]".
- iExists _. iFrame "#".
- iExists κ''.
- by iSplit; first iApply lft_incl_trans.
+ iFrame "∗#".
+ by iApply lft_incl_trans.
Qed.
Global Instance ghosttoken_wf α : TyWf (ghosttoken α) :=
@@ -431,10 +430,8 @@ Section ghostcell.
iExists l, vl.
iSplit; first done.
simpl_subst.
- iFrame.
- iSplit; first by refine (match vl with Vector.nil => _ end).
- iExists γ.
- by iFrame "Hidx Hown".
+ iFrame "∗#".
+ by refine (match vl with Vector.nil => _ end).
+ iIntros (r) "Hna Hf Hown".
simpl_subst.
iDestruct ("Hcloseα" with "[Hf]") as "[Htok Hf]"; [by rewrite (right_id static)|].
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index e0830e404c098a6969865f883e08cd1b39f738bc..9b89451b816d9f2649a3cf227c7927bab8780b40 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -161,8 +161,8 @@ Section code.
with "[] LFT HE Hna HL Hk"); last first.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
- iFrame. iSplitL "Hx".
- - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
+ iFrame. iSplitR.
+ - simpl. by rewrite vec_to_list_length.
- iExists (#false :: vl). rewrite heap_pointsto_vec_cons. iFrame; eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -199,10 +199,8 @@ Section code.
with "[] LFT HE Hna HL Hk"); last first.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
- iFrame. iSplitR "Hm0 Hm".
- - iExists _. iFrame.
- - iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
- rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+ iFrame. iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
+ rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index cc75fa98b3dbb126aa9b537b1ef2c2cc41b5473b..f2af7f3adbbe63efbc6f38b3081ed95f670943fb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -161,8 +161,7 @@ Section rc.
{ by apply auth_both_valid_discrete. }
iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
with "[Ha Hν2 Hl'1 Hl'2 H†HPend]") as "#?".
- { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. iExists _.
- iFrame "#∗". rewrite Qp.div_2; auto. }
+ { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. rewrite Qp.div_2; auto. }
iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
by iApply type_incl_refl. }
@@ -322,8 +321,8 @@ Section code.
iSplitL "Hty".
{ iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
by iApply "Hinclo". }
- iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame. iExists _.
- iFrame. rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+ iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame.
+ rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
by iFrame.
* iIntros "Hl1".
iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
@@ -375,7 +374,7 @@ Section code.
{ apply auth_update_dealloc.
rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
apply (cancel_local_update_unit _ (_, _)). }
- iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
+ iApply "Hclose". iFrame "Hst Hl2 Hl†Hna Hν†". iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
{ rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
@@ -537,10 +536,9 @@ Section code.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lrc â— box (rc ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦".
- { iExists _. rewrite uninit_own. auto. }
+ iSplitR; first done.
iNext. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
- rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
+ rewrite freeable_sz_full_S. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -1083,8 +1081,8 @@ Section code.
iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
iSplitR; first by iApply type_incl_refl.
iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
- iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
- iExists _. iFrame. by rewrite Qp.div_2. }
+ iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _.
+ do 2 iFrame. by rewrite Qp.div_2. }
iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
@@ -1125,7 +1123,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
!tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
- unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
+ unfold rc_persist, tc_opaque. iFrame "∗#". }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
iApply type_let.
{ apply rc_drop_type. }
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 569e39ca82ea36b0c84e3579e6f71148c0e3c49f..9a1c5996bc3c1b9faa9291e5693f500509615598 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -406,18 +406,16 @@ Section code.
destruct st as [[[q'' strong]| |]|]; [..|done|].
- iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
- iExists _. iFrame. iExists _. iFrame.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
- iExists _. iDestruct "Hrcst" as "[Hlw >$]". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
- iExists _. iFrame. simpl.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
- iExists _. iDestruct "Hrcst" as "(>Hlw & >$ & >H†& >H)". destruct weakc.
+ iLeft. iSplitR; first done. iMod ("Hclose" with "[$Hna Hrcâ—]") as "$".
{ iExists _. iFrame. }
rewrite Hszeq. auto with iFrame.
+ iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
- iFrame. iExists _. iFrame.
+ iFrame.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
- subst. wp_read. wp_let. wp_op. wp_if.
iApply (type_type _ _ _ [ w â— box (uninit 1); #lw â— box (uninit (2 + ty.(ty_size))) ]
@@ -475,7 +473,7 @@ Section code.
iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
- iExists _. iFrame. rewrite vec_to_list_length. auto. }
+ rewrite vec_to_list_length. auto. }
iApply type_jump; solve_typing.
Qed.
End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 2c381d7cfbebd4df64b370099078387abf758351..c3402c9fdf48ab4e187aac7b55b5d501ed95a1c7 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -82,16 +82,14 @@ Section ref_functions.
iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
iMod ("Hcloseδ" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
- iFrame. iExists _. iFrame.
- rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
+ iFrame. rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
iApply (type_type _ _ _
[ x ◠box (&shr{α}(ref β ty)); #lr ◠box(ref β ty)]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. simpl.
- iExists _, _, _, _, _. iFrame "∗#". }
+ rewrite /= freeable_sz_full. iFrame "∗#". simpl. iFrame "∗#". }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -171,7 +169,7 @@ Section ref_functions.
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply cancel_local_update_unit, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
+ - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame "Hshr H†".
iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
{ rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
by rewrite Pos.add_1_l Pos.pred_succ. }
@@ -350,8 +348,7 @@ Section ref_functions.
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
iMod ("Hclosena" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
- iFrame. iExists _. iFrame.
- rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
+ iFrame. rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefs ◠box (Π[ref α ty1; ref α ty2]) ]
with "[] LFT HE Hna HL Hk"); first last.
@@ -360,7 +357,7 @@ Section ref_functions.
rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton !shift_loc_assoc.
iFrame. iExists [_;_], [_;_]. iSplit=>//=.
iSplitL "Hν H◯"; [by auto 10 with iFrame|]. iExists [_;_], [].
- iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
+ iSplitR=>//=. rewrite right_id. by iFrame "∗#". }
iApply type_jump; solve_typing.
Qed.
End ref_functions.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 68237cf7293ab661b13644d065952dc9b36bd7f1..bff7a76bbf4c71ffbfee4fe58fd28116b3548c24 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -36,9 +36,8 @@ Section refcell_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (refcell ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=.
- iFrame. iSplitL "Hx↦".
- - iExists _. rewrite uninit_own. auto.
- - simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
+ iFrame. iSplitR; first done.
+ simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. by iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -70,10 +69,8 @@ Section refcell_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iSplitR "Hr↦ Hx".
- - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
- rewrite /= vec_to_list_length. auto.
- - iExists vl. iFrame. }
+ iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
+ by rewrite /= vec_to_list_length. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -109,8 +106,7 @@ Section refcell_functions.
iApply (type_type _ _ _
[ #lx ◠box (uninit 1); #(lx' +ₗ 1) ◠&uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iNext. iExists _. rewrite uninit_own. iFrame. }
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -189,7 +185,7 @@ Section refcell_functions.
- done. }
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
- iExists _. iFrame. rewrite -(assoc Qp.add) Qp.div_2 //.
+ rewrite -(assoc Qp.add) Qp.div_2 //.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index a5f24d8aba1498abf72b14e3794c1cad5bda255c..095a0f2641b9eedd5f020bf0e4be0d03a1ef4267 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -148,7 +148,7 @@ Section refmut_functions.
apply (cancel_local_update_unit (writing_stR q _)), _. }
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
- last (rewrite pos_op_add; lia). iFrame.
+ last (rewrite pos_op_add; lia). iFrame "H↦lrc H†".
iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
@@ -325,7 +325,7 @@ Section refmut_functions.
iMod ("Hclosena" with "[Hlrc H◠Hν1 H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, true, _, _)).
rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
- iFrame. iSplitL; [|done]. iExists _. iFrame.
+ iFrame.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefmuts ◠box (Π[refmut α ty1; refmut α ty2]) ]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 24bb58414b436d9414e4fd7c00fbfa8b5385e1da..9676e30c513b4d7f8af158d956829c7348ab7b14 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -164,7 +164,7 @@ Section rwlock.
rewrite Qp.div_2. iSplitL; last by auto.
iIntros "!> !> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
- iMod (own_alloc (◠writing_st)) as (γ) "Hst". { by apply auth_auth_valid. }
- iFrame. iExists _, _. eauto with iFrame.
+ by iFrame.
Qed.
Next Obligation.
iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index f3038b00d7082c6d4718dc3901f31f0b7d21a64f..9e7068bb34612c66adc1a67981681729612a99f2 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -38,9 +38,8 @@ Section rwlock_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (rwlock ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦".
- - iExists _. rewrite uninit_own. auto.
- - iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
+ iSplitR; first done.
+ iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -73,9 +72,7 @@ Section rwlock_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iSplitR "Hr↦ Hx".
- - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto.
- - iExists vl. iFrame. }
+ iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -109,8 +106,7 @@ Section rwlock_functions.
iApply (type_type _ _ _
[ #lx ◠box (uninit 1); #(lx' +ₗ 1) ◠&uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iNext. iExists _. rewrite uninit_own. iFrame. }
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -196,8 +192,8 @@ Section rwlock_functions.
- apply frac_valid. rewrite /= -Hqq' comm_L.
by apply Qp.add_le_mono_l, Qp.div_le.
- done. }
- iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
- iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
+ iFrame "∗#". rewrite Z.add_comm /=. iFrame.
+ iSplitR; first by rewrite /= Hag agree_idemp.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first solve_ndisj.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
@@ -219,8 +215,8 @@ Section rwlock_functions.
#lx ◠rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame.
- iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
+ tctx_hasty_val' //. iFrame "∗#".
+ iApply ty_shr_mono; last done.
iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
@@ -294,7 +290,7 @@ Section rwlock_functions.
#lx ◠rwlockwriteguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame. iExists _, _, _. iFrame "∗#". }
+ tctx_hasty_val' //. iFrame "∗#". }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 3c51bb4377a3d94be21fe9201959378567974cd0..833d6fb42b41a8b665ece311e2e808d694d04638 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -44,7 +44,7 @@ Section code.
iApply (type_call_iris _ [Ï] () [_; _]
with "LFT HE Hna [HÏ] Hf' [Henv Htl Htl†Hx'vl]"); [solve_typing| | |].
{ by rewrite /= (right_id static). }
- { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
+ { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. }
(* Prove the continuation of the function call. *)
iIntros (r) "Hna HÏ Hr". simpl.
iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
@@ -60,7 +60,7 @@ Section code.
iApply (type_type _ _ _ [ x â— _; #lr â— box (uninit ty.(ty_size)) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+ unlock. iFrame. auto using vec_to_list_length. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0c315e44cef0434e5c919eb8c920ab36f75f7543..4c5e65a2f64cbe8576a98d858b0da8d1c787660e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -196,8 +196,7 @@ Section util.
- iIntros "Hown". destruct v as [[|l|]|]; try done.
iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_pointsto_ty_own.
iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
- - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
- iFrame. iExists _. iFrame.
+ - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v. iFrame.
Qed.
Lemma ownptr_uninit_own n m tid v :
@@ -225,7 +224,7 @@ Section typing.
rewrite typed_write_eq. iIntros (Hsz) "!>".
iIntros ([[]|] tid F qmax qL ?) "_ _ $ Hown"; try done.
rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
- iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
+ iDestruct (ty_size_eq with "Hown") as "#>%". iFrame. auto.
Qed.
Lemma read_own_copy E L ty n :
@@ -233,9 +232,9 @@ Section typing.
Proof.
rewrite typed_read_eq. iIntros (Hsz) "!>".
iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
- iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
- iExists _. auto.
+ iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+ iExists l, _, _. iSplitR; first done.
+ iFrame "∗#"; auto.
Qed.
Lemma read_own_move E L ty n :
@@ -243,10 +242,11 @@ Section typing.
Proof.
rewrite typed_read_eq. iModIntro.
iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
- iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
+ iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
- iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
- iExists _. iFrame. done.
+ iExists l, vl, _. iSplitR; first done.
+ iFrame; auto.
+ by iIntros "!> $".
Qed.
Lemma type_new_instr {E L} (n : Z) :
@@ -257,8 +257,7 @@ Section typing.
iIntros (? tid qmax) "#LFT #HE $ $ _".
iApply wp_new; try done. iModIntro.
iIntros (l) "(H†& Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
- iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
- iExists (repeat #☠(Z.to_nat n)). iFrame. by rewrite /= repeat_length.
+ iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame. by rewrite /= repeat_length.
Qed.
Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 7d4bf78f23291f13fc3ec19f526c430baa3af303..f647f477746ea2c11eed783e167fd01f6b174cc7 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -44,7 +44,7 @@ Section product.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
rewrite heap_pointsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
- iFrame. iExists _, _. by iFrame.
+ by iFrame.
Qed.
Program Definition product2 (ty1 ty2 : type) :=
@@ -201,10 +201,10 @@ Section typing.
iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
- iExists _, _. iSplit; first by rewrite assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first by rewrite assoc. by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit; first by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first by rewrite -assoc. by iFrame.
- iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
by iFrame.
- iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index b652d36f65b191b0e995cd5bdc779e39fd20a6de..f575e1aa0987b0eb8631c3cc253f635b5ba5bd8e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -78,8 +78,7 @@ Section product_split.
rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
last by rewrite tctx_interp_singleton.
- rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
- iExists #l. iSplit; done.
+ rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. by iFrame.
Qed.
(** Owned pointers *)
@@ -96,9 +95,9 @@ Section product_split.
iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
iDestruct (ty_size_eq with "H1") as "#>EQ".
iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
- + iExists _. iFrame "#∗". iExists _. by iFrame.
+ + iExists _. by iFrame "#∗".
+ iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
- iFrame. iExists _. by iFrame.
+ by iFrame.
Qed.
Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
@@ -113,9 +112,8 @@ Section product_split.
rewrite HÏ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
- iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app. iFrame.
- iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
- rewrite {3}/ty_own /=. auto 10 with iFrame.
+ iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app.
+ iDestruct (ty_size_eq with "H1") as "#>->". by iFrame.
Qed.
Lemma tctx_split_own_prod E L n tyl p :
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 17b45d45078f838259e19c74abcc191adec9ed35..2d8fb4de5ab669b851fd9b4ee617bc0053f90e32 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -48,7 +48,7 @@ Section sum.
iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
iExists (#i::vl'++vl'').
rewrite heap_pointsto_vec_cons heap_pointsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
- iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
+ iFrame. iExists vl''. iSplit; first done. iPureIntro.
simpl. f_equal. by rewrite app_length Hvl'.
Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 1ccdfae180671778998b808f411c7a049fae5f09..c1efe2657b0f0c0ab013111e90f511cf76febbe8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -39,7 +39,7 @@ Section case.
iFrame. auto.
+ eauto with iFrame.
+ rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc_nat.
- iFrame. iExists _. iFrame. auto.
+ by iFrame.
- rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
iExists (#i :: vl' ++ vl''). iNext. rewrite heap_pointsto_vec_cons heap_pointsto_vec_app.
iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
@@ -265,10 +265,8 @@ Section case.
{ iApply "HLclose". by iFrame. }
iNext.
rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
- iSplitL "H↦pad".
- - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
- iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
- - iExists _. iFrame.
+ rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia. iFrame.
+ rewrite /= drop_length. iPureIntro. lia.
Qed.
Lemma type_sum_memcpy {E L} sty tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e: