Commit 2d178e1e authored by Hai Dang's avatar Hai Dang

Bump Iris (changes in auth)

parent 5b5acee6
Pipeline #17336 passed with stage
in 7 minutes and 26 seconds
......@@ -3,7 +3,7 @@ In this exercise we use the spin-lock from the previous exercise to implement
the running example during the lecture of the tutorial: proving that when two
threads increase a reference that's initially zero by two, the result is four.
*)
From iris.algebra Require Import auth frac_auth.
From iris.algebra Require Import auth frac_auth excl.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation.
From exercises Require Import ex_03_spinlock.
......@@ -75,7 +75,9 @@ Section proof2.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]"; by eauto with iFrame.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ n m :
......@@ -83,7 +85,7 @@ Section proof2.
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ n' n m :
......@@ -137,7 +139,8 @@ Section proof3.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]"; [done|].
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *)
admit. }
......
......@@ -8,7 +8,7 @@ first, the outcome is either 2 or 4.
Contrary to the earlier exercises, this exercise is nearly entirely open.
*)
From iris.algebra Require Import auth frac_auth.
From iris.algebra Require Import auth frac_auth excl.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation lib.par.
From exercises Require Import ex_03_spinlock.
......@@ -33,7 +33,9 @@ Section proof.
Lemma ghost_var_alloc b :
(|==> γ, own γ ( (Excl' b)) own γ ( (Excl' b)))%I.
Proof.
iMod (own_alloc ( (Excl' b) (Excl' b))) as (γ) "[??]"; by eauto with iFrame.
iMod (own_alloc ( (Excl' b) (Excl' b))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ b c :
......@@ -41,7 +43,7 @@ Section proof.
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ b' b c :
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [] # This repo does not install
remove: []
depends: [
"coq-iris" { (= "dev.2019-03-04.1.a848ac3b") | (= "dev") }
"coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
]
......@@ -3,7 +3,7 @@ In this exercise we use the spin-lock from the previous exercise to implement
the running example during the lecture of the tutorial: proving that when two
threads increase a reference that's initially zero by two, the result is four.
*)
From iris.algebra Require Import auth frac_auth.
From iris.algebra Require Import auth frac_auth excl.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation.
From solutions Require Import ex_03_spinlock.
......@@ -79,7 +79,9 @@ Section proof2.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]"; by eauto with iFrame.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ n m :
......@@ -87,7 +89,7 @@ Section proof2.
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ n' n m :
......@@ -150,7 +152,8 @@ Section proof3.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]"; [done|].
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0%nat. iFrame. }
iIntros (l) "#Hl". wp_let.
......
......@@ -8,7 +8,7 @@ first, the outcome is either 2 or 4.
Contrary to the earlier exercises, this exercise is nearly entirely open.
*)
From iris.algebra Require Import auth frac_auth.
From iris.algebra Require Import auth frac_auth excl.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation lib.par.
From solutions Require Import ex_03_spinlock.
......@@ -33,7 +33,9 @@ Section proof.
Lemma ghost_var_alloc b :
(|==> γ, own γ ( (Excl' b)) own γ ( (Excl' b)))%I.
Proof.
iMod (own_alloc ( (Excl' b) (Excl' b))) as (γ) "[??]"; by eauto with iFrame.
iMod (own_alloc ( (Excl' b) (Excl' b))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ b c :
......@@ -41,7 +43,7 @@ Section proof.
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ b' b c :
......
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