From c722fb2812068eddc55898eae6ca7266153e9605 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Nov 2023 21:42:26 +0100
Subject: [PATCH] update dependencies
---
coq-lambda-rust.opam | 2 +-
theories/lang/heap.v | 144 +++++++++---------
theories/lang/lang.v | 50 +++---
theories/lang/lib/memcpy.v | 2 +-
theories/lang/lib/new_delete.v | 2 +-
theories/lang/lib/spawn.v | 4 +-
theories/lang/lib/swap.v | 2 +-
theories/lang/lifting.v | 68 ++++-----
theories/lang/races.v | 116 +++++++-------
theories/lang/tactics.v | 8 +-
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 | 8 +-
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 +-
36 files changed, 399 insertions(+), 399 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index fcb1e0f8..256e076b 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2023-10-03.0.70b30af7") | (= "dev") }
+ "coq-iris" { (= "dev.2023-11-06.5.4cfd3db8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 784b32e6..e77f2782 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -36,19 +36,19 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
Section definitions.
Context `{!heapGS Σ}.
- Definition heap_mapsto_st (st : lock_state)
+ Definition heap_pointsto_st (st : lock_state)
(l : loc) (q : Qp) (v: val) : iProp Σ :=
own heap_name (â—¯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
- Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
- heap_mapsto_st (RSt 0) l q v.
- Definition heap_mapsto_aux : seal (@heap_mapsto_def). Proof. by eexists. Qed.
- Definition heap_mapsto := unseal heap_mapsto_aux.
- Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
- seal_eq heap_mapsto_aux.
+ Definition heap_pointsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
+ heap_pointsto_st (RSt 0) l q v.
+ Definition heap_pointsto_aux : seal (@heap_pointsto_def). Proof. by eexists. Qed.
+ Definition heap_pointsto := unseal heap_pointsto_aux.
+ Definition heap_pointsto_eq : @heap_pointsto = @heap_pointsto_def :=
+ seal_eq heap_pointsto_aux.
- Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
- ([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
+ Definition heap_pointsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
+ ([∗ list] i ↦ v ∈ vl, heap_pointsto (l +ₗ i) q v)%I.
Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitO) :=
match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
@@ -66,17 +66,17 @@ Section definitions.
∗ ⌜heap_freeable_rel σ hFâŒ)%I.
End definitions.
-Global Typeclasses Opaque heap_mapsto_vec.
-Global Instance: Params (@heap_mapsto) 4 := {}.
+Global Typeclasses Opaque heap_pointsto_vec.
+Global Instance: Params (@heap_pointsto) 4 := {}.
Global Instance: Params (@heap_freeable) 5 := {}.
-Notation "l ↦{ q } v" := (heap_mapsto l q v)
+Notation "l ↦{ q } v" := (heap_pointsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
+Notation "l ↦ v" := (heap_pointsto l 1 v) (at level 20) : bi_scope.
-Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
+Notation "l ↦∗{ q } vl" := (heap_pointsto_vec l q vl)
(at level 20, q at level 50, format "l ↦∗{ q } vl") : bi_scope.
-Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope.
+Notation "l ↦∗ vl" := (heap_pointsto_vec l 1 vl) (at level 20) : bi_scope.
Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
(at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope.
@@ -111,81 +111,81 @@ Section heap.
Implicit Types σ : state.
Implicit Types E : coPset.
- (** General properties of mapsto and freeable *)
- Global Instance heap_mapsto_timeless l q v : Timeless (l↦{q}v).
- Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
+ (** General properties of pointsto and freeable *)
+ Global Instance heap_pointsto_timeless l q v : Timeless (l↦{q}v).
+ Proof. rewrite heap_pointsto_eq /heap_pointsto_def. apply _. Qed.
- Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+ Global Instance heap_pointsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
Proof.
intros p q.
- by rewrite heap_mapsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
+ by rewrite heap_pointsto_eq -own_op -auth_frag_op singleton_op -pair_op agree_idemp.
Qed.
- Global Instance heap_mapsto_as_fractional l q v:
+ Global Instance heap_pointsto_as_fractional l q v:
AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
Proof. split; first done. apply _. Qed.
- Global Instance frame_mapsto p l v q1 q2 q :
+ Global Instance frame_pointsto p l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
Proof. apply: frame_fractional. Qed.
- Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
- Proof. rewrite /heap_mapsto_vec. apply _. Qed.
+ Global Instance heap_pointsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
+ Proof. rewrite /heap_pointsto_vec. apply _. Qed.
- Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
+ Global Instance heap_pointsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Proof.
- intros p q. rewrite /heap_mapsto_vec -big_sepL_sep.
+ intros p q. rewrite /heap_pointsto_vec -big_sepL_sep.
by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
Qed.
- Global Instance heap_mapsto_vec_as_fractional l q vl:
+ Global Instance heap_pointsto_vec_as_fractional l q vl:
AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
Proof. split; first done. apply _. Qed.
Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
- Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2âŒ.
+ Lemma heap_pointsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2âŒ.
Proof.
- rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+ rewrite heap_pointsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
Qed.
- Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
- Proof. by rewrite /heap_mapsto_vec. Qed.
+ Lemma heap_pointsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
+ Proof. by rewrite /heap_pointsto_vec. Qed.
- Lemma heap_mapsto_vec_app l q vl1 vl2 :
+ Lemma heap_pointsto_vec_app l q vl1 vl2 :
l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
Proof.
- rewrite /heap_mapsto_vec big_sepL_app.
+ rewrite /heap_pointsto_vec big_sepL_app.
do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
Qed.
- Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
- Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
+ Lemma heap_pointsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
+ Proof. by rewrite /heap_pointsto_vec /= shift_loc_0 right_id. Qed.
- Lemma heap_mapsto_vec_cons l q v vl:
+ Lemma heap_pointsto_vec_cons l q v vl:
l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
Proof.
- by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
+ by rewrite (heap_pointsto_vec_app l q [v] vl) heap_pointsto_vec_singleton.
Qed.
- Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
+ Lemma heap_pointsto_vec_op l q1 q2 vl1 vl2 :
length vl1 = length vl2 →
l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌠∧ l ↦∗{q1+q2} vl1.
Proof.
intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
- revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
- { rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
- rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
+ { rewrite !heap_pointsto_vec_nil. iIntros "_"; auto. }
+ rewrite !heap_pointsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (l +â‚— 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (.:: vl2)).
- iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
+ iDestruct (heap_pointsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst.
Qed.
- Lemma heap_mapsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
+ Lemma heap_pointsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
(∀ vl, Φ vl -∗ ⌜length vl = nâŒ) →
l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = nâŒ) ⊣⊢ l ↦∗{q1+q2}: Φ.
Proof.
@@ -193,37 +193,37 @@ Section heap.
- iIntros "[Hmt1 Hmt2]".
iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
iDestruct (Hlen with "Hown") as %?.
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_pointsto_vec_op; last congruence.
iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
iDestruct (Hlen with "Hown") as %?.
iSplitL "Hmt1 Hown"; iExists _; by iFrame.
Qed.
- Lemma heap_mapsto_pred_wand l q Φ1 Φ2 :
+ Lemma heap_pointsto_pred_wand l q Φ1 Φ2 :
l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
Proof.
iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
iFrame "Hm". by iApply "Hwand".
Qed.
- Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
+ Lemma heap_pointsto_pred_iff_proper l q Φ1 Φ2 :
□ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
Proof.
- iIntros "#HΦ !>". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
+ iIntros "#HΦ !>". iSplit; iIntros; iApply (heap_pointsto_pred_wand with "[-]"); try done; [|];
iIntros; by iApply "HΦ".
Qed.
- Lemma heap_mapsto_vec_combine l q vl :
+ Lemma heap_pointsto_vec_combine l q vl :
vl ≠[] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
{[l +â‚— i := (q, Cinr 0%nat, to_agree v)]}).
Proof.
- rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
+ rewrite /heap_pointsto_vec heap_pointsto_eq /heap_pointsto_def /heap_pointsto_st=>?.
rewrite (big_opL_commute auth_frag) big_opL_commute1 //.
Qed.
- Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
+ Global Instance heap_pointsto_pred_fractional l (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
Proof.
intros p q q'. iSplit.
@@ -232,9 +232,9 @@ Section heap.
- iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
iDestruct "H2" as (vl2) "[Hown2 #HP2]".
set (ll := min (length vl1) (length vl2)).
- rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_mapsto_vec_app.
+ rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_pointsto_vec_app.
iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
- iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first.
+ iCombine "Hown1" "Hown2" as "Hown". rewrite heap_pointsto_vec_op; last first.
{ rewrite !firstn_length. subst ll.
rewrite -!Nat.min_assoc Nat.min_idempotent Nat.min_comm -Nat.min_assoc Nat.min_idempotent Nat.min_comm. done. }
iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
@@ -246,7 +246,7 @@ Section heap.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
Qed.
- Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
+ Global Instance heap_pointsto_pred_as_fractional l q (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
Proof. split; first done. apply _. Qed.
@@ -379,7 +379,7 @@ Section heap.
iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro.
auto using heap_freeable_rel_init_mem. }
- rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //; last first.
+ rewrite heap_freeable_eq /heap_freeable_def heap_pointsto_vec_combine //; last first.
{ destruct (Z.to_nat n); done. }
iFrame.
Qed.
@@ -420,7 +420,7 @@ Section heap.
{ intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
assert (0 < n) by (subst n; by destruct vl).
iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
- { rewrite heap_mapsto_vec_combine //. iFrame. }
+ { rewrite heap_pointsto_vec_combine //. iFrame. }
iMod (own_update_2 with "HhF Hf") as "HhF".
{ apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
iModIntro; subst. repeat iSplit; eauto using heap_freeable_is_Some.
@@ -428,7 +428,7 @@ Section heap.
eauto using heap_freeable_rel_free_mem.
Qed.
- Lemma heap_mapsto_lookup σ l ls q v :
+ Lemma heap_pointsto_lookup σ l ls q v :
own heap_name (◠to_heap σ) -∗
own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
⌜∃ n' : nat,
@@ -448,7 +448,7 @@ Section heap.
- exists O. by rewrite Nat.add_0_r.
Qed.
- Lemma heap_mapsto_lookup_1 σ l ls v :
+ Lemma heap_pointsto_lookup_1 σ l ls v :
own heap_name (◠to_heap σ) -∗
own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
⌜σ !! l = Some (ls, v)âŒ.
@@ -465,9 +465,9 @@ Section heap.
Lemma heap_read_vs σ n1 n2 nf l q v:
σ !! l = Some (RSt (n1 + nf), v) →
- own heap_name (◠to_heap σ) -∗ heap_mapsto_st (RSt n1) l q v
+ own heap_name (◠to_heap σ) -∗ heap_pointsto_st (RSt n1) l q v
==∗ own heap_name (◠to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
- ∗ heap_mapsto_st (RSt n2) l q v.
+ ∗ heap_pointsto_st (RSt n2) l q v.
Proof.
intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
iApply own_update. eapply auth_update, singleton_local_update.
@@ -480,16 +480,16 @@ Section heap.
heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)âŒ.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
- rewrite heap_mapsto_eq.
- iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ rewrite heap_pointsto_eq.
+ iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
Qed.
Lemma heap_read_1 σ l v :
heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)âŒ.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
- rewrite heap_mapsto_eq.
- iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+ rewrite heap_pointsto_eq.
+ iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
Qed.
Lemma heap_read_na σ l q v :
@@ -500,13 +500,13 @@ Section heap.
heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
- rewrite heap_mapsto_eq.
- iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ rewrite heap_pointsto_eq.
+ iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
- iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable.
@@ -514,9 +514,9 @@ Section heap.
Lemma heap_write_vs σ st1 st2 l v v':
σ !! l = Some (st1, v) →
- own heap_name (◠to_heap σ) -∗ heap_mapsto_st st1 l 1%Qp v
+ own heap_name (◠to_heap σ) -∗ heap_pointsto_st st1 l 1%Qp v
==∗ own heap_name (◠to_heap (<[l:=(st2, v')]> σ))
- ∗ heap_mapsto_st st2 l 1%Qp v'.
+ ∗ heap_pointsto_st st2 l 1%Qp v'.
Proof.
intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
iApply own_update. eapply auth_update, singleton_local_update.
@@ -528,8 +528,8 @@ Section heap.
heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
- rewrite heap_mapsto_eq.
- iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+ rewrite heap_pointsto_eq.
+ iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; auto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
Qed.
@@ -542,13 +542,13 @@ Section heap.
heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
Proof.
iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
- rewrite heap_mapsto_eq.
- iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; eauto.
+ rewrite heap_pointsto_eq.
+ iDestruct (heap_pointsto_lookup_1 with "Hσ Hmt") as %?; eauto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
{ iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
- iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ iDestruct (heap_pointsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
iModIntro; iSplit; [done|]. iFrame "Hmt".
iExists hF. iFrame. eauto using heap_freeable_rel_stable.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 16a15295..37a0c55f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -232,48 +232,48 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
Definition stuck_term := App (Lit $ LitInt 0) [].
-Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
+Inductive base_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
| BinOpS op l1 l2 l' σ :
bin_op_eval σ op l1 l2 l' →
- head_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
+ base_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
| BetaS f xl e e' el σ:
Forall (λ ei, is_Some (to_val ei)) el →
Closed (f :b: xl +b+ []) e →
subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
- head_step (App (Rec f xl e) el) σ [] e' σ []
+ base_step (App (Rec f xl e) el) σ [] e' σ []
| ReadScS l n v σ:
σ !! l = Some (RSt n, v) →
- head_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
+ base_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
| ReadNa1S l n v σ:
σ !! l = Some (RSt n, v) →
- head_step (Read Na1Ord (Lit $ LitLoc l)) σ
+ base_step (Read Na1Ord (Lit $ LitLoc l)) σ
[]
(Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
[]
| ReadNa2S l n v σ:
σ !! l = Some (RSt $ S n, v) →
- head_step (Read Na2Ord (Lit $ LitLoc l)) σ
+ base_step (Read Na2Ord (Lit $ LitLoc l)) σ
[]
(of_val v) (<[l:=(RSt n, v)]>σ)
[]
| WriteScS l e v v' σ:
to_val e = Some v →
σ !! l = Some (RSt 0, v') →
- head_step (Write ScOrd (Lit $ LitLoc l) e) σ
+ base_step (Write ScOrd (Lit $ LitLoc l) e) σ
[]
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
| WriteNa1S l e v v' σ:
to_val e = Some v →
σ !! l = Some (RSt 0, v') →
- head_step (Write Na1Ord (Lit $ LitLoc l) e) σ
+ base_step (Write Na1Ord (Lit $ LitLoc l) e) σ
[]
(Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
[]
| WriteNa2S l e v v' σ:
to_val e = Some v →
σ !! l = Some (WSt, v') →
- head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
+ base_step (Write Na2Ord (Lit $ LitLoc l) e) σ
[]
(Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
[]
@@ -281,12 +281,12 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) →
lit_neq lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
+ base_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
| CasSucS l e1 lit1 e2 lit2 litl σ :
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt 0, LitV litl) →
lit_eq σ lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+ base_step (CAS (Lit $ LitLoc l) e1 e2) σ
[]
(Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
[]
@@ -308,30 +308,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) → 0 < n →
lit_eq σ lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+ base_step (CAS (Lit $ LitLoc l) e1 e2) σ
[]
stuck_term σ
[]
| AllocS n l σ :
0 < n →
(∀ m, σ !! (l +ₗ m) = None) →
- head_step (Alloc $ Lit $ LitInt n) σ
+ base_step (Alloc $ Lit $ LitInt n) σ
[]
(Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
[]
| FreeS n l σ :
0 < n →
(∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
- head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
+ base_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
[]
(Lit LitPoison) (free_mem l (Z.to_nat n) σ)
[]
| CaseS i el e σ :
0 ≤ i →
el !! (Z.to_nat i) = Some e →
- head_step (Case (Lit $ LitInt i) el) σ [] e σ []
+ base_step (Case (Lit $ LitInt i) el) σ [] e σ []
| ForkS e σ:
- head_step (Fork e) σ [] (Lit LitPoison) σ [e].
+ base_step (Fork e) σ [] (Lit LitPoison) σ [e].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -355,11 +355,11 @@ Lemma fill_item_val Ki e :
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma val_stuck e1 σ1 κ e2 σ2 ef :
- head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
+ base_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
-Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
- head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
+Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 ef :
+ base_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
Proof.
destruct Ki; inversion_clear 1; decompose_Forall_hyps;
simplify_option_eq; by eauto.
@@ -446,7 +446,7 @@ Lemma alloc_fresh n σ :
let l := (fresh_block σ, 0) in
let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
0 < n →
- head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
+ base_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
Proof.
intros l init Hn. apply AllocS; first done.
- intros i. apply (is_fresh_block _ i).
@@ -540,8 +540,8 @@ Proof.
Qed.
(* Misc *)
-Lemma stuck_not_head_step σ e' κ σ' ef :
- ¬head_step stuck_term σ e' κ σ' ef.
+Lemma stuck_not_base_step σ e' κ σ' ef :
+ ¬base_step stuck_term σ e' κ σ' ef.
Proof. inversion 1. Qed.
(** Equality and other typeclass stuff *)
@@ -611,10 +611,10 @@ Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
(** Language *)
-Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val,
- val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+ val_stuck, fill_item_val, fill_item_no_val_inj, base_ctx_step_val.
Qed.
Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
@@ -624,7 +624,7 @@ Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
Proof.
apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
- apply prim_head_irreducible; unfold stuck_term.
+ apply prim_base_irreducible; unfold stuck_term.
- inversion 1.
- apply ectxi_language_sub_redexes_are_values.
intros [] ??; simplify_eq/=; eauto; discriminate_list.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 9edcaae8..43ff59d1 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -30,7 +30,7 @@ Proof.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
- revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
+ revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 2b153350..7c7bef80 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -23,7 +23,7 @@ Section specs.
Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
- rewrite heap_mapsto_vec_nil. auto.
+ rewrite heap_pointsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†"; first lia. iApply "HΦ". subst. iFrame.
Qed.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 07a32237..e2777f89 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -70,7 +70,7 @@ Proof.
wp_let. wp_alloc l as "Hl" "H†". wp_let.
iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
- rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+ rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
{ iNext. iRight. iExists false. auto. }
@@ -111,7 +111,7 @@ Proof.
{ iNext. iLeft. iFrame. }
iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
- { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
+ { rewrite heap_pointsto_vec_cons heap_pointsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
Qed.
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 11f3cc45..996fa785 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -22,7 +22,7 @@ Proof.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
- revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
+ revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_pointsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_let; wp_read; do 2 wp_write. do 3 wp_op.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 9de46d59..398d16ac 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -31,9 +31,9 @@ Ltac inv_bin_op_eval :=
end.
Local Hint Extern 0 (atomic _) => solve_atomic : core.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
+Local Hint Extern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : core.
-Local Hint Constructors head_step bin_op_eval lit_neq lit_eq : core.
+Local Hint Constructors base_step bin_op_eval lit_neq lit_eq : core.
Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val : core.
@@ -71,9 +71,9 @@ Implicit Types ef : option expr.
Lemma wp_fork E e :
{{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
Proof.
- iIntros (?) "?HΦ". iApply wp_lift_atomic_head_step; [done|].
+ iIntros (?) "?HΦ". iApply wp_lift_atomic_base_step; [done|].
iIntros (σ1 κ ? κs n) "Hσ !>"; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step. iFrame.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. iFrame.
iModIntro. by iApply "HΦ".
Qed.
@@ -81,9 +81,9 @@ Qed.
Local Ltac solve_exec_safe :=
intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with lia.
Local Ltac solve_exec_puredet :=
- simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval; inv_lit; done.
+ simpl; intros; destruct_and?; inv_base_step; inv_bin_op_eval; inv_lit; done.
Local Ltac solve_pure_exec :=
- intros ?; apply nsteps_once, pure_head_step_pure_step;
+ intros ?; apply nsteps_once, pure_base_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Global Instance pure_rec e f xl erec erec' el :
@@ -140,9 +140,9 @@ Lemma wp_alloc E (n : Z) :
{{{ True }}} Alloc (Lit $ LitInt n) @ E
{{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌠∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
Proof.
- iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n') "Hσ !>"; iSplit; first by auto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
iApply ("HΦ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
@@ -154,11 +154,11 @@ Lemma wp_free E (n:Z) l vl :
Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
{{{ RET LitV LitPoison; True }}}.
Proof.
- iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n') "Hσ".
iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
iModIntro; iSplit; first by auto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
Qed.
@@ -166,10 +166,10 @@ Lemma wp_read_sc E l q v :
{{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -177,17 +177,17 @@ Lemma wp_read_na E l q v :
{{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
+ iIntros (Φ) ">Hv HΦ". iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
- iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_head_step. iMod "Hclose" as "_".
+ iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1 n.
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
- iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_head_step.
+ iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
@@ -196,11 +196,11 @@ Lemma wp_write_sc E l e v v' :
{{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
- iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iMod (heap_write _ _ _ v with "Hσ Hv") as "[Hσ Hv]".
iModIntro; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -210,16 +210,16 @@ Lemma wp_write_na E l e v v' :
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
- iApply wp_lift_head_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
+ iApply wp_lift_base_step; auto. iIntros (σ1 ? κ κs n) "Hσ".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
- iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_head_step. iMod "Hclose" as "_".
+ iNext; iIntros (e2 σ2 efs Hstep) "_"; inv_base_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
- clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
+ clear dependent σ1. iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
- iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_head_step.
+ iNext; iIntros (e2 σ2 efs Hstep) "_ !>"; inv_base_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
@@ -230,10 +230,10 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
{{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step; inv_lit.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -244,10 +244,10 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
{{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct lit1; by eauto).
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step; [inv_lit|].
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; [inv_lit|].
iMod (heap_write with "Hσ Hv") as "[$ Hv]".
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -274,12 +274,12 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
Proof.
iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
iModIntro; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step; inv_lit.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; inv_lit.
iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
Qed.
@@ -292,10 +292,10 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
else ⌜l1 ≠ll⌠∗ l ↦ LitV (LitLoc ll) }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
- iApply wp_lift_atomic_head_step_no_fork; auto.
+ iApply wp_lift_atomic_base_step_no_fork; auto.
iIntros (σ1 ? κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
- iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_head_step; last lia.
+ iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step; last lia.
- inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
iApply "HΦ"; simpl; auto.
- iMod (heap_write with "Hσ Hv") as "[$ Hv]".
@@ -310,12 +310,12 @@ Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
Proof.
iIntros (Hl1 Hl2 Hpost) "HP".
destruct (bool_decide_reflect (l1 = l2)) as [->|].
- - iApply wp_lift_pure_det_head_step_no_fork';
+ - iApply wp_lift_pure_det_base_step_no_fork';
[done|solve_exec_safe|solve_exec_puredet|].
iPoseProof (Hpost with "HP") as "?".
iIntros "!> _". by iApply wp_value.
- - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
- iIntros (σ1 ? κ κs n') "Hσ1". iModIntro. inv_head_step.
+ - iApply wp_lift_atomic_base_step_no_fork; subst=>//.
+ iIntros (σ1 ? κ κs n') "Hσ1". iModIntro. inv_base_step.
iSplitR.
{ iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
(* We need to do a little gymnastics here to apply Hne now and strip away a
@@ -326,7 +326,7 @@ Proof.
+ iExists _, _. by iApply Hl2.
+ by iApply Hpost. }
clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "_ !>".
- inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+ inv_base_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+ iExFalso. iDestruct "HP" as "[Hl1 _]".
iDestruct "Hl1" as (??) "Hl1".
iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 501581fd..9d1d9fd7 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
-(* This is a crucial definition; if we forget to sync it with head_step,
+(* This is a crucial definition; if we forget to sync it with base_step,
the results proven here are worthless. *)
Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
| Access_read ord l σ :
@@ -27,24 +27,24 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
σ (FreeAcc, Na2Ord) (l +ₗ i).
(* Some sanity checks to make sure the definition above is not entirely insensible. *)
-Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
+Goal ∀ e1 e2 e3 σ, base_reducible (CAS e1 e2 e3) σ →
∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
Proof.
intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
(eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
Qed.
-Goal ∀ o e σ, head_reducible (Read o e) σ →
+Goal ∀ o e σ, base_reducible (Read o e) σ →
∃ a l, next_access_head (Read o e) σ a l.
Proof.
intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_read; done.
Qed.
-Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
+Goal ∀ o e1 e2 σ, base_reducible (Write o e1 e2) σ →
∃ a l, next_access_head (Write o e1 e2) σ a l.
Proof.
intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
eapply Access_write; try done; eexists; done.
Qed.
-Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
+Goal ∀ e1 e2 σ, base_reducible (Free e1 e2) σ →
∃ a l, next_access_head (Free e1 e2) σ a l.
Proof.
intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_free; done.
@@ -70,20 +70,20 @@ Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
nonracing_accesses a1 a2.
-Lemma next_access_head_reductible_ctx e σ σ' a l K :
- next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
+Lemma next_access_base_reductible_ctx e σ σ' a l K :
+ next_access_head e σ' a l → reducible (fill K e) σ → base_reducible e σ.
Proof.
- intros Hhead Hred. apply prim_head_reducible.
+ intros Hhead Hred. apply prim_base_reducible.
- eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
- apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
Qed.
-Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
- ∀ κ e' σ' efs, ectx_language.head_step e σ κ e' σ' efs → e' ≠App (Lit $ LitInt 0) [].
+Definition base_reduce_not_to_stuck (e : expr) (σ : state) :=
+ ∀ κ e' σ' efs, ectx_language.base_step e σ κ e' σ' efs → e' ≠App (Lit $ LitInt 0) [].
-Lemma next_access_head_reducible_state e σ a l :
- next_access_head e σ a l → head_reducible e σ →
- head_reduce_not_to_stuck e σ →
+Lemma next_access_base_reducible_state e σ a l :
+ next_access_head e σ a l → base_reducible e σ →
+ base_reduce_not_to_stuck e σ →
match a with
| (ReadAcc, (ScOrd | Na1Ord)) => ∃ v n, σ !! l = Some (RSt n, v)
| (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
@@ -92,7 +92,7 @@ Lemma next_access_head_reducible_state e σ a l :
| (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
end.
Proof.
- intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
+ intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_base_step; eauto.
- rename select nat into n.
destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
by eapply CasStuckS.
@@ -101,21 +101,21 @@ Proof.
- match goal with H : ∀ m, _ |- context[_ +ₗ ?i] => destruct (H i) as [_ [[]?]] end; eauto.
Qed.
-Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
+Lemma next_access_base_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
next_access_head e1 σ1 (a, Na1Ord) l →
- head_step e1 σ1 κ e2 σ2 ef →
+ base_step e1 σ1 κ e2 σ2 ef →
next_access_head e2 σ2 (a, Na2Ord) l.
Proof.
- intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; by rewrite to_of_val.
+ intros Ha Hstep. inversion Ha; subst; clear Ha; inv_base_step; constructor; by rewrite to_of_val.
Qed.
-Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
+Lemma next_access_base_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
next_access_head e1 σ (a1, Na1Ord) l →
- head_step e1 σ κ e1' σ' e'f →
+ base_step e1 σ κ e1' σ' e'f →
next_access_head e2 σ a2 l →
next_access_head e2 σ' a2 l.
Proof.
- intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
+ intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_base_step;
destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
(* Oh my. FIXME. *)
- eapply lit_eq_state; last done.
@@ -130,9 +130,9 @@ Proof.
cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
Qed.
-Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
- next_access_head e1 σ (FreeAcc, o1) l → head_step e1 σ κ e1' σ' e'f →
- next_access_head e2 σ a2 l → head_reducible e2 σ' →
+Lemma next_access_base_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
+ next_access_head e1 σ (FreeAcc, o1) l → base_step e1 σ κ e1' σ' e'f →
+ next_access_head e2 σ a2 l → base_reducible e2 σ' →
False.
Proof.
intros Ha1 Hstep Ha2 Hred2.
@@ -146,16 +146,16 @@ Proof.
rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
destruct l; intros [= ?]. lia. }
assert (FREE' : σ' !! l = None).
- { inversion Ha1; clear Ha1; inv_head_step. auto. }
+ { inversion Ha1; clear Ha1; inv_base_step. auto. }
destruct Hred2 as (κ'&e2'&σ''&ef&?).
- inversion Ha2; clear Ha2; inv_head_step.
+ inversion Ha2; clear Ha2; inv_base_step.
eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
Qed.
Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
(∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
e' ∈ el' → to_val e' = None → reducible e' σ') →
- fill K e ∈ el → head_step e σ κ e' σ' ef → head_reduce_not_to_stuck e' σ'.
+ fill K e ∈ el → base_step e σ κ e' σ' ef → base_reduce_not_to_stuck e' σ'.
Proof.
intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
@@ -172,7 +172,7 @@ Qed.
Lemma safe_not_reduce_to_stuck el σ K e :
(∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
e' ∈ el' → to_val e' = None → reducible e' σ') →
- fill K e ∈ el → head_reduce_not_to_stuck e σ.
+ fill K e ∈ el → base_reduce_not_to_stuck e σ.
Proof.
intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
@@ -192,93 +192,93 @@ Proof.
intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
assert (to_val e1 = None) by by destruct Ha1.
- assert (Hrede1:head_reducible e1 σ).
- { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
+ assert (Hrede1:base_reducible e1 σ).
+ { eapply (next_access_base_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
- assert (Hnse1:head_reduce_not_to_stuck e1 σ).
+ assert (Hnse1:base_reduce_not_to_stuck e1 σ).
{ eapply (safe_not_reduce_to_stuck _ _ K1); first done. set_solver+. }
- assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
+ assert (Hσe1:=next_access_base_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
- { intros. eapply next_access_head_Na1Ord_step, Hstep1.
+ { intros. eapply next_access_base_Na1Ord_step, Hstep1.
by destruct a1; simpl in *; subst. }
assert (Hrtc_step1:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1' :: t2 ++ fill K2 e2 :: t3 ++ ef1, σ1')).
{ eapply rtc_l, rtc_refl. eexists. eapply step_atomic, Ectx_step, Hstep1; try done.
by rewrite -assoc. }
- assert (Hrede1: a1.2 = Na1Ord → head_reducible e1' σ1').
+ assert (Hrede1: a1.2 = Na1Ord → base_reducible e1' σ1').
{ destruct a1 as [a1 []]=>// _.
- eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
+ eapply (next_access_base_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
fill_not_val=>//.
- by auto.
- abstract set_solver.
- by destruct Hstep1; inversion Ha1. }
- assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
+ assert (Hnse1: base_reduce_not_to_stuck e1' σ1').
{ eapply (safe_step_not_reduce_to_stuck _ _ K1); first done; last done. set_solver+. }
assert (to_val e2 = None) by by destruct Ha2.
- assert (Hrede2:head_reducible e2 σ).
- { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
+ assert (Hrede2:base_reducible e2 σ).
+ { eapply (next_access_base_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
- assert (Hnse2:head_reduce_not_to_stuck e2 σ).
+ assert (Hnse2:base_reduce_not_to_stuck e2 σ).
{ eapply (safe_not_reduce_to_stuck _ _ K2); first done. set_solver+. }
- assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
+ assert (Hσe2:=next_access_base_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
- { intros. eapply next_access_head_Na1Ord_step, Hstep2.
+ { intros. eapply next_access_base_Na1Ord_step, Hstep2.
by destruct a2; simpl in *; subst. }
assert (Hrtc_step2:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1 :: t2 ++ fill K2 e2' :: t3 ++ ef2, σ2')).
{ eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc. eexists.
eapply step_atomic, Ectx_step, Hstep2; try done. by rewrite -assoc. }
- assert (Hrede2: a2.2 = Na1Ord → head_reducible e2' σ2').
+ assert (Hrede2: a2.2 = Na1Ord → base_reducible e2' σ2').
{ destruct a2 as [a2 []]=>// _.
- eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
+ eapply (next_access_base_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
fill_not_val=>//.
- by auto.
- abstract set_solver.
- by destruct Hstep2; inversion Ha2. }
- assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
+ assert (Hnse2':base_reduce_not_to_stuck e2' σ2').
{ eapply (safe_step_not_reduce_to_stuck _ _ K2); first done; last done. set_solver+. }
assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
- { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
+ { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
- assert (Hrede1_2: head_reducible e2 σ1').
- { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ a2 l K2), Hsafe, fill_not_val=>//.
+ assert (Hrede1_2: base_reducible e2 σ1').
+ { intros. eapply (next_access_base_reductible_ctx e2 σ1' σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
- assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
+ assert (Hnse1_2:base_reduce_not_to_stuck e2 σ1').
{ eapply (safe_not_reduce_to_stuck _ _ K2).
- intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe1'1:=
- λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
+ λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
assert (Hσe1'2:=
- λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
+ λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
- { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
+ { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
- assert (Hrede2_1: head_reducible e1 σ2').
- { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
+ assert (Hrede2_1: base_reducible e1 σ2').
+ { intros. eapply (next_access_base_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
- assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
+ assert (Hnse2_1:base_reduce_not_to_stuck e1 σ2').
{ eapply (safe_not_reduce_to_stuck _ _ K1).
- intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe2'1:=
- λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
+ λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
assert (Hσe2'2:=
- λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
+ λ Hord, next_access_base_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
assert (a1.1 = FreeAcc → False).
{ destruct a1 as [[]?]; inversion 1.
- eauto using next_access_head_Free_concurent_step. }
+ eauto using next_access_base_Free_concurent_step. }
assert (a2.1 = FreeAcc → False).
{ destruct a2 as [[]?]; inversion 1.
- eauto using next_access_head_Free_concurent_step. }
+ eauto using next_access_base_Free_concurent_step. }
destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
repeat match goal with
@@ -290,7 +290,7 @@ Proof.
clear κ2' e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1.
destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
- inv_head_step.
+ inv_base_step.
match goal with
| H : <[?l:=_]> ?σ !! ?l = _ |- _ => by rewrite lookup_insert in H
end.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 206c2888..993b79e7 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -232,12 +232,12 @@ Ltac simpl_subst :=
Global Arguments W.to_expr : simpl never.
Global Arguments subst : simpl never.
-(** The tactic [inv_head_step] performs inversion on hypotheses of the
-shape [head_step]. The tactic will discharge head-reductions starting
+(** The tactic [inv_base_step] performs inversion on hypotheses of the
+shape [base_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
to values, and finite map operations. This tactic is slightly ad-hoc
and tuned for proving our lifting lemmas. *)
-Ltac inv_head_step :=
+Ltac inv_base_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
@@ -245,7 +245,7 @@ Ltac inv_head_step :=
apply (f_equal (to_val)) in H; rewrite to_of_val in H;
injection H; clear H; intro
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
- | H : head_step ?e _ _ _ _ _ |- _ =>
+ | H : base_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index da85d29a..8b101078 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -94,7 +94,7 @@ Section borrow.
wp_apply (wp_hasty with "Hp"). iIntros ([[|l|]|]) "_ Hown"; try done.
iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']"; first 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↦#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]"; first done.
@@ -103,7 +103,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.
@@ -158,7 +158,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']"; first 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 bfbac4ea..47b7e97f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -120,7 +120,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 "Hb" as (i) "(#Hpb&Hpbown)".
set (C := (∃ _ _ _, _ ∗ _ ∗ &at{_,_} _)%I).
@@ -181,7 +181,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 (γ ν q) "(#Hpersist & Htk & Hν)".
iRight. iExists _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
- iIntros "%κ %tid %l #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -241,7 +241,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 "Hb" as (i) "(#Hpb&Hpbown)".
set (C := (∃ _ _, _ ∗ &at{_,_} _)%I).
@@ -349,11 +349,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.
@@ -364,7 +364,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.
@@ -389,11 +389,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ν").
@@ -402,7 +402,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 (γ) "[Ha Htok]".
{ rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
@@ -430,7 +430,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. *)
@@ -449,7 +449,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.
@@ -767,7 +767,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†"); [solve_ndisj..|].
@@ -778,15 +778,15 @@ Section arc.
iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
{ unfold P2. auto with iFrame. }
wp_apply (drop_weak_spec with "[//] Htok"). 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†]").
{ 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.
@@ -823,7 +823,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 "[-]"); [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) ]
@@ -870,12 +870,12 @@ 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†"); [solve_ndisj..|].
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']"); rewrite /= ?firstn_length_le; try lia.
@@ -887,14 +887,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 "[-]"); [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..|].
@@ -938,7 +938,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.
@@ -1024,7 +1024,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 (γ ν q') "[#(Hi & Hs & #Hc) Htoks]". wp_let.
@@ -1035,7 +1035,7 @@ Section arc.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
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;
@@ -1050,7 +1050,7 @@ Section arc.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
wp_apply wp_new=>//; first lia. iIntros (l) "(H†& Hlvl) (#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.
@@ -1059,7 +1059,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;
@@ -1072,7 +1072,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
iIntros (l) "/= (H†& Hl)". 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 //. }
@@ -1083,7 +1083,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]".
@@ -1091,7 +1091,7 @@ Section arc.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
wp_apply wp_new=>//; first lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
- rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc.
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. } { by rewrite Hsz. }
@@ -1101,7 +1101,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 29577ea8..4cbc56fc 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -138,8 +138,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.
@@ -184,7 +184,7 @@ Section typing.
wp_case.
wp_alloc n as "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
@@ -195,7 +195,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.
@@ -274,7 +274,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.
@@ -338,7 +338,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.
@@ -384,7 +384,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.
@@ -398,7 +398,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 1383b30b..3405077e 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -68,7 +68,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 54ab58f0..c7ccb91e 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; first set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_incl_syn_sem. }
@@ -54,7 +54,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; first set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_intersect_incl_l.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 4860947f..e0830e40 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -42,7 +42,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↦ 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. *)
@@ -50,7 +50,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.b2z b) :: vl).
- rewrite heap_mapsto_vec_cons. iFrame. iPureIntro. eauto. }
+ rewrite heap_pointsto_vec_cons. iFrame. 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.
@@ -99,7 +99,7 @@ Section mutex.
- iIntros "!> %κ %tid %l Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
- iApply heap_mapsto_pred_iff_proper.
+ iApply heap_pointsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
Qed.
@@ -120,7 +120,7 @@ Section mutex.
iIntros (???? l) "Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
- iApply heap_mapsto_pred_iff_proper.
+ iApply heap_pointsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
Qed.
End mutex.
@@ -149,9 +149,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]"); [by rewrite vec_to_list_length..|].
iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
@@ -163,7 +163,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. iFrame; eauto. }
+ - iExists (#false :: vl). rewrite heap_pointsto_vec_cons. iFrame; eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -186,9 +186,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 Hvlm]".
+ iDestruct (heap_pointsto_ty_own with "Hm") as (vlm) "[>Hm 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]"); [by rewrite vec_to_list_length..|].
@@ -201,7 +201,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.
@@ -228,11 +228,11 @@ Section code.
iMod (bor_acc_cons with "LFT Hm' Hα") as "[Hm' Hclose2]"; first done.
wp_op. iDestruct "Hm'" as (vl) "[H↦ 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. done. }
+ iExists (_ :: _). rewrite heap_pointsto_vec_cons. do 2 iFrame. done. }
{ 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 b9c67b55..08a0db07 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -50,7 +50,7 @@ Section mguard.
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.
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.
+ iApply at_bor_shorten; first by iApply lft_incl_syn_sem.
iApply (at_bor_iff with "[] Hinv"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
- iApply heap_mapsto_pred_iff_proper.
+ iApply heap_pointsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
+ iApply bor_iff; last done. iNext.
- 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".
@@ -180,7 +180,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..|].
wp_apply (acquire_spec with "[] Hα"); first by iApply (mutex_acc with "LFT Hshr Hακ'").
@@ -191,7 +191,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 "#∗". }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -221,7 +221,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 9e3f2ad0..cc75fa98 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -134,7 +134,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 "Hb" as (i) "(#Hpb&Hpbown)".
set (C := (∃ _ _ _, _ ∗ _ ∗ &na{_,_,_} _)%I).
@@ -214,7 +214,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 "%κ %tid %l #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -524,11 +524,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.
@@ -539,7 +539,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.
@@ -566,7 +566,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.
@@ -606,7 +606,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.
@@ -628,7 +628,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. *)
@@ -647,7 +647,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.
@@ -727,7 +727,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.
@@ -822,7 +822,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.
@@ -885,8 +885,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.
@@ -899,7 +899,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;
@@ -912,7 +912,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.
@@ -924,7 +924,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.
@@ -1018,8 +1018,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.
@@ -1031,7 +1031,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;
@@ -1046,7 +1046,7 @@ Section code.
iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia; first done.
rewrite -!lock Nat2Z.id.
iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [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.
@@ -1056,7 +1056,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".
@@ -1071,7 +1071,7 @@ Section code.
iIntros (lr) "/= ([H†|%] & H↦lr)"; 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.
@@ -1098,7 +1098,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]".
@@ -1106,7 +1106,7 @@ Section code.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
wp_apply wp_new=>//; first lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
- rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+ rewrite !heap_pointsto_vec_cons shift_loc_assoc.
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. } { by rewrite Hsz. }
@@ -1116,7 +1116,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 2239d898..569e39ca 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 "Hb" as (i) "(#Hpb&Hpbown)".
set (C := (∃ _ _, _ ∗ &na{_,_,_} _)%I).
@@ -140,7 +140,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..|].
@@ -182,7 +182,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.
@@ -199,7 +199,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 *)
@@ -215,7 +215,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.
@@ -242,7 +242,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.
@@ -278,7 +278,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.
@@ -306,7 +306,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.
@@ -350,7 +350,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.
@@ -425,7 +425,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.
@@ -456,10 +456,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.
@@ -469,7 +469,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 506c0454..2c381d7c 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -63,7 +63,7 @@ Section ref_functions.
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]"; first 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')".
@@ -77,7 +77,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]".
@@ -117,7 +117,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α]"; first 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..|].
@@ -151,7 +151,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..|].
@@ -188,7 +188,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.
@@ -219,11 +219,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..|].
@@ -233,7 +233,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ν]".
@@ -241,14 +241,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.
@@ -298,11 +298,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..|].
@@ -312,7 +312,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ν]".
@@ -321,10 +321,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]"; first done.
@@ -342,10 +342,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]".
@@ -357,7 +357,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 d4911684..7c4b2403 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -124,8 +124,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]"; first done.
iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]"; first done.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 2a6f1f34..68237cf7 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -29,7 +29,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.
@@ -38,7 +38,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.
@@ -63,7 +63,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.
@@ -71,7 +71,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..|].
@@ -98,11 +98,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.
@@ -169,7 +169,7 @@ Section refcell_functions.
simpl. iApply type_jump; solve_typing.
- wp_op. wp_write. wp_apply wp_new; [done..|].
iIntros (lref) "(H†& Hlref)". 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) ∗
@@ -216,7 +216,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; first done. iApply lft_incl_refl. }
iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
@@ -269,7 +269,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)". 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ν]"; first done.
@@ -294,7 +294,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 ccc5f4dc..a5f24d8a 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -30,7 +30,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]"; first 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]".
@@ -83,7 +83,7 @@ Section refmut_functions.
iMod (bor_fracture (λ q', (q * q').[ν])%I with "LFT [H]") as "H"; first done.
{ by rewrite Qp.mul_1_r. }
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↦ _]"; first done.
+ rewrite heap_pointsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]"; first done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]"; first done.
wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_let. iMod "Hb".
@@ -119,7 +119,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)";
@@ -159,7 +159,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.
@@ -190,11 +190,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..|].
@@ -204,7 +204,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ν]".
@@ -212,14 +212,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.
@@ -269,11 +269,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..|].
@@ -283,7 +283,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ν]".
@@ -292,10 +292,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]"; first done.
@@ -316,10 +316,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]".
@@ -332,7 +332,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 a34db311..24bb5841 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -135,8 +135,8 @@ Section rwlock.
(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|iExists _; iFrame]. }
iMod (bor_sep with "LFT H") as "[Hn Hvl]"; first done.
iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]"; first done.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index f4aba92a..f3038b00 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -31,7 +31,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.
@@ -40,7 +40,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.
@@ -65,7 +65,7 @@ Section rwlock_functions.
iDestruct "Hx" as "[Hx Hx†]".
iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ 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..|].
@@ -74,7 +74,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.
@@ -99,9 +99,9 @@ Section rwlock_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. iFrame.
+ iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. iFrame.
- iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try done.
- rewrite heap_mapsto_vec_cons.
+ rewrite heap_pointsto_vec_cons.
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 c796ae0b..7c984a6b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -30,7 +30,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α]"; first 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 33d062b8..ad717ed7 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -31,7 +31,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]"; first 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]".
@@ -77,7 +77,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"; first done.
iMod (bor_exists with "LFT H") as (δ) "H"; first done.
iMod (bor_exists with "LFT H") as (tid_shr) "H"; first done.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index f2f4c05d..3c51bb43 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -36,7 +36,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 5f027bee..0c315e44 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -71,7 +71,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 (λ q, l ↦{q} #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 6f77a8ca..7d4bf78f 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -21,7 +21,7 @@ Section product.
split; first 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.
@@ -38,12 +38,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.
@@ -132,7 +132,7 @@ Section product.
iDestruct (ty_size_eq with "H1") as "#>%".
iDestruct (ty_size_eq with "H2") as "#>%".
iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
- rewrite !heap_mapsto_vec_op; [|congruence..].
+ rewrite !heap_pointsto_vec_op; [|congruence..].
iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]"; first by iExists _; iFrame.
iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]"; last done. by iExists _; iFrame.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 8c227021..b652d36f 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 #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
- iExists (vl1 ++ vl2). rewrite heap_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 2409eef3..ab253010 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -80,7 +80,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. *)
@@ -253,8 +253,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 "$".
@@ -282,7 +282,7 @@ Section typing_rules.
(l vl q) "(% & Hl & Hown & Hclose)"; first done.
subst v. 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 33b9953a..17b45d45 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_op _ q' q'02); last (by intros; iApply ty_size_eq).
+ rewrite -(heap_pointsto_pred_op _ 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 366638aa..f2ae8ad1 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -497,7 +497,7 @@ Section type.
iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
{ iNext. iDestruct (st_size_eq with "Hown") as %->.
iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp.div_2.
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_pointsto_vec_op // Qp.div_2.
iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
@@ -793,7 +793,7 @@ End subtyping.
Section type_util.
Context `{!typeGS Σ}.
- 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 206da192..1ccdfae1 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_nat.
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.
@@ -72,7 +72,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.
@@ -84,7 +84,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; first by auto.
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
{ iExists vl'. iFrame. }
@@ -95,7 +95,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".
@@ -162,7 +162,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").
iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
@@ -171,12 +171,12 @@ Section case.
induction tyl as [|ty' tyl IH]=>//= -[|i] /=.
- intros [= ->]. simpl in *. lia.
- apply IH. 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.
@@ -205,11 +205,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)"; first 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.
@@ -243,7 +243,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"). iIntros (v2 Hv2) "Hty2".
rewrite typed_read_eq in Hr.
@@ -253,7 +253,7 @@ Section case.
induction tyl as [|ty' tyl IH]=>//= -[|i] /=.
- intros [= ->]. lia.
- specialize (IH 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]"); [|lia|].
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 2b22b368..6de5527f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -25,7 +25,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'. subst. rewrite heap_mapsto_vec_singleton.
+ iFrame. iExists l'. subst. rewrite heap_pointsto_vec_singleton.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
iApply delay_sharing_nested; try done. iApply lft_incl_refl.
Qed.
--
GitLab