client.v 1.95 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From barrier Require Import barrier.
2
From program_logic Require Import auth sts saved_prop hoare ownership.
Ralf Jung's avatar
Ralf Jung committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(* 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.
21
    ewp eapply (newchan_spec N heapN True%I); last done.
Ralf Jung's avatar
Ralf Jung committed
22 23 24 25 26 27 28
    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.
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56

Section ClosedProofs.
  Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: authF (constF heapRA)
                                     .:: (λ _, constF unitRA) : iFunctorG.
  Notation iProp := (iPropG heap_lang Σ).

  Instance: authG heap_lang Σ heapRA.
  Proof. split; try apply _. by exists 2%nat. Qed.

  Instance: stsG heap_lang Σ barrier_proto.sts.
  Proof. split; try apply _. by exists 1%nat. Qed.

  Instance: savedPropG heap_lang Σ.
  Proof. by exists 0%nat. Qed.

  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
  Proof.
    apply ht_alt. rewrite (heap_alloc  (ndot nroot "Barrier")); last first.
    { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
      move=>? _. exact I. }
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
    rewrite -(client_safe (ndot nroot "Heap" ) (ndot nroot "Barrier" )) //.
    (* This, too, should be automated. *)
    apply ndot_ne_disjoint. discriminate.
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.