Commit 59f2c74c authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Change names for bor_persistent.

parent a5e0c019
Pipeline #9114 passed with stage
in 11 minutes and 18 seconds
......@@ -119,7 +119,7 @@ Proof.
iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
Qed.
Lemma bor_persistent P `{!Persistent P} E κ :
Lemma bor_persistent_notok P `{!Persistent P} E κ :
lftN E
lft_ctx - &{κ}P ={E}= P [†κ].
Proof.
......@@ -129,7 +129,7 @@ Proof.
- iMod "Hclose" as "_". auto.
Qed.
Lemma bor_persistent_tok P `{!Persistent P} E κ q :
Lemma bor_persistent P `{!Persistent P} E κ q :
lftN E
lft_ctx - &{κ}P - q.[κ] ={E}= P q.[κ].
Proof.
......@@ -174,7 +174,7 @@ Proof.
rewrite ->(bor_unfold_idx _ P).
iMod (bor_exists with "LFT Hbor") as (i) "Hbor"; [done|].
iMod (bor_sep with "LFT Hbor") as "[Hidx Hbor]"; [done|].
iMod (bor_persistent with "LFT Hidx") as "#[Hidx|H†]"; [done| |].
iMod (bor_persistent_notok with "LFT Hidx") as "#[Hidx|H†]"; [done| |].
- iIntros "!>". iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
- iApply (bor_fake with "LFT"); [done|]. rewrite -lft_dead_or. auto.
Qed.
......
......@@ -151,7 +151,7 @@ Section borrow.
iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
destruct vl as [|[[]|][]];
try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
......
......@@ -116,7 +116,7 @@ Section arc.
but that would be additional work here... *)
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
......@@ -237,7 +237,7 @@ Section arc.
but that would be additional work here... *)
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
......@@ -934,7 +934,7 @@ Section arc.
iMod (bor_exists with "LFT Hrc'") as (rcvl) "Hrc'"=>//.
iMod (bor_sep with "LFT Hrc'") as "[Hrc'↦ Hrc]"=>//.
destruct rcvl as [|[[|rc|]|][|]]; try by
iMod (bor_persistent_tok with "LFT Hrc Hα") as "[>[] ?]".
iMod (bor_persistent with "LFT Hrc Hα") as "[>[] ?]".
rewrite heap_mapsto_vec_singleton.
iMod (bor_acc with "LFT Hrc'↦ Hα") as "[Hrc'↦ Hclose2]"=>//. wp_read.
iMod ("Hclose2" with "Hrc'↦") as "[_ Hα]".
......
......@@ -51,12 +51,12 @@ Section mguard.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
setoid_rewrite heap_mapsto_vec_singleton.
iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
iMod (bor_sep with "LFT H") as "[_ H]"; first done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
......@@ -208,12 +208,12 @@ Section code.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
[solve_typing..|].
destruct vl as [|[[|lm|]|] [|]]; simpl;
try by iMod (bor_persistent_tok with "LFT Hprot Hα") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hprot Hα") as "[>[] _]".
rewrite heap_mapsto_vec_singleton.
iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
iMod (bor_persistent with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
wp_read. wp_let. iMod "Hlm".
......
......@@ -135,7 +135,7 @@ Section rc.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
......
......@@ -33,7 +33,7 @@ Section weak.
but that would be additional work here... *)
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][|]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
......
......@@ -42,18 +42,18 @@ Section ref.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
iMod (bor_persistent_tok with "LFT Hshr Htok") as "[#Hshr Htok]". done.
iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
......
......@@ -43,7 +43,7 @@ Section refmut.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
......@@ -55,7 +55,7 @@ Section refmut.
{ by rewrite Qp_mult_1_l. }
iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
iApply lft_incl_glb; first done. iApply lft_incl_refl.
......
......@@ -71,14 +71,14 @@ Section refmut_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
[solve_typing..|].
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
iMod (bor_exists with "LFT H") as (ν) "H". done.
iMod (bor_exists with "LFT H") as (γ) "H". done.
iMod (bor_exists with "LFT H") as (δ) "H". done.
iMod (bor_exists with "LFT H") as (ty') "H". done.
iMod (bor_sep with "LFT H") as "[Hb H]". done.
iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
iMod (bor_sep with "LFT H") as "[_ H]". done.
iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
......
......@@ -37,17 +37,17 @@ Section rwlockreadguard.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
iMod (bor_persistent_tok with "LFT Hshr Htok") as "[#Hshr Htok]". done.
iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
......
......@@ -38,12 +38,12 @@ Section rwlockwriteguard.
iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
......
......@@ -76,13 +76,13 @@ Section rwlockwriteguard_functions.
iMod (bor_sep with "LFT H") as "[H↦ H]". done.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
destruct vl as [|[[|l|]|][]];
try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
rewrite heap_mapsto_vec_singleton.
iMod (bor_exists with "LFT H") as (γ) "H". done.
iMod (bor_exists with "LFT H") as (δ) "H". done.
iMod (bor_sep with "LFT H") as "[Hb H]". done.
iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_op. wp_let. iMod "Hb".
......
......@@ -70,7 +70,7 @@ Section own.
iMod (bor_exists with "LFT Hshr") as (vl) "Hb"; first solve_ndisj.
iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
destruct vl as [|[[|l'|]|][]];
try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
iMod (bor_fracture (λ q, l {q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
......
......@@ -133,7 +133,7 @@ Next Obligation.
iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
iMod (bor_persistent with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
Qed.
Next Obligation.
......
......@@ -25,7 +25,7 @@ Section uniq_bor.
move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first solve_ndisj;
(iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
iMod (bor_fracture (λ q, l {q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
iApply delay_sharing_nested; try done. iApply lft_incl_refl.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment