connection states in haskell protocol definition

2020-05-09 12:38:07 +01:00
parent b16b5c5948
commit 7ee44a6d41
9 changed files with 150 additions and 85 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -40,6 +40,8 @@ cabal.project.local
 cabal.project.local~
 .HTF/
 .ghc.environment.*
+.cabal
+stack.yaml.lock

 # Idris
-*.ibc
+*.ibc
--- a/definitions/package.yaml
+++ b/definitions/package.yaml
@@ -13,25 +13,59 @@ extra-source-files:
 ghc-options:
  - -Wall
  - -Wcompat
-  - -Worphans
  - -Werror=incomplete-patterns
  - -Wredundant-constraints
  - -Wincomplete-record-updates
  - -Wincomplete-uni-patterns

 default-extensions:
-  - DeriveAnyClass
-  - DeriveGeneric
-  - DuplicateRecordFields
-  - FlexibleInstances
+  - TemplateHaskell
  - NoImplicitPrelude
+  # numbers, strings, lists
+  - NegativeLiterals
+  - NumericUnderscores
  - OverloadedStrings
+  # function syntax
+  - BlockArguments
+  - EmptyCase
+  - LambdaCase
+  # Records
+  - DuplicateRecordFields
+  - NamedFieldPuns
+  - RecordWildCards
+  # deriving
+  - DeriveAnyClass
+  - DeriveFunctor
+  - DeriveGeneric
+  - StandaloneDeriving
+  # type classes
+  - FunctionalDependencies
+  - FlexibleContexts
+  - FlexibleInstances
+  - InstanceSigs
+  - TypeSynonymInstances
+  - UndecidableInstances
+  # types
+  - DataKinds
+  - ConstraintKinds
+  - GADTs
+  - KindSignatures
+  - LiberalTypeSynonyms
+  - NoStarIsType
+  - PolyKinds
+  - RankNTypes
+  - ScopedTypeVariables
+  - TypeApplications
+  - TypeFamilies
+  - TypeOperators
  
 dependencies:
  - aeson
  - base >= 4.7 && < 5
  - classy-prelude
+  - decidable
  - lens
+  - singletons
  - servant-docs
  - servant-server

