Commit 9d76d017 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Update dependencies

parent dd6a3c1a
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-06-15.0.e84de6cc") | (= "dev") }
"coq-iris" { (= "dev.2020-06-18.3.5f98a0bf") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
......
......@@ -3,7 +3,7 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth.
From iris.algebra Require Import numbers frac_auth.
From iris_examples.lecture_notes Require Import modular_incr.
......
......@@ -9,6 +9,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang Require Import notation lang.
From iris.algebra Require Import numbers.
From iris.heap_lang.lib Require Import par.
......@@ -356,7 +357,7 @@ End monotone_counter.
As we stated in an exercise in the counter modules section of the lecture
notes, the resource algebra we constructed above is nothing but Auth(N_max).
Auth and N_max are both part of the iris Coq library. They are called authR
and mnatUR (standing for authoritative Resource algebra and max nat Unital
and max_natUR (standing for authoritative Resource algebra and max nat Unital
Resource algebra). *)
(* Auth is defined in iris.algebra.auth. *)
......@@ -404,40 +405,44 @@ End auth_update.
Section monotone_counter'.
(* We tell Coq that our Iris instantiation has the following resource
algebras. Note that the only diffference from above is that we use authR
mnatUR in place of the resource algebra mcounterRA we constructed above. *)
Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR mnatUR)}.
Definition mcounterΣ' : gFunctors := #[GFunctor (authR mnatUR)].
max_natUR in place of the resource algebra mcounterRA we constructed above. *)
Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR max_natUR)}.
Definition mcounterΣ' : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_mcounterΣ' {Σ} : subG mcounterΣ' Σ mcounterG' Σ.
Proof. solve_inG. Qed.
(* We now prove the same three properties we claim were required from the resource
algebra in Section 7.7. *)
Instance mcounterRA_frag_core' (n : mnatUR): CoreId ( n).
Instance mcounterRA_frag_core' (n : max_natUR): CoreId ( n).
Proof.
apply _.
(* CoreID is a typeclass, so typeclass search can automatically deduce what
we want. Concretely, the proof follows by lemmas auth_frag_core_id and
mnat_core_id proved in the Iris Coq library. *)
max_nat_core_id proved in the Iris Coq library. *)
Qed.
Lemma mcounterRA_valid_auth_frag' (m n : mnatUR): ( m n) (n m)%nat.
Lemma mcounterRA_valid_auth_frag' (m n : max_natUR): ( m n) (max_nat_car n max_nat_car m)%nat.
Proof.
(* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
The general definition also involves the use of step-indices, which is not needed in our case. *)
rewrite auth_both_valid.
split.
- intros [? _]; by apply mnat_included.
- intros ?%mnat_included; done.
- intros [? _]; by apply max_nat_included.
- intros ?%max_nat_included; done.
Qed.
Lemma mcounterRA_update' (m n : mnatUR): m n ~~> (S m : mnatUR) (S n : mnatUR).
Lemma max_nat_op_succ m : MaxNat (S m) = MaxNat m MaxNat (S m).
Proof. rewrite max_nat_op_max. apply f_equal. lia. Qed.
Lemma mcounterRA_update' (m n : max_natUR) :
m n ~~> MaxNat (S (max_nat_car m)) MaxNat (S (max_nat_car n)).
Proof.
replace (S m) with (m (S m)); last auto with arith.
replace (S n) with (n (S n)); last auto with arith.
apply cmra_update_valid0; intros ?%cmra_discrete_valid%mcounterRA_valid_auth_frag'.
apply auth_update_add'; first reflexivity.
exists (S m); symmetry; apply max_r; auto with arith.
destruct m as [m], n as [n]. simpl.
rewrite (max_nat_op_succ m) (max_nat_op_succ n).
apply cmra_update_valid0. intros ?%cmra_discrete_valid%mcounterRA_valid_auth_frag'.
simpl in *. apply auth_update_add'; first reflexivity.
exists (MaxNat (S m)). rewrite max_nat_op_max. apply f_equal. lia.
Qed.
(* We can now verify the programs. *)
......@@ -447,9 +452,9 @@ Section monotone_counter'.
(* The rest of this section is exactly the same as the preceding one. We use
the properties of the RA we have proved above. *)
Definition counter_inv' ( : loc) (γ : gname) : iProp := ( (m : mnatUR), #m own γ ( m))%I.
Definition counter_inv' ( : loc) (γ : gname) : iProp := ( (m : nat), #m own γ ( MaxNat m))%I.
Definition isCounter' ( : loc) (n : mnatUR) : iProp :=
Definition isCounter' ( : loc) (n : max_natUR) : iProp :=
( γ, own γ ( n) inv N (counter_inv' γ))%I.
Global Instance isCounter_persistent' n: Persistent (isCounter' n).
......@@ -457,12 +462,12 @@ Section monotone_counter'.
apply _.
Qed.
Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v 0%nat }}}.
Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v (MaxNat 0) }}}.
Proof.
iIntros (Φ) "_ HCont".
rewrite /newCounter -wp_fupd.
wp_lam.
iMod (own_alloc ( (0%nat : mnatUR) (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
iMod (own_alloc ( MaxNat 0 MaxNat 0)) as (γ) "[HAuth HFrac]".
- apply mcounterRA_valid_auth_frag'; auto.
- wp_alloc as "Hpt".
iMod (inv_alloc N _ (counter_inv' γ) with "[Hpt HAuth]") as "HInv".
......@@ -472,7 +477,7 @@ Section monotone_counter'.
Qed.
(* The read method specification. *)
Lemma read_spec' n: {{{ isCounter' n }}} read # {{{ m, RET #m; n m%nat }}}.
Lemma read_spec' n : {{{ isCounter' (MaxNat n) }}} read # {{{ m, RET #m; n m%nat }}}.
Proof.
iIntros (Φ) "HCounter HCont".
iDestruct "HCounter" as (γ) "[HOwnFrag HInv]".
......@@ -488,7 +493,7 @@ Section monotone_counter'.
Qed.
(* The read method specification. *)
Lemma incr_spec' n: {{{ isCounter' n }}} incr # {{{ RET #(); isCounter' (1 + n)%nat }}}.
Lemma incr_spec' n : {{{ isCounter' (MaxNat n) }}} incr # {{{ RET #(); isCounter' (MaxNat (1 + n)) }}}.
Proof.
iIntros (Φ) "HCounter HCont".
iDestruct "HCounter" as (γ) "[HOwnFrag #HInv]".
......@@ -507,7 +512,7 @@ Section monotone_counter'.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
+ wp_cmpxchg_suc.
iMod (own_update γ (( m n)) ( (S m : mnatUR) ( (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
iMod (own_update γ ( (MaxNat m) (MaxNat n)) ( (MaxNat (S m)) ( (MaxNat (S n)))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
{ apply mcounterRA_update'. }
{ rewrite own_op; iFrame. }
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
......
From iris.algebra Require Import excl auth list gset gmap agree csum.
From iris.algebra Require Import numbers excl auth list gset gmap agree csum.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants proph_map saved_prop.
......@@ -116,7 +116,7 @@ Definition per_slot :=
Definition eltsUR := authR $ optionUR $ exclR $ listO locO.
Definition contUR := csumR (exclR unitR) (agreeR (prodO natO natO)).
Definition slotUR := authR $ gmapUR nat per_slot.
Definition backUR := authR mnatUR.
Definition backUR := authR max_natUR.
Class hwqG Σ :=
HwqG {
......@@ -182,12 +182,12 @@ Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
(** Operations for the CMRA used to show that back only increases. *)
Definition back_value γb n := own γb ( (n : mnatUR) : backUR).
Definition back_lower_bound γb n := own γb ( (n : mnatUR) : backUR).
Definition back_value γb n := own γb ( MaxNat n).
Definition back_lower_bound γb n := own γb ( MaxNat n).
Lemma new_back : |==> γb, back_value γb 0.
Proof.
iMod (own_alloc ( (0 : mnatUR) : backUR)) as (γb) "H●".
iMod (own_alloc ( MaxNat 0)) as (γb) "H●".
- by rewrite auth_auth_valid.
- by iExists γb.
Qed.
......@@ -196,14 +196,14 @@ Lemma back_incr γb n :
back_value γb n == back_value γb (S n).
Proof.
iIntros "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ (S n)). by lia.
apply auth_update_alloc, (max_nat_local_update _ _ (MaxNat (S n))). simpl. lia.
Qed.
Lemma back_snapshot γb n :
back_value γb n == back_value γb n back_lower_bound γb n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
by apply auth_update_alloc, max_nat_local_update.
Qed.
Lemma back_le γb n1 n2 :
......@@ -211,8 +211,7 @@ Lemma back_le γb n1 n2 :
Proof.
iIntros "H1 H2". iCombine "H1 H2" as "H".
iDestruct (own_valid with "H") as %Hvalid. iPureIntro.
apply auth_both_valid in Hvalid as [H1 H2].
by apply mnat_included.
apply auth_both_valid in Hvalid as [H1%max_nat_included _]. done.
Qed.
(* Stores a lower bound on the [i2] part of any contradiction that
......@@ -228,14 +227,14 @@ Lemma i2_lower_bound_update γi n m :
i2_lower_bound γi n == i2_lower_bound γi m.
Proof.
iIntros (H) "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ m). by lia.
apply auth_update_alloc, (max_nat_local_update _ _ (MaxNat m)). simpl. lia.
Qed.
Lemma i2_lower_bound_snapshot γi n :
i2_lower_bound γi n == i2_lower_bound γi n no_contra_wit γi n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
by apply auth_update_alloc, max_nat_local_update.
Qed.
(** Operations for the one-shot CMRA used for contradiction states. *)
......
From iris_examples.logrel.heaplang Require Export ltyping.
From iris.heap_lang.lib Require Import assert.
From iris.algebra Require Import auth.
From iris.algebra Require Import numbers auth.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import notation proofmode.
......@@ -13,8 +13,8 @@ Definition symbol_adt_ty `{heapG Σ} : lty Σ :=
(() A, (() A) * (A ()))%lty.
(* The required ghost theory *)
Class symbolG Σ := { symbol_inG :> inG Σ (authR mnatUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR mnatUR)].
Class symbolG Σ := { symbol_inG :> inG Σ (authR max_natUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
Proof. solve_inG. Qed.
......@@ -22,8 +22,8 @@ Proof. solve_inG. Qed.
Section symbol_ghosts.
Context `{!symbolG Σ}.
Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (n : mnat)).
Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (S n : mnat)).
Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat n)).
Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat (S n))).
Global Instance counter_timeless γ n : Timeless (counter γ n).
Proof. apply _. Qed.
......@@ -39,7 +39,7 @@ Section symbol_ghosts.
Lemma counter_alloc n : |==> γ, counter γ n.
Proof.
iMod (own_alloc ( (n:mnat) (n:mnat))) as (γ) "[Hγ Hγf]";
iMod (own_alloc ( MaxNat n MaxNat n)) as (γ) "[Hγ Hγf]";
first by apply auth_both_valid.
iExists γ. by iFrame.
Qed.
......@@ -47,14 +47,14 @@ Section symbol_ghosts.
Lemma counter_inc γ n : counter γ n == counter γ (S n) symbol γ n.
Proof.
rewrite -own_op.
apply own_update, auth_update_alloc, mnat_local_update. omega.
apply own_update, auth_update_alloc, max_nat_local_update. simpl. lia.
Qed.
Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
Proof.
iIntros "Hc Hs".
iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_both_valid.
iPureIntro. omega.
iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
simpl in *. iPureIntro. lia.
Qed.
End symbol_ghosts.
......
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