Kill bigops.

theories/channel/channel.v

@@ -67,8 +67,8 @@ Section channel.
 
   Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
     (∃ ls rs,
-      llist l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
-      llist r rs ∗ own (chan_r_name γ) (● to_auth_excl rs))%I.
+      llist sbi_internal_eq l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
+      llist sbi_internal_eq r rs ∗ own (chan_r_name γ) (● to_auth_excl rs))%I.
   Typeclasses Opaque chan_inv.
 
   Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
@@ -99,8 +99,8 @@ Section channel.
     iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
     wp_apply (newlock_spec N (∃ ls rs,
-      llist l ls ∗ own lsγ (● to_auth_excl ls) ∗
-      llist r rs ∗ own rsγ (● to_auth_excl rs))%I with "[Hl Hr Hls Hrs]").
+      llist sbi_internal_eq l ls ∗ own lsγ (● to_auth_excl ls) ∗
+      llist sbi_internal_eq r rs ∗ own rsγ (● to_auth_excl rs))%I with "[Hl Hr Hls Hrs]").
     { eauto 10 with iFrame. }
     iIntros (lk γlk) "#Hlk". wp_pures.
     iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
@@ -109,9 +109,9 @@ Section channel.
 
   Lemma chan_inv_alt s γ l r :
     chan_inv γ l r ⊣⊢ ∃ ls rs,
-      llist (side_elim s l r) ls ∗
+      llist sbi_internal_eq (side_elim s l r) ls ∗
       own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
-      llist (side_elim s r l) rs ∗
+      llist sbi_internal_eq (side_elim s r l) rs ∗
       own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
   Proof.
     destruct s; rewrite /chan_inv //=.
@@ -137,7 +137,7 @@ Section channel.
     iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
     iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
     wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
-    wp_apply (lsnoc_spec with "Hll"); iIntros "Hll".
+    wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
     wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
     iApply (chan_inv_alt s).
     rewrite /llist. eauto 20 with iFrame.
@@ -171,7 +171,7 @@ Section channel.
       iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
       wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
       wp_apply (lisnil_spec with "Hll"); iIntros "Hll".
-      wp_apply (lpop_spec with "Hll"); iIntros "Hll".
+      wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
       wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
       { iApply (chan_inv_alt s).
         rewrite /llist. eauto 10 with iFrame. }

theories/examples/map.v

@@ -63,9 +63,7 @@ Section map.
   Implicit Types n : nat.
 
   Definition map_spec (vmap : val) : iProp Σ := (∀ x v,
-    {{{ IA x v }}}
-      vmap v
-    {{{ l ws, RET #l; llist l ws ∗ [∗ list] y;w ∈ map x;ws, IB y w }}})%I.
+    {{{ IA x v }}} vmap v {{{ l, RET #l; llist IB l (map x) }}})%I.
 
   Definition map_worker_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
       nat -d> gmultiset A -d> iProto Σ := λ i X,
@@ -75,7 +73,7 @@ Section map.
         <+>
       rec (pred i) X
      ) <{⌜ i ≠ 1 ∨ X = ∅ ⌝}&>
-         <?> x (l : loc) ws, MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist l ws ∗ [∗ list] y;w ∈ map x;ws, IB y w }};
+         <?> x (l : loc), MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist IB l (map x) }};
          rec i (X ∖ {[ x ]}))%proto.
   Instance map_worker_protocol_aux_contractive : Contractive map_worker_protocol_aux.
   Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
@@ -112,7 +110,7 @@ Section map.
     rewrite left_id_L.
     wp_apply (release_spec with "[$Hlk $Hl Hc Hs]").
     { iExists (S i), _. iFrame. }
-    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l ws) "HI".
+    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l) "HI".
     wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ")
