From e7f21fde0eae40142b96a2a0ecbc669ce257c0e0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 10:29:29 +0100
Subject: [PATCH] add a (dummy) client

---
 _CoqProject      |  1 +
 barrier/client.v | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 barrier/client.v

diff --git a/_CoqProject b/_CoqProject
index baef6bf5b..0b2786915 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -81,3 +81,4 @@ heap_lang/notation.v
 heap_lang/tests.v
 heap_lang/substitution.v
 barrier/barrier.v
+barrier/client.v
diff --git a/barrier/client.v b/barrier/client.v
new file mode 100644
index 000000000..2d11a0135
--- /dev/null
+++ b/barrier/client.v
@@ -0,0 +1,29 @@
+From barrier Require Import barrier.
+(* FIXME This needs to be imported even though barrier exports it *)
+From heap_lang Require Import notation.
+Import uPred.
+
+Definition client := (let: "b" := newchan '() in wait "b")%L.
+
+Section client.
+  Context {Σ : iFunctorG} (N : namespace).
+  Context `{heapG Σ} (heapN : namespace).
+  Context `{stsG heap_lang Σ barrier_proto.sts}.
+  Context `{savedPropG heap_lang Σ}.
+
+  Local Notation iProp := (iPropG heap_lang Σ).
+
+  Lemma client_safe :
+    heapN ⊥ N → heap_ctx heapN ⊑ || client {{ λ _, True }}.
+  Proof.
+    intros ?. rewrite /client.
+    (* FIXME: wp (eapply newchan_spec with (P:=True%I)). *)
+    wp_focus (newchan _).
+    rewrite -(newchan_spec N heapN True%I) //.
+    apply sep_intro_True_r; first done.
+    apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
+    wp_let. etrans; last eapply wait_spec.
+    apply sep_mono_r. apply wand_intro_r. eauto.
+  Qed.
+
+End client.
-- 
GitLab