From 0b58a0c8f691ac8815ed6618e83a6efb3b0dd2ee Mon Sep 17 00:00:00 2001 From: Hoang-Hai Dang Date: Fri, 24 May 2019 15:19:57 +0200 Subject: [PATCH] Bump Iris (changes in auth) --- opam | 2 +- theories/algebra/ufrac_auth.v | 26 +++++++++++++++--------- theories/heap_lang/adequacy.v | 10 ++++----- theories/heap_lang/heap.v | 4 ++-- theories/heap_lang/lib/queue.v | 7 ++++--- theories/heap_lang/lib/spin_lock_track.v | 8 ++++---- theories/iron_logic/fcinv.v | 2 +- 7 files changed, 33 insertions(+), 26 deletions(-) diff --git a/opam b/opam index 338be66..bdfb5bd 100644 --- a/opam +++ b/opam @@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] install: [make "install"] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] depends: [ - "coq-iris" { (= "dev.2019-05-09.1.d0daa181") | (= "dev") } + "coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") } ] diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v index 6731d1f..0e8271b 100644 --- a/theories/algebra/ufrac_auth.v +++ b/theories/algebra/ufrac_auth.v @@ -53,21 +53,27 @@ Section ufrac_auth. Proof. solve_proper. Qed. Global Instance ufrac_auth_auth_discrete a : Discrete a → Discrete (●?{q} a). - Proof. intros; apply Auth_discrete; apply _. Qed. + Proof. + intros; apply (@auth_auth_discrete (optionUR (prodR fracR A))); + [apply Some_discrete|]; apply _. + Qed. Global Instance ufrac_auth_frag_discrete a : Discrete a → Discrete (◯?{q} a). - Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed. + Proof. + intros; apply (@auth_frag_discrete (optionUR (prodR fracR A))), Some_discrete; + apply _. + Qed. Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●?{p} a ⋅ ◯?{p} a). - Proof. done. Qed. + Proof. by rewrite auth_both_validN. Qed. Lemma ufrac_auth_valid p a : ✓ a → ✓ (●?{p} a ⋅ ◯?{p} a). - Proof. done. Qed. + Proof. intros. by apply (@auth_both_valid_2 (optionUR (prodR ufracR A))). Qed. Lemma ufrac_auth_agreeN n p a b : ✓{n} (●?{p} a ⋅ ◯?{p} b) → a ≡{n}≡ b. Proof. - rewrite auth_validN_eq /= => -[Hincl Hvalid]. - move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]]. - move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=]. + rewrite auth_both_validN => -[Hincl Hvalid]. + move: Hincl=> /Some_includedN=> -[[//]|[[[p' ?] ?] [/=]]]. + rewrite ufrac_op'=> [/Qp_eq/=]. rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst. Qed. Lemma ufrac_auth_agree p a b : ✓ (●?{p} a ⋅ ◯?{p} b) → a ≡ b. @@ -78,10 +84,10 @@ Section ufrac_auth. Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed. Lemma ufrac_auth_includedN n p q a b : ✓{n} (●?{p} a ⋅ ◯?{q} b) → Some b ≼{n} Some a. - Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed. + Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed. Lemma ufrac_auth_included `{CmraDiscrete A} q p a b : ✓ (●?{p} a ⋅ ◯?{q} b) → Some b ≼ Some a. - Proof. rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _] //. Qed. + Proof. rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _] //. Qed. Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b : ✓{n} (●?{p} a ⋅ ◯?{q} b) → b ≼{n} a. Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed. @@ -91,7 +97,7 @@ Section ufrac_auth. Lemma ufrac_auth_auth_validN n q a : ✓{n} (●?{q} a) ↔ ✓{n} a. Proof. - split; [by intros [_ [??]]|]. + rewrite -auth_auth_validN. split; [by intros []|]. repeat split; simpl; by try apply: ucmra_unit_leastN. Qed. Lemma ufrac_auth_auth_valid q a : ✓ (●?{q} a) ↔ ✓ a. diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v index c008ea7..08c788a 100644 --- a/theories/heap_lang/adequacy.v +++ b/theories/heap_lang/adequacy.v @@ -4,7 +4,7 @@ in [iron_logic/adequacy]. Note, we only state adequacy for the lifted logic, because in the Coq formalization we state all specifications in terms of the lifted logic. *) -From iris.algebra Require Import big_op gmap ufrac. +From iris.algebra Require Import big_op gmap ufrac excl. From iron.iron_logic Require Export weakestpre adequacy. From iron.algebra Require Import ufrac_auth. From iron.heap_lang Require Import heap. @@ -37,7 +37,7 @@ Proof. iMod (own_alloc (●?{1} ∅ ⋅ (◯?{1/2} ∅ ⋅ ◯?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]". { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. by apply ufrac_auth_valid. } - iMod (own_alloc (● ∅)) as (γf) "Hf"; first done. + iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iFrame "Hp". iSplitL "Hσ Hf". @@ -55,7 +55,7 @@ Proof. (◯?{1/2} (to_heap σ) ⋅ ◯?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]". { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. apply ufrac_auth_valid; by apply to_heap_valid. } - iMod (own_alloc (● ∅)) as (γf) "Hf"; first done. + iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iFrame "Hp". iSplitL "Hσ Hf". @@ -98,7 +98,7 @@ Proof. - intros Hwp Hsteps. eapply (iron_wp_all_adequacy _ heap_lang _ _ ∅ σ2' _ _ (λ _, σ2' = σ2) _ ε); [|done]; iIntros (? κs) "". - iMod (own_alloc (● ∅)) as (γf) "Hf"; first done. + iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. iMod (own_alloc (●?{1} (to_heap ∅) ⋅ (◯?{1/2} (to_heap ∅) ⋅ ◯?{1/2} ε))) as (γ) "[Hσ [Hσ' Hp]]". { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. @@ -123,7 +123,7 @@ Proof. - intros Hwp Hsteps. eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _ (Some (1 / 2)%Qp)); [|done]; iIntros (? κs) "". - iMod (own_alloc (● ∅)) as (γf) "Hf"; first done. + iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. iMod (own_alloc (●?{1} (to_heap σ1) ⋅ (◯?{1/2} (to_heap σ1) ⋅ ◯?{1/2} ε))) as (γ) "[Hσ [Hσ' Hp]]". { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. diff --git a/theories/heap_lang/heap.v b/theories/heap_lang/heap.v index 6eaeed0..ff41e50 100644 --- a/theories/heap_lang/heap.v +++ b/theories/heap_lang/heap.v @@ -1,7 +1,7 @@ (** This file defines the basic points-to [↦] connectives for the Iron logic instantiated with the heap_lang language. As a counter part to this, it defines the state interpretation [heap_ctx]. *) -From iris.algebra Require Import frac_auth gmap agree gmultiset ufrac. +From iris.algebra Require Import excl frac_auth gmap agree gmultiset ufrac. From iris.base_logic.lib Require Export own. From iris.bi.lib Require Import fractional. From iris.proofmode Require Import tactics. @@ -242,7 +242,7 @@ Section heap. iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]". iAssert ⌜ πfs !! j = Some π ⌝%I as %Hj. { iDestruct (own_valid_2 with "Hn Hj") - as %[Hj%singleton_included Hvalid]%auth_valid_discrete_2. + as %[Hj%singleton_included Hvalid]%auth_both_valid. destruct Hj as (eπ'&Hj%leibniz_equiv&[[=]|(?&?&[= <-]&[= <-]&Heπ)]%option_included). destruct Heπ as [<-%leibniz_equiv|Hincl]; last first. { exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //. diff --git a/theories/heap_lang/lib/queue.v b/theories/heap_lang/lib/queue.v index 3cc3e76..12c873e 100644 --- a/theories/heap_lang/lib/queue.v +++ b/theories/heap_lang/lib/queue.v @@ -212,7 +212,8 @@ Section queue_spec. iDestruct "Hlhptr" as "[Hlhptr Hlhptr']". iMod (own_alloc (1%Qp, to_agree [])) as (γ) "[Hγ Hγ']"; first done. iMod (own_alloc (Excl ())) as (γd) "Hγd"; first done. - iMod (own_alloc (● (Excl' l) ⋅ ◯ (Excl' l))) as (γe) "[Hγe Hγe']"; first done. + iMod (own_alloc (● (Excl' l) ⋅ ◯ (Excl' l))) as (γe) "[Hγe Hγe']"; + first by apply auth_both_valid. iMod (fcinv_alloc_named _ N (λ γinv, queue_inv (QueueName γinv γ γd γe) lhptr ltptr) with "[Hlhptr' Hγ' Hl Hγe]") as (γinv) "([Hγinv Hγinv']&Hγc&#?)". { iIntros "!>" (γinv). @@ -293,7 +294,7 @@ Section queue_spec. iMod (fcinv_open _ N with "[$] Hγinv") as "[H Hclose]"; first done. iDestruct "H" as (lh lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt')". iDestruct (own_valid_2 with "Hγe Hγe'") - as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. iMod (own_update_2 with "Hγe Hγe'") as "[Hγe Hγe']". { by apply auth_update, option_local_update, (exclusive_local_update _ (Excl ltn)). } @@ -326,7 +327,7 @@ Section queue_spec. iMod (fcinv_cancel with "[$] Hγc [$Hγinv $Hγinv']") as "H"; first done. iDestruct "H" as (lh lt' vs) "(>Hvs' & >Hlhptr' & >Hγe & Hlist & >Hlt)". iDestruct (own_valid_2 with "Hγe Hγe'") - as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. iDestruct "Hlhptr" as (v') "Hlhptr". iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %?; simplify_eq. iCombine "Hlhptr Hlhptr'" as "Hlhptr". diff --git a/theories/heap_lang/lib/spin_lock_track.v b/theories/heap_lang/lib/spin_lock_track.v index a633351..f3ddfaf 100644 --- a/theories/heap_lang/lib/spin_lock_track.v +++ b/theories/heap_lang/lib/spin_lock_track.v @@ -10,7 +10,7 @@ From iron.iron_logic Require Export weakestpre. From iron.heap_lang Require Export lang adequacy. From iron.heap_lang Require Import proofmode notation. From iron.iron_logic Require Import fcinv. -From iris.algebra Require Import auth. +From iris.algebra Require Import auth excl. Set Default Proof Using "Type". Definition new_lock : val := λ: <>, ref #false. @@ -97,7 +97,7 @@ Section proof. Proof. iIntros (Φ) "HR HΦ". rewrite -iron_wp_fupd /new_lock /=. wp_lam. wp_alloc l as "Hl". - iMod (own_alloc (● None)) as (γ) "Hγ"; first done. + iMod (own_alloc (● None)) as (γ) "Hγ"; first by apply auth_auth_valid. iMod (fcinv_alloc_named _ N (λ γinv, lock_inv (LockName γinv γ) l R) with "[-HΦ]") as (γinv) "(Hγ & Hγc & #?)". { iIntros "!>" (γinv). iExists false. by iFrame. } @@ -143,7 +143,7 @@ Section proof. iDestruct "Hinv" as ([|]) "[Hl Hinv]". - wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv]". iDestruct (own_valid_2 with "Hγ Hγf") - as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. + as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid. iMod (own_update_2 with "Hγ Hγf") as "Hγ". { eapply auth_update_dealloc, delete_option_local_update; apply _. } iMod ("Hclose" with "[HR Hl Hγ]"). @@ -151,7 +151,7 @@ Section proof. iApply "HΦ". iModIntro. by iFrame. - iDestruct "Hinv" as "[>Hγ ?]". by iDestruct (own_valid_2 with "Hγ Hγf") - as %[[[] ?%leibniz_equiv_iff] _]%auth_valid_discrete_2. + as %[[[] ?%leibniz_equiv_iff] _]%auth_both_valid. Qed. Lemma free_spec γ lk R `{!Uniform R} : diff --git a/theories/iron_logic/fcinv.v b/theories/iron_logic/fcinv.v index 714f18b..74c460a 100644 --- a/theories/iron_logic/fcinv.v +++ b/theories/iron_logic/fcinv.v @@ -123,7 +123,7 @@ Proof. iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]". { apply pred_infinite_True. } iMod (own_alloc (●! (1%Qp : ufrac) ⋅ ◯! (1%Qp : ufrac))) - as (γf) "[Hγauth Hγ]"; first done. + as (γf) "[Hγauth Hγ]"; first by apply auth_both_valid. set (γ := FcInvName γinv γf). iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"]. iExists γ, ε, ε; iSplit; [done|iSplitL "Hγinv"; [auto|]]. -- GitLab