From 102f489791ed7ae843600750732213da1924a32e Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sat, 15 Feb 2020 10:55:56 +0100 Subject: [PATCH] bump Iris --- opam | 2 +- theories/lifetime/na_borrow.v | 2 +- theories/typing/lib/arc.v | 6 +++--- theories/typing/lib/rc/rc.v | 12 ++++++------ theories/typing/lib/rc/weak.v | 10 +++++----- theories/typing/util.v | 4 ++-- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/opam b/opam index 298e0e97..2cbc4276 100644 --- a/opam +++ b/opam @@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries. """ depends: [ - "coq-iris" { (= "dev.2020-02-12.1.db3bebcd") | (= "dev") } + "coq-iris" { (= "dev.2020-02-14.2.a3cea59c") | (= "dev") } ] build: [make "-j%{jobs}%"] diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v index 7af98c9e..81816c74 100644 --- a/theories/lifetime/na_borrow.v +++ b/theories/lifetime/na_borrow.v @@ -44,7 +44,7 @@ Section na_bor. Proof. iIntros (???) "#LFT#HP Hκ Hnaown". iDestruct "HP" as (i) "(#Hpers&#Hinv)". - iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done. + iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done. iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done. iIntros "{$HP $Hnaown} !> HP Hnaown". iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame. diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v index fcd2e370..a252a860 100644 --- a/theories/typing/lib/arc.v +++ b/theories/typing/lib/arc.v @@ -85,7 +85,7 @@ Section arc. iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H". iMod (inv_alloc arc_endN _ ([†ν] ∨ _)%I with "[H]") as "#INV"; first by iRight; iApply "H". iIntros "!> !# Hν". - iMod (inv_open with "INV") as "[[H†|[$ Hvs]] Hclose]"; + iMod (inv_acc with "INV") as "[[H†|[$ Hvs]] Hclose]"; [set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|]. rewrite difference_union_distr_l_L difference_diag_L right_id_L difference_disjoint_L; last solve_ndisj. @@ -124,7 +124,7 @@ Section arc. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I with "[Hpbown]") as "#Hinv"; first by iLeft. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb". { rewrite bor_unfold_idx. iExists _. by iFrame. } @@ -245,7 +245,7 @@ Section arc. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I with "[Hpbown]") as "#Hinv"; first by iLeft. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb". { rewrite bor_unfold_idx. iExists _. by iFrame. } diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index 67f16b8d..654a10db 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -142,7 +142,7 @@ Section rc. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I with "[Hpbown]") as "#Hinv"; first by iLeft. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb". { rewrite bor_unfold_idx. iExists _. by iFrame. } @@ -279,7 +279,7 @@ Section code. auto 10 with iFrame. - iDestruct "Hown" as (γ ν q) "(#Hpersist & Htok & Hν1)". iPoseProof "Hpersist" as (ty') "(Hincl & Hinv & _ & #Hνend)". - iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|]. iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]". iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)] %option_included _]%prod_included [Hval _]]%auth_both_valid. @@ -334,7 +334,7 @@ Section code. rewrite Hincls. iFrame. iSplitL "Hty". { iDestruct "Hty" as (vl) "[??]". iExists _. iFrame. by iApply "Hinclo". } iIntros "!> Hna". iClear "Hνend". clear q' Hqq' weak Hval. - iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|]. iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]". iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)] %option_included _]%prod_included [Hval _]]%auth_both_valid. @@ -404,7 +404,7 @@ Section code. iModIntro. wp_let. wp_op. rewrite shift_loc_0. (* Finally, finally... opening the thread-local Rc protocol. *) iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)". - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)] @@ -463,7 +463,7 @@ Section code. iModIntro. wp_let. wp_op. (* Finally, finally... opening the thread-local Rc protocol. *) iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)". - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)] @@ -568,7 +568,7 @@ Section code. iModIntro. wp_let. wp_op. rewrite shift_loc_0. (* Finally, finally... opening the thread-local Rc protocol. *) iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)". - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)] diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v index f9cfc80c..ded42fd5 100644 --- a/theories/typing/lib/rc/weak.v +++ b/theories/typing/lib/rc/weak.v @@ -40,7 +40,7 @@ Section weak. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I with "[Hpbown]") as "#Hinv"; first by iLeft. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose1]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb". { rewrite bor_unfold_idx. iExists _. by iFrame. } @@ -154,7 +154,7 @@ Section code. iModIntro. wp_let. wp_op. rewrite shift_loc_0. (* Finally, finally... opening the thread-local Rc protocol. *) iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)". - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hwtok") as @@ -257,7 +257,7 @@ Section code. iModIntro. wp_let. wp_op. (* Finally, finally... opening the thread-local Rc protocol. *) iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)". - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)] @@ -323,7 +323,7 @@ Section code. iAssert (∃ wv : Z, (l' +ₗ 1) ↦ #wv ∗ ((l' +ₗ 1) ↦ #(wv + 1) ={⊤}=∗ na_own tid ⊤ ∗ (q / 2).[α] ∗ own γ weak_tok))%I with "[> Hna Hα1]" as (wv) "[Hwv Hclose2]". - { iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. + { iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|]. iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hwtok") as @@ -397,7 +397,7 @@ Section code. with "[>Hna Hwtok]" as (wv) "[Hlw [(% & Hna & H)|[% Hclose]]]". { iPoseProof "Hpersist" as (ty') "([>Hszeq _] & Hinv & _ & _)". iDestruct "Hszeq" as %Hszeq. - iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|]. + iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|]. iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]". iDestruct (own_valid_2 with "Hrc● Hwtok") as %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid. diff --git a/theories/typing/util.v b/theories/typing/util.v index 9dae5dac..ce4cb571 100644 --- a/theories/typing/util.v +++ b/theories/typing/util.v @@ -36,7 +36,7 @@ Section util. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l)%I with "[Hpbown]") as "#Hinv"; first by eauto. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj. { rewrite bor_unfold_idx. eauto. } @@ -58,7 +58,7 @@ Section util. iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ'' tid l)%I with "[Hpbown]") as "#Hinv"; first by eauto. iIntros "!> !# * % Htok". - iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj. + iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj. iDestruct "INV" as "[>Hbtok|#Hshr]". - iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj. { iApply bor_unfold_idx. eauto. } -- GitLab