Misc changes

multi_actris/channel/channel.v

-(** This file contains the definition of the channels, encoded as a pair of
-lock-protected buffers, and their primitive proof rules. Moreover:
+(** This file contains the definition of the channels,
+and their primitive proof rules. Moreover:
 
 - It defines the connective [c ↣ prot] for ownership of channel endpoints,
   which describes that channel endpoint [c] adheres to protocol [prot].
-- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
-  separation protocols.
-
-An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
-and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
-this file.
+- It proves Actris's specifications of [send] and [recv] w.r.t.
+  multiparty dependent separation protocols.
 
 In this file we define the three message-passing connectives:
 
-- [new_chan] creates references to two empty buffers and a lock, and returns a
-  pair of endpoints, where the order of the two references determines the
-  polarity of the endpoints.
-- [send] takes an endpoint and adds an element to the first buffer.
-- [recv] performs a busy loop until there is something in the second buffer,
-  which it pops and returns, locking during each peek.
+- [new_chan] creates an n*n matrix of references where [i,j] is the singleton
+  buffer from participant i to participant j
+- [send] takes an endpoint, a participant id, and a value, and puts the value in 
+  the reference corresponding to the participant id, and waits until recv takes
+  it out.
+- [recv] takes an endpoint, and a participant id, and waits until a value is put
+  into the corresponding reference.
 
 It is additionaly shown that the channel ownership [c ↣ prot] is closed under
 the subprotocol relation [⊑] *)
@@ -50,7 +47,6 @@ Definition send : val :=
     let: "l" := matrix_get "m" "i" "j" in
     "l" <- SOME "v";; wait "l".
 
-(* TODO: Move recursion further in *)
 Definition recv : val :=
   rec: "go" "c" "j" :=
     let: "m" := Fst "c" in
@@ -185,23 +181,15 @@ Section channel.
                      (λ i j l, ∃ γt,
             inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
                                        l))%I); [done..| |].