@@ -159,41 +157,31 @@ Section map.
     wp_apply (start_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
   Qed.
 
-  Lemma par_map_server_spec n c l k vs xs ws X ys :
+  Lemma par_map_server_spec n c l k xs X ys :
     (n = 0 → X = ∅ ∧ xs = []) →
-    {{{
-      llist l vs ∗ llist k ws ∗
-      c ↣ map_worker_protocol n X @ N ∗
-      ([∗ list] x;v ∈ xs;vs, IA x v) ∗ ([∗ list] y;w ∈ ys;ws, IB y w)
-    }}}
+    {{{ llist IA l xs ∗ llist IB k ys ∗ c ↣ map_worker_protocol n X @ N }}}
       par_map_server #n c #l #k
-    {{{ ys' ws', RET #();
-       ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗
-       llist k ws' ∗ [∗ list] y;w ∈ ys' ++ ys;ws', IB y w
-    }}}.
+    {{{ ys', RET #(); ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗ llist IB k (ys' ++ ys) }}}.
   Proof.
-    iIntros (Hn Φ) "(Hl & Hk & Hc & HIA & HIB) HΦ".
-    iLöb as "IH" forall (n l vs xs ws X ys Hn Φ); wp_rec; wp_pures; simpl.
+    iIntros (Hn Φ) "(Hl & Hk & Hc) HΦ".
+    iLöb as "IH" forall (n l xs X ys Hn Φ); wp_rec; wp_pures; simpl.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []); simpl; auto with iFrame. }
     destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
     - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
-      destruct vs as [|v vs], xs as [|x xs]; csimpl; try done; wp_pures.
+      destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-        iApply ("IH" with "[%] Hl Hk Hc [//] [$] HΦ"); naive_solver.
-      + iDestruct "HIA" as "[HIAx HIA]". wp_select.
-        wp_apply (lpop_spec with "Hl"); iIntros "Hl".
-        wp_send with "[$HIAx]".
-        wp_apply ("IH" with "[] Hl Hk Hc HIA HIB"); first done.
-        iIntros (ys' ws').
+        iApply ("IH" with "[%] Hl Hk Hc [$]"); naive_solver.
+      + wp_select. wp_apply (lpop_spec with "Hl"); iIntros (v) "[HIx Hl]".
+        wp_send with "[$HIx]".
+        wp_apply ("IH" with "[] Hl Hk Hc"); first done. iIntros (ys').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
-    - wp_recv (x l' w) as (Hx) "[Hl' HIBx]".
+    - wp_recv (x l') as (Hx) "Hl'".
       wp_apply (lprep_spec with "[$Hk $Hl']"); iIntros "[Hk _]".
-      wp_apply ("IH" $! _ _ _ _ _ _ (_ ++ _) with "[] Hl Hk Hc HIA [HIBx HIB]"); first done.
-      { simpl; iFrame. }
-      iIntros (ys' ws'); iDestruct 1 as (Hys) "HIB"; simplify_eq/=.
+      wp_apply ("IH" with "[] Hl Hk Hc"); first done.
+      iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
       + iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
           -?gmultiset_elem_of_singleton_subseteq //.
@@ -202,18 +190,18 @@ Section map.
       + by rewrite -assoc_L.
   Qed.
 
-  Lemma par_map_spec n vmap l vs xs :
+  Lemma par_map_spec n vmap l xs :
     0 < n →
     map_spec vmap -∗
-    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, IA x v }}}
+    {{{ llist IA l xs }}}
       par_map #n vmap #l
