From e3ec5e48fe95e62342bd1d47042dfc15acae7e90 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 23 Nov 2016 14:31:46 +0100
Subject: [PATCH] Update wrt Iris.
---
iris | 2 +-
theories/adequacy.v | 2 +-
theories/frac_borrow.v | 24 ++++++-----
theories/heap.v | 97 ++++++++++++++++++++++--------------------
theories/lang.v | 1 -
theories/lifetime.v | 84 +++++++++++++++++++-----------------
theories/lifting.v | 8 ++--
theories/memcpy.v | 2 +-
theories/perm.v | 6 +--
theories/perm_incl.v | 12 +++---
theories/proofmode.v | 8 ++--
theories/shr_borrow.v | 20 +++++----
theories/tl_borrow.v | 10 ++---
theories/type.v | 60 +++++++++++++-------------
theories/type_incl.v | 2 +-
theories/typing.v | 28 ++++++------
16 files changed, 188 insertions(+), 178 deletions(-)
diff --git a/iris b/iris
index 8f33e282..f24fd7c3 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd
+Subproject commit f24fd7c35eb4e29c5fccb47200a22b7087fbcb64
diff --git a/theories/adequacy.v b/theories/adequacy.v
index 1cd713a0..e5c53aef 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -17,7 +17,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. intros [? [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv. split; apply _. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
- (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ■φ v }}) →
+ (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌠}}) →
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy Σ). iIntros (?) "Hσ".
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index f68755d8..5d695993 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -7,23 +7,23 @@ Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR.
Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
- (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
+ (⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ']))%I.
Notation "&frac{ κ } P" := (frac_borrow κ P)
(format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
Section frac_borrow.
-
Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
+ Implicit Types E : coPset.
Global Instance frac_borrow_proper :
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
Proof. solve_proper. Qed.
Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
- Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
- lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+ Lemma borrow_fracture φ E κ :
+ ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
Proof.
- iIntros "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+ iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H†Hclose]]". done.
- iMod ("Hclose" with "*[-]") as "Hφ"; last first.
{ iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
@@ -37,11 +37,12 @@ Section frac_borrow.
iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
Qed.
- Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
- lft_ctx ⊢ &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
- ∨ [†κ] ∗ |={E∖lftN,E}=> True.
+ Lemma frac_borrow_atomic_acc E κ φ :
+ ↑lftN ⊆ E →
+ lft_ctx ⊢ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
+ ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
- iIntros "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
+ iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
iMod (shr_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H†Hclose]]". done.
- iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
@@ -49,11 +50,12 @@ Section frac_borrow.
iApply fupd_intro_mask. set_solver. done.
Qed.
- Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
+ Lemma frac_borrow_acc E q κ φ:
+ ↑lftN ⊆ E →
lft_ctx ⊢ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
&frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
- iIntros "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
+ iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
diff --git a/theories/heap.v b/theories/heap.v
index 97087b8f..5e4a0ba9 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -62,7 +62,7 @@ Section definitions.
Definition heap_inv : iProp Σ :=
(∃ (σ:state) hF, ownP σ ∗ own heap_name (◠to_heap σ)
∗ own heap_freeable_name (◠hF)
- ∗ ■heap_freeable_rel σ hF)%I.
+ ∗ ⌜heap_freeable_rel σ hFâŒ)%I.
Definition heap_ctx : iProp Σ := inv heapN heap_inv.
Global Instance heap_ctx_persistent : PersistentP heap_ctx.
@@ -95,6 +95,7 @@ Section heap.
Context {Σ : gFunctors}.
Implicit Types P Q : iProp Σ.
Implicit Types σ : state.
+ Implicit Types E : coPset.
(** Allocation *)
Lemma to_heap_valid σ : ✓ to_heap σ.
@@ -129,10 +130,10 @@ Section heap.
Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
- l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
+ l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ ⌜v1 = v2⌠∧ l ↦{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
- { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
+ { by rewrite heap_mapsto_op_eq pure_True // left_id. }
apply (anti_symm (⊢)); last by apply pure_elim_l.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_own_valid /=.
@@ -166,20 +167,21 @@ Section heap.
Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
length vl1 = length vl2 →
- l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ vl1 = vl2 ∧ l ↦∗{q1+q2} vl1.
+ l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌠∧ l ↦∗{q1+q2} vl1.
Proof.
- iIntros (Hlen%Forall2_same_length); iSplit.
+ 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]]".
- iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]"; subst; first by iFrame.
+ iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]";
+ subst; first by iFrame.
rewrite (inj_iff (:: vl2)). iApply heap_mapsto_op. by iFrame.
- iIntros "[% Hl]"; subst. by iApply heap_mapsto_vec_op_eq.
Qed.
Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
- (∀ vl, Φ vl ⊢ length vl = n) →
- l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, length vl = n) ⊣⊢ l ↦∗{q1+q2}: Φ.
+ (∀ vl, Φ vl ⊢ ⌜length vl = nâŒ) →
+ l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = nâŒ) ⊣⊢ l ↦∗{q1+q2}: Φ.
Proof.
intros Hlen. iSplit.
- iIntros "[Hmt1 Hmt2]".
@@ -209,7 +211,7 @@ Section heap.
by rewrite (big_opL_commute_L (Auth None)) big_opL_commute1 //.
Qed.
- Lemma inter_lookup_Some i j (n:nat):
+ Lemma inter_lookup_Some i j (n : nat):
i ≤ j < i+n → inter i n !! j = Excl' ().
Proof.
revert i. induction n as [|n IH]=>/= i; first lia.
@@ -322,10 +324,10 @@ Section heap.
rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
Qed.
- Lemma wp_alloc E n :
- nclose heapN ⊆ E → 0 < n →
+ Lemma wp_alloc E n:
+ ↑heapN ⊆ E → 0 < n →
{{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
- {{{ l vl, RET LitV $ LitLoc l; n = length vl ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+ {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌠∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
Proof.
iIntros (???) "#Hinv HΦ". rewrite /heap_ctx /heap_inv.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -368,8 +370,7 @@ Section heap.
Qed.
Lemma wp_free E (n:Z) l vl :
- nclose heapN ⊆ E →
- n = length vl →
+ ↑heapN ⊆ E → n = length vl →
{{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
{{{ RET LitV LitUnit; True }}}.
@@ -377,7 +378,7 @@ Section heap.
iIntros (???Φ) "(#Hinv & >Hmt & >Hf) HΦ". rewrite /heap_ctx /heap_inv.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
rewrite heap_freeable_eq /heap_freeable_def.
- iDestruct (own_valid_2 with "[$HhF $Hf]") as % [Hl Hv]%auth_valid_discrete_2.
+ iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -388,7 +389,7 @@ Section heap.
{ intros i. subst n. eauto using heap_freeable_is_Some. }
iNext. iIntros "Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
{ rewrite heap_mapsto_vec_combine //. iFrame. }
- iMod (own_update_2 with "[$HhF $Hf]") as "HhF".
+ iMod (own_update_2 with "HhF Hf") as "HhF".
{ apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
iMod ("Hclose" with "[-HΦ]") as "_"; last by iApply "HΦ".
iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
@@ -396,12 +397,13 @@ Section heap.
Qed.
Lemma heap_mapsto_lookup l ls q v σ:
- own heap_name (◠to_heap σ) ∗
- own heap_name (â—¯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]})
- ⊢ ■∃ n' : nat,
- σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v).
+ own heap_name (◠to_heap σ) ⊢
+ own heap_name (◯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]}) -∗
+ ⌜∃ n' : nat,
+ σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)âŒ.
Proof.
- rewrite own_valid_2. iDestruct 1 as %[Hl?]%auth_valid_discrete_2.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_valid_discrete_2.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
rewrite leibniz_equiv_iff /to_heap lookup_fmap fmap_Some.
move=> [[[ls'' v'] [??]]]; simplify_eq.
@@ -413,11 +415,12 @@ Section heap.
Qed.
Lemma heap_mapsto_lookup_1 l ls v σ:
- own heap_name (◠to_heap σ) ∗
- own heap_name (â—¯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]})
- ⊢ ■(σ !! l = Some (ls, v)).
+ own heap_name (◠to_heap σ) ⊢
+ own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]}) -∗
+ ⌜σ !! l = Some (ls, v)âŒ.
Proof.
- rewrite own_valid_2. iDestruct 1 as %[Hl?]%auth_valid_discrete_2.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_valid_discrete_2.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
rewrite leibniz_equiv_iff /to_heap lookup_fmap fmap_Some.
move=> [[[ls'' v'] [??]] Hincl]; simplify_eq.
@@ -427,14 +430,14 @@ Section heap.
Qed.
Lemma wp_read_sc E l q v :
- nclose heapN ⊆ E →
+ ↑heapN ⊆ E →
{{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (??) "[#Hinv >Hv] HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
iApply (wp_read_sc_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
iNext. iExists σ, hF. iFrame. eauto.
@@ -454,7 +457,7 @@ Section heap.
Qed.
Lemma wp_read_na E l q v :
- nclose heapN ⊆ E →
+ ↑heapN ⊆ E →
{{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
@@ -462,15 +465,15 @@ Section heap.
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iApply (wp_read_na1_pst E).
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
iMod (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+ iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
iModIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
{ iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
iModIntro. clear dependent n σ hF.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
iApply (wp_read_na2_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -490,14 +493,14 @@ Section heap.
Qed.
Lemma wp_write_sc E l e v v' :
- nclose heapN ⊆ E → to_val e = Some v →
+ ↑heapN ⊆ E → to_val e = Some v →
{{{ heap_ctx ∗ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
{{{ RET LitV LitUnit; l ↦ v }}}.
Proof.
iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+ iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
iApply (wp_write_sc_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -505,7 +508,7 @@ Section heap.
Qed.
Lemma wp_write_na E l e v v' :
- nclose heapN ⊆ E → to_val e = Some v →
+ ↑heapN ⊆ E → to_val e = Some v →
{{{ heap_ctx ∗ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
{{{ RET LitV LitUnit; l ↦ v }}}.
Proof.
@@ -513,15 +516,15 @@ Section heap.
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iApply (wp_write_na1_pst E).
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+ iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+ iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
iModIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
{ iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
iModIntro. clear dependent σ hF.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+ iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
iApply (wp_write_na2_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
@@ -529,7 +532,7 @@ Section heap.
Qed.
Lemma wp_cas_int_fail E l q z1 e2 v2 zl :
- nclose heapN ⊆ E → to_val e2 = Some v2 → z1 ≠zl →
+ ↑heapN ⊆ E → to_val e2 = Some v2 → z1 ≠zl →
{{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
{{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
@@ -537,7 +540,7 @@ Section heap.
iIntros (? <-%of_to_val ??) "[#Hinv >Hv] HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
{ by rewrite /= bool_decide_false. }
iNext. iIntros "Hσ". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -545,7 +548,7 @@ Section heap.
Qed.
Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' :
- nclose heapN ⊆ E → to_val e2 = Some v2 → l1 ≠l' →
+ ↑heapN ⊆ E → to_val e2 = Some v2 → l1 ≠l' →
{{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
{{{ RET LitV $ LitInt 0;
@@ -554,9 +557,9 @@ Section heap.
iIntros (? <-%of_to_val ??) "(#Hinv & >Hl & >Hl' & >Hl1) HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl]") as %[n Hσl].
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl']") as %[n' Hσl'].
- iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl1]") as %[n1 Hσl1].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hl") as %[n Hσl].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hl'") as %[n' Hσl'].
+ iDestruct (heap_mapsto_lookup with "Hvalσ Hl1") as %[n1 Hσl1].
iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
{ by rewrite /= bool_decide_false // Hσl1 Hσl'. }
iNext. iIntros "Hσ ".
@@ -565,7 +568,7 @@ Section heap.
Qed.
Lemma wp_cas_int_suc E l z1 e2 v2 :
- nclose heapN ⊆ E → to_val e2 = Some v2 →
+ ↑heapN ⊆ E → to_val e2 = Some v2 →
{{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
{{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
@@ -573,7 +576,7 @@ Section heap.
iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+ iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
{ by rewrite /= bool_decide_true. }
iNext. iIntros "Hσ".
@@ -583,7 +586,7 @@ Section heap.
Qed.
Lemma wp_cas_loc_suc E l l1 e2 v2 :
- nclose heapN ⊆ E → to_val e2 = Some v2 →
+ ↑heapN ⊆ E → to_val e2 = Some v2 →
{{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
{{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
@@ -591,7 +594,7 @@ Section heap.
iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+ iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
{ by rewrite /= bool_decide_true. }
iNext. iIntros "Hσ".
diff --git a/theories/lang.v b/theories/lang.v
index 8b2f09a9..8acb16cc 100644
--- a/theories/lang.v
+++ b/theories/lang.v
@@ -1,5 +1,4 @@
From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.algebra Require Export cofe.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 193be22d..bbc61eef 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -42,7 +42,7 @@ Section defs.
own lft_toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
Definition lft_dead (κ : lifetime) : iProp Σ :=
- (∃ Λ, ■(∃ n, κ !! Λ = Some (S n)) ∗
+ (∃ Λ, ⌜∃ n, κ !! Λ = Some (S n)⌠∗
own lft_toks_name (◯ {[ Λ := Cinr () ]}))%I.
Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
@@ -132,42 +132,42 @@ Section lft.
Qed.
Axiom lft_create :
- ∀ `(nclose lftN ⊆ E),
- lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
+ ∀ `(↑lftN ⊆ E),
+ lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
Axiom idx_borrow_acc :
- ∀ `(nclose lftN ⊆ E) q κ i P,
+ ∀ `(↑lftN ⊆ E) q κ i P,
lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own 1 i
-∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
Axiom idx_borrow_atomic_acc :
- ∀ `(nclose lftN ⊆ E) q κ i P,
+ ∀ `(↑lftN ⊆ E) q κ i P,
lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own q i
- ={E,E∖lftN}=∗
- ▷ P ∗ (▷ P ={E∖lftN,E}=∗ idx_borrow_own q i) ∨
- [†κ] ∗ (|={E∖lftN,E}=> idx_borrow_own q i).
+ ={E,E∖↑lftN}=∗
+ ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_borrow_own q i) ∨
+ [†κ] ∗ (|={E∖↑lftN,E}=> idx_borrow_own q i).
(** Basic borrows *)
Axiom borrow_create :
- ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
- Axiom borrow_fake : ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+ ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+ Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
Axiom borrow_split :
- ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
+ ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
Axiom borrow_combine :
- ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
+ ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
Axiom borrow_acc_strong :
- ∀ `(nclose lftN ⊆ E) q κ P,
+ ∀ `(↑lftN ⊆ E) q κ P,
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
- ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
+ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
Axiom borrow_acc_atomic_strong :
- ∀ `(nclose lftN ⊆ E) κ P,
- lft_ctx ⊢ &{κ}P ={E,E∖lftN}=∗
- (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E∖lftN,E}=∗ &{κ}Q) ∨
- [†κ] ∗ |={E∖lftN,E}=> True.
+ ∀ `(↑lftN ⊆ E) κ P,
+ lft_ctx ⊢ &{κ}P ={E,E∖↑lftN}=∗
+ (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ}Q) ∨
+ [†κ] ∗ |={E∖↑lftN,E}=> True.
Axiom borrow_reborrow' :
- ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
+ ∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Axiom borrow_unnest :
- ∀ `(nclose lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
+ ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
(*** Derived lemmas *)
@@ -176,7 +176,7 @@ Section lft.
rewrite /lft_own /lft_dead.
iIntros "Hl Hr". iDestruct "Hr" as (Λ) "[HΛ Hr]".
iDestruct "HΛ" as %[n HΛ].
- iDestruct (own_valid_2 with "[$Hl $Hr]") as %Hval. iPureIntro.
+ iDestruct (own_valid_2 with "Hl Hr") as %Hval. iPureIntro.
generalize (Hval Λ).
by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
Qed.
@@ -224,34 +224,37 @@ Section lft.
FromSep q.[κ1⋅κ2] q.[κ1] q.[κ2].
Proof. by rewrite /FromSep lft_own_op. Qed.
- Lemma borrow_acc E q κ P : nclose lftN ⊆ E →
- lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+ Lemma borrow_acc E q κ P :
+ ↑lftN ⊆ E →
+ lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
Qed.
- Lemma borrow_exists {A} `(nclose lftN ⊆ E) κ (Φ : A → iProp Σ) {_:Inhabited A}:
+ Lemma borrow_exists {A} E κ (Φ : A → iProp Σ) {_:Inhabited A}:
+ ↑lftN ⊆ E →
lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
Proof.
- iIntros "#LFT Hb".
+ iIntros (?) "#LFT Hb".
iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H†Hclose]]". done.
- iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>_?". eauto.
- iMod "Hclose" as "_". iExists inhabitant. by iApply (borrow_fake with "LFT").
Qed.
- Lemma borrow_or `(nclose lftN ⊆ E) κ P Q:
- lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+ Lemma borrow_or E κ P Q:
+ ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
- iIntros "#LFT H". rewrite uPred.or_alt.
+ iIntros (?) "#LFT H". rewrite uPred.or_alt.
iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
Qed.
- Lemma borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
+ Lemma borrow_persistent E `{PersistentP _ P} κ q:
+ ↑lftN ⊆ E →
lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
- iIntros "#LFT Hb Htok".
+ iIntros (?) "#LFT Hb Htok".
iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
by iMod ("Hob" with "HP") as "[_$]".
Qed.
@@ -263,8 +266,8 @@ Typeclasses Opaque borrow.
(*** Inclusion and shortening. *)
Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
- (□((∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ])) ∗
- ([†κ'] ={lftN}=∗ [†κ])))%I.
+ (□((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+ ([†κ'] ={↑lftN}=∗ [†κ])))%I.
Infix "⊑" := lft_incl (at level 60) : C_scope.
@@ -273,17 +276,18 @@ Section incl.
Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
- Lemma lft_incl_acc `(nclose lftN ⊆ E) κ κ' q:
+ Lemma lft_incl_acc E κ κ' q:
+ ↑lftN ⊆ E →
κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Proof.
- iIntros "#[H _] Hq". iApply fupd_mask_mono. eassumption.
+ iIntros (?) "#[H _] Hq". iApply fupd_mask_mono. eassumption.
iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
Qed.
- Lemma lft_incl_dead `(nclose lftN ⊆ E) κ κ': κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+ Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
Proof.
- iIntros "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
+ iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
Qed.
Lemma lft_le_incl κ κ': κ' ≼ κ → True ⊢ κ ⊑ κ'.
@@ -338,11 +342,11 @@ Section incl.
- iIntros "?". by iDestruct (lft_not_dead_static with "[-]") as "[]".
Qed.
- Lemma reborrow `(nclose lftN ⊆ E) P κ κ':
- lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+ Lemma reborrow E P κ κ':
+ ↑lftN ⊆ E → lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
- iIntros "#LFT #H⊑ HP". iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]".
- done. by exists κ'.
+ iIntros (?) "#LFT #H⊑ HP".
+ iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]". done. by exists κ'.
iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
{ iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
diff --git a/theories/lifting.v b/theories/lifting.v
index 26ba40bd..e3f6b3fa 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -26,8 +26,8 @@ Lemma wp_alloc_pst E σ n:
0 < n →
{{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
{{{ l σ', RET LitV $ LitLoc l;
- ■(∀ m, σ !! (shift_loc l m) = None) ∗
- ■(∃ vl, n = length vl ∧ init_mem l vl σ = σ') ∗
+ ⌜∀ m, σ !! (shift_loc l m) = None⌠∗
+ ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌠∗
ownP σ' }}}.
Proof.
iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
@@ -66,7 +66,7 @@ Proof.
Qed.
Lemma wp_read_na1_pst E l Φ :
- (|={E,∅}=> ∃ σ n v, σ !! l = Some(RSt $ n, v) ∧
+ (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌠∧
▷ ownP σ ∗
▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
@@ -97,7 +97,7 @@ Proof.
Qed.
Lemma wp_write_na1_pst E l v Φ :
- (|={E,∅}=> ∃ σ v', σ !! l = Some(RSt 0, v') ∧
+ (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌠∧
▷ ownP σ ∗
▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}))
diff --git a/theories/memcpy.v b/theories/memcpy.v
index 4fb6d9a2..e945532f 100644
--- a/theories/memcpy.v
+++ b/theories/memcpy.v
@@ -18,7 +18,7 @@ Notation "e1 <-[ i ]{ n } ! e2" :=
format "e1 <-[ i ]{ n } ! e2") : lrust_expr_scope.
Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
- nclose heapN ⊆ E →
+ ↑heapN ⊆ E →
length vl1 = n → length vl2 = n →
{{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
diff --git a/theories/perm.v b/theories/perm.v
index fbe763f4..6638a701 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -24,14 +24,14 @@ Section perm.
from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
Definition extract (κ : lifetime) (Ï : perm) : perm :=
- λ tid, ([†κ] ={lftN}=∗ Ï tid)%I.
+ λ tid, ([†κ] ={↑lftN}=∗ Ï tid)%I.
Definition tok (κ : lifetime) (q : Qp) : perm :=
λ _, q.[κ]%I.
Definition killable (κ : lifetime) : perm :=
- λ _, (□ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]))%I.
+ λ _, (□ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]))%I.
Definition incl (κ κ' : lifetime) : perm :=
λ _, (κ ⊑ κ')%I.
@@ -105,7 +105,7 @@ Section has_type.
Qed.
Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
- (ν ◠ty)%P tid ∗ (∀ (v : val), eval_expr ν = Some v ∗ (v ◠ty)%P tid ={E}=∗ Φ v)
+ (ν ◠ty)%P tid ∗ (∀ (v : val), ⌜eval_expr ν = Some v⌠∗ (v ◠ty)%P tid ={E}=∗ Φ v)
⊢ WP ν @ E {{ Φ }}.
Proof.
iIntros "[H◠HΦ]". setoid_rewrite has_type_value. unfold has_type.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 4d646f39..93eebced 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -125,7 +125,7 @@ Section props.
iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)".
subst. rewrite heap_mapsto_vec_app -heap_freeable_op_eq.
iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
- iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+ iAssert (â–· ⌜length vl1 = ty_size ty1âŒ)%I with "[#]" as ">EQ".
{ iNext. by iApply ty_size_eq. }
iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
+ iExists _. iSplitR. done. iFrame. iExists _. by iFrame.
@@ -136,7 +136,7 @@ Section props.
iExists l. iSplitR. done. rewrite -heap_freeable_op_eq. 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.
- iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+ iAssert (â–· ⌜length vl1 = ty_size ty1âŒ)%I with "[#]" as ">EQ".
{ iNext. by iApply ty_size_eq. }
iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
Qed.
@@ -275,7 +275,7 @@ Section props.
destruct (eval_expr ν) as [[[|l|]|]|];
try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
- iApply (fupd_mask_mono lftN). done.
+ iApply (fupd_mask_mono (↑lftN)). done.
iMod (borrow_create with "LFT Hown") as "[Hbor Hext]". done.
iSplitL "Hbor". by simpl; eauto.
iMod (borrow_create with "LFT Hf") as "[_ Hf]". done.
@@ -291,7 +291,7 @@ Section props.
destruct (eval_expr ν) as [[[|l|]|]|];
try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
- iApply (fupd_mask_mono lftN). done.
+ iApply (fupd_mask_mono (↑lftN)). done.
iMod (reborrow with "LFT Hord H") as "[H Hextr]". done.
iModIntro. iSplitL "H". iExists _. by eauto.
iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
@@ -299,8 +299,8 @@ Section props.
Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
Proof.
- iIntros (tid) "#LFT _ Htok". iApply fupd_mask_mono. done.
- iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". reflexivity.
+ iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
{ by rewrite Qp_mult_1_r. }
iSplitL "Hbor". iApply (frac_borrow_incl with "LFT Hbor").
diff --git a/theories/proofmode.v b/theories/proofmode.v
index ade46392..7c1cde57 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -21,7 +21,7 @@ Global Instance into_and_mapsto_vec l q vl :
Proof. by rewrite /IntoAnd heap_mapsto_vec_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
- (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → 0 < n →
+ (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
IntoLaterEnvs Δ Δ' →
(∀ l vl, n = length vl → ∃ Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
@@ -39,7 +39,7 @@ Proof.
Qed.
Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
- (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → n = length vl →
+ (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
IntoLaterEnvs Δ Δ' →
envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
envs_delete i1 false Δ' = Δ'' →
@@ -57,7 +57,7 @@ Proof.
Qed.
Lemma tac_wp_read Δ Δ' E i l q v o Φ :
- (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+ (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
(Δ' ⊢ |={E}=> Φ v) →
@@ -76,7 +76,7 @@ Qed.
Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
to_val e = Some v' →
- (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+ (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
IntoLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
index 65714ea6..a4eed050 100644
--- a/theories/shr_borrow.v
+++ b/theories/shr_borrow.v
@@ -16,17 +16,18 @@ Section shared_borrows.
Proof. solve_proper. Qed.
Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
- Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
+ Lemma borrow_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
Proof.
- iIntros "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
+ iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#". iApply inv_alloc. auto.
Qed.
- Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ :
- lft_ctx ⊢ &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
- [†κ] ∗ |={E∖lftN,E}=> True.
+ Lemma shr_borrow_acc E κ :
+ ↑lftN ⊆ E →
+ lft_ctx ⊢ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+ [†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
- iIntros "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+ iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
iInv lftN as (q') ">Hq'" "Hclose".
rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
@@ -35,10 +36,11 @@ Section shared_borrows.
- iRight. iFrame. iIntros "!>". by iMod "Hclose".
Qed.
- Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
- lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
+ Lemma shr_borrow_acc_tok E q κ :
+ ↑lftN ⊆ E →
+ lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
Proof.
- iIntros "#LFT #Hshr Hκ".
+ iIntros (?) "#LFT #Hshr Hκ".
iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H†_]]". done.
- iIntros "!>HP". by iMod ("Hclose" with "HP").
- iDestruct (lft_own_dead with "Hκ H†") as "[]".
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index b85f4058..7dcd10f8 100644
--- a/theories/tl_borrow.v
+++ b/theories/tl_borrow.v
@@ -20,17 +20,17 @@ Section tl_borrow.
intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
Qed.
- Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+ Lemma borrow_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ|tid|N}P.
Proof.
- iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
+ iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
Qed.
Lemma tl_borrow_acc q κ E F :
- nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
+ ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
- ▷P ∗ tl_own tid (F ∖ N) ∗
- (▷P -∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
+ ▷P ∗ tl_own tid (F ∖ ↑N) ∗
+ (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
Proof.
iIntros (???) "#LFT#HP Hκ Htlown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
diff --git a/theories/type.v b/theories/type.v
index ebc124bc..abbe4b63 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -11,7 +11,7 @@ Class iris_typeG Σ := Iris_typeG {
type_frac_borrowG Σ :> frac_borrowG Σ
}.
-Definition mgmtE := nclose tlN ∪ lftN.
+Definition mgmtE := ↑tlN ∪ ↑lftN.
Definition lrustN := nroot .@ "lrust".
(* [perm] is defined here instead of perm.v in order to define [cont] *)
@@ -30,7 +30,7 @@ Record type :=
ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
- ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
+ ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_sizeâŒ;
(* The mask for starting the sharing does /not/ include the
namespace N, for allowing more flexibility for the user of
this type (typically for the [own] type). AFAIK, there is no
@@ -40,8 +40,8 @@ Record type :=
invariants, which does not need the mask. Moreover, it is
more consistent with thread-local tokens, which we do not
give any. *)
- ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
- lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
+ ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+ lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
lft_ctx ⊢ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
ty_shr_acc κ tid E F l q :
@@ -59,7 +59,7 @@ Record simple_type `{iris_typeG Σ} :=
{ st_size : nat;
st_own : thread_id → list val → iProp Σ;
- st_size_eq tid vl : st_own tid vl ⊢ length vl = st_size;
+ st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = st_sizeâŒ;
st_own_persistent tid vl : PersistentP (st_own tid vl) }.
Global Existing Instance st_own_persistent.
@@ -99,7 +99,7 @@ Next Obligation.
iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
+ iNext. iExists _. by iFrame.
+ iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
- iAssert (â–· (length vl = length vl'))%I as ">%".
+ iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
{ iNext.
iDestruct (st_size_eq with "Hown") as %->.
iDestruct (st_size_eq with "Hown'") as %->. done. }
@@ -137,15 +137,15 @@ Section types.
Next Obligation. intros. iIntros "_ []". Qed.
Program Definition unit : type :=
- {| st_size := 0; st_own tid vl := (vl = [])%I |}.
+ {| st_size := 0; st_own tid vl := ⌜vl = []âŒ%I |}.
Next Obligation. iIntros (tid vl) "%". simpl. by subst. Qed.
Program Definition bool : type :=
- {| st_size := 1; st_own tid vl := (∃ z:bool, vl = [ #z ])%I |}.
+ {| st_size := 1; st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]âŒ)%I |}.
Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
Program Definition int : type :=
- {| st_size := 1; st_own tid vl := (∃ z:Z, vl = [ #z ])%I |}.
+ {| st_size := 1; st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]âŒ)%I |}.
Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
Program Definition own (q : Qp) (ty : type) :=
@@ -157,7 +157,7 @@ Section types.
Since this assertion is timeless, this should not cause
problems. *)
- (∃ l:loc, vl = [ #l ] ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
+ (∃ l:loc, ⌜vl = [ #l ]⌠∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
ty_shr κ tid E l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
∀ q', □ (q'.[κ] ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
@@ -177,11 +177,11 @@ Section types.
iMod (borrow_split with "LFT Hb2") as "[Hb2 _]". set_solver.
iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
- iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
+ iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
+ replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite /borrow. iExists i. eauto. }
@@ -209,7 +209,7 @@ Section types.
Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl :=
- (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
+ (∃ l:loc, ⌜vl = [ #l ]⌠∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
ty_shr κ' tid E l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
∀ q', □ (q'.[κ ⋅ κ']
@@ -229,11 +229,11 @@ Section types.
rewrite heap_mapsto_vec_singleton.
iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
+ iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid (↑N) l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
+ replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ rewrite /borrow. eauto. }
@@ -262,14 +262,14 @@ Section types.
Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
{| st_size := 1;
st_own tid vl :=
- (∃ (l:loc), vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
+ (∃ (l:loc), ⌜vl = [ #l ]⌠∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
Next Obligation.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
Lemma split_prod_mt tid ty1 ty2 q l :
(l ↦∗{q}: λ vl,
- ∃ vl1 vl2, vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
+ ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
Proof.
iSplit; iIntros "H".
@@ -287,9 +287,9 @@ Section types.
{| ty_size := ty1.(ty_size) + ty2.(ty_size);
ty_dup := ty1.(ty_dup) && ty2.(ty_dup);
ty_own tid vl := (∃ vl1 vl2,
- vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
+ ⌜vl = vl1 ++ vl2⌠∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
ty_shr κ tid E l :=
- (∃ E1 E2, ■(E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E) ∗
+ (∃ E1 E2, ⌜E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E⌠∗
ty1.(ty_shr) κ tid E1 l ∗
ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
Next Obligation. intros ty1 ty2 tid vl [Hdup1 Hdup2]%andb_True. apply _. Qed.
@@ -304,7 +304,7 @@ Section types.
iMod (borrow_split with "LFT H") as "[H1 H2]". set_solver.
iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
- iModIntro. iExists (N .@ 1). iExists (N .@ 2). iFrame.
+ iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
Qed.
Next Obligation.
@@ -326,18 +326,18 @@ Section types.
destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.
- iAssert (â–· (length vl1 = ty1.(ty_size)))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl1 = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
{ iNext. by iApply ty_size_eq. }
- iAssert (â–· (length vl2 = ty2.(ty_size)))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl2 = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
{ iNext. by iApply ty_size_eq. }
iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
- iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
- iIntros "[H1 H2]".
iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
- iAssert (â–· (length vl1' = ty1.(ty_size)))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl1' = ty1.(ty_size)âŒ)%I with "[#]" as ">%".
{ iNext. by iApply ty_size_eq. }
- iAssert (â–· (length vl2' = ty2.(ty_size)))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl2' = ty2.(ty_size)âŒ)%I with "[#]" as ">%".
{ iNext. by iApply ty_size_eq. }
iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
rewrite !heap_mapsto_vec_op; try by congruence.
@@ -350,7 +350,7 @@ Section types.
Lemma split_sum_mt l tid q tyl :
(l ↦∗{q}: λ vl,
- ∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I
+ ∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ ty_own (nth i tyl emp) tid vl')%I
⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
Proof.
iSplit; iIntros "H".
@@ -369,7 +369,7 @@ Section types.
Proof. intros. constructor; done. Qed.
Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
- ty_own (nth i tyl emp) tid vl ⊢ length vl = n.
+ ty_own (nth i tyl emp) tid vl ⊢ ⌜length vl = nâŒ.
Proof.
iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
@@ -380,7 +380,7 @@ Section types.
Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
{| ty_size := S n; ty_dup := forallb ty_dup tyl;
ty_own tid vl :=
- (∃ (i : nat) vl', vl = #i :: vl' ∗ (nth i tyl emp).(ty_own) tid vl')%I;
+ (∃ (i : nat) vl', ⌜vl = #i :: vl'⌠∗ (nth i tyl emp).(ty_own) tid vl')%I;
ty_shr κ tid N l :=
(∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
(nth i tyl emp).(ty_shr) κ tid N (shift_loc l 1))%I
@@ -436,12 +436,12 @@ Section types.
Qed.
Program Definition uninit : type :=
- {| st_size := 1; st_own tid vl := (length vl = 1%nat)%I |}.
+ {| st_size := 1; st_own tid vl := ⌜length vl = 1%natâŒ%I |}.
Next Obligation. done. Qed.
Program Definition cont {n : nat} (Ï : vec val n → @perm Σ) :=
{| ty_size := 1; ty_dup := false;
- ty_own tid vl := (∃ f, vl = [f] ∗
+ ty_own tid vl := (∃ f, ⌜vl = [f]⌠∗
∀ vl, Ï vl tid -∗ tl_own tid ⊤
-∗ WP f (map of_val vl) {{λ _, False}})%I;
ty_shr κ tid N l := True%I |}.
@@ -459,7 +459,7 @@ Section types.
needs a Send closure). *)
Program Definition fn {A n} (Ï : A -> vec val n → @perm Σ) : type :=
{| st_size := 1;
- st_own tid vl := (∃ f, vl = [f] ∗ ∀ x vl,
+ st_own tid vl := (∃ f, ⌜vl = [f]⌠∗ ∀ x vl,
{{ Ï x vl tid ∗ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
Next Obligation.
iIntros (x n Ï tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index e2fdf2af..a7f34971 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -16,7 +16,7 @@ Section ty_incl.
object when it is shared. We place this property under the
hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
is still included in any other. *)
- ty2.(ty_shr) κ tid E l ∗ ty1.(ty_size) = ty2.(ty_size)).
+ ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)âŒ).
Global Instance ty_incl_refl Ï : Reflexive (ty_incl Ï).
Proof. iIntros (ty tid) "__!>". iSplit; iIntros "!#"; eauto. Qed.
diff --git a/theories/typing.v b/theories/typing.v
index bf0398bf..d7f653f8 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -142,7 +142,7 @@ Section typing.
Proof.
iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
- iApply (wp_frame_step_l with "[-]"); try done.
+ iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done.
iDestruct ("Hend" with "Htok") as "$". by wp_seq.
iIntros (v) "[#Hκ _]". by iApply fupd_mask_mono; last iApply "Hextr".
Qed.
@@ -173,10 +173,10 @@ Section typing.
Qed.
Definition consumes (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
- ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
+ ∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
lft_ctx ⊢ Ï1 ν tid -∗ tl_own tid ⊤ -∗
(∀ (l:loc) vl q,
- (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗{q} vl ∗
+ (⌜length vl = ty.(ty_size)⌠∗ ⌜eval_expr ν = Some #l⌠∗ l ↦∗{q} vl ∗
|={E}â–·=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ Ï2 ν tid ∗ tl_own tid ⊤)))
-∗ Φ #l)
-∗ WP ν @ E {{ Φ }}.
@@ -188,7 +188,7 @@ Section typing.
iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & H↦ & >H†)".
iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
@@ -202,7 +202,7 @@ Section typing.
iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "Hâ—" as (l) "(Heq & H↦ & >H†)".
iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
- iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">Hlen".
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">Hlen".
by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
@@ -224,7 +224,7 @@ Section typing.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
@@ -240,11 +240,11 @@ Section typing.
iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
rewrite has_type_value. iDestruct "Hâ—" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
- rewrite (union_difference_L (nclose lrustN) ⊤); last done.
+ rewrite (union_difference_L (↑lrustN) ⊤); last done.
setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
iMod (ty_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
by rewrite ty.(ty_size_eq).
iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
@@ -296,9 +296,9 @@ Section typing.
{ iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
iSpecialize ("Hown" $! _ with "Htok2").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
- - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ∗ v = #vl)%I); try done.
+ - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q'''} v ∗ ⌜v = #vlâŒ)%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
- iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
+ iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
- iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
iMod ("Hclose'" with "[$H↦]") as "Htok'".
@@ -346,9 +346,9 @@ Section typing.
iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
iSpecialize ("Hown" $! _ with "Htok").
iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
- - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
+ - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q''} v ∗ ⌜v = #l'âŒ)%I); try done.
iSplitL "Hown"; last by wp_read; eauto.
- iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
+ iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
- iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
iMod ("Hclose''" with "Htok") as "Htok".
@@ -358,10 +358,10 @@ Section typing.
Qed.
Definition update (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
- ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
+ ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
lft_ctx ⊢ Ï1 ν tid -∗
(∀ (l:loc) vl,
- (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗ vl ∗
+ (⌜length vl = ty.(ty_size)⌠∗ ⌜eval_expr ν = Some #l⌠∗ l ↦∗ vl ∗
∀ vl', l ↦∗ vl' ∗ â–· (ty.(ty_own) tid vl') ={E}=∗ Ï2 ν tid)
-∗ Φ #l)
-∗ WP ν @ E {{ Φ }}.
--
GitLab