diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index fcb1e0f8b91e6a58c59ef9ace28ce7c35178c386..256e076b177265279e36d722aef4a87bce2ed5b3 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 784b32e675d50de99b0a7d43e9b09b93f77a3e83..e77f27827510e4a3d1658791f5cfe3c814d24890 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 16a15295a5fead45a95c63f310fa5ddd0916f9ae..37a0c55f3543572ba95331a31d928015f010ee2b 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 9edcaae8dc916218ca6d3ca664837c0be11608b2..43ff59d1ecb8bbf805e92def80caa715dbe96fb1 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 2b1533507ad6da9be3f902d9a1ee6c7b365e0dde..7c7bef80947f844433139ea4b6ac9492228a7871 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 07a32237ac12a79036e8b03f2cfa96ea55f98ba9..e2777f892571510e1d4cb86bc9ce8c70260ce518 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 11f3cc450866241827abd1a834ccee156ee44e2d..996fa7854fc411f286b5cc27b9eeab77afd1d656 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 9de46d5961c1ecc349d1d0f1f68d40331ce4637a..398d16ac7b998fd957ad76b94793e7bf997a28bc 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 501581fd0aaeb8c8947d36b6815c163085627ff9..9d1d9fd757759aa744351bb33690b8d1af6f258b 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 206c28880427b65699f2ed02c98cfb6fe84260c0..993b79e7e365f1129b577d2a9cb38c6025e38004 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 da85d29a44884c46c339a9d0e44d1ec024b85c8b..8b1010782b2728eabff29bd063d4cff208e46772 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 bfbac4ea22294874c08dbb7cab62cda82cf47bb1..47b7e97f4b812d39e58d4cfb87a7d6d0900ec6ee 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 29577ea86c9c287ce2c9d55dd4492bae9f68ed47..4cbc56fcc9de78bd094c9a04995cf45d2122b475 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 1383b30b69e18d31791d80ce9aaaeb7615c1dc38..3405077ee74781787d59a31269114efde0135fb8 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 54ab58f06ef3e50883e6be8b1f44fa87e0b6b662..c7ccb91e9502965783fedc86d2d068ba8131f327 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 4860947f3e0d9c8a4ffe48e605b11ad867815ffb..e0830e404c098a6969865f883e08cd1b39f738bc 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 b9c67b55f999b40cf320bb06dd8a046432d9ad80..08a0db07355b2ffe31c17b439fef7cf1a69de328 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 9e3f2ad0d7da0768365ddf523d0e2220c7b4fa71..cc75fa98b3dbb126aa9b537b1ef2c2cc41b5473b 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 2239d898938bb388fca9920ea03deddf4fe68c5a..569e39ca82ea36b0c84e3579e6f71148c0e3c49f 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 506c0454d5af8c56573211687663cff2ad542d16..2c381d7cfbebd4df64b370099078387abf758351 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 d4911684494259e0272cdb233a9c2be6b6beb83d..7c4b240359c3af992548d724ce1cb075742195cd 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 2a6f1f34393f4566afffaf9da2d23ea916cba374..68237cf7293ab661b13644d065952dc9b36bd7f1 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 ccc5f4dc4564d43fddb2fa382903e4800f052a0c..a5f24d8aba1498abf72b14e3794c1cad5bda255c 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 a34db311822e9f10e43d43e76ca6b8545cd04f97..24bb58414b436d9414e4fd7c00fbfa8b5385e1da 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 f4aba92a1ad9549530b914d056ebb1c1539a3e4e..f3038b00d7082c6d4718dc3901f31f0b7d21a64f 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 c796ae0b74dbd295646d6680d0bb68b42b70202a..7c984a6bb1aa7d40adde7bd32a147e43b26b8e47 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 33d062b88b2e36112747ea11032f45bacee5084d..ad717ed752bb88379cb8a075704e6ebc0d5105c6 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 f2f4c05d2ec936f11971d725c5ffaedbfbf99687..3c51bb4377a3d94be21fe9201959378567974cd0 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 5f027bee3fc7415bd0920e9d13a4101e6b4775df..0c315e44cef0434e5c919eb8c920ab36f75f7543 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 6f77a8ca4d845737204c218e7515ab40decf2460..7d4bf78f23291f13fc3ec19f526c430baa3af303 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 8c2270214a6eeed30d1d2f818c5707fb346881bd..b652d36f65b191b0e995cd5bdc779e39fd20a6de 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 2409eef344c0abce43d76401628996bdd7a5856e..ab253010cf32ce3011f0ad2422279741b87bb26e 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 33b9953a1a656cb2e24a1460390a674fc2c50cf6..17b45d45078f838259e19c74abcc191adec9ed35 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 366638aa7bd7f9adca7fecb67b8d8fae50dc6153..f2ae8ad1bb8efc05c04d0820c08604eb9f3b1356 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 206da1922f877ba4596b3528c4892b04b6cccc85..1ccdfae180671778998b808f411c7a049fae5f09 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 2b22b368db1356a6c067343ce2bf345251434263..6de5527f3b8e6c29164fcd9bcb705065f641087f 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.