-    { iApply (big_sepL_intro).
-      iIntros "!>" (k tt Hin).
-      iApply (big_sepL_intro).
-      iIntros "!>" (k' tt' Hin').
-      iIntros (l) "Hl".
+    { iApply (big_sepL_intro). iIntros "!>" (k tt Hin). iApply (big_sepL_intro).
+      iIntros "!>" (k' tt' Hin'). iIntros (l) "Hl".
       iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
-      iExists γ'.
-      iApply inv_alloc.
-      iNext.
-      iLeft. iFrame. }
-    iIntros (mat) "Hmat".
-    iApply "HΦ".
+      iExists γ'. iApply inv_alloc. iNext. iLeft. iFrame. }
+    iIntros (mat) "Hmat". iApply "HΦ".
     iExists _, _, _. iFrame "#∗".
     rewrite left_id. iSplit; [done|].
     iApply (big_sepL_impl with "H").
-    iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
-    iFrame.
+    iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)". iFrame.
     rewrite (list_lookup_total_alt ps).
     simpl. rewrite right_id_L. rewrite HSome'. iFrame.
   Qed.

multi_actris/channel/proofmode.v

@@ -338,7 +338,6 @@ Proof.
   iNext. iRewrite -"Hp1". done.
 Qed.
 
-(* TODO: Improve automation *)
 Tactic Notation "iProto_consistent_take_step_step" :=
   let i := fresh in
   let j := fresh in

multi_actris/channel/proto.v

-(** This file defines the core of the Actris logic: It defines dependent
-separation protocols and the various operations on it like dual, append, and
-branching.
-
-Dependent separation protocols [iProto] are defined by instantiating the
-parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
-We define ways of constructing instances of the instantiated type via two
-constructors:
-- [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
-  sequence of binders [iMsg_exist], terminated by the payload constructed with
-  [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
-  carried proposition and the [iProto] tail, respectively.
-
-For convenience sake, we provide the following notations:
-- [END], which is simply [iProto_end].
-- [∃ x, m], which is [iMsg_exist] with argument [m].
-- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
-- [<a> m], which is [iProto_message] with arguments [a] and [m].
-
-We also include custom notation to more easily construct complete constructions:
-- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
-- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
-
-Futhermore, we define the following operations:
-- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
-- [iProto_app], which appends two protocols.
-
-In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
-the following inductive definition for asynchronous subtyping on session types:
-
-                 p1 <: p2           p1 <: p2          p1 <: !B.p3    ?A.p3 <: p2
-----------   ----------------   ----------------     ----------------------------
-end <: end    !A.p1 <: !A.p2     ?A.p1 <: ?A.p2             ?A.p1 <: !B.p2
-
-Example:
-
-!R <: !R  ?Q <: ?Q      ?Q <: ?Q
--------------------  --------------
-?Q.!R <: !R.?Q       ?P.?Q <: ?P.?Q
-------------------------------------
-   ?P.?Q.!R <: !R.?P.?Q
-
-Lastly, relevant type classes instances 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. *)
+(** This file defines the core of the Multiparty Actris logic:
+It defines multiparty dependent separation protocols, and the Multiparty Actris
+ghost theory. *)
 From iris.algebra Require Import gmap excl_auth gmap_view.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export lib.iprop.

multi_actris/channel/proto_model.v

@@ -12,8 +12,9 @@ recursive domain equation:
 
 Here, the left-hand side of the sum is used for the terminated process, while
 the right-hand side is used for the communication constructors. The type
-[action] is an inductively defined datatype with two constructors [Send] and
-[Recv]. Compared to having an additional sum in [proto], this makes it
+[action] is a pair of a an inductively defined datatype [tag] with two
+constructors [Send] and [Recv], and a synchronosation id of [nat].
+Compared to having an additional sum in [proto], this makes it
 possible to factorize the code in a better way.
 
 The remainder [V → ▶ proto → PROP] is a predicate that ranges over the

multi_actris/examples/basics.v

@@ -37,7 +37,6 @@ Section channel.
     ⊢ iProto_consistent iProto_roundtrip.
   Proof. rewrite /iProto_roundtrip. iProto_consistent_take_steps. Qed.
 
-  (* TODO: Fix nat/Z coercion. *)
   Lemma roundtrip_prog_spec :
     {{{ True }}} roundtrip_prog #() {{{ RET #42 ; True }}}.
   Proof using chanG0 heapGS0 Σ.
@@ -320,7 +319,6 @@ Section forwarder.
      (<(Recv, 1) @ (x:Z)> MSG #x ;
             <(Send, 0)> MSG #x ; END)%proto].
 
-  (* TODO: Anonymous variable in this is unsatisfactory *)
   Lemma iProto_forwarder_consistent :
     ⊢ iProto_consistent iProto_forwarder.
   Proof.

multi_actris/examples/leader_election_del.v

@@ -179,7 +179,6 @@ Section ring_leader_election_example.
     (relay_recv_aux i (relay_recv_prot i)).
   Proof. apply (fixpoint_unfold (relay_recv_aux i)). Qed.
 
-
   Definition prot_pool : list (iProto Σ) :=
      [rle_preprot 3 0 1 (λ id_max, forward_prot (relay_send_prot id_max) 3 0 1 id_max);
       rle_prot 0 1 2 (λ id_max, forward_prot (relay_send_prot id_max) 0 1 2 id_max) false;

multi_actris/utils/matrix.v

@@ -24,7 +24,6 @@ Section with_Σ.
         [∗ list] j ↦ _ ∈ replicate n (),
           P i j (l +ₗ pos n i j).
 
-
   Lemma array_to_matrix_pre l n m v :
     l ↦∗ replicate (n * m) v -∗
     [∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
@@ -42,7 +41,6 @@ Section with_Σ.
     by iFrame.
   Qed.
 
-  (* TODO: rename *)
   Lemma big_sepL_replicate_type {A B} n (x1 : A) (x2 : B) (P : nat → iProp Σ) :
     ([∗ list] i ↦ _ ∈ replicate n x1, P i) ⊢
     ([∗ list] i ↦ _ ∈ replicate n x2, P i).
@@ -117,7 +115,6 @@ Section with_Σ.
     { iIntros "!>" (k x HIn).
       iApply (big_sepL_lookup_acc _ _ j ()).
       by apply lookup_replicate. }
-    simpl.
     rewrite {1}(big_sepL_lookup_acc _ (replicate m ()) i ());
       [|by apply lookup_replicate].
     iDestruct "Hm" as "[[Hij Hi] Hm]".