Use proper linked lists instead of functional lists.

TODO: fix in-place merge function.

_CoqProject

 -Q theories actris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/utils/auth_excl.v
-theories/utils/list.v
+theories/utils/flist.v
+theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
 theories/channel/channel.v

theories/channel/channel.v

 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From actris.utils Require Import auth_excl list.
+From actris.utils Require Import auth_excl llist.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
@@ -11,8 +11,8 @@ Definition side_elim {A} (s : side) (l r : A) : A :=
 
 Definition new_chan : val :=
   λ: <>,
-     let: "l" := ref (lnil #()) in
-     let: "r" := ref (lnil #()) in
+     let: "l" := lnil #() in
+     let: "r" := lnil #() in
      let: "lk" := newlock #() in
      ((("l","r"),"lk"), (("r","l"),"lk")).
 
@@ -21,7 +21,7 @@ Definition send : val :=
     let: "lk" := Snd "c" in
     acquire "lk";;
     let: "l" := Fst (Fst "c") in
-    "l" <- lsnoc !"l" "v";;
+    lsnoc "l" "v";;
     release "lk".
 
 Definition try_recv : val :=
@@ -29,11 +29,7 @@ Definition try_recv : val :=
     let: "lk" := Snd "c" in
     acquire "lk";;
     let: "l" := Snd (Fst "c") in
-    let: "ret" :=
-      match: !"l" with
-        SOME "p" => "l" <- Snd "p";; SOME (Fst "p")
-      | NONE => NONE
-      end in
+    let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
     release "lk";; "ret".
 
 Definition recv : val :=
@@ -52,27 +48,32 @@ Definition chanΣ : gFunctors :=
 Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
+(** MOVE TO IRIS *)
+Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
+Proof.
+  apply strongly_atomic_atomic, ectx_language_atomic;
+    [inversion 1; naive_solver
+    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
+Qed.
+
 Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
-  Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
-    (∃ l' : loc, ⌜l = #l'⌝ ∧ l' ↦ llist xs)%I.
-
   Record chan_name := Chan_name {
     chan_lock_name : gname;
     chan_l_name : gname;
     chan_r_name : gname
   }.
 
-  Definition chan_inv (γ : chan_name) (l r : val) : iProp Σ :=
+  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
     (∃ ls rs,
-      is_list_ref l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
-      is_list_ref r rs ∗ own (chan_r_name γ) (● to_auth_excl rs))%I.
+      llist l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
+      llist r rs ∗ own (chan_r_name γ) (● to_auth_excl rs))%I.
   Typeclasses Opaque chan_inv.
 
   Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
-    (∃ l r lk : val,
-      ⌜ c1 = ((l, r), lk)%V ∧ c2 = ((r, l), lk)%V ⌝ ∗
+    (∃ (l r : loc) (lk : val),
+      ⌜ c1 = ((#l, #r), lk)%V ∧ c2 = ((#r, #l), lk)%V ⌝ ∗
       is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
 
   Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
@@ -91,20 +92,15 @@ Section channel.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
     wp_lam.
-    wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
-    wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
+    wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
+    wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
     iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
     { by apply auth_both_valid. }
     iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
-    iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
-    { rewrite /is_list_ref; eauto. }
-    iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
-    { rewrite /is_list_ref; eauto. }
     wp_apply (newlock_spec N (∃ ls rs,
-      is_list_ref #l ls ∗ own lsγ (● to_auth_excl ls) ∗
-      is_list_ref #r rs ∗ own rsγ (● to_auth_excl rs))%I
-                with "[Hl Hr Hls Hrs]").
+      llist l ls ∗ own lsγ (● to_auth_excl ls) ∗
+      llist 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.
@@ -113,9 +109,9 @@ Section channel.
 
   Lemma chan_inv_alt s γ l r :
     chan_inv γ l r ⊣⊢ ∃ ls rs,
-      is_list_ref (side_elim s l r) ls ∗
+      llist (side_elim s l r) ls ∗
       own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
-      is_list_ref (side_elim s r l) rs ∗
+      llist (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 //=.
@@ -131,24 +127,20 @@ Section channel.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
-    assert (side_elim s (l, r, lk)%V (r, l, lk)%V =
-      ((side_elim s l r, side_elim s r l), lk)%V) as -> by (by destruct s).
+    assert (side_elim s (#l, #r, lk)%V (#r, #l, lk)%V =
+      ((#(side_elim s l r), #(side_elim s r l)), lk)%V) as -> by (by destruct s).
     wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    wp_pures.
     iDestruct (chan_inv_alt s with "Hinv") as
-      (vs ws) "(Href & Hvs & Href' & Hws)".
-    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
-    wp_load.
-    wp_apply (lsnoc_spec with "[//]"); iIntros (_).
-    wp_bind (_ <- _)%E.
+      (vs ws) "(Hll & Hvs & Href' & Hws)".
+    wp_seq. wp_bind (Fst (_,_)%V)%E.
     iMod "HΦ" as (vs') "[Hchan HΦ]".
     iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
     iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
-    wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
-    iModIntro.
+    wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
+    wp_apply (lsnoc_spec with "Hll"); iIntros "Hll".
     wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
     iApply (chan_inv_alt s).
-    rewrite /is_list_ref. eauto 20 with iFrame.
+    rewrite /llist. eauto 20 with iFrame.
   Qed.
 
   Lemma try_recv_spec Φ E γ c1 c2 s :
@@ -162,28 +154,27 @@ Section channel.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
-    assert (side_elim s (r, l, lk)%V (l, r, lk)%V =
-      ((side_elim s r l, side_elim s l r), lk)%V) as -> by (by destruct s).
+    assert (side_elim s (#r, #l, lk)%V (#l, #r, lk)%V =
+      ((#(side_elim s r l), #(side_elim s l r)), lk)%V) as -> by (by destruct s).
     wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    wp_pures.
     iDestruct (chan_inv_alt s with "Hinv")
-      as (vs ws) "(Href & Hvs & Href' & Hws)".
-    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
-    wp_bind (! _)%E. destruct vs as [|v vs]; simpl.
-    - iDestruct "HΦ" as "[>HΦ _]". wp_load. iMod "HΦ"; iModIntro.
+      as (vs ws) "(Hll & Hvs & Href' & Hws)".
+    wp_seq. wp_bind (Fst (_,_)%V)%E. destruct vs as [|v vs]; simpl.
+    - iDestruct "HΦ" as "[>HΦ _]". wp_pures. iMod "HΦ"; iModIntro.
+      wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_pures.
       wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
       { iApply (chan_inv_alt s).
-        rewrite /is_list_ref. eauto 10 with iFrame. }
+        rewrite /llist. eauto 10 with iFrame. }
       iIntros (_). by wp_pures.
     - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
       iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
       iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
-      wp_load.
-      iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
-      wp_store; wp_pures.
+      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 (release_spec with "[-HΦ $Hlocked $Hlock]").
       { iApply (chan_inv_alt s).
-        rewrite /is_list_ref. eauto 10 with iFrame. }
+        rewrite /llist. eauto 10 with iFrame. }
       iIntros (_). by wp_pures.
   Qed.
 

theories/examples/loop_sort.v

 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
-From actris.utils Require Import list.
 From actris.examples Require Import sort.
 
 Definition loop_sort_service : val :=

theories/examples/map.v

 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
-From actris.utils Require Import list contribution.
+From actris.utils Require Import llist contribution.
 From iris.algebra Require Import gmultiset.
 
 Definition map_worker : val :=
@@ -30,22 +30,25 @@ Definition start_map_service : val := λ: "n" "map",
 
 Definition par_map_server : val :=
   rec: "go" "n" "c" "xs" "ys" :=
-    if: "n" = #0 then "ys" else
+    if: "n" = #0 then #() else
     if: recv "c" then (* send item to map_worker *)
       if: lisnil "xs" then
         send "c" #false;;
         "go" ("n" - #1) "c" "xs" "ys"
       else
         send "c" #true;;
-        send "c" (lhead "xs");;
-        "go" "n" "c" (ltail "xs") "ys"
+        send "c" (lpop "xs");;
+        "go" "n" "c" "xs" "ys"
     else (* receive item from map_worker *)
       let: "zs" := recv "c" in
-      "go" "n" "c" "xs" (lapp "zs" "ys").
+      lprep "ys" "zs";;
+      "go" "n" "c" "xs" "ys".
 
 Definition par_map : val := λ: "n" "map" "xs",
   let: "c" := start_map_service "n" "map" in
-  par_map_server "n" "c" "xs" (lnil #()).
+  let: "ys" := lnil #() in
+  par_map_server "n" "c" "xs" "ys";;
+  "ys".
 
 Class mapG Σ A `{Countable A} := {
   map_contributionG :> contributionG Σ (gmultisetUR A);
@@ -62,7 +65,7 @@ Section map.
   Definition map_spec (vmap : val) : iProp Σ := (∀ x v,
     {{{ IA x v }}}
       vmap v
-    {{{ ws, RET (llist ws); [∗ list] y;w ∈ map x;ws, IB y w }}})%I.
+    {{{ l ws, RET #l; llist l ws ∗ [∗ list] y;w ∈ map x;ws, IB y w }}})%I.
 
   Definition map_worker_protocol_aux (rec : nat -d> gmultiset A -d> iProto Σ) :
       nat -d> gmultiset A -d> iProto Σ := λ i X,
@@ -72,7 +75,7 @@ Section map.
         <+>
       rec (pred i) X
      ) <{⌜ i ≠ 1 ∨ X = ∅ ⌝}&>
-         <?> x ws, MSG llist ws {{ ⌜ x ∈ X ⌝ ∧ [∗ list] y;w ∈ map x;ws, IB y w }};
+         <?> x (l : loc) ws, MSG #l {{ ⌜ x ∈ X ⌝ ∗ llist l ws ∗ [∗ list] y;w ∈ map x;ws, IB y w }};
          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.
@@ -109,7 +112,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 (w) "HI".
+    clear dependent i X. iIntros "Hu". wp_apply ("Hmap" with "HI"); iIntros (l ws) "HI".
     wp_apply (acquire_spec with "[$Hlk $Hu]"); iIntros "[Hl H]".
     iDestruct "H" as (i X) "[Hs Hc]".
     iDestruct (@server_agree with "Hs Hγ")
@@ -156,38 +159,39 @@ Section map.
     wp_apply (start_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
   Qed.
 
-  Lemma par_map_server_spec n c vs xs ws X ys :
+  Lemma par_map_server_spec n c l k vs xs ws 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)
     }}}
-      par_map_server #n c (llist vs) (llist ws)
-    {{{ ys' ws', RET (llist ws');
-       ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ ∗ [∗ list] y;w ∈ ys' ++ ys;ws', IB y w
+      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
     }}}.
   Proof.
-    iIntros (Hn Φ) "(Hc & HIA & HIB) HΦ".
-    iLöb as "IH" forall (n vs xs ws X ys Hn Φ); wp_rec; wp_pures; simpl.
+    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.
     case_bool_decide; wp_pures; simplify_eq/=.
     { destruct Hn as [-> ->]; first lia.
-      iApply ("HΦ" $! []); simpl; auto. }
+      iApply ("HΦ" $! []); simpl; auto with iFrame. }
     destruct n as [|n]=> //=. wp_branch as %?|%_; wp_pures.
-    - wp_apply (lisnil_spec with "[//]"); iIntros (_).
+    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct vs as [|v vs], xs as [|x xs]; csimpl; try done; wp_pures.
       + wp_select. wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-        iApply ("IH" with "[%] Hc [//] [$] HΦ"); naive_solver.
+        iApply ("IH" with "[%] Hl Hk Hc [//] [$] HΦ"); naive_solver.
       + iDestruct "HIA" as "[HIAx HIA]". wp_select.
-        wp_apply (lhead_spec with "[//]"); iIntros (_).
+        wp_apply (lpop_spec with "Hl"); iIntros "Hl".
         wp_send with "[$HIAx]".
-        wp_apply (ltail_spec with "[//]"); iIntros (_).
-        wp_apply ("IH" with "[] Hc HIA HIB"); first done.
+        wp_apply ("IH" with "[] Hl Hk Hc HIA HIB"); first done.
         iIntros (ys' ws').
         rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
         rewrite assoc_L -(comm _ [x]). iApply "HΦ".
-    - wp_recv (x w) as (Hx) "HIBx".
-      wp_apply (lapp_spec with "[//]"); iIntros (_).
-      wp_apply ("IH" $! _ _ _ _ _ (_ ++ _) with "[] Hc HIA [HIBx HIB]"); first done.
+    - wp_recv (x l' w) as (Hx) "[Hl' HIBx]".
+      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/=.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
@@ -198,17 +202,18 @@ Section map.
       + by rewrite -assoc_L.
   Qed.
 
-  Lemma par_map_spec n vmap vs xs :
+  Lemma par_map_spec n vmap l vs xs :
     0 < n →
     map_spec vmap -∗
-    {{{ [∗ list] x;v ∈ xs;vs, IA x v }}}
-      par_map #n vmap (llist vs)
-    {{{ ys ws, RET (llist ws); ⌜ys ≡ₚ xs ≫= map⌝ ∗ [∗ list] y;w ∈ ys;ws, IB y w }}}.
+    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, IA x v }}}
+      par_map #n vmap #l
+    {{{ k ys ws, RET #k; ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist k ws ∗ [∗ list] y;w ∈ ys;ws, IB y w }}}.
   Proof.
-    iIntros (?) "#Hmap !>"; iIntros (Φ) "HI HΦ". wp_lam; wp_pures.
+    iIntros (?) "#Hmap !>"; iIntros (Φ) "[Hl HI] HΦ". wp_lam; wp_pures.
     wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (c) "Hc".
-    wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (_).
-    wp_apply (par_map_server_spec _ _ _ _ [] ∅ [] with "[$Hc $HI //]"); first lia.
-    iIntros (ys ws). rewrite /= gmultiset_elements_empty !right_id_L . iApply "HΦ".
+    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Φ".
   Qed.
 End map.

theories/examples/sort.v

 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From actris.utils Require Import list compare.
+From actris.utils Require Export llist compare.
 
-Definition lmerge : val :=
+Definition lmerge : val. (*
   rec: "go" "cmp" "ys" "zs" :=
     if: lisnil "ys" then "zs" else
     if: lisnil "zs" then "ys" else
@@ -12,21 +12,20 @@ Definition lmerge : val :=
     if: "cmp" "y" "z"
     then lcons "y" ("go" "cmp" (ltail "ys") "zs")
     else lcons "z" ("go" "cmp" "ys" (ltail "zs")).
+*) Admitted.
 
 Definition sort_service : val :=
   rec: "go" "c" :=
     let: "cmp" := recv "c" in
     let: "xs" := recv "c" in
-    if: llength !"xs" ≤ #1 then send "c" #() else
-    let: "ys_zs" := lsplit !"xs" in
-    let: "ys" := ref (Fst "ys_zs") in
-    let: "zs" := ref (Snd "ys_zs") in
+    if: llength "xs" ≤ #1 then send "c" #() else
+    let: "zs" := lsplit "xs" in
     let: "cy" := start_chan "go" in
     let: "cz" := start_chan "go" in
-    send "cy" "cmp";; send "cy" "ys";;
+    send "cy" "cmp";; send "cy" "xs";;
     send "cz" "cmp";; send "cz" "zs";;
     recv "cy";; recv "cz";;
-    "xs" <- lmerge "cmp" !"ys" !"zs";;
+    lmerge "cmp" "xs" "zs";;
     send "c" #().
 
 Section sort.
@@ -37,19 +36,22 @@ Section sort.
          `{!RelDecision R, !Total R} (cmp : val),
        MSG cmp {{ cmp_spec I R cmp }};
      <!> (xs : list A) (l : loc) (vs : list val),
-       MSG #l {{ l ↦ llist vs ∗ [∗ list] x;v ∈ xs;vs, I x v }};
+       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 ⌝ ∗
-                  l ↦ llist vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
+                  llist l vs' ∗ [∗ list] x;v ∈ xs';vs', I x v }};
      END)%proto.
 
   Lemma lmerge_spec {A} (I : A → val → iProp Σ) (R : A → A → Prop)
-      `{!RelDecision R, !Total R} (cmp : val) xs1 xs2 vs1 vs2 :
+      `{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 vs1 vs2 :
     cmp_spec I R cmp -∗
-    {{{ ([∗ list] x;v ∈ xs1;vs1, I x v) ∗ ([∗ list] x;v ∈ xs2;vs2, I x v) }}}
-      lmerge cmp (llist vs1) (llist vs2)
-    {{{ ws, RET llist ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
-  Proof.
+    {{{
+      llist l1 vs1 ∗ llist l2 vs2 ∗
+      ([∗ list] x;v ∈ xs1;vs1, I x v) ∗ ([∗ list] x;v ∈ xs2;vs2, I x v)
+    }}}
+      lmerge cmp #l1 #l2
+    {{{ ws, RET #(); llist l1 ws ∗ [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
+  Proof. (*
     iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
     wp_lam. wp_apply (lisnil_spec with "[//]"); iIntros (_).
     destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
@@ -74,7 +76,7 @@ Section sort.
       iIntros (ws) "HI".
       wp_apply (lcons_spec with "[//]"); iIntros (_).
       iApply "HΨ". iFrame.
-  Qed.
+  Qed. *) Admitted.
 
   Lemma sort_service_spec p c :
     {{{ c ↣ iProto_dual sort_protocol <++> p @ N }}}
@@ -85,14 +87,14 @@ Section sort.
     wp_lam.
     wp_recv (A I R ?? cmp) as "#Hcmp".
     wp_recv (xs l vs) as "[Hl HI]".
-    wp_load. wp_apply (llength_spec with "[//]"); iIntros (_).
+    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_load. wp_apply (lsplit_spec with "[//]"); iIntros (vs1 vs2 ->).
-    wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
+    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 _)).
@@ -106,9 +108,7 @@ Section sort.
     wp_send with "[$Hl2 $HI2]".
     wp_recv (ys1 ws1) as (??) "[Hl1 HI1]".
     wp_recv (ys2 ws2) as (??) "[Hl2 HI2]".
-    do 2 wp_load.
-    wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
-    wp_store.
+    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]".
     - iSplit; iPureIntro.
       + by apply (Sorted_list_merge _).

theories/examples/sort_client.v

 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From actris.utils Require Import list compare.
 From actris.examples Require Import sort.
 
 Definition sort_client : val := λ: "cmp" "xs",
@@ -15,10 +14,10 @@ Section sort_client.
   Lemma sort_client_spec {A} (I : A → val → iProp Σ) R
        `{!RelDecision R, !Total R} cmp l (vs : list val) (xs : list A) :
     cmp_spec I R cmp -∗
-    {{{ l ↦ llist vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
+    {{{ llist l vs ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
       sort_client cmp #l
     {{{ ys ws, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗
-               l ↦ llist ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
+               llist l ws ∗ [∗ list] y;w ∈ ys;ws, I y w }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
     wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
@@ -31,9 +30,9 @@ Section sort_client.
   Qed.
 
   Lemma sort_client_Zle_spec l (xs : list Z) :
-    {{{ l ↦ llist (LitV ∘ LitInt <$> xs) }}}
+    {{{ llist l (LitV ∘ LitInt <$> xs) }}}
       sort_client cmpZ #l
-    {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ l ↦ llist (LitV ∘ LitInt <$> ys) }}}.
+    {{{ 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Φ]").

theories/examples/sort_elem.v

@@ -2,7 +2,7 @@ From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From actris.utils Require Import list compare.
+From actris.utils Require Import compare.
 
 Definition cont := true.
 Definition stop := false.

theories/examples/sort_elem_client.v

@@ -2,21 +2,18 @@ From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From actris.utils Require Import list compare.
+From actris.utils Require Import llist compare.
 From actris.examples Require Import sort_elem.
 
 Definition send_all : val :=
   rec: "go" "c" "xs" :=
-    match: "xs" with
-      SOME "p" => send "c" #cont;; send "c" (Fst "p");; "go" "c" (Snd "p")
-    | NONE => #()
-    end.
+    if: lisnil "xs" then #() else
+    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
 
 Definition recv_all : val :=
   rec: "go" "c" :=
-    if: recv "c"
-    then let: "x" := recv "c" in lcons "x" ("go" "c")
-    else lnil #().
+    if: ~recv "c" then lnil #() else
+    let: "x" := recv "c" in lcons "x" ("go" "c").
 
 Definition sort_elem_client : val :=
   λ: "cmp" "xs",
@@ -30,26 +27,28 @@ 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' xs vs :
-    {{{ c ↣ sort_elem_head_protocol I R xs' <++> p @ N ∗ [∗ list] x;v ∈ xs;vs, I x v }}}
-      send_all c (llist vs)
+  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 }}}
+      send_all c #l
     {{{ RET #(); c ↣ sort_elem_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
   Proof.
-    iIntros (Φ) "[Hc HI] HΦ".
+    iIntros (Φ) "(Hl & Hc & HI) HΦ".
     iInduction xs as [|x xs] "IH" forall (xs' vs); destruct vs as [|v vs]=>//.
-    { wp_lam; wp_pures. iApply "HΦ". rewrite right_id_L. iFrame. }
-    iDestruct "HI" as "[HIxv HI]". wp_lam; wp_pures.
-    wp_select. wp_send with "[$HIxv]". wp_apply ("IH" with "Hc HI").
-    by rewrite -assoc_L.
+    { 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.
   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
-    {{{ ys ws, RET (llist ws);
+    {{{ l ys ws, RET #l;
         ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗
-        c ↣ p @ N ∗ [∗ list] y;w ∈ ys;ws, I y w
+        llist l ws ∗ c ↣ p @ N ∗ [∗ list] y;w ∈ ys;ws, I y w
     }}}.
   Proof.
     iIntros (Hsort Φ) "Hc HΦ".
@@ -57,30 +56,32 @@ Section sort_elem_client.
     wp_lam. wp_branch as %_ | %Hperm; wp_pures.
     - wp_recv (y v) as (Htl) "HIxv".
       wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
-      iIntros (ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
-      wp_apply (lcons_spec