Some updates to comments

theories/channel/channel.v

@@ -9,13 +9,14 @@ determines the polarity of the endpoints.
 
 The [send] primitive takes such an endpoint abstraction and adds an element to
 the first buffer under the lock. Conversely [recv] loops until there is
-something in the second, locking during each peek.
+something in the second buffer, which it pops and returns, locking during
+each peek.
 
 The specifications are defined in terms of the logical connectives [is_chan]
-and [chan_own], which respectively determines the contents of a channel and
-the ownership of it.
+and [chan_own], which respectively determines the contents of a channel using
+a lock over an invariant and the ownership of it using ghost fragments
+over buffers.
 *)
-
 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.

theories/channel/proto_model.v

 (** This file defines the model of Dependent Separation Protocols,
 along with various operations on the connective, such as append
-and map.
+and map and the necessary typeclass instances.
 
 Dependent Separation Protocols can ultimately be expressed as:
 proto := 1 + (B * (V -> (▶ proto -> PROP) -> PROP))
@@ -10,9 +10,9 @@ Here the left-hand side of the sum is the terminal protocol
 where B is the canonical representation of actions determining
 whether the protocol sends or receives, and
 (V -> (▶ proto -> PROP) -> PROP) is a continuation that
-depends on a communicated value V and the dependent tail
-(▶ proto -> PROP) from protocols guarded under laters,
- to the propositions of the logic.
+depends on the communicated value V and the dependent tail
+(▶ proto -> PROP) from protocols guarded under laters to the
+propositions of the logic.
 
 The type is defined as a solution to a recursive domain
 equation, as it is self-referential under the guard of ▶.

theories/examples/sort.v

 (** This file implements a distributed Merge Sort,
-a specification thereof and its proofs. *)
+a specification thereof and its proofs, including
+a variant in which the comparison function is sent
+over the channel. *)
 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.