From cae8a10205d6aa5e915f04c99de5088bc778d062 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 28 May 2018 13:30:10 +0200 Subject: [PATCH] update for Iris.gen_proofmode --- opam | 2 +- theories/lang/heap.v | 18 +++++------ theories/lang/lib/arc.v | 2 +- theories/lang/proofmode.v | 30 +++++++++---------- theories/lifetime/at_borrow.v | 2 +- theories/lifetime/frac_borrow.v | 6 ++-- theories/lifetime/lifetime.v | 2 +- theories/lifetime/lifetime_sig.v | 13 ++++---- theories/lifetime/model/accessors.v | 5 ++-- theories/lifetime/model/borrow.v | 3 +- theories/lifetime/model/borrow_sep.v | 5 ++-- theories/lifetime/model/creation.v | 1 - theories/lifetime/model/definitions.v | 11 ++++--- theories/lifetime/model/faking.v | 3 +- theories/lifetime/model/primitive.v | 20 ++++++------- theories/lifetime/model/reborrow.v | 3 +- theories/lifetime/na_borrow.v | 2 +- theories/typing/bool.v | 1 - theories/typing/borrow.v | 1 - theories/typing/cont.v | 1 - theories/typing/cont_context.v | 1 - theories/typing/fixpoint.v | 12 ++++---- theories/typing/function.v | 29 +++++++----------- theories/typing/lft_contexts.v | 3 +- theories/typing/lib/arc.v | 10 +++---- theories/typing/lib/cell.v | 3 +- theories/typing/lib/diverging_static.v | 3 +- theories/typing/lib/fake_shared_box.v | 1 - theories/typing/lib/join.v | 1 - theories/typing/lib/mutex/mutex.v | 1 - theories/typing/lib/mutex/mutexguard.v | 3 +- theories/typing/lib/panic.v | 2 +- theories/typing/lib/rc/rc.v | 1 - theories/typing/lib/rc/weak.v | 1 - theories/typing/lib/refcell/ref.v | 2 +- theories/typing/lib/refcell/ref_code.v | 2 +- theories/typing/lib/refcell/refcell.v | 6 ++-- theories/typing/lib/refcell/refcell_code.v | 2 +- theories/typing/lib/refcell/refmut.v | 4 +-- theories/typing/lib/refcell/refmut_code.v | 2 +- theories/typing/lib/rwlock/rwlock.v | 18 +++++------ theories/typing/lib/rwlock/rwlock_code.v | 2 +- theories/typing/lib/rwlock/rwlockreadguard.v | 4 +-- .../typing/lib/rwlock/rwlockreadguard_code.v | 2 +- theories/typing/lib/rwlock/rwlockwriteguard.v | 6 ++-- .../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +- theories/typing/lib/spawn.v | 1 - theories/typing/lib/take_mut.v | 1 - theories/typing/own.v | 6 ++-- theories/typing/product_split.v | 1 - theories/typing/programs.v | 1 - theories/typing/shr_bor.v | 1 - theories/typing/soundness.v | 1 - theories/typing/sum.v | 7 ++--- theories/typing/type.v | 9 +++--- theories/typing/type_context.v | 1 - theories/typing/uniq_bor.v | 5 ++-- 57 files changed, 126 insertions(+), 162 deletions(-) diff --git a/opam b/opam index 510b3089..aecd02cb 100644 --- a/opam +++ b/opam @@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"] install: [make "install"] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] depends: [ - "coq-iris" { (= "dev.2018-06-23.0.a6e581d0") | (= "dev") } + "coq-iris" { (= "branch.gen_proofmode.2018-05-28.0.daeeaf05") | (= "dev") } ] diff --git a/theories/lang/heap.v b/theories/lang/heap.v index fd04e13d..94d49b2b 100644 --- a/theories/lang/heap.v +++ b/theories/lang/heap.v @@ -2,7 +2,7 @@ From Coq Require Import Min. From stdpp Require Import coPset. From iris.algebra Require Import big_op gmap frac agree. From iris.algebra Require Import csum excl auth cmra_big_op. -From iris.base_logic Require Import big_op lib.fractional. +From iris.bi Require Import fractional. From iris.base_logic Require Export lib.own. From iris.proofmode Require Export tactics. From lrust.lang Require Export lang. @@ -71,21 +71,21 @@ Instance: Params (@heap_mapsto) 4. Instance: Params (@heap_freeable) 5. Notation "l ↦{ q } v" := (heap_mapsto l q v) - (at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope. -Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope. + (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. +Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope. Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl) - (at level 20, q at level 50, format "l ↦∗{ q } vl") : uPred_scope. -Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : uPred_scope. + (at level 20, q at level 50, format "l ↦∗{ q } vl") : bi_scope. +Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope. Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I - (at level 20, q at level 50, format "l ↦∗{ q }: P") : uPred_scope. + (at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope. Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I - (at level 20, format "l ↦∗: P") : uPred_scope. + (at level 20, format "l ↦∗: P") : bi_scope. Notation "†{ q } l … n" := (heap_freeable l q n) - (at level 20, q at level 50, format "†{ q } l … n") : uPred_scope. -Notation "†l … n" := (heap_freeable l 1 n) (at level 20) : uPred_scope. + (at level 20, q at level 50, format "†{ q } l … n") : bi_scope. +Notation "†l … n" := (heap_freeable l 1 n) (at level 20) : bi_scope. Section to_heap. Implicit Types σ : state. diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v index 88394b66..86858ce8 100644 --- a/theories/lang/lib/arc.v +++ b/theories/lang/lib/arc.v @@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon. From iris.base_logic.lib Require Import invariants. From iris.program_logic Require Import weakestpre. From iris.proofmode Require Import tactics. -From iris.base_logic Require Import fractional. +From iris.bi Require Import fractional. From iris.algebra Require Import excl csum frac auth. From lrust.lang Require Import lang proofmode notation new_delete. Set Default Proof Using "Type". diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v index 9c7eb813..5371e45f 100644 --- a/theories/lang/proofmode.v +++ b/theories/lang/proofmode.v @@ -9,7 +9,7 @@ Import uPred. Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v : IntoVal e v → envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}). -Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed. +Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed. Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta]. @@ -20,7 +20,7 @@ Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ Φ : envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) → envs_entails Δ (WP fill K e1 @ E {{ Φ }}). Proof. - rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=. + rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=. rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv. Qed. @@ -45,8 +45,8 @@ Lemma tac_wp_eq_loc `{lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ : envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) → envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}). Proof. - rewrite /envs_entails=> ? /envs_lookup_sound'. rewrite sep_elim_l=> ?. - move /envs_lookup_sound'; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind. + rewrite envs_entails_eq=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?. + move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind. rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono. Qed. @@ -70,7 +70,7 @@ Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head. Lemma tac_wp_bind `{lrustG Σ} K Δ E Φ e : envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I → envs_entails Δ (WP fill K e @ E {{ Φ }}). -Proof. rewrite /envs_entails=> ->. apply: wp_bind. Qed. +Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed. Ltac wp_bind_core K := lazymatch eval hnf in K with @@ -92,7 +92,7 @@ Section heap. Context `{lrustG Σ}. Implicit Types P Q : iProp Σ. Implicit Types Φ : val → iProp Σ. -Implicit Types Δ : envs (iResUR Σ). +Implicit Types Δ : envs (uPredI (iResUR Σ)). Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ : 0 < n → @@ -103,12 +103,12 @@ Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ : envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) → envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}). Proof. - rewrite /envs_entails=> ?? HΔ. rewrite -wp_bind. + rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact:wp_alloc. - rewrite -and_sep_l. apply and_intro; first auto with I. + rewrite -persistent_and_sep. apply and_intro; first auto with I. rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l. apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc. - apply pure_elim_sep_l=> Hn. apply wand_elim_r'. + rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'. destruct (HΔ l sz) as (Δ''&?&HΔ'); first done. rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'. Qed. @@ -117,17 +117,17 @@ Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ : n = length vl → MaybeIntoLaterNEnvs 1 Δ Δ' → envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I → - envs_delete i1 false Δ' = Δ'' → + envs_delete false i1 false Δ' = Δ'' → envs_lookup i2 Δ'' = Some (false, †l…n')%I → - envs_delete i2 false Δ'' = Δ''' → + envs_delete false i2 false Δ'' = Δ''' → n' = length vl → envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) → envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}). Proof. - rewrite /envs_entails; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind. + rewrite envs_entails_eq; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind. eapply wand_apply; first exact:wp_free; simpl. rewrite into_laterN_env_sound -!later_sep; apply later_mono. - do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -assoc. + do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc. Qed. Lemma tac_wp_read K Δ Δ' E i l q v o Φ : @@ -137,7 +137,7 @@ Lemma tac_wp_read K Δ Δ' E i l q v o Φ : envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) → envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}). Proof. - rewrite /envs_entails; intros [->| ->] ???. + rewrite envs_entails_eq; intros [->| ->] ???. - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na. rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl. by apply later_mono, sep_mono_r, wand_mono. @@ -155,7 +155,7 @@ Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ : envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) → envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}). Proof. - rewrite /envs_entails; intros ? [->| ->] ????. + rewrite envs_entails_eq; intros ? [->| ->] ????. - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na. rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v index 472f29ff..3373c818 100644 --- a/theories/lifetime/at_borrow.v +++ b/theories/lifetime/at_borrow.v @@ -9,7 +9,7 @@ Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) := (∃ i, &{κ,i}P ∗ (⌜N ## lftN⌠∗ inv N (idx_bor_own 1 i) ∨ ⌜N = lftN⌠∗ inv N (∃ q, idx_bor_own q i)))%I. -Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : uPred_scope. +Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope. Section atomic_bors. Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace). diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v index f7c31e84..489ed417 100644 --- a/theories/lifetime/frac_borrow.v +++ b/theories/lifetime/frac_borrow.v @@ -1,6 +1,6 @@ From Coq Require Import Qcanon. From iris.proofmode Require Import tactics. -From iris.base_logic Require Import lib.fractional. +From iris.bi Require Import fractional. From iris.algebra Require Import frac. From lrust.lifetime Require Export at_borrow. Set Default Proof Using "Type". @@ -10,7 +10,7 @@ Class frac_borG Σ := frac_borG_inG :> inG Σ fracR. Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) := (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ'])))%I. -Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : uPred_scope. +Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope. Section frac_bor. Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ). @@ -78,7 +78,7 @@ Section frac_bor. 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φ]". + 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]". diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v index 22ba7677..735ae6d1 100644 --- a/theories/lifetime/lifetime.v +++ b/theories/lifetime/lifetime.v @@ -88,7 +88,7 @@ Lemma bor_or E κ P Q : ↑lftN ⊆ E → lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q). Proof. - iIntros (?) "#LFT H". rewrite uPred.or_alt. + iIntros (?) "#LFT H". rewrite bi.or_alt. (* The (A:=...) is needed due to Coq bug #5458 *) iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto. Qed. diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v index 488f8293..d0b5af77 100644 --- a/theories/lifetime/lifetime_sig.v +++ b/theories/lifetime/lifetime_sig.v @@ -1,7 +1,8 @@ From iris.algebra Require Import frac. From stdpp Require Export gmultiset strings. From iris.base_logic.lib Require Export invariants. -From iris.base_logic.lib Require Import boxes fractional. +From iris.base_logic.lib Require Import boxes. +From iris.bi Require Import fractional. Set Default Proof Using "Type". Definition lftN : namespace := nroot .@ "lft". @@ -36,13 +37,13 @@ Module Type lifetime_sig. (** Notation *) Notation "q .[ κ ]" := (lft_tok q κ) - (format "q .[ κ ]", at level 0) : uPred_scope. - Notation "[†κ ]" := (lft_dead κ) (format "[†κ ]"): uPred_scope. + (format "q .[ κ ]", at level 0) : bi_scope. + Notation "[†κ ]" := (lft_dead κ) (format "[†κ ]"): bi_scope. - Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope. - Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope. + Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope. + Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope. - Infix "⊑" := lft_incl (at level 70) : uPred_scope. + Infix "⊑" := lft_incl (at level 70) : bi_scope. Infix "⊓" := lft_intersect (at level 40) : stdpp_scope. Section properties. diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v index 1dbe1206..14f35f7f 100644 --- a/theories/lifetime/model/accessors.v +++ b/theories/lifetime/model/accessors.v @@ -1,7 +1,6 @@ From lrust.lifetime Require Export primitive. From iris.proofmode Require Import tactics. From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. Set Default Proof Using "Type". @@ -202,7 +201,7 @@ Proof. iLeft. iFrame "%". iExists _, _. iFrame. } iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro. iSplit; first by iApply lft_incl_refl. iExists j. iFrame. - iExists Q. rewrite -uPred.iff_refl. eauto. + iExists Q. rewrite -bi.iff_refl. eauto. + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]". iDestruct (own_bor_valid_2 with "Hinv Hbor") as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2. @@ -249,7 +248,7 @@ Proof. rewrite own_bor_op. iDestruct "Hown" as "[Hâ— Hâ—¯]". iMod ("Hclose'" with "[- Hâ—¯]"); last first. { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl. - iExists j. iFrame. iExists Q. rewrite -uPred.iff_refl. auto. } + iExists j. iFrame. iExists Q. rewrite -bi.iff_refl. auto. } iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame. iNext. rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in). diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v index 5d3f2864..8138b837 100644 --- a/theories/lifetime/model/borrow.v +++ b/theories/lifetime/model/borrow.v @@ -1,7 +1,6 @@ From lrust.lifetime Require Export primitive. From lrust.lifetime Require Export faking. From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". @@ -44,7 +43,7 @@ Proof. iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|]. iSplitL "HBâ—¯ HsliceB". + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame. - iExists P. rewrite -uPred.iff_refl. auto. + iExists P. rewrite -bi.iff_refl. auto. + clear -HE. iIntros "!> H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". iDestruct ("HIlookup" with "HI") as %Hκ. diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v index 4c8c24fb..60be506b 100644 --- a/theories/lifetime/model/borrow_sep.v +++ b/theories/lifetime/model/borrow_sep.v @@ -1,7 +1,6 @@ From lrust.lifetime Require Export primitive. From lrust.lifetime Require Export faking reborrow. From iris.algebra Require Import csum auth frac gmap agree. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". @@ -52,10 +51,10 @@ Proof. 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 κ'. iFrame "#". iExists γ1. - iFrame. iExists P. rewrite -uPred.iff_refl. auto. } + iFrame. iExists P. rewrite -bi.iff_refl. auto. } iAssert (&{κ}Q)%I with "[Hâ—¯2 Hs2]" as "$". { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2. - iFrame. iExists Q. rewrite -uPred.iff_refl. auto. } + iFrame. iExists Q. rewrite -bi.iff_refl. auto. } 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â—". diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v index 1861dd1b..00d6a80e 100644 --- a/theories/lifetime/model/creation.v +++ b/theories/lifetime/model/creation.v @@ -1,7 +1,6 @@ From lrust.lifetime Require Export primitive. From lrust.lifetime Require Import faking. From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v index 22988966..c44b0486 100644 --- a/theories/lifetime/model/definitions.v +++ b/theories/lifetime/model/definitions.v @@ -1,5 +1,4 @@ From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From lrust.lifetime Require Export lifetime_sig. Set Default Proof Using "Type". @@ -209,13 +208,13 @@ Instance raw_bor_params : Params (@raw_bor) 4. Instance bor_params : Params (@bor) 4. Notation "q .[ κ ]" := (lft_tok q κ) - (format "q .[ κ ]", at level 0) : uPred_scope. -Notation "[†κ ]" := (lft_dead κ) (format "[†κ ]"): uPred_scope. + (format "q .[ κ ]", at level 0) : bi_scope. +Notation "[†κ ]" := (lft_dead κ) (format "[†κ ]"): bi_scope. -Notation "&{ κ }" := (bor κ) (format "&{ κ }") : uPred_scope. -Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope. +Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope. +Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope. -Infix "⊑" := lft_incl (at level 70) : uPred_scope. +Infix "⊑" := lft_incl (at level 70) : bi_scope. (* TODO: Making all these things opaque is rather annoying, we should find a way to avoid it, or *at least*, to avoid having to manually unfold diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v index dfb8359c..c00558ab 100644 --- a/theories/lifetime/model/faking.v +++ b/theories/lifetime/model/faking.v @@ -1,6 +1,5 @@ From lrust.lifetime Require Export primitive. From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". @@ -89,7 +88,7 @@ Proof. by do 2 eapply lookup_to_gmap_None. } rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯". - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame. - - iExists γ. iFrame. iExists P. rewrite -uPred.iff_refl. eauto. + - iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto. Qed. Lemma raw_bor_fake' E κ P : diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v index 629093d7..038aa8d1 100644 --- a/theories/lifetime/model/primitive.v +++ b/theories/lifetime/model/primitive.v @@ -1,7 +1,7 @@ From lrust.lifetime.model Require Export definitions. -From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. -From iris.base_logic.lib Require Import boxes fractional. +From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classes. +From iris.base_logic.lib Require Import boxes. +From iris.bi Require Import fractional. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". Import uPred. @@ -70,9 +70,9 @@ Proof. iExists γs. iSplit. done. rewrite own_op; iFrame. Qed. Global Instance own_bor_into_op κ x x1 x2 : - IsOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2). + IsOp x x1 x2 → IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2). Proof. - rewrite /IsOp /IntoAnd=>->. by rewrite -own_bor_op. + rewrite /IsOp /IntoSep=>-> /=. by rewrite -own_bor_op. Qed. Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x. Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed. @@ -104,9 +104,9 @@ Proof. iExists γs. iSplit; first done. rewrite own_op; iFrame. Qed. Global Instance own_cnt_into_op κ x x1 x2 : - IsOp x x1 x2 → IntoAnd false (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2). + IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2). Proof. - rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_cnt_op. + rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op. Qed. Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x. Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed. @@ -138,9 +138,9 @@ Proof. iExists γs. iSplit. done. rewrite own_op; iFrame. Qed. Global Instance own_inh_into_op κ x x1 x2 : - IsOp x x1 x2 → IntoAnd false (own_inh κ x) (own_inh κ x1) (own_inh κ x2). + IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2). Proof. - rewrite /IsOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_inh_op. + rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op. Qed. Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x. Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed. @@ -275,7 +275,7 @@ Qed. 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"=> //. + iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //. iDestruct (own_valid_2 with "H H'") as %Hvalid. move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid. Qed. diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v index f73146de..5187975f 100644 --- a/theories/lifetime/model/reborrow.v +++ b/theories/lifetime/model/reborrow.v @@ -1,6 +1,5 @@ From lrust.lifetime Require Import borrow accessors. From iris.algebra Require Import csum auth frac gmap agree gset. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import boxes. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". @@ -61,7 +60,7 @@ Proof. (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done. rewrite /to_borUR lookup_fmap. by rewrite HBj. } iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj". - { iExists j. iFrame. iExists P. rewrite -uPred.iff_refl. auto. } + { iExists j. iFrame. iExists P. rewrite -bi.iff_refl. auto. } iSplitL "Hbox HBâ— HB". { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B). rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame. diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v index bac68ad6..41551687 100644 --- a/theories/lifetime/na_borrow.v +++ b/theories/lifetime/na_borrow.v @@ -8,7 +8,7 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ} (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I. Notation "&na{ κ , tid , N }" := (na_bor κ tid N) - (format "&na{ κ , tid , N }") : uPred_scope. + (format "&na{ κ , tid , N }") : bi_scope. Section na_bor. Context `{invG Σ, lftG Σ, na_invG Σ} diff --git a/theories/typing/bool.v b/theories/typing/bool.v index 08784b1a..4a4d6a15 100644 --- a/theories/typing/bool.v +++ b/theories/typing/bool.v @@ -1,4 +1,3 @@ -From iris.base_logic Require Import big_op. From iris.proofmode Require Import tactics. From lrust.typing Require Export type. From lrust.typing Require Import programs. diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v index 680dca38..6ab60442 100644 --- a/theories/typing/borrow.v +++ b/theories/typing/borrow.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang Require Import proofmode. From lrust.typing Require Export uniq_bor shr_bor own. From lrust.typing Require Import lft_contexts type_context programs. diff --git a/theories/typing/cont.v b/theories/typing/cont.v index c25ab6b1..02ef7650 100644 --- a/theories/typing/cont.v +++ b/theories/typing/cont.v @@ -1,4 +1,3 @@ -From iris.base_logic Require Import big_op. From iris.proofmode Require Import tactics. From lrust.typing Require Export type. From lrust.typing Require Import programs. diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v index 0dac90df..a86297a4 100644 --- a/theories/typing/cont_context.v +++ b/theories/typing/cont_context.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang Require Import notation. From lrust.typing Require Import type lft_contexts type_context. Set Default Proof Using "Type". diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v index fb89f3fa..f93012b0 100644 --- a/theories/typing/fixpoint.v +++ b/theories/typing/fixpoint.v @@ -60,8 +60,8 @@ Section fixpoint. eapply (limit_preserving_ext (λ _, _ ∧ _)). { split; (intros [H1 H2]; split; [apply H1|apply H2]). } apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?). - + apply uPred.limit_preserving_Persistent; solve_proper. - + apply limit_preserving_impl, uPred.limit_preserving_entails; + + apply bi.limit_preserving_Persistent; solve_proper. + + apply limit_preserving_impl, bi.limit_preserving_entails; solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv). Qed. @@ -74,7 +74,7 @@ Section fixpoint. - exists bool. apply _. - done. - repeat (apply limit_preserving_forall=> ?). - apply uPred.limit_preserving_entails; solve_proper. + apply bi.limit_preserving_entails; solve_proper. Qed. Global Instance fixpoint_sync : @@ -86,7 +86,7 @@ Section fixpoint. - exists bool. apply _. - done. - repeat (apply limit_preserving_forall=> ?). - apply uPred.limit_preserving_entails; solve_proper. + apply bi.limit_preserving_entails; solve_proper. Qed. Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)). @@ -111,7 +111,7 @@ Section subtyping. - by eexists _. - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12. - repeat (apply limit_preserving_forall=> ?). - apply uPred.limit_preserving_entails; solve_proper. + apply bi.limit_preserving_entails; solve_proper. Qed. Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} : @@ -124,7 +124,7 @@ Section subtyping. - by eexists _. - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12. - apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?); - apply uPred.limit_preserving_entails; solve_proper. + apply bi.limit_preserving_entails; solve_proper. Qed. Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} : diff --git a/theories/typing/function.v b/theories/typing/function.v index 69362f45..06b711f5 100644 --- a/theories/typing/function.v +++ b/theories/typing/function.v @@ -1,6 +1,5 @@ -From iris.base_logic Require Import big_op. From iris.proofmode Require Import tactics. -From iris.algebra Require Import vector. +From iris.algebra Require Import vector list. From lrust.typing Require Export type. From lrust.typing Require Import own programs cont. Set Default Proof Using "Type". @@ -88,23 +87,17 @@ Section fn. do 5 f_equiv. apply type_dist2_dist. apply Hfp. - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv. cut (∀ n tid p i, Proper (dist n ==> dist n) - (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌠→ tctx_elt_interp tid (p â— ty))%I). + (λ (l : list type), + match l !! i with + | Some ty => tctx_elt_interp tid (p â— ty) | None => emp + end)%I). { intros Hprop. apply Hprop, list_fmap_ne; last first. - symmetry. eapply Forall2_impl; first apply Hfp. intros. apply dist_later_dist, type_dist2_dist_later. done. - apply _. } - clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy. - specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|]; - inversion_clear Hxy; last done. - transitivity (tctx_elt_interp tid (p â— tyx)); - last transitivity (tctx_elt_interp tid (p â— tyy)); last 2 first. - + unfold tctx_elt_interp. do 3 f_equiv. by apply ty_own_ne. - + apply equiv_dist. iSplit. - * iIntros "H * #EQ". by iDestruct "EQ" as %[=->]. - * iIntros "H". by iApply "H". - + apply equiv_dist. iSplit. - * iIntros "H". by iApply "H". - * iIntros "H * #EQ". by iDestruct "EQ" as %[=->]. + clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i). + case _ : (x !! i)=>[tyx|]; case _ : (y !! i)=>[tyy|]; + inversion_clear 1; [solve_proper|done]. Qed. Global Instance fn_ne n' : @@ -191,15 +184,15 @@ Section typing. -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length // -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length // !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap. - iApply big_sepL_impl. iSplit; last done. iIntros "{HT Hty}!#". + iApply (big_sepL_impl with "HT"). iIntros "!#". iIntros (i [p [ty1' ty2']]) "#Hzip H /=". iDestruct "H" as (v) "[? Hown]". iExists v. iFrame. rewrite !lookup_zip_with. iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 & (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some. - iDestruct (big_sepL_lookup with "Htys") as "#Hty". + iDestruct (big_sepL_lookup with "Htys") as "#Hty'". { rewrite lookup_zip_with /=. erewrite Hty'2. simpl. by erewrite Hty'1. } - iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)". + iDestruct (box_type_incl with "[$Hty']") as "(_ & #Hincl & _)". by iApply "Hincl". Qed. diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v index d1506438..12913694 100644 --- a/theories/typing/lft_contexts.v +++ b/theories/typing/lft_contexts.v @@ -1,6 +1,5 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. -From iris.base_logic.lib Require Import fractional. +From iris.bi Require Import fractional. From lrust.lang Require Import proofmode. From lrust.typing Require Export base. From lrust.lifetime Require Import frac_borrow. diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v index ce484f17..fcd2e370 100644 --- a/theories/typing/lib/arc.v +++ b/theories/typing/lib/arc.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lang.lib Require Import memcpy arc. From lrust.lifetime Require Import at_borrow. From lrust.typing Require Export type. @@ -203,7 +203,7 @@ Section arc. Proof. intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=. unfold full_arc_own, shared_arc_own. - repeat (apply send_change_tid || apply uPred.exist_mono || + repeat (apply send_change_tid || apply bi.exist_mono || (apply arc_persist_send; apply _) || f_equiv || intros ?). Qed. @@ -211,7 +211,7 @@ Section arc. Send ty → Sync ty → Sync (arc ty). Proof. intros Hse Hsy ν tid tid' l. - repeat (apply send_change_tid || apply uPred.exist_mono || + repeat (apply send_change_tid || apply bi.exist_mono || (apply arc_persist_send; apply _) || f_equiv || intros ?). Qed. @@ -311,7 +311,7 @@ Section arc. Send ty → Sync ty → Send (weak ty). Proof. intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=. - repeat (apply send_change_tid || apply uPred.exist_mono || + repeat (apply send_change_tid || apply bi.exist_mono || (apply arc_persist_send; apply _) || f_equiv || intros ?). Qed. @@ -319,7 +319,7 @@ Section arc. Send ty → Sync ty → Sync (weak ty). Proof. intros Hse Hsy ν tid tid' l. - repeat (apply send_change_tid || apply uPred.exist_mono || + repeat (apply send_change_tid || apply bi.exist_mono || (apply arc_persist_send; apply _) || f_equiv || intros ?). Qed. diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v index 4afcfed7..dea59d49 100644 --- a/theories/typing/lib/cell.v +++ b/theories/typing/lib/cell.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. @@ -40,7 +39,7 @@ Section cell. iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)". iSplit; [done|iSplit; iIntros "!# * H"]. - iApply ("Hown" with "H"). - - iApply na_bor_iff; last done. iSplit; iIntros "!>!# H"; + - iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown". Qed. Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2). diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v index 6926982a..b07fdb62 100644 --- a/theories/typing/lib/diverging_static.v +++ b/theories/typing/lib/diverging_static.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.typing Require Export type. From lrust.typing Require Import typing. Set Default Proof Using "Type". @@ -23,7 +22,7 @@ Section diverging_static. (* F : FnOnce(&'static T), as witnessed by the impl call_once *) typed_val call_once (fn(∅; F, &shr{static} T) → unit) → typed_val (diverging_static_loop call_once) - (fn(∀ α, λ Ï, T.(ty_outlives_E) static; &shr{α} T, F) → emp). + (fn(∀ α, λ Ï, T.(ty_outlives_E) static; &shr{α} T, F) → ∅). Proof. intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret arg). inv_vec arg=>x f. simpl_subst. diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v index 35c849e5..d6cb31f4 100644 --- a/theories/typing/lib/fake_shared_box.v +++ b/theories/typing/lib/fake_shared_box.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.typing Require Import typing. Set Default Proof Using "Type". diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v index b11f27ef..f1df0427 100644 --- a/theories/typing/lib/join.v +++ b/theories/typing/lib/join.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang Require Import spawn. From lrust.typing Require Export type. From lrust.typing Require Import typing. diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v index 58e43755..e1935d62 100644 --- a/theories/typing/lib/mutex/mutex.v +++ b/theories/typing/lib/mutex/mutex.v @@ -1,7 +1,6 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy lock. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v index 507f88e0..be34421c 100644 --- a/theories/typing/lib/mutex/mutexguard.v +++ b/theories/typing/lib/mutex/mutexguard.v @@ -1,7 +1,6 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy lock. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. @@ -122,7 +121,7 @@ Section mguard. Global Instance mutexguard_sync α ty : Sync ty → Sync (mutexguard α ty). Proof. - move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv. + move=>?????/=. apply bi.exist_mono=>?. do 7 f_equiv. by rewrite sync_change_tid. Qed. diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v index a827be9c..5296c6c4 100644 --- a/theories/typing/lib/panic.v +++ b/theories/typing/lib/panic.v @@ -16,7 +16,7 @@ Section panic. Definition panic : val := funrec: <> [] := #☠. - Lemma panic_type : typed_val panic (fn(∅) → emp). + Lemma panic_type : typed_val panic (fn(∅) → ∅). Proof. intros E L. iApply type_fn; [done|]. iIntros "!# *". inv_vec args. iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst. diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index 2ab6d344..25061bdd 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -1,7 +1,6 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v index 291c57a7..311caf7e 100644 --- a/theories/typing/lib/rc/weak.v +++ b/theories/typing/lib/rc/weak.v @@ -1,7 +1,6 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v index d5307a39..57404623 100644 --- a/theories/typing/lib/refcell/ref.v +++ b/theories/typing/lib/refcell/ref.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.refcell Require Import refcell. diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v index b37cfeb5..f70befa8 100644 --- a/theories/typing/lib/refcell/ref_code.v +++ b/theories/typing/lib/refcell/ref_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import lifetime na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.refcell Require Import refcell ref. diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v index efdb9d10..7223ac08 100644 --- a/theories/typing/lib/refcell/refcell.v +++ b/theories/typing/lib/refcell/refcell.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing. Set Default Proof Using "Type". @@ -75,7 +75,7 @@ Section refcell_inv. iAssert (â–¡ (&{α}((l +â‚— 1) ↦∗: ty_own ty1 tid) -∗ &{α}((l +â‚— 1) ↦∗: ty_own ty2 tid)))%I as "#Hb". { iIntros "!# H". iApply bor_iff; last done. - iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl; + iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl; iFrame; by iApply "Hown". } iDestruct "H" as (st) "H"; iExists st; iDestruct "H" as "($&$&H)"; destruct st as [[agν st]|]; try done; @@ -184,7 +184,7 @@ Section refcell. - iPureIntro. simpl. congruence. - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown". - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame. - iApply na_bor_iff; last done. iSplit; iIntros "!>!# H". + iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1". Qed. Lemma refcell_mono' E L ty1 ty2 : diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v index b5c99421..a571826a 100644 --- a/theories/typing/lib/refcell/refcell_code.v +++ b/theories/typing/lib/refcell/refcell_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing option. diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v index f9a2ec91..790cdcec 100644 --- a/theories/typing/lib/refcell/refmut.v +++ b/theories/typing/lib/refcell/refmut.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing util. From lrust.typing.lib.refcell Require Import refcell. @@ -93,7 +93,7 @@ Section refmut. iExists ν, γ, β, ty'. iFrame "∗#". iSplit. + iApply bor_shorten; last iApply bor_iff; last done. * iApply lft_intersect_mono; first done. iApply lft_incl_refl. - * iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]"; + * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Ho". + by iApply lft_incl_trans. - iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc. diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v index e2f0360b..443129c2 100644 --- a/theories/typing/lib/refcell/refmut_code.v +++ b/theories/typing/lib/refcell/refmut_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.refcell Require Import refcell refmut. diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v index 67d1092e..2ee4f34a 100644 --- a/theories/typing/lib/rwlock/rwlock.v +++ b/theories/typing/lib/rwlock/rwlock.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import at_borrow. From lrust.typing Require Import typing. Set Default Proof Using "Type". @@ -71,7 +71,7 @@ Section rwlock_inv. iAssert (â–¡ (&{α}((l +â‚— 1) ↦∗: ty_own ty1 tid) -∗ &{α}((l +â‚— 1) ↦∗: ty_own ty2 tid)))%I as "#Hb". { iIntros "!# H". iApply bor_iff; last done. - iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl; + iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl; iFrame; by iApply "Hown". } iDestruct "H" as (st) "H"; iExists st; iDestruct "H" as "($&$&H)"; destruct st as [[|[[agν ?]?]|]|]; try done; @@ -177,7 +177,7 @@ Section rwlock. - iPureIntro. simpl. congruence. - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown". - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame. - iApply at_bor_iff; last done. iSplit; iIntros "!>!# H". + iApply at_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1". Qed. Lemma rwlock_mono' E L ty1 ty2 : @@ -198,12 +198,12 @@ Section rwlock. Global Instance rwlock_sync : Send ty → Sync ty → Sync (rwlock ty). Proof. - move=>???????/=. do 2 apply uPred.exist_mono=>?. apply uPred.sep_mono_r. - iApply at_bor_iff. iIntros "!> !#". iApply uPred.equiv_iff. - apply uPred.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv. - - do 5 f_equiv. apply uPred.equiv_spec; split; iApply send_change_tid. - - apply uPred.equiv_spec; split; iApply sync_change_tid. - - apply uPred.equiv_spec; split; iApply send_change_tid. + move=>???????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r. + iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff. + apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv. + - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid. + - apply bi.equiv_spec; split; iApply sync_change_tid. + - apply bi.equiv_spec; split; iApply send_change_tid. Qed. End rwlock. diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v index 130dff9e..22876856 100644 --- a/theories/typing/lib/rwlock/rwlock_code.v +++ b/theories/typing/lib/rwlock/rwlock_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing option. diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v index 1b0ffdc5..45ef6012 100644 --- a/theories/typing/lib/rwlock/rwlockreadguard.v +++ b/theories/typing/lib/rwlock/rwlockreadguard.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.rwlock Require Import rwlock. @@ -117,7 +117,7 @@ Section rwlockreadguard. Global Instance rwlockreadguard_sync α ty : Sync ty → Sync (rwlockreadguard α ty). Proof. - move=>?????/=. apply uPred.exist_mono=>?. by rewrite sync_change_tid. + move=>?????/=. apply bi.exist_mono=>?. by rewrite sync_change_tid. Qed. (* POSIX requires the unlock to occur from the thread that acquired diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v index 5bfcaccd..c0e61e1b 100644 --- a/theories/typing/lib/rwlock/rwlockreadguard_code.v +++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import lifetime na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard. diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v index efb27daa..b3a1b5b8 100644 --- a/theories/typing/lib/rwlock/rwlockwriteguard.v +++ b/theories/typing/lib/rwlock/rwlockwriteguard.v @@ -1,6 +1,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import util typing. From lrust.typing.lib.rwlock Require Import rwlock. @@ -87,7 +87,7 @@ Section rwlockwriteguard. iDestruct "H" as (γ β) "(Hb & #H⊑ & #Hinv & Hown)". iExists γ, β. iFrame "∗#". iSplit; last iSplit. + iApply bor_iff; last done. - iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]"; + iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Ho". + by iApply lft_incl_trans. + iApply at_bor_iff; try done. @@ -120,7 +120,7 @@ Section rwlockwriteguard. Global Instance rwlockwriteguard_sync α ty : Sync ty → Sync (rwlockwriteguard α ty). Proof. - move=>?????/=. apply uPred.exist_mono=>?. do 6 f_equiv. + move=>?????/=. apply bi.exist_mono=>?. do 7 f_equiv. by rewrite sync_change_tid. Qed. diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v index 50928962..9b15a6c8 100644 --- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v +++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v @@ -1,7 +1,7 @@ From Coq.QArith Require Import Qcanon. From iris.proofmode Require Import tactics. From iris.algebra Require Import auth csum frac agree. -From iris.base_logic Require Import big_op fractional. +From iris.bi Require Import fractional. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Import typing. From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard. diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v index c9a91819..32d51df5 100644 --- a/theories/typing/lib/spawn.v +++ b/theories/typing/lib/spawn.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang Require Import spawn. From lrust.typing Require Export type. From lrust.typing Require Import typing. diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v index 8d9b75a9..2e075ad5 100644 --- a/theories/typing/lib/take_mut.v +++ b/theories/typing/lib/take_mut.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import memcpy. From lrust.lifetime Require Import na_borrow. From lrust.typing Require Export type. diff --git a/theories/typing/own.v b/theories/typing/own.v index 05fa25c2..d1cfa6ae 100644 --- a/theories/typing/own.v +++ b/theories/typing/own.v @@ -1,6 +1,5 @@ From Coq Require Import Qcanon. From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang.lib Require Import new_delete memcpy. From lrust.typing Require Export type. From lrust.typing Require Import util uninit type_context programs. @@ -57,7 +56,7 @@ Section own. Since this assertion is timeless, this should not cause problems. *) - â–· l ↦∗: ty.(ty_own) tid ∗ â–· freeable_sz n ty.(ty_size) l + â–· (l ↦∗: ty.(ty_own) tid ∗ freeable_sz n ty.(ty_size) l) | _ => False end%I; ty_shr κ tid l := @@ -72,6 +71,7 @@ Section own. destruct vl as [|[[|l'|]|][]]; try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj). iFrame. iExists l'. rewrite heap_mapsto_vec_singleton. + rewrite bi.later_sep. 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. iApply delay_sharing_later; done. @@ -203,7 +203,7 @@ Section util. (own_ptr n (uninit m)).(ty_own) tid [v] ⊣⊢ ∃ (l : loc) (vl' : vec val m), ⌜v = #l⌠∗ â–· l ↦∗ vl' ∗ â–· freeable_sz n m l. Proof. - rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit. + rewrite ownptr_own. apply bi.exist_proper=>l. iSplit. (* FIXME: The goals here look rather confusing: One cannot tell that we are looking at a statement in Iris; the top-level → could just as well be a Coq implication. *) - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v. diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v index 525c039c..8130c5ae 100644 --- a/theories/typing/product_split.v +++ b/theories/typing/product_split.v @@ -1,6 +1,5 @@ From Coq Require Import Qcanon. From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.typing Require Export type. From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor. Set Default Proof Using "Type". diff --git a/theories/typing/programs.v b/theories/typing/programs.v index 755256c0..5a298fa4 100644 --- a/theories/typing/programs.v +++ b/theories/typing/programs.v @@ -1,4 +1,3 @@ -From iris.base_logic Require Import big_op. From lrust.lang Require Import proofmode memcpy. From lrust.typing Require Export type lft_contexts type_context cont_context. Set Default Proof Using "Type". diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v index 3d4bfc70..7d836353 100644 --- a/theories/typing/shr_bor.v +++ b/theories/typing/shr_bor.v @@ -1,4 +1,3 @@ -From iris.base_logic Require Import big_op. From iris.proofmode Require Import tactics. From lrust.typing Require Export type. From lrust.typing Require Import lft_contexts type_context programs. diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v index cc98e8b4..e35c3b50 100644 --- a/theories/typing/soundness.v +++ b/theories/typing/soundness.v @@ -1,5 +1,4 @@ From iris.algebra Require Import frac. -From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Import na_invariants. From iris.proofmode Require Import tactics. From lrust.lang Require Import races adequacy proofmode notation. diff --git a/theories/typing/sum.v b/theories/typing/sum.v index 107c3b04..c7915072 100644 --- a/theories/typing/sum.v +++ b/theories/typing/sum.v @@ -1,7 +1,6 @@ -From iris.base_logic Require Import big_op. From iris.proofmode Require Import tactics. From iris.algebra Require Import list. -From iris.base_logic Require Import fractional. +From iris.bi Require Import fractional. From lrust.typing Require Export type. Set Default Proof Using "Type". @@ -231,9 +230,9 @@ Section sum. iIntros (????) "[]". Qed. - Definition emp := sum []. + Definition emp_type := sum []. - Global Instance emp_empty : Empty type := emp. + Global Instance emp_type_empty : Empty type := emp_type. End sum. (* Σ is commonly used for the current functor. So it cannot be defined diff --git a/theories/typing/type.v b/theories/typing/type.v index 34fb8dd9..7dd9169b 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -1,5 +1,4 @@ From iris.base_logic.lib Require Export na_invariants. -From iris.base_logic Require Import big_op. From lrust.lang Require Export proofmode notation. From lrust.lifetime Require Export frac_borrow. From lrust.typing Require Export base. @@ -215,10 +214,10 @@ Section ofe. - by intros []. - (* TODO: automate this *) repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?). - + apply uPred.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty. - + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty. - + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty. - + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty. + + apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty. + + apply bi.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty. + + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty. + + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty. Qed. Inductive st_equiv' (ty1 ty2 : simple_type) : Prop := diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v index aa879676..6b3e7e72 100644 --- a/theories/typing/type_context.v +++ b/theories/typing/type_context.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.typing Require Import type lft_contexts. Set Default Proof Using "Type". diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v index ec9013bd..eb07fa95 100644 --- a/theories/typing/uniq_bor.v +++ b/theories/typing/uniq_bor.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics. -From iris.base_logic Require Import big_op. From lrust.lang Require Import heap. From lrust.typing Require Export type. From lrust.typing Require Import util lft_contexts type_context programs. @@ -55,7 +54,7 @@ Section uniq_bor. iSpecialize ("Hκ" with "HE"). iSplit; iAlways. - iIntros (? [|[[]|][]]) "H"; try done. iApply (bor_shorten with "Hκ"). iApply bor_iff; last done. - iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]"; + iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Ho". - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'". { iApply lft_intersect_mono. done. iApply lft_incl_refl. } @@ -82,7 +81,7 @@ Section uniq_bor. Send ty → Send (uniq_bor κ ty). Proof. iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done. - iApply bor_iff; last done. iNext. iAlways. iApply uPred.equiv_iff. + iApply bor_iff; last done. iNext. iAlways. iApply bi.equiv_iff. do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend. Qed. -- GitLab