From 903cd502c8686b72cd31ce7c69921fe92daa9257 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Jun 2019 00:29:26 +0200
Subject: [PATCH] bump Iris for comparison changes
---
opam | 2 +-
theories/examples/various.v | 4 ++--
theories/lib/counter.v | 4 ++--
theories/lib/lock.v | 2 +-
theories/logic/proofmode/spec_tactics.v | 14 +++++++-------
theories/logic/proofmode/tactics.v | 14 +++++++-------
theories/logic/rules.v | 14 +++++++-------
theories/logic/spec_rules.v | 9 ++++-----
theories/typing/fundamental.v | 3 +--
9 files changed, 32 insertions(+), 34 deletions(-)
diff --git a/opam b/opam
index 9d113d2..a7cee3d 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-18.2.e039d7c7") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-18.8.72595700") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 43555ad..91f5495 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -202,14 +202,14 @@ Section proofs.
rel_cas_l_atomic.
iInv i3n as (n) "(Hx & Hx' & >Hbb)" "Hcl".
iDestruct "Hbb" as "[(Hb & Hb' & Hx1 & Hx'1) | (Hb & Hb')]"; last first.
- { iModIntro; iExists _; iFrame.
+ { iModIntro; iExists _; iFrame. simpl.
iSplitL; last by iIntros (?); congruence.
iIntros (?); iNext; iIntros "Hb".
rel_cas_fail_r; rel_if_r; rel_if_l.
iMod ("Hcl" with "[-]").
{ iNext. iExists n. iFrame. iRight. iFrame. }
rel_values. }
- { iModIntro. iExists _; iFrame.
+ { iModIntro. iExists _; iFrame. simpl.
iSplitR; first by iIntros (?); congruence.
iIntros (?); iNext; iIntros "Hb".
rel_cas_suc_r; rel_if_r; rel_if_l.
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index fba4c9f..703a0f4 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -102,14 +102,14 @@ Section CG_Counter.
repeat rel_pure_l. rel_cas_l_atomic.
iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
destruct (decide (n = n')); subst.
- - iExists #n'. iFrame.
+ - iExists #n'. iFrame. simpl.
iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
iIntros "_ !> Hx". simpl.
iDestruct "HQ" as "[_ HQ]".
replace (n' + 1)%Z with (1 + n')%Z; last by lia. (* TODO :( *)
iSpecialize ("HQ" with "[$Hx $HR]").
rel_if_true_l. by iApply "HQ".
- - iExists #n'. iFrame.
+ - iExists #n'. iFrame. simpl.
iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
iIntros "_ !> Hx". simpl.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 4036da7..e4b1a42 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -89,7 +89,7 @@ Section lockG_rules.
iDestruct "Hlock" as (l) "[% #?]". simplify_eq.
rel_cas_l_atomic.
iInv N as (b) "[Hl HR]" "Hclose".
- iModIntro. iExists _. iFrame.
+ iModIntro. iExists _. iFrame. simpl.
iSplit.
- iIntros (?). iNext. iIntros "Hl".
assert (b = true) as ->. { destruct b; congruence. }
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index dc0887d..1511b7e 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -257,7 +257,7 @@ Lemma tac_tp_cas_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 Ï i1 i2 i3 p K' e (l : l
IntoVal e1 v1 →
IntoVal e2 v2 →
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I →
- v' ≠v1 →
+ val_for_compare v' ≠val_for_compare v1 →
vals_cas_compare_safe v' v1 →
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j ⤇ fill K' #false)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3 →
@@ -300,8 +300,8 @@ Tactic Notation "tp_cas_fail" constr(j) :=
|iSolveTC
|iSolveTC
|iAssumptionCore || fail "tp_cas_fail: cannot find '? ↦ ?'"
- |try congruence (* v' ≠v1 *)
- |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
+ |try (simpl; congruence) (* v' ≠v1 *)
+ |try heap_lang.proofmode.solve_vals_cas_compare_safe
|pm_reflexivity || fail "tp_cas_fail: this should not happen"
|(* new goal *)]).
@@ -313,8 +313,8 @@ Lemma tac_tp_cas_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 Ï i1 i2 i3 p K' e (l : lo
IntoVal e1 v1 →
IntoVal e2 v2 →
envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I →
- v' = v1 →
- val_is_unboxed v1 →
+ val_for_compare v' = val_for_compare v1 →
+ vals_cas_compare_safe v' v1 →
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j ⤇ fill K' #true)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3 →
envs_entails Δ3 (|={E1,E2}=> Q) →
@@ -356,8 +356,8 @@ Tactic Notation "tp_cas_suc" constr(j) :=
|iSolveTC
|iSolveTC
|iAssumptionCore || fail "tp_cas_suc: cannot find '? ↦ ?'"
- |try congruence (* v' = v1 *)
- |try fast_done (* val_is_unboxed v1 *)
+ |try (simpl; congruence) (* v' = v1 *)
+ |try heap_lang.proofmode.solve_vals_cas_compare_safe
|pm_reflexivity || fail "tp_cas_suc: this should not happen"
|(* new goal *)]).
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 66a7b2f..eef8817 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -438,7 +438,7 @@ Lemma tac_rel_cas_fail_r `{relocG Σ} K ℶ1 i1 E (l : loc) e1 e2 v1 v2 v e t er
IntoVal e2 v2 →
nclose specN ⊆ E →
envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
- v ≠v1 →
+ val_for_compare v ≠val_for_compare v1 →
vals_cas_compare_safe v v1 →
eres = fill K #false →
envs_entails ℶ1 (refines E t eres A) →
@@ -457,8 +457,8 @@ Lemma tac_rel_cas_suc_r `{relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) e1 e2 v1 v2 v e
IntoVal e2 v2 →
nclose specN ⊆ E →
envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
- v = v1 →
- val_is_unboxed v1 →
+ val_for_compare v = val_for_compare v1 →
+ vals_cas_compare_safe v v1 →
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v2)) ℶ1 = Some ℶ2 →
eres = fill K #true →
envs_entails ℶ2 (refines E t eres A) →
@@ -488,8 +488,8 @@ Tactic Notation "rel_cas_fail_r" :=
(* the remaining goals are from tac_rel_cas_fail_r (except for the first one, which has already been solved by this point) *)
[solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
|solve_mapsto ()
- |try congruence (** v ≠v1 *)
- |try (fast_done || (left; fast_done) || (right; fast_done)) (** vals_cas_compare_safe *)
+ |try (simpl; congruence) (** v ≠v1 *)
+ |try heap_lang.proofmode.solve_vals_cas_compare_safe
|reflexivity
|rel_finish (** new goal *)].
@@ -509,8 +509,8 @@ Tactic Notation "rel_cas_suc_r" :=
(* the remaining goals are from tac_rel_cas_suc_r (except for the first one, which has already been solved by this point) *)
[solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
|solve_mapsto ()
- |try congruence (** v = v1 *)
- |try fast_done (** val_is_unboxed *)
+ |try (simpl; congruence) (** v = v1 *)
+ |try heap_lang.proofmode.solve_vals_cas_compare_safe
|pm_reflexivity (** new env *)
|reflexivity
|rel_finish (** new goal *)].
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index f0735a6..378f916 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -199,7 +199,7 @@ Section rules.
IntoVal e1 v1 →
IntoVal e2 v2 →
vals_cas_compare_safe v v1 →
- v ≠v1 →
+ val_for_compare v ≠val_for_compare v1 →
l ↦ₛ v -∗
(l ↦ₛ v -∗ REL t << fill K (of_val #false) @ E : A)
-∗ REL t << fill K (CAS #l e1 e2) @ E : A.
@@ -220,8 +220,8 @@ Section rules.
nclose specN ⊆ E →
IntoVal e1 v1 →
IntoVal e2 v2 →
- val_is_unboxed v1 →
- v = v1 →
+ vals_cas_compare_safe v v1 →
+ val_for_compare v = val_for_compare v1 →
l ↦ₛ v -∗
(l ↦ₛ v2 -∗ REL t << fill K (of_val #true) @ E : A)
-∗ REL t << fill K (CAS #l e1 e2) @ E : A.
@@ -390,17 +390,17 @@ Section rules.
IntoVal e2 v2 →
val_is_unboxed v1 →
(|={⊤,E}=> ∃ v', ▷ l ↦ v' ∗
- (⌜v' ≠v1⌠-∗ ▷ (l ↦ v' -∗ REL fill K (of_val #false) << t @ E : A)) ∧
- (⌜v' = v1⌠-∗ ▷ (l ↦ v2 -∗ REL fill K (of_val #true) << t @ E : A)))
+ (⌜val_for_compare v' ≠val_for_compare v1⌠-∗ ▷ (l ↦ v' -∗ REL fill K (of_val #false) << t @ E : A)) ∧
+ (⌜val_for_compare v' = val_for_compare v1⌠-∗ ▷ (l ↦ v2 -∗ REL fill K (of_val #true) << t @ E : A)))
-∗ REL fill K (CAS #l e1 e2) << t : A.
Proof.
iIntros (<-<-?) "Hlog".
iApply refines_atomic_l; auto.
iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
- destruct (decide (v' = v1)).
+ destruct (decide (val_for_compare v' = val_for_compare v1)).
- (* CAS successful *) subst.
iApply (wp_cas_suc with "Hl"); eauto.
- { by left. }
+ { by right. }
iDestruct "Hlog" as "[_ Hlog]".
iSpecialize ("Hlog" with "[]"); eauto.
- (* CAS failed *)
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index ea219b9..85de095 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -218,7 +218,7 @@ Section rules.
IntoVal e2 v2 →
nclose specN ⊆ E →
vals_cas_compare_safe v' v1 →
- v' ≠v1 →
+ val_for_compare v' ≠val_for_compare v1 →
spec_ctx Ï âˆ— j ⤇ fill K (CAS #l e1 e2) ∗ l ↦ₛ{q} v'
={E}=∗ j ⤇ fill K #false ∗ l ↦ₛ{q} v'.
Proof.
@@ -242,12 +242,12 @@ Section rules.
IntoVal e1 v1 →
IntoVal e2 v2 →
nclose specN ⊆ E →
- val_is_unboxed v1 →
- v1 = v1' →
+ vals_cas_compare_safe v1' v1 →
+ val_for_compare v1' = val_for_compare v1 →
spec_ctx Ï âˆ— j ⤇ fill K (CAS #l e1 e2) ∗ l ↦ₛ v1'
={E}=∗ j ⤇ fill K #true ∗ l ↦ₛ v2.
Proof.
- iIntros (<-<-??<-) "(#Hinv & Hj & Hl)"; subst.
+ iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst.
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
@@ -265,7 +265,6 @@ Section rules.
iExists (<[j:=fill K (# true)]> tp), (state_upd_heap <[l:=v2]> σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
- left; eauto.
Qed.
Lemma step_faa E Ï j K l e1 e2 (i1 i2 : Z) :
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 77ede4c..3aa081a 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -295,7 +295,7 @@ Section fundamental.
simplify_eq. rel_cas_l_atomic.
iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #Hv]]" "Hclose".
iModIntro. iExists _; iFrame. simpl.
- destruct (decide (v1 = v2')) as [|Hneq]; subst.
+ destruct (decide (val_for_compare v1 = val_for_compare v2')) as [|Hneq]; subst.
- iSplitR; first by (iIntros (?); contradiction).
iIntros (?). iNext. iIntros "Hv1".
iDestruct (eq_type_sound with "Hv") as "%"; first fast_done.
@@ -513,4 +513,3 @@ Section fundamental.
Qed.
End fundamental.
-
--
GitLab