map_reduce.v 14.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From actris.channel Require Import proto_channel proofmode.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.heap_lang Require Import proofmode notation.
3
From actris.utils Require Import llist compare contribution group.
jihgfee's avatar
jihgfee committed
4
From actris.examples Require Import map sort_fg.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
10
From iris.algebra Require Import gmultiset.

(** Functional version of map reduce (aka the specification) *)
Definition map_reduce {A B C} `{EqDecision K}
    (map : A  list (K * B)) (red : K  list B  list C) : list A  list C :=
  mbind (curry red)  group  mbind map.
11
Instance: Params (@map_reduce) 7.
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
12
13

(** Distributed version *)
14
Definition par_map_reduce_map : val :=
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
15
16
17
18
19
20
21
22
  rec: "go" "n" "cmap" "csort" "xs" :=
    if: "n" = #0 then #() else
    if: recv "cmap" then (* send item to mapper *)
      if: lisnil "xs" then
        send "cmap" #false;;
        "go" ("n" - #1) "cmap" "csort" "xs"
      else
        send "cmap" #true;;
23
24
        send "cmap" (lpop "xs");;
        "go" "n" "cmap" "csort" "xs"
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
25
26
27
28
29
30
31
    else (* receive item from mapper *)
      let: "zs" := recv "cmap" in
      send_all "csort" "zs";;
      "go" "n" "cmap" "csort" "xs".

Definition par_map_reduce_collect : val :=
  rec: "go" "csort" "i" "ys" :=
32
    if: ~recv "csort" then NONE else
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
33
34
    let: "jy" := recv "csort" in
    let: "j" := Fst "jy" in let: "y" := Snd "jy" in
35
36
    if: "i" = "j" then lcons "y" "ys";; "go" "csort" "j" "ys" else
    SOME ("j", "y").
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
37

38
Definition par_map_reduce_reduce : val :=
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
39
  rec: "go" "n" "csort" "cred" "acc" "zs" :=
40
    if: "n" = #0 then #() else
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
41
42
43
44
45
46
47
    if: recv "cred" then (* Send item to mapper *)
      match: "acc" with
        NONE =>
         (* nothing left *)
         send "cred" #false;; "go" ("n" - #1) "csort" "cred" NONE "zs"
      | SOME "acc" =>
         (* Read subsequent items with the same key *)
Robbert Krebbers's avatar
Robbert Krebbers committed
48
         let: "ys" := lnil #() in lcons (Snd "acc") "ys";;
49
         let: "new_acc" := par_map_reduce_collect "csort" (Fst "acc") "ys" in
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
50
         send "cred" #true;;
51
52
         send "cred" (Fst "acc", "ys");;
         "go" "n" "csort" "cred" "new_acc" "zs"
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
53
54
55
      end
    else (* receive item from mapper *)
      let: "zs'" := recv "cred" in
56
57
      lprep "zs" "zs'";;
      "go" "n" "csort" "cred" "acc" "zs".
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
58
59
60

Definition cmpZfst : val := λ: "x" "y", Fst "x"  Fst "y".

61
Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
62
  let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
63
  let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
64
  par_map_reduce_map "n" "cmap" "csort" "xs";;
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
65
  send "csort" #stop;;
66
  let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
67
  (* We need the first sorted element in the loop to compare subsequent elements *)
68
  if: ~recv "csort" then #() else (* Handle the empty case *)
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
69
  let: "jy" := recv "csort" in
70
  par_map_reduce_reduce "m" "csort" "cred" (SOME "jy") "xs".
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
71
72


Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
(** Properties about the functional version *)
Section map_reduce.
  Context {A B C} `{EqDecision K} (map : A  list (K * B)) (red : K  list B  list C).
  Context `{! j, Proper (() ==> ()) (red j)}.

  Global Instance bind_red_perm : Proper ((ₚₚ) ==> ()) (mbind (curry red)).
  Proof.
    induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|];
      simplify_eq/=; try done.
    - repeat (done || f_equiv).
    - by rewrite !assoc_L (comm _ (red i2 xs2)).
    - by etrans.
  Qed.
  Global Instance map_reduce_perm : Proper (() ==> ()) (map_reduce map red).
  Proof. intros xs1 xs2 Hxs. by rewrite /map_reduce /= Hxs. Qed.
End map_reduce.

(** Correctness proofs of the distributed version *)
Class map_reduceG Σ A B `{Countable A, Countable B} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
  map_reduce_mapG :> mapG Σ A;
  map_reduce_reduceG :> mapG Σ (Z * list B);
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
}.

