From e70f486ed4b5a7fb030be6e94abaaee5b33a4f0e Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Wed, 27 Mar 2019 15:08:15 +0100
Subject: [PATCH] Fix atomic snapshot example
---
opam | 2 +-
theories/logatom/snapshot/atomic_snapshot.v | 12 ++++++------
2 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/opam b/opam
index b8bd54fb..e4c60130 100644
--- a/opam
+++ b/opam
@@ -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-03-14.3.2d1c8352") | (= "dev") }
+ "coq-iris" { (= "dev.2019-03-26.0.0495f119") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 0f91a22b..5a59300e 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -365,10 +365,10 @@ Section atomic_snapshot.
wp_load. eauto.
Qed.
- Definition val_to_bool (v : option val) : bool :=
+ Definition val_list_to_bool (v : list val) : bool :=
match v with
- | Some (LitV (LitBool b)) => b
- | _ => false
+ | LitV (LitBool b) :: _ => b
+ | _ => false
end.
Lemma readPair_spec γ p :
@@ -413,7 +413,7 @@ Section atomic_snapshot.
iMod "AU" as (xv yv) "[Hpair Hclose]".
rewrite /pair_content.
iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- destruct (val_to_bool proph_val) eqn:Hproph.
+ destruct (val_list_to_bool proph_val) eqn:Hproph.
- (* prophecy value is predicting that timestamp has not changed, so we commit *)
(* committing AU *)
iMod ("Hclose" with "Hpair") as "HΦ".
@@ -443,7 +443,7 @@ Section atomic_snapshot.
}
wp_load. wp_let. wp_proj. wp_let. wp_proj. wp_op.
case_bool_decide; wp_let; wp_apply (wp_resolve_proph with "Hpr");
- iIntros (->); wp_seq; wp_if.
+ iIntros (vs') "[Eq _]"; iDestruct "Eq" as %->; wp_seq; wp_if.
+ inversion H; subst; clear H. wp_pures.
assert (v_x2 = v_y) as ->. {
assert (v_x2 <= v_y) as vneq. {
@@ -479,7 +479,7 @@ Section atomic_snapshot.
}
wp_load. repeat (wp_let; wp_proj). wp_op. wp_let.
wp_apply (wp_resolve_proph with "Hpr").
- iIntros (Heq). subst.
+ iIntros (vs') "[Heq _]"; iDestruct "Heq" as %->.
case_bool_decide.
+ inversion H; subst; clear H. inversion Hproph.
+ wp_seq. wp_if. iApply "IH"; rewrite /is_pair; eauto.
--
GitLab