From 70e0bae24ce0382a110f0841210ba6d7de074ba4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Jul 2019 22:31:59 +0200
Subject: [PATCH] Kill bigops.

---
 theories/channel/channel.v           |  16 +--
 theories/examples/map.v              |  58 ++++------
 theories/examples/map_reduce.v       | 131 ++++++++++-------------
 theories/examples/sort.v             |  67 ++++++------
 theories/examples/sort_client.v      |  27 +----
 theories/examples/sort_elem_client.v |  47 ++++-----
 theories/utils/llist.v               | 152 ++++++++++++++++-----------
 7 files changed, 232 insertions(+), 266 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 3bbacfb..fdca205 100644
--- a/theories/channel/channel.v
+++ b/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. }
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 1d62b9d..610eb64 100644
--- a/theories/examples/map.v
+++ b/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.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index b0080bd..3061b5b 100644
--- a/theories/examples/map_reduce.v
+++ b/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.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index adc93fb..b2d0043 100644
--- a/theories/examples/sort.v
+++ b/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]".
     wp_apply (start_chan_proto_spec N sort_protocol); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcy"); auto. }
@@ -101,13 +94,13 @@ Section sort.
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hcmp]".
-    wp_send with "[$Hl1 $HI1]".
+    wp_send with "[$Hl1]".
     wp_send with "[$Hcmp]".
-    wp_send with "[$Hl2 $HI2]".
-    wp_recv (ys1 ws1) as (??) "[Hl1 HI1]".
-    wp_recv (ys2 ws2) as (??) "[Hl2 HI2]".
-    wp_apply (lmerge_spec with "Hcmp [$Hl1 $Hl2 $HI1 $HI2]"); iIntros (ws) "[Hl HI]".
-    wp_send ((list_merge R ys1 ys2) ws) with "[$Hl $HI]".
+    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]".
     - iSplit; iPureIntro.
       + by apply (Sorted_list_merge _).
       + rewrite (merge_Permutation R). by f_equiv.
diff --git a/theories/examples/sort_client.v b/theories/examples/sort_client.v
index 095c5da..c6c876e 100644
--- a/theories/examples/sort_client.v
+++ b/theories/examples/sort_client.v
@@ -12,12 +12,11 @@ Section sort_client.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
   Lemma sort_client_spec {A} (I : A → val → iProp Σ) R
-       `{!RelDecision R, !Total R} cmp l (vs : list val) (xs : list A) :
+       `{!RelDecision R, !Total R} cmp l (xs : list A) :
     cmp_spec I R cmp -∗
-    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+    {{{ llist I l xs }}}
       sort_client cmp #l