Section mapper.
  Context `{Countable A, Countable B} {C : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
  Context (IA : A  val  iProp Σ) (IB : Z  B  val  iProp Σ) (IC : C  val  iProp Σ).
  Context (map : A  list (Z * B)) (red : Z  list B  list C).
  Context `{! j, Proper (() ==> ()) (red j)}.
  Local Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  Implicit Types n : nat.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107

  Definition IZB (iy : Z * B) (w : val) : iProp Σ :=
    ( w',  w = (#iy.1, w')%V   IB iy.1 iy.2 w')%I.
  Definition IZBs (iys : Z * list B) (w : val) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
108
    ( (l : loc),  w = (#iys.1, #l)%V   llist (IB iys.1) l (iys.2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
  Definition RZB : relation (Z * B) := prod_relation ()%Z (λ _ _ : B, True).

  Instance RZB_dec : RelDecision RZB.
  Proof. solve_decision. Qed.
  Instance RZB_total : Total RZB.
  Proof. intros [i1 y1] [i2 y2]. destruct (total ()%Z i1 i2); [left|right]; done. Qed.
  Instance RZB_trans : Transitive RZB.
  Proof. by apply (prod_relation_trans _). Qed.
  Lemma RZB_cmp_spec : cmp_spec IZB RZB cmpZfst.
  Proof.
    iIntros ([i1 y1] [i2 y2] v1 v2) "!>"; iIntros (Φ) "[HI1 HI2] HΦ".
    iDestruct "HI1" as (w1 ->) "HI1". iDestruct "HI2" as (w2 ->) "HI2 /=".
    wp_lam; wp_pures. iSpecialize ("HΦ" with "[HI1 HI2]").
    { iSplitL "HI1"; rewrite /IZB /=; eauto with iFrame. }
    repeat case_bool_decide=> //; unfold RZB, prod_relation in *; naive_solver.
  Qed.

126
  Lemma par_map_reduce_map_spec n cmap csort l xs X ys :
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
    (n = 0  X =   xs = []) 
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
129
      llist IA l xs 
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
      cmap  par_map_protocol IA IZB map n (X : gmultiset A) 
      csort  sort_fg_head_protocol IZB RZB ys
Robbert Krebbers's avatar
Robbert Krebbers committed
132
    }}}
