sort.v 5.94 KB
Newer Older
1
(** This file implements a distributed Merge Sort,
jihgfee's avatar
jihgfee committed
2
3
4
a specification thereof and its proofs, including
a variant in which the comparison function is sent
over the channel. *)
5
From stdpp Require Import sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From actris.channel Require Import proto_channel proofmode.
7
From iris.heap_lang Require Import proofmode notation.
8
From actris.utils Require Export llist compare.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Definition lmerge : val :=
11
  rec: "go" "cmp" "ys" "zs" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
    if: lisnil "ys" then lapp "ys" "zs" else
    if: lisnil "zs" then #() else
14
15
16
    let: "y" := lhead "ys" in
    let: "z" := lhead "zs" in
    if: "cmp" "y" "z"
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
    then lpop "ys";; "go" "cmp" "ys" "zs";; lcons "y" "ys"
    else lpop "zs";; "go" "cmp" "ys" "zs";; lcons "z" "ys".
Robbert Krebbers's avatar
Robbert Krebbers committed
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20
Definition sort_service : val :=
21
  rec: "go" "cmp" "c" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
22
    let: "xs" := recv "c" in
23
24
    if: llength "xs"  #1 then send "c" #() else
    let: "zs" := lsplit "xs" in
25
26
27
28
    let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
    let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
    send "cy" "xs";;
    send "cz" "zs";;
Robbert Krebbers's avatar
Robbert Krebbers committed
29
    recv "cy";; recv "cz";;
30
    lmerge "cmp" "xs" "zs";;
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
    send "c" #().

33
34
35
36
37
38
39
40
41
Definition sort_service_func : val := λ: "c",
  let: "cmp" := recv "c" in
  sort_service "cmp" "c".

Definition sort_client_func : val := λ: "cmp" "xs",
  let: "c" := start_chan sort_service_func in
  send "c" "cmp";; send "c" "xs";;
  recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
42
Section sort.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Context `{!heapG Σ, !proto_chanG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
44

45
46
47
48
49
50
51
  Definition sort_protocol {A} (I : A  val  iProp Σ) (R : A  A  Prop)
      `{!RelDecision R, !Total R} : iProto Σ :=
    (<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
     <?> (xs' : list A), MSG #() {{  Sorted R xs'    xs'  xs   llist I l xs' }};
     END)%proto.

  Definition sort_protocol_func : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
52
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
53
         `{!RelDecision R, !Total R} (cmp : val),
Robbert Krebbers's avatar
Robbert Krebbers committed
54
       MSG cmp {{ cmp_spec I R cmp }};
55
     sort_protocol I R)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57

  Lemma lmerge_spec {A} (I : A  val  iProp Σ) (R : A  A  Prop)
Robbert Krebbers's avatar
Robbert Krebbers committed
58
      `{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
59
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    {{{ llist I l1 xs1  llist I l2 xs2 }}}
61
      lmerge cmp #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    {{{ RET #(); llist I l1 (list_merge R xs1 xs2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
    iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
    iLöb as "IH" forall (l2 xs1 xs2 Ψ).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
    wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    destruct xs1 as [|x1 xs1]; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
    { wp_apply (lapp_spec with "[$Hl1 $Hl2]"); iIntros "[Hl1 _] /=".
      iApply "HΨ". iFrame. by rewrite list_merge_nil_l. }
    wp_apply (lisnil_spec with "Hl2"); iIntros "Hl2".
Robbert Krebbers's avatar
Robbert Krebbers committed
71
    destruct xs2 as [|x2 xs2]; wp_pures.
72
    { iApply "HΨ". iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
75
    wp_apply (lhead_spec_aux with "Hl1"); iIntros (v1 l1') "[HIx1 Hl1]".
    wp_apply (lhead_spec_aux with "Hl2"); iIntros (v2 l2') "[HIx2 Hl2]".
    wp_apply ("Hcmp" with "[$HIx1 $HIx2]"); iIntros "[HIx1 HIx2] /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
    case_bool_decide; wp_pures.
    - rewrite decide_True //.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
80
81
82
      wp_apply (lpop_spec_aux with "Hl1"); iIntros "Hl1".
      wp_apply ("IH" $! _ _ (_ :: _) with "Hl1 [HIx2 Hl2]").
      { iExists _, _. iFrame. }
      iIntros "Hl1".
      wp_apply (lcons_spec with "[$Hl1 $HIx1]"). iIntros "Hl1". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
    - rewrite decide_False //.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
      wp_apply (lpop_spec_aux with "Hl2"); iIntros "Hl2".
      wp_apply ("IH" $! _ (_ :: _) with "[HIx1 Hl1] Hl2").
      { iExists _, _. iFrame. }
      iIntros "Hl1".
      wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  Qed.
90

91
92
93
  Lemma sort_service_spec {A} (I : A  val  iProp Σ) (R : A  A  Prop)
      `{!RelDecision R, !Total R} (cmp : val) p c :
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
94
    {{{ c  (iProto_dual (sort_protocol I R) <++> p) }}}
95
      sort_service cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    {{{ RET #(); c  p }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proof.
98
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
    wp_recv (xs l) as "Hl".
100
    wp_apply (llength_spec with "Hl"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
103
    wp_op; case_bool_decide as Hlen; wp_if.
    { assert (Sorted R xs).
      { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
Robbert Krebbers's avatar
Robbert Krebbers committed
104
      wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
105
106
    wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
      iDestruct 1 as (->) "[Hl1 Hl2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
107
    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cy) "Hcy".
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
      wp_apply ("IH" with "Hcy"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
110
    wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
      wp_apply ("IH" with "Hcz"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
115
116
117
118
    wp_send with "[$Hl1]".
    wp_send with "[$Hl2]".
    wp_recv (ys1) as (??) "Hl1".
    wp_recv (ys2) as (??) "Hl2".
    wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2]"); iIntros "Hl".
    wp_send ((list_merge R ys1 ys2)) with "[$Hl]".
119
120
121
122
    - iSplit; iPureIntro.
      + by apply (Sorted_list_merge _).
      + rewrite (merge_Permutation R). by f_equiv.
    - by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  Qed.
124
125

  Lemma sort_service_func_spec p c :
Robbert Krebbers's avatar
Robbert Krebbers committed
126
    {{{ c  (iProto_dual sort_protocol_func <++> p) }}}
127
      sort_service_func c
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    {{{ RET #(); c  p }}}.
129
130
131
132
133
134
135
136
137
138
139
140
141
142
  Proof.
    iIntros (Ψ) "Hc HΨ". wp_lam.
    wp_recv (A I R ?? cmp) as "#Hcmp".
    by wp_apply (sort_service_spec with "Hcmp Hc").
  Qed.

  Lemma sort_client_func_spec {A} (I : A  val  iProp Σ) R
       `{!RelDecision R, !Total R} cmp l (xs : list A) :
    cmp_spec I R cmp -
    {{{ llist I l xs }}}
      sort_client_func cmp #l
    {{{ ys, RET #(); Sorted R ys  ys  xs  llist I l ys }}}.
  Proof.
    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
144
145
    { rewrite -(right_id END%proto _ (iProto_dual _)).
      wp_apply (sort_service_func_spec with "Hc"); auto. }
146
    (* TODO: This needs explicit (A I R) after Coq 8.10. Figure out why *)
Jonas Kastberg's avatar
Jonas Kastberg committed
147
    wp_send (A I R) with "[$Hcmp]".
148
149
150
151
    wp_send with "[$Hl]".
    wp_recv (ys) as "(Hsorted & Hperm & Hl)".
    wp_pures. iApply "HΦ"; iFrame.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
End sort.