-    {{{ k ys ws, RET #k; ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist k ws ∗ [∗ list] y;w ∈ ys;ws, IB y w }}}.
+    {{{ k ys, RET #k; ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB k ys }}}.
   Proof.
-    iIntros (?) "#Hmap !>"; iIntros (Φ) "[Hl HI] HΦ". wp_lam; wp_pures.
+    iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
     wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (c) "Hc".
     wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-    wp_apply (par_map_server_spec _ _ _ _ _ _ [] ∅ [] with "[$Hl $Hk $Hc $HI //]"); first lia.
-    iIntros (ys ws) "H". rewrite /= gmultiset_elements_empty !right_id_L .
-    wp_pures. by iApply "HΦ".
+    wp_apply (par_map_server_spec with "[$Hl $Hk $Hc //]"); first lia.
+    iIntros (ys) "[??]". rewrite /= gmultiset_elements_empty !right_id_L .
+    wp_pures. iApply "HΦ"; auto.
   Qed.
 End map.

theories/examples/map_reduce.v

@@ -222,8 +222,7 @@ Section mapper.
   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 Σ :=
-    (∃ (l : loc) ws,
-      ⌜ w = (#iys.1, #l)%V ⌝ ∗ llist l ws ∗ [∗ list] y;w'∈iys.2;ws, IB iys.1 y w')%I.
+    (∃ (l : loc), ⌜ w = (#iys.1, #l)%V ⌝ ∗ llist (IB iys.1) l (iys.2))%I.
   Definition RZB : relation (Z * B) := prod_relation (≤)%Z (λ _ _ : B, True).
 
   Instance RZB_dec : RelDecision RZB.
@@ -241,13 +240,12 @@ Section mapper.
     repeat case_bool_decide=> //; unfold RZB, prod_relation in *; naive_solver.
   Qed.
 
-  Lemma par_map_reduce_map_server_spec n cmap csort l vs xs X ys :
+  Lemma par_map_reduce_map_server_spec n cmap csort l xs X ys :
     (n = 0 → X = ∅ ∧ xs = []) →
     {{{
-      llist l vs ∗
+      llist IA l xs ∗
       cmap ↣ map_worker_protocol IA IZB map n (X : gmultiset A) @ N ∗
-      csort ↣ sort_elem_head_protocol IZB RZB ys @ N ∗
-      ([∗ list] x;v ∈ xs;vs, IA x v)
+      csort ↣ sort_elem_head_protocol IZB RZB ys @ N
     }}}
       par_map_reduce_map_server #n cmap csort #l
     {{{ ys', RET #();
@@ -255,28 +253,26 @@ Section mapper.
       csort ↣ sort_elem_head_protocol IZB RZB (ys ++ ys') @ N
     }}}.
   Proof.
-    iIntros (Hn Φ) "(Hl & Hcmap & Hcsort & HIA) HΦ".
-    iLöb as "IH" forall (n vs xs X ys Hn Φ); wp_rec; wp_pures; simpl.
+    iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ".
+    iLöb as "IH" forall (n xs X ys Hn Φ); wp_rec; wp_pures; simpl.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
       iApply ("HΦ" $! []). rewrite right_id_L. auto. }
     destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
     - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
-      destruct vs as [|v vs], xs as [|x xs]; csimpl; try done; wp_pures.
+      destruct xs as [|x xs]; csimpl; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-        iApply ("IH" $! _ _ [] with "[%] Hl Hcmap Hcsort [//] HΦ"); naive_solver.
-      + iDestruct "HIA" as "[HIAx HIA]". wp_select.
-        wp_apply (lpop_spec with "Hl"); iIntros "Hl".
-        wp_send with "[$HIAx]".
-        wp_apply ("IH" with "[%] Hl Hcmap Hcsort HIA"); first done.
-        iIntros (ys').
+        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').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
-    - wp_recv (x k ws) as (Hx) "[Hk HIBfx]".
+    - wp_recv (x k) as (Hx) "Hk".
       rewrite -(right_id END%proto _ (sort_elem_head_protocol _ _ _)).
-      wp_apply (send_all_spec with "[$Hk $Hcsort $HIBfx]"); iIntros "Hcsort".
+      wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "Hcsort".
       rewrite right_id.
-      wp_apply ("IH" with "[] Hl Hcmap Hcsort HIA"); first done.
+      wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
       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)
@@ -285,46 +281,42 @@ Section mapper.
       by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
   Qed.
 
-  Lemma par_map_reduce_collect_spec csort iys iys_sorted i l ys ws :
+  Lemma par_map_reduce_collect_spec csort iys iys_sorted i l ys :
     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 →
     {{{
-      llist l (reverse ws) ∗
-      csort ↣ sort_elem_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys)) @ N ∗
-      [∗ list] y;w ∈ ys;ws, IB i y w
+      llist (IB i) l (reverse ys) ∗
+      csort ↣ sort_elem_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys)) @ N
     }}}
       par_map_reduce_collect csort #i #l
-    {{{ ys' ws' miy, RET accv miy;
+    {{{ ys' miy, RET accv miy;
       ⌜ 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 ⌝ ∗
-      llist l (reverse ws') ∗
+      llist (IB i) l (reverse (ys ++ ys')) ∗
       csort ↣ from_option (λ _, sort_elem_tail_protocol IZB RZB iys
         ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy @ N ∗
-      ([∗ list] y;w ∈ ys ++ ys';ws', IB i y w) ∗
       from_option (λ '(i,y,w), IB i y w) True miy
     }}}.
   Proof.
-    iIntros (acc accv Hys Hsort Hi Φ) "(Hl & Hcsort & HIB) HΦ".
-    iLöb as "IH" forall (ys ws Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
+    iIntros (acc accv Hys Hsort Hi Φ) "[Hl Hcsort] HΦ".
+    iLöb as "IH" forall (ys Hys Hsort Hi Φ); wp_rec; wp_pures; simpl.
     wp_branch as %_|%Hperm; last first; wp_pures.
-    { iApply ("HΦ" $! [] _ None with "[$Hl $Hcsort HIB]"); simpl.
+    { iApply ("HΦ" $! [] None with "[Hl $Hcsort]"); simpl.
      iEval (rewrite !right_id_L); auto with iFrame. }
-    wp_recv ([j y] ?) as (Htl w ->) "HIBy /=". wp_pures. rewrite -assoc_L.
+    wp_recv ([j y] ?) as (Htl w ->) "HIy /=". wp_pures. rewrite -assoc_L.
     case_bool_decide as Hij; simplify_eq/=; wp_pures.
-    - wp_apply (lcons_spec with "Hl"); iIntros "Hl".
+    - wp_apply (lcons_spec with "[$Hl $HIy]"); iIntros "Hl".
       rewrite -reverse_snoc. wp_apply ("IH" $! (ys ++ [y])
-        with "[%] [%] [//] Hl [Hcsort] [HIB HIBy] [HΦ]"); try iClear "IH".
+        with "[%] [%] [//] Hl [Hcsort] [HΦ]"); try iClear "IH".
       + intros ?; discriminate_list.
       + rewrite fmap_app /= assoc_L. by apply Sorted_snoc.
       + by rewrite fmap_app /= assoc_L.
-      + iApply (big_sepL2_app with "HIB"). by iFrame.
-      + iIntros "!>" (ys' ws' miy). rewrite -!(assoc_L _ ys) /=.
-        iApply ("HΦ" $! (y :: ys')).
-    - iApply ("HΦ" $! [] _ (Some (j,y,w))).
+      + iIntros "!>" (ys' miy). rewrite -!(assoc_L _ ys) /=. iApply "HΦ".
+    - iApply ("HΦ" $! [] (Some (j,y,w))).
       rewrite /= !right_id_L assoc_L. iFrame. iPureIntro; split.
       { by apply Sorted_snoc. }
       split; first congruence.
@@ -338,61 +330,56 @@ Section mapper.
       eapply elem_of_StronglySorted_app; set_solver.
   Qed.
 
-  Lemma par_map_reduce_reduce_server_spec n iys iys_sorted miy zs l ws Y csort cred :
+  Lemma par_map_reduce_reduce_server_spec n iys iys_sorted miy zs l Y csort cred :
     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) →
     {{{
-      llist l ws ∗
+      llist IC l zs ∗
       csort ↣ from_option (λ _, sort_elem_tail_protocol IZB RZB iys
         (iys_sorted ++ acc miy)) END%proto miy @ N ∗
       cred ↣ map_worker_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) @ N ∗
-      from_option (λ '(i,y,w), IB i y w) True miy ∗
-      ([∗ list] z;w ∈ zs;ws, IC z w)
+      from_option (λ '(i,y,w), IB i y w) True miy
     }}}
       par_map_reduce_reduce_server #n csort cred (accv miy) #l
-    {{{ zs' ws', RET #();
+    {{{ zs', RET #();
        ⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗
-       llist l ws' ∗ [∗ list] z;w ∈ zs' ++ zs;ws', IC z w
+       llist IC l (zs' ++ zs)
     }}}.
   Proof.
-    iIntros (acc accv Hn Hmiy Hsort Φ) "(Hl & Hcsort & Hcred & HIB & HIC) HΦ".
-    iLöb as "IH" forall (n iys_sorted miy zs ws Y Hn Hmiy Hsort Φ); wp_rec; wp_pures; simpl.
+    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.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
-      iApply ("HΦ" $! [] with "[$Hl $HIC]"); iPureIntro; simpl.
+      iApply ("HΦ" $! [] with "[$Hl]"); iPureIntro; simpl.
       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
-          with "[%] [%] [%] Hl Hcsort Hcred [] HIC HΦ"); naive_solver.
-      + wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-        wp_apply (lcons_spec with "Hk"); iIntros "Hk".
-        wp_apply (par_map_reduce_collect_spec _ _ _ _ _ [_] [_]
-          with "[$Hk $Hcsort HIB]"); try done.
-        { simpl; iFrame. }
-        iIntros (ys' ws'' miy).
-        iDestruct 1 as (? Hmiy') "(Hk & Hcsort & HIB & HIC')"; csimpl.
-        wp_select; wp_pures. wp_send ((i, reverse (y :: ys'))) with "[HIB Hk]".
-        { iExists k, (reverse ws''); rewrite /= big_sepL2_reverse; auto with iFrame. }
+          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. }
         wp_pures. iApply ("IH" $! _ (_ ++ _) miy
-          with "[%] [%] [//] Hl Hcsort Hcred HIC' HIC"); first done.
+          with "[%] [%] [//] Hl Hcsort Hcred HImiy"); first done.
         { destruct miy as [[[i' y'] w']|]; set_solver +Hmiy'. }
-        iIntros "!>" (zs' ws'''). iDestruct 1 as (Hperm) "HIC".
+        iIntros "!>" (zs'). iDestruct 1 as (Hperm) "HIC".
         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 (++ _)).
-    - wp_recv ([i ys] k ws') as (Hy) "[Hk HICi]".
+    - wp_recv ([i ys] k) as (Hy) "Hk".
       wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
-      wp_apply ("IH" $! _ _ _ (_ ++ _)
-        with "[ ] [//] [//] Hl Hcsort Hcred HIB [HIC HICi]"); first done.
-      { simpl; iFrame. }
-      iIntros (zs' ws''); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
+      wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
+      iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
       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 //.
@@ -401,37 +388,35 @@ Section mapper.
       by rewrite right_id_L !assoc_L.
   Qed.
 
-  Lemma par_map_reduce_spec n vmap vred l vs xs :
+  Lemma par_map_reduce_spec n vmap vred l xs :
     0 < n →
     map_spec IA IZB map vmap -∗
     map_spec IZBs IC (curry red) vred -∗
-    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, IA x v }}}
+    {{{ llist IA l xs }}}
       par_map_reduce #n vmap vred #l
-    {{{ k zs ws, RET #k;
-      ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist k ws ∗ [∗ list] z;w ∈ zs;ws, IC z w
-    }}}.
+    {{{ k zs, RET #k; ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC k zs }}}.
   Proof.
-    iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "[Hl HI] HΦ". wp_lam; wp_pures.
+    iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
     wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (cmap) "Hcmap".
     wp_apply (start_chan_proto_spec N (sort_elem_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
     { wp_apply (sort_elem_service_spec N with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
     rewrite right_id.
-    wp_apply (par_map_reduce_map_server_spec with "[$Hl $Hcmap $Hcsort $HI]"); first lia.
+    wp_apply (par_map_reduce_map_server_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "Hcsort /=". wp_select; wp_pures; simpl.
     wp_apply (start_map_service_spec with "Hred [//]"); iIntros (cred) "Hcred".
     wp_branch as %_|%Hnil; last first.
     { wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-      iApply ("HΦ" $! k []); simpl. iFrame. iSplit; [iPureIntro|done].
+      iApply ("HΦ" $! k [] with "[$Hk]"); simpl.
       by rewrite /map_reduce /= -Hiys -Hnil. }
     wp_recv ([i y] ?) as (_ w ->) "HIB /="; wp_pures.
     wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
-    wp_apply (par_map_reduce_reduce_server_spec _ _ [] (Some (i, y, w)) [] _ []
+    wp_apply (par_map_reduce_reduce_server_spec _ _ [] (Some (i, y, w))
       with "[$Hk $Hcsort $Hcred $HIB]"); simpl; auto; [lia|set_solver|].
-    iIntros (zs ws). rewrite /= gmultiset_elements_empty !right_id.
-    iDestruct 1 as (Hzs) "[Hk HIC]". wp_pures.
-    iApply ("HΦ" with "[$Hk $HIC]"). by rewrite Hzs Hiys.
+    iIntros (zs). rewrite /= gmultiset_elements_empty !right_id.
+    iDestruct 1 as (Hzs) "Hk". wp_pures.
+    iApply ("HΦ" with "[$Hk]"). by rewrite Hzs Hiys.
   Qed.
 End mapper.

theories/examples/sort.v

@@ -34,47 +34,42 @@ Section sort.
     (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
          `{!RelDecision R, !Total R} (cmp : val),
        MSG cmp {{ cmp_spec I R cmp }};
-     <!> (xs : list A) (l : loc) (vs : list val),
-       MSG #l {{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, I x v }};
-     <?> (xs' : list A) (vs' : list val),
-       MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗
-                  llist l vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
+     <!> (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.
 
   Lemma lmerge_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
-      `{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 vs1 vs2 :
+      `{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 :
     cmp_spec I R cmp -∗
-    {{{
-      llist l1 vs1 ∗ llist l2 vs2 ∗
-      ([∗ list] x;v ∈ xs1;vs1, I x v) ∗ ([∗ list] x;v ∈ xs2;vs2, I x v)
-    }}}
+    {{{ llist I l1 xs1 ∗ llist I l2 xs2 }}}
       lmerge cmp #l1 #l2
-    {{{ ws, RET #(); llist l1 ws ∗ [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
+    {{{ RET #(); llist I l1 (list_merge R xs1 xs2) }}}.
   Proof.
-    iIntros "#Hcmp" (Ψ) "!> (Hl1 & Hl2 & HI1 & HI2) HΨ".
-    iLöb as "IH" forall (l2 xs1 xs2 vs1 vs2 Ψ).
+    iIntros "#Hcmp" (Ψ) "!> [Hl1 Hl2] HΨ".
+    iLöb as "IH" forall (l2 xs1 xs2 Ψ).
     wp_lam. wp_apply (lisnil_spec with "Hl1"); iIntros "Hl1".
-    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
+    destruct xs1 as [|x1 xs1]; wp_pures.
     { 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".
-    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; done || wp_pures.
+    destruct xs2 as [|x2 xs2]; wp_pures.
     { iApply "HΨ". iFrame. }
-    wp_apply (lhead_spec with "Hl1"); iIntros "Hl1".
-    wp_apply (lhead_spec with "Hl2"); iIntros "Hl2".
-    iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".
-    wp_apply ("Hcmp" with "[$HI1 $HI2]"); iIntros "[HI1 HI2]".
+    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] /=".
     case_bool_decide; wp_pures.
     - rewrite decide_True //.
-      wp_apply (lpop_spec with "Hl1"); iIntros "Hl1".
-      wp_apply ("IH" $! _ _ (x2 :: _) with "Hl1 Hl2 HI1' [$HI2 $HI2']").
-      iIntros (ws) "[Hl1 HI]".
-      wp_apply (lcons_spec with "Hl1"); iIntros "Hl1". iApply "HΨ". iFrame.
+      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.
     - rewrite decide_False //.
-      wp_apply (lpop_spec with "Hl2"); iIntros "Hl2".
-      wp_apply ("IH" $! _ (x1 :: _) with "Hl1 Hl2 [$HI1 $HI1'] HI2'").
-      iIntros (ws) "[Hl1 HI]".
-      wp_apply (lcons_spec with "Hl1"); iIntros "Hl1". iApply "HΨ". iFrame.
+      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.
   Qed.
 
   Lemma sort_service_spec p c :
@@ -84,16 +79,14 @@ Section sort.
   Proof.
     iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
     wp_recv (A I R ?? cmp) as "#Hcmp".
-    wp_recv (xs l vs) as "[Hl HI]".
+    wp_recv (xs l) as "Hl".
     wp_apply (llength_spec with "Hl"); iIntros "Hl".
-    iDestruct (big_sepL2_length with "HI") as %<-.
     wp_op; case_bool_decide as Hlen; wp_if.
     { assert (Sorted R xs).
       { destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
-      wp_send with "[$Hl $HI]"; first by auto. by iApply "HΨ". }
+      wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
     wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".