From 56a4744fef587e7f4a296c4f3eb6c36904efe1c0 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Thu, 10 Oct 2019 21:28:34 -0400
Subject: [PATCH] Added descriptive headers to all files

---
 theories/channel/channel.v       | 49 +++++++++++++++++++++++---------
 theories/channel/proofmode.v     |  8 ++++++
 theories/channel/proto_channel.v | 19 +++++++++++++
 theories/channel/proto_model.v   | 20 +++++++++++++
 theories/examples/basics.v       | 11 +++++++
 theories/examples/map.v          |  2 ++
 theories/examples/map_reduce.v   |  2 ++
 theories/examples/sort.v         |  2 ++
 theories/examples/sort_br_del.v  |  2 ++
 theories/examples/sort_fg.v      |  2 ++
 theories/utils/auth_excl.v       |  2 ++
 theories/utils/compare.v         |  4 +++
 theories/utils/contribution.v    | 12 ++++++++
 theories/utils/group.v           |  2 ++
 theories/utils/llist.v           |  2 ++
 15 files changed, 126 insertions(+), 13 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index fdca205..7cd0f22 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,3 +1,21 @@
+(** This file contains the definition of the Channel language encoding,
+being a pair of buffers, with the three message-passing primitives
+[new_chan], [send] and [receive], along with their respective specifications.
+
+The abstract representation of a channel endpoint is two buffer references
+and a lock. [new_chan] creates references to two empty buffers and a lock, and
+returns a pair of such endpoints, where the order of the two references
+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.
+
+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.
+*)
+
 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.
@@ -9,6 +27,7 @@ Instance side_inhabited : Inhabited side := populate Left.
 Definition side_elim {A} (s : side) (l r : A) : A :=
   match s with Left => l | Right => r end.
 
+(** Message-Passing Primitives *)
 Definition new_chan : val :=
   λ: <>,
      let: "l" := lnil #() in
@@ -39,6 +58,7 @@ Definition recv : val :=
     | NONE => "go" "c"
     end.
 
+(** Channel ghost functor *)
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
   chanG_authG :> auth_exclG (listO valO) Σ;
@@ -65,6 +85,7 @@ Section channel.
     chan_r_name : gname
   }.
 