-    {{{ ys ws, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
-               llist l ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
+    {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
     wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
@@ -25,25 +24,7 @@ Section sort_client.
       wp_apply (sort_service_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
     wp_send with "[$Hl]".
-    wp_recv (ys ws) as "(Hsorted & Hperm & Hl & HI)".
+    wp_recv (ys) as "(Hsorted & Hperm & Hl)".
     wp_pures. iApply "HΦ"; iFrame.
   Qed.
-
-  Lemma sort_client_Zle_spec l (xs : list Z) :
-    {{{ llist l (LitV ∘ LitInt <$> xs) }}}
-      sort_client cmpZ #l
-    {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ llist l (LitV ∘ LitInt <$> ys) }}}.
-  Proof.
-    iIntros (Φ) "Hl HΦ".
-    iApply (sort_client_spec IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
-    { iApply cmpZ_spec. }
-    { iFrame "Hl". iInduction xs as [|x xs] "IH"; csimpl; by iFrame "#". }
-    iIntros "!>" (ys ws) "(?&?&?&HI)".
-    iAssert ⌜ ws = (LitV ∘ LitInt) <$> ys ⌝%I with "[HI]" as %->.
-    { iInduction ys as [|y ys] "IH" forall (ws);
-        destruct ws as [|w ws]; csimpl; try done.
-      iDestruct "HI" as "[-> HI2]".
-      by iDestruct ("IH" with "HI2") as %->. }
-    iApply ("HΦ" $! ys with "[$]").
-  Qed.
 End sort_client.
diff --git a/theories/examples/sort_elem_client.v b/theories/examples/sort_elem_client.v
index 9732425..ee1ff15 100644
--- a/theories/examples/sort_elem_client.v
+++ b/theories/examples/sort_elem_client.v
@@ -28,61 +28,56 @@ Section sort_elem_client.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
   Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
 
-  Lemma send_all_spec c p xs' l xs vs :
-    {{{ llist l vs ∗ c ↣ sort_elem_head_protocol I R xs' <++> p @ N ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+  Lemma send_all_spec c p xs' l xs :
+    {{{ llist I l xs ∗ c ↣ sort_elem_head_protocol I R xs' <++> p @ N }}}
       send_all c #l
     {{{ RET #(); c ↣ sort_elem_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
   Proof.
-    iIntros (Φ) "(Hl & Hc & HI) HΦ".
-    iInduction xs as [|x xs] "IH" forall (xs' vs); destruct vs as [|v vs]=>//.
+    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. }
-    iDestruct "HI" as "[HIxv HI]". wp_lam.
-    wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_select.
-    wp_apply (lpop_spec with "Hl"); iIntros "Hl".
-    wp_send with "[$HIxv]". wp_apply ("IH" with "Hl Hc HI"). by rewrite -assoc_L.
+    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 xs ys' :
     Sorted R ys' →
     {{{ c ↣ sort_elem_tail_protocol I R xs ys' <++> p @ N }}}
       recv_all c
-    {{{ l ys ws, RET #l;
-        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗
-        llist l ws ∗ c ↣ p @ N ∗ [∗ list] y;w ∈ ys;ws, I y w
+    {{{ l ys, RET #l;
+        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗ llist I l ys ∗ c ↣ p @ N
     }}}.
   Proof.
     iIntros (Hsort Φ) "Hc HΦ".
     iLöb as "IH" forall (xs ys' Φ Hsort).
     wp_lam. wp_branch as %_ | %Hperm; wp_pures.
-    - wp_recv (y v) as (Htl) "HIxv".
+    - wp_recv (y v) as (Htl) "HIx".
       wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
-      iIntros (l ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "(Hl & Hc & HI)".
-      wp_apply (lcons_spec with "Hl"); iIntros "Hl"; wp_pures.
-      iApply ("HΦ" $! _ (y :: ys)); simpl; eauto with iFrame.
+      iIntros (l 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.
     - wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
-      iApply ("HΦ" $! _ [] []); rewrite /= right_id_L; by iFrame.
+      iApply ("HΦ" $! _ []); rewrite /= right_id_L; by iFrame.
   Qed.
 
-  Lemma sort_client_spec cmp l vs xs :
+  Lemma sort_client_spec cmp l xs :
     cmp_spec I R cmp -∗
-    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+    {{{ llist I l xs }}}
       sort_elem_client cmp #l
-    {{{ k ys ws, RET #k;
-        ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
-        llist k ws ∗ [∗ list] y;w ∈ ys;ws, I y w
-    }}}.
+    {{{ k ys, RET #k; ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I k ys }}}.
   Proof.
-    iIntros "#Hcmp !>" (Φ) "[Hl HI] HΦ". wp_lam.
+    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
     wp_apply (start_chan_proto_spec N (sort_elem_top_protocol <++> END)%proto);
       iIntros (c) "Hc".
     { wp_apply (sort_elem_service_top_spec N with "Hc"); auto. }
     rewrite /sort_elem_top_protocol.
     wp_send (A I R) with "[$Hcmp]".
-    wp_apply (send_all_spec with "[$Hl $HI $Hc]"); iIntros "Hc".
+    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "Hc".
     wp_select.
-    wp_apply (recv_all_spec _ _ _ [] with "[$Hc]"); auto.
-    iIntros (k ys ws) "/=". iDestruct 1 as (??) "(Hk & _ & HI)".
+    wp_apply (recv_all_spec with "Hc"); auto.
+    iIntros (k ys) "/=". iDestruct 1 as (??) "[Hk _]".
     iApply "HΦ"; auto with iFrame.
   Qed.
 End sort_elem_client.
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index f57d57c..c4be3f0 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -2,10 +2,11 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
 
 (** Immutable ML-style functional lists *)
-Fixpoint llist `{heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
-  match vs with
+Fixpoint llist `{heapG Σ} {A} (I : A → val → iProp Σ)
+    (l : loc) (xs : list A) : iProp Σ :=
+  match xs with
   | [] => l ↦ NONEV
-  | v :: vs => ∃ l' : loc, l ↦ SOMEV (v,#l') ∗ llist l' vs
+  | x :: xs => ∃ (v : val) (l' : loc), I x v ∗ l ↦ SOMEV (v,#l') ∗ llist I l' xs
   end%I.
 Arguments llist : simpl never.
 
@@ -72,137 +73,160 @@ Definition lsplit_at : val :=
 Definition lsplit : val := λ: "l", lsplit_at "l" (llength "l" `quot` #2).
 
 Section lists.
-Context `{heapG Σ}.
+Context `{heapG Σ} {A} (I : A → val → iProp Σ).
 Implicit Types i : nat.
-Implicit Types v : val.
-Implicit Types vs : list val.
-Local Arguments llist {_ _} _ !_ /.
+Implicit Types xs : list A.
+Implicit Types l : loc.
+Local Arguments llist {_ _ _} _ _ !_ /.
 
 Lemma lnil_spec :
-  {{{ True }}} lnil #() {{{ l, RET #l; llist l [] }}}.
+  {{{ True }}} lnil #() {{{ l, RET #l; llist I l [] }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_alloc l. by iApply "HΦ". Qed.
 
-Lemma lcons_spec l v vs :
-  {{{ llist l vs }}} lcons v #l {{{ RET #(); llist l (v :: vs) }}}.
+Lemma lcons_spec l x xs v :
+  {{{ llist I l xs ∗ I x v }}} lcons v #l {{{ RET #(); llist I l (x :: xs) }}}.
 Proof.
-  iIntros (Φ) "Hll HΦ". wp_lam. destruct vs as [|v' vs]; simpl; wp_pures.
+  iIntros (Φ) "[Hll Hx] HΦ". wp_lam. destruct xs as [|x' xs]; simpl; wp_pures.
   - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
-  - iDestruct "Hll" as (l') "[Hl Hll]".
-    wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
+  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)".
+    wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto 10 with iFrame.
 Qed.
 
-Lemma lisnil_spec l vs:
-  {{{ llist l vs }}}
+Lemma lisnil_spec l xs:
+  {{{ llist I l xs }}}
     lisnil #l
-  {{{ RET #(if vs is [] then true else false); llist l vs }}}.
+  {{{ RET #(if xs is [] then true else false); llist I l xs }}}.
 Proof.
-  iIntros (Φ) "Hll HΦ". wp_lam. destruct vs as [|v' vs]; simpl; wp_pures.
+  iIntros (Φ) "Hll HΦ". wp_lam. destruct xs as [|x xs]; simpl; wp_pures.
   - wp_load; wp_pures. by iApply "HΦ".
-  - iDestruct "Hll" as (l') "[Hl Hll]".
+  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)".
     wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma lhead_spec l v vs :
-  {{{ llist l (v :: vs) }}} lhead #l {{{ RET v; llist l (v :: vs) }}}.
+(** Not the nicest spec, they leaks *)
+Lemma lhead_spec_aux l x xs :
+  {{{ llist I l (x :: xs) }}}
+    lhead #l
+  {{{ v (l' : loc), RET v; I x v ∗ l ↦ SOMEV (v,#l') ∗ llist I l' xs }}}.
 Proof.
-  iIntros (Φ) "/=". iDestruct 1 as (l') "[Hl Hll]". iIntros "HΦ".
+  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
   wp_lam. wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
 Qed.
-
-Lemma lpop_spec l v vs :
-  {{{ llist l (v :: vs) }}} lpop #l {{{ RET v; llist l vs }}}.
+Lemma lpop_spec_aux l l' v xs :
+  {{{ l ↦ SOMEV (v,#l') ∗ llist I l' xs }}} lpop #l {{{ RET v; llist I l xs }}}.
 Proof.
-  iIntros (Φ) "/=". iDestruct 1 as (l') "[Hl Hll]". iIntros "HΦ".
-  wp_lam. wp_load. wp_pures. destruct vs as [|v' vs]; simpl; wp_pures.
+  iIntros (Φ) "[Hl Hll] HΦ".
+  wp_lam. wp_load. wp_pures. destruct xs as [|x' xs]; simpl; wp_pures.
   - wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
-  - iDestruct "Hll" as (l'') "[Hl' Hll]".
+  - iDestruct "Hll" as (v' l'') "(HIx' & Hl' & Hll)".
     wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma llookup_spec l i vs v :
-  vs !! i = Some v →
-  {{{ llist l vs }}} llookup #l #i {{{ RET v; llist l vs }}}.
+Lemma lhead_spec l x xs :
+  {{{ llist I l (x :: xs) }}}
+    lhead #l
+  {{{ v, RET v; I x v ∗ (I x v -∗ llist I l (x :: xs)) }}}.
+Proof.
+  iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
+  iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
+  simpl; eauto with iFrame.
+Qed.
+
+Lemma lpop_spec l x xs :
+  {{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v ∗ llist I l xs }}}.
+Proof.
+  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
+  wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
+Qed.
+
+Lemma llookup_spec l i xs x :
+  xs !! i = Some x →
+  {{{ llist I l xs }}}
+    llookup #l #i
+  {{{ v, RET v; I x v ∗ (I x v -∗ llist I l xs) }}}.
 Proof.
   iIntros (Hi Φ) "Hll HΦ".
-  iInduction vs as [|v' vs] "IH" forall (l i v Hi Φ); [done|simpl; wp_rec; wp_pures].
+  iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
   destruct i as [|i]; simplify_eq/=; wp_pures.
-  - wp_apply (lhead_spec with "Hll"); iIntros "Hll". by iApply "HΦ".
-  - iDestruct "Hll" as (l') "[Hl' Hll]". wp_load; wp_pures.
+  - wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
+    iApply "HΦ"; eauto with iFrame.
+  - iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
     rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply ("IH" with "[//] Hll"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
+    wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
+    iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
 Qed.
 
-Lemma llength_spec l vs :
-  {{{ llist l vs }}} llength #l {{{ RET #(length vs); llist l vs }}}.
+Lemma llength_spec l xs :
+  {{{ llist I l xs }}} llength #l {{{ RET #(length xs); llist I l xs }}}.
 Proof.
   iIntros (Φ) "Hll HΦ".
-  iInduction vs as [|v vs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
+  iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load; wp_pures. by iApply "HΦ".
-  - iDestruct "Hll" as (l') "[Hl' Hll]". wp_load; wp_pures.
+  - iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
     wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
     rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma lapp_spec l1 l2 vs1 vs2 :
-  {{{ llist l1 vs1 ∗ llist l2 vs2 }}}
+Lemma lapp_spec l1 l2 xs1 xs2 :
+  {{{ llist I l1 xs1 ∗ llist I l2 xs2 }}}
     lapp #l1 #l2
-  {{{ RET #(); llist l1 (vs1 ++ vs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ".
-  iInduction vs1 as [|v1 vs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
-  - wp_load. wp_pures. destruct vs2 as [|v2 vs2]; simpl; wp_pures.
+  iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
+  - wp_load. wp_pures. destruct xs2 as [|x2 xs2]; simpl; wp_pures.
     + wp_load. wp_store. iApply "HΦ". eauto with iFrame.
-    + iDestruct "Hll2" as (l2') "[Hl2 Hll2]". wp_load. wp_store.
+    + iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
       iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
-  - iDestruct "Hll1" as (l') "[Hl1 Hll1]". wp_load; wp_pures.
+  - iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
     wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
     iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma lprep_spec l1 l2 vs1 vs2 :
-  {{{ llist l1 vs2 ∗ llist l2 vs1 }}}
+Lemma lprep_spec l1 l2 xs1 xs2 :
+  {{{ llist I l1 xs2 ∗ llist I l2 xs1 }}}
     lprep #l1 #l2
-  {{{ RET #(); llist l1 (vs1 ++ vs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
   wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
-  iDestruct "Hl1" as (w) "Hl1". destruct (vs1 ++ vs2) as [|v vs]; simpl; wp_pures.
+  iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
   - wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
-  - iDestruct "Hll2" as (l') "[Hl2 Hll2]". wp_load. wp_store.
+  - iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
     iApply "HΦ"; iSplitR "Hl2"; eauto with iFrame.
 Qed.
 
-Lemma lsnoc_spec l vs v :
-  {{{ llist l vs }}} lsnoc #l v {{{ RET #(); llist l (vs ++ [v]) }}}.
+Lemma lsnoc_spec l xs x v :
+  {{{ llist I l xs ∗ I x v }}} lsnoc #l v {{{ RET #(); llist I l (xs ++ [x]) }}}.
 Proof.
-  iIntros (Φ) "Hll HΦ".
-  iInduction vs as [|v' vs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
+  iIntros (Φ) "[Hll HIx] HΦ".
+  iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
-  - iDestruct "Hll" as (l') "[Hl Hll]". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
+  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
+    wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma lsplit_at_spec l vs (n : nat) :
-  {{{ llist l vs }}}
+Lemma lsplit_at_spec l xs (n : nat) :
+  {{{ llist I l xs }}}
     lsplit_at #l #n
-  {{{ k, RET #k; llist l (take n vs) ∗ llist k (drop n vs) }}}.
+  {{{ k, RET #k; llist I l (take n xs) ∗ llist I k (drop n xs) }}}.
 Proof.
   iIntros (Φ) "Hll HΦ".
-  iInduction vs as [|v vs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
+  iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
   - destruct n as [|n]; simpl; wp_pures.
     + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame.
     + wp_load. wp_alloc k. iApply "HΦ"; iFrame.
-  - iDestruct "Hll" as (l') "[Hl Hll]". destruct n as [|n]; simpl; wp_pures.
+  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
     + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
     + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
       wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
       iApply "HΦ"; eauto with iFrame.
 Qed.
 
-Lemma lsplit_spec l vs :
-  {{{ llist l vs }}}
+Lemma lsplit_spec l xs :
+  {{{ llist I l xs }}}
     lsplit #l
-  {{{ k ws1 ws2, RET #k; ⌜ vs = ws1 ++ ws2 ⌝ ∗ llist l ws1 ∗ llist k ws2 }}}.
+  {{{ k xs1 xs2, RET #k; ⌜ xs = xs1 ++ xs2 ⌝ ∗ llist I l xs1 ∗ llist I k xs2 }}}.
 Proof.
   iIntros (Φ) "Hl HΦ". wp_lam.
   wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
-- 
GitLab