Add closed proof of message passing example.

coq/ra/_CoqProject

@@ -62,3 +62,4 @@ examples/message_passing.v
 examples/spin_lock.v
 examples/circ_buffer.v
 examples/ticket_lock.v
+tests/message_passing.v

coq/ra/tests/message_passing.v

+From iris.heap_lang Require Import adequacy.
+From ra.examples Require Import message_passing.
+From ra.gps Require Import shared inst_shared.
+From ra Require Import adequacy.
+
+Let Σ : gFunctors := #[ baseΣ;
+                        gpsΣ protocols.boolProtocol _ ;
+                        gps_agreeΣ protocols.boolProtocol _;
+                        absViewΣ;
+                        persistorΣ;
+                        mpΣ ].
+
+Program Definition initial_state :=
+  {| threads := {[ 1%positive := ∅ ]};
+     mem := mkMemory ∅ (_);
+     nats := ∅ |}.
+Next Obligation.
+  rewrite /pairwise_disj. set_solver.
+Qed.
+
+Lemma message_passing :
+  adequate (message_passing, 1%positive) initial_state (λ v, v = (LitV (LitInt 37), 1%positive)).
+Proof.
+  apply (base_adequacy Σ _ ∅); auto.
+  - split; repeat red; rewrite /initial_state /=; try set_solver.
+    intros ? ?. case: (decide (π = 1%positive)) => [->|?].
+    + rewrite lookup_singleton. move => [<- {V}]. set_solver.
+    + rewrite lookup_singleton_ne //.
+  - iIntros (?) "[#PS Seen]".
+    iApply fupd_wp.
+    iApply fupd_mask_mono;
+    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.
+Qed.
+
+Print Assumptions message_passing.
\ No newline at end of file