--- a/definitions/simplex-definitions.cabal
+++ b/definitions/simplex-definitions.cabal
@@ -1,59 +0,0 @@
-cabal-version: 1.12
-
-- This file has been generated from package.yaml by hpack version 0.31.2.
--
-- see: https://github.com/sol/hpack
--
-- hash: 0ccb821856e91efe2302b7718ec2477aa768ae2bdf82cdd9d352333d5a8bf829
-
-name:           simplex-definitions
-version:        0.1.0.0
-category:       Web
-homepage:       https://github.com/simplex-chat/protocol/blob/master/definitions/readme.md
-author:         Evgeny Poberezkin
-maintainer:     Evgeny Poberezkin
-copyright:      2020 Evgeny Poberezkin
-license:        AGPL-3
-license-file:   LICENSE
-build-type:     Simple
-extra-source-files:
-    readme.md
-
-library
-  exposed-modules:
-      Simplex.Messaging.Types
-      Simplex.Messaging.ServerAPI
-  other-modules:
-      Main
-      Paths_simplex_definitions
-  hs-source-dirs:
-      src
-  default-extensions: DeriveAnyClass DeriveGeneric DuplicateRecordFields FlexibleInstances NoImplicitPrelude OverloadedStrings
-  ghc-options: -Wall -Wcompat -Worphans -Werror=incomplete-patterns -Wredundant-constraints -Wincomplete-record-updates -Wincomplete-uni-patterns
-  build-depends:
-      aeson
-    , base >=4.7 && <5
-    , classy-prelude
-    , lens
-    , servant-docs
-    , servant-server
-  default-language: Haskell2010
-
-executable api-docs
-  main-is: Main.hs
-  other-modules:
-      Simplex.Messaging.ServerAPI
-      Simplex.Messaging.Types
-      Paths_simplex_definitions
-  hs-source-dirs:
-      src
-  default-extensions: DeriveAnyClass DeriveGeneric DuplicateRecordFields FlexibleInstances NoImplicitPrelude OverloadedStrings
-  ghc-options: -Wall -Wcompat -Worphans -Werror=incomplete-patterns -Wredundant-constraints -Wincomplete-record-updates -Wincomplete-uni-patterns
-  build-depends:
-      aeson
-    , base >=4.7 && <5
-    , classy-prelude
-    , lens
-    , servant-docs
-    , servant-server
-  default-language: Haskell2010
--- a/definitions/src/Simplex/Messaging/Protocol.hs
+++ b/definitions/src/Simplex/Messaging/Protocol.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Simplex.Messaging.Protocol where
+
+import Data.Kind
+import Data.Singletons()
+import Data.Singletons.TH
+import Data.Type.Predicate
+import Data.Type.Predicate.Auto
+
+$(singletons [d|
+  data Participant = Recipient | Broker | Sender
+
+  data ConnectionState =  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)
+                        | None      -- (all) not available or removed from the broker
+  |])
+
+-- 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 = BrkNew
+instance Auto (TyPred BrokerCS) 'Secured  where auto = BrkSecured
+instance Auto (TyPred BrokerCS) 'Disabled where auto = BrkDisabled
+instance Auto (TyPred BrokerCS) 'Drained  where auto = BrkDrained
+instance Auto (TyPred BrokerCS) 'None     where auto = BrkNone
+
+-- 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 = SndNew
+instance Auto (TyPred SenderCS) 'Confirmed where auto = SndConfirmed
+instance Auto (TyPred SenderCS) 'Secured   where auto = SndSecured
+instance Auto (TyPred SenderCS) 'None      where auto = SndNone
+
+-- 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 p a s where auto' :: p a 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
+  EDrained  :: EstablishedState 'Drained
+
+
+-- 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
+
+data family (<==|) rb (ss :: ConnectionState)
+data instance (<==|) (rs <==> bs) ss :: Type where
+  (:<==|) :: Prf HasState 'Sender ss
+          => rs <==> bs
+          -> Sing ss
+          -> rs <==> bs <==| ss
+
+st1 :: 'New <==> 'New
+st1 = SNew :<==> SNew
+
+st2 :: 'Pending <==> 'New <==| 'Confirmed
+st2 = SPending :<==> SNew :<==| SConfirmed
+
+-- this must not type check
+-- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed
+-- stBad = SPending :<==> SConfirmed :<==| SConfirmed
--- a/definitions/src/Simplex/Messaging/ServerAPI.hs
+++ b/definitions/src/Simplex/Messaging/ServerAPI.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}

 module Simplex.Messaging.ServerAPI
  ( ServerAPI
@@ -78,8 +77,9 @@ serverApiExtra =
    "Send message"
    []

-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
  toCapture _ =
--- a/definitions/src/Simplex/Messaging/Types.hs
+++ b/definitions/src/Simplex/Messaging/Types.hs
@@ -2,7 +2,7 @@ module Simplex.Messaging.Types where

 import ClassyPrelude
 import Data.Aeson
-import GHC.Generics
+import GHC.Generics()

 newtype NewConnectionReqBody = NewConnectionReqBody
  { recipientKey :: Base64EncodedString
--- a/definitions/stack.yaml
+++ b/definitions/stack.yaml
@@ -17,7 +17,7 @@
 #
 # resolver: ./custom-snapshot.yaml
 # resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: lts-15.3
+resolver: lts-15.11

 # User packages to be built.
 # Various formats can be used as shown in the example below.
@@ -39,7 +39,10 @@ packages:
 # - git: https://github.com/commercialhaskell/stack.git
 #   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
 #
-# extra-deps: []
+extra-deps:
+- decidable-0.3.0.0@sha256:34857003b57139a047c9ab7944c313c227d9db702a8dcefa1478966257099423,1774
+- functor-products-0.1.1.0@sha256:2bea36b6106b5756be6b81b3a5bfe7b41db1cf45fb63c19a1f04b572ba90fd0c,1456
+- vinyl-0.12.1@sha256:03f5e246fae2434250987bbfe708015dc6e23f60c20739c34738acde1383b96c,3921

 # Override default flag values for local packages and extra-deps
 # flags: {}
--- a/definitions/stack.yaml.lock
+++ b/definitions/stack.yaml.lock
@@ -1,12 +0,0 @@
-# This file was autogenerated by Stack.
-# You should not edit this file by hand.
-# For more information, please see the documentation at:
-#   https://docs.haskellstack.org/en/stable/lock_files
-
-packages: []
-snapshots:
- completed:
-    size: 491373
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/15/3.yaml
-    sha256: 29e9ff61b8bf4b4fcff55cde3ac106ebb971f0d21331dccac9eee63374fa6ca8
-  original: lts-15.3
--- a/specification/Simplex/Messaging/Protocol.idr
+++ b/specification/Simplex/Messaging/Protocol.idr
@@ -2,7 +2,7 @@ module Simplex.Messaging.Protocol

 %access public export

-data Participant = Recipient | Sender | Broker
+data Participant = Recipient | Broker | Sender

 data Client : Participant -> Type where
  CRecipient : Client Recipient