From cc5ddc6625286a06f08492ecb04a84f1545c86f9 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 7 Aug 2020 16:01:01 +0200
Subject: [PATCH] Aligned program with paper

---
 theories/examples/swap_mapper.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 4e5aee2..cfeecaa 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -27,7 +27,7 @@ Definition swap_mapper_client : val :=
   λ: "f" "xs",
     let: "c" := start_chan (λ: "c", swap_mapper_service "f" "c") in
     let: "n" := llength "xs" in
-    send_all "c" "xs";; send "c" #false;; recv_all "c" "xs" "n".
+    send_all "c" "xs";; recv_all "c" "xs" "n";; send "c" #false.
 
 Section with_Σ.
   Context `{heapG Σ, chanG Σ}.
@@ -380,12 +380,12 @@ Section with_Σ.
     wp_apply (llength_spec with "HIT"); iIntros "HIT".
     wp_apply (send_all_spec with "[$HIT Hc]").
     { iApply (iProto_mapsto_le with "Hc").
-      iApply subprot_n_swap_end. }
+      iApply subprot_n_swap. }
     iIntros "[HIT Hc]".
-    wp_send with "[//]".
     rewrite right_id rev_involutive.
     wp_apply (recv_all_spec with "[$HIT $Hc]").
     iIntros (ys) "(% & HIT & Hc)".
+    wp_select.
     iApply "HΦ".
     by iFrame.
   Qed.
-- 
GitLab