From 445adad8307e86c26fc5164b53369ce8d8b02d26 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Thu, 11 Jul 2019 10:59:34 +0200
Subject: [PATCH] Combined sort_fg_client and sort_fg

---
 _CoqProject                        |  1 -
 theories/examples/sort_fg.v        | 72 ++++++++++++++++++++++++++-
 theories/examples/sort_fg_client.v | 78 ------------------------------
 3 files changed, 70 insertions(+), 81 deletions(-)
 delete mode 100644 theories/examples/sort_fg_client.v

diff --git a/_CoqProject b/_CoqProject
index 2149c15..c843c5a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -12,7 +12,6 @@ theories/channel/proofmode.v
 theories/examples/sort.v
 theories/examples/loop_sort.v
 theories/examples/sort_fg.v
-theories/examples/sort_fg_client.v
 theories/examples/map.v
 theories/examples/map_reduce.v
 theories/examples/basics.v
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 50d5bdd..bc5edc7 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -2,7 +2,7 @@ From stdpp Require Export 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 compare.
+From actris.utils Require Import llist compare.
 
 Definition cont := true.
 Definition stop := false.
@@ -51,6 +51,23 @@ Definition sort_service_fg_func : val := λ: "c",
   let: "cmp" := recv "c" in
   sort_service_fg "cmp" "c".
 
+Definition send_all : val :=
+  rec: "go" "c" "xs" :=
+    if: lisnil "xs" then #() else
+    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
+
+Definition recv_all : val :=
+  rec: "go" "c" "ys" :=
+    if: ~recv "c" then #() else
+    let: "x" := recv "c" in
+    "go" "c" "ys";; lcons "x" "ys".
+
+Definition sort_client_fg : val := λ: "cmp" "xs",
+  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
+  send_all "c" "xs";;
+  send "c" #stop;;
+  recv_all "c" "xs".
+
 Section sort_fg.
   Context `{!heapG Σ, !proto_chanG Σ}.
 
@@ -220,6 +237,57 @@ Section sort_fg.
         wp_select. by iApply "HΨ".
     - wp_select. by iApply "HΨ".
   Qed.
+  
+  Lemma send_all_spec c p xs' l xs :
+    {{{ llist I l xs ∗ c ↣ (sort_fg_head_protocol xs' <++> p) }}}
+      send_all c #l
+    {{{ RET #(); llist I l [] ∗ c ↣ (sort_fg_head_protocol (xs' ++ xs) <++> p) }}}.
+  Proof.
+    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. }
+    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 l xs ys' :
+    Sorted R ys' →
+    {{{ llist I l [] ∗ c ↣ (sort_fg_tail_protocol xs ys' <++> p) }}}
+      recv_all c #l
+    {{{ ys, RET #();
+        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗ llist I l ys ∗ c ↣ p
+    }}}.
+  Proof.
+    iIntros (Hsort Φ) "[Hl Hc] HΦ".
+    iLöb as "IH" forall (xs ys' Φ Hsort).
+    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
+    - wp_recv (y v) as (Htl) "HIx".
+      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
+      iIntros (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.
+    - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
+  Qed.
+
+  Lemma sort_client_fg_spec cmp l xs :
+    cmp_spec I R cmp -∗
+    {{{ llist I l xs }}}
+      sort_client_fg cmp #l
+    {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
+  Proof.
+    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
+    wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto);
+      iIntros (c) "Hc".
+    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
+    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
+    wp_select.
+    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
+    iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
+    iApply "HΦ"; auto with iFrame.
+  Qed.
+  
   End sort_fg_inner.
 
   Definition sort_fg_func_protocol : iProto Σ :=
@@ -237,4 +305,4 @@ Section sort_fg.
     wp_recv (A I R ? ? cmp) as "#Hcmp".
     by wp_apply (sort_service_fg_spec with "Hcmp Hc").
   Qed.
-End sort_fg.
+End sort_fg.
\ No newline at end of file
diff --git a/theories/examples/sort_fg_client.v b/theories/examples/sort_fg_client.v
deleted file mode 100644
index 5eacc5d..0000000
--- a/theories/examples/sort_fg_client.v
+++ /dev/null
@@ -1,78 +0,0 @@
-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 llist compare.
-From actris.examples Require Export sort_fg.
-
-Definition send_all : val :=
-  rec: "go" "c" "xs" :=
-    if: lisnil "xs" then #() else
-    send "c" #cont;; send "c" (lpop "xs");; "go" "c" "xs".
-
-Definition recv_all : val :=
-  rec: "go" "c" "ys" :=
-    if: ~recv "c" then #() else
-    let: "x" := recv "c" in
-    "go" "c" "ys";; lcons "x" "ys".
-
-Definition sort_client_fg : val := λ: "cmp" "xs",
-  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
-  send_all "c" "xs";;
-  send "c" #stop;;
-  recv_all "c" "xs".
-
-Section sort_fg_client.
-  Context `{!heapG Σ, !proto_chanG Σ}.
-  Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
-
-  Lemma send_all_spec c p xs' l xs :
-    {{{ llist I l xs ∗ c ↣ (sort_fg_head_protocol I R xs' <++> p) }}}
-      send_all c #l
-    {{{ RET #(); llist I l [] ∗ c ↣ (sort_fg_head_protocol I R (xs' ++ xs) <++> p) }}}.
-  Proof.
-    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. }
-    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 l xs ys' :
-    Sorted R ys' →
-    {{{ llist I l [] ∗ c ↣ (sort_fg_tail_protocol I R xs ys' <++> p) }}}
-      recv_all c #l
-    {{{ ys, RET #();
-        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗ llist I l ys ∗ c ↣ p
-    }}}.
-  Proof.
-    iIntros (Hsort Φ) "[Hl Hc] HΦ".
-    iLöb as "IH" forall (xs ys' Φ Hsort).
-    wp_lam. wp_branch as %_ | %Hperm; wp_pures.
-    - wp_recv (y v) as (Htl) "HIx".
-      wp_apply ("IH" with "[] Hl Hc"); first by auto using Sorted_snoc.
-      iIntros (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.
-    - iApply ("HΦ" $! []); rewrite /= right_id_L; by iFrame.
-  Qed.
-
-  Lemma sort_client_fg_spec cmp l xs :
-    cmp_spec I R cmp -∗
-    {{{ llist I l xs }}}
-      sort_client_fg cmp #l
-    {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
-  Proof.
-    iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_apply (start_chan_proto_spec (sort_fg_protocol I R <++> END)%proto);
-      iIntros (c) "Hc".
-    { wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
-    wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
-    wp_select.
-    wp_apply (recv_all_spec with "[$Hl $Hc]"); auto.
-    iIntros (ys) "/=". iDestruct 1 as (??) "[Hk _]".
-    iApply "HΦ"; auto with iFrame.
-  Qed.
-End sort_fg_client.
-- 
GitLab