sort_fg_client.v 2.96 KB
Newer Older
1
From stdpp Require Import sorting.
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.
5
From actris.utils Require Import llist compare.
6
From actris.examples Require Export sort_fg.
7 8 9

Definition send_all : val :=
  rec: "go" "c" "xs" :=
10 11
    if: lisnil "xs" then #() else
    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
12 13

Definition recv_all : val :=
14 15
  rec: "go" "c" "ys" :=
    if: ~recv "c" then #() else
16
    let: "x" := recv "c" in
17
    "go" "c" "ys";; lcons "x" "ys".
18

19 20 21 22
Definition sort_client_fg : val := λ: "cmp" "xs",
  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
  send_all "c" "xs";;
  send "c" #stop;;
23
  recv_all "c" "xs".
24

25
Section sort_fg_client.
26
  Context `{!heapG Σ, !proto_chanG Σ}.
27
  Context {A} (I : A  val  iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
28

Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Lemma send_all_spec c p xs' l xs :
30
    {{{ llist I l xs  c  (sort_fg_head_protocol I R xs' <++> p) }}}
31
      send_all c #l
32
    {{{ RET #(); llist I l []  c  (sort_fg_head_protocol I R (xs' ++ xs) <++> p) }}}.
33
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
    iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs').
36 37
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
      iApply "HΦ". rewrite right_id_L. iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40
    wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
    wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
    wp_send with "[$HIx]". wp_apply ("IH" with "Hl Hc"). by rewrite -assoc_L.
41
  Qed.
42

43
  Lemma recv_all_spec c p l xs ys' :
44
    Sorted R ys' 
45
    {{{ llist I l []  c  (sort_fg_tail_protocol I R xs ys' <++> p) }}}
46 47
      recv_all c #l
    {{{ ys, RET #();
48
        Sorted R (ys' ++ ys)  ys' ++ ys ≡ₚ xs  llist I l ys  c  p
49
    }}}.
50
  Proof.
51
    iIntros (Hsort Φ) "[Hl Hc] HΦ".
52
    iLöb as "IH" forall (xs ys' Φ Hsort).
53
    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
    - wp_recv (y v) as (Htl) "HIx".
55 56
      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
      iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
      iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
59
    - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
60
  Qed.
61

62
  Lemma sort_client_fg_spec cmp l xs :
63
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
64
    {{{ llist I l xs }}}
65
      sort_client_fg cmp #l
66
    {{{ ys, RET #(); Sorted R ys  ys ≡ₚ xs  llist I l ys }}}.
67
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
69
    wp_apply (start_chan_proto_spec (sort_fg_protocol I R <++> END)%proto);
70
      iIntros (c) "Hc".
71
    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
72
    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
73
    wp_select.
74 75
    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
    iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
76
    iApply "HΦ"; auto with iFrame.
77
  Qed.
78
End sort_fg_client.