From fc7bdf6708807c6d87b16ceed3a8391d893c4abf Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Fri, 16 Feb 2018 16:29:02 +0100
Subject: [PATCH] Port tests/message_passing.v.

---
 theories/tests/message_passing.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/theories/tests/message_passing.v b/theories/tests/message_passing.v
index 648fc9ae..518033fc 100644
--- a/theories/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -18,7 +18,7 @@ Next Obligation.
 Qed.
 
 Lemma message_passing :
-  adequate (message_passing, ∅) initial_state (λ v, v.1 = LitV (LitInt 37)).
+  adequate NotStuck (message_passing, ∅) initial_state (λ v, v.1 = LitV (LitInt 37)).
 Proof.
   apply (base_adequacy Σ _ ∅); auto.
   - split; repeat red; rewrite /initial_state /=; try set_solver.
@@ -29,9 +29,13 @@ Proof.
     last iMod (persistor_init with "PS") as (?) "#Pers".
     { by auto. }
     iModIntro.
-    iApply (message_passing_spec ∅ with "[%] PS Seen Pers").
-    { reflexivity. }
-    iNext. iViewUp. iIntros (v) "? %". by subst.
+    iPoseProof (message_passing_spec (fun v => ⌜v = #37⌝)%I with "[$PS $Pers]") as "T".
+    iSpecialize ("T" $! ∅ with "[%]"); [reflexivity|].
+    rewrite WP_Def.wp_eq /WP_Def.wp_def. cbn.
+    iApply wp_mono; cycle 1.
+    + iApply "T"; [|done|done].
+      iNext. iIntros. iPureIntro. intros []. done.
+    + iIntros ([v ?]) "[_ %]". subst v. done.
 Qed.
 
 Print Assumptions message_passing.
-- 
GitLab