From cf424f14d1f59ce62a1f8e72fd0dbae9ab2b8387 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Sat, 12 Oct 2019 12:39:12 -0400
Subject: [PATCH] Updated documentation of proofmode

---
 theories/channel/proofmode.v     | 38 +++++++++++++++++++++++++-------
 theories/channel/proto_channel.v |  2 +-
 2 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 969b503..95f5645 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,11 +1,33 @@
-(** This file contains tactics for the message-passing
-connectives, as well as the necessary typeclasses.
-
-This includes a way of reducing protocols to a normal
-form, to prepare them for use in the appropriate
-specifications. This normalisation includes e.g.
-resolving duals.
- *)
+(** This file contains tactics for the message-passing connectives,
+as well as the necessary typeclasses.
+This includes a way of reducing protocols to a normal form, to prepare
+them for use in the appropriate specifications.
+This normalisation includes e.g. resolving duals.
+
+The tactics are:
+- [wp_send (x1 .. xn) with "selpat"] which resolves weakest preconditions of the
+form [wp (send c v) Q], in the presence of an ownership of a send protocol
+[c ↣  <!> x .. y, MSG v; {{ P }}; prot] in the context. That is done by using
+[x1 .. xn] to existentially quantify the variables [x .. y], and "ipat" to
+resolve the predicate [P]. The result is continuing as [Q],
+with [c ↣  prot] in the context.
+
+- [wp_recv (x1 .. xn) as "ipat"] which conversely resolves [wp (recv c) Q] with
+[c ↣  <?> x .. y, MSG v; {{ P }}; prot] in the context, where the variables
+[x .. y] are introduced as [x1 .. xn], and the predicate [P] is introduces based
+on the pattern [ipat].
+
+- [wp_select with "selpat"] which resolves [wp (select c b) Q] with
+[c ↣  prot1 {Q1}<+>{Q2} prot2] in the context. Here [selpat] is used to
+resolve either [Q1] or [Q2], based on the chosen branch. The resulting
+protocol is similarly [c ↣  prot1] or [c ↣  prot2] based on the chosen
+branch.
+
+- [wp_branch as ipat1 | ipat2] which resolves [wp (branch c e1 e2) Q] with
+[c ↣  prot1 {Q1}<&>{Q2} prot2] in the context. The result is two subgoals,
+in which [Q1] and [Q2] are introduced using [ipat1] and [ipat2], and the
+protocol ownership is [c ↣  prot1] and [c ↣  prot2] respectively. *)
+
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
 From actris Require Export proto_channel.
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index c3d796e..b92b47c 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -32,7 +32,7 @@ in terms of sending and receiving boolean flags:
 Q1 or Q2, based on the sent or received flag.
 
 The logical connective of protocol ownership are then defined:
-- [c >-> prot] which describes that channel endpoint [c] adheres
+- [c ↣  prot] which describes that channel endpoint [c] adheres
 to protocol [prot], achieved through Iris invariants and ghost state along
 with the logical connectives of the channel encodings [is_chan] and [chan_own]. 
 
-- 
GitLab