From 3258d3a82c381f6900f01510ece5b30f0962a81f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 4 Jun 2019 10:29:10 +0200
Subject: [PATCH] bump Iris; fix for prophecy resolution changes
---
opam | 2 +-
theories/examples/coinflip.v | 8 ++++----
theories/examples/lateearlychoice.v | 6 +++---
theories/examples/or.v | 6 +++---
theories/logic/proofmode/tactics.v | 2 +-
theories/logic/rules.v | 4 ++--
theories/logic/spec_rules.v | 2 +-
theories/prelude/ctx_subst.v | 7 ++++---
8 files changed, 19 insertions(+), 18 deletions(-)
diff --git a/opam b/opam
index 421efdf..4d3fe01 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2019-06-01.2.88c7fc6d") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-03.2.b368c861") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 2e9c2fd..5a42d2f 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -59,8 +59,8 @@ Section proofs.
(** Lazy coin (with prophecies) refines eager coin *)
Definition I (cl ce : loc) (p : proph_id) :=
- (∃ vs : list val, proph p vs ∗
- (cl ↦ NONEV ∗ ce ↦ₛ #(val_to_bool vs)
+ (∃ vs : list (val*val), proph p vs ∗
+ (cl ↦ NONEV ∗ ce ↦ₛ #(extract_bool vs)
∨ ∃ (b:bool), cl ↦ SOMEV #b ∗ ce ↦ₛ #b))%I.
Lemma coin_lazy'_eager_refinement :
@@ -105,12 +105,12 @@ Section proofs.
iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
iDestruct "H" as "[[Hcl Hce]|H]"; last iDestruct "H" as (x) "[Hcl Hce]";
rel_store_l; repeat rel_pure_l.
- + rel_apply_r (refines_rand_r (val_to_bool vs)).
+ + rel_apply_r (refines_rand_r (extract_bool vs)).
rel_store_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs. iFrame. iLeft. iFrame. }
iNext. rel_values.
- + rel_apply_r (refines_rand_r (val_to_bool vs)).
+ + rel_apply_r (refines_rand_r (extract_bool vs)).
rel_store_r.
rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
{ iExists vs. iFrame. iLeft. iFrame. }
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 029080a..226a584 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -62,9 +62,9 @@ Section proof.
iMod ("Hcl" with "[Hy]") as "_"; eauto with iFrame.
Qed.
- Definition val_to_bool (vs : list val) : bool :=
+ Definition extract_bool (vs : list (val*val)) : bool :=
match vs with
- | LitV (LitBool b)::_ => b
+ | (_,LitV (LitBool b))::_ => b
| _ => true
end.
@@ -77,7 +77,7 @@ Section proof.
rel_rec_l. rel_rec_r.
rel_newproph_l vs p as "Hp".
repeat rel_pure_l.
- rel_apply_r (refines_rand_r (val_to_bool vs)).
+ rel_apply_r (refines_rand_r (extract_bool vs)).
repeat rel_pure_r.
iApply (refines_seq lrel_unit).
{ iApply refines_store.
diff --git a/theories/examples/or.v b/theories/examples/or.v
index a0562e2..080b9ff 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -1,6 +1,6 @@
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** (In)equational theory of erratic choice operator (`or`). *)
-From reloc Require Export reloc lib.Y (* for bot *).
+From reloc Require Export reloc lib.Y. (* for bot *)
Set Default Proof Using "Type".
(** (Binary) non-determinism can be simluated with concurrency. In
@@ -221,9 +221,9 @@ Section rules.
(** To prove the refinement in the other direction, we instrument
our program with prophecies and resolve them when we actually make
the choice on the LHS *)
- Definition to_choice (vs : list val) : bool :=
+ Definition to_choice (vs : list (val*val)) : bool :=
match vs with
- | LitV (LitInt 0)::_ => true
+ | (_,LitV (LitInt 0))::_ => true
| _ => false
end.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 1986990..683799b 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -521,7 +521,7 @@ Tactic Notation "rel_newproph_l_atomic" := rel_apply_l refines_newproph_l.
Lemma tac_rel_newproph_l_simpl `{relocG Σ} K ℶ1 ℶ2 e t A :
e = fill K NewProph →
MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
- (envs_entails ℶ2 (∀ (vs : list val) (p : proph_id),
+ (envs_entails ℶ2 (∀ (vs : list (val*val)) (p : proph_id),
(proph p vs -∗ refines ⊤ (fill K (of_val #p)) t A))) →
envs_entails ℶ1 (refines ⊤ e t A).
Proof.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index e77ff8c..e8f213f 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -335,7 +335,7 @@ Section rules.
Qed.
Lemma refines_newproph_l K E t A :
- (|={⊤,E}=> ▷ (∀ (vs : list val) (p : proph_id),
+ (|={⊤,E}=> ▷ (∀ (vs : list (val*val)) (p : proph_id),
proph p vs -∗
REL fill K (of_val #p) << t @ E : A))%I
-∗ REL fill K NewProph << t : A.
@@ -349,7 +349,7 @@ Section rules.
Lemma refines_resolveproph_l K E (p : proph_id) w t A :
(|={⊤,E}=> ∃ vs,
▷ (proph p vs) ∗
- ▷ (∀ (vs' : list val), ⌜vs = w::vs'⌠-∗
+ ▷ (∀ (vs' : list (val*val)), ⌜vs = (LitV LitUnit,w)::vs'⌠-∗
proph p vs' -∗
REL fill K (of_val #()) << t @ E : A))%I
-∗ REL fill K (ResolveProph #p w) << t : A.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 78b0437..08e4a31 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -134,6 +134,7 @@ Section rules.
iExists (<[j:=fill K #()]> tp), σ.
rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+ econstructor; eauto.
Qed.
(** Alloc, load, and store *)
@@ -320,4 +321,3 @@ Section rules.
Qed.
End rules.
-
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index 8b633b6..a69e74e 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -29,8 +29,9 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
| CasRCtx e0 e1 => CasRCtx (subst_map es e0) (subst_map es e1)
| FaaLCtx v2 => FaaLCtx v2
| FaaRCtx e1 => FaaRCtx (subst_map es e1)
- | ProphLCtx v2 => ProphLCtx v2
- | ProphRCtx e1 => ProphRCtx (subst_map es e1)
+ | ResolveLCtx Ki v1 v2 => ResolveLCtx (subst_map_ctx_item es Ki) v1 v2
+ | ResolveMCtx e0 v2 => ResolveMCtx (subst_map es e0) v2
+ | ResolveRCtx e0 e1 => ResolveRCtx (subst_map es e0) (subst_map es e1)
end.
Definition subst_map_ctx (es : stringmap val) (K : list ectx_item) :=
@@ -39,7 +40,7 @@ Definition subst_map_ctx (es : stringmap val) (K : list ectx_item) :=
Lemma subst_map_fill_item (vs : stringmap val) (Ki : ectx_item) (e : expr) :
subst_map vs (fill_item Ki e) =
fill_item (subst_map_ctx_item vs Ki) (subst_map vs e).
-Proof. induction Ki; simpl; eauto. Qed.
+Proof. induction Ki; simpl; eauto with f_equal. Qed.
Lemma subst_map_fill (vs : stringmap val) (K : list ectx_item) (e : expr) :
subst_map vs (fill K e) = fill (subst_map_ctx vs K) (subst_map vs e).
--
GitLab