sort_elem_client.v 3.14 KB
Newer Older
1
From stdpp Require Import sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From actris.channel Require Import proto_channel proofmode.
3 4
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
From actris.utils Require Import list compare.
From actris.examples Require Import sort_elem.
7 8 9 10 11

Definition send_all : val :=
  rec: "go" "c" "xs" :=
    match: "xs" with
      SOME "p" => send "c" #cont;; send "c" (Fst "p");; "go" "c" (Snd "p")
Robbert Krebbers's avatar
Robbert Krebbers committed
12
    | NONE => #()
13 14 15 16 17
    end.

Definition recv_all : val :=
  rec: "go" "c" :=
    if: recv "c"
18
    then let: "x" := recv "c" in lcons "x" ("go" "c")
19 20
    else lnil #().

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Definition sort_elem_client : val :=
22
  λ: "cmp" "xs",
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    let: "c" := start_chan sort_elem_service_top in
24
    send "c" "cmp";;
25
    send_all "c" "xs";;
Robbert Krebbers's avatar
Robbert Krebbers committed
26
    send "c" #stop;;
27 28
    recv_all "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
29
Section sort_elem_client.
30
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
31
  Context {A} (I : A  val  iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
32

33
  Lemma send_all_spec c p xs' xs vs :
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    {{{ c  sort_elem_head_protocol I R xs' <++> p @ N  [ list] x;v  xs;vs, I x v }}}
35
      send_all c (llist vs)
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    {{{ RET #(); c  sort_elem_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
37 38 39
  Proof.
    iIntros (Φ) "[Hc HI] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs' vs); destruct vs as [|v vs]=>//.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
    { wp_lam; wp_pures. iApply "HΦ". rewrite right_id_L. iFrame. }
41 42 43 44
    iDestruct "HI" as "[HIxv HI]". wp_lam; wp_pures.
    wp_select. wp_send with "[$HIxv]". wp_apply ("IH" with "Hc HI").
    by rewrite -assoc_L.
  Qed.
45

Robbert Krebbers's avatar
Robbert Krebbers committed
46 47
  Lemma recv_all_spec c p xs ys' :
    Sorted R ys' 
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    {{{ c  sort_elem_tail_protocol I R xs ys' <++> p @ N }}}
49
      recv_all c
50
    {{{ ys ws, RET (llist ws);
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
        Sorted R (ys' ++ ys)  ys' ++ ys  xs 
        c  p @ N  [ list] y;w  ys;ws, I y w
53
    }}}.
54 55
  Proof.
    iIntros (Hsort Φ) "Hc HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
56
    iLöb as "IH" forall (xs ys' Φ Hsort).
57
    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
58 59
    - wp_recv (y v) as (Htl) "HIxv".
      wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
      iIntros (ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
61
      wp_apply (lcons_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
      iApply ("HΦ" $! (y :: ys)). simpl; iFrame; auto.
63 64 65
    - wp_apply (lnil_spec with "[//]"); iIntros (_).
      iApply ("HΦ" $! [] []); rewrite /= right_id_L; by iFrame.
  Qed.
66

Robbert Krebbers's avatar
Robbert Krebbers committed
67
  Lemma sort_client_spec cmp vs xs :
68 69
    cmp_spec I R cmp -
    {{{ [ list] x;v  xs;vs, I x v }}}
70 71
      sort_elem_client cmp (llist vs)
    {{{ ys ws, RET (llist ws); Sorted R ys  ys  xs 
72 73
               [ list] y;w  ys;ws, I y w }}}.
  Proof.
74
    iIntros "#Hcmp !>" (Φ) "HI HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
    wp_apply (start_chan_proto_spec N (sort_elem_top_protocol <++> END)%proto);
76
      iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
    { wp_apply (sort_elem_service_top_spec N with "Hc"); auto. }
    rewrite /sort_elem_top_protocol.
79 80
    wp_send (A I R) with "[$Hcmp]".
    wp_apply (send_all_spec with "[$HI $Hc]"); iIntros "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    wp_select.
82 83 84
    wp_apply (recv_all_spec _ _ _ [] with "[$Hc]"); auto.
    iIntros (ys ws) "/=". iDestruct 1 as (??) "[_ HI]".
    iApply "HΦ"; auto.
85
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
End sort_elem_client.