Added list reverse example

_CoqProject

@@ -19,6 +19,7 @@ theories/examples/map.v
 theories/examples/map_reduce.v
 theories/examples/swap_mapper.v
 theories/examples/subprotocols.v
+theories/examples/list_rev.v
 theories/logrel/model.v
 theories/logrel/telescopes.v
 theories/logrel/subtyping.v

theories/examples/list_rev.v

+From actris.channel Require Import proofmode proto channel.
+From iris.proofmode Require Import tactics.
+From actris.utils Require Import llist.
+
+Definition list_rev_service : val :=
+  λ: "c",
+    let: "l" := recv "c" in
+    lreverse "l";; send "c" #().
+
+Definition list_rev_client : val :=
+  λ: "l",
+    let: "c" := start_chan list_rev_service in
+    send "c" "l";; recv "c".
+
+Section list_rev_example.
+  Context `{heapG Σ, chanG Σ}.
+
+  Definition list_rev_prot : iProto Σ :=
+    (<! (l : loc) (vs : list val)> MSG #l {{ llist internal_eq l vs }} ;
+     <?> MSG #() {{ llist internal_eq l (reverse vs) }} ; END)%proto.
+
+  Lemma list_rev_service_spec c prot :
+    {{{ c ↣ (iProto_app (iProto_dual list_rev_prot) prot) }}}
+      list_rev_service c
+    {{{ RET #(); c ↣ prot }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    wp_lam.
+    wp_recv (l vs) as "Hl".
+    wp_apply (lreverse_spec with "Hl").
+    iIntros "Hl".
+    wp_send with "[$Hl]".
+    iApply ("HΦ" with "Hc").
+  Qed.
+
+  Lemma llist_split {T} (IT : T → val → iProp Σ) xs l :
+    ⊢ llist IT l xs ∗-∗
+      ∃ (vs : list val), llist internal_eq l vs ∗ [∗ list] x;v ∈ xs;vs, IT x v.
+  Proof.
+    iSplit.
+    - iIntros "Hl".
+      iInduction xs as [|x xs] "IH" forall (l).
+      + iExists []. eauto.
+      + iDestruct "Hl" as (v lcons) "[HIT [Hlcons Hrec]]".
+        iDestruct ("IH" with "Hrec") as (vs) "[Hvs H]".
+        iExists (v::vs). iFrame.
+        iExists v, lcons. eauto with iFrame.
+    - iDestruct 1 as (vs) "[Hvs HIT]".
+      iInduction xs as [|x xs] "IH" forall (l vs).
+      + by iDestruct (big_sepL2_nil_inv_l with "HIT") as %->.
+      + iDestruct (big_sepL2_cons_inv_l with "HIT") as (v vs' ->) "[HIT HITs]".
+        iDestruct "Hvs" as (w lcons Heq) "[Hl Hvs]".
+        iExists w, lcons.
+        iFrame.
+        iSplitL "HIT".
+        { by iEval (rewrite -Heq). }
+        iApply ("IH" with "Hvs HITs").
+  Qed.
+
+  Definition list_rev_protI {T} (IT : T → val → iProp Σ) : iProto Σ :=
+    (<! (l : loc) (xs : list T)> MSG #l {{ llist IT l xs }} ;
+     <?> MSG #() {{ llist IT l (reverse xs) }} ; END)%proto.
+
+  Lemma list_rev_subprot {T} (IT : T → val → iProp Σ) :
+    ⊢ list_rev_prot ⊑ (list_rev_protI IT).
+  Proof.
+    iIntros (l xs) "Hl".
+    iDestruct (llist_split with "Hl") as (vs) "[Hl HI]".
+    iExists l, vs. iFrame "Hl".
+    iModIntro.
+    iIntros "Hl".
+    iSplitL.
+    { rewrite big_sepL2_reverse_2.
+      iApply llist_split. iExists (reverse vs). iFrame. }
+    eauto.
+  Qed.
+
+  Lemma list_rev_client_spec {T} (IT : T → val → iProp Σ) l xs :
+    {{{ llist IT l xs }}}
+      list_rev_client #l
+    {{{ RET #(); llist IT l (reverse xs) }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_lam.
+    wp_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
+    - rewrite -(iProto_app_end_r list_rev_prot).
+      iApply (list_rev_service_spec with "Hc"). eauto.
+    - iDestruct (iProto_mapsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
+      { iApply list_rev_subprot. }
+      wp_send (l xs) with "[$Hl]".
+      wp_recv as "Hl".
+      by iApply "HΦ".
+  Qed.
+
+End list_rev_example.

theories/utils/llist.v

@@ -75,6 +75,17 @@ Definition lsplit_at : val :=
 
 Definition lsplit : val := λ: "l", lsplit_at "l" (llength "l" `quot` #2).
 
+Definition lreverse_at : val :=
+  rec: "go" "l" "acc" :=
+    match: !"l" with
+      NONE => "acc"
+    | SOME "p" => (lcons (Fst "p") "acc");; "go" (Snd "p") "acc"
+    end.
+
+Definition lreverse : val :=
+  λ: "l", let: "l'" := ref (!"l") in
+          "l" <- !(lreverse_at "l'" (lnil #())).
+
 Section lists.
 Context `{heapG Σ} {A} (I : A → val → iProp Σ).
 Implicit Types i : nat.
