From 817a80f9f8c6bb8615795fb4c247d644259bb072 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 14:10:52 +0100
Subject: [PATCH] state the theorem we want to prove

---
 barrier/barrier.v    | 24 ++++++++++++++++++++++++
 heap_lang/notation.v |  3 ++-
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index b18b25fa7..eecd0a8d1 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -123,5 +123,29 @@ Section proof.
     (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts.in_states StsI sts γ (i_states i) {[ Change i ]} ★
         saved_prop_own SpI i Q ★ ▷(Q -★ R))%I.
     
+  Lemma newchan_spec (P : iProp) (Q : val → iProp) :
+    (∀ l, recv l P ★ send l P -★ Q (LocV l)) ⊑ wp coPset_all (newchan '()) Q.
+  Proof.
+  Abort.
+
+  Lemma signal_spec l P (Q : val → iProp) :
+    (send l P ★ P ★ Q '()) ⊑ wp coPset_all (signal (LocV l)) Q.
+  Proof.
+  Abort.
+
+  Lemma wait_spec l P (Q : val → iProp) :
+    (recv l P ★ (P -★ Q '())) ⊑ wp coPset_all (wait (LocV l)) Q.
+  Proof.
+  Abort.
+
+  Lemma split_spec l P1 P2 Q :
+    (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Q '())) ⊑ wp coPset_all Skip Q.
+  Proof.
+  Abort.
+
+  Lemma recv_strengthen l P1 P2 :
+    (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
+  Proof.
+  Abort.
 
 End proof.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 20bc92f40..30db88cc8 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -20,7 +20,8 @@ Coercion of_val : val >-> expr.
    pretty printing. *)
 Notation "' l" := (Lit l%Z) (at level 8, format "' l").
 Notation "' l" := (LitV l%Z) (at level 8, format "' l").
-Notation "()"  := LitUnit  (at level 0) : lang_scope.
+Notation "'()"  := (Lit LitUnit) (at level 0).
+Notation "'()"  := (LitV LitUnit) (at level 0).
 Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
 Notation "'ref' e" := (Alloc e%L)
   (at level 30, right associativity) : lang_scope.
-- 
GitLab