Commit 3092552d authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent dd32b1ff
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-11-07.3.eb2dfc72") | (= "dev") }
"coq-iris" { (= "dev.2019-11-07.9.4f3eb1ac") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -35,14 +35,15 @@ Section monotone_counter.
*)
(* The carrier of our resource algebra is the set ℕ_{⊥,⊤} × ℕ. NBT (Natural
numbers with Top and Bottom) is the first component of this product. *)
numbers with Top and Bottom) is the first component of this product. We
wrap the project into a record to avoid ambiguous type class search. *)
Inductive NBT :=
Bot : NBT (* Bottom *)
| Top : NBT (* Top *)
| NBT_incl : nat NBT. (* Inclusion of natural numbers into our new type. *)
(* The carrier of our RA. *)
Definition mcounterRAT : Type := NBT * nat.
Record mcounterRAT := MCounter { mcounter_auth : NBT; mcounter_flag : nat }.
(* The notion of a resource algebra as used in Iris is more general than the one
currently described. It is called a cmra (standing roughly for complete
......@@ -71,14 +72,12 @@ Section monotone_counter.
a lot of the notation mechanism (we can write x ⋅ y for the operation), and
some other infrastucture and generic lemmas. *)
Instance mcounterRAop : Op mcounterRAT :=
λ p p,
let (x, n) := p in
let (y, m) := p in
λ '(MCounter x n) '(MCounter y m),
match x with
Bot => (y, max n m)
Bot => MCounter y (max n m)
| _ => match y with
Bot => (x, max n m)
| _ => (Top, max n m)
Bot => MCounter x (max n m)
| _ => MCounter Top (max n m)
end
end.
......@@ -89,8 +88,8 @@ Section monotone_counter.
deal with many boring use cases. *)
Instance mcounterRAValid : Valid mcounterRAT :=
λ x, match x with
(Bot, _) => True
| (NBT_incl x, m) => x m
MCounter Bot _ => True
| MCounter (NBT_incl x) m => x m
| _ => False
end.
......@@ -99,19 +98,21 @@ Section monotone_counter.
option A. Again, PCore is a typeclass for better automation support, and
thus our definition is an instance. *)
Instance mcounterRACore : PCore mcounterRAT :=
λ x, let (_, n) := x in Some (Bot, n).
λ '(MCounter _ n), Some (MCounter Bot n).
(* We can then package these definitions up into an RA structure, used by the
Iris library. *)
(* We need these auxiliary lemmas in the proof below.
We need the type annotation to guide the type inference. *)
Lemma mcounterRA_op_second (x y : NBT) n m: z, ((x, n) : mcounterRAT) (y, m) = (z, max n m).
Lemma mcounterRA_op_second (x y : NBT) n m :
z, MCounter x n MCounter y m = MCounter z (max n m).
Proof.
destruct x as [], y as []; eexists; unfold op, mcounterRAop; simpl; auto.
Qed.
Lemma mcounterRA_included_aux x y (n m : nat): ((x, n) : mcounterRAT) (y, m) (n m)%nat.
Lemma mcounterRA_included_aux x y (n m : nat) :
MCounter x n MCounter y m (n m)%nat.
Proof.
intros [[z k] [=H]].
revert H.
......@@ -119,14 +120,15 @@ Section monotone_counter.
inversion 1; subst; auto with arith.
Qed.
Lemma mcounterRA_included_frag (n m : nat): ((Bot, n) : mcounterRAT) (Bot, m) (n m)%nat.
Lemma mcounterRA_included_frag (n m : nat) :
MCounter Bot n MCounter Bot m (n m)%nat.
Proof.
split.
- apply mcounterRA_included_aux.
- intros H%Max.max_r; exists (Bot, m); unfold op, mcounterRAop; rewrite H; auto.
- intros H%Max.max_r; exists (MCounter Bot m); unfold op, mcounterRAop; rewrite H; auto.
Qed.
Lemma mcounterRA_valid x (n : nat): ((NBT_incl x, n) : mcounterRAT) (n x)%nat.
Lemma mcounterRA_valid x (n : nat): (MCounter (NBT_incl x) n) (n x)%nat.
Proof.
split; auto.
Qed.
......@@ -147,7 +149,7 @@ Section monotone_counter.
- unfold pcore, mcounterRACore, op, mcounterRAop; intros [[]] [[]] [=->]; auto.
- unfold pcore, mcounterRACore, op, mcounterRAop.
intros [x n] [y m] cx Hleq%mcounterRA_included_aux [=<-].
exists (Bot, m); split; first auto.
exists (MCounter Bot m); split; first auto.
by apply mcounterRA_included_frag.
- (* Validity axiom: validity is down-closed with respect to the extension order. *)
intros [[]].
......@@ -182,8 +184,8 @@ Section monotone_counter.
since the same notation is already defined for the general authoritative RA
construction in the Iris Coq library.
*)
Local Notation "◯ n" := ((Bot, n%nat) : mcounterRA) (at level 20).
Local Notation "● m" := ((NBT_incl m%nat, 0%nat) : mcounterRA) (at level 20).
Local Notation "◯ n" := (MCounter Bot n%nat) (at level 20).
Local Notation "● m" := (MCounter (NBT_incl m%nat) 0%nat) (at level 20).
(* We now prove the three properties we claim were required from the resource
algebra in Section 7.7.
......@@ -293,7 +295,7 @@ Section monotone_counter.
wp_load.
(* NOTE: We use the validity property of the RA we have constructed. From the fact that we own
◯ n and ● m to conclude that n ≤ m. *)
iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag.
iDestruct (own_valid_2 with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
......
......@@ -22,7 +22,7 @@ Section fundamental.
Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types e : expr.
Implicit Types Δ : listO D.
Hint Resolve to_of_val.
Hint Resolve to_of_val : core.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
constr(Hv) uconstr(Hp) :=
......
......@@ -265,13 +265,8 @@ Section logrel.
destruct (decide (l = l2)); subst; last auto.
iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
iDestruct "Hi" as ((v1, v2)) "(Hl3 & Hl2' & ?)".
iMod "Hl2'"; simpl.
unfold heapS_mapsto.
iDestruct (@own_valid_2 _ _ _ cfg_name with "Hl1 Hl2'") as %[_ Hvl].
exfalso.
specialize (Hvl l6); revert Hvl. simpl.
rewrite /= gmap.lookup_op !lookup_singleton -Some_op. by intros [? _].
iDestruct "Hi" as ((v1, v2)) "(Hl3 & >Hl2' & ?)".
by iDestruct (mapstoS_valid_2 with "Hl1 Hl2'") as %[].
Qed.
Lemma interp_ref_open' Δ τ l l' :
......@@ -368,18 +363,11 @@ Section logrel.
by iDestruct (@mapsto_valid_2 with "Hlx1' Hl1''") as %?.
+ iInv (logN.@(l2, l3')) as "Hib1" "Hcl1".
iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
iDestruct "Hib1" as ((v11, v12)) "(Hl1 & Hl2' & Hr1)".
iDestruct "Hib2" as ((v11', v12')) "(Hl1' & Hl2'' & Hr2)".
simpl.
iMod "Hl2'"; iMod "Hl2''".
unfold heapS_mapsto.
iDestruct (@own_valid_2 _ _ _ cfg_name with "Hl2' Hl2''") as %[_ Hvl].
exfalso.
specialize (Hvl l3'); revert Hvl.
rewrite /= gmap.lookup_op !lookup_singleton -Some_op. by intros [? _].
iDestruct "Hib1" as ((v11, v12)) "(>Hl1 & >Hl2' & Hr1)".
iDestruct "Hib2" as ((v11', v12')) "(>Hl1' & >Hl2'' & Hr2) /=".
by iDestruct (mapstoS_valid_2 with "Hl2' Hl2''") as %[].
+ iModIntro; iPureIntro; split; intros; simplify_eq. }
Qed.
End logrel.
Typeclasses Opaque interp_env.
......
......@@ -80,7 +80,7 @@ Section conversions.
Qed.
Lemma tpool_lookup_Some tp j e : to_tpool tp !! j = Excl' e tp !! j = Some e.
Proof. rewrite tpool_lookup fmap_Some. naive_solver. Qed.
Hint Resolve tpool_lookup_Some.
Hint Resolve tpool_lookup_Some : core.
Lemma to_tpool_insert tp j e :
j < length tp
......@@ -130,11 +130,35 @@ Section cfg.
Implicit Types e : expr.
Implicit Types v : val.
Local Hint Resolve tpool_lookup.
Local Hint Resolve tpool_lookup_Some.
Local Hint Resolve to_tpool_insert.
Local Hint Resolve to_tpool_insert'.
Local Hint Resolve tpool_singleton_included.
Local Hint Resolve tpool_lookup : core.
Local Hint Resolve tpool_lookup_Some : core.
Local Hint Resolve to_tpool_insert : core.
Local Hint Resolve to_tpool_insert' : core.
Local Hint Resolve tpool_singleton_included : core.
Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 - l ↦ₛ{q2} v2 - v1 = v2.
Proof.
apply wand_intro_r.
rewrite /heapS_mapsto -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> -[_] /=. rewrite op_singleton singleton_valid -pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
Lemma mapstoS_combine l q1 q2 v1 v2 :
l ↦ₛ{q1} v1 - l ↦ₛ{q2} v2 - l ↦ₛ{q1 + q2} v1 v1 = v2.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapstoS_agree with "Hl1 Hl2") as %->.
rewrite /heapS_mapsto. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
Qed.
Lemma mapstoS_valid l q v : l ↦ₛ{q} v - q.
Proof.
rewrite /heapS_mapsto own_valid !discrete_valid -auth_frag_valid.
by apply pure_mono=> -[_] /singleton_valid [??].
Qed.
Lemma mapstoS_valid_2 l q1 q2 v1 v2 : l ↦ₛ{q1} v1 - l ↦ₛ{q2} v2 - (q1 + q2)%Qp.
Proof.
iIntros "H1 H2". iDestruct (mapstoS_combine with "H1 H2") as "[? ->]".
by iApply (mapstoS_valid l _ v2).
Qed.
Lemma step_insert K tp j e σ κ e' σ' efs :
tp !! j = Some (fill K e) head_step e σ κ e' σ' efs
......
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