Commit 0b58a0c8 authored by Hai Dang's avatar Hai Dang

Bump Iris (changes in auth)

parent cfcd6329
Pipeline #17256 failed with stage
in 13 minutes and 36 seconds
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-05-09.1.d0daa181") | (= "dev") } "coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
] ]
...@@ -53,21 +53,27 @@ Section ufrac_auth. ...@@ -53,21 +53,27 @@ Section ufrac_auth.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance ufrac_auth_auth_discrete a : Discrete a Discrete (?{q} a). 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). 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). 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). 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. Lemma ufrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Proof. Proof.
rewrite auth_validN_eq /= => -[Hincl Hvalid]. rewrite auth_both_validN => -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]]. move: Hincl=> /Some_includedN=> -[[//]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=]. rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst. rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed. Qed.
Lemma ufrac_auth_agree p a b : (?{p} a ?{p} b) a b. Lemma ufrac_auth_agree p a b : (?{p} a ?{p} b) a b.
...@@ -78,10 +84,10 @@ Section ufrac_auth. ...@@ -78,10 +84,10 @@ Section ufrac_auth.
Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed. 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. 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 : Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
(?{p} a ?{q} b) Some b Some a. (?{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 : Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
{n} (?{p} a ?{q} b) b {n} a. {n} (?{p} a ?{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed. Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
...@@ -91,7 +97,7 @@ Section ufrac_auth. ...@@ -91,7 +97,7 @@ Section ufrac_auth.
Lemma ufrac_auth_auth_validN n q a : {n} (?{q} a) {n} a. Lemma ufrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Proof. Proof.
split; [by intros [_ [??]]|]. rewrite -auth_auth_validN. split; [by intros []|].
repeat split; simpl; by try apply: ucmra_unit_leastN. repeat split; simpl; by try apply: ucmra_unit_leastN.
Qed. Qed.
Lemma ufrac_auth_auth_valid q a : (?{q} a) a. Lemma ufrac_auth_auth_valid q a : (?{q} a) a.
......
...@@ -4,7 +4,7 @@ in [iron_logic/adequacy]. ...@@ -4,7 +4,7 @@ in [iron_logic/adequacy].
Note, we only state adequacy for the lifted logic, because in the Coq Note, we only state adequacy for the lifted logic, because in the Coq
formalization we state all specifications in terms of the lifted logic. *) 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.iron_logic Require Export weakestpre adequacy.
From iron.algebra Require Import ufrac_auth. From iron.algebra Require Import ufrac_auth.
From iron.heap_lang Require Import heap. From iron.heap_lang Require Import heap.
...@@ -37,7 +37,7 @@ Proof. ...@@ -37,7 +37,7 @@ Proof.
iMod (own_alloc (?{1} (?{1/2} ?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]". iMod (own_alloc (?{1} (?{1/2} ?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id. { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
by apply ufrac_auth_valid. } 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). iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf". iFrame "Hp". iSplitL "Hσ Hf".
...@@ -55,7 +55,7 @@ Proof. ...@@ -55,7 +55,7 @@ Proof.
(?{1/2} (to_heap σ) ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]". (?{1/2} (to_heap σ) ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id. { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
apply ufrac_auth_valid; by apply to_heap_valid. } 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). iModIntro. pose (HeapG _ _ _ γ _ _ γf).
iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I.
iFrame "Hp". iSplitL "Hσ Hf". iFrame "Hp". iSplitL "Hσ Hf".
...@@ -98,7 +98,7 @@ Proof. ...@@ -98,7 +98,7 @@ Proof.
- intros Hwp Hsteps. - intros Hwp Hsteps.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ2' _ _ (λ _, σ2' = σ2) _ ε); eapply (iron_wp_all_adequacy _ heap_lang _ _ σ2' _ _ (λ _, σ2' = σ2) _ ε);
[|done]; iIntros (? κs) "". [|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} ε))) iMod (own_alloc (?{1} (to_heap ) (?{1/2} (to_heap ) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]". as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id. { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
...@@ -123,7 +123,7 @@ Proof. ...@@ -123,7 +123,7 @@ Proof.
- intros Hwp Hsteps. - intros Hwp Hsteps.
eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _ eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _
(Some (1 / 2)%Qp)); [|done]; iIntros (? κs) "". (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} ε))) iMod (own_alloc (?{1} (to_heap σ1) (?{1/2} (to_heap σ1) ?{1/2} ε)))
as (γ) "[Hσ [Hσ' Hp]]". as (γ) "[Hσ [Hσ' Hp]]".
{ rewrite -ufrac_auth_frag_op Qp_div_2 right_id. { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
......
(** This file defines the basic points-to [↦] connectives for the Iron logic (** 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 instantiated with the heap_lang language. As a counter part to this, it defines
the state interpretation [heap_ctx]. *) 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.base_logic.lib Require Export own.
From iris.bi.lib Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
...@@ -242,7 +242,7 @@ Section heap. ...@@ -242,7 +242,7 @@ Section heap.
iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]". iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]".
iAssert πfs !! j = Some π %I as %Hj. iAssert πfs !! j = Some π %I as %Hj.
{ iDestruct (own_valid_2 with "Hn 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 Hj as (eπ'&Hj%leibniz_equiv&[[=]|(?&?&[= <-]&[= <-]&Heπ)]%option_included).
destruct Heπ as [<-%leibniz_equiv|Hincl]; last first. destruct Heπ as [<-%leibniz_equiv|Hincl]; last first.
{ exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //. { exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //.
......
...@@ -212,7 +212,8 @@ Section queue_spec. ...@@ -212,7 +212,8 @@ Section queue_spec.
iDestruct "Hlhptr" as "[Hlhptr Hlhptr']". iDestruct "Hlhptr" as "[Hlhptr Hlhptr']".
iMod (own_alloc (1%Qp, to_agree [])) as (γ) "[Hγ Hγ']"; first done. 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 ())) 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) 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&#?)". with "[Hlhptr' Hγ' Hl Hγe]") as (γinv) "([Hγinv Hγinv']&Hγc&#?)".
{ iIntros "!>" (γinv). { iIntros "!>" (γinv).
...@@ -293,7 +294,7 @@ Section queue_spec. ...@@ -293,7 +294,7 @@ Section queue_spec.
iMod (fcinv_open _ N with "[$] Hγinv") as "[H Hclose]"; first done. 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 "H" as (lh lt' vs) "(>Hvs & >Hlhptr' & >Hγe & Hlist & >Hlt')".
iDestruct (own_valid_2 with "Hγe Hγe'") 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']". iMod (own_update_2 with "Hγe Hγe'") as "[Hγe Hγe']".
{ by apply auth_update, option_local_update, { by apply auth_update, option_local_update,
(exclusive_local_update _ (Excl ltn)). } (exclusive_local_update _ (Excl ltn)). }
...@@ -326,7 +327,7 @@ Section queue_spec. ...@@ -326,7 +327,7 @@ Section queue_spec.
iMod (fcinv_cancel with "[$] Hγc [$Hγinv $Hγinv']") as "H"; first done. 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 "H" as (lh lt' vs) "(>Hvs' & >Hlhptr' & >Hγe & Hlist & >Hlt)".
iDestruct (own_valid_2 with "Hγe Hγe'") 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 "Hlhptr" as (v') "Hlhptr".
iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %?; simplify_eq. iDestruct (mapsto_agree with "Hlhptr Hlhptr'") as %?; simplify_eq.
iCombine "Hlhptr Hlhptr'" as "Hlhptr". iCombine "Hlhptr Hlhptr'" as "Hlhptr".
......
...@@ -10,7 +10,7 @@ From iron.iron_logic Require Export weakestpre. ...@@ -10,7 +10,7 @@ From iron.iron_logic Require Export weakestpre.
From iron.heap_lang Require Export lang adequacy. From iron.heap_lang Require Export lang adequacy.
From iron.heap_lang Require Import proofmode notation. From iron.heap_lang Require Import proofmode notation.
From iron.iron_logic Require Import fcinv. 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". Set Default Proof Using "Type".
Definition new_lock : val := λ: <>, ref #false. Definition new_lock : val := λ: <>, ref #false.
...@@ -97,7 +97,7 @@ Section proof. ...@@ -97,7 +97,7 @@ Section proof.
Proof. Proof.
iIntros (Φ) "HR HΦ". rewrite -iron_wp_fupd /new_lock /=. iIntros (Φ) "HR HΦ". rewrite -iron_wp_fupd /new_lock /=.
wp_lam. wp_alloc l as "Hl". 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) iMod (fcinv_alloc_named _ N (λ γinv, lock_inv (LockName γinv γ) l R)
with "[-HΦ]") as (γinv) "(Hγ & Hγc & #?)". with "[-HΦ]") as (γinv) "(Hγ & Hγc & #?)".
{ iIntros "!>" (γinv). iExists false. by iFrame. } { iIntros "!>" (γinv). iExists false. by iFrame. }
...@@ -143,7 +143,7 @@ Section proof. ...@@ -143,7 +143,7 @@ Section proof.
iDestruct "Hinv" as ([|]) "[Hl Hinv]". iDestruct "Hinv" as ([|]) "[Hl Hinv]".
- wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv]". - wp_store. iDestruct "Hinv" as (p') "[Hγ Hγinv]".
iDestruct (own_valid_2 with "Hγ Hγf") 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γ". iMod (own_update_2 with "Hγ Hγf") as "Hγ".
{ eapply auth_update_dealloc, delete_option_local_update; apply _. } { eapply auth_update_dealloc, delete_option_local_update; apply _. }
iMod ("Hclose" with "[HR Hl Hγ]"). iMod ("Hclose" with "[HR Hl Hγ]").
...@@ -151,7 +151,7 @@ Section proof. ...@@ -151,7 +151,7 @@ Section proof.
iApply "HΦ". iModIntro. by iFrame. iApply "HΦ". iModIntro. by iFrame.
- iDestruct "Hinv" as "[>Hγ ?]". - iDestruct "Hinv" as "[>Hγ ?]".
by iDestruct (own_valid_2 with "Hγ Hγf") 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. Qed.
Lemma free_spec γ lk R `{!Uniform R} : Lemma free_spec γ lk R `{!Uniform R} :
......
...@@ -123,7 +123,7 @@ Proof. ...@@ -123,7 +123,7 @@ Proof.
iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]". iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]".
{ apply pred_infinite_True. } { apply pred_infinite_True. }
iMod (own_alloc (! (1%Qp : ufrac) ! (1%Qp : ufrac))) 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). set (γ := FcInvName γinv γf).
iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"]. iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"].
iExists γ, ε, ε; iSplit; [done|iSplitL "Hγinv"; [auto|]]. iExists γ, ε, ε; iSplit; [done|iSplitL "Hγinv"; [auto|]].
......
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