diff --git a/definitions/src/Main.hs b/definitions/app/api-docs/Main.hs similarity index 72% rename from definitions/src/Main.hs rename to definitions/app/api-docs/Main.hs index 97abfc5b68..cd9bf37c21 100644 --- a/definitions/src/Main.hs +++ b/definitions/app/api-docs/Main.hs @@ -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 diff --git a/definitions/app/print-scenarios/Main.hs b/definitions/app/print-scenarios/Main.hs new file mode 100644 index 0000000000..9f605eccc7 --- /dev/null +++ b/definitions/app/print-scenarios/Main.hs @@ -0,0 +1,7 @@ +module Main where + +import Simplex.Messaging.PrintScenario +import Simplex.Messaging.Scenarios + +main :: IO () +main = printScenario establishConnection diff --git a/definitions/package.yaml b/definitions/package.yaml index 45836f8e49..7cd5218aa7 100644 --- a/definitions/package.yaml +++ b/definitions/package.yaml @@ -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: diff --git a/definitions/src/Predicate.hs b/definitions/src/Predicate.hs deleted file mode 100644 index 0f60757ce2..0000000000 --- a/definitions/src/Predicate.hs +++ /dev/null @@ -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 [] diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index dd48e31851..86ca6cfe0a 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -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 diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 05a57e8d99..126e22af8c 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -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 diff --git a/definitions/src/Simplex/Messaging/Connection.hs b/definitions/src/Simplex/Messaging/Connection.hs new file mode 100644 index 0000000000..b6c924d8b4 --- /dev/null +++ b/definitions/src/Simplex/Messaging/Connection.hs @@ -0,0 +1 @@ +module Simplex.Messaging.Connection where diff --git a/definitions/src/Simplex/Messaging/PrintScenario.hs b/definitions/src/Simplex/Messaging/PrintScenario.hs new file mode 100644 index 0000000000..95c6ddad19 --- /dev/null +++ b/definitions/src/Simplex/Messaging/PrintScenario.hs @@ -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)" diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 727219f07f..c15e97ceac 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -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 diff --git a/definitions/src/Simplex/Messaging/ProtocolDo.hs b/definitions/src/Simplex/Messaging/ProtocolDo.hs deleted file mode 100644 index 7e1ddbee07..0000000000 --- a/definitions/src/Simplex/Messaging/ProtocolDo.hs +++ /dev/null @@ -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 diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index dfb9aa487d..3922e70e4d 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -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" diff --git a/definitions/src/Simplex/Messaging/ServerAPI.hs b/definitions/src/Simplex/Messaging/ServerAPI.hs index fc20227413..b087d12e9f 100644 --- a/definitions/src/Simplex/Messaging/ServerAPI.hs +++ b/definitions/src/Simplex/Messaging/ServerAPI.hs @@ -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" + } diff --git a/definitions/src/Simplex/Messaging/Test.hs b/definitions/src/Simplex/Messaging/Test.hs deleted file mode 100644 index 42e9085b0d..0000000000 --- a/definitions/src/Simplex/Messaging/Test.hs +++ /dev/null @@ -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 diff --git a/definitions/src/Simplex/Messaging/Types.hs b/definitions/src/Simplex/Messaging/Types.hs index 7434c8e55d..e582de8527 100644 --- a/definitions/src/Simplex/Messaging/Types.hs +++ b/definitions/src/Simplex/Messaging/Types.hs @@ -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 diff --git a/definitions/tests/doctest-driver.hs b/definitions/tests/doctest-driver.hs index 48e0aa73d9..e18adfbdc5 100644 --- a/definitions/tests/doctest-driver.hs +++ b/definitions/tests/doctest-driver.hs @@ -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 #-} diff --git a/simplex-messaging-api.md b/simplex-messaging-api.md index cbd06e6b77..e122fa8730 100644 --- a/simplex-messaging-api.md +++ b/simplex-messaging-api.md @@ -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