sort_fg.v 12 KB
Newer Older
1
2
(** This file implements a fine-grained Merge Sort,
a specification thereof and its proofs. *)
3
From stdpp Require Export sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.channel Require Import proto_channel proofmode.
jihgfee's avatar
jihgfee committed
5
6
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
jihgfee's avatar
jihgfee committed
7
From actris.utils Require Import llist compare.
jihgfee's avatar
jihgfee committed
8

jihgfee's avatar
jihgfee committed
9
10
11
Definition cont := true.
Definition stop := false.

12
Definition sort_service_fg_split : val :=
jihgfee's avatar
jihgfee committed
13
  rec: "go" "c" "c1" "c2" :=
14
15
16
17
    if: ~(recv "c") then send "c1" #stop;; send "c2" #stop else
    let: "x" := recv "c" in
    send "c1" #cont;; send "c1" "x";;
    "go" "c" "c2" "c1".
jihgfee's avatar
jihgfee committed
18

Robbert Krebbers's avatar
Robbert Krebbers committed
19
Definition sort_service_fg_forward : val :=
jihgfee's avatar
jihgfee committed
20
  rec: "go" "c" "cin" :=
21
22
23
24
    if: ~(recv "cin") then send "c" #stop else
    let: "x" := recv "cin" in
    send "c" #cont;; send "c" "x";;
    "go" "c" "cin".
jihgfee's avatar
jihgfee committed
25

26
Definition sort_service_fg_merge : val :=
27
28
29
  rec: "go" "cmp" "c" "x1" "c1" "c2" :=
    if: ~recv "c2" then
      send "c" #cont;; send "c" "x1";;
Robbert Krebbers's avatar
Robbert Krebbers committed
30
      sort_service_fg_forward "c" "c1"
31
32
33
34
35
36
    else
      let: "x2" := recv "c2" in
      if: "cmp" "x1" "x2" then
        send "c" #cont;; send "c" "x1";; "go" "cmp" "c" "x2" "c2" "c1"
      else
        send "c" #cont;; send "c" "x2";; "go" "cmp" "c" "x1" "c1" "c2".
jihgfee's avatar
jihgfee committed
37

38
Definition sort_service_fg : val :=
39
40
41
42
43
  rec: "go" "cmp" "c" :=
    if: ~(recv "c") then send "c" #stop else
    let: "x" := recv "c" in
    if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
    let: "y" := recv "c" in
44
45
    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
46
47
    send "c1" #cont;; send "c1" "x";;
    send "c2" #cont;; send "c2" "y";;
48
    sort_service_fg_split "c" "c1" "c2";;
