client.v 1.34 KB
Newer Older
1
From barrier Require Import proof.
2
From program_logic Require Import auth sts saved_prop hoare ownership.
Ralf Jung's avatar
Ralf Jung committed
3
4
5
6
7
Import uPred.

Definition client := (let: "b" := newchan '() in wait "b")%L.

Section client.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
Ralf Jung's avatar
Ralf Jung committed
9
10
11
12
13
14
  Local Notation iProp := (iPropG heap_lang Σ).

  Lemma client_safe :
    heapN  N  heap_ctx heapN  || client {{ λ _, True }}.
  Proof.
    intros ?. rewrite /client.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
    ewp eapply (newchan_spec heapN N True%I); last done.
Ralf Jung's avatar
Ralf Jung committed
16
17
18
    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.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
    apply sep_mono_r, wand_intro_r. eauto.
Ralf Jung's avatar
Ralf Jung committed
20
21
  Qed.
End client.
22
23

Section ClosedProofs.
24
  Definition Σ : iFunctorG := #[ heapGF ; barrierGF ].
25
26
27
28
  Notation iProp := (iPropG heap_lang Σ).

  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
29
    apply ht_alt. rewrite (heap_alloc  (nroot .@ "Barrier")); last first.
30
    { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
Robbert Krebbers's avatar
Robbert Krebbers committed
31
      by move=>? _. }
32
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
    rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
34
    (* This, too, should be automated. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    by apply ndot_ne_disjoint.
36
37
38
39
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.