Commit e7f21fde authored by Ralf Jung's avatar Ralf Jung

add a (dummy) client

parent d4fd7c20
...@@ -81,3 +81,4 @@ heap_lang/notation.v ...@@ -81,3 +81,4 @@ heap_lang/notation.v
heap_lang/tests.v heap_lang/tests.v
heap_lang/substitution.v heap_lang/substitution.v
barrier/barrier.v barrier/barrier.v
barrier/client.v
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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment