diff --git a/_CoqProject b/_CoqProject
index c64653019cc75e03e59e33475feaf8b2b19c7fd0..99d284ab9a620e7face66e98e0d56c74f7b4b112 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,5 +4,25 @@ theories/lifetime/definitions.v
theories/lifetime/derived.v
theories/lifetime/creation.v
theories/lifetime/primitive.v
-theories/lifetime/todo.v
+theories/lifetime/accessors.v
theories/lifetime/borrow.v
+theories/lifetime/rebor.v
+theories/lifetime/shr_borrow.v
+theories/lifetime/frac_borrow.v
+theories/lifetime/tl_borrow.v
+theories/lang/adequacy.v
+theories/lang/derived.v
+theories/lang/heap.v
+theories/lang/lang.v
+theories/lang/lifting.v
+theories/lang/memcpy.v
+theories/lang/notation.v
+theories/lang/proofmode.v
+theories/lang/races.v
+theories/lang/tactics.v
+theories/lang/wp_tactics.v
+theories/typing/type.v
+theories/typing/type_incl.v
+theories/typing/perm.v
+theories/typing/perm_incl.v
+theories/typing/typing.v
diff --git a/iris b/iris
index 26ae0c67ca3e0dacedb957709c9526e66741e55d..42cf780adc3d61438701a106e50e07977c9b6abb 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 26ae0c67ca3e0dacedb957709c9526e66741e55d
+Subproject commit 42cf780adc3d61438701a106e50e07977c9b6abb
diff --git a/opam b/opam
new file mode 100644
index 0000000000000000000000000000000000000000..3c8ddd9c17f82f4253711864c2c990e88b2b472e
--- /dev/null
+++ b/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "coq-lambda-rust"
+version: "dev"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The RustBelt Team"
+homepage: "http://plv.mpi-sws.org/rustbelt/"
+bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
+license: "BSD"
+dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq"
+build: [
+ [make "-j%{jobs}%"]
+]
+install: [make "install"]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
+depends: [
+ "https://gitlab.mpi-sws.org/FP/iris-coq/" { (= "dev")) }
+]
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
deleted file mode 100644
index f68755d8bd070e3514cd8968297116dfc1d7c891..0000000000000000000000000000000000000000
--- a/theories/frac_borrow.v
+++ /dev/null
@@ -1,120 +0,0 @@
-From Coq Require Import Qcanon.
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac.
-From lrust Require Export lifetime shr_borrow.
-
-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.
-Notation "&frac{ κ } P" := (frac_borrow κ P)
- (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section frac_borrow.
-
- Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
-
- 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{κ}φ.
- Proof.
- 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φ").
- iApply lft_incl_refl. }
- iSplitL. by iExists 1%Qp; iFrame; auto.
- iIntros "!>H†Hφ!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
- iDestruct "Hκ" as (q'') "[_ Hκ]".
- iDestruct (lft_own_dead with "Hκ H†") as "[]".
- - iMod ("Hclose" with "*") as "Hφ"; last first.
- iExists γ, κ. iSplitR. by iApply lft_incl_refl.
- 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.
- Proof.
- 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.
- - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
- iApply fupd_intro_mask. set_solver. done.
- Qed.
-
- Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
- 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.
- 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.
- iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
- destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
- iExists qq.
- iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
- { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
- rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
- iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
- iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
- { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
- - subst. iExists qq. iIntros "{$Hκq}!%".
- by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
- - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
- rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%".
- by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
- clear Hqφ qφ qφ0. iIntros "!>Hqφ".
- iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
- iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
- { subst. iCombine "Hown" "Hownq" as "Hown".
- by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
- iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
- iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
- assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
- { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
- rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
- destruct Hval as [Hval|Hval].
- by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
- - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
- iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
- iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
- { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
- iRight. iExists _. iIntros "{$Hq'qκ}!%".
- revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
- iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame.
- - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
- { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
- iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
- Qed.
-
- Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
- Proof.
- iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
- iApply lft_incl_trans. iFrame.
- Qed.
-
- Lemma frac_borrow_incl κ κ' q:
- lft_ctx ⊢ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
- Proof.
- iIntros "#LFT#Hbor!#". iSplitR.
- - iIntros (q') "Hκ'".
- iMod (frac_borrow_acc with "LFT [] Hbor Hκ'") as (q'') "[>? Hclose]". done.
- + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto.
- + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
- - iIntros "H†'".
- iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
- iDestruct "H" as (q') "[>Hκ' _]".
- iDestruct (lft_own_dead with "Hκ' H†'") as "[]".
- Qed.
-
-End frac_borrow.
-
-Typeclasses Opaque frac_borrow.
diff --git a/theories/adequacy.v b/theories/lang/adequacy.v
similarity index 87%
rename from theories/adequacy.v
rename to theories/lang/adequacy.v
index 1cd713a040d9b4e1475939d93a4e4d112d556033..0189938398f2dbc58668dc9107b832bed0527186 100644
--- a/theories/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -1,7 +1,7 @@
From iris.program_logic Require Export hoare adequacy.
-From lrust Require Export heap.
From iris.algebra Require Import auth.
-From lrust Require Import proofmode notation.
+From lrust.lang Require Export heap.
+From lrust.lang Require Import proofmode notation.
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> irisPreG lrust_lang Σ;
@@ -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/derived.v b/theories/lang/derived.v
similarity index 75%
rename from theories/derived.v
rename to theories/lang/derived.v
index a7c7ad94ce5ee4ff8392f8947580535d00056f9d..f44b27824a057c43d5546b9334428979249a91d2 100644
--- a/theories/derived.v
+++ b/theories/lang/derived.v
@@ -1,4 +1,4 @@
-From lrust Require Export lifting.
+From lrust.lang Require Export lifting.
From iris.proofmode Require Import tactics.
Import uPred.
@@ -25,35 +25,35 @@ Lemma wp_lam E xl e e' el Φ :
Forall (λ ei, is_Some (to_val ei)) el →
Closed (xl +b+ []) e →
subst_l xl el e = Some e' →
- ▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
+ ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v →
Closed (x :b: []) e2 →
- ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
+ ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
Proof. eauto using wp_lam. Qed.
Lemma wp_seq E e1 e2 v Φ :
to_val e1 = Some v →
Closed [] e2 →
- ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
+ ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
- (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV true)) →
- (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV false)) →
- P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+ (n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
+ (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
+ P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
Qed.
Lemma wp_if E (b : bool) e1 e2 Φ :
- (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I
- ⊢ WP If (Lit b) e1 e2 @ E {{ Φ }}.
+ (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
+ WP If (Lit b) e1 e2 @ E {{ Φ }}.
Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
End derived.
diff --git a/theories/heap.v b/theories/lang/heap.v
similarity index 87%
rename from theories/heap.v
rename to theories/lang/heap.v
index 97087b8f529dd3775a849e69f5e64e1007fadafd..af3550b31a09c89ddf19e8fe9f3f539bdec8a6fc 100644
--- a/theories/heap.v
+++ b/theories/lang/heap.v
@@ -1,8 +1,8 @@
From iris.algebra Require Import cmra_big_op gmap frac dec_agree.
From iris.algebra Require Import csum excl auth.
-From iris.base_logic Require Import big_op lib.invariants.
+From iris.base_logic Require Import big_op lib.invariants lib.fractional.
From iris.proofmode Require Export tactics.
-From lrust Require Export lifting.
+From lrust.lang Require Export lifting.
Import uPred.
Definition heapN : namespace := nroot .@ "heap".
@@ -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 σ.
@@ -117,22 +118,35 @@ Section heap.
Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
+ Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+ Proof.
+ intros p q. by rewrite heap_mapsto_eq -own_op
+ -auth_frag_op op_singleton pair_op dec_agree_idemp.
+ Qed.
+ Global Instance heap_mapsto_as_fractional l q v:
+ AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+ Proof. done. Qed.
+
Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
Proof. apply _. Qed.
- Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
- Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
-
- Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
+ Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
Proof.
- by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
+ intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+ by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
Qed.
+ Global Instance heap_mapsto_vec_as_fractional l q vl:
+ AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
+ Proof. done. Qed.
+
+ Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
+ Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. 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 -(fractional (Φ := λ q, l ↦{q} _)%I) 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 /=.
@@ -158,28 +172,23 @@ Section heap.
by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
Qed.
- Lemma heap_mapsto_vec_op_eq l q1 q2 vl :
- l ↦∗{q1} vl ∗ l ↦∗{q2} vl ⊣⊢ l ↦∗{q1+q2} vl.
- Proof.
- rewrite /heap_mapsto_vec -big_sepL_sepL. by setoid_rewrite heap_mapsto_op_eq.
- Qed.
-
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.
+ - by iIntros "[% [$ Hl2]]"; subst.
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]".
@@ -187,19 +196,11 @@ Section heap.
iDestruct (Hlen with "Hown") as %?.
iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- - iIntros "Hmt". setoid_rewrite <-heap_mapsto_vec_op_eq.
- iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
+ - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
iDestruct (Hlen with "Hown") as %?.
iSplitL "Hmt1 Hown"; iExists _; by iFrame.
Qed.
- Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ l ↦{q/2} v ∗ l ↦{q/2} v.
- Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
-
- Lemma heap_mapsto_vec_op_split l q vl :
- l ↦∗{q} vl ⊣⊢ l ↦∗{q/2} vl ∗ l ↦∗{q/2} vl.
- Proof. by rewrite heap_mapsto_vec_op_eq Qp_div_2. Qed.
-
Lemma heap_mapsto_vec_combine l q vl :
vl ≠[] →
l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
@@ -209,7 +210,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 +323,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 +369,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 +377,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 +388,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 +396,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 +414,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 +429,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 +456,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 +464,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 +492,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 +507,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 +515,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 +531,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 +539,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 +547,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 +556,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 +567,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 +575,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 +585,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 +593,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/lang.v
similarity index 99%
rename from theories/lang.v
rename to theories/lang/lang.v
index 8b2f09a9dc79bf9fbb19762bbe1ec713adba7ce5..8acb16ccbf9a777126b621ea696096d1ed6c58ec 100644
--- a/theories/lang.v
+++ b/theories/lang/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/lifting.v b/theories/lang/lifting.v
similarity index 87%
rename from theories/lifting.v
rename to theories/lang/lifting.v
index 26ba40bde604251a87f843733bc2bee604c51629..a0fc74912e16d223de9c322b9aedb5fa886a60b8 100644
--- a/theories/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,7 +1,7 @@
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
-From lrust Require Export lang.
-From lrust Require Import tactics.
+From lrust.lang Require Export lang.
+From lrust.lang Require Import tactics.
From iris.proofmode Require Import tactics.
Import uPred.
Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
@@ -13,11 +13,11 @@ Implicit Types ef : option expr.
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
Lemma wp_bind {E e} K Φ :
- WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
- WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+ WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
@@ -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,11 +66,11 @@ 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 {{ Φ }}))
- ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+ WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
+ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
iIntros "HΦP". iApply (wp_lift_head_step E); auto.
iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -97,11 +97,11 @@ 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 {{ Φ }}))
- ⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+ WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
+ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
Proof.
iIntros "HΦP". iApply (wp_lift_head_step E); auto.
iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -147,8 +147,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
Forall (λ ei, is_Some (to_val ei)) el →
Closed (f :b: xl +b+ []) erec →
subst_l xl el erec = Some erec' →
- ▷ WP subst' f e erec' @ E {{ Φ }}
- ⊢ WP App e el @ E {{ Φ }}.
+ ▷ WP subst' f e erec' @ E {{ Φ }} -∗
+ WP App e el @ E {{ Φ }}.
Proof.
iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
@@ -156,7 +156,7 @@ Qed.
Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l' →
- ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+ ▷ (|={E}=> Φ (LitV l')) -∗ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto.
@@ -166,7 +166,7 @@ Qed.
Lemma wp_case E i e el Φ :
0 ≤ i →
nth_error el (Z.to_nat i) = Some e →
- ▷ WP e @ E {{ Φ }} ⊢ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
+ ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
Proof.
iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
diff --git a/theories/memcpy.v b/theories/lang/memcpy.v
similarity index 93%
rename from theories/memcpy.v
rename to theories/lang/memcpy.v
index 4fb6d9a2082cd800978fbecb70b91125c817b5c3..7c42700673bbcffe528937237f632c76f2ca6dfb 100644
--- a/theories/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,6 @@
From iris.base_logic.lib Require Import namespaces.
-From lrust Require Export notation.
-From lrust Require Import heap proofmode.
+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode.
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
@@ -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/notation.v b/theories/lang/notation.v
similarity index 98%
rename from theories/notation.v
rename to theories/lang/notation.v
index f60e5d3cb3309d12cf7cc4838d37385dd148ddb4..719f38bd50dc29696270886fe743092d877986e6 100644
--- a/theories/notation.v
+++ b/theories/lang/notation.v
@@ -1,4 +1,4 @@
-From lrust Require Export derived.
+From lrust.lang Require Export derived.
Coercion LitInt : Z >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/proofmode.v b/theories/lang/proofmode.v
similarity index 91%
rename from theories/proofmode.v
rename to theories/lang/proofmode.v
index ade46392b711c4e74f78101efd0c833e3c0d7c29..2b327fe5e2e10700b7983ced6488ac73a85caf67 100644
--- a/theories/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.base_logic Require Import namespaces.
-From lrust Require Export wp_tactics heap.
+From lrust.lang Require Export wp_tactics heap.
Import uPred.
Ltac wp_strip_later ::= iNext.
@@ -12,16 +12,8 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
-Global Instance into_and_mapsto l q v :
- IntoAnd false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoAnd heap_mapsto_op_split. Qed.
-
-Global Instance into_and_mapsto_vec l q vl :
- IntoAnd false (l ↦∗{q} vl) (l ↦∗{q/2} vl) (l ↦∗{q/2} 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 +31,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 +49,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 +68,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/races.v b/theories/lang/races.v
similarity index 99%
rename from theories/races.v
rename to theories/lang/races.v
index c7273d30e8ce9a6749e72fb08c99926b1cc3ea51..439161514d8d5d0f2a5031c2b743ab74d2b6db2a 100644
--- a/theories/races.v
+++ b/theories/lang/races.v
@@ -1,7 +1,7 @@
+From iris.prelude Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
-From lrust Require Import tactics.
-From iris.prelude Require Import gmap.
+From lrust.lang Require Import tactics.
Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
diff --git a/theories/tactics.v b/theories/lang/tactics.v
similarity index 99%
rename from theories/tactics.v
rename to theories/lang/tactics.v
index 91bdc55c60f2d6f96cbcf3cc92087bac4dc06b9c..21e3309ba8c83e4f188836669ef099d0fa920f04 100644
--- a/theories/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,5 +1,5 @@
-From lrust Require Export lang.
From iris.prelude Require Import fin_maps.
+From lrust.lang Require Export lang.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
diff --git a/theories/wp_tactics.v b/theories/lang/wp_tactics.v
similarity index 98%
rename from theories/wp_tactics.v
rename to theories/lang/wp_tactics.v
index 0775226d94c4be664d143af37e3941ff34253e64..0d136c4826ebfb35ab5c9157f5e0521b5bd3dd5d 100644
--- a/theories/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -1,4 +1,4 @@
-From lrust Require Export tactics derived.
+From lrust.lang Require Export tactics derived.
Import uPred.
(** wp-specific helper tactics *)
diff --git a/theories/lifetime/todo.v b/theories/lifetime/accessors.v
similarity index 97%
rename from theories/lifetime/todo.v
rename to theories/lifetime/accessors.v
index b04360b6ee797a87018d9999b3153b5cd8057ca0..3c74848b7921d164cd994ccc18112a09ca7ad400 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/accessors.v
@@ -1,6 +1,6 @@
From lrust.lifetime Require Export definitions.
-Section todo.
+Section accessors.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
@@ -31,4 +31,4 @@ Lemma idx_bor_atomic_acc E q κ i P :
[†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
Proof. Admitted.
-End todo.
\ No newline at end of file
+End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index b169837ac1df533ae1f2f70bf68b21d19e58a0d7..239a0e222f8a0aa2d8148db7bbd977cec0bc8efb 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export primitive creation rebor.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
@@ -17,31 +17,15 @@ Qed.
Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
Proof.
unfold bor. iIntros "#Hκκ' H". iDestruct "H" as (i) "[#? ?]".
- iExists i. iFrame. iApply lft_incl_trans. eauto.
+ iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
Qed.
Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
-Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". iApply lft_incl_trans. eauto. Qed.
-
-Lemma bor_fake_internal E κ P :
- ↑borN ⊆ E →
- ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
-Proof.
- iIntros (?) "Hdead". rewrite /lft_bor_dead.
- iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
- iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
- iMod (own_bor_update with "Hown") as "Hown".
- { apply auth_update_alloc.
- apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
- do 2 eapply lookup_to_gmap_None. by eauto. }
- rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
- iDestruct "Hown" as "[Hâ— Hâ—¯]". iSplitL "Hâ— Hbox"; last by eauto.
- iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
-Qed.
+Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'"). Qed.
Lemma bor_fake E κ P :
↑lftN ⊆ E →
- lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+ lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
Proof.
iIntros (?) "#Hmgmt H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
@@ -51,7 +35,7 @@ Proof.
?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
- iMod (bor_fake_internal with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+ iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
Qed.
@@ -120,7 +104,7 @@ Proof.
rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
- iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
- iMod (bor_fake_internal with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+ iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
Qed.
@@ -156,7 +140,7 @@ Proof.
(alloc_singleton_local_update _ γ2 (1%Qp, DecAgree Bor_in)); last done.
rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
- rewrite !own_bor_op. iDestruct "Hbor" as "[[Hâ— Hâ—¯2] Hâ—¯1]".
+ rewrite !own_bor_op. iDestruct "Hbor" as "[[Hâ— Hâ—¯2] Hâ—¯1]".
iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists (κ', γ1). iFrame "∗#". }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
@@ -169,19 +153,73 @@ Proof.
+ by rewrite -fmap_None -lookup_fmap fmap_delete.
+ by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
- iMod (bor_fake_internal with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
- iMod (bor_fake_internal with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
+ iMod (raw_bor_fake with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
+ iMod (raw_bor_fake with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iSplitL "Hbor1"; iExists (_, _); eauto.
Qed.
-
-
Lemma bor_combine E κ P Q :
↑lftN ⊆ E →
lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
-Proof. Admitted.
+Proof.
+ iIntros (?) "#Hmgmt HP HQ". rewrite {1 2}/bor.
+ iDestruct "HP" as ([κ1 i1]) "[#Hκ1 Hbor1]".
+ iDestruct "HQ" as ([κ2 i2]) "[#Hκ2 Hbor2]".
+ iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as (j1) "[Hbor1 _]".
+ done. by apply gmultiset_union_subseteq_l.
+ iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as (j2) "[Hbor2 _]".
+ done. by apply gmultiset_union_subseteq_r.
+ iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
+ iDestruct "Hbor1" as "[Hbor1 Hslice1]". iDestruct "Hbor2" as "[Hbor2 Hslice2]".
+ iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
+ rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+ /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
+ iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
+ - rewrite lft_inv_alive_unfold /lft_bor_alive.
+ iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
+ iDestruct "H" as (B) "(Hbox & >Hown & HB)".
+ iDestruct (own_bor_valid_2 with "Hown Hbor1")
+ as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
+ iDestruct (own_bor_valid_2 with "Hown Hbor2")
+ as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
+ iAssert (⌜j1 ≠j2âŒ)%I with "[#]" as %Hj1j2.
+ { iIntros (->).
+ iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
+ exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
+ compute. tauto. }
+ iMod (box_combine with "Hslice1 Hslice2 Hbox") as (γ) "(% & Hslice & Hbox)".
+ solve_ndisj. done. by rewrite lookup_fmap EQB1. by rewrite lookup_fmap EQB2.
+ iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
+ rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
+ { etrans; last etrans.
+ - apply cmra_update_op; last done.
+ apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+ - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+ - apply auth_update_alloc,
+ (alloc_singleton_local_update _ γ (1%Qp, DecAgree Bor_in)); last done.
+ rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
+ -fmap_None -lookup_fmap !fmap_delete //. }
+ rewrite own_bor_op. iDestruct "Hbor" as "[Hâ— Hâ—¯]".
+ iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
+ { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2, γ). iFrame.
+ iApply (lft_incl_glb with "Hκ1 Hκ2"). }
+ iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
+ iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
+ rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox Hâ—".
+ rewrite !big_sepM_insert /=.
+ + rewrite (big_sepM_delete _ _ _ _ EQB1) /=.
+ rewrite (big_sepM_delete _ _ j2 Bor_in) /=. by iDestruct "HB" as "[_ $]".
+ rewrite lookup_delete_ne //.
+ + rewrite -fmap_None -lookup_fmap !fmap_delete //.
+ - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+ iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+ iMod ("Hclose" with "[-Hbor]") as "_".
+ { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
+ iRight. iSplit; last by auto. iExists _. iFrame. }
+ unfold bor. iExists (_, _). iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
+Qed.
End borrow.
\ No newline at end of file
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 8ea552ffac0541f7f4b00a6f9babaa52b5f9c6da..0b9e20bff843a7af269bebc58cff24fecc067b78 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -117,7 +117,7 @@ Proof.
{ iIntros (i s HBI).
iDestruct (big_sepM_lookup _ B with "HB") as "HB"=> //.
destruct s as [|q|κ']; rewrite /bor_cnt //.
- { iDestruct (lft_tok_dead_own with "HB Hκ") as "[]". }
+ { iDestruct (lft_tok_dead with "HB Hκ") as "[]". }
iDestruct "HB" as "[% Hcnt]".
iDestruct (own_cnt_auth with "HI Hcnt") as %?.
iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index e8bc268bb0046fdcf2d7203f143380ce250516b4..8441937fb2892c5c56c9d281cf57bc453efb3b12 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -37,7 +37,7 @@ Instance lft_names_eq_dec : EqDecision lft_names.
Proof. solve_decision. Defined.
Definition alftUR := gmapUR atomic_lft lft_stateR.
-Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
+Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
Definition ilftUR := gmapUR lft (dec_agreeR lft_names).
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap DecAgree.
@@ -285,9 +285,10 @@ Proof. solve_proper. Qed.
Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
Proof. apply (ne_proper _). Qed.
-(*** PersistentP and TimelessP instances *)
+(*** PersistentP and TimelessP and instances *)
Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
Proof. rewrite /lft_tok. apply _. Qed.
+
Global Instance lft_dead_persistent κ : PersistentP [†κ].
Proof. rewrite /lft_dead. apply _. Qed.
Global Instance lft_dead_timeless κ : PersistentP [†κ].
@@ -298,7 +299,7 @@ Proof. rewrite /lft_incl. apply _. Qed.
Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
Proof. rewrite /idx_bor. apply _. Qed.
-Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
+Global Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
Proof. rewrite /idx_bor_own. apply _. Qed.
Global Instance lft_ctx_persistent : PersistentP lft_ctx.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 689aa4eeb57db243d7d9e338ae266eb16edf48cf..263a0af2d56d69a4f14e71e580b22201d4d61221 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive borrow todo.
+From lrust.lifetime Require Export primitive borrow accessors rebor.
From iris.proofmode Require Import tactics.
Section derived.
@@ -8,7 +8,7 @@ Implicit Types κ : lft.
(*** Derived lemmas *)
Lemma bor_acc E q κ P :
↑lftN ⊆ E →
- lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+ lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
Proof.
iIntros (?) "#LFT HP Htok".
iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
@@ -17,7 +17,7 @@ Qed.
Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
↑lftN ⊆ E →
- lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+ lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H†Hclose]]"; first done.
@@ -28,15 +28,15 @@ Qed.
Lemma bor_or E κ P Q :
↑lftN ⊆ E →
- lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+ lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
Proof.
iIntros (?) "#LFT H". rewrite uPred.or_alt.
iMod (bor_exists with "LFT H") as ([]) "H"; auto.
Qed.
-Lemma bor_persistent `{!PersistentP P} E κ q :
+Lemma bor_persistent P `{!PersistentP P} E κ q :
↑lftN ⊆ E →
- lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+ lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
Proof.
iIntros (?) "#LFT Hb Htok".
iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
@@ -45,7 +45,7 @@ Qed.
Lemma lft_incl_acc E κ κ' q :
↑lftN ⊆ E →
- κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+ κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Proof.
rewrite /lft_incl.
iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
@@ -53,44 +53,17 @@ Proof.
iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
Qed.
-Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
Proof.
rewrite /lft_incl.
iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
Qed.
-Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ∪ κ''.
-Proof. (*
- iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
- - iIntros (q) "[Hκ'1 Hκ'2]".
- iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
- iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
- destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
- iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
- iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
- iIntros "!>[Hκ'0 Hκ''0]".
- iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
- by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
- - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
-Qed. *) Admitted.
-
-Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
+Lemma lft_incl_static κ : (κ ⊑ static)%I.
Proof.
iIntros "!#". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
-Lemma reborrow E P κ κ' :
- ↑lftN ⊆ E →
- lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-Proof.
- iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' 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.
-Qed.
-*)
-Admitted.
End derived.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..ea78aee6e7e0203e22b7ec9db6ea273f65f1fa3c
--- /dev/null
+++ b/theories/lifetime/frac_borrow.v
@@ -0,0 +1,129 @@
+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import lib.fractional.
+From iris.algebra Require Import frac.
+From lrust.lifetime Require Export shr_borrow .
+
+Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
+
+Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ) :=
+ (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
+ (⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ']))%I.
+Notation "&frac{ κ } P" := (frac_bor κ P)
+ (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
+
+Section frac_bor.
+ Context `{invG Σ, lftG Σ, frac_borG Σ}.
+ Implicit Types E : coPset.
+
+ Global Instance frac_bor_proper :
+ Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
+ Proof. solve_proper. Qed.
+ Global Instance frac_bor_persistent : PersistentP (&frac{κ}Φ) := _.
+
+ Lemma bor_fracture φ E κ :
+ ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+ Proof.
+ iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+ iMod (bor_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H†Hclose]]". done.
+ - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
+ { iExists γ, κ. iSplitR; last by iApply (bor_share with "Hφ").
+ iApply lft_incl_refl. }
+ iSplitL. by iExists 1%Qp; iFrame; auto.
+ iIntros "!>H†HΦ!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
+ iDestruct "Hκ" as (q'') "[_ Hκ]".
+ iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+ - iMod ("Hclose" with "*") as "HΦ"; last first.
+ iExists γ, κ. iSplitR. by iApply lft_incl_refl.
+ iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
+ Qed.
+
+ Lemma frac_bor_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]".
+ iMod (shr_bor_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.
+ - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
+ iApply fupd_intro_mask. set_solver. done.
+ Qed.
+
+ Lemma frac_bor_acc_strong 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_bor.
+ iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
+ iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
+ iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
+ iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
+ destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
+ iExists qq.
+ iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
+ { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
+ rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
+ iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
+ iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
+ { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
+ - subst. iExists qq. iIntros "{$Hκq}!%".
+ by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
+ - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
+ iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
+ clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
+ iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
+ iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
+ { subst. iCombine "Hown" "Hownq" as "Hown".
+ by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
+ iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
+ iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
+ assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
+ { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
+ rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
+ destruct Hval as [Hval|Hval].
+ by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
+ - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
+ iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
+ iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
+ { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
+ iRight. iExists _. iIntros "{$Hq'qκ}!%".
+ revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
+ iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+ - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
+ { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
+ iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+ Qed.
+
+ Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+ Proof.
+ iIntros (?) "LFT". iApply (frac_bor_acc_strong with "LFT"). done.
+ iIntros "!#*". rewrite fractional. iSplit; auto.
+ Qed.
+
+ Lemma frac_bor_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
+ Proof.
+ iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
+ iApply (lft_incl_trans with "Hκκ' []"). auto.
+ Qed.
+
+ Lemma frac_bor_incl κ κ' q:
+ lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
+ Proof.
+ iIntros "#LFT#Hbor!#". iSplitR.
+ - iIntros (q') "Hκ'".
+ iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+ iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
+ - iIntros "H†'".
+ iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+ iDestruct "H" as (q') "[>Hκ' _]".
+ iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
+ Qed.
+
+End frac_bor.
+
+Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 6d83a7ae491dba69c9d04179671762d52dfae5da..33e0e6f32377393a4b3c749ff405036ae802b817 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -1,7 +1,7 @@
From lrust.lifetime Require Export definitions.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes.
+From iris.base_logic.lib Require Import boxes fractional.
From iris.proofmode Require Import tactics.
Import uPred.
@@ -19,7 +19,7 @@ Qed.
(** Ownership *)
Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
- own_ilft_auth I ⊢
+ own_ilft_auth I -∗
own ilft_name (â—¯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)âŒ.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
@@ -28,7 +28,7 @@ Proof.
Qed.
Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
- own_alft_auth A ⊢
+ own_alft_auth A -∗
own alft_name (â—¯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some bâŒ.
Proof.
iIntros "HA HΛ".
@@ -38,7 +38,7 @@ Proof.
move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
Qed.
-Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)âŒ.
+Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜is_Some (I !! κ)âŒ.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
@@ -53,9 +53,9 @@ Proof.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
-Lemma own_bor_valid κ x : own_bor κ x ⊢ ✓ x.
+Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_bor_valid_2 κ x y : own_bor κ x ⊢ own_bor κ y -∗ ✓ (x ⋅ y).
+Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
Proof.
@@ -67,7 +67,7 @@ Proof.
intros. apply wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
Qed.
-Lemma own_cnt_auth I κ x : own_ilft_auth I ⊢ own_cnt κ x -∗ ⌜is_Some (I !! κ)âŒ.
+Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜is_Some (I !! κ)âŒ.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
@@ -82,21 +82,21 @@ Proof.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
-Lemma own_cnt_valid κ x : own_cnt κ x ⊢ ✓ x.
+Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_cnt_valid_2 κ x y : own_cnt κ x ⊢ own_cnt κ y -∗ ✓ (x ⋅ y).
+Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
Qed.
Lemma own_cnt_update_2 κ x1 x2 y :
- x1 ⋅ x2 ~~> y → own_cnt κ x1 ⊢ own_cnt κ x2 ==∗ own_cnt κ y.
+ x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
Proof.
intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
Qed.
-Lemma own_inh_auth I κ x : own_ilft_auth I ⊢ own_inh κ x -∗ ⌜is_Some (I !! κ)âŒ.
+Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜is_Some (I !! κ)âŒ.
Proof.
iIntros "HI"; iDestruct 1 as (γs) "[? _]".
by iApply (own_ilft_auth_agree with "HI").
@@ -111,9 +111,9 @@ Proof.
move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
-Lemma own_inh_valid κ x : own_inh κ x ⊢ ✓ x.
+Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
-Lemma own_inh_valid_2 κ x y : own_inh κ x ⊢ own_inh κ y -∗ ✓ (x ⋅ y).
+Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
Proof.
@@ -188,7 +188,7 @@ Qed.
Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof. exists Λ. by rewrite lookup_insert. Qed.
-Lemma lft_inv_alive_twice κ : lft_inv_alive κ ⊢ lft_inv_alive κ -∗ False.
+Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
Proof.
rewrite lft_inv_alive_unfold /lft_inh.
iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
@@ -217,16 +217,7 @@ Proof.
rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
Qed.
-Lemma lft_tok_frac_op κ q q' : (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
-Proof.
- rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper=> Λ _.
- by rewrite -own_op -auth_frag_op op_singleton.
-Qed.
-
-Lemma lft_tok_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
-Proof. by rewrite -lft_tok_frac_op Qp_div_2. Qed.
-
-Lemma lft_tok_dead_own q κ : q.[κ] ⊢ [†κ] -∗ False.
+Lemma lft_tok_dead q κ : q.[κ] -∗ [†κ] -∗ False.
Proof.
rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
@@ -234,14 +225,32 @@ Proof.
move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
Qed.
-Lemma lft_tok_static q : True ⊢ q.[static].
+Lemma lft_tok_static q : q.[static]%I.
Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
-Lemma lft_dead_static : [†static] ⊢ False.
+Lemma lft_dead_static : [†static] -∗ False.
Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
+(* Fractional and AsFractional instances *)
+Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+Proof.
+ intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
+ intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
+Qed.
+Global Instance lft_tok_as_fractional κ q :
+ AsFractional q.[κ] (λ q, q.[κ])%I q.
+Proof. done. Qed.
+Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+Proof.
+ intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
+ by rewrite -auth_frag_op op_singleton.
+Qed.
+Global Instance idx_bor_own_as_fractional i q :
+ AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+Proof. done. Qed.
+
(** Lifetime inclusion *)
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
+Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
Proof.
iIntros (->%gmultiset_union_difference) "!#". iSplitR.
- iIntros (q). rewrite <-lft_tok_op. iIntros "[H Hf]". iExists q. iFrame.
@@ -249,12 +258,12 @@ Proof.
- iIntros "? !>". iApply lft_dead_or. auto.
Qed.
-Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
+Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
Proof. by apply lft_le_incl. Qed.
-Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
+Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
- rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
+ rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
- iIntros (q) "Hκ".
iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
@@ -263,4 +272,19 @@ Proof.
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Proof.
+ unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
+ - iIntros (q) "[Hκ'1 Hκ'2]".
+ iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
+ iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
+ destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
+ iExists qq. rewrite -lft_tok_op.
+ iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
+ iIntros "!>[Hκ'0 Hκ''0]".
+ iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+ iApply "Hclose''". iFrame.
+ - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
+Qed.
+
End primitive.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 5311c81dd034041899bd594dcb488e3c14295b0b..91b9e902ab39a94ab521bcc6dda6826491b14167 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive (* borrow *).
+From lrust.lifetime Require Export primitive.
From iris.algebra Require Import csum auth frac gmap dec_agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
@@ -8,6 +8,22 @@ Section rebor.
Context `{invG Σ, lftG Σ}.
Implicit Types κ : lft.
+Lemma raw_bor_fake E κ P :
+ ↑borN ⊆ E →
+ ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
+Proof.
+ iIntros (?) "Hdead". rewrite /lft_bor_dead.
+ iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
+ iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+ iMod (own_bor_update with "Hown") as "Hown".
+ { apply auth_update_alloc.
+ apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
+ do 2 eapply lookup_to_gmap_None. by eauto. }
+ rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
+ iDestruct "Hown" as "[Hâ— Hâ—¯]". iSplitL "Hâ— Hbox"; last by eauto.
+ iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
+Qed.
+
Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
let Iinv := (
own_ilft_auth I ∗
@@ -111,12 +127,33 @@ admit.
Admitted.
+
+Lemma raw_rebor E κ κ' i P :
+ ↑lftN ⊆ E → κ ⊆ κ' →
+ lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
+ ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+Admitted.
+
Lemma bor_rebor' E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
- lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
+ lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
Proof. Admitted.
+Lemma rebor E P κ κ' :
+ ↑lftN ⊆ E →
+ lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+Proof.
+ iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' 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.
+Qed.
+*)
+Admitted.
+
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
- lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
+ lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
Proof. Admitted.
+
End rebor.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..2db70d36bb3c96688f0741845acef3352b6a6db4
--- /dev/null
+++ b/theories/lifetime/shr_borrow.v
@@ -0,0 +1,56 @@
+From iris.algebra Require Import gmap auth frac.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Export derived.
+
+(** Shared bors *)
+Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
+ (∃ i, idx_bor κ i P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
+Notation "&shr{ κ } P" := (shr_bor κ P)
+ (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
+
+Section shared_bors.
+ Context `{invG Σ, lftG Σ} (P : iProp Σ).
+
+ Global Instance shr_bor_proper :
+ Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
+ Proof. solve_proper. Qed.
+ Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
+
+ Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
+ Proof.
+ iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+ iExists i. iFrame "#". iApply inv_alloc. auto.
+ Qed.
+
+ Lemma shr_bor_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)".
+ iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
+ iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
+ iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]". done.
+ - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+ - iRight. iFrame. iIntros "!>". by iMod "Hclose".
+ Qed.
+
+ Lemma shr_bor_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κ".
+ iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H†_]]". done.
+ - iIntros "!>HP". by iMod ("Hclose" with "HP").
+ - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+ Qed.
+
+ Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
+ Proof.
+ iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+ by iApply (idx_bor_shorten with "H⊑").
+ Qed.
+
+End shared_bors.
+
+Typeclasses Opaque shr_bor.
diff --git a/theories/lifetime/tl_borrow.v b/theories/lifetime/tl_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..34d7314179d88a8ae4e0afdde5ce184390f4b439
--- /dev/null
+++ b/theories/lifetime/tl_borrow.v
@@ -0,0 +1,51 @@
+From lrust.lifetime Require Export derived.
+From iris.base_logic.lib Require Export thread_local.
+From iris.proofmode Require Import tactics.
+
+Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
+ (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
+ (∃ i, idx_bor κ i P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
+
+Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
+ (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+
+Section tl_bor.
+ Context `{invG Σ, lftG Σ, thread_localG Σ}
+ (tid : thread_id) (N : namespace) (P : iProp Σ).
+
+ Global Instance tl_bor_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
+ Global Instance tl_bor_proper κ :
+ Proper ((⊣⊢) ==> (⊣⊢)) (tl_bor κ tid N).
+ Proof.
+ intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
+ Qed.
+
+ Lemma bor_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ,tid,N}P.
+ Proof.
+ iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "[#? Hown]".
+ iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
+ Qed.
+
+ Lemma tl_bor_acc q κ E 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).
+ Proof.
+ iIntros (???) "#LFT#HP Hκ Htlown".
+ iDestruct "HP" as (i) "(#Hpers&#Hinv)".
+ iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
+ iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+ iIntros "{$HP $Htlown}!>HP Htlown".
+ iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
+ Qed.
+
+ Lemma tl_bor_shorten κ κ': κ ⊑ κ' -∗ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
+ Proof.
+ iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+ iApply (idx_bor_shorten with "Hκκ' H").
+ Qed.
+
+End tl_bor.
+
+Typeclasses Opaque tl_bor.
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
deleted file mode 100644
index 65714ea6a06397e9faf6d4776af86ed8627f722f..0000000000000000000000000000000000000000
--- a/theories/shr_borrow.v
+++ /dev/null
@@ -1,55 +0,0 @@
-From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
-From lrust Require Export lifetime.
-
-(** Shared borrows *)
-Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) :=
- (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I.
-Notation "&shr{ κ } P" := (shr_borrow κ P)
- (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section shared_borrows.
- Context `{invG Σ, lifetimeG Σ} (P : iProp Σ).
-
- Global Instance shr_borrow_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
- Proof. solve_proper. Qed.
- Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
-
- Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
- Proof.
- 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.
- Proof.
- 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.
- iMod (idx_borrow_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]". done.
- - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
- - 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.[κ]).
- Proof.
- 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 "[]".
- Qed.
-
- Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
- Proof.
- iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
- by iApply (idx_borrow_shorten with "H⊑").
- Qed.
-
-End shared_borrows.
-
-Typeclasses Opaque shr_borrow.
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
deleted file mode 100644
index 6cfa358b330c64c7c491a038ba20b09f7a5cfd39..0000000000000000000000000000000000000000
--- a/theories/tl_borrow.v
+++ /dev/null
@@ -1,51 +0,0 @@
-From lrust Require Export lifetime.
-From iris.base_logic.lib Require Export thread_local.
-From iris.proofmode Require Import tactics.
-
-Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
- (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
- (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
-
-Notation "&tl{ κ , tid , N } P" := (tl_borrow κ tid N P)
- (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
-
-Section tl_borrow.
- Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
- (tid : thread_id) (N : namespace) (P : iProp Σ).
-
- Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
- Global Instance tl_borrow_proper κ :
- Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
- Proof.
- 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.
- Proof.
- 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 →
- 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).
- Proof.
- iIntros (???) "#LFT#HP Hκ Htlown".
- iDestruct "HP" as (i) "(#Hpers&#Hinv)".
- iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
- iMod (idx_borrow_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
- iIntros "{$HP $Htlown}!>HP Htlown".
- iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
- Qed.
-
- Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
- Proof.
- iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
- iApply (idx_borrow_shorten with "Hκκ' H").
- Qed.
-
-End tl_borrow.
-
-Typeclasses Opaque tl_borrow.
diff --git a/theories/perm.v b/theories/typing/perm.v
similarity index 79%
rename from theories/perm.v
rename to theories/typing/perm.v
index fbe763f4eddc1fbc07f8b492dcce6365ae5c91e6..7e88e51a27fd4afcc50f1b6ff08bf6cbfb6e83e9 100644
--- a/theories/perm.v
+++ b/theories/typing/perm.v
@@ -1,5 +1,7 @@
From iris.proofmode Require Import tactics.
-From lrust Require Export type proofmode.
+From lrust.typing Require Export type.
+From lrust.lang Require Export proofmode.
+From lrust.lifetime Require Import frac_borrow.
Delimit Scope perm_scope with P.
Bind Scope perm_scope with perm.
@@ -23,17 +25,17 @@ Section perm.
Definition has_type (ν : expr) (ty : type) : perm := λ tid,
from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
- Definition extract (κ : lifetime) (Ï : perm) : perm :=
- λ tid, ([†κ] ={lftN}=∗ Ï tid)%I.
+ Definition extract (κ : lft) (Ï : perm) : perm :=
+ λ tid, ([†κ] ={↑lftN}=∗ Ï tid)%I.
- Definition tok (κ : lifetime) (q : Qp) : perm :=
+ Definition tok (κ : lft) (q : Qp) : perm :=
λ _, q.[κ]%I.
- Definition killable (κ : lifetime) : perm :=
- λ _, (□ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]))%I.
+ Definition killable (κ : lft) : perm :=
+ λ _, (□ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]))%I.
- Definition incl (κ κ' : lifetime) : perm :=
+ Definition incl (κ κ' : lft) : perm :=
λ _, (κ ⊑ κ')%I.
Definition exist {A : Type} (P : A -> perm) : @perm Σ :=
@@ -61,7 +63,7 @@ Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope
Notation "†κ" := (killable κ) (format "†κ", at level 75).
-Infix "⊑" := incl (at level 60) : perm_scope.
+Infix "⊑" := incl (at level 70) : perm_scope.
Notation "∃ x .. y , P" :=
(exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
@@ -105,12 +107,13 @@ 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)
- ⊢ WP ν @ E {{ Φ }}.
+ (ν ◠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.
+ iIntros "H◠HΦ". setoid_rewrite has_type_value. unfold has_type.
destruct (eval_expr ν) eqn:EQν; last by iDestruct "Hâ—" as "[]". simpl.
- iMod ("HΦ" $! v with "[$Hâ—]") as "HΦ". done.
+ iMod ("HΦ" $! v with "[] Hâ—") as "HΦ". done.
iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
forall (Φ v EQν); try done.
- inversion EQν. subst. wp_value. auto.
diff --git a/theories/perm_incl.v b/theories/typing/perm_incl.v
similarity index 88%
rename from theories/perm_incl.v
rename to theories/typing/perm_incl.v
index 4d646f391561e4efcc01630bd7c6b9de769e1b76..8791ec050e943875fbfa01102529372ddd6f6d37 100644
--- a/theories/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -1,6 +1,7 @@
From Coq Require Import Qcanon.
From iris.base_logic Require Import big_op.
-From lrust Require Export type perm.
+From lrust.typing Require Export type perm.
+From lrust.lifetime Require Import frac_borrow.
Import Perm Types.
@@ -10,13 +11,13 @@ Section defs.
(* Definitions *)
Definition perm_incl (Ï1 Ï2 : perm) :=
- ∀ tid, lft_ctx ⊢ Ï1 tid ={⊤}=∗ Ï2 tid.
+ ∀ tid, lft_ctx -∗ Ï1 tid ={⊤}=∗ Ï2 tid.
Global Instance perm_equiv : Equiv perm :=
λ Ï1 Ï2, perm_incl Ï1 Ï2 ∧ perm_incl Ï2 Ï1.
Definition borrowing κ (Ï Ï1 Ï2 : perm) :=
- ∀ tid, lft_ctx ⊢ Ï tid -∗ Ï1 tid ={⊤}=∗ Ï2 tid ∗ (κ ∋ Ï1)%P tid.
+ ∀ tid, lft_ctx -∗ Ï tid -∗ Ï1 tid ={⊤}=∗ Ï2 tid ∗ (κ ∋ Ï1)%P tid.
End defs.
@@ -93,15 +94,13 @@ Section props.
Lemma perm_tok_plus κ q1 q2 :
tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
- Proof.
- rewrite /tok /sep /=; split; iIntros (tid) "_ ?"; rewrite lft_own_frac_op //.
- Qed.
+ Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
- Proof. iIntros (tid) "_ [#?#?]!>". iApply lft_incl_trans. auto. Qed.
+ Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
Lemma perm_incl_share q ν κ ty :
ν ◠&uniq{κ} ty ∗ q.[κ] ⇒ ν ◠&shr{κ} ty ∗ q.[κ].
@@ -125,7 +124,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 +135,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.
@@ -193,7 +192,7 @@ Section props.
* etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
Qed.
- Lemma perm_split_uniq_borrow_prod2 ty1 ty2 κ ν :
+ Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
ν ◠&uniq{κ} (product2 ty1 ty2) ⇒
ν ◠&uniq{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◠&uniq{κ} ty2.
Proof.
@@ -201,11 +200,11 @@ Section props.
destruct (eval_expr ν) as [[[|l|]|]|];
iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-].
- rewrite /= split_prod_mt. iMod (borrow_split with "LFT H") as "[H1 H2]".
+ rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
set_solver. iSplitL "H1"; eauto.
Qed.
- Lemma perm_split_uniq_borrow_prod tyl κ ν :
+ Lemma perm_split_uniq_bor_prod tyl κ ν :
ν ◠&uniq{κ} (Πtyl) ⇒
foldr (λ tyoffs acc,
ν +ₗ #(tyoffs.2:nat) ◠&uniq{κ} (tyoffs.1) ∗ acc)%P
@@ -216,12 +215,12 @@ Section props.
iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
rewrite shift_loc_0 /=. eauto. }
generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
- etransitivity. apply perm_split_uniq_borrow_prod2.
+ etransitivity. apply perm_split_uniq_bor_prod2.
iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
Qed.
- Lemma perm_split_shr_borrow_prod2 ty1 ty2 κ ν :
+ Lemma perm_split_shr_bor_prod2 ty1 ty2 κ ν :
ν ◠&shr{κ} (product2 ty1 ty2) ⇒
ν ◠&shr{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◠&shr{κ} ty2.
Proof.
@@ -235,7 +234,7 @@ Section props.
set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl.
Qed.
- Lemma perm_split_shr_borrow_prod tyl κ ν :
+ Lemma perm_split_shr_bor_prod tyl κ ν :
ν ◠&shr{κ} (Πtyl) ⇒
foldr (λ tyoffs acc,
(ν +ₗ #(tyoffs.2:nat))%E ◠&shr{κ} (tyoffs.1) ∗ acc)%P
@@ -246,12 +245,12 @@ Section props.
iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". }
generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
- etransitivity. apply perm_split_shr_borrow_prod2.
+ etransitivity. apply perm_split_shr_bor_prod2.
iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
Qed.
- Lemma reborrow_shr_perm_incl κ κ' ν ty :
+ Lemma rebor_shr_perm_incl κ κ' ν ty :
κ ⊑ κ' ∗ ν ◠&shr{κ'}ty ⇒ ν ◠&shr{κ}ty.
Proof.
iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
@@ -275,35 +274,35 @@ 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.
- iMod (borrow_create with "LFT Hown") as "[Hbor Hext]". done.
+ iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
iSplitL "Hbor". by simpl; eauto.
- iMod (borrow_create with "LFT Hf") as "[_ Hf]". done.
+ iMod (bor_create with "LFT Hf") as "[_ Hf]". done.
iIntros "!>#H†".
iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
iExists _. iFrame. auto.
Qed.
- Lemma reborrow_uniq_borrowing κ κ' ν ty :
+ Lemma rebor_uniq_borrowing κ κ' ν ty :
borrowing κ (κ ⊑ κ') (ν ◠&uniq{κ'}ty) (ν ◠&uniq{κ}ty).
Proof.
iIntros (tid) "#LFT #Hord H". unfold has_type.
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.
- iMod (reborrow with "LFT Hord H") as "[H Hextr]". done.
+ iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
iModIntro. iSplitL "H". iExists _. by eauto.
iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
Qed.
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.
- iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
+ iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
+ iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
+ iMod (bor_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").
+ iSplitL "Hbor". iApply (frac_bor_incl with "LFT Hbor").
iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
Qed.
diff --git a/theories/type.v b/theories/typing/type.v
similarity index 71%
rename from theories/type.v
rename to theories/typing/type.v
index ebc124bc32a755adcd645aa66ae94439131b6e1d..2f7e5ea823c90f662aa99389cc3241c7f159185b 100644
--- a/theories/type.v
+++ b/theories/typing/type.v
@@ -2,16 +2,17 @@ From Coq Require Import Qcanon.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Export thread_local.
From iris.program_logic Require Import hoare.
-From lrust Require Export notation lifetime frac_borrow heap.
+From lrust.lang Require Export heap notation.
+From lrust.lifetime Require Import frac_borrow.
Class iris_typeG Σ := Iris_typeG {
type_heapG :> heapG Σ;
- type_lifetimeG :> lifetimeG Σ;
+ type_lftG :> lftG Σ;
type_thread_localG :> thread_localG Σ;
- type_frac_borrowG Σ :> frac_borrowG Σ
+ type_frac_borrowG Σ :> frac_borG Σ
}.
-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] *)
@@ -25,12 +26,12 @@ Record type :=
{ ty_size : nat;
ty_dup : bool;
ty_own : thread_id → list val → iProp Σ;
- ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
+ ty_shr : lft → thread_id → coPset → loc → iProp Σ;
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,13 +41,13 @@ 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;
+ lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
ty_shr_acc κ tid E F l q :
ty_dup → mgmtE ∪ F ⊆ E →
- lft_ctx ⊢ ty_shr κ tid F l -∗
+ lft_ctx -∗ ty_shr κ tid F l -∗
q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
(▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
}.
@@ -59,7 +60,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.
@@ -76,35 +77,31 @@ Program Coercion ty_of_st (st : simple_type) : type :=
Next Obligation. intros. apply st_size_eq. Qed.
Next Obligation.
intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
- iMod (borrow_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
- iMod (borrow_split with "LFT Hmt") as "[Hmt Hown]". set_solver.
- iMod (borrow_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
- iMod (borrow_fracture with "LFT [Hmt]") as "Hfrac"; last first.
+ iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
+ iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
+ iMod (bor_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
+ iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
{ iExists vl. by iFrame. }
done. set_solver.
Qed.
Next Obligation.
intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
iDestruct "H" as (vl) "[Hf Hown]".
- iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
+ iExists vl. iFrame. by iApply (frac_bor_shorten with "Hord").
Qed.
Next Obligation.
intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
iDestruct "Hshr" as (vl) "[Hf Hown]".
- iMod (frac_borrow_acc with "LFT [] Hf Hlft") as (q') "[Hmt Hclose]";
- first set_solver.
- - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
- iSplit; auto.
- - iModIntro. rewrite {1}heap_mapsto_vec_op_split. iExists _.
- 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 ">%".
- { 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.
- iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+ iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+ iModIntro. iExists _. 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 ">%".
+ { 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.
+ iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
End type.
@@ -129,23 +126,23 @@ Section types.
Next Obligation. iIntros (tid vl) "[]". Qed.
Next Obligation.
iIntros (????????) "#LFT Hb Htok".
- iMod (borrow_exists with "LFT Hb") as (vl) "Hb". set_solver.
- iMod (borrow_split with "LFT Hb") as "[_ Hb]". set_solver.
- iMod (borrow_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". set_solver.
+ iMod (bor_sep with "LFT Hb") as "[_ Hb]". set_solver.
+ iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
Qed.
Next Obligation. intros. iIntros "_ _ []". Qed.
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 +154,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
@@ -168,24 +165,24 @@ Section types.
Qed.
Next Obligation.
move=> q ty E N κ l tid q' ?? /=. iIntros "#LFT Hshr Htok".
- iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
- iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
- iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
- iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
+ iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+ iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+ iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+ iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
+ iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
rewrite heap_mapsto_vec_singleton.
- 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 (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
+ iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
+ rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
+ iMod (inv_alloc N _ (idx_bor_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. }
- iMod (borrow_acc_strong with "LFT Hb Htok") as "[Hown Hclose']". set_solver.
+ { rewrite bor_unfold_idx. iExists i. eauto. }
+ iMod (bor_acc_strong with "LFT Hb Htok") as "[Hown Hclose']". set_solver.
iIntros "!>". iNext.
iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>?$".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
@@ -195,7 +192,7 @@ Section types.
Next Obligation.
intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]".
- iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
+ iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros (q') "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
@@ -206,14 +203,14 @@ Section types.
Qed.
Next Obligation. done. Qed.
- Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
+ Program Definition uniq_bor (κ:lft) (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'.[κ ⋅ κ']
- ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
+ ∀ q', □ (q'.[κ∪κ']
+ ={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ']))%I
|}.
Next Obligation. done. Qed.
Next Obligation.
@@ -221,36 +218,39 @@ Section types.
Qed.
Next Obligation.
move=> κ ty E N κ' l tid q' ??/=. iIntros "#LFT Hshr Htok".
- iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
- iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
- iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
- iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
- iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
+ iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+ iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+ iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+ iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
+ iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
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 (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
+ rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
+ iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
+ iApply (step_fupd_mask_mono (mgmtE ∪ ↑N) _ _ ((mgmtE ∪ ↑N) ∖ ↑N ∖ ↑lftN)).
+ { assert (nclose lftN ⊥ ↑tlN) by solve_ndisj. set_solver. } set_solver.
iMod (inv_open with "Hinv") as "[INV Hclose]". 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. }
- iMod (borrow_unnest with "LFT Hb") as "Hb". set_solver.
+ { rewrite (bor_unfold_idx κ'). eauto. }
+ iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
iIntros "!>". iNext. iMod "Hb".
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
- - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+ - iMod (step_fupd_mask_mono _ _ _ _ True%I with "[]") as "Hclose'"; last first.
+ iIntros "!>". iNext. iMod "Hclose'" as "_".
+ iMod ("Hclose" with "[]") as "_"; by eauto. eauto. done. set_solver.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
- iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
- { iApply lft_incl_lb. iSplit.
- - iApply lft_le_incl. by exists κ'.
- - iApply lft_incl_trans. iSplit; last done.
- iApply lft_le_incl. exists κ0. apply (comm _). }
- iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
+ iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
+ { iApply (lft_incl_glb with "[] []").
+ - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
+ - iApply (lft_incl_trans with "[] Hκ").
+ iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+ iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
iMod ("Hvs" $! q' with "Htok") as "Hclose'". iIntros "!>". iNext.
@@ -259,17 +259,17 @@ Section types.
Qed.
Next Obligation. done. Qed.
- Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
+ Program Definition shared_bor (κ : lft) (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.
@@ -301,10 +301,10 @@ Section types.
Next Obligation.
intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
rewrite split_prod_mt.
- iMod (borrow_split with "LFT H") as "[H1 H2]". set_solver.
+ iMod (bor_sep 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.
@@ -325,19 +325,19 @@ Section types.
iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
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 ">%".
+ rewrite !split_prod_mt.
+ 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
@@ -397,36 +397,32 @@ Section types.
Qed.
Next Obligation.
intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
- iMod (borrow_exists with "LFT Hown") as (i) "Hown". set_solver.
- iMod (borrow_split with "LFT Hown") as "[Hmt Hown]". set_solver.
+ iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
+ iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
iMod ((nth i tyl emp).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
- iMod (borrow_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
+ iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
Qed.
Next Obligation.
intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
- by iApply (frac_borrow_shorten with "Hord").
+ by iApply (frac_bor_shorten with "Hord").
iApply ((nth i tyl emp).(ty_shr_mono) with "LFT Hord"); last done. done.
Qed.
Next Obligation.
intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
iIntros "#LFT #H[[Htok1 Htok2] Htl]".
setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
- iMod (frac_borrow_acc with "LFT [] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
+ iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
as (q'2) "[Hownq Hclose']"; try done.
{ edestruct nth_in_or_default as [| ->]; last done.
rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
- iExists q'. iModIntro.
- rewrite -{1}heap_mapsto_op_eq -{1}heap_mapsto_vec_prop_op;
- last (by intros; apply sum_size_eq, Hn).
+ rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
- iSplitL "Hown1 Hownq1".
+ iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
- iNext. iExists i. by iFrame.
- iIntros "H". iDestruct "H" as (i') "[Hown1 Hownq1]".
- rewrite (lft_own_split _ q).
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
iMod ("Hclose" with "Hown") as "$".
@@ -436,12 +432,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 +455,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.
@@ -476,9 +472,9 @@ Hint Extern 1 (Types.LstTySize _ (_ :: _)) =>
Import Types.
Notation "∅" := emp : lrust_type_scope.
-Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
+Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
(format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
-Notation "&shr{ κ } ty" := (shared_borrow κ ty)
+Notation "&shr{ κ } ty" := (shared_bor κ ty)
(format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
Arguments product : simpl never.
diff --git a/theories/type_incl.v b/theories/typing/type_incl.v
similarity index 91%
rename from theories/type_incl.v
rename to theories/typing/type_incl.v
index e2fdf2af343a3a10518f9cf01a6549e7fff5dcc5..060c52bcf09c573e1b50de35b55813966f0afa5d 100644
--- a/theories/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,6 +1,7 @@
From iris.base_logic Require Import big_op.
From iris.program_logic Require Import hoare.
-From lrust Require Export type perm_incl.
+From lrust.typing Require Export type perm_incl.
+From lrust.lifetime Require Import frac_borrow.
Import Types.
@@ -9,17 +10,17 @@ Section ty_incl.
Context `{iris_typeG Σ}.
Definition ty_incl (Ï : perm) (ty1 ty2 : type) :=
- ∀ tid, lft_ctx ⊢ Ï tid ={⊤}=∗
+ ∀ tid, lft_ctx -∗ Ï tid ={⊤}=∗
(□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
(□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
(* [ty_incl] needs to prove something about the length of the
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.
+ Proof. iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto. Qed.
Lemma ty_incl_trans Ï Î¸ ty1 ty2 ty3 :
ty_incl Ï ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (Ï âˆ— θ) ty1 ty3.
@@ -68,17 +69,17 @@ Section ty_incl.
by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
Qed.
- Lemma lft_incl_ty_incl_uniq_borrow ty κ1 κ2 :
+ Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
Proof.
iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
- iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
- by iApply (borrow_shorten with "Hincl").
- - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
- { iApply lft_incl_lb. iSplit.
- - iApply lft_incl_trans. iSplit; last done.
- iApply lft_le_incl. by exists κ.
- - iApply lft_le_incl. exists κ1. by apply (comm _). }
+ by iApply (bor_shorten with "Hincl").
+ - iAssert (κ1 ∪ κ ⊑ κ2 ∪ κ)%I as "#Hincl'".
+ { iApply (lft_incl_glb with "[] []").
+ - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl.
+ apply gmultiset_union_subseteq_l.
+ - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
iFrame. iIntros (q') "!#Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
@@ -87,7 +88,7 @@ Section ty_incl.
by iApply (ty_shr_mono with "LFT Hincl' H").
Qed.
- Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
+ Lemma lft_incl_ty_incl_shared_bor ty κ1 κ2 :
ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
Proof.
iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
@@ -173,15 +174,15 @@ Section ty_incl.
apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
induction tyl2 as [|ty tyl2 IH]; simpl.
- - iIntros (tid) "#LFT _". iMod (borrow_create with "LFT []") as "[Hbor _]".
+ - iIntros (tid) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]".
done. instantiate (1:=True%I). by auto. instantiate (1:=static).
- iMod (borrow_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
+ iMod (bor_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
iSplitL; iIntros "/=!>!#*H".
+ iExists [], vl. iFrame. auto.
+ iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto.
setoid_rewrite heap_mapsto_vec_nil.
- iApply (frac_borrow_shorten with "[] Hbor"). iApply lft_incl_static.
+ iApply (frac_bor_shorten with "[] Hbor"). iApply lft_incl_static.
- etransitivity; last apply ty_incl_prod2_assoc1.
eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
Qed.
@@ -191,7 +192,7 @@ Section ty_incl.
ty_incl Ï (sum tyl1) (sum tyl2).
Proof.
iIntros (DUP FA tid) "#LFT #HÏ". rewrite /sum /=. iSplitR "".
- - assert (Hincl : lft_ctx ⊢ Ï tid ={⊤}=∗
+ - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
(□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
→ (nth i tyl2 ∅%T).(ty_own) tid vl)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
@@ -202,7 +203,7 @@ Section ty_incl.
iMod (Hincl with "LFT HÏ") as "#Hincl". iIntros "!>!#*H".
iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
by iApply "Hincl".
- - assert (Hincl : lft_ctx ⊢ Ï tid ={⊤}=∗
+ - assert (Hincl : lft_ctx -∗ Ï tid ={⊤}=∗
(□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
→ (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
{ clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
diff --git a/theories/typing.v b/theories/typing/typing.v
similarity index 80%
rename from theories/typing.v
rename to theories/typing/typing.v
index bf0398bf219a0eabc4ffe3958671c293c70740da..f9d4063712724f535ec6bfff248fbfbcfb1c208e 100644
--- a/theories/typing.v
+++ b/theories/typing/typing.v
@@ -1,7 +1,9 @@
From iris.program_logic Require Import hoare.
From iris.base_logic Require Import big_op.
-From lrust Require Export type perm notation memcpy.
-From lrust Require Import perm_incl proofmode.
+From lrust.lang Require Export notation memcpy.
+From lrust.typing Require Export type perm.
+From lrust Require Import typing.perm_incl lang.proofmode.
+From lrust.lifetime Require Import frac_borrow.
Import Types Perm.
@@ -87,7 +89,7 @@ Section typing.
Lemma typed_valuable (ν : expr) ty:
typed_step_ty (ν ◠ty) ν ty.
Proof.
- iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
+ iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
Qed.
Lemma typed_plus e1 e2 Ï1 Ï2:
@@ -142,7 +144,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.
@@ -165,7 +167,7 @@ Section typing.
typed_step (ν ◠own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
Proof.
iIntros (tid) "!#(#HEAP&_&Hâ—&$)". wp_bind ν.
- iApply (has_type_wp with "[$Hâ—]"). iIntros (v) "[_ Hâ—]!>".
+ iApply (has_type_wp with "[$Hâ—]"). iIntros (v) "_ Hâ— !>".
rewrite has_type_value.
iDestruct "Hâ—" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
@@ -173,10 +175,10 @@ Section typing.
Qed.
Definition consumes (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
- ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
- lft_ctx ⊢ Ï1 ν tid -∗ tl_own tid ⊤ -∗
+ ∀ ν 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 {{ Φ }}.
@@ -184,11 +186,11 @@ Section typing.
Lemma consumes_copy_own ty q:
ty.(ty_dup) → consumes ty (λ ν, ν ◠own q ty)%P (λ ν, ν ◠own q ty)%P.
Proof.
- iIntros (? ν tid Φ E ?) "_ Hâ— Htl HΦ". iApply (has_type_wp with "[- $Hâ—]").
- iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ iIntros (? ν tid Φ E ?) "_ Hâ— Htl HΦ". 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 & 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.
@@ -198,11 +200,11 @@ Section typing.
consumes ty (λ ν, ν ◠own q ty)%P
(λ ν, ν ◠own q (Π(replicate ty.(ty_size) uninit)))%P.
Proof.
- iIntros (ν tid Φ E ?) "_ Hâ— Htl HΦ". iApply (has_type_wp with "[- $Hâ—]").
- iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ iIntros (ν tid Φ E ?) "_ Hâ— Htl HΦ". 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 & 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†".
@@ -213,38 +215,38 @@ Section typing.
clear. induction ty.(ty_size). done. by apply (f_equal S).
Qed.
- Lemma consumes_copy_uniq_borrow ty κ κ' q:
+ Lemma consumes_copy_uniq_bor ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
(λ ν, ν ◠&uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) Htl HΦ".
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ 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 H↦]". iDestruct "Heq" as %[=->].
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.
+ iMod (bor_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.
iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
Qed.
- Lemma consumes_copy_shr_borrow ty κ κ' q:
+ Lemma consumes_copy_shr_bor ty κ κ' q:
ty.(ty_dup) →
consumes ty (λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
(λ ν, ν ◠&shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (? ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) Htl HΦ".
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ 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.
@@ -262,43 +264,42 @@ Section typing.
iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
Qed.
- Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
+ Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
typed_step (ν ◠&uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
(!ν)
(λ v, v ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]!>". iDestruct "Hνv" as %Hνv.
+ 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 H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
- iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
+ iMod (bor_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
subst. rewrite heap_mapsto_vec_singleton. wp_read.
iMod ("Hclose'" with "*[H↦ Hown H†]") as "[Hbor Htok]"; last first.
- - iMod (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
- iMod (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
+ - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+ iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
- iIntros "{$H↦ $H†$Hown}!>_(?&?&?)!>". iNext. iExists _.
rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
Qed.
- Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
+ Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
typed_step (ν ◠&shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
(!ν)
(λ v, v ◠&shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑ & Htok) & $)". wp_bind ν.
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]!>". iDestruct "Hνv" as %Hνv.
+ 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 #H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
iDestruct "H↦" as (vl) "[H↦b Hown]".
- iMod (frac_borrow_acc with "LFT [] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
+ iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
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'".
@@ -306,50 +307,53 @@ Section typing.
iFrame "#". iExists _. eauto.
Qed.
- Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
+ Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
typed_step (ν ◠&uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◠&uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]!>". iDestruct "Hνv" as %Hνv.
+ 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 H↦]". iDestruct "Heq" as %[=->].
iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
- iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
- iMod (borrow_split with "LFT Hbor") as "[H↦ Hbor]". done.
- iMod (borrow_exists with "LFT Hbor") as (l') "Hbor". done.
- iMod (borrow_split with "LFT Hbor") as "[Heq Hbor]". done.
- iMod (borrow_unnest with "LFT Hbor") as "Hbor". done.
- iMod (borrow_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
- iMod (borrow_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
- rewrite heap_mapsto_vec_singleton. wp_read.
- iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
- iMod ("Hclose" with "Htok") as "$". iFrame "#".
- iMod "Hbor". iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
- iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
+ iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
+ iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+ iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
+ iMod (bor_sep with "LFT Hbor") as "[Heq Hbor]". done.
+ iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
+ iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+ rewrite heap_mapsto_vec_singleton.
+ iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ ⌜v = #l'⌠∗ l ↦#l')%I). done.
+ iSplitR "Hbor H↦"; last first.
+ - iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done; last first.
+ iSplitL "Hbor". by iApply (bor_unnest with "LFT Hbor"). wp_read. auto.
+ - iIntros (v) "(Hbor & % & H↦)". subst.
+ iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
+ iMod ("Hclose" with "Htok") as "$". iFrame "#".
+ iExists _. iSplitR. done. iApply (bor_shorten with "[] Hbor").
+ iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
Qed.
- Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
+ Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
typed_step (ν ◠&shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
(!ν)
(λ v, v ◠&shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
Proof.
iIntros (tid) "!#(#HEAP & #LFT & (H◠& #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]!>". iDestruct "Hνv" as %Hνv.
+ 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 %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
- iMod (frac_borrow_acc with "LFT [] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
- { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
- iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
- { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+ iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+ iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
+ { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
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);
- last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
+ 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".
iMod ("Hclose'" with "[$H↦]") as "Htok'".
@@ -358,20 +362,19 @@ Section typing.
Qed.
Definition update (ty : type) (Ï1 Ï2 : expr → perm) : Prop :=
- ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
- lft_ctx ⊢ Ï1 ν tid -∗
+ ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
+ lft_ctx -∗ Ï1 ν tid -∗
(∀ (l:loc) 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 {{ Φ }}.
+ (⌜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 {{ Φ }}.
Lemma update_strong ty1 ty2 q:
ty1.(ty_size) = ty2.(ty_size) →
update ty1 (λ ν, ν ◠own q ty2)%P (λ ν, ν ◠own q ty1)%P.
Proof.
- iIntros (Hsz ν tid Φ E ?) "_ Hâ— HΦ". iApply (has_type_wp with "[- $Hâ—]").
- iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ iIntros (Hsz ν tid Φ E ?) "_ Hâ— HΦ". 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 & H↦ & >H†)".
iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
@@ -384,10 +387,10 @@ Section typing.
(λ ν, ν ◠&uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
Proof.
iIntros (ν tid Φ E ?) "#LFT (H◠& #H⊑ & Htok) HΦ".
- iApply (has_type_wp with "[- $Hâ—]"). iIntros (v) "[Hνv Hâ—]". iDestruct "Hνv" as %Hνv.
+ 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 & H↦)". iDestruct "Heq" as %[=->].
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.
+ iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
@@ -401,7 +404,7 @@ Section typing.
iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [HÏ1 Hâ—] & $)". wp_bind ν1.
iApply (Hupd with "LFT HÏ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
- wp_bind ν2. iApply (has_type_wp with "[- $Hâ—]"). iIntros (v') "[% Hâ—]!>".
+ wp_bind ν2. iApply (has_type_wp with "Hâ—"). iIntros (v') "% Hâ—!>".
rewrite heap_mapsto_vec_singleton. wp_write.
rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
Qed.
@@ -450,7 +453,7 @@ Section typing.
typed_program (Ï âˆ— ν â— bool) (if: ν then e1 else e2).
Proof.
iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [HÏ Hâ—] & Htl)".
- wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% Hâ—]!>".
+ wp_bind ν. iApply (has_type_wp with "Hâ—"). iIntros (v) "% Hâ—!>".
rewrite has_type_value. iDestruct "Hâ—" as (b) "Heq". iDestruct "Heq" as %[= ->].
wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
Qed.