map_reduce.v 14.3 KB
Newer Older
1
2
(** This file implements a map-reduce program,
a specification thereof and its proofs. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From actris.channel Require Import proto_channel proofmode.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.heap_lang Require Import proofmode notation.
5
From actris.utils Require Import llist compare contribution group.
jihgfee's avatar
jihgfee committed
6
From actris.examples Require Import map sort_fg.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
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.
13
Instance: Params (@map_reduce) 7.
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
14
15

(** Distributed version *)
16
Definition par_map_reduce_map : val :=
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
17
18
19
20
21
22
23
24
  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;;
25
26
        send "cmap" (lpop "xs");;
        "go" "n" "cmap" "csort" "xs"
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
27
28
29
30
31
32
33
    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" :=
34
    if: ~recv "csort" then NONE else
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
35
36
    let: "jy" := recv "csort" in
    let: "j" := Fst "jy" in let: "y" := Snd "jy" in
37
38
    if: "i" = "j" then lcons "y" "ys";; "go" "csort" "j" "ys" else
    SOME ("j", "y").
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
39

40
Definition par_map_reduce_reduce : val :=
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
41
  rec: "go" "n" "csort" "cred" "acc" "zs" :=
42
    if: "n" = #0 then #() else
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
43
44
45
46
47
48
49
    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
50
         let: "ys" := lnil #() in lcons (Snd "acc") "ys";;
51
         let: "new_acc" := par_map_reduce_collect "csort" (Fst "acc") "ys" in
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
52
         send "cred" #true;;
53
54
         send "cred" (Fst "acc", "ys");;
         "go" "n" "csort" "cred" "new_acc" "zs"
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
55
56
57
      end
    else (* receive item from mapper *)
      let: "zs'" := recv "cred" in
58
59
      lprep "zs" "zs'";;
      "go" "n" "csort" "cred" "acc" "zs".
Robbert Krebbers's avatar
Tweak.    
Robbert Krebbers committed
60
61
62

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

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


Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(** 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
94
95
  map_reduce_mapG :> mapG Σ A;
  map_reduce_reduceG :> mapG Σ (Z * list B);
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
99
}.

Section mapper.
  Context `{Countable A, Countable B} {C : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
103
104
  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
105
  Implicit Types n : nat.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109

  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
110
    ( (l : loc),  w = (#iys.1, #l)%V   llist (IB iys.1) l (iys.2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
  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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
169
  Lemma par_map_reduce_collect_spec csort iys iys_sorted i l ys :
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
    let acc := from_option (λ '(i,y,w), [(i,y)]) [] in
    let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in
    ys  [] 
Robbert Krebbers's avatar
Robbert Krebbers committed
173
    Sorted RZB (iys_sorted ++ ((i,.) <$> ys)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
    i  iys_sorted.*1 
    {{{
Robbert Krebbers's avatar
Robbert Krebbers committed
176
      llist (IB i) l (reverse ys) 
Robbert Krebbers's avatar
Robbert Krebbers committed
177
      csort  sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,.) <$> ys))
Robbert Krebbers's avatar
Robbert Krebbers committed
178
    }}}
179
      par_map_reduce_collect csort #i #l
Robbert Krebbers's avatar
Robbert Krebbers committed
180
    {{{ ys' miy, RET accv miy;
Robbert Krebbers's avatar
Robbert Krebbers committed
181
       Sorted RZB ((iys_sorted ++ ((i,.) <$> ys ++ ys')) ++ acc miy)  
Robbert Krebbers's avatar
Robbert Krebbers committed
182
       from_option (λ '(j,_,_), i  j  j  iys_sorted.*1)
Robbert Krebbers's avatar
Robbert Krebbers committed
183
                    (iys_sorted ++ ((i,.) <$> ys ++ ys')  iys) miy  
Robbert Krebbers's avatar
Robbert Krebbers committed
184
      llist (IB i) l (reverse (ys ++ ys')) 
185
      csort  from_option (λ _, sort_fg_tail_protocol IZB RZB iys
Robbert Krebbers's avatar
Robbert Krebbers committed
186
        ((iys_sorted ++ ((i,.) <$> ys ++ ys')) ++ acc miy)) END%proto miy 
Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
189
      from_option (λ '(i,y,w), IB i y w) True miy
    }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
    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
192
    wp_branch as %_|%Hperm; last first; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
    { iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
194
     iEval (rewrite !right_id_L); auto with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
195
    wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
    case_bool_decide as Hij; simplify_eq/=; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    - wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
198
      rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
Robbert Krebbers's avatar
Robbert Krebbers committed
199
        with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
200
201
202
      + 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
203
204
      + iIntros "!>" (ys' miy). rewrite -!(assoc_L _ ys) /=. iApply "HΦ".
    - iApply ("HΦ" $! [] (Some (j,y,w))).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
208
209
210
211
212
213
214
215
216
217
      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.

218
  Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
223
224
    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
225
      llist IC l zs 
226
      csort  from_option (λ _, sort_fg_tail_protocol IZB RZB iys
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
        (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
229
      from_option (λ '(i,y,w), IB i y w) True miy
Robbert Krebbers's avatar
Robbert Krebbers committed
230
    }}}
231
      par_map_reduce_reduce #n csort cred (accv miy) #l
Robbert Krebbers's avatar
Robbert Krebbers committed
232
    {{{ zs', RET #();
Robbert Krebbers's avatar
Robbert Krebbers committed
233
        (group iys_sorted = curry red) ++ zs'  (group iys ++ elements Y) = curry red  
Robbert Krebbers's avatar
Robbert Krebbers committed
234
       llist IC l (zs' ++ zs)
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
    }}}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
    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
239
240
    case_bool_decide; wp_pures; simplify_eq/=.
    { destruct Hn as [-> ->]; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
      iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
245
246
      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
247
248
249
250
251
252
253
254
          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
255
        wp_pures. iApply ("IH" $! _ (_ ++ _) miy
Robbert Krebbers's avatar
Robbert Krebbers committed
256
          with "[%] [%] [//] Hl Hcsort Hcred HImiy"); first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
        { destruct miy as [[[i' y'] w']|]; set_solver +Hmiy'. }
Robbert Krebbers's avatar
Robbert Krebbers committed
258
        iIntros "!>" (zs'). iDestruct 1 as (Hperm) "HIC".
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
262
        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.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
        apply (inj (.++ _)).
Robbert Krebbers's avatar
Robbert Krebbers committed
264
    - wp_recv ([i ys] k) as (Hy) "Hk".
265
      wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
      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
268
269
270
      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
271
      rewrite (comm_L disj_union) gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
273
274
275
      rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
      by rewrite right_id_L !assoc_L.
  Qed.

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