@@ -246,4 +257,54 @@ Proof.
   wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
   iApply "HΦ". iFrame. by rewrite take_drop.
 Qed.
+
+Lemma lreverse_at_spec l xs acc ys :
+  {{{ llist I l xs ∗ llist I acc ys }}}
+    lreverse_at #l #acc
+  {{{ l', RET #l'; llist I l' (reverse xs ++ ys) }}}.
+Proof.
+  iIntros (Φ) "[Hl Hacc] HΦ".
+  iInduction xs as [|x xs] "IH" forall (l acc Φ ys).
+  - wp_lam. wp_pures.
+    wp_load. wp_pures. iApply "HΦ". rewrite app_nil_l. iApply "Hacc".
+  - wp_lam. wp_pures. simpl.
+    iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
+    wp_load. wp_pures. wp_apply (lcons_spec with "[$Hacc $HI]").
+    iIntros "Hacc". wp_pures.
+    iApply ("IH" with "Hl' Hacc").
+    iIntros "!>" (l'') "Hl''".
+    iApply "HΦ". rewrite reverse_cons -app_assoc. iApply "Hl''".
+Qed.
+
+Lemma lreverse_spec l xs :
+  {{{ llist I l xs }}}
+    lreverse #l
+  {{{ RET #(); llist I l (reverse xs) }}}.
+Proof.
+  iIntros (Φ) "Hl HΦ". wp_lam.
+  destruct xs.
+  - wp_load. wp_alloc l' as "Hl'".
+    wp_apply (lnil_spec)=> //.
+    iIntros (lnil) "Hlnil".
+    iAssert (llist I l' []) with "Hl'" as "Hl'".
+    wp_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
+    iIntros (l'') "Hl''".
+    wp_load. wp_store. iApply "HΦ". rewrite app_nil_r. iApply "Hl".
+  - iDestruct "Hl" as (v lcons) "[HI [Hlcons Hrec]]".
+    wp_load. wp_alloc l' as "Hl'".
+    wp_apply (lnil_spec)=> //.
+    iIntros (lnil) "Hlnil".
+    wp_apply (lreverse_at_spec _ (a::xs) with "[Hl' HI Hrec Hlnil]").
+    { iFrame "Hlnil". iExists v, lcons. iFrame. }
+    iIntros (l'') "Hl''".
+    assert (∃ ys, ys = reverse (a :: xs)) as [ys Hys].
+    { by exists (reverse (a :: xs)). }
+    rewrite -Hys. destruct ys.
+    + wp_load. wp_store. by iApply "HΦ".
+    + simpl. iDestruct "Hl''" as (v' lcons') "[HI [Hcons Hrec]]".
+      wp_load. wp_store.
+      iApply "HΦ". rewrite app_nil_r.
+      eauto with iFrame.
+Qed.
+
 End lists.