49
    let: "x" := (if: recv "c1" then recv "c1" else assert #false) in
50
    sort_service_fg_merge "cmp" "c" "x" "c1" "c2".
51

52
Definition sort_service_fg_func : val := λ: "c",
53
  let: "cmp" := recv "c" in
54
  sort_service_fg "cmp" "c".
55

jihgfee's avatar
jihgfee committed
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
Definition send_all : val :=
  rec: "go" "c" "xs" :=
    if: lisnil "xs" then #() else
    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".

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

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;;
  recv_all "c" "xs".

73
Section sort_fg.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Context `{!heapG Σ, !proto_chanG Σ}.
75

76
  Section sort_fg_inner.
77
  Context {A} (I : A  val  iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
jihgfee's avatar
jihgfee committed
78

79
  Definition sort_fg_tail_protocol_aux (xs : list A)
80
81
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ ys,
    ((<?> y v, MSG v {{  TlRel R y ys   I y v }}; (rec : _  iProto Σ) (ys ++ [y]))
82
     <&{ ys  xs }> END)%proto.
jihgfee's avatar
jihgfee committed
83

84
85
  Instance sort_fg_tail_protocol_aux_contractive xs :
    Contractive (sort_fg_tail_protocol_aux xs).
86
  Proof. solve_proto_contractive. Qed.
87
88
89
90
91
92
93
94
  Definition sort_fg_tail_protocol (xs : list A) : list A  iProto Σ :=
    fixpoint (sort_fg_tail_protocol_aux xs).
  Global Instance sort_fg_tail_protocol_unfold xs ys :
    ProtoUnfold (sort_fg_tail_protocol xs ys)
      (sort_fg_tail_protocol_aux xs (sort_fg_tail_protocol xs) ys).
  Proof. apply proto_unfold_eq, (fixpoint_unfold (sort_fg_tail_protocol_aux _)). Qed.

  Definition sort_fg_head_protocol_aux
95
96
      (rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
    ((<!> x v, MSG v {{ I x v }}; (rec : _  iProto Σ) (xs ++ [x]))
97
     <+> sort_fg_tail_protocol xs [])%proto.
98

99
100
  Instance sort_fg_head_protocol_aux_contractive :
    Contractive sort_fg_head_protocol_aux.
101
  Proof. solve_proto_contractive. Qed.
102

103
104
105
106
107
108
  Definition sort_fg_head_protocol : list A  iProto Σ :=
    fixpoint sort_fg_head_protocol_aux.
  Global Instance sort_fg_head_protocol_unfold xs :
    ProtoUnfold (sort_fg_head_protocol xs)
      (sort_fg_head_protocol_aux sort_fg_head_protocol xs).
  Proof. apply proto_unfold_eq, (fixpoint_unfold sort_fg_head_protocol_aux). Qed.
jihgfee's avatar
jihgfee committed
109

110
  Definition sort_fg_protocol : iProto Σ := sort_fg_head_protocol [].
111

112
  Lemma sort_service_fg_split_spec c p c1 c2 xs xs1 xs2 :
jihgfee's avatar
jihgfee committed
113
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
      c  (iProto_dual (sort_fg_head_protocol xs) <++> p) 
      c1  sort_fg_head_protocol xs1  c2  sort_fg_head_protocol xs2
116
    }}}
117
      sort_service_fg_split c c1 c2
jihgfee's avatar
jihgfee committed
118
    {{{ xs' xs1' xs2', RET #();
119
      xs'  xs1' ++ xs2' 
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
      c  (iProto_dual (sort_fg_tail_protocol (xs ++ xs') []) <++> p) 
      c1  sort_fg_tail_protocol (xs1 ++ xs1') [] 
      c2  sort_fg_tail_protocol (xs2 ++ xs2') []
123
    }}}.
jihgfee's avatar
jihgfee committed
124
125
  Proof.
    iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
126
    wp_rec. wp_branch.
127
    - wp_recv (x v) as "HI". wp_select. wp_send with "[$HI]".
128
129
130
131
      wp_apply ("IH" with "Hc Hc2 Hc1").
      iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
      rewrite -!(assoc_L (++)).
      iApply "HΨ". iFrame "Hc Hc1 Hc2". by rewrite Hxs' (comm (++) xs1') assoc_L.
132
    - wp_select. wp_select.
133
      iApply ("HΨ" $! [] [] []). rewrite !right_id_L. by iFrame.
jihgfee's avatar
jihgfee committed
134
  Qed.
jihgfee's avatar
jihgfee committed
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
  Lemma sort_service_fg_forward_spec c p cin xs ys zs xs' ys' :
137
138
    xs  xs' ++ zs 
    ys  ys' ++ zs 
139
140
    Sorted R ys 
    ( x, TlRel R x ys'  TlRel R x ys) 
jihgfee's avatar
jihgfee committed
141
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
      c  (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) 
      cin  sort_fg_tail_protocol xs' ys'
jihgfee's avatar
jihgfee committed
144
    }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
145
      sort_service_fg_forward c cin
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    {{{ RET #(); c  p  cin  END }}}.
jihgfee's avatar
jihgfee committed
147
  Proof.
148
149
    iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
    iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
150
    wp_rec. wp_branch as %_ | %Hys'.
151
152
    - wp_recv (x v) as (Htl) "HI".
      wp_select. wp_send with "[$HI]"; first by auto.
153
      wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
154
155
      * done.
      * by rewrite Hys -!assoc_L (comm _ zs).
156
157
      * auto using Sorted_snoc.
      * intros x'.
158
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
159
    - wp_select with "[]".
160
161
      { by rewrite /= Hys Hxs Hys'. }
      iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
162
  Qed.
163

164
  Lemma sort_service_fg_merge_spec cmp c p c1 c2 xs ys xs1 xs2 y1 w1 ys1 ys2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
    xs  xs1 ++ xs2 
    ys  ys1 ++ ys2 
167
168
169
    Sorted R ys 
    TlRel R y1 ys 
    ( x, TlRel R x ys2  R x y1  TlRel R x ys) 
170
    cmp_spec I R cmp -
jihgfee's avatar
jihgfee committed
171
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
      c  (iProto_dual (sort_fg_tail_protocol xs ys) <++> p) 
      c1  sort_fg_tail_protocol xs1 (ys1 ++ [y1]) 
      c2  sort_fg_tail_protocol xs2 ys2 
175
      I y1 w1
Robbert Krebbers's avatar
Robbert Krebbers committed
176
    }}}
177
      sort_service_fg_merge cmp c w1 c1 c2
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    {{{ RET #(); c  p }}}.
jihgfee's avatar
jihgfee committed
179
  Proof.
180
181
182
    iIntros (Hxs Hys Hsort Htl Htl_le) "#Hcmp !>".
    iIntros (Ψ) "(Hc & Hc1 & Hc2 & HIy1) HΨ".
    iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
183
    wp_rec. wp_branch as %_ | %Hys2.
184
    - wp_recv (x v) as (Htl2) "HIx".
185
      wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
jihgfee's avatar
jihgfee committed
186
      case_bool_decide.
187
      + wp_select. wp_send with "[$HIy1 //]".
188
189
190
        wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx HΨ").
        * by rewrite comm.
        * by rewrite assoc (comm _ ys2) Hys.
191
192
193
        * by apply Sorted_snoc.
        * by constructor.
        * intros x'.
194
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
195
      + wp_select. wp_send with "[$HIx]".
196
197
        { iPureIntro. by apply Htl_le, total_not. }
        wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
198
        * by rewrite Hys assoc.
199
200
201
        * by apply Sorted_snoc, Htl_le, total_not.
        * constructor. by apply total_not.
        * intros x'.
202
          inversion 1; discriminate_list || simplify_list_eq. by constructor.
203
    - wp_select. wp_send with "[$HIy1 //]".
Robbert Krebbers's avatar
Robbert Krebbers committed
204
      wp_apply (sort_service_fg_forward_spec with "[$Hc $Hc1]").
205
206
      * done.
      * by rewrite Hys Hys2 -!assoc_L (comm _ xs2).
207
208
      * by apply Sorted_snoc.
      * intros x'.
209
210
        inversion 1; discriminate_list || simplify_list_eq. by constructor.
      * iIntros "[Hc Hc1]". iApply "HΨ". iFrame.
jihgfee's avatar
jihgfee committed
211
  Qed.
jihgfee's avatar
jihgfee committed
212

213
  Lemma sort_service_fg_spec cmp c p :
214
    cmp_spec I R cmp -
Robbert Krebbers's avatar
Robbert Krebbers committed
215
    {{{ c  (iProto_dual sort_fg_protocol <++> p) }}}
216
      sort_service_fg cmp c
Robbert Krebbers's avatar
Robbert Krebbers committed
217
    {{{ RET #(); c  p }}}.
jihgfee's avatar
jihgfee committed
218
  Proof.
219
    iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c p Ψ).
220
221
222
    wp_rec; wp_pures. wp_branch; wp_pures.
    - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
      + wp_recv (x2 v2) as "HIx2".
Robbert Krebbers's avatar
Robbert Krebbers committed
223
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
224
225
        { iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
        iIntros (cy) "Hcy".
Robbert Krebbers's avatar
Robbert Krebbers committed
226
        wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
227
228
        { iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
        iIntros (cz) "Hcz". rewrite !right_id.
229
230
        wp_select. wp_send with "[$HIx1]".
        wp_select. wp_send with "[$HIx2]".
231
        wp_apply (sort_service_fg_split_spec with "[$Hc $Hcy $Hcz]").
232
        iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
233
        wp_branch as %_ | %[]%Permutation_nil_cons.
234
        wp_recv (x v) as "[_ HIx]".
235
        wp_apply (sort_service_fg_merge_spec _ _ _ _ _ _ [] _ _ _ _ [] []
236
          with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
237
        by rewrite Hxs' Permutation_middle.
238
      + wp_select. wp_send with "[$HIx1]"; first by auto using TlRel_nil.
239
240
        wp_select. by iApply "HΨ".
    - wp_select. by iApply "HΨ".
jihgfee's avatar
jihgfee committed
241
  Qed.
jihgfee's avatar
jihgfee committed
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
  
  Lemma send_all_spec c p xs' l xs :
    {{{ llist I l xs  c  (sort_fg_head_protocol xs' <++> p) }}}
      send_all c #l
    {{{ RET #(); llist I l []  c  (sort_fg_head_protocol (xs' ++ xs) <++> p) }}}.
  Proof.
    iIntros (Φ) "[Hl Hc] HΦ".
    iInduction xs as [|x xs] "IH" forall (xs').
    { wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl"; wp_pures.
      iApply "HΦ". rewrite right_id_L. iFrame. }
    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.
  Qed.

  Lemma recv_all_spec c p l xs ys' :
    Sorted R ys' 
    {{{ llist I l []  c  (sort_fg_tail_protocol xs ys' <++> p) }}}
      recv_all c #l
    {{{ ys, RET #();
        Sorted R (ys' ++ ys)  ys' ++ ys  xs  llist I l ys  c  p
    }}}.
  Proof.
    iIntros (Hsort Φ) "[Hl Hc] HΦ".
    iLöb as "IH" forall (xs ys' Φ Hsort).
    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
    - wp_recv (y v) as (Htl) "HIx".
      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
      iIntros (ys). rewrite -!assoc_L. iDestruct 1 as (??) "[Hl Hc]".
      wp_apply (lcons_spec with "[$Hl $HIx]"); iIntros "Hl"; wp_pures.
      iApply ("HΦ" with "[$Hl $Hc]"); simpl; eauto.
    - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
  Qed.

  Lemma sort_client_fg_spec cmp l xs :
    cmp_spec I R cmp -
    {{{ llist I l xs }}}
      sort_client_fg cmp #l
    {{{ ys, RET #(); Sorted R ys  ys  xs  llist I l ys }}}.
  Proof.
    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
    wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto);
      iIntros (c) "Hc".
    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
    wp_select.
    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
    iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
    iApply "HΦ"; auto with iFrame.
  Qed.
  
293
  End sort_fg_inner.
294

295
  Definition sort_fg_func_protocol : iProto Σ :=
296
297
298
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
         `{!RelDecision R, !Total R} (cmp : val),
       MSG cmp {{ cmp_spec I R cmp }};
299
     sort_fg_head_protocol I R [])%proto.
300

301
  Lemma sort_service_fg_func_spec c p :
Robbert Krebbers's avatar
Robbert Krebbers committed
302
    {{{ c  (iProto_dual sort_fg_func_protocol <++> p) }}}
303
      sort_service_fg_func c
Robbert Krebbers's avatar
Robbert Krebbers committed
304
    {{{ RET #(); c  p }}}.
305
  Proof.
306
    iIntros (Ψ) "Hc HΨ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    wp_recv (A I R ? ? cmp) as "#Hcmp".
308
    by wp_apply (sort_service_fg_spec with "Hcmp Hc").
309
  Qed.
jihgfee's avatar
jihgfee committed
310
End sort_fg.