Commit ae3400d6 authored by Ralf Jung's avatar Ralf Jung

bump Iris; fix for frac_auth notation changes

parent d21da3ed
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-06-11.2.0a05a8c0") | (= "dev") } "coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -16,11 +16,11 @@ Section proof. ...@@ -16,11 +16,11 @@ Section proof.
Context `{inG Σ (frac_authR (gmultisetUR val))}. Context `{inG Σ (frac_authR (gmultisetUR val))}.
Definition bagM_inv (γb : name Σ b) (γ : gname) : iProp Σ := Definition bagM_inv (γb : name Σ b) (γ : gname) : iProp Σ :=
inv NI ( X, bag_contents b γb X own γ (! X))%I. inv NI ( X, bag_contents b γb X own γ (F X))%I.
Definition bagM (γb : name Σ b) (γ : gname) (x : val) : iProp Σ := Definition bagM (γb : name Σ b) (γ : gname) (x : val) : iProp Σ :=
(is_bag b NB γb x bagM_inv γb γ)%I. (is_bag b NB γb x bagM_inv γb γ)%I.
Definition bagPart (γ : gname) (q : Qp) (X : gmultiset val) : iProp Σ := Definition bagPart (γ : gname) (q : Qp) (X : gmultiset val) : iProp Σ :=
(own γ (!{q} X))%I. (own γ (F{q} X))%I.
Lemma bagPart_compose (γ: gname) (q1 q2: Qp) (X Y : gmultiset val) : Lemma bagPart_compose (γ: gname) (q1 q2: Qp) (X Y : gmultiset val) :
bagPart γ q1 X - bagPart γ q2 Y - bagPart γ (q1+q2) (X Y). bagPart γ q1 X - bagPart γ q2 Y - bagPart γ (q1+q2) (X Y).
...@@ -50,8 +50,8 @@ Section proof. ...@@ -50,8 +50,8 @@ Section proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd. iIntros (Φ) "_ HΦ". iApply wp_fupd.
iApply (newBag_spec b NB); eauto. iApply (newBag_spec b NB); eauto.
iNext. iIntros (v γb) "[#Hbag Hcntn]". iNext. iIntros (v γb) "[#Hbag Hcntn]".
iMod (own_alloc (! ! )) as (γ) "[Hown Hpart]"; first by apply auth_both_valid. iMod (own_alloc (F F )) as (γ) "[Hown Hpart]"; first by apply auth_both_valid.
iMod (inv_alloc NI _ ( X, bag_contents b γb X own γ (! X))%I with "[Hcntn Hown]") as "#Hinv". iMod (inv_alloc NI _ ( X, bag_contents b γb X own γ (F X))%I with "[Hcntn Hown]") as "#Hinv".
{ iNext. iExists _. iFrame. } { iNext. iExists _. iFrame. }
iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart". iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".
Qed. Qed.
......
...@@ -16,28 +16,28 @@ Proof. solve_inG. Qed. ...@@ -16,28 +16,28 @@ Proof. solve_inG. Qed.
Section ccounter. Section ccounter.
Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace). Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace).
Lemma ccounterRA_valid (m n : natR) (q : frac): (! m !{q} n) (n m)%nat. Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) (n m)%nat.
Proof. Proof.
intros ?. intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *) (* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q). by apply nat_included, (frac_auth_included_total q).
Qed. Qed.
Lemma ccounterRA_valid_full (m n : natR): (! m ! n) (n = m)%nat. Lemma ccounterRA_valid_full (m n : natR): (F m F n) (n = m)%nat.
Proof. Proof.
by intros ?%frac_auth_agree. by intros ?%frac_auth_agree.
Qed. Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (! m !{q} n) ~~> (! (S m) !{q} (S n)). Lemma ccounterRA_update (m n : natR) (q : frac): (F m F{q} n) ~~> (F (S m) F{q} (S n)).
Proof. Proof.
apply frac_auth_update, (nat_local_update _ _ (S _) (S _)). apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
lia. lia.
Qed. Qed.
Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ := Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ :=
( n, own γ₁ (! n) γ₂ ⤇½ (Z.of_nat n))%I. ( n, own γ₁ (F n) γ₂ ⤇½ (Z.of_nat n))%I.
Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (!{q} n) inv (N .@ "counter") (ccounter_inv γ₁ γ₂) Cnt N l γ₂)%I. Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (F{q} n) inv (N .@ "counter") (ccounter_inv γ₁ γ₂) Cnt N l γ₂)%I.
(** The main proofs. *) (** The main proofs. *)
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) : Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
...@@ -58,7 +58,7 @@ Section ccounter. ...@@ -58,7 +58,7 @@ Section ccounter.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd. iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
wp_apply newcounter_spec; auto. wp_apply newcounter_spec; auto.
iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]". iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
iMod (own_alloc (! m%nat ! m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid. iMod (own_alloc (F m%nat F m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]"). iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
{ iNext. iExists _. by iFrame. } { iNext. iExists _. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto. iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
...@@ -70,7 +70,7 @@ Section ccounter. ...@@ -70,7 +70,7 @@ Section ccounter.
{{{ (y : Z), RET #y; is_ccounter γ₁ γ₂ q (S n) }}}. {{{ (y : Z), RET #y; is_ccounter γ₁ γ₂ q (S n) }}}.
Proof. Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ". iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
iApply (incr_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ _, (own γ₁ (!{q} (S n))))%I with "[] [Hown]"); first set_solver. iApply (incr_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ _, (own γ₁ (F{q} (S n))))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HOwnElem HP]". - iIntros (m) "!# [HOwnElem HP]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose". iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HOwnElem H2") as %->. iDestruct (makeElem_eq with "HOwnElem H2") as %->.
...@@ -94,7 +94,7 @@ Section ccounter. ...@@ -94,7 +94,7 @@ Section ccounter.
{{{ (c : Z), RET #c; Z.of_nat n c is_ccounter γ₁ γ₂ q n }}}. {{{ (c : Z), RET #c; Z.of_nat n c is_ccounter γ₁ γ₂ q n }}}.
Proof. Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ". iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ m, n m (own γ₁ (!{q} n)))%I with "[] [Hown]"); first set_solver. wp_apply (read_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ m, n m (own γ₁ (F{q} n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]". - iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose". iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->. iDestruct (makeElem_eq with "HownE H2") as %->.
...@@ -115,7 +115,7 @@ Section ccounter. ...@@ -115,7 +115,7 @@ Section ccounter.
{{{ RET #n; is_ccounter γ₁ γ₂ 1 n }}}. {{{ RET #n; is_ccounter γ₁ γ₂ 1 n }}}.
Proof. Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ". iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (! n))%I (λ m, Z.of_nat n = m (own γ₁ (! n)))%I with "[] [Hown]"); first set_solver. wp_apply (read_spec N γ₂ _ (own γ₁ (F n))%I (λ m, Z.of_nat n = m (own γ₁ (F n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]". - iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose". iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->. iDestruct (makeElem_eq with "HownE H2") as %->.
......
...@@ -547,21 +547,21 @@ Section ccounter. ...@@ -547,21 +547,21 @@ Section ccounter.
algebra, specialized to our use case. These are listed in the exercise in algebra, specialized to our use case. These are listed in the exercise in
the relevant section of the lecture notes. *) the relevant section of the lecture notes. *)
(* We are using some new notation. The frac_auth library defines the notation (* We are using some new notation. The frac_auth library defines the notation
!{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●! m F{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●F m
means ● (1, m) and ◯! n means ◯ (1, n). *) means ● (1, m) and ◯F n means ◯ (1, n). *)
Lemma ccounterRA_valid (m n : natR) (q : frac): (! m !{q} n) (n m)%nat. Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) (n m)%nat.
Proof. Proof.
intros ?. intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *) (* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q). by apply nat_included, (frac_auth_included_total q).
Qed. Qed.
Lemma ccounterRA_valid_full (m n : natR): (! m ! n) (n = m)%nat. Lemma ccounterRA_valid_full (m n : natR): (F m F n) (n = m)%nat.
Proof. Proof.
by intros ?%frac_auth_agree. by intros ?%frac_auth_agree.
Qed. Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (! m !{q} n) ~~> (! (S m) !{q} (S n)). Lemma ccounterRA_update (m n : natR) (q : frac): (F m F{q} n) ~~> (F (S m) F{q} (S n)).
Proof. Proof.
apply frac_auth_update, (nat_local_update _ _ (S _) (S _)). apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
lia. lia.
...@@ -580,10 +580,10 @@ Section ccounter. ...@@ -580,10 +580,10 @@ Section ccounter.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace). Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ := Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ (! n) l #n)%I. ( n, own γ (F n) l #n)%I.
Definition is_ccounter (γ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := Definition is_ccounter (γ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ :=
(own γ (!{q} n) inv N (ccounter_inv γ l))%I. (own γ (F{q} n) inv N (ccounter_inv γ l))%I.
(** The main proofs. *) (** The main proofs. *)
...@@ -606,7 +606,7 @@ Section ccounter. ...@@ -606,7 +606,7 @@ Section ccounter.
{{{ γ , RET #; is_ccounter γ 1 0%nat }}}. {{{ γ , RET #; is_ccounter γ 1 0%nat }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc as "Hpt". iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc as "Hpt".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid. iMod (own_alloc (F O%nat F 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (inv_alloc N _ (ccounter_inv γ ) with "[Hpt Hγ]"). iMod (inv_alloc N _ (ccounter_inv γ ) with "[Hpt Hγ]").
{ iNext. iExists 0%nat. by iFrame. } { iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto. iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
......
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