From 0649227a2c2d82387d742bcc3d6d142d3159e106 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Nov 2023 07:33:42 +0100
Subject: [PATCH] update dependencies
---
coq-lambda-rust.opam | 2 +-
theories/typing/base.v | 24 +++----
theories/typing/borrow.v | 6 +-
theories/typing/lib/arc.v | 64 +++++++++----------
theories/typing/lib/brandedvec.v | 16 ++---
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/fake_shared.v | 4 +-
theories/typing/lib/mutex/mutex.v | 24 +++----
theories/typing/lib/mutex/mutexguard.v | 12 ++--
theories/typing/lib/rc/rc.v | 52 +++++++--------
theories/typing/lib/rc/weak.v | 28 ++++----
theories/typing/lib/refcell/ref_code.v | 38 +++++------
theories/typing/lib/refcell/refcell.v | 4 +-
theories/typing/lib/refcell/refcell_code.v | 20 +++---
theories/typing/lib/refcell/refmut_code.v | 36 +++++------
theories/typing/lib/rwlock/rwlock.v | 4 +-
theories/typing/lib/rwlock/rwlock_code.v | 12 ++--
.../typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 4 +-
theories/typing/lib/take_mut.v | 2 +-
theories/typing/own.v | 8 +--
theories/typing/product.v | 10 +--
theories/typing/product_split.v | 4 +-
theories/typing/programs.v | 8 +--
theories/typing/sum.v | 10 +--
theories/typing/type.v | 4 +-
theories/typing/type_sum.v | 26 ++++----
theories/typing/uniq_bor.v | 2 +-
28 files changed, 214 insertions(+), 214 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index aed9d929..5860f96e 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2023-10-14.0.18d22854") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2023-11-06.0.fdf1fcba") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/typing/base.v b/theories/typing/base.v
index 8340847e..f81e7fff 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -59,15 +59,15 @@ Notation shift_loc_0 := shift_0.
Notation shift_loc_assoc := shift_lblock_assoc.
Notation shift_loc_assoc_nat := shift_nat_assoc.
-Notation heap_mapsto_agree := own_loc_na_agree.
-
-Notation heap_mapsto_vec := own_loc_na_vec.
-Notation heap_mapsto_vec_nil := own_loc_na_vec_nil.
-Notation heap_mapsto_vec_cons := own_loc_na_vec_cons.
-Notation heap_mapsto_vec_singleton := own_loc_na_vec_singleton.
-Notation heap_mapsto_vec_app := own_loc_na_vec_app.
-Notation heap_mapsto_vec_combine := own_loc_na_vec_combine.
-
-Notation heap_mapsto_pred_wand := own_loc_na_pred_wand.
-Notation heap_mapsto_pred_combine := own_loc_na_pred_combine.
-Notation heap_mapsto_pred_iff_proper := own_loc_na_pred_iff_proper.
+Notation heap_pointsto_agree := own_loc_na_agree.
+
+Notation heap_pointsto_vec := own_loc_na_vec.
+Notation heap_pointsto_vec_nil := own_loc_na_vec_nil.
+Notation heap_pointsto_vec_cons := own_loc_na_vec_cons.
+Notation heap_pointsto_vec_singleton := own_loc_na_vec_singleton.
+Notation heap_pointsto_vec_app := own_loc_na_vec_app.
+Notation heap_pointsto_vec_combine := own_loc_na_vec_combine.
+
+Notation heap_pointsto_pred_wand := own_loc_na_pred_wand.
+Notation heap_pointsto_pred_combine := own_loc_na_pred_combine.
+Notation heap_pointsto_pred_iff_proper := own_loc_na_pred_iff_proper.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 7646e4a1..9d44fb8e 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -93,7 +93,7 @@ Section borrow.
wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". { done. }
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
- iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
+ iDestruct "Hown" as "[Hown H†]". rewrite heap_pointsto_vec_singleton -wp_fupd. wp_read.
iMod ("Hclose'" $! (_↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
@@ -102,7 +102,7 @@ Section borrow.
iDestruct ("HLclose" with "HL") as "$".
by rewrite tctx_interp_singleton tctx_hasty_val' //=.
- iIntros "!>(?&?&?)!>". iNext. iExists _.
- rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
+ rewrite -heap_pointsto_vec_singleton. iFrame. by iFrame.
- iFrame.
Qed.
@@ -157,7 +157,7 @@ Section borrow.
destruct vl as [|[[]|][]];
try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". { done. }
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
iApply wp_fupd. wp_read.
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 539b417f..8cd1ecb5 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -165,7 +165,7 @@ Section arc.
iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- setoid_rewrite heap_mapsto_vec_singleton.
+ setoid_rewrite heap_pointsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -241,7 +241,7 @@ Section arc.
- iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H†& Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
- iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
+ iFrame. iApply (heap_pointsto_pred_wand with "Hc"). iApply "Hoincl". }
iDestruct "Hvl" as (???? ν t q) "(#Hpersist & Htk & Hν)".
iRight. iExists _,_,_,_,_,_,_. iFrame "#∗". by iApply arc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -304,7 +304,7 @@ Section arc.
iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- setoid_rewrite heap_mapsto_vec_singleton.
+ setoid_rewrite heap_pointsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -422,11 +422,11 @@ Section arc.
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
iDestruct (ownptr_uninit_own with "Hrcbox")
as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
rewrite shift_loc_assoc.
iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
- inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+ inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -437,7 +437,7 @@ Section arc.
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.
- iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iLeft.
+ iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -462,11 +462,11 @@ Section arc.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrc [Hrcbox _]]". rewrite !tctx_hasty_val.
iDestruct (ownptr_uninit_own with "Hrcbox")
as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
rewrite shift_loc_assoc.
iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
- inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+ inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
@@ -476,7 +476,7 @@ Section arc.
iApply (type_type _ _ _ [ #lrc â— box (weak ty)]
with "[] LFT HE Hna HL Hk [>-]"); last first.
{ rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
- iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
with "Hrcbox↦0 Hrcbox↦1 [-]") as (γi γs γw γsw t q) "[Ha Htok]".
{ rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
@@ -504,7 +504,7 @@ Section arc.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
rewrite !tctx_hasty_val [[rcx]]lock.
iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
- subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
+ subst x. inv_vec vlrc2=>?. rewrite heap_pointsto_vec_singleton.
destruct rc' as [[|rc'|]|]; try done. simpl of_val.
iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
(* All right, we are done preparing our context. Let's get going. *)
@@ -523,7 +523,7 @@ Section arc.
iApply (type_type _ _ _ [ rcx ◠box (&shr{α}(arc ty)); #lrc2 ◠box (&shr{α}ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_pointsto_vec_singleton.
iFrame "Hx". by iApply ty_shr_mono. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -868,7 +868,7 @@ Section arc.
rewrite {3}[option]lock. simpl. rewrite -{2 3}lock. (* FIXME: Tried using contextual pattern, did not work. *)
iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
first by iDestruct "Hown" as (???) "[>% ?]".
- rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
+ rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver|].
@@ -881,15 +881,15 @@ Section arc.
iIntros "[? Hrc']". wp_seq.
wp_apply (drop_fake_spec with "[//] [$Hdrop Hrc' H†] "); [solve_ndisj|..].
{ unfold P2. auto with iFrame. } unlock. iIntros ([]); last first.
- { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
+ { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Nat.max_0_r.
auto 10 with iFrame. }
iIntros "([H†H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
wp_apply (wp_delete _ _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]"); [done|..].
{ simpl. lia. }
- { rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
- iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+ { rewrite 2!heap_pointsto_vec_cons shift_loc_assoc. auto with iFrame. }
+ iFrame. iIntros "_". iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame.
iExists 1%nat, _, []. rewrite right_id_L. iFrame. iSplit; [by auto|simpl].
auto with lia. }
iIntros (?) "Hr". wp_seq.
@@ -927,7 +927,7 @@ Section arc.
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ _ (_::_::vl) with "[-]"); [done|simpl;lia| |done].
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc. iFrame. }
iIntros (?) "_". wp_seq.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (uninit 0) ]
@@ -975,13 +975,13 @@ Section arc.
iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
iDestruct "Hown" as ">Hlen".
destruct vl0 as [|? vl0]=>//; iDestruct "Hlen" as %[=Hlen0].
- rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
+ rewrite heap_pointsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [done..|set_solver+|].
iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
- rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
+ rewrite -(firstn_skipn ty.(ty_size) vl0) heap_pointsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
iDestruct (ty_size_eq with "Hown") as %Hlen.
wp_apply (wp_memcpy with "[$Hr1 $Hrc']"); [done|..];
@@ -994,14 +994,14 @@ Section arc.
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ _ (_::_::vl') with "[-]"); [done|simpl; lia| |done].
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc. iFrame. }
iIntros (?) "_". wp_seq.
iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #r ◠box (Σ[ ty; arc ty ]) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ 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_mapsto_vec_app
- -heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+ rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
+ -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
rewrite app_length drop_length. lia. }
iApply type_delete; [solve_typing..|].
@@ -1046,7 +1046,7 @@ Section arc.
iMod (bor_sep with "LFT Hrc'") as "[Hrc'↦ Hrc]"=>//.
destruct rcvl as [|[[|rc|]|][|]]; try by
iMod (bor_persistent with "LFT Hrc Hα") as "[>[] ?]".
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iMod (bor_acc with "LFT Hrc'↦ Hα") as "[Hrc'↦ Hclose2]"=>//. wp_read.
iMod ("Hclose2" with "Hrc'↦") as "[_ Hα]".
iMod (bor_acc_cons with "LFT Hrc Hα") as "[Hrc Hclose2]"=>//. wp_let.
@@ -1136,7 +1136,7 @@ Section arc.
iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"=>//.
iDestruct "Hrc'" as (rcvl) "[Hrc'↦ Hrc]".
destruct rcvl as [|[[|rc|]|][|]]; try by iDestruct "Hrc" as ">[]".
- rewrite heap_mapsto_vec_singleton. wp_read.
+ rewrite heap_pointsto_vec_singleton. wp_read.
iAssert (shared_arc_own rc ty tid)%I with "[>Hrc]" as "Hrc".
{ iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
iDestruct "Hrc" as (γi γs γw γsw ν t q') "[#(Hi & Hs & #Hc) [Htok1 Htok2]]". wp_let.
@@ -1148,7 +1148,7 @@ Section arc.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
- { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ { iIntros "!> Hrc2". iExists [_]. rewrite heap_pointsto_vec_singleton.
iFrame. iLeft. by iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
iApply (type_type _ _ _ [ rcx ◠box (uninit 1); #(rc +ₗ 2) ◠&uniq{α}ty;
@@ -1163,7 +1163,7 @@ Section arc.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
wp_apply wp_new=>//; [set_solver+|lia|].
iIntros (l) "(H†& Hlvl & Hml) (#Hν & Hown & H†') !>". rewrite -!lock Nat2Z.id.
- wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+ wp_let. wp_op. rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %Hsz.
@@ -1172,7 +1172,7 @@ Section arc.
iIntros "[H↦ H↦']". wp_seq. wp_write.
iMod ("Hclose2" $! ((l +ₗ 2) ↦∗: ty_own ty tid)%I
with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
- { iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ { iIntros "!> H↦". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
iApply (type_type _ _ _ [ rcx ◠box (uninit 1); (#l +ₗ #2) ◠&uniq{α}ty;
@@ -1185,7 +1185,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
iIntros (l) "/= (H†& Hl & Hm)". wp_let. wp_op.
- rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
+ rewrite heap_pointsto_vec_singleton. wp_write. wp_let.
wp_bind (of_val clone).
iApply (wp_wand with "[Hna]").
{ iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna"); rewrite /llctx_interp /tctx_interp //. }
@@ -1196,7 +1196,7 @@ Section arc.
iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_] with
"LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
@@ -1205,7 +1205,7 @@ Section arc.
wp_apply wp_new=>//. { lia. }
iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
- rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [done|..].
{ by rewrite repeat_length. } { by rewrite Hsz. }
@@ -1215,7 +1215,7 @@ Section arc.
iIntros "_". wp_seq. wp_write.
iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
"[Hrc'↦ Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
- { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ { iIntros "!> H". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
{ iExists _. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index d2d8fc0f..52971aaf 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -141,8 +141,8 @@ Section brandedvec.
{ iNext. iDestruct (ty_size_eq with "Hown'") as %->. done. }
destruct vl' as [|v' vl']; first done.
destruct vl' as [|]; last first. { simpl in *. lia. }
- rewrite !heap_mapsto_vec_singleton.
- iDestruct (heap_mapsto_agree with "Hmt1 Hmt2") as %->.
+ rewrite !heap_pointsto_vec_singleton.
+ iDestruct (heap_pointsto_agree with "Hmt1 Hmt2") as %->.
iCombine "Hmt1" "Hmt2" as "Hmt".
iApply "Hclose". done.
Qed.
@@ -187,7 +187,7 @@ Section typing.
wp_case.
wp_alloc n as "Hm" "Hn" "Hdead".
wp_let.
- rewrite !heap_mapsto_vec_singleton.
+ rewrite !heap_pointsto_vec_singleton.
wp_write.
iAssert (∀ E : coPset, ⌜↑lftN ⊆ E⌠→
|={E}=> ∃ α, tctx_elt_interp tid ((LitV n : expr) ◠box (brandvec α)) ∗ 1.[α])%I
@@ -198,7 +198,7 @@ Section typing.
iExists α.
rewrite !tctx_hasty_val.
rewrite ownptr_own.
- rewrite -heap_mapsto_vec_singleton.
+ rewrite -heap_pointsto_vec_singleton.
iFrame "Htok".
iExists n, (Vector.cons (LitV 0) Vector.nil).
iSplitR; first done.
@@ -277,7 +277,7 @@ Section typing.
iDestruct "Hv'" as (m) "#[Hghost Hmem]".
iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
iMod (frac_bor_acc with "LFT Hmem Hβ") as (qβ') "[>Hn'↦ Hcloseβ]"; first done.
- rewrite !heap_mapsto_vec_singleton.
+ rewrite !heap_pointsto_vec_singleton.
wp_read.
iMod ("Hcloseβ" with "Hn'↦") as "Hβ".
wp_op.
@@ -342,7 +342,7 @@ Section typing.
iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "((Hβ1 & Hβ2 & Hβ3) & HL & Hclose)"; [solve_typing..|].
iMod (frac_bor_acc with "LFT Hn Hβ1") as (qβn) "[>Hn↦ Hcloseβ1]"; first solve_ndisj.
iMod (frac_bor_acc with "LFT Hm Hβ2") as (qβm) "[>Hm↦ Hcloseβ2]"; first solve_ndisj.
- rewrite !heap_mapsto_vec_singleton.
+ rewrite !heap_pointsto_vec_singleton.
wp_read.
wp_op.
wp_read.
@@ -390,7 +390,7 @@ Section typing.
iMod (bor_acc with "LFT Hn Hβ") as "[H↦ Hclose']"; first solve_ndisj.
iDestruct "H↦" as (vl) "[> H↦ Hn]".
iDestruct "Hn" as (n) "[Hn > %]". simplify_eq.
- rewrite !heap_mapsto_vec_singleton.
+ rewrite !heap_pointsto_vec_singleton.
wp_read.
wp_let.
wp_op.
@@ -404,7 +404,7 @@ Section typing.
iDestruct "Hlb" as "#Hlb".
iMod ("Hclose'" with "[H↦ Hidx Hown]") as "[Hn Hβ]".
{ iExists (#(n+1)::nil).
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iFrame "∗".
iIntros "!>".
iExists (n + 1)%nat.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 03d565f0..4bcf5adf 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -64,7 +64,7 @@ Section cell.
{ iExists vl. by iFrame. }
iModIntro. iSplitL "".
{ iNext. iExists vl. destruct vl; last done. iFrame "Hown".
- by iApply heap_mapsto_vec_nil. }
+ by iApply heap_pointsto_vec_nil. }
by iIntros "$ _". }
(* Now we are in the non-0 case. *)
iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 4efaf32f..a9aefbaf 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -23,7 +23,7 @@ Section fake_shared.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
- rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+ rewrite heap_pointsto_vec_singleton. iSplit; auto. }
iDestruct "H" as "#H". iIntros "!> * % $".
iApply step_fupd_intro. { set_solver. }
simpl. iApply ty_shr_mono; last done.
@@ -55,7 +55,7 @@ Section fake_shared.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
- rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+ rewrite heap_pointsto_vec_singleton. iSplit; auto. }
iDestruct "H" as "#H". iIntros "!> * % $".
iApply step_fupd_intro. { set_solver. }
simpl. iApply ty_shr_mono; last done.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index ffd35d9d..7102dfbf 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -41,7 +41,7 @@ Section mutex.
iIntros (ty E κ l tid q ?) "#LFT Hbor Htok".
iMod (bor_acc_cons with "LFT Hbor Htok") as "[H Hclose]"; first done.
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ [#hInv H]]"; try iDestruct "H" as ">[]".
- rewrite heap_mapsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
+ rewrite heap_pointsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]".
iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
(* We need to turn the ohne borrow into two, so we close it -- and then
we open one of them again. *)
@@ -49,7 +49,7 @@ Section mutex.
with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
{ clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
- rewrite heap_mapsto_vec_cons. iFrame "∗ hInv". iPureIntro. eauto. }
+ rewrite heap_pointsto_vec_cons. iFrame "∗ hInv". iPureIntro. eauto. }
{ iNext. iSplitL "Hl"; first by eauto.
iExists vl. iFrame. }
clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done.
@@ -94,7 +94,7 @@ Section mutex.
iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
iExists γ.
iApply lock_proto_iff_proper; [|iFrame].
- iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
+ iApply bor_iff_proper. iApply heap_pointsto_pred_iff_proper.
iNext. iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
Qed.
@@ -115,7 +115,7 @@ Section mutex.
iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
iExists γ. iApply lock_proto_iff_proper; [|iFrame].
- iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
+ iApply bor_iff_proper. iApply heap_pointsto_pred_iff_proper.
iNext. iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
Qed.
End mutex.
@@ -144,9 +144,9 @@ Section code.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hm [Hx _]]".
rewrite !tctx_hasty_val /=.
iDestruct (ownptr_uninit_own with "Hm") as (lm vlm) "(% & Hm & Hm†)".
- subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+ subst m. inv_vec vlm=>m vlm. simpl. iDestruct (heap_pointsto_vec_cons with "Hm") as "[Hm0 Hm]".
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
- iDestruct (heap_mapsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
+ iDestruct (heap_pointsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
(* All right, we are done preparing our context. Let's get going. *)
wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [done|by rewrite vec_to_list_length..|].
iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
@@ -158,7 +158,7 @@ Section code.
{ 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.
- - iExists (#false :: vl). rewrite heap_mapsto_vec_cons.
+ - iExists (#false :: vl). rewrite heap_pointsto_vec_cons.
iFrame "∗ HINV". eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -182,9 +182,9 @@ Section code.
iDestruct (ownptr_uninit_own with "Hx") as (lx vlx) "(% & Hx & Hx†)".
subst x. simpl.
destruct m as [[|lm|]|]; try done. iDestruct "Hm" as "[Hm Hm†]".
- iDestruct (heap_mapsto_ty_own with "Hm") as (vlm) "[>Hm [#HINV Hvlm]]".
+ iDestruct (heap_pointsto_ty_own with "Hm") as (vlm) "[>Hm [#HINV Hvlm]]".
inv_vec vlm=>m vlm. destruct m as [[|m|]|]; try by iDestruct "Hvlm" as ">[]".
- simpl. iDestruct (heap_mapsto_vec_cons with "Hm") as "[Hm0 Hm]".
+ simpl. iDestruct (heap_pointsto_vec_cons with "Hm") as "[Hm0 Hm]".
iDestruct "Hvlm" as "[_ Hvlm]".
(* All right, we are done preparing our context. Let's get going. *)
wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [done|by rewrite vec_to_list_length..|].
@@ -197,7 +197,7 @@ Section code.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
iFrame. iSplitR "Hm0 Hm".
- iExists _. iFrame.
- - iExists (_ :: _). rewrite heap_mapsto_vec_cons. 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.
@@ -224,11 +224,11 @@ Section code.
iMod (bor_acc_cons with "LFT Hm' Hα") as "[Hm' Hclose2]"; first done.
wp_op. iDestruct "Hm'" as (vl) "[H↦ [#HINV Hm']]".
destruct vl as [|[[|m'|]|] vl]; try done. simpl.
- iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
+ iDestruct (heap_pointsto_vec_cons with "H↦") as "[H↦1 H↦2]".
iDestruct "Hm'" as "[% Hvl]".
iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
{ iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
- iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. iFrame "HINV". eauto. }
+ iExists (_ :: _). rewrite heap_pointsto_vec_cons. do 2 iFrame. iFrame "HINV". eauto. }
{ iExists vl. iFrame. }
iMod ("Hclose1" with "Hα HL") as "HL".
(* Switch back to typing mode. *)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 9b2ac252..e9304df7 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -49,7 +49,7 @@ Section mguard.
iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; [done|].
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- setoid_rewrite heap_mapsto_vec_singleton.
+ setoid_rewrite heap_pointsto_vec_singleton.
iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
iMod (bor_sep with "LFT H") as "[_ H]"; first done.
@@ -99,10 +99,10 @@ Section mguard.
+ iDestruct "Hinv" as (γ) "Hproto".
iExists γ. iApply lock_proto_lft_mono; first by iApply lft_incl_syn_sem.
iApply lock_proto_iff_proper; [|iFrame].
- iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
+ iApply bor_iff_proper. iNext. iApply heap_pointsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
+ iApply bor_iff; last done. iIntros "!>".
- iApply heap_mapsto_pred_iff_proper.
+ iApply heap_pointsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
@@ -165,7 +165,7 @@ Section code.
rewrite !tctx_hasty_val [[x]]lock /=.
destruct m as [[|lm|]|]; try done. iDestruct "Hm" as (κ') "[#Hακ' #Hshr]".
iDestruct (ownptr_uninit_own with "Hg") as (lg vlg) "(% & Hg & Hg†)".
- subst g. inv_vec vlg=>g. rewrite heap_mapsto_vec_singleton.
+ subst g. inv_vec vlg=>g. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
iDestruct "Hshr" as (γ) "Hshr".
@@ -177,7 +177,7 @@ 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' //.
- unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hg".
+ unlock. iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hg".
iExists _. iFrame "#∗". iExists _. iFrame "#". }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -207,7 +207,7 @@ Section code.
[solve_typing..|].
destruct vl as [|[[|lm|]|] [|]]; simpl;
try by iMod (bor_persistent with "LFT Hprot Hα") as "[>[] _]".
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 4eb224d6..eaf6cc42 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -136,7 +136,7 @@ Section rc.
iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- setoid_rewrite heap_mapsto_vec_singleton.
+ setoid_rewrite heap_pointsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -222,7 +222,7 @@ Section rc.
- iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H†& Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
- iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
+ iFrame. iApply (heap_pointsto_pred_wand with "Hc"). iApply "Hoincl". }
iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
iRight. iExists _, _, _. iFrame "#∗". by iApply rc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -531,11 +531,11 @@ Section code.
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
iDestruct (ownptr_uninit_own with "Hrcbox")
as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
rewrite shift_loc_assoc.
iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
- inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
+ inv_vec vlrc=>?. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -546,7 +546,7 @@ Section code.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
iSplitL "Hx↦".
{ iExists _. rewrite uninit_own. auto. }
- iNext. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iLeft.
+ iNext. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -573,7 +573,7 @@ Section code.
rewrite !tctx_hasty_val [[x]]lock.
destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
- subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+ subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
wp_bind (!_)%E.
@@ -613,7 +613,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
- rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
+ rewrite heap_pointsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -635,7 +635,7 @@ Section code.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
rewrite !tctx_hasty_val [[rcx]]lock.
iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
- subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton.
+ subst x. inv_vec vlrc2=>?. rewrite heap_pointsto_vec_singleton.
destruct rc' as [[|rc'|]|]; try done. simpl of_val.
iDestruct "Hrc'" as (l') "[Hrc' #Hdelay]".
(* All right, we are done preparing our context. Let's get going. *)
@@ -654,7 +654,7 @@ Section code.
iApply (type_type _ _ _ [ rcx ◠box (&shr{α}(rc ty)); #lrc2 ◠box (&shr{α}ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
+ unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_pointsto_vec_singleton.
iFrame "Hx". by iApply ty_shr_mono. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -734,7 +734,7 @@ Section code.
{ unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
rewrite shift_loc_0 /=. iFrame. iExists [_; _].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
auto with iFrame. }
iApply (type_delete (Î [uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
@@ -829,7 +829,7 @@ Section code.
{ unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
rewrite shift_loc_0 /=. iFrame. iExists [_; _].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
auto with iFrame. }
iApply (type_delete (Î [uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
@@ -892,8 +892,8 @@ Section code.
destruct rc' as [[|rc'|]|]; try done.
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
- iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
- inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
+ iDestruct (heap_pointsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+ inv_vec vl=>l. rewrite heap_pointsto_vec_singleton.
wp_read. destruct l as [[|l|]|]; try done.
wp_let. wp_op. rewrite shift_loc_0.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
@@ -906,7 +906,7 @@ Section code.
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
wp_op. iIntros "(Hl†& Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα]"; [|iNext; iExact "Hty"|].
- { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
+ { iIntros "!> Hty". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ r ◠box (uninit 2); #l +ₗ #2 ◠&uniq{α}ty;
@@ -919,7 +919,7 @@ Section code.
+ wp_op; case_bool_decide; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
{ iIntros "!> HX". iModIntro. iExact "HX". }
- { iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
+ { iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. auto. }
iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ r â— box (uninit 2); rcx â— box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -931,7 +931,7 @@ Section code.
iMod ("Hproto" with "Hl1") as "[Hna Hrc]".
iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
{ iIntros "!> HX". iModIntro. iExact "HX". }
- { iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
+ { iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. auto. }
iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ r â— box (uninit 2); rcx â— box (uninit 1)]
with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -1025,8 +1025,8 @@ Section code.
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
[solve_typing..|].
iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"; first solve_ndisj.
- iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
- inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
+ iDestruct (heap_pointsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+ inv_vec vl=>l. rewrite heap_pointsto_vec_singleton.
wp_read. destruct l as [[|l|]|]; try done. wp_let. wp_op. rewrite shift_loc_0.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
@@ -1038,7 +1038,7 @@ Section code.
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
wp_op. iIntros "(Hl†& Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
- { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
+ { iIntros "!> Hty". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
iApply (type_type _ _ _ [ r ◠box (uninit 1); #l +ₗ #2 ◠&uniq{α}ty;
@@ -1053,7 +1053,7 @@ Section code.
iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; [set_solver+|lia|done|].
rewrite -!lock Nat2Z.id.
iNext. iIntros (lr) "/= ([H†|%] & H↦lr & Hm) [Hty Hproto] !>"; last lia.
- rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
+ rewrite 2!heap_pointsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
wp_let. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. wp_op.
iDestruct "Hty" as (vlr) "[H↦vlr Hty]". rewrite shift_loc_assoc.
iDestruct (ty_size_eq with "Hty") as %Hsz.
@@ -1063,7 +1063,7 @@ Section code.
iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
iMod ("Hclose2" $! ((lr +ₗ 2) ↦∗: ty_own ty tid)%I
with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
- { iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ { iIntros "!> H !>". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iLeft. iFrame. }
{ iExists _. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
@@ -1078,7 +1078,7 @@ Section code.
iIntros (lr) "/= ([H†|%] & H↦lr & Hm)"; last lia.
iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
- rewrite heap_mapsto_vec_singleton. wp_write.
+ rewrite heap_pointsto_vec_singleton. wp_write.
iAssert (∃ γ ν q, rc_persist tid ν γ l ty ∗ ⎡own γ (rc_tok q)⎤ ∗ q.[ν])%I
with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
{ iDestruct "Hty" as "[(Hl1 & Hl2 & Hl†& Hl3)|Hty]"; last done.
@@ -1104,7 +1104,7 @@ Section code.
iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) [_]
with "LFT HE Hna Hαν Hclone [H†H↦lr]"); [solve_typing| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
@@ -1113,7 +1113,7 @@ Section code.
wp_apply wp_new=>//. { lia. }
iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
- rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]");
[by rewrite ?repeat_length ?Hsz //..|].
@@ -1123,7 +1123,7 @@ Section code.
iIntros "_". wp_seq. wp_write.
iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
"[Hrc' Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
- { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ { iIntros "!> H". iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
{ iExists _. iFrame. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4bf178dc..35fbe7be 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -32,7 +32,7 @@ Section weak.
iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- setoid_rewrite heap_mapsto_vec_singleton.
+ setoid_rewrite heap_pointsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct (monPred_in_intro with "Hb") as (V) "[#Hin Hb]".
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -146,7 +146,7 @@ Section code.
rewrite !tctx_hasty_val [[w]]lock.
destruct w' as [[|lw|]|]; try done. iDestruct "Hw'" as (l') "[#Hlw #Hshr]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
- subst r. inv_vec vlr=>r0 r1. rewrite !heap_mapsto_vec_cons.
+ subst r. inv_vec vlr=>r0 r1. rewrite !heap_pointsto_vec_cons.
iDestruct "Hr" as "(Hr1 & Hr2 & _)".
(* All right, we are done preparing our context. Let's get going. *)
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
@@ -188,7 +188,7 @@ Section code.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
unlock. iFrame "Hr†Hw". iSplitL "Hr1 Hr2".
- iExists [_;_].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame.
- iRight. auto with iFrame. }
iApply (type_sum_assign (option (rc ty))); [solve_typing..|].
iApply type_jump; solve_typing.
@@ -205,7 +205,7 @@ Section code.
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 heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame. }
iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
iApply type_jump; solve_typing.
- (* Failure : general case *)
@@ -221,7 +221,7 @@ Section code.
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 heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. auto with iFrame. }
iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -248,7 +248,7 @@ Section code.
rewrite !tctx_hasty_val [[x]]lock.
destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
- subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+ subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
wp_bind (!_)%E.
@@ -283,7 +283,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
- rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
+ rewrite heap_pointsto_vec_singleton /=. eauto 10 with iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -311,7 +311,7 @@ Section code.
rewrite !tctx_hasty_val [[x]]lock.
destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr & Hr†)".
- subst r. inv_vec vlr=>r. rewrite heap_mapsto_vec_singleton.
+ subst r. inv_vec vlr=>r. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)"; [solve_typing..|].
wp_bind (!_)%E.
@@ -355,7 +355,7 @@ Section code.
iApply (type_type _ _ _ [ x ◠box (&shr{α}(weak ty)); #lr ◠box (weak ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
+ unlock. iFrame. iExists [# #l']. rewrite heap_pointsto_vec_singleton /=.
auto 10 with iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -430,7 +430,7 @@ Section code.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
rewrite /= freeable_sz_full_S. iFrame. iExists (_::_::_).
- rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. iFrame.
+ rewrite 2!heap_pointsto_vec_cons shift_loc_assoc. iFrame.
iIntros "!> !%". simpl. congruence. }
iApply type_delete; [try solve_typing..|].
iApply type_jump; solve_typing.
@@ -461,10 +461,10 @@ Section code.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
"(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
- iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+ iDestruct (heap_pointsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
iDestruct (ownptr_uninit_own with "Hw") as (lw vlw) "(% & Hw↦ & Hw†)". subst w.
- inv_vec vlw=>?. rewrite heap_mapsto_vec_singleton.
+ inv_vec vlw=>?. rewrite heap_pointsto_vec_singleton.
(* All right, we are done preparing our context. Let's get going. *)
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
@@ -474,7 +474,7 @@ Section code.
iApply (type_type _ _ _ [ #lw â— box (weak ty)]
with "[] LFT HE Hna HL Hk [> -]"); last first.
{ rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
- iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+ iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iMod (own_alloc (◠_ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
{ apply auth_both_valid_discrete. by split. }
iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index ba589a06..c3db6221 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -62,7 +62,7 @@ Section ref_functions.
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iDestruct (refcell_inv_reading_inv with "INV Hâ—¯")
as (q' n) "(H↦lrc & _ & [H◠H◯] & H†& Hq' & Hshr')".
@@ -76,7 +76,7 @@ Section ref_functions.
by apply Qp.add_le_mono_l, Qp.div_le. }
wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr&?)".
iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I with "[H↦1 H↦2]" as "H↦".
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
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]".
@@ -116,7 +116,7 @@ Section ref_functions.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
@@ -150,7 +150,7 @@ Section ref_functions.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
try iDestruct "Hx" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
@@ -187,7 +187,7 @@ Section ref_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)] with "[] LFT HE Hna HL Hk");
first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton uninit_own. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
@@ -218,11 +218,11 @@ Section ref_functions.
iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
try iDestruct "Href" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
wp_read. wp_let. wp_apply wp_new; try done.
- iIntros (lx) "(H†& Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+ iIntros (lx) "(H†& Hlx & ?)". rewrite heap_pointsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
iMod (lctx_lft_alive_tok_noend Ï with "HE HL") as (?) "(HÏ & HL & Hclose2)";[solve_typing..|].
@@ -232,7 +232,7 @@ Section ref_functions.
iApply (type_call_iris _ [α ⊓ ν; Ï] (α ⊓ ν) [_; _]
with "LFT HE Hna [HανÏ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
iIntros ([[|r|]|]) "Hna HÎ±Î½Ï Hr //".
iDestruct ("Hclose4" with "HανÏ") as "[Hαν HÏ]".
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -240,14 +240,14 @@ Section ref_functions.
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as ([|r'[]]) "[Hr #Hr']";
try by iDestruct (ty_size_eq with "Hr'") as "%".
- rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+ rewrite heap_pointsto_vec_singleton. wp_read. wp_let.
wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
- { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+ { rewrite heap_pointsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
wp_seq. wp_write.
iApply (type_type _ [_] _ [ #lref ◠box (ref α ty2) ]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //. simpl. iFrame.
- iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iExists [_;_]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
iApply type_jump; solve_typing.
Qed.
@@ -297,11 +297,11 @@ Section ref_functions.
iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
try iDestruct "Href" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
wp_read. wp_let. wp_apply wp_new; [done..|].
- iIntros (lx) "(H†& Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+ iIntros (lx) "(H†& Hlx & ?)". rewrite heap_pointsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
iMod (lctx_lft_alive_tok_noend Ï with "HE HL") as (?) "(HÏ & HL & Hclose2)";[solve_typing..|].
@@ -311,7 +311,7 @@ Section ref_functions.
iApply (type_call_iris _ [α ⊓ ν; Ï] (α ⊓ ν) [_; _]
with "LFT HE Hna [HανÏ] Hf' [$Henv Hlx H†]"); [solve_typing|done| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
iIntros ([[|r|]|]) "Hna HÎ±Î½Ï Hr //".
iDestruct ("Hclose4" with "HανÏ") as "[Hαν HÏ]".
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -320,10 +320,10 @@ Section ref_functions.
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
@@ -341,10 +341,10 @@ Section ref_functions.
by apply Qp.add_le_mono_l, Qp.div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefs) "(Hrefs†& Hrefs & ?)".
- rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
+ rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton. wp_let.
iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
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]".
@@ -356,7 +356,7 @@ Section ref_functions.
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
simpl. iFrame. iExists [_;_;_;_].
- rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
+ 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. }
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5bc0bc91..193d6315 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -125,8 +125,8 @@ Section refcell.
(l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
{ iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "Hn".
iDestruct "Hvl" as (vl') "[H↦ Hvl]".
- iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame. }
- { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+ iExists (#n'::vl'). rewrite heap_pointsto_vec_cons. iFrame. }
+ { iNext. rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; eauto with iFrame. }
iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". { done. }
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index e745680a..f71cc563 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -28,7 +28,7 @@ Section refcell_functions.
iDestruct "HT" as "[Hr Hx]".
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
- inv_vec vlr=>??. iDestruct (heap_mapsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
+ inv_vec vlr=>??. iDestruct (heap_pointsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
iIntros "[Hr↦1 Hx↦]". wp_seq.
@@ -37,7 +37,7 @@ Section refcell_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=.
iFrame. iSplitL "Hx↦".
- iExists _. rewrite uninit_own. auto.
- - simpl. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame=>//=. }
+ - simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -62,7 +62,7 @@ Section refcell_functions.
iDestruct "HT" as "[Hr Hx]".
iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
inv_vec vlx=>-[[|?|?]|????] vl; simpl; try iDestruct "Hx" as ">[]".
- iDestruct (heap_mapsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
+ iDestruct (heap_pointsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
iIntros "[Hr↦ Hx↦1]". wp_seq.
@@ -70,7 +70,7 @@ Section refcell_functions.
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_mapsto_vec_cons uninit_own. iFrame.
+ - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
rewrite /= vec_to_list_length. auto.
- iExists vl. iFrame. }
iApply type_delete; [solve_typing..|].
@@ -97,11 +97,11 @@ Section refcell_functions.
(&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
{ iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
- iIntros "[H1 H2]". iDestruct "H1" as (z) "?". iDestruct "H2" as (vl) "[??]".
- iExists (_::_). rewrite heap_mapsto_vec_cons /=. iFrame=>//=.
+ iExists (_::_). rewrite heap_pointsto_vec_cons /=. iFrame=>//=.
- iIntros "H".
iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]";
simpl; try iDestruct "H" as "[]".
- rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦1 H↦2]".
+ rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦1 H↦2]".
iSplitL "H↦1"; eauto. iExists _. iFrame. }
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
@@ -168,7 +168,7 @@ Section refcell_functions.
simpl. iApply type_jump; solve_typing.
- wp_op. wp_write. wp_apply wp_new; [done..|].
iIntros (lref) "(H†& Hlref & Hlm)". wp_let.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
@@ -215,7 +215,7 @@ Section refcell_functions.
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
- iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iExists [_; _]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iFrame. simpl. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
iApply lft_intersect_mono; [done|]. iApply lft_incl_refl. }
iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
@@ -268,7 +268,7 @@ Section refcell_functions.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- wp_write. wp_apply wp_new; [done..|].
iIntros (lref) "(H†& Hlref & Hm)". wp_let.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
destruct st as [[[[ν []] s] n]|]; try done.
iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
@@ -293,7 +293,7 @@ Section refcell_functions.
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
- iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iExists [_; _]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iFrame. simpl.
iExists _, _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index af534737..dc3cc2e9 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -29,7 +29,7 @@ Section refmut_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
[solve_typing..|].
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
[solve_typing..|].
iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
@@ -82,7 +82,7 @@ Section refmut_functions.
unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
{ split. - by rewrite Qp.mul_1_r. - apply _. }
iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
- rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". { done. }
+ rewrite heap_pointsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". { done. }
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". { done. }
wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_let. iMod "Hb".
@@ -118,7 +118,7 @@ Section refmut_functions.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; simpl;
try iDestruct "Hx" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
iDestruct "Hx" as (ν q γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
@@ -158,7 +158,7 @@ Section refmut_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)]
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton uninit_own. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
@@ -189,11 +189,11 @@ Section refmut_functions.
iDestruct "Href" as "[Href Href†]".
iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href"; simpl;
try iDestruct "Href" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν q γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
wp_read. wp_let. wp_apply wp_new; [done..|].
- iIntros (lx) "(H†& Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+ iIntros (lx) "(H†& Hlx & ?)". rewrite heap_pointsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
iMod (lctx_lft_alive_tok_noend Ï with "HE HL") as (?) "(HÏ & HL & Hclose2)";[solve_typing..|].
@@ -203,7 +203,7 @@ Section refmut_functions.
iApply (type_call_iris _ [α ⊓ ν; Ï] (α ⊓ ν) [_; _]
with "LFT HE Hna [HανÏ] Hf' [$Henv Hlx H†Hbor]"); [solve_typing|done| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
iIntros ([[|r|]|]) "Hna HÎ±Î½Ï Hr //".
iDestruct ("Hclose4" with "HανÏ") as "[Hαν HÏ]".
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -211,14 +211,14 @@ Section refmut_functions.
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as ([|r'[]]) "[Hr Hr']";
try by iDestruct (ty_size_eq with "Hr'") as "%".
- rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
+ rewrite heap_pointsto_vec_singleton. wp_read. wp_let.
wp_apply (wp_delete _ _ _ _ [_] with "[Hr Hr†]")=>//.
- { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+ { rewrite heap_pointsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
wp_seq. wp_write.
iApply (type_type _ [_] _ [ #lref ◠box (refmut α ty2) ]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //. simpl. iFrame.
- iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ iExists [_;_]. rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
iApply type_jump; solve_typing.
Qed.
@@ -268,11 +268,11 @@ Section refmut_functions.
iDestruct "Hrefmut" as "[Hrefmut Hrefmut†]".
iDestruct "Hrefmut" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hrefmut"; simpl;
try iDestruct "Hrefmut" as "[_ >[]]".
- rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite {1}heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hrefmut" as "[[Hrefmut↦1 Hrefmut↦2] Hrefmut]".
iDestruct "Hrefmut" as (ν qν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
wp_read. wp_let. wp_apply wp_new; [done..|].
- iIntros (lx) "(H†& Hlx & ?)". rewrite heap_mapsto_vec_singleton.
+ iIntros (lx) "(H†& Hlx & ?)". rewrite heap_pointsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
iMod (lctx_lft_alive_tok_noend Ï with "HE HL") as (?) "(HÏ & HL & Hclose2)";[solve_typing..|].
@@ -282,7 +282,7 @@ Section refmut_functions.
iApply (type_call_iris _ [α ⊓ ν; Ï] (α ⊓ ν) [_; _]
with "LFT HE Hna [HανÏ] Hf' [$Henv Hlx H†Hbor]"); [solve_typing|done| |].
{ rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
- iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+ iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. by iFrame. }
iIntros ([[|r|]|]) "Hna HÎ±Î½Ï Hr //".
iDestruct ("Hclose4" with "HανÏ") as "[Hαν HÏ]".
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
@@ -291,10 +291,10 @@ Section refmut_functions.
iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[Hr1' H]".
iDestruct "H" as (vl2 vl2' ->) "[Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hr1 Hr2 Hr†]")=>//.
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
@@ -315,10 +315,10 @@ Section refmut_functions.
by apply Qp.add_le_mono_l, Qp.div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_". wp_seq. wp_apply wp_new; [done..|]. iIntros (lrefmuts) "(Hrefmuts†& Hrefmuts & ?)".
- rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton. wp_let.
+ rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton. wp_let.
iDestruct "Hrefmuts" as "(Hrefmuts1 & Hrefmuts2 & Hrefmuts3 & Hrefmuts4)".
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
iMod ("Hclosena" with "[Hlrc H◠Hν1 H†] Hna") as "[Hβ Hna]".
@@ -331,7 +331,7 @@ Section refmut_functions.
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val' //= -freeable_sz_full.
simpl. iFrame. iExists [_;_;_;_].
- rewrite 3!heap_mapsto_vec_cons heap_mapsto_vec_singleton !shift_loc_assoc.
+ rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton !shift_loc_assoc.
iFrame. iExists [_;_], [_;_]. iSplit=>//=.
iSplitL "Hν Hγ Hr1'"; [by auto 10 with iFrame|]. iExists [_;_], [].
iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index c05cf674..4d77b0af 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -405,8 +405,8 @@ Section rwlock.
(l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H Htok]".
{ iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
iDestruct "Hvl" as (vl') "[H↦ Hvl]".
- iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗% hInv". }
- { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+ iExists (#n'::vl'). rewrite heap_pointsto_vec_cons. iFrame "∗% hInv". }
+ { iNext. rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; [eauto|iExists _; iFrame]. }
iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
iMod (rwlock_proto_create with "LFT Htok hInv Hvl Hn") as "[$ Hproto]". { done. }
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 39d39a62..6a816a42 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -45,7 +45,7 @@ Section rwlock_functions.
destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
- rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
+ rewrite heap_pointsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
iIntros "[Hr↦1 Hx↦]". wp_seq.
@@ -55,7 +55,7 @@ Section rwlock_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
iSplitL "Hx↦".
- iExists _. rewrite uninit_own. auto.
- - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
+ - iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -80,7 +80,7 @@ Section rwlock_functions.
iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ [HI Hx]]"; try iDestruct "Hx" as ">[]".
destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
- iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
+ iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_pointsto_vec_cons.
iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
@@ -89,7 +89,7 @@ Section rwlock_functions.
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_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
+ - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto.
- iExists vl. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -115,9 +115,9 @@ Section rwlock_functions.
{ iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
- iIntros "[H1 H2]". iDestruct "H1" as "[? H1]".
iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
- iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
+ iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. iFrame.
- iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ [HI H]]"; try done.
- rewrite heap_mapsto_vec_cons. iFrame "HI".
+ rewrite heap_pointsto_vec_cons. iFrame "HI".
iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index df763433..98923018 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -32,7 +32,7 @@ Section rwlockreadguard_functions.
iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
- rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
+ rewrite heap_pointsto_vec_singleton. wp_read. wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
iApply (type_type _ _ _ [ x ◠box (&shr{α}(rwlockreadguard β ty));
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index ddf79195..8c71fb6c 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -33,7 +33,7 @@ Section rwlockwriteguard_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
[solve_typing..|].
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
[solve_typing..|].
iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
@@ -79,7 +79,7 @@ Section rwlockwriteguard_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
destruct vl as [|[[|l|]|][]];
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
- rewrite heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton.
iMod (bor_exists with "LFT H") as (γ) "H". { done. }
iMod (bor_exists with "LFT H") as (δ) "H". { done. }
iMod (bor_exists with "LFT H") as (tid_shr) "H". { done. }
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index c36ab18f..906d5a18 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -35,7 +35,7 @@ Section code.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
iMod (lctx_lft_alive_tok_noend Ï with "HE HL") as (qÏ) "(HÏ & HL & Hclose2)"; [solve_typing..|].
iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
- iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
+ iDestruct (heap_pointsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
iIntros "[Htl Hx'↦]". wp_seq.
(* Call the function. *)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f1796172..30dc609d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -70,7 +70,7 @@ Section own.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
destruct vl as [|[[|l'|]|][]];
try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
- iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
+ iFrame. iExists l'. rewrite heap_pointsto_vec_singleton.
rewrite bi.later_sep.
iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
@@ -97,7 +97,7 @@ Section own.
iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iModIntro.
- iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
- iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
+ iDestruct "Heq" as %->. iFrame. iApply (heap_pointsto_pred_wand with "Hmt").
iApply "Ho".
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iFrame. iIntros "!>". iIntros (F' q) "% Htok".
@@ -133,7 +133,7 @@ Section own.
Send ty → Send (own_ptr n ty).
Proof.
iIntros (Hsend tid1 tid2 [|[[| |]|][]]) "H"; try done.
- iDestruct "H" as "[Hm $]". iNext. iApply (heap_mapsto_pred_wand with "Hm").
+ iDestruct "H" as "[Hm $]". iNext. iApply (heap_pointsto_pred_wand with "Hm").
iIntros (vl) "?". by iApply Hsend.
Qed.
@@ -194,7 +194,7 @@ Section util.
Proof.
iSplit.
- iIntros "Hown". destruct v as [[|l|]|]; try done.
- iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
+ 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.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 976583fa..696d302c 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -25,7 +25,7 @@ Section product.
split. { by apply _. } iIntros (????????) "_ _ Htok $".
iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
iExists 1%Qp. iModIntro. iSplitR.
- { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
+ { iExists []. iSplitL; last by auto. rewrite heap_pointsto_vec_nil. auto. }
iIntros "Htok2 _". iApply "Htok". done.
Qed.
@@ -42,12 +42,12 @@ Section product.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
- subst. rewrite heap_mapsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
+ subst. rewrite heap_pointsto_vec_app. iDestruct "H↦" as "[H↦1 H↦2]".
iDestruct (ty_size_eq with "H1") as %->.
iSplitL "H1 H↦1"; iExists _; iFrame.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
- rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
+ rewrite heap_pointsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
iFrame. iExists _, _. by iFrame.
Qed.
@@ -134,8 +134,8 @@ Section product.
iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
iDestruct (ty_size_eq with "H1") as "#>%".
iDestruct (ty_size_eq with "H2") as "#>%".
- iDestruct (heap_mapsto_vec_combine with "H↦1 H↦1f") as "H↦1"; [congruence|].
- iDestruct (heap_mapsto_vec_combine with "H↦2 H↦2f") as "H↦2"; [congruence|].
+ iDestruct (heap_pointsto_vec_combine with "H↦1 H↦1f") as "H↦1"; [congruence|].
+ iDestruct (heap_pointsto_vec_combine with "H↦2 H↦2f") as "H↦2"; [congruence|].
iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]".
{ by iExists _; iFrame. }
iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index d0167501..7242ba71 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -92,7 +92,7 @@ Section product_split.
iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
- rewrite heap_mapsto_vec_app -freeable_sz_split.
+ rewrite heap_pointsto_vec_app -freeable_sz_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".
@@ -113,7 +113,7 @@ Section product_split.
rewrite HÏ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
iExists #_. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
- iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
+ 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.
Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 9eab149f..d5c811cf 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -83,7 +83,7 @@ Section typing.
Proof. rewrite typed_write_eq. apply _. Qed.
(* Technically speaking, we could remvoe the vl quantifiaction here and use
- mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
+ pointsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
make work for some of the provers way harder, since they'd have to show
that nobody could possibly have changed the vl (because only half the
fraction was given). So we go with the definition that is easier to prove. *)
@@ -256,8 +256,8 @@ Section typing_rules.
iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
- rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_write.
- rewrite -heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_singleton. iApply wp_fupd. wp_write.
+ rewrite -heap_pointsto_vec_singleton.
iMod ("Hclose" with "[Hl Hown2]") as "(HL & Hown)".
{ iExists _. iFrame. }
iDestruct ("HLclose" with "HL") as "$".
@@ -285,7 +285,7 @@ Section typing_rules.
(l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
destruct vl as [|v [|]]; try done.
- rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
+ rewrite heap_pointsto_vec_singleton. iApply wp_fupd. wp_read.
iMod ("Hclose" with "Hl") as "($ & HL & Hown2)".
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 5f05f2d5..10ed7a06 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -37,9 +37,9 @@ Section sum.
Proof.
iSplit; iIntros "H".
- iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
- subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
+ subst. iExists i. iDestruct (heap_pointsto_vec_cons with "Hmt") as "[$ Hmt]".
iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
- iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
+ iDestruct (heap_pointsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
+ iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
+ iExists vl'. by iFrame.
@@ -47,7 +47,7 @@ Section sum.
iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
iExists (#i::vl'++vl'').
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
+ 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.
simpl. f_equal. by rewrite app_length Hvl'.
Qed.
@@ -201,14 +201,14 @@ Section sum.
- apply shr_locsE_subseteq. lia.
- set_solver+. }
destruct (Qp.lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
- rewrite -(heap_mapsto_pred_combine _ q' q'02); last (by intros; iApply ty_size_eq).
+ rewrite -(heap_pointsto_pred_combine _ q' q'02); last (by intros; iApply ty_size_eq).
rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
iExists q'. iModIntro. iSplitL "Hown1 HownC1".
+ iNext. iExists i. iFrame.
+ iIntros "Htl H". iDestruct "H" as (i') "[>Hown1 HownC1]".
iDestruct ("Htlclose" with "Htl") as "Htl".
- iDestruct (heap_mapsto_agree with "[Hown1] [Hown2]") as "#Heq".
+ iDestruct (heap_pointsto_agree with "[Hown1] [Hown2]") as "#Heq".
{ iDestruct "Hown1" as "[$ _]". } { iDestruct "Hown2" as "[$ _]". }
iDestruct "Heq" as %[= ->%Nat2Z.inj].
iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index ae9b7185..e40f037b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -504,7 +504,7 @@ Section type.
{ iNext. iDestruct (st_size_eq with "Hown") as %->.
iDestruct (st_size_eq with "Hown'") as %->. done. }
iApply "Hclose".
- by iDestruct (heap_mapsto_vec_combine with "Hmt2 Hmt1") as "[$$]".
+ by iDestruct (heap_pointsto_vec_combine with "Hmt2 Hmt1") as "[$$]".
Qed.
(** Send and Sync types *)
@@ -751,7 +751,7 @@ End subtyping.
Section type_util.
Context `{!typeG Σ}.
- Lemma heap_mapsto_ty_own l ty tid :
+ Lemma heap_pointsto_ty_own l ty tid :
l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
Proof.
iSplit.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 55098ec9..ad3f4e0a 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -24,7 +24,7 @@ Section case.
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
rewrite -Nat.add_1_l app_length -!freeable_sz_split
- heap_mapsto_vec_cons heap_mapsto_vec_app.
+ heap_pointsto_vec_cons heap_pointsto_vec_app.
iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
rewrite nth_lookup.
@@ -35,13 +35,13 @@ Section case.
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
- rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
- + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
+ + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_pointsto_vec_singleton.
iFrame. auto.
+ eauto with iFrame.
+ rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
iFrame. iExists _. iFrame. auto.
- rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
- iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
+ 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.
Qed.
@@ -73,7 +73,7 @@ Section case.
iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
iDestruct "EQlen" as %[=EQlen].
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app nth_lookup.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_app nth_lookup.
iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
@@ -85,7 +85,7 @@ Section case.
{ iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
iExists (#i::vl'2++vl''). iIntros "!>". iNext.
iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_app EQlenvl' EQlenvl'2.
iFrame. iExists _, _, _. iSplit. { by auto. }
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
{ iExists vl'. iFrame. }
@@ -96,7 +96,7 @@ Section case.
- iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
[by iIntros "!>$"| |].
{ iExists (#i::vl'++vl'').
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_app /= -EQlen. iFrame. iNext.
iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
iMod ("Hclose" with "Htok") as "HL".
iDestruct ("HLclose" with "HL") as "HL".
@@ -163,7 +163,7 @@ Section case.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] [= ->]].
- rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+ rewrite heap_pointsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|].
iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
@@ -172,12 +172,12 @@ Section case.
induction tyl as [|?? IHtyl]=>//= -[|i] /=.
- intros [= ->]. simpl in *. lia.
- apply IHtyl. simpl in *. lia. }
- rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+ rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
rewrite tctx_interp_singleton tctx_hasty_val' //.
iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
{ iApply "HLclose". done. }
iNext.
- iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
+ iExists (_::_::_). rewrite !heap_pointsto_vec_cons. iFrame.
iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
@@ -206,11 +206,11 @@ Section case.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". { done. }
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
- rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
+ rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
{ iApply "HLclose". done. }
- iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+ iModIntro. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame.
iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
Qed.
@@ -244,7 +244,7 @@ Section case.
rewrite typed_write_eq in Hw.
iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
clear Hw. destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
- rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+ rewrite heap_pointsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|]. iIntros (v2 Hv2) "Hty2".
rewrite typed_read_eq in Hr.
@@ -253,7 +253,7 @@ Section case.
{ revert i Hty. rewrite Hlen. clear. induction tyl as [|?? IHtyl]=>//= -[|i] /=.
- intros [= ->]. lia.
- specialize (IHtyl i). intuition lia. }
- rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
+ rewrite -(take_drop (ty.(ty_size)) vl1) heap_pointsto_vec_app.
iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
iDestruct (ty_size_eq with "Hty") as "#>%".
iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [done| |lia|].
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 027962ae..e5e2c9f3 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -24,7 +24,7 @@ Section uniq_bor.
iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first solve_ndisj;
(iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
- iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
+ iFrame. iExists l'. rewrite heap_pointsto_vec_singleton.
iMod (bor_fracture (l ↦{1} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
iApply delay_sharing_nested; try done. iApply lft_incl_refl.
Qed.
--
GitLab