From e4c72b1d7865da7f963171ea3e11ba8e9435e6c4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Nov 2018 19:31:00 +0100
Subject: [PATCH] Update Readme and development wrt. technical appendix.
---
README.md | 90 +++++++++++++++---------
theories/lifetime/frac_borrow.v | 4 +-
theories/lifetime/lifetime.v | 22 ++++++
theories/lifetime/lifetime_sig.v | 9 +--
theories/lifetime/model/accessors.v | 9 +--
theories/lifetime/model/creation.v | 4 +-
theories/lifetime/model/primitive.v | 24 ++-----
theories/lifetime/model/reborrow.v | 6 +-
theories/lifetime/na_borrow.v | 2 +-
theories/typing/lib/arc.v | 13 ++--
theories/typing/lib/rc/rc.v | 2 +-
theories/typing/lib/rc/weak.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
theories/typing/util.v | 4 +-
14 files changed, 113 insertions(+), 80 deletions(-)
diff --git a/README.md b/README.md
index ec9743e5..584f6b8c 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,7 @@
# LAMBDA-RUST COQ DEVELOPMENT
-This is the Coq development accompanying lambda-Rust.
+This is the Coq development accompanying lambda-Rust, in the
+weak-memory setting..
## Prerequisites
@@ -31,9 +32,6 @@ CPU cores.
## Structure
-* The folder [lang](theories/lang) contains the formalization of the lambda-Rust
- core language, including the theorem showing that programs with data races get
- stuck.
* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
logic, including derived constructions like (non-)atomic persistent borrows.
* The subfolder [model](theories/lifetime/model) proves the core rules, which
@@ -58,9 +56,9 @@ CPU cores.
### Type System Rules
-The files in [typing](theories/typing) prove semantic versions of the proof
-rules given in the paper. Notice that mutable borrows are called "unique
-borrows" in the Coq development.
+The files in [typing](theories/typing) prove semantic versions of the
+proof rules given in the original RustBelt paper. Notice that mutable
+borrows are called "unique borrows" in the Coq development.
| Proof Rule | File | Lemma |
|-----------------------|-----------------|-----------------------|
@@ -93,37 +91,65 @@ borrows" in the Coq development.
| F-endlft | programs.v | type_endlft |
| F-call | function.v | type_call' |
-Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
+Some of these lemmas are called `something'` because the version
+without the `'` is a derived, more specialized form used together with
+our eauto-based `solve_typing` tactic. You can see this tactic in
+action in the [examples](theories/typing/examples) subfolder.
### Lifetime Logic Rules
The files in [lifetime](theories/lifetime) prove the lifetime logic, with the
core rules being proven in the [model](theories/lifetime/model) subfolder and
then sealed behind a module signature in
-[lifetime.v](theories/lifetime/lifetime.v).
-
-
-| Proof Rule | File | Lemma |
-|-------------------|---------------------|----------------------|
-| LftL-begin | model/creation.v | lft_create |
-| LftL-tok-fract | model/primitive.v | lft_tok_fractional |
-| LftL-not-own-end | model/primitive.v | lft_tok_dead |
-| LftL-end-persist | model/definitions.v | lft_dead_persistent |
-| LftL-borrow | model/borrow.v | bor_create |
-| LftL-bor-split | model/bor_sep.v | bor_sep |
-| LftL-bor-acc | lifetime.v | bor_acc |
-| LftL-bor-shorten | model/primitive.v | bor_shorten |
-| LftL-incl-isect | model/primitive.v | lft_intersect_incl_l |
-| LftL-incl-glb | model/primitive.v | lft_incl_glb |
-| LftL-tok-inter | model/primitive.v | lft_tok_sep |
-| LftL-end-inter | model/primitive.v | lft_dead_or |
-| LftL-tok-unit | model/primitive.v | lft_tok_static |
-| LftL-end-unit | model/primitive.v | lft_dead_static |
-| LftL-reborrow | lifetime.v | rebor |
-| LftL-bor-fracture | frac_borrow.v | bor_fracture |
-| LftL-fract-acc | frac_borrow.v | frac_bor_atomic_acc |
-| LftL-bor-na | na_borrow.v | bor_na |
-| LftL-na-acc | na_borrow.v | na_bor_acc |
+[lifetime.v](theories/lifetime/lifetime.v). The interface of the core
+lifetime logic is in [lifetime_sig.v](theories/lifetime/lifetime_sig.v).
+
+| Proof Rule | File | Lemma |
+|----------------------------|----------------------|-----------------------|
+| LftL-begin | model/creation.v | lft_create |
+| LftL-tok-fract | model/primitive.v | lft_tok_fractional |
+| LftL-tok-fract-obj | model/primitive.v | lft_tok_split_obj |
+| LftL-tok-comp | model/primitive.v | lft_tok_sep |
+| LftL-tok-unit | model/primitive.v | lft_tok_static |
+| LftL-not-own-end | model/primitive.v | lft_tok_dead |
+| LftL-end-comp | model/primitive.v | lft_dead_or |
+| LftL-end-unit | model/primitive.v | lft_dead_static |
+| LftL-borrow | model/borrow.v | bor_create |
+| LftL-bor-sep | model/bor_sep.v | bor_sep, bor_combine |
+| LftL-bor-fake | model/faking.v | bor_fake |
+| LftL-bor-acc-strong | model/accessors.v | bor_acc_strong |
+| LftL-bor-acc-atomic-strong | model/accessors.v | bor_acc_atomic_strong |
+| LftL-bor-idx | model/primitive.v | bor_unfold_idx |
+| LftL-idx-shorten | model/primitive.v | idx_bor_shorten |
+| LftL-idx-acc | model/accessors.v | idx_bor_acc |
+| LftL-idx-bor-unnest | model/reborrow.v | idx_bor_unnest |
+| LftL-idx-bor-iff | model/reborrow.v | idx_bor_iff |
+| LftL-bor-in-at | model/in_at_borrow.v | in_at_bor_share |
+| LftL-in-at-acc | model/in_at_borrow.v | in_at_bor_acc |
+| LftL-in-at-shorten | model/in_at_borrow.v | in_at_bor_shorten |
+| LftL-in-at-iff | model/in_at_borrow.v | in_at_bor_iff |
+| LftL-incl-isect | model/primitive.v | lft_intersect_incl_l |
+| LftL-incl-glb | model/primitive.v | lft_incl_glb |
+| LftL-fract-lincl | frac_borrow.v | frac_bor_lft_incl |
+| LftL-bor-shorten | lifetime.v | bor_shorten |
+| LftL-reborrow | lifetime.v | rebor |
+| LftL-bor-unnest | lifetime.v | bor_unnest |
+| LftL-bor-acc-cons | lifetime.v | bor_acc_cons |
+| LftL-bor-acc | lifetime.v | bor_acc |
+| LftL-bor-freeze | lifetime.v | bor_exists |
+| LftL-bor-iff | lifetime.v | bor_iff |
+| LftL-bor-at | at_borrow.v | at_bor_share |
+| LftL-at-acc | at_borrow.v | at_bor_acc |
+| LftL-at-shorten | at_borrow.v | at_bor_shorten |
+| LftL-at-iff | at_borrow.v | at_bor_iff |
+| LftL-bor-na | na_borrow.v | bor_na |
+| LftL-na-acc | na_borrow.v | na_bor_acc |
+| LftL-na-shorten | na_borrow.v | na_bor_shorten |
+| LftL-na-iff | na_borrow.v | na_bor_iff |
+| LftL-bor-fracture | frac_borrow.v | bor_fracture' |
+| LftL-fract-acc | frac_borrow.v | frac_bor_acc |
+| LftL-fract-shorten | frac_borrow.v | frac_bor_shorten |
+| LftL-fract-iff | frac_borrow.v | frac_bor_iff |
## For Developers: How to update the Iris dependency
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e4f38a86..2b61160f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -84,7 +84,7 @@ Section frac_bor.
iDestruct "Hφ" as (q q' q'' ?? Hsum) "(Hφ1 & Htok & Hφ2 & _)".
destruct (decide (0 < q')%Qc).
{ iExFalso. rewrite -(embed_pure False). iModIntro ⎡_⎤%I.
- iApply (lft_tok_dead with "Htok [H†]"). iApply "H†". }
+ iApply (lft_tok_dead_subj with "Htok [H†]"). iApply "H†". }
destruct (Qcle_lt_or_eq 0 q') as [|<-]; [done|done|].
rewrite Qcplus_0_r in Hsum. destruct (decide (0 < q'')%Qc).
{ iDestruct ("Hfrac" with "[Hφ1 Hφ2]") as "H".
@@ -115,7 +115,7 @@ Section frac_bor.
iIntros (?) "#LFT Hfrac Hκ".
iDestruct "Hfrac" as (γ κ' V0 φ') "#(Hκκ' & HV0 & Hφ' & Hfrac & Hshr)".
iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[Hκ Hclose]". done.
- rewrite -{1}(Qp_div_2 qκ'). rewrite lft_tok_split_unit.
+ rewrite -{1}(Qp_div_2 qκ'). rewrite lft_tok_split_obj.
iDestruct "Hκ" as "[Hκ1 Hκ2]".
iMod (in_at_bor_acc with "LFT Hshr Hκ1") as (Vb) "[H Hclose']"; try done.
iCombine "H HV0" as "HH".
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 7e7641ef..56220c21 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -29,6 +29,21 @@ Section derived.
Context `{invG Σ, lftG Lat E0 Σ}.
Implicit Types κ : lft.
+Lemma lft_tok_dead_subj q κ :
+ q.[κ] -∗ <subj> [† κ] -∗ False.
+Proof.
+ iStartProof (iProp _). iIntros "% ?" (V) "-> H†".
+ iDestruct "H†" as (?) "H†".
+ iApply (lft_tok_dead $! (_⊔_) with "[$] [$]").
+Qed.
+
+Lemma bor_shorten κ κ' P :
+ κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+Proof.
+ rewrite !bor_unfold_idx. iIntros "#?".
+ iDestruct 1 as (i) "[??]". iExists i. iFrame. by iApply idx_bor_shorten.
+Qed.
+
Lemma bor_acc_atomic_cons E κ P :
↑lftN ⊆ E →
⎡lft_ctx⎤ -∗ &{κ}P ={E,E∖↑lftN}=∗
@@ -119,6 +134,13 @@ Proof.
iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
Qed.
+Lemma bor_iff κ P P' :
+ ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Proof.
+ rewrite !bor_unfold_idx. iIntros "#?".
+ iDestruct 1 as (i) "[??]". iExists i. iFrame. by iApply idx_bor_iff.
+Qed.
+
Lemma bor_iff_proper κ P P' :
▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
Proof.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 9d9468c9..41ecad21 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -101,10 +101,10 @@ Module Type lifetime_sig.
(** Laws *)
Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
- Parameter lft_tok_split_unit :
+ Parameter lft_tok_split_obj :
∀ `{LatBottom Lat} q1 q2 κ, (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
- Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ <subj> [† κ] -∗ False.
+ Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
Parameter lft_tok_static : ∀ q, (q.[static])%I.
Parameter lft_dead_static : [† static] -∗ False.
@@ -115,9 +115,6 @@ Module Type lifetime_sig.
Parameter bor_fake : ∀ `{LatBottom Lat} E κ P,
↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ <subj>[†κ] ={E}=∗ &{κ}P.
- Parameter bor_iff : ∀ κ P P', ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
- Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
-
Parameter bor_sep : ∀ `{LatBottom Lat} E κ P Q, ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗
&{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
Parameter bor_combine : ∀ `{LatBottom Lat} E κ P Q,
@@ -159,7 +156,7 @@ Module Type lifetime_sig.
inheritance). Hence, we actually get that the consequence view
shift happens at a view which is larger than the current view.
See the comment in accessors.v for why the consequence VS only
- gets the dead token under the objective modality. *)
+ gets the dead token under the subjectively modality. *)
Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E →
⎡lft_ctx⎤ -∗ &{κ}P ={E,E∖↑lftN}=∗
(∃ P' κ', κ ⊑ κ' ∗ ▷ (⎡P'⎤ ∧ P) ∗
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 3a2c5308..82af0c04 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -151,8 +151,8 @@ Proof.
iDestruct "Hinv" as "[Hinv Hclose']".
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
{ iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
- iDestruct (lft_tok_dead with "Htok [H†]") as "[]".
- by rewrite monPred_subjectively_unfold /=. }
+ iDestruct "H†" as (V) "H†".
+ iDestruct (lft_tok_dead $! (Vtok⊔V) with "Htok H†") as "[]". }
rewrite [in _ Vκ]lft_inv_alive_unfold.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_open_internal with "Hs Halive Hbor Htok") as (V) "(% & Halive & Hf & HP)".
@@ -248,8 +248,9 @@ Proof.
iDestruct "Hinv" as "[Hinv Hclose'']".
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
{ iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
- iDestruct (lft_tok_dead with "Htok [H†]") as "[]".
- by rewrite monPred_subjectively_unfold /=. }
+ iDestruct (monPred_in_intro with "Htok") as (Vtok) "[_ Htok]".
+ iDestruct "H†" as (V) "H†". iAssert ⎡False⎤%I as %[]. iModIntro.
+ iApply (lft_tok_dead $! (Vtok⊔V) with "Htok H†"). }
rewrite [in _ Vκ]lft_inv_alive_unfold.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iCombine "Hbor Htok" as "HborHtok".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index c6816981..0ceda27b 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -26,8 +26,8 @@ Proof.
iAssert ⌜∀ i s, B !! i = Some s → ∃ V, s = Bor_in V ∧ V ⊑ (Vs κ)⌝%I with "[#]" as %HB.
{ iIntros (i s HBI). rewrite (big_sepM_lookup _ B) //.
destruct s as [V|q|κ']; rewrite /bor_cnt; [iExists _; by iSplit| |].
- { iDestruct (lft_tok_dead with "[HB] [Hκ]") as "[]";
- [iDestruct "HB" as "[_ $]" | by rewrite monPred_subjectively_unfold]. }
+ { iDestruct "HB" as "[_ HB]". iDestruct "Hκ" as (Vκ) "Hκ".
+ iDestruct (lft_tok_dead $! (Vtok⊔Vκ) 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"; [by apply HK|].
rewrite /lft_inv_dead; iDestruct "Hdead" as (R Vinh) "(_ & _ & Hcnt' & _)".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8044b21b..ba33ebbe 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -283,14 +283,12 @@ Proof.
rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
Qed.
-Lemma lft_tok_dead q κ : q.[κ] -∗ <subj> [† κ] -∗ False.
+Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
Proof.
- (* FIXME iris : FromExists / IntoExists for subjectively
- Idem for objectively. *)
- rewrite /lft_tok /lft_dead /= monPred_subjectively_unfold. iIntros "H".
- iDestruct 1 as (V0 Λ' V') "(% & % & H')".
+ rewrite /lft_tok /lft_dead. iIntros "H".
+ iDestruct 1 as (Λ' V') "(% & #? & H')".
iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
- iDestruct "H" as (V'') "[_' H]". iDestruct (own_valid_2 with "H H'") as %Hvalid.
+ iDestruct "H" as (V'') "[#? H]". iDestruct (own_valid_2 with "H H'") as %Hvalid.
move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
Qed.
@@ -320,7 +318,7 @@ Qed.
Global Instance lft_tok_as_fractional κ q :
AsFractional (q.[κ]) (λ q, q.[κ])%I q.
Proof. split. done. apply _. Qed.
-Lemma lft_tok_split_unit `{LatBottom Lat bot} q1 q2 κ :
+Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
(q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
Proof.
rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sepMS.
@@ -418,18 +416,6 @@ Proof.
- iDestruct 1 as ([κ' s]) "[[??]?]". iExists κ'. iFrame. iExists s. by iFrame.
Qed.
-Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
-Proof.
- rewrite !bor_unfold_idx. iIntros "#HPP' HP". iDestruct "HP" as (i) "[??]".
- iExists i. iFrame. by iApply (idx_bor_iff with "HPP'").
-Qed.
-
-Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
-Proof.
- rewrite /bor. iIntros "#Hκκ'". iDestruct 1 as (i) "[#? ?]".
- iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
-Qed.
-
Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i}P -∗ &{κ,i}P.
Proof.
rewrite /idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'").
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index a74d56d7..48d3106f 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -232,9 +232,9 @@ Proof.
{ iMod (bor_acc_strong with "LFT [Hbor] []") as (?) "(_ & Hbor & _)";
[done| |iApply (lft_tok_static 1)|].
- rewrite /bor. iExists static. iFrame. iApply lft_incl_refl.
- - iDestruct "Hbor" as ">Hbor". iApply bor_shorten.
- + iApply lft_intersect_incl_l.
- + rewrite bor_unfold_idx /=. auto. }
+ - iDestruct "Hbor" as ">Hbor". rewrite bor_unfold_idx /=.
+ iExists i. iFrame. iApply idx_bor_shorten; [|done].
+ iApply lft_intersect_incl_l. }
rewrite /idx_bor /bor. destruct i as [κ0 i].
iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 810e8be3..203fc247 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -56,7 +56,7 @@ Section na_bor.
iApply (idx_bor_shorten with "Hκκ' H").
Qed.
- Lemma na_bor_fake E κ P : ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
+ Lemma na_bor_fake E κ P : ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ <subj> [†κ] ={E}=∗ &na{κ,tid,N}P.
Proof.
iIntros (?) "#LFT#H†". iApply (bor_na with "[>]"); first done.
by iApply (bor_fake with "LFT H†").
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index dd715e07..f5d9cd01 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -126,7 +126,8 @@ Section arc.
{ rewrite -embed_or. iNext. by iApply "H". }
iIntros "!> !# Hν".
iMod (inv_open with "INV") as "[[H†|[>$ Hvs]] Hclose]"; [set_solver|..].
- { iDestruct "H†" as (?) ">H†". iDestruct (lft_tok_dead with "Hν [H†]") as "[]".
+ { iDestruct "H†" as (?) ">H†".
+ iDestruct (lft_tok_dead_subj with "Hν [H†]") as "[]".
rewrite monPred_subjectively_unfold. by iExists _. }
iDestruct (monPred_in_elim with "Inc [Hvs]") as "Hvs";
first by rewrite -monPred_at_later.
@@ -139,7 +140,7 @@ Section arc.
iIntros "{$Hν} !>". iMod ("Hclose" with "[Hν]") as "_"; [|done].
iLeft. iDestruct (monPred_in_intro with "Hν") as (?) "[? ?]".
iNext. by iExists _.
- Unshelve. by move => ??; iApply lft_tok_split_unit.
+ Unshelve. by move => ??; iApply lft_tok_split_obj.
Qed.
Program Definition arc (ty : type) :=
@@ -180,7 +181,7 @@ Section arc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
remember ((full_arc_own _ _ _ ∨ shared_arc_own _ _ _)%I) as X.
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
@@ -319,7 +320,7 @@ Section arc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
iDestruct "HP" as (γi γs γw γsw ν tw q') "[#Hpersist H]".
@@ -671,7 +672,7 @@ Section arc.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
- Unshelve. by move => ??; iApply lft_tok_split_unit.
+ Unshelve. by move => ??; iApply lft_tok_split_obj.
Qed.
Definition weak_clone : val :=
@@ -828,7 +829,7 @@ Section arc.
iApply (type_sum_unit (option (arc ty))); [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
- Unshelve. by move => ??; iApply lft_tok_split_unit.
+ Unshelve. by move => ??; iApply lft_tok_split_obj.
Qed.
(* Code : drop *)
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 37bee7d3..046524d3 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -149,7 +149,7 @@ Section rc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
remember ((∃ _ _ _, rc_persist _ _ _ _ _ ∗ _)%I) as X.
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; [solve_ndisj|].
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 226d8a01..6f8044b2 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -46,7 +46,7 @@ Section weak.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
iDestruct "HP" as (γ ν) "(#Hpersist & Hweak)".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index df68916d..7cb236ba 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -176,7 +176,7 @@ Section rwlock_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
- iDestruct (lft_tok_split_unit (qβ/2) (qβ/2) β with "[Hβtok]")
+ iDestruct (lft_tok_split_obj (qβ/2) (qβ/2) β with "[Hβtok]")
as "[Hβtok1 Hβtok2]". { by rewrite Qp_div_2. }
iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & R) & Hinv)".
iDestruct "R" as (tR vR) "R".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 613d28d3..18cf8124 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -40,7 +40,7 @@ Section util.
iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- rewrite -(Qp_div_2 q).
- iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
rewrite monPred_objectively_unfold. iSpecialize ("Htok" $! V).
iApply (monPred_in_elim with "Hin"). iModIntro.
iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
@@ -71,7 +71,7 @@ Section util.
iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- rewrite -(Qp_div_2 q).
- iDestruct (lft_tok_split_unit with "Htok") as "[$ Htok]".
+ iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
rewrite monPred_objectively_unfold. iSpecialize ("Htok" $! V).
iApply (monPred_in_elim with "Hin"). iModIntro.
iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
--
GitLab