Commit a38a1915 authored by Ralf Jung's avatar Ralf Jung

update dependencies

parent 707db861
Pipeline #42977 passed with stage
in 52 minutes and 16 seconds
......@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
"coq-gpfsl" { (= "dev.2021-02-14.0.24c31b61") | (= "dev") }
"coq-gpfsl" { (= "dev.2021-02-16.0.c0f38bcc") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -347,7 +347,7 @@ Proof.
- iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iExists _. iFrame "%". iRight. by iFrame.
- iExists (i.1). rewrite monPred_subjectively_unfold /=. iFrame "#".
rewrite bi.True_emp. iApply fupd_intro_mask'. solve_ndisj. }
rewrite bi.True_emp. iApply fupd_mask_subseteq. solve_ndisj. }
iLeft. unfold lft_bor_alive, idx_bor_own. iDestruct "Hbor" as (Vb) "[#HVb Hbor]".
iExists (P' Vb), (i.1). iFrame "#". rewrite [in _ Vκ]lft_inv_alive_unfold /lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
......@@ -358,7 +358,7 @@ Proof.
solve_ndisj. by rewrite lookup_fmap EQB.
iApply fupd_frame_l. iSplitL "HP'".
{ iNext. iSplit; [done|]. iApply "HPP'". by iApply monPred_in_elim. }
iMod fupd_intro_mask' as "Hclose"; [|iModIntro; iIntros (Q) "HvsQ HQ"].
iMod fupd_mask_subseteq as "Hclose"; [|iModIntro; iIntros (Q) "HvsQ HQ"].
solve_ndisj.
iMod "Hclose" as "_".
iAssert (▷⌜Vb Vκ⌝)%I as "#>%".
......
......@@ -62,7 +62,7 @@ Proof.
iDestruct (monPred_in_intro with "Htok") as (V) "[#HV Htok]".
iMod (idx_bor_acc_internal with "LFT Hs Hown Htok") as (Vb) "(% & HP & Hclose'')".
solve_ndisj. solve_ndisj.
iMod fupd_intro_mask' as "Hclose'''"; last iModIntro. solve_ndisj.
iMod fupd_mask_subseteq as "Hclose'''"; last iModIntro. solve_ndisj.
iExists Vb. iSplitL "HP".
{ iIntros "HVb". iApply "HPP'". iApply (monPred_in_elim with "HVb").
by rewrite monPred_at_later. }
......
......@@ -563,7 +563,7 @@ Section arc.
first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
......@@ -609,7 +609,7 @@ Section arc.
with "[] [] WR [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
......@@ -658,7 +658,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (t'' q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
......@@ -707,7 +707,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
......@@ -754,7 +754,7 @@ Section arc.
with "[] [] WR [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
......@@ -805,7 +805,7 @@ Section arc.
[by iDestruct "Hpersist" as "[$ _]"| |by iExists _,_|].
{ iIntros "!# Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q0. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro.
iExists Vb, q0. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
solve_ndisj. iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
......
......@@ -47,7 +47,7 @@ Section util.
iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
iApply "Hclose". auto.
- iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
- iMod fupd_mask_subseteq as "Hclose'"; first solve_ndisj. iModIntro.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_".
+ iModIntro. eauto.
+ iFrame. iModIntro. by iApply monPred_in_elim.
......@@ -79,7 +79,7 @@ Section util.
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]"; first solve_ndisj.
{ by iApply bor_shorten. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first solve_ndisj.
- iMod fupd_mask_subseteq as "Hclose'"; last iModIntro; first solve_ndisj.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_".
+ iModIntro. eauto.
+ iFrame. iModIntro. by iApply monPred_in_elim.
......
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