Commit 1813cb14 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 9795c36e
...@@ -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-08-29.2.b75bb397") | (= "dev") } "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -7,9 +7,9 @@ From iris_examples.barrier Require Import proof specification. ...@@ -7,9 +7,9 @@ From iris_examples.barrier Require Import proof specification.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition one_shotR (Σ : gFunctors) (F : oFunctor) := Definition one_shotR (Σ : gFunctors) (F : oFunctor) :=
csumR (exclR unitO) (agreeR $ laterO $ F (iPreProp Σ) _). csumR (exclR unitO) (agreeR $ laterO $ F (iPrePropO Σ) _).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()). Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : oFunctor} (x : F (iProp Σ) _) : one_shotR Σ F := Definition Shot {Σ} {F : oFunctor} (x : F (iPropO Σ) _) : one_shotR Σ F :=
Cinr $ to_agree $ Next $ oFunctor_map F (iProp_fold, iProp_unfold) x. Cinr $ to_agree $ Next $ oFunctor_map F (iProp_fold, iProp_unfold) x.
Class oneShotG (Σ : gFunctors) (F : oFunctor) := Class oneShotG (Σ : gFunctors) (F : oFunctor) :=
...@@ -28,7 +28,7 @@ Section proof. ...@@ -28,7 +28,7 @@ Section proof.
Local Set Default Proof Using "Type*". Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}. Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace). Context (N : namespace).
Local Notation X := (F (iProp Σ) _). Local Notation X := (F (iPropO Σ) _).
Definition barrier_res γ (Φ : X iProp Σ) : iProp Σ := Definition barrier_res γ (Φ : X iProp Σ) : iProp Σ :=
( x, own γ (Shot x) Φ x)%I. ( x, own γ (Shot x) Φ x)%I.
...@@ -43,7 +43,7 @@ Proof. ...@@ -43,7 +43,7 @@ Proof.
iIntros (v) "?"; iExists x; by iSplit. iIntros (v) "?"; iExists x; by iSplit.
Qed. Qed.
Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ). Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iPropO Σ).
Context {Φ_split : x, Φ x - (Φ1 x Φ2 x)}. Context {Φ_split : x, Φ x - (Φ1 x Φ2 x)}.
Context {Ψ_join : x, Ψ1 x - Ψ2 x - Ψ x}. Context {Ψ_join : x, Ψ1 x - Ψ2 x - Ψ x}.
......
...@@ -10,7 +10,7 @@ Local Set Default Proof Using "Type*". ...@@ -10,7 +10,7 @@ Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ}. Context `{!heapG Σ, !barrierG Σ}.
Lemma barrier_spec (N : namespace) : Lemma barrier_spec (N : namespace) :
recv send : loc iProp Σ -n> iProp Σ, recv send : loc iPropO Σ -n> iPropO Σ,
( P, {{ True }} newbarrier #() ( P, {{ True }} newbarrier #()
{{ v, l : loc, v = #l recv l P send l P }}) {{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }}) ( l P, {{ send l P P }} signal #l {{ _, True }})
......
...@@ -44,8 +44,8 @@ Section stacks. ...@@ -44,8 +44,8 @@ Section stacks.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val. Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed. Proof. intros [|][|]; simpl; congruence. Qed.
Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iProp Σ) : Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iPropO Σ) :
option loc -d> iProp Σ := λ v, match v with option loc -d> iPropO Σ := λ v, match v with
| None => True | None => True
| Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t | Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t
end%I. end%I.
......
...@@ -254,8 +254,8 @@ Section stack_works. ...@@ -254,8 +254,8 @@ Section stack_works.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val. Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed. Proof. intros [|][|]; simpl; congruence. Qed.
Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iProp Σ) : Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iPropO Σ) :
option loc -d> iProp Σ := λ v, match v with option loc -d> iPropO Σ := λ v, match v with
| None => True | None => True
| Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t | Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t
end%I. end%I.
......
...@@ -189,7 +189,7 @@ Section contents. ...@@ -189,7 +189,7 @@ Section contents.
Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv). Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).
Program Definition pre_runner (γ : name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) : Program Definition pre_runner (γ : name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) :
(valO -n> iProp Σ) -n> (valO -n> iProp Σ) := λne R r, (valO -n> iPropO Σ) -n> (valO -n> iPropO Σ) := λne R r,
( (body bag : val), r = (body, bag)%V ( (body bag : val), r = (body, bag)%V
bagS b (N.@"bag") (λ x y, γ γ', isTask (body,x) γ γ' y P Q) γ bag bagS b (N.@"bag") (λ x y, γ γ', isTask (body,x) γ γ' y P Q) γ bag
r a: val, (R r P a - WP body r a {{ v, Q a v }}))%I. r a: val, (R r P a - WP body r a {{ v, Q a v }}))%I.
...@@ -200,7 +200,7 @@ Section contents. ...@@ -200,7 +200,7 @@ Section contents.
Proof. unfold pre_runner. solve_contractive. Qed. Proof. unfold pre_runner. solve_contractive. Qed.
Definition runner (γ: name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) : Definition runner (γ: name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) :
valO -n> iProp Σ := valO -n> iPropO Σ :=
(fixpoint (pre_runner γ P Q))%I. (fixpoint (pre_runner γ P Q))%I.
Lemma runner_unfold γ r P Q : Lemma runner_unfold γ r P Q :
......
...@@ -42,7 +42,7 @@ Implicit Types l : loc. ...@@ -42,7 +42,7 @@ Implicit Types l : loc.
of Iris propositions (written Prop in the lecture notes) depends on this Σ. of Iris propositions (written Prop in the lecture notes) depends on this Σ.
But since Σ is the same throughout the development we shall define But since Σ is the same throughout the development we shall define
shorthand notation which hides it. *) shorthand notation which hides it. *)
Notation iProp := (iProp Σ). Notation iProp := (iPropO Σ).
(* First we define the is_list representation predicate via a guarded fixed (* First we define the is_list representation predicate via a guarded fixed
point of the functional is_list_pre. Note the use of the later modality. The point of the functional is_list_pre. Note the use of the later modality. The
......
...@@ -7,7 +7,7 @@ Import uPred. ...@@ -7,7 +7,7 @@ Import uPred.
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{irisG F_mu_lang Σ}. Context `{irisG F_mu_lang Σ}.
Notation D := (valO -n> iProp Σ). Notation D := (valO -n> iPropO Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Implicit Types interp : listO D D. Implicit Types interp : listO D D.
......
...@@ -19,7 +19,7 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" := ...@@ -19,7 +19,7 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
Section fundamental. Section fundamental.
Context `{heapG Σ,cfgSG Σ}. Context `{heapG Σ,cfgSG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types e : expr. Implicit Types e : expr.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Hint Resolve to_of_val. Hint Resolve to_of_val.
......
...@@ -9,7 +9,7 @@ Definition logN : namespace := nroot .@ "logN". ...@@ -9,7 +9,7 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{heapG Σ}. Context `{heapG Σ}.
Notation D := (valO -n> iProp Σ). Notation D := (valO -n> iPropO Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Implicit Types interp : listO D D. Implicit Types interp : listO D D.
...@@ -60,7 +60,7 @@ Section logrel. ...@@ -60,7 +60,7 @@ Section logrel.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper. intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed. Qed.
Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi, Program Definition interp_ref_inv (l : loc) : D -n> iPropO Σ := λne τi,
( v, l v τi v)%I. ( v, l v τi v)%I.
Solve Obligations with solve_proper. Solve Obligations with solve_proper.
......
...@@ -25,7 +25,7 @@ Definition logN : namespace := nroot .@ "logN". ...@@ -25,7 +25,7 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{heapG Σ, cfgSG Σ}. Context `{heapG Σ, cfgSG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Implicit Types interp : listO D D. Implicit Types interp : listO D D.
...@@ -94,7 +94,7 @@ Section logrel. ...@@ -94,7 +94,7 @@ Section logrel.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper. intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
Qed. Qed.
Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi, Program Definition interp_ref_inv (ll : loc * loc) : D -n> iPropO Σ := λne τi,
( vv, ll.1 vv.1 ll.2 ↦ₛ vv.2 τi vv)%I. ( vv, ll.1 vv.1 ll.2 ↦ₛ vv.2 τi vv)%I.
Solve Obligations with repeat intros ?; simpl; auto_equiv. Solve Obligations with repeat intros ?; simpl; auto_equiv.
......
...@@ -35,7 +35,7 @@ Definition FG_counter : expr := ...@@ -35,7 +35,7 @@ Definition FG_counter : expr :=
Section CG_Counter. Section CG_Counter.
Context `{heapIG Σ, cfgSG Σ}. Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
(* Coarse-grained increment *) (* Coarse-grained increment *)
......
...@@ -10,7 +10,7 @@ Definition stackN : namespace := nroot .@ "stack". ...@@ -10,7 +10,7 @@ Definition stackN : namespace := nroot .@ "stack".
Section Stack_refinement. Section Stack_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}. Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Lemma FG_CG_counter_refinement : Lemma FG_CG_counter_refinement :
......
...@@ -17,7 +17,7 @@ Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : bi_scope. ...@@ -17,7 +17,7 @@ Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : bi_scope.
Section Rules. Section Rules.
Context `{stackG Σ}. Context `{stackG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵏ v). Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵏ v).
Proof. apply _. Qed. Proof. apply _. Qed.
......
...@@ -19,7 +19,7 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" := ...@@ -19,7 +19,7 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
Section fundamental. Section fundamental.
Context `{heapIG Σ, cfgSG Σ}. Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types e : expr. Implicit Types e : expr.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Hint Resolve to_of_val. Hint Resolve to_of_val.
......
...@@ -28,7 +28,7 @@ Definition logN : namespace := nroot .@ "logN". ...@@ -28,7 +28,7 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{heapIG Σ, cfgSG Σ}. Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodO valO valO -n> iProp Σ). Notation D := (prodO valO valO -n> iPropO Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Implicit Types interp : listO D D. Implicit Types interp : listO D D.
...@@ -104,7 +104,7 @@ Section logrel. ...@@ -104,7 +104,7 @@ Section logrel.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper. intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
Qed. Qed.
Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi, Program Definition interp_ref_inv (ll : loc * loc) : D -n> iPropO Σ := λne τi,
( vv, ll.1 ↦ᵢ vv.1 ll.2 ↦ₛ vv.2 τi vv)%I. ( vv, ll.1 ↦ᵢ vv.1 ll.2 ↦ₛ vv.2 τi vv)%I.
Solve Obligations with solve_proper. Solve Obligations with solve_proper.
......
...@@ -10,7 +10,7 @@ Definition logN : namespace := nroot .@ "logN". ...@@ -10,7 +10,7 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{heapIG Σ}. Context `{heapIG Σ}.
Notation D := (valO -n> iProp Σ). Notation D := (valO -n> iPropO Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listO D. Implicit Types Δ : listO D.
Implicit Types interp : listO D D. Implicit Types interp : listO D D.
...@@ -62,7 +62,7 @@ Section logrel. ...@@ -62,7 +62,7 @@ Section logrel.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper. intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed. Qed.
Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi, Program Definition interp_ref_inv (l : loc) : D -n> iPropO Σ := λne τi,
( v, l ↦ᵢ v τi v)%I. ( v, l ↦ᵢ v τi v)%I.
Solve Obligations with solve_proper. Solve Obligations with solve_proper.
......
...@@ -24,7 +24,7 @@ Section lty_ofe. ...@@ -24,7 +24,7 @@ Section lty_ofe.
Canonical Structure ltyC := OfeT (lty Σ) lty_ofe_mixin. Canonical Structure ltyC := OfeT (lty Σ) lty_ofe_mixin.
Global Instance lty_cofe : Cofe ltyC. Global Instance lty_cofe : Cofe ltyC.
Proof. Proof.
apply (iso_cofe_subtype' (λ A : val -d> iProp Σ, w, Persistent (A w)) apply (iso_cofe_subtype' (λ A : val -d> iPropO Σ, w, Persistent (A w))
(@Lty _) lty_car)=> //. (@Lty _) lty_car)=> //.
- apply _. - apply _.
- apply limit_preserving_forall=> w. - apply limit_preserving_forall=> w.
......
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