From 23d07cc3500840cc547504f17e6ae5c46ac7b7df Mon Sep 17 00:00:00 2001
From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com>
Date: Fri, 8 May 2020 13:15:41 +0100
Subject: [PATCH] add connection message count to command type

---
 specification/Simplex/Messaging/Protocol.idr  | 47 +++++++++----------
 specification/Simplex/Messaging/Scenarios.idr |  6 ++-
 2 files changed, 25 insertions(+), 28 deletions(-)

diff --git a/specification/Simplex/Messaging/Protocol.idr b/specification/Simplex/Messaging/Protocol.idr
index 844991048d..83b23c3ad2 100644
--- a/specification/Simplex/Messaging/Protocol.idr
+++ b/specification/Simplex/Messaging/Protocol.idr
@@ -197,8 +197,8 @@ prefix 6 ///, >>>
 
 data RBConnState : Type where
   (<==>) : (recipient : ConnectionState)
-        -> (broker    : ConnectionState)
-        -> {auto prf  : HasState Broker broker}
+        -> (broker    : (Nat, ConnectionState)) -- number of messages in connection
+        -> {auto prf  : (\(_, s) => HasState Broker s) broker}
         -> RBConnState
 
 data AllConnState : Type where
@@ -230,57 +230,52 @@ data Command : (ty : Type)
              -> {auto prf : HasState Sender s}
              -> Command BrkCreateConnRes
                   Recipient Broker
-                  (Null <==> Null <==| s)
-                  (>>> New <==> New  <==| s)
+                  (Null <==> (Z, Null) <==| s)
+                  (>>> New <==> (Z, New)  <==| s)
 
   Subscribe   : Command () Recipient Broker state (>>> state) -- to improve
 
   SendInvite  : Invitation
              -> {auto prf : HasState Broker s}
              -> Command () Recipient Sender
-                  (New <==> s <==| Null)
-                  (>>> Pending <==> s <==| New)
+                  (New <==> (n, s) <==| Null)
+                  (>>> Pending <==> (n, s) <==| New)
 
   ConfirmConn : (senderBrokerKey : Key)
              -> Command () Sender Broker
-                  (s <==> New <==| New)
-                  (>>> s <==> New <==| Confirmed)
+                  (s <==> (n, New) <==| New)
+                  (>>> s <==> (S n, New) <==| Confirmed)
 
   PushConfirm : {auto prf : HasState Sender s}
              -> Command () Broker Recipient
-                  (Pending <==> New <==| s)
-                  (>>> Confirmed <==> New <==| s)
+                  (Pending <==> (S n, New) <==| s)
+                  (>>> Confirmed <==> (n, New) <==| s)
 
   SecureConn  : (senderBrokerKey : Key)
              -> {auto prf : HasState Sender s}
              -> Command () Recipient Broker
-                  (Confirmed <==> New <==| s)
-                  (>>> Secured <==> Secured <==| s)
+                  (Confirmed <==> (n, New) <==| s)
+                  (>>> Secured <==> (n, Secured) <==| s)
 
   SendWelcome : {auto prf : HasState Broker bs}
              -> Command () Sender Broker
-                  (rs <==> bs <==| Confirmed)
-                  (>>> rs <==> bs <==| Secured)
+                  (rs <==> (n, Secured) <==| Confirmed)
+                  (>>> rs <==> (S n, Secured) <==| Secured)
 
   PushWelcome : {auto prf : HasState Sender s}
              -> Command () Broker Recipient
-                  (Secured <==> Secured <==| s)
-                  (>>> Secured <==> Secured <==| s)
+                  (Secured <==> (S n, Secured) <==| s)
+                  (>>> Secured <==> (n, Secured) <==| s)
 
   SendMsg     : Message
-             -> {auto prf : HasState Broker bs}
              -> Command () Sender Broker
-                  (rs <==> bs <==| Secured)
-                  (\state, x => case x of
-                                  OK _  => state
-                                  Err _ => state
-                                  Deny  => (rs <==> bs <==| Null))
+                  (rs <==> (n, Secured) <==| Secured)
+                  (>>> rs <==> (S n, Secured) <==| Secured)
 
-  PushMsg     : Message
-             -> {auto prf : HasState Sender s}
+  PushMsg     : {auto prf : HasState Sender s}
              -> Command () Broker Recipient
-                  (Secured <==> Secured <==| s)
-                  (/// Secured <==> Secured <==| s)
+                  (Secured <==> (S n, Secured) <==| s)
+                  (>>> Secured <==> (n, Secured) <==| s)
 
   Pure  : (res : Result a) -> Command a from to state state_fn
   (>>=) : Command a from1 to1 state1 state2_fn
diff --git a/specification/Simplex/Messaging/Scenarios.idr b/specification/Simplex/Messaging/Scenarios.idr
index eb8282e4ce..9d7190369e 100644
--- a/specification/Simplex/Messaging/Scenarios.idr
+++ b/specification/Simplex/Messaging/Scenarios.idr
@@ -3,8 +3,8 @@ module Simplex.Messaging.Scenarios
 import Protocol
 
 establishConnection : Command () Recipient Recipient
-                        (Null <==> Null <==| Null)
-                        (>>> Secured <==> Secured <==| Secured)
+                        (Null <==> (Z, Null) <==| Null)
+                        (>>> Secured <==> (Z, Secured) <==| Secured)
 establishConnection = do
   ids <- CreateConn "recipient's public key for broker"
   Subscribe
@@ -14,3 +14,5 @@ establishConnection = do
   SecureConn "sender's public key for broker"
   SendWelcome
   PushWelcome
+  SendMsg "Hello"
+  PushMsg