133
      par_map_reduce_map #n cmap csort #l
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
    {{{ ys', RET #();
      ys'  (xs ++ elements X) = map 
Robbert Krebbers's avatar
Robbert Krebbers committed
136
      llist IA l []  csort  sort_fg_head_protocol IZB RZB (ys ++ ys')
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
    }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
    iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ".
    iLöb as "IH" forall (n xs X ys Hn Φ); wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
    case_bool_decide; wp_pures; simplify_eq/=.
    { destruct Hn as [-> ->]; first lia.
143
      iApply ("HΦ" $! []). rewrite right_id_L. auto with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
145
    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
146
      destruct xs as [|x xs]; csimpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
      + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
        iApply ("IH" $! _ [] with "[%] Hl Hcmap Hcsort HΦ"); naive_solver.
      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
        wp_send with "[$HIx]".
        wp_apply ("IH" with "[%] Hl Hcmap Hcsort"); first done. iIntros (ys').
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
        rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
        rewrite assoc_L -(comm _ [x]). iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    - wp_recv (x k) as (Hx) "Hk".
155
      rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
156
      wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "[_ Hcsort]".
Robbert Krebbers's avatar
Robbert Krebbers committed
157
      rewrite right_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
      wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
      iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
      rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
      iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
        -?gmultiset_elem_of_singleton_subseteq //.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
      rewrite (comm_L disj_union) gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
      by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
167
  Lemma par_map_reduce_collect_spec csort iys iys_sorted i l ys :
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
172
173
    let acc := from_option (λ '(i,y,w), [(i,y)]) [] in
    let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in
    ys  [] 
    Sorted RZB (iys_sorted ++ ((i,) <$> ys)) 
    i  iys_sorted.*1 
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
174
      llist (IB i) l (reverse ys) 
Robbert Krebbers's avatar
Robbert Krebbers committed
175
      csort  sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys))
Robbert Krebbers's avatar
Robbert Krebbers committed
176
    }}}
177
      par_map_reduce_collect csort #i #l
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    {{{ ys' miy, RET accv miy;
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
       Sorted RZB ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)  
       from_option (λ '(j,_,_), i  j  j  iys_sorted.*1)
                    (iys_sorted ++ ((i,) <$> ys ++ ys')  iys) miy  
Robbert Krebbers's avatar
Robbert Krebbers committed
182
      llist (IB i) l (reverse (ys ++ ys')) 
183
      csort  from_option (λ _, sort_fg_tail_protocol IZB RZB iys
Robbert Krebbers's avatar
Robbert Krebbers committed
184
        ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy 
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
      from_option (λ '(i,y,w), IB i y w) True miy
    }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
    iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
    iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
    wp_branch as %_|%Hperm; last first; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
    { iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
192
     iEval (rewrite !right_id_L); auto with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
193
    wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
    case_bool_decide as Hij; simplify_eq/=; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
    - wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
196
      rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
Robbert Krebbers's avatar
Robbert Krebbers committed
197
        with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
      + intros ?; discriminate_list.
      + rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
      + by rewrite fmap_app /= assoc_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
      + iIntros "!>" (ys' miy). rewrite -!(assoc_L _ ys) /=. iApply "HΦ".
    - iApply ("HΦ" $! [] (Some (j,y,w))).
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
205
206
207
208
209
210
211
212
213
214
215
      rewrite /= !right_id_L assoc_L. iFrame. iPureIntro; split.
      { by apply Sorted_snoc. }
      split; first congruence.
      intros [[j' y'] [-> Hj]]%elem_of_list_fmap.
      destruct Hij; do 2 f_equal.
      destruct ys as [|y'' ys _] using rev_ind; first done.
      move: Htl. rewrite fmap_app assoc_L /=.
      inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
      assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
      apply (Sorted_StronglySorted _) in Hsort.
      eapply elem_of_StronglySorted_app; set_solver.
  Qed.

216
  Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
219
220
221
222
    let acc := from_option (λ '(i,y,w), [(i,y)]) [] in
    let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in
    (n = 0  miy = None  Y = ) 
    from_option (λ '(i,_,_), i  iys_sorted.*1) (iys_sorted  iys) miy 
    Sorted RZB (iys_sorted ++ acc miy) 
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
223
      llist IC l zs 
224
      csort  from_option (λ _, sort_fg_tail_protocol IZB RZB iys
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
        (iys_sorted ++ acc miy)) END%proto miy 
      cred  par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
227
      from_option (λ '(i,y,w), IB i y w) True miy
Robbert Krebbers's avatar
Robbert Krebbers committed
228
    }}}
229
      par_map_reduce_reduce #n csort cred (accv miy) #l
Robbert Krebbers's avatar
Robbert Krebbers committed
230
    {{{ zs', RET #();
Robbert Krebbers's avatar
Robbert Krebbers committed
231
        (group iys_sorted = curry red) ++ zs'  (group iys ++ elements Y) = curry red  
Robbert Krebbers's avatar
Robbert Krebbers committed
232
       llist IC l (zs' ++ zs)
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
    }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
    iIntros (acc accv Hn Hmiy Hsort Φ) "(Hl & Hcsort & Hcred & HImiy) HΦ".
    iLöb as "IH" forall (n iys_sorted miy zs Y Hn Hmiy Hsort Φ); wp_rec; wp_pures; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
    case_bool_decide; wp_pures; simplify_eq/=.
    { destruct Hn as [-> ->]; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
      iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
241
242
243
244
      by rewrite gmultiset_elements_empty !right_id_L Hmiy. }
    destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
    - destruct miy as [[[i y] w]|]; simplify_eq/=; wp_pures; last first.
      + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
        iApply ("IH" $! _ _ None
Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
248
249
250
251
252
          with "[%] [%] [%] Hl Hcsort Hcred [] HΦ"); naive_solver.
      + wp_apply (lnil_spec (IB i) with "[//]"); iIntros (k) "Hk".
        wp_apply (lcons_spec with "[$Hk $HImiy]"); iIntros "Hk".
        wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] 
          with "[$Hk $Hcsort]"); try done.
        iIntros (ys' miy). iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HImiy)"; csimpl.
        wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[Hk]".
        { iExists k; simpl; auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
253
        wp_pures. iApply ("IH" $! _ (_ ++ _) miy
Robbert Krebbers's avatar
Robbert Krebbers committed
254
          with "[%] [%] [//] Hl Hcsort Hcred HImiy"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
        { destruct miy as [[[i' y'] w']|]; set_solver +Hmiy'. }
Robbert Krebbers's avatar
Robbert Krebbers committed
256
        iIntros "!>" (zs'). iDestruct 1 as (Hperm) "HIC".
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
259
260
261
        iApply ("HΦ" with "[$HIC]"); iPureIntro; move: Hperm.
        rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
        rewrite group_snoc // reverse_Permutation.
        rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
        apply (inj (++ _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
262
    - wp_recv ([i ys] k) as (Hy) "Hk".
263
      wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
Robbert Krebbers's avatar
Robbert Krebbers committed
264
265
      wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
      iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
      iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
      iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
        -?gmultiset_elem_of_singleton_subseteq //.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
      rewrite (comm_L disj_union) gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
271
272
273
      rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
      by rewrite right_id_L !assoc_L.
  Qed.

274
275
  Lemma par_map_reduce_spec n m vmap vred l xs :
    0 < n  0 < m 
Robbert Krebbers's avatar
Robbert Krebbers committed
276
277
    map_spec IA IZB map vmap -
    map_spec IZBs IC (curry red) vred -
Robbert Krebbers's avatar
Robbert Krebbers committed
278
    {{{ llist IA l xs }}}
279
      par_map_reduce #n #m vmap vred #l
280
    {{{ zs, RET #(); zs  map_reduce map red xs  llist IC l zs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
  Proof.
282
    iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
    wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ));
284
285
      iIntros (cmap) "// Hcmap".
    { wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
286
    wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
Robbert Krebbers's avatar
Robbert Krebbers committed
287
      iIntros (csort) "Hcsort".
Robbert Krebbers's avatar
Robbert Krebbers committed
288
    { wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
290
      iApply RZB_cmp_spec. }
    rewrite right_id.
291
    wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
    iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
293
    iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
294
    wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ));
295
296
      iIntros (cred) "// Hcred".
    { wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
297
    wp_branch as %_|%Hnil; last first.
298
    { wp_pures. iApply ("HΦ" $! [] with "[$Hl]"); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
      by rewrite /map_reduce /= -Hiys -Hnil. }
    wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
301
302
    wp_apply (par_map_reduce_reduce_spec _ _ [] (Some (i, y, w)) []
      with "[$Hl $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
    iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
    iDestruct 1 as (Hzs) "Hk". wp_pures.
    iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
  Qed.
End mapper.