+  (** The invariant of channels *)
   Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
     (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
@@ -79,6 +100,18 @@ Section channel.
   Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
   Proof. by apply _. Qed.
 
+  Lemma chan_inv_alt s γ l r :
+    chan_inv γ l r ⊣⊢ ∃ ls rs,
+      llist sbi_internal_eq (side_elim s l r) ls ∗
+      own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
+      llist sbi_internal_eq (side_elim s r l) rs ∗
+      own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
+  Proof.
+    destruct s; rewrite /chan_inv //=.
+    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
+  Qed.
+
+  (** The ownership of channels *)
   Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
     own (side_elim s chan_l_name chan_r_name γ) (◯ to_auth_excl vs)%I.
 
@@ -94,9 +127,9 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
     { by apply auth_both_valid. }
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    iMod (own_alloc (● (to_auth_excl [])  ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
     { by apply auth_both_valid. }
     wp_apply (newlock_spec N (∃ ls rs,
       llist sbi_internal_eq l ls ∗ own lsγ (● to_auth_excl ls) ∗
@@ -107,17 +140,6 @@ Section channel.
     rewrite /chan_inv /=. eauto 20 with iFrame.
   Qed.
 
-  Lemma chan_inv_alt s γ l r :
-    chan_inv γ l r ⊣⊢ ∃ ls rs,
-      llist sbi_internal_eq (side_elim s l r) ls ∗
-      own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
-      llist sbi_internal_eq (side_elim s r l) rs ∗
-      own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
-  Proof.
-    destruct s; rewrite /chan_inv //=.
-    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
-  Qed.
-
   Lemma send_spec Φ E γ c1 c2 v s :
     is_chan γ c1 c2 -∗
     (|={⊤,E}=> ∃ vs,
@@ -194,4 +216,5 @@ Section channel.
       iIntros "!> !>" (v vs' ->) "Hvs".
       iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
   Qed.
+
 End channel.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index ea2a2e8..969b503 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,3 +1,11 @@
+(** 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.
+ *)
 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 5a02c3c..0d90334 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,3 +1,22 @@
+(** This file contains the instantiation of the
+Dependent Separation Protocols with the encoded messages.
+For starters this means fixing the types of message to the
+language value type [val] and the logic to the iris logic [iProp Σ].
+
+It then defines a convenient way of constructing instances of the type
+via [iProto_end] and [iProto_message] with associated notation,
+as well as type-specific variants of [dual] and [append].
+An encoding of branching behaviour is additionally included, defined
+in terms of sending and receiving boolean flags, along with relevant notation.
+
+The logical connectives of protocol ownership [c >-> prot] are then defined.
+This is achieved through Iris invariants and ghost state along with the
+logical connectives of the channel encodings. 
+
+Lastly, relevant typeclasses are defined for each of the above notions,
+such as contractiveness and non-expansiveness, after which the specifications
+of the message-passing primitives are defined in terms of the protocol connectives.
+*)
 From actris.channel Require Export channel.
 From actris.channel Require Import proto_model.
 From iris.base_logic.lib Require Import invariants.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 41af2de..c9600aa 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -1,3 +1,23 @@
+(** This file defines the model of Dependent Separation Protocols,
+along with various operations on the connective, such as append
+and map.
+
+Dependent Separation Protocols can ultimately be expressed as:
+proto := 1 + (B * (V -> (â–¶ proto -> PROP) -> PROP))
+
+Here the left-hand side of the sum is the terminal protocol
+[proto_end], while the right-hand side is [proto_message],
+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.
+
+The type is defined as a solution to a recursive domain
+equation, as it is self-referential under the guard of â–¶.
+*)
+
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import cofe_solver.
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index b1f8784..1088d62 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -1,15 +1,21 @@
+(** This file includes basic examples that each
+encapsulate a feature of the Dependent Separation Protocols.
+*)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
 From actris.utils Require Import contribution.
 
+(** Basic *)
 Definition prog1 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
+(** References *)
 Definition prog2 : val := λ: <>,
   let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
+(** Delegation *)
 Definition prog3 : val := λ: <>,
   let: "c1" := start_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
@@ -17,12 +23,14 @@ Definition prog3 : val := λ: <>,
     send (Snd "cc2") #42) in
   recv (recv "c1").
 
+(** Dependent Behaviour *)
 Definition prog4 : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "x" := recv "c'" in send "c'" ("x" + #2)) in
   send "c" #40;;
   recv "c".
 
+(** Higher-Order *)
 Definition prog5 : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
@@ -30,6 +38,7 @@ Definition prog5 : val := λ: <>,
   send "c" (λ: <>, !"r");;
   recv "c" #().
 
+(** Locks *)
 Definition prog_lock : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     let: "l" := newlock #() in
@@ -40,6 +49,7 @@ Definition prog_lock : val := λ: <>,
 Section proofs.
 Context `{heapG Σ, proto_chanG Σ}.
 
+(** Protocols for their respective programs *)
 Definition prot1 : iProto Σ :=
   (<?> MSG #42; END)%proto.
 
@@ -65,6 +75,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
   | S n' => <?> MSG #21; prot_lock n'
   end%proto.
 
+(** Specs and proofs of their respective programs *)
 Lemma prog1_spec : {{{ True }}} prog1 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 5cafc7f..7a44671 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,3 +1,5 @@
+(** This file implements a distributed map service,
+a specification thereof and its proofs. *)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
 From actris.utils Require Import llist contribution.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 903a017..a14aa34 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,3 +1,5 @@
+(** This file implements a map-reduce program,
+a specification thereof and its proofs. *)
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From actris.utils Require Import llist compare contribution group.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 5860079..c096a66 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,3 +1,5 @@
+(** This file implements a distributed Merge Sort,
+a specification thereof and its proofs. *)
 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index 296e1b4..68670d7 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -1,3 +1,5 @@
+(** This file implements a looping distributed Merge Sort,
+a specification thereof and its proofs. *)
 From stdpp Require Import sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index bc5edc7..410f929 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -1,3 +1,5 @@
+(** This file implements a fine-grained Merge Sort,
+a specification thereof and its proofs. *)
 From stdpp Require Export sorting.
 From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/utils/auth_excl.v b/theories/utils/auth_excl.v
index f9a5871..952adad 100644
--- a/theories/utils/auth_excl.v
+++ b/theories/utils/auth_excl.v
@@ -1,3 +1,5 @@
+(** This file provides utility for defining and using
+the commonly used ghost functor over authoritative exclusive ownership. *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import own.
diff --git a/theories/utils/compare.v b/theories/utils/compare.v
index 422bf77..dc19a1d 100644
--- a/theories/utils/compare.v
+++ b/theories/utils/compare.v
@@ -1,3 +1,7 @@
+(** This file includes a definition and specification
+for comparing values based on a given interpretation [I]
+and a relation [R], along with an implementation in the [heap_lang]
+language, given the [≤] relation.*)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index c221ed5..15cb3ef 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -1,3 +1,15 @@
+(** This file defines a ghost functor for tracking
+"contributions" made to a shared concurrent effort.
+It is ultimately defined as:
+contribution := Auth (Option ((Pos * A) + Excl 1))
+
+Intuitively it allows one to allocate a [server] and
+a number of [client] fragments. The server keeps track
+of the number of active clients, and what resources they
+are currently holding.
+To deallocate a client it must hold no resources.
+To deallocate a server there must be no remaining clients.
+*)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
 From iris.proofmode Require Export tactics.
 From iris.algebra Require Import excl auth csum gmultiset frac_auth.
diff --git a/theories/utils/group.v b/theories/utils/group.v
index 90c86fa..9b3b0b0 100644
--- a/theories/utils/group.v
+++ b/theories/utils/group.v
@@ -1,3 +1,5 @@
+(** This file provides utility for grouping elements
+based on keys. *)
 From stdpp Require Export prelude.
 From Coq Require Export SetoidPermutation.
 
diff --git a/theories/utils/llist.v b/theories/utils/llist.v
index a948859..d710ab0 100644
--- a/theories/utils/llist.v
+++ b/theories/utils/llist.v
@@ -1,3 +1,5 @@
+(** This file defines an encoding of lists in the [heap_lang]
+language, along with common functions such as append and split. *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
 
-- 
GitLab