dandri/simplex-chat
1
0
Fork 0
mirror of https://github.com/simplex-chat/simplex-chat.git synced 2026-03-30 05:40:00 +00:00
Code Issues Packages Projects Releases Wiki Activity

Different approach to commands (#34)

Browse Source 
* different approach to command types (WIP)

* PartyProtocol class and other commands

* pretty-print scenarion

* remove old files

* remove unused prf/predicate templates

* remove NoImplicitePrelude from doctest (although there are no doctests atm)
This commit is contained in:
Evgeny Poberezkin
2020-05-31 21:51:15 +01:00
committed by GitHub
parent dc7835992c
commit cc55bf3e6b
16 changed files with 525 additions and 976 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
definitions/src/Main.hs → definitions/app/api-docs/Main.hs
View File

@@ -2,7 +2,6 @@ module Main where
import Simplex.Messaging.ServerAPI
import ClassyPrelude
import Servant
import Servant.Docs
@@ -14,4 +13,4 @@ apiDocs = docsWith
(Proxy :: Proxy ServerAPI)
main :: IO ()
main = writeFile "../simplex-messaging-api.md" $ fromString $ markdown apiDocs
main = writeFile "../simplex-messaging-api.md" $ markdown apiDocs

7
definitions/app/print-scenarios/Main.hs Normal file
View File

@@ -0,0 +1,7 @@
module Main where
import Simplex.Messaging.PrintScenario
import Simplex.Messaging.Scenarios
main :: IO ()
main = printScenario establishConnection

51
definitions/package.yaml
View File

@@ -1,14 +1,14 @@
name: simplex-definitions
version: 0.1.0.0
name: simplex-definitions
version: 0.1.0.0
#synopsis:
#description:
homepage: https://github.com/simplex-chat/protocol/blob/master/definitions/readme.md
license: AGPL-3
author: Evgeny Poberezkin
copyright: 2020 Evgeny Poberezkin
category: Web
homepage: https://github.com/simplex-chat/protocol/blob/master/definitions/readme.md
license: AGPL-3
author: Evgeny Poberezkin
copyright: 2020 Evgeny Poberezkin
category: Web
extra-source-files:
- readme.md
- readme.md
ghc-options:
- -Wall
@@ -18,39 +18,42 @@ ghc-options:
- -Wincomplete-record-updates
- -Wincomplete-uni-patterns
default-extensions:
- BlockArguments
- DuplicateRecordFields
- LambdaCase
- NamedFieldPuns
- NoImplicitPrelude
- OverloadedStrings
- RecordWildCards
# default-extensions:
# - BlockArguments
# - DuplicateRecordFields
# - LambdaCase
# - NamedFieldPuns
# - NoImplicitPrelude
# - OverloadedStrings
# - RecordWildCards
dependencies:
- aeson
- base >= 4.7 && < 5
- classy-prelude
- decidable
- lens
- mtl
- singletons
- servant-docs
- servant-server
- template-haskell
# - pretty-show
library:
source-dirs: src
exposed-modules:
- Predicate
- Simplex.Messaging.Types
- Simplex.Messaging.ServerAPI
executables:
api-docs:
source-dirs: src
main: Main.hs
source-dirs: app/api-docs
main: Main.hs
ghc-options: -threaded
dependencies: simplex-definitions
print-scenarios:
source-dirs: app/print-scenarios
main: Main.hs
ghc-options: -threaded
dependencies: simplex-definitions
tests:
simplex-definitions-doctests:

58
definitions/src/Predicate.hs
View File

@@ -1,58 +0,0 @@
{-# LANGUAGE TemplateHaskell #-}
module Predicate where
import ClassyPrelude
import Data.Type.Predicate
import Data.Type.Predicate.Auto
import Language.Haskell.TH
-- This template adds instances of Auto typeclass (from decidable package)
-- to a given parametrised type definition
--
-- Given type definitions:
--
-- data P = A | B | C
--
-- $(predicate [d|
-- data T (a :: P) where
-- TA :: T 'A
-- TB :: T 'B
-- |])
--
-- `predicate` splice will add these instances:
--
-- instance Auto (TyPred T) 'A where auto = TA -- autoTC could have been used here too
-- instance Auto (TyPred T) 'B where auto = TB
--
-- to be used in type constraints
predicate :: Q [Dec] -> Q [Dec]
predicate decls = concat <$> (decls >>= mapM addInstances)
where
addInstances :: Dec -> Q [Dec]
addInstances d@(DataD _ _ _ _ constructors _) = do
ds <- mapM mkInstance constructors
if any null ds
then do
reportWarning $
"warning: not a parametrised GADT predicate (no instances added)\n"
++ pprint d
return [d]
else
return $ d : concat ds
addInstances d = do
reportWarning $ "warning: not a data type declaration\n" ++ pprint d
return [d]
mkInstance :: Con -> Q [Dec]
mkInstance (GadtC
[con] _
(AppT
(ConT ty)
(PromotedT p))) =
[d|
instance Auto (TyPred $(conT ty)) $(promotedT p) where
auto = $(conE con)
|]
mkInstance _ = return []

65
definitions/src/Simplex/Messaging/Broker.hs
View File

@@ -1,47 +1,32 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- {-# OPTIONS_GHC -ddump-splices #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Simplex.Messaging.Broker where
import ClassyPrelude
import Simplex.Messaging.Protocol
import Simplex.Messaging.Types
$(protocol Broker [d|
bcCreateConn = CreateConn <-- Recipient
bcSubscribe = Subscribe <-- Recipient
baPushConfirm = PushConfirm --> Recipient
baPushMsg = PushMsg --> Recipient
|])
instance Monad m => PartyProtocol m Broker where
api ::
Command from fs fs' Broker ps ps' res ->
Connection Broker ps ->
m (Either String (res, Connection Broker ps'))
api (CreateConn _) = apiStub
api (Subscribe _) = apiStub
api (Unsubscribe _) = apiStub
api (ConfirmConn _ _) = apiStub
api (SecureConn _ _) = apiStub
api (SendMsg _ _) = apiStub
api (DeleteMsg _ _) = apiStub
bcCreateConn :: Connection Broker None Idle
-> CreateConnRequest
-> Either String (CreateConnResponse, Connection Broker New Idle)
bcCreateConn = protoCmdStub
bcSubscribe :: Connection Broker s Idle
-> ()
-> Either String ((), Connection Broker s Subscribed)
bcSubscribe = protoCmdStub
baPushConfirm :: Connection Broker New Subscribed
-> SecureConnRequest
-> Either String ()
-> Either String (Connection Broker New Subscribed)
baPushConfirm = protoActionStub
baPushMsg :: Connection Broker Secured Subscribed
-> MessagesResponse -- TODO, has to be a single message
-> Either String ()
-> Either String (Connection Broker Secured Subscribed)
baPushMsg = protoActionStub
action ::
Command Broker ps ps' to ts ts' res ->
Connection Broker ps ->
Either String res ->
m (Either String (Connection Broker ps'))
action (PushConfirm _ _) = actionStub
action (PushMsg _ _) = actionStub

76
definitions/src/Simplex/Messaging/Client.hs
View File

@@ -1,48 +1,46 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- {-# OPTIONS_GHC -ddump-splices #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Simplex.Messaging.Client where
import ClassyPrelude
import Simplex.Messaging.Protocol
import Simplex.Messaging.Types
instance Monad m => PartyProtocol m Recipient where
api ::
Command from fs fs' Recipient ps ps' res ->
Connection Recipient ps ->
m (Either String (res, Connection Recipient ps'))
api (PushConfirm _ _) = apiStub
api (PushMsg _ _) = apiStub
$(protocol Recipient [d|
raCreateConn = CreateConn --> Broker
raSubscribe = Subscribe --> Broker
rcPushConfirm = PushConfirm <-- Broker
rcPushMsg = PushMsg <-- Broker
|])
action ::
Command Recipient ps ps' to ts ts' res ->
Connection Recipient ps ->
Either String res ->
m (Either String (Connection Recipient ps'))
action (CreateConn _) = actionStub
action (Subscribe _) = actionStub
action (Unsubscribe _) = actionStub
action (SendInvite _) = actionStub
action (SecureConn _ _) = actionStub
action (DeleteMsg _ _) = actionStub
instance Monad m => PartyProtocol m Sender where
api ::
Command from fs fs' Sender ps ps' res ->
Connection Sender ps ->
m (Either String (res, Connection Sender ps'))
api (SendInvite _) = apiStub
raCreateConn :: Connection Recipient None Idle
-> CreateConnRequest
-> Either String CreateConnResponse
-> Either String (Connection Recipient New Idle)
raCreateConn = protoActionStub
raSubscribe :: Connection Recipient s Idle
-> ()
-> Either String ()
-> Either String (Connection Recipient s Subscribed)
raSubscribe = protoActionStub
rcPushConfirm :: Connection Recipient Pending Subscribed
-> SecureConnRequest
-> Either String ((), Connection Recipient Confirmed Subscribed)
rcPushConfirm = protoCmdStub
rcPushMsg :: Connection Recipient Secured Subscribed
-> MessagesResponse -- TODO, has to be a single message
-> Either String ((), Connection Recipient Secured Subscribed)
rcPushMsg = protoCmdStub
action ::
Command Sender ps ps' to ts ts' res ->
Connection Sender ps ->
Either String res ->
m (Either String (Connection Sender ps'))
action (ConfirmConn _ _) = actionStub
action (SendMsg _ _) = actionStub

1
definitions/src/Simplex/Messaging/Connection.hs Normal file
View File

@@ -0,0 +1 @@
module Simplex.Messaging.Connection where

68
definitions/src/Simplex/Messaging/PrintScenario.hs Normal file
View File

@@ -0,0 +1,68 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
module Simplex.Messaging.PrintScenario where
import Control.Monad.Writer
import Data.Singletons
import Simplex.Messaging.Protocol
import Simplex.Messaging.Types
printScenario :: Protocol rs bs ss rs' bs' ss' a -> IO ()
printScenario scn = ps 1 "" $ execWriter $ logScenario scn
where
ps :: Int -> String -> [(String, String)] -> IO ()
ps _ _ [] = return ()
ps i p ((p', l) : ls)
| p' == "" = prt i $ "## " <> l <> "\n"
| p' /= p = prt (i + 1) $ show i <> ". " <> p' <> ":\n" <> l'
| otherwise = prt i l'
where
prt i' s = putStrLn s >> ps i' p' ls
l' = " - " <> l
logScenario :: Protocol rs bs ss rs' bs' ss' a -> Writer [(String, String)] a
logScenario (Start s) = tell [("", s)]
logScenario (p :>> c) = logScenario p >> logCommand c
logScenario (p :>>= f) = logScenario p >>= \x -> logCommand (f x)
logCommand :: PartiesCommand from fs fs' to ts ts' a -> Writer [(String, String)] a
logCommand ((:->) from to cmd) = do
tell [(party from, commandStr cmd <> " " <> party to)]
mockCommand cmd
commandStr :: Command from fs fs' to ts ts' a -> String
commandStr (CreateConn _) = "creates connection in"
commandStr (Subscribe cid) = "subscribes to connection " <> show cid <> " in"
commandStr (Unsubscribe cid) = "unsubscribes from connection " <> show cid <> " in"
commandStr (SendInvite _) = "sends out-of band invitation to "
commandStr (ConfirmConn cid _) = "confirms connection " <> show cid <> " in"
commandStr (PushConfirm cid _) = "pushes confirmation for " <> show cid <> " to"
commandStr (SecureConn cid _) = "secures connection " <> show cid <> " in"
commandStr (SendMsg cid _) = "sends message to connection " <> show cid <> " in"
commandStr (PushMsg cid _) = "pushes message from connection " <> show cid <> " to"
commandStr (DeleteMsg cid _) = "deletes message from connection " <> show cid <> " in"
mockCommand :: Monad m => Command from fs fs' to ts ts' a -> m a
mockCommand (CreateConn _) =
return
CreateConnResponse
{ recipientId = "Qxz93A",
senderId = "N9pA3g"
}
mockCommand (Subscribe _) = return ()
mockCommand (Unsubscribe _) = return ()
mockCommand (SendInvite _) = return ()
mockCommand (ConfirmConn _ _) = return ()
mockCommand (PushConfirm _ _) = return ()
mockCommand (SecureConn _ _) = return ()
mockCommand (SendMsg _ _) = return ()
mockCommand (PushMsg _ _) = return ()
mockCommand (DeleteMsg _ _) = return ()
party :: Sing (p :: Party) -> String
party SRecipient = "Alice (recipient)"
party SBroker = "Alice's server (broker)"
party SSender = "Bob (sender)"

566
definitions/src/Simplex/Messaging/Protocol.hs
View File

@@ -1,421 +1,199 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Simplex.Messaging.Protocol where
import ClassyPrelude
import Control.Monad.Fail
import Data.Kind
import Data.Singletons
import Data.Singletons.ShowSing
import Data.Singletons.TH
import Data.Type.Predicate
import Data.Type.Predicate.Auto
import GHC.TypeLits
import Language.Haskell.TH hiding (Type)
import qualified Language.Haskell.TH as TH
import Predicate
import Data.Type.Bool (type (||))
import Simplex.Messaging.Types
-- import Text.Show.Pretty (ppShow)
$(singletons [d|
data Participant = Recipient | Broker | Sender
deriving (Show, Eq)
$( singletons
[d|
data Party = Recipient | Broker | Sender
deriving (Show, Eq)
data ConnectionState = None -- (all) not available or removed from the broker
| New -- (participants: all) connection created (or received from sender)
| Pending -- (recipient) sent to sender out-of-band
| Confirmed -- (recipient) confirmed by sender with the broker
| Secured -- (all) secured with the broker
| Disabled -- (broker, recipient) disabled with the broker by recipient
deriving (Show, ShowSing, Eq)
data ConnState
= None -- (all) not available or removed from the broker
| New -- (recipient, broker) connection created (or received from sender)
| Pending -- (recipient, sender) sent to sender out-of-band
| Confirmed -- (recipient) confirmed by sender with the broker
| Secured -- (all) secured with the broker
| Disabled -- (broker, recipient) disabled with the broker by recipient
deriving (Show, Eq)
|]
)
data ConnSubscription = Subscribed | Idle
|])
type family HasState (p :: Party) (s :: ConnState) :: Constraint where
HasState Recipient s = ()
HasState Broker None = ()
HasState Broker New = ()
HasState Broker Secured = ()
HasState Broker Disabled = ()
HasState Sender None = ()
HasState Sender New = ()
HasState Sender Confirmed = ()
HasState Sender Secured = ()
type Prf1 t a = Auto (TyPred t) a
$(predicate [d|
-- broker connection states
data BrokerCS :: ConnectionState -> Type where
BrkNew :: BrokerCS New
BrkSecured :: BrokerCS Secured
BrkDisabled :: BrokerCS Disabled
BrkNone :: BrokerCS None
-- sender connection states
data SenderCS :: ConnectionState -> Type where
SndNew :: SenderCS New
SndConfirmed :: SenderCS Confirmed
SndSecured :: SenderCS Secured
SndNone :: SenderCS None
|])
-- allowed participant connection states
data HasState (p :: Participant) (s :: ConnectionState) :: Type where
RcpHasState :: HasState Recipient s
BrkHasState :: Prf1 BrokerCS s => HasState Broker s
SndHasState :: Prf1 SenderCS s => HasState Sender s
class Prf t p s where auto' :: t p s
instance Prf HasState Recipient s
where auto' = RcpHasState
instance Prf1 BrokerCS s => Prf HasState Broker s
where auto' = BrkHasState
instance Prf1 SenderCS s => Prf HasState Sender s
where auto' = SndHasState
-- established connection states (used by broker and recipient)
data EstablishedState (s :: ConnectionState) :: Type where
ESecured :: EstablishedState Secured
EDisabled :: EstablishedState Disabled
type Enabled rs bs =
( (rs == New || rs == Pending || rs == Confirmed || rs == Secured) ~ True,
(bs == New || bs == Secured) ~ True
)
data
Command
(from :: Party)
(fs :: ConnState)
(fs' :: ConnState)
(to :: Party)
(ts :: ConnState)
(ts' :: ConnState)
(res :: Type) :: Type where
CreateConn ::
PublicKey ->
Command Recipient None New Broker None New CreateConnResponse
Subscribe ::
Enabled rs bs =>
ConnId ->
Command Recipient rs rs Broker bs bs ()
Unsubscribe ::
Enabled rs bs =>
ConnId ->
Command Recipient rs rs Broker bs bs ()
SendInvite ::
Invitation ->
Command Recipient New Pending Sender None New ()
ConfirmConn ::
SenderConnId ->
Encrypted ->
Command Sender New Confirmed Broker New New ()
PushConfirm ::
ConnId ->
Message ->
Command Broker New New Recipient Pending Confirmed ()
SecureConn ::
ConnId ->
PublicKey ->
Command Recipient Confirmed Secured Broker New Secured ()
SendMsg ::
(ss == Confirmed || ss == Secured) ~ True =>
SenderConnId ->
Encrypted ->
Command Sender ss Secured Broker Secured Secured ()
PushMsg ::
ConnId ->
Message ->
Command Broker Secured Secured Recipient Secured Secured ()
DeleteMsg ::
ConnId ->
MessageId ->
Command Recipient Secured Secured Broker Secured Secured ()
-- connection type stub for all participants, TODO move from idris
data Connection (p :: Participant)
(s :: ConnectionState)
(ss :: ConnSubscription) :: Type where
Connection :: String -> Connection p s ss -- TODO replace with real type definition
data
Connection
(p :: Party)
(s :: ConnState) :: Type where
Connection :: String -> Connection p s -- TODO replace with real type definition
class Monad m => PartyProtocol m (p :: Party) where
api ::
Command from fs fs' p ps ps' res ->
Connection p ps ->
m (Either String (res, Connection p ps'))
action ::
Command p ps ps' to ts ts' res ->
Connection p ps ->
Either String res ->
m (Either String (Connection p ps'))
-- data types for connection states of all participants
infixl 7 <==>, <==| -- types
infixl 7 :<==>, :<==| -- constructors
apiStub :: Monad m => Connection p ps -> m (Either String (res, Connection p ps'))
apiStub _ = return $ Left "api not implemented"
data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
(:<==>) :: (Prf HasState Recipient rs, Prf HasState Broker bs)
=> Sing rs
-> Sing bs
-> rs <==> bs
actionStub :: Monad m => Connection p ps -> Either String res -> m (Either String (Connection p ps'))
actionStub _ _ = return $ Left "action not implemented"
deriving instance Show (rs <==> bs)
type AllowedStates from fs fs' to ts ts' =
( HasState from fs,
HasState from fs',
HasState to ts,
HasState to ts'
)
data family (<==|) rb (ss :: ConnectionState) :: Type
data instance (<==|) (rs <==> bs) ss :: Type where
(:<==|) :: Prf HasState Sender ss
=> rs <==> bs
-> Sing ss
-> rs <==> bs <==| ss
infix 6 :->
deriving instance Show (rs <==> bs <==| ss)
data PartiesCommand from fs fs' to ts ts' res :: Type where
(:->) ::
AllowedStates from fs fs' to ts ts' =>
Sing from ->
Sing to ->
Command from fs fs' to ts ts' res ->
PartiesCommand from fs fs' to ts ts' res
-- example of states of connection for all participants
-- recipient <==> broker <==| sender
st2 :: Pending <==> New <==| Confirmed
st2 = SPending :<==> SNew :<==| SConfirmed
$( promote
[d|
cConnSt :: Party -> ConnState -> ConnState -> ConnState -> ConnState
cConnSt p rs bs ss = case p of
Recipient -> rs
Broker -> bs
Sender -> ss
-- | Using not allowed connection type results in type error
--
-- >>> :{
-- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed
-- stBad = SPending :<==> SConfirmed :<==| SConfirmed
-- :}
-- ...
-- ... No instance for (Auto (TyPred BrokerCS) 'Confirmed)
-- ... arising from a use of ‘:<==>’
-- ...
pConnSt :: Party -> ConnState -> Party -> ConnState -> Party -> ConnState -> ConnState
pConnSt p ps from fs' to ts'
| p == from = fs'
| p == to = ts'
| otherwise = ps
|]
)
infixl 4 :>>
infixl 4 :>>, :>>=
data
Protocol
(rs :: ConnState)
(bs :: ConnState)
(ss :: ConnState)
(rs' :: ConnState)
(bs' :: ConnState)
(ss' :: ConnState)
(res :: Type) :: Type where
Start :: String -> Protocol rs bs ss rs' bs' ss' ()
(:>>) ::
Protocol rs bs ss rs' bs' ss' a ->
PartiesCommand from (CConnSt from rs' bs' ss') fs' to (CConnSt to rs' bs' ss') ts' b ->
Protocol rs bs ss
(PConnSt Recipient rs' from fs' to ts')
(PConnSt Broker bs' from fs' to ts')
(PConnSt Sender ss' from fs' to ts')
b
(:>>=) ::
Protocol rs bs ss rs' bs' ss' a ->
(a -> PartiesCommand from (CConnSt from rs' bs' ss') fs' to (CConnSt to rs' bs' ss') ts' b) ->
Protocol rs bs ss
(PConnSt Recipient rs' from fs' to ts')
(PConnSt Broker bs' from fs' to ts')
(PConnSt Sender ss' from fs' to ts')
b
data Command arg res
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(messages :: Nat) (messages' :: Nat)
:: Type where
infix 5 |$
CreateConn :: Prf HasState Sender s
=> Command
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle 0 0
Subscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command
() ()
Recipient Broker
(r <==> b <==| s)
(r <==> b <==| s)
Idle Subscribed n n
Unsubscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command
() ()
Recipient Broker
(r <==> b <==| s)
(r <==> b <==| s)
Subscribed Idle n n
SendInvite :: Prf HasState Broker s
=> Command
String () -- invitation - TODO
Recipient Sender
(New <==> s <==| None)
(Pending <==> s <==| New)
ss ss n n
ConfirmConn :: Prf HasState Recipient s
=> Command
SecureConnRequest ()
Sender Broker
(s <==> New <==| New)
(s <==> New <==| Confirmed)
ss ss n (n+1)
PushConfirm :: Prf HasState Sender s
=> Command
SecureConnRequest ()
Broker Recipient
(Pending <==> New <==| s)
(Confirmed <==> New <==| s)
Subscribed Subscribed n n
SecureConn :: Prf HasState Sender s
=> Command
SecureConnRequest ()
Recipient Broker
(Confirmed <==> New <==| s)
(Secured <==> Secured <==| s)
ss ss n n
SendWelcome :: Prf HasState Recipient s
=> Command
() ()
Sender Broker
(s <==> Secured <==| Confirmed)
(s <==> Secured <==| Secured)
ss ss n (n+1)
SendMsg :: Prf HasState Recipient s
=> Command
SendMessageRequest ()
Sender Broker
(s <==> Secured <==| Secured)
(s <==> Secured <==| Secured)
ss ss n (n+1)
PushMsg :: Prf HasState 'Sender s
=> Command
MessagesResponse () -- TODO, has to be a single message
Broker Recipient
(Secured <==> Secured <==| s)
(Secured <==> Secured <==| s)
Subscribed Subscribed n n
DeleteMsg :: Prf HasState Sender s
=> Command
() () -- TODO needs message ID parameter
Recipient Broker
(Secured <==> Secured <==| s)
(Secured <==> Secured <==| s)
ss ss n (n-1)
Return :: b -> Command a b from to state state ss ss n n
(:>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3
(:>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3
Fail :: String
-> Command a String from to state (None <==> None <==| None) ss ss n n
-- show and validate expexcted command participants
infix 6 -->
(-->) :: Sing from -> Sing to
-> ( Command a b from to s s' ss ss' n n'
-> Command a b from to s s' ss ss' n n' )
(-->) _ _ = id
-- extract connection state of specfic participant
type family PConnSt (p :: Participant) state where
PConnSt Recipient (r <==> b <==| s) = r
PConnSt Broker (r <==> b <==| s) = b
PConnSt Sender (r <==> b <==| s) = s
-- Type classes to ensure consistency of types of implementations
-- of participants commands/actions and connection state transitions (types)
-- with types of protocol commands defined above.
-- One participant's command is another participant's action.
class ProtocolCommand
arg res
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(messages :: Nat) (messages' :: Nat)
where
command :: Command arg res from to state state' ss ss' messages messages'
cmdMe :: Sing to
cmdOther :: Sing from
protoCmd :: Connection to (PConnSt to state) ss
-> arg
-> Either String (res, Connection to (PConnSt to state') ss')
protoCmdStub :: Connection to ps ss
-> arg
-> Either String (res, Connection to ps' ss')
protoCmdStub _ _ = Left "Command not implemented"
class ProtocolAction
arg res
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(messages :: Nat) (messages' :: Nat)
where
action :: Command arg res from to state state' ss ss' messages messages'
actionMe :: Sing from
actionOther :: Sing to
protoAction :: Connection from (PConnSt from state) ss
-> arg
-> Either String res
-> Either String (Connection from (PConnSt from state') ss')
protoActionStub :: Connection from ps ss
-> arg
-> Either String res
-> Either String (Connection from ps' ss')
protoActionStub _ _ _ = Left "Action not implemented"
-- TH to generate typeclasse instances for ProtocolCommand
-- and ProtocolAction classes from implementation definition syntax.
--
-- Given this declaration:
--
-- $(protocol Recipient [d|
-- rcPushConfirm = PushConfirm <-- Broker
-- raCreateConn = CreateConn --> Broker
-- |])
--
-- two instance declarations will be generated:
-- - for ProtocolCommand with `protoCmd = rcPushConfirm` and `command = PushConfirm`
-- - for ProtocolAction class with `protoAction = raCreateConn` and `action = CreateConn`
-- matching PushConfirm and CreateConn constructors types
-- Type definitions for functions rcPushConfirm and raCreateConn have to be written manually -
-- they have to be consistent with the typeclass.
data ProtocolOpeartion = POCommand | POAction | POUndefined
data ProtocolClassDescription = ProtocolClassDescription
{ clsName :: String
, mthd :: String
, meSing :: String
, otherSing :: String
, protoMthd :: String }
protocol :: Participant -> Q [Dec] -> Q [Dec]
protocol me ds = ds >>= mapM mkProtocolInstance
where
getCls :: ProtocolOpeartion -> Maybe ProtocolClassDescription
getCls POUndefined = Nothing
getCls POCommand = Just ProtocolClassDescription
{ clsName = "ProtocolCommand"
, mthd = "command"
, meSing = "cmdMe"
, otherSing = "cmdOther"
, protoMthd = "protoCmd" }
getCls POAction = Just ProtocolClassDescription
{ clsName = "ProtocolAction"
, mthd = "action"
, meSing = "actionMe"
, otherSing = "actionOther"
, protoMthd = "protoAction" }
mkProtocolInstance :: Dec -> Q Dec
mkProtocolInstance d = case d of
ValD
(VarP fName)
(NormalB
(InfixE
(Just (ConE cmd))
opExp
(Just (ConE other)))) [] ->
case getCls (getOperation opExp) of
Nothing -> badSyntax d
Just cls -> instanceDecl d fName cmd other cls
_ -> badSyntax d
instanceDecl :: Dec
-> Name -> Name -> Name
-> ProtocolClassDescription
-> Q Dec
instanceDecl d fName cmd other ProtocolClassDescription{..} =
reify cmd >>= \case
DataConI _ (ForallT _ ctxs ty) _ -> do
tc <- changeTyCon d ty clsName
return $
InstanceD Nothing ctxs tc
[ mkMethod mthd (ConE cmd)
, mkMethod meSing (mkSing $ show me)
, mkMethod otherSing (mkSing $ nameBase other)
, mkMethod protoMthd (VarE . mkName $ nameBase fName) ]
_ -> badSyntax d
mkMethod :: String -> Exp -> Dec
mkMethod name rhs = ValD (VarP (mkName name)) (NormalB rhs) []
mkSing :: String -> Exp
mkSing = ConE . mkName . ('S':)
changeTyCon :: Dec -> TH.Type -> String -> Q TH.Type
changeTyCon d (AppT t1 t2) n =
(`AppT` t2) <$> changeTyCon d t1 n
changeTyCon d (ConT name) n =
if nameBase name == "Command"
then conT $ mkName n
else badConstructor d
changeTyCon d _ _ = badConstructor d
badConstructor :: Dec -> Q TH.Type
badConstructor d = fail $ "constructor type must be Command\n" ++ pprint d
getOperation :: Exp -> ProtocolOpeartion
getOperation = \case
VarE name -> getOp name
UnboundVarE name -> getOp name
_ -> POUndefined
where
getOp n = case nameBase n of
"<--" -> POCommand
"-->" -> POAction
_ -> POUndefined
badSyntax :: Dec -> Q Dec
badSyntax d = fail $ "invalid protocol syntax: " ++ pprint d
-- introspect :: Name -> Q Exp
-- introspect n = reify n >>= runIO . putStrLn . pack . ppShow >> [|return ()|]
(|$) :: (a -> b) -> a -> b
f |$ x = f x

23
definitions/src/Simplex/Messaging/ProtocolDo.hs
View File

@@ -1,23 +0,0 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module Simplex.Messaging.ProtocolDo where
import ClassyPrelude
import Simplex.Messaging.Protocol
-- redifine Monad operators to compose commands
-- using `do` notation with RebindableSyntax extension
(>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3
(>>=) = (:>>=)
(>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3
(>>) = (:>>)
fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n
fail = Fail

51
definitions/src/Simplex/Messaging/Scenarios.hs
View File

@@ -1,18 +1,13 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-fields #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
-- below warning appears because of hiding Monad operators from prelude exports
{-# OPTIONS_GHC -fno-warn-dodgy-imports #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}
module Simplex.Messaging.Scenarios where
import ClassyPrelude hiding ((>>=), (>>), fail)
import Data.Singletons
import Simplex.Messaging.Protocol
import Simplex.Messaging.ProtocolDo
import Simplex.Messaging.Types
r :: Sing Recipient
@@ -24,24 +19,20 @@ b = SBroker
s :: Sing Sender
s = SSender
establishConnection :: Command
CreateConnRequest ()
Recipient Broker
(None <==> None <==| None)
(Secured <==> Secured <==| Secured)
Idle Idle 0 0
establishConnection = do -- it is commands composition, not Monad
r --> b $ CreateConn
r --> b $ Subscribe
r --> s $ SendInvite
s --> b $ ConfirmConn
b --> r $ PushConfirm
r --> b $ SecureConn
r --> b $ DeleteMsg
s --> b $ SendWelcome
b --> r $ PushMsg
r --> b $ DeleteMsg
s --> b $ SendMsg
b --> r $ PushMsg
r --> b $ DeleteMsg
r --> b $ Unsubscribe
establishConnection :: Protocol None None None Secured Secured Secured ()
establishConnection =
Start "Establish simplex messaging connection and send first message"
:>> r :-> b |$ CreateConn "BODbZxmtKUUF1l8pj4nVjQ"
:>> r :-> b |$ Subscribe "RU"
:>> r :-> s |$ SendInvite "invitation RU" -- invitation - TODo
:>> s :-> b |$ ConfirmConn "SU" "encrypted"
:>> b :-> r |$ PushConfirm "RU" Message {msgId = "abc", msg = "XPaVEVNunkYKqqK0dnAT5Q"}
:>> r :-> b |$ SecureConn "RU" "XPaVEVNunkYKqqK0dnAT5Q"
:>> r :-> b |$ DeleteMsg "RU" "abc"
:>> s :-> b |$ SendMsg "SU" "welcome" -- welcome message
:>> b :-> r |$ PushMsg "RU" Message {msgId = "def", msg = "welcome"}
:>> r :-> b |$ DeleteMsg "RU" "def"
:>> s :-> b |$ SendMsg "SU" "hello there"
:>> b :-> r |$ PushMsg "RU" Message {msgId = "ghi", msg = "hello there"}
:>> r :-> b |$ DeleteMsg "RU" "ghi"
:>> r :-> b |$ Unsubscribe "RU"

192
definitions/src/Simplex/Messaging/ServerAPI.hs
View File

@@ -1,109 +1,126 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Simplex.Messaging.ServerAPI
( ServerAPI
, serverApiIntro
, serverApiExtra
) where
( ServerAPI,
serverApiIntro,
serverApiExtra,
)
where
import ClassyPrelude
import Control.Lens
import Data.Function()
import Data.Function ()
import Servant
import Servant.Docs
import Simplex.Messaging.Types
type ServerAPI =
CreateConnection
:<|> SecureConnection
:<|> DeleteConnection
:<|> GetMessages
:<|> DeleteMessage
:<|> SendMessage
CreateConnection
:<|> SecureConnection
:<|> DeleteConnection
:<|> GetMessages
:<|> DeleteMessage
:<|> SendMessage
type CreateConnection = "connection" :> ReqBody '[JSON] CreateConnRequest
:> PostCreated '[JSON] CreateConnResponse
type CreateConnection =
"connection" :> ReqBody '[JSON] CreateConnRequest
:> PostCreated '[JSON] CreateConnResponse
type SecureConnection = "connection" :> Capture "connectionId" Base64EncodedString
:> ReqBody '[JSON] SecureConnRequest
:> Put '[JSON] NoContent
type SecureConnection =
"connection" :> Capture "connectionId" Base64EncodedString
:> ReqBody '[JSON] SecureConnRequest
:> Put '[JSON] NoContent
type DeleteConnection = "connection" :> Capture "connectionId" Base64EncodedString
:> Delete '[JSON] NoContent
type DeleteConnection =
"connection" :> Capture "connectionId" Base64EncodedString
:> Delete '[JSON] NoContent
type GetMessages = "connection" :> Capture "connectionId" Base64EncodedString :>
"messages" :> QueryParam "fromMessageId" (Maybe Base64EncodedString)
:> Get '[JSON] MessagesResponse
type GetMessages =
"connection" :> Capture "connectionId" Base64EncodedString
:> "messages"
:> QueryParam "fromMessageId" (Maybe Base64EncodedString)
:> Get '[JSON] MessagesResponse
type DeleteMessage = "connection" :> Capture "connectionId" Base64EncodedString :>
"messages" :> Capture "messageId" Base64EncodedString
:> Delete '[JSON] NoContent
type DeleteMessage =
"connection" :> Capture "connectionId" Base64EncodedString
:> "messages"
:> Capture "messageId" Base64EncodedString
:> Delete '[JSON] NoContent
type SendMessage = "connection" :> Capture "senderConnectionId" Base64EncodedString :>
"messages" :> ReqBody '[JSON] SendMessageRequest
:> PostCreated '[JSON] NoContent
type SendMessage =
"connection" :> Capture "senderConnectionId" Base64EncodedString
:> "messages"
:> ReqBody '[JSON] SendMessageRequest
:> PostCreated '[JSON] NoContent
-- API docs
serverApiIntro :: DocIntro
serverApiIntro = DocIntro "Simplex messaging protocol REST API"
[ "This document lists all required REST endpoints of simplex messaging API."
, "Also see [Simplex messaging protocol implementation](simplex-messaging-implementation.md) for more details."
]
serverApiIntro =
DocIntro
"Simplex messaging protocol REST API"
[ "This document lists all required REST endpoints of simplex messaging API.",
"Also see [Simplex messaging protocol implementation](simplex-messaging-implementation.md) for more details."
]
serverApiExtra :: ExtraInfo ServerAPI
serverApiExtra =
info (Proxy :: Proxy CreateConnection)
info
(Proxy :: Proxy CreateConnection)
"Create connection"
[]
<>
info (Proxy :: Proxy SecureConnection)
"Secure connection"
[]
<>
info (Proxy :: Proxy DeleteConnection)
"Delete connection"
[]
<>
info (Proxy :: Proxy GetMessages)
"Get messages"
[]
<>
info (Proxy :: Proxy DeleteMessage)
"Delete message"
[]
<>
info (Proxy :: Proxy SendMessage)
"Send message"
[]
<> info
(Proxy :: Proxy SecureConnection)
"Secure connection"
[]
<> info
(Proxy :: Proxy DeleteConnection)
"Delete connection"
[]
<> info
(Proxy :: Proxy GetMessages)
"Get messages"
[]
<> info
(Proxy :: Proxy DeleteMessage)
"Delete message"
[]
<> info
(Proxy :: Proxy SendMessage)
"Send message"
[]
where
info p title comments =
extraInfo p $ defAction & notes <>~ [DocNote title comments]
where
info p title comments =
extraInfo p $ defAction & notes <>~ [ DocNote title comments ]
instance ToCapture (Capture "connectionId" Text) where
instance ToCapture (Capture "connectionId" String) where
toCapture _ =
DocCapture "connectionId"
"Recipient connection ID - unique connection ID to be used by connection recipient"
DocCapture
"connectionId"
"Recipient connection ID - unique connection ID to be used by connection recipient"
instance ToCapture (Capture "senderConnectionId" Text) where
instance ToCapture (Capture "senderConnectionId" String) where
toCapture _ =
DocCapture "senderConnectionId"
"Sender connection ID - unique connection ID to be used by connection sender"
DocCapture
"senderConnectionId"
"Sender connection ID - unique connection ID to be used by connection sender"
instance ToCapture (Capture "messageId" Text) where
instance ToCapture (Capture "messageId" String) where
toCapture _ =
DocCapture "messageId"
"Message ID - unique message ID to be used by connection recipient"
DocCapture
"messageId"
"Message ID - unique message ID to be used by connection recipient"
instance ToParam (QueryParam "fromMessageId" (Maybe Base64EncodedString)) where
toParam _ =
DocQueryParam "fromMessageId"
["message ID, e.g., `p8PCiGPZ`"]
"if set, the server will respond with the messages received starting from the message with server message ID (unique per server) passed in this parameter."
Normal
DocQueryParam
"fromMessageId"
["message ID, e.g., `p8PCiGPZ`"]
"if set, the server will respond with the messages received starting from the message with server message ID (unique per server) passed in this parameter."
Normal
instance ToSample CreateConnRequest where
toSamples _ = singleSample $ CreateConnRequest "BODbZxmtKUUF1l8pj4nVjQ"
@@ -115,19 +132,24 @@ instance ToSample SecureConnRequest where
toSamples _ = singleSample $ SecureConnRequest "XPaVEVNunkYKqqK0dnAT5Q"
dummyMessage :: Message
dummyMessage = Message
{ connId = "p8PCiGPZ"
, ts = "2020-03-15T19:58:33.695Z"
, msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
}
dummyMessage =
Message
{ msgId = "p8PCiGPZ",
ts = "2020-03-15T19:58:33.695Z",
msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
}
instance ToSample MessagesResponse where
toSamples _ = singleSample $ MessagesResponse
{ messages = [dummyMessage]
, nextMessageId = Nothing
}
toSamples _ =
singleSample $
MessagesResponse
{ messages = [dummyMessage],
nextMessageId = Nothing
}
instance ToSample SendMessageRequest where
toSamples _ = singleSample $ SendMessageRequest
{ msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
}
toSamples _ =
singleSample $
SendMessageRequest
{ msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
}

246
definitions/src/Simplex/Messaging/Test.hs
View File

@@ -1,246 +0,0 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -freduction-depth=0 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Simplex.Messaging.Test where
import ClassyPrelude
import Data.Kind
import Data.Singletons
import Data.Singletons.ShowSing
import Data.Singletons.TH
import Data.Type.Predicate
import Data.Type.Predicate.Auto
import Simplex.Messaging.Types
$(singletons [d|
data Participant = Recipient | Broker | Sender
data ConnectionState = None -- (all) not available or removed from the broker
| New -- (participants: all) connection created (or received from sender)
| Pending -- (recipient) sent to sender out-of-band
| Confirmed -- (recipient) confirmed by sender with the broker
| Secured -- (all) secured with the broker
| Disabled -- (broker, recipient) disabled with the broker by recipient
| Drained -- (broker, recipient) drained (no messages)
deriving (Show, ShowSing, Eq)
data ConnSubscription = Subscribed | Idle
|])
-- broker connection states
type Prf1 t a = Auto (TyPred t) a
data BrokerCS :: ConnectionState -> Type where
BrkNew :: BrokerCS New
BrkSecured :: BrokerCS Secured
BrkDisabled :: BrokerCS Disabled
BrkDrained :: BrokerCS Drained
BrkNone :: BrokerCS None
instance Auto (TyPred BrokerCS) New where auto = autoTC
instance Auto (TyPred BrokerCS) Secured where auto = autoTC
instance Auto (TyPred BrokerCS) Disabled where auto = autoTC
instance Auto (TyPred BrokerCS) Drained where auto = autoTC
instance Auto (TyPred BrokerCS) None where auto = autoTC
-- sender connection states
data SenderCS :: ConnectionState -> Type where
SndNew :: SenderCS New
SndConfirmed :: SenderCS Confirmed
SndSecured :: SenderCS Secured
SndNone :: SenderCS None
instance Auto (TyPred SenderCS) New where auto = autoTC
instance Auto (TyPred SenderCS) Confirmed where auto = autoTC
instance Auto (TyPred SenderCS) Secured where auto = autoTC
instance Auto (TyPred SenderCS) None where auto = autoTC
-- allowed participant connection states
data HasState (p :: Participant) (s :: ConnectionState) :: Type where
RcpHasState :: HasState Recipient s
BrkHasState :: Prf1 BrokerCS s => HasState Broker s
SndHasState :: Prf1 SenderCS s => HasState Sender s
class Prf t p s where auto' :: t p s
instance Prf HasState Recipient s
where auto' = RcpHasState
instance Prf1 BrokerCS s => Prf HasState Broker s
where auto' = BrkHasState
instance Prf1 SenderCS s => Prf HasState Sender s
where auto' = SndHasState
-- connection type stub for all participants, TODO move from idris
data Connection (p :: Participant)
(s :: ConnectionState)
(ss :: ConnSubscription) :: Type where
Connection :: String -> Connection p s ss -- TODO replace with real type definition
-- data types for connection states of all participants
infixl 7 <==>, <==| -- types
infixl 7 :<==>, :<==| -- constructors
data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
(:<==>) :: (Prf HasState Recipient rs, Prf HasState Broker bs)
=> Sing rs
-> Sing bs
-> rs <==> bs
deriving instance Show (rs <==> bs)
data family (<==|) rcpBrk (ss :: ConnectionState) :: Type
data instance (<==|) (rs <==> bs) ss :: Type where
(:<==|) :: Prf HasState Sender ss
=> rs <==> bs
-> Sing ss
-> rs <==> bs <==| ss
deriving instance Show (rs <==> bs <==| ss)
-- type family (<==|) rb ss where
-- (rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss
-- recipient <==> broker <==| sender
st2 :: Pending <==> New <==| Confirmed
st2 = SPending :<==> SNew :<==| SConfirmed
-- this must not type check
-- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed
-- stBad = SPending :<==> SConfirmed :<==| SConfirmed
-- data type with all available protocol commands
$(singletons [d|
data ProtocolCmd = CreateConnCmd
| SubscribeCmd
| Comp -- result of composing multiple commands
|])
data Command (cmd :: ProtocolCmd) arg result
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
:: Type where
CreateConn :: Prf HasState Sender s
=> Command CreateConnCmd
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle
Subscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command SubscribeCmd
() ()
Recipient Broker
(r <==> b <==| s)
(r <==> b <==| s)
Idle Subscribed
-- extract connection state of specfic participant
type family PConnSt (p :: Participant) state where
PConnSt Recipient (r <==> b <==| s) = r
PConnSt Broker (r <==> b <==| s) = b
PConnSt Sender (r <==> b <==| s) = s
-- Type classes to ensure consistency of types of implementations
-- of participants actions/functions and connection state transitions (types)
-- with types of protocol commands defined above.
-- TODO for some reason this type class is not enforced -
-- it still allows to construct invalid implementations.
-- See comment in Broker.hs
-- As done in Client.hs it type-checks, but it looks ugly
-- class PrfCmd cmd arg res from to s1 s2 s3 s1' s2' s3' ss ss' where
-- command :: Command cmd arg res from to (AllConnState s1 s2 s3) (AllConnState s1' s2' s3') ss ss'
-- instance Prf HasState Sender s
-- => PrfCmd CreateConnCmd
-- CreateConnRequest CreateConnResponse
-- Recipient Broker
-- None None s
-- New New s
-- Idle Idle
-- where
-- command = CreateConn
-- data Cmd cmd arg res from to ss ss' :: Type where
-- Cmd :: Command cmd arg res
-- from to
-- (AllConnState s1 s2 s3)
-- (AllConnState s1' s2' s3')
-- ss ss'
-- -> Cmd cmd arg res from to ss ss'
class ProtocolFunc
(cmd :: ProtocolCmd) arg res
(from :: Participant) (p :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
where
pfCommand :: Command (cmd :: ProtocolCmd) arg res
(from :: Participant) (p :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
protoFunc :: Connection p (PConnSt p state) ss
-> arg
-> Either String (res, Connection p (PConnSt p state') ss')
-- For some reason PrfCmd type-class requirement is not enforced here:
-- if I change one of the connection states to one for which
-- instance of PrfCmd does not exist (i.e. Command cannot be constructed),
-- it compiles anyway.
-- Creating Command instance here would prevent compilation
-- in case the types are incorrect, as it is done in Client.hs
instance Prf HasState Sender s
=> ProtocolFunc CreateConnCmd
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle -- connection states
where
pfCommand = CreateConn
protoFunc = brkCreateConn
brkCreateConn :: Connection Broker None Idle
-> CreateConnRequest
-> Either String (CreateConnResponse, Connection Broker New Idle)
brkCreateConn (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str)
-- TODO stub
-- -- below code should NOT compile, but it does
-- instance ProtocolFunc Broker CreateConnCmd
-- CreateConnRequest CreateConnResponse -- request response
-- None New Idle Idle -- "Secured" should not be allowed here,
-- where -- such command does not exist, so no instance of
-- protoFunc _ = \(Connection str) _ -> Right (CreateConnResponse "1" "2", Connection str) -- PrfCmd exist...? But it compiles.
-- bCreateConn' :: Connection Broker None Idle
-- -> CreateConnRequest
-- -> Either String
-- (CreateConnResponse, Connection Broker New Idle)
-- bCreateConn' = protoFunc $ CreateConn @None

90
definitions/src/Simplex/Messaging/Types.hs
View File

@@ -1,52 +1,76 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
module Simplex.Messaging.Types where
import ClassyPrelude
import Data.Aeson
import GHC.Generics()
import Data.String
import GHC.Generics
newtype CreateConnRequest = CreateConnRequest
{ recipientKey :: Key
} deriving (Eq, Show, Generic, ToJSON, FromJSON)
newtype CreateConnRequest
= CreateConnRequest
{ recipientKey :: Key
}
deriving (Eq, Show, Generic, ToJSON, FromJSON)
instance IsString CreateConnRequest where
fromString = CreateConnRequest . pack
fromString = CreateConnRequest
data CreateConnResponse
= CreateConnResponse
{ recipientId :: String,
senderId :: String
}
deriving (Show, Generic, ToJSON, FromJSON)
data CreateConnResponse = CreateConnResponse
{ recipientId :: String
, senderId :: String
} deriving (Show, Generic, ToJSON, FromJSON)
newtype SecureConnRequest = SecureConnRequest
{ senderKey :: Key
} deriving (Show, Generic, ToJSON, FromJSON)
newtype SecureConnRequest
= SecureConnRequest
{ senderKey :: Key
}
deriving (Show, Generic, ToJSON, FromJSON)
instance IsString SecureConnRequest where
fromString = SecureConnRequest . pack
fromString = SecureConnRequest
data Message
= Message
{ msgId :: MessageId,
ts :: TimeStamp,
msg :: Encrypted -- TODO make it Text
}
deriving (Show, Generic, ToJSON, FromJSON)
data Message = Message
{ connId :: Base64EncodedString
, ts :: TimeStamp
, msg :: Base64EncodedString
} deriving (Show, Generic, ToJSON, FromJSON)
data MessagesResponse
= MessagesResponse
{ messages :: [Message],
nextMessageId :: Maybe Base64EncodedString
}
deriving (Show, Generic, ToJSON, FromJSON)
data MessagesResponse = MessagesResponse
{ messages :: [Message]
, nextMessageId :: Maybe Base64EncodedString
} deriving (Show, Generic, ToJSON, FromJSON)
newtype SendMessageRequest = SendMessageRequest
{ msg :: Base64EncodedString
} deriving (Show, Generic, ToJSON, FromJSON)
newtype SendMessageRequest
= SendMessageRequest
{ msg :: Base64EncodedString
}
deriving (Show, Generic, ToJSON, FromJSON)
instance IsString SendMessageRequest where
fromString = SendMessageRequest . pack
fromString = SendMessageRequest
type Invitation = Base64EncodedString -- TODO define
type Key = Base64EncodedString
type Base64EncodedString = Text
type TimeStamp = Text
type Key = Base64EncodedString -- deprecated, not to be used
type PublicKey = Base64EncodedString
type ConnId = Base64EncodedString
type SenderConnId = Base64EncodedString
type MessageId = Base64EncodedString
type Encrypted = Base64EncodedString
type Base64EncodedString = String
type TimeStamp = String

2
definitions/tests/doctest-driver.hs
View File

@@ -1 +1 @@
{-# OPTIONS_GHC -F -pgmF doctest-driver-gen -optF src -optF -XBlockArguments -optF -XDuplicateRecordFields -optF -XLambdaCase -optF -XNamedFieldPuns -optF -XNoImplicitPrelude -optF -XOverloadedStrings -optF -XRecordWildCards -optF -XAllowAmbiguousTypes -optF -XConstraintKinds -optF -XDeriveAnyClass -optF -XEmptyCase -optF -XFlexibleContexts -optF -XFlexibleInstances -optF -XGADTs -optF -XInstanceSigs -optF -XMultiParamTypeClasses -optF -XNoStarIsType -optF -XScopedTypeVariables -optF -XStandaloneDeriving -optF -XTemplateHaskell -optF -XTypeApplications -optF -XTypeFamilies -optF -XTypeInType -optF -XTypeOperators -optF -XUndecidableInstances #-}
{-# OPTIONS_GHC -F -pgmF doctest-driver-gen -optF src -optF -XBlockArguments -optF -XDuplicateRecordFields -optF -XLambdaCase -optF -XNamedFieldPuns -optF -XOverloadedStrings -optF -XRecordWildCards -optF -XAllowAmbiguousTypes -optF -XConstraintKinds -optF -XDeriveAnyClass -optF -XEmptyCase -optF -XFlexibleContexts -optF -XFlexibleInstances -optF -XGADTs -optF -XInstanceSigs -optF -XMultiParamTypeClasses -optF -XNoStarIsType -optF -XScopedTypeVariables -optF -XStandaloneDeriving -optF -XTemplateHaskell -optF -XTypeApplications -optF -XTypeFamilies -optF -XTypeInType -optF -XTypeOperators -optF -XUndecidableInstances #-}

2
simplex-messaging-api.md
View File

@@ -130,7 +130,7 @@ Also see [Simplex messaging protocol implementation](simplex-messaging-implement
- Example (`application/json;charset=utf-8`, `application/json`):
```javascript
{"messages":[{"ts":"2020-03-15T19:58:33.695Z","msg":"OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs","connId":"p8PCiGPZ"}],"nextMessageId":null}
{"messages":[{"ts":"2020-03-15T19:58:33.695Z","msg":"OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs","msgId":"p8PCiGPZ"}],"nextMessageId":null}
```
## DELETE /connection/:connectionId/messages/:messageId