Define header sync protocol

marlowe-runtime/marlowe-runtime.cabal

@@ -64,6 +64,10 @@ library
   import: lang
   hs-source-dirs:   src
   exposed-modules:
+    Language.Marlowe.Protocol.HeaderSync.Client
+    Language.Marlowe.Protocol.HeaderSync.Codec
+    Language.Marlowe.Protocol.HeaderSync.Server
+    Language.Marlowe.Protocol.HeaderSync.Types
     Language.Marlowe.Protocol.Sync.Client
     Language.Marlowe.Protocol.Sync.Codec
     Language.Marlowe.Protocol.Sync.Server

marlowe-runtime/src/Language/Marlowe/Protocol/HeaderSync/Client.hs

@@ -0,0 +1,94 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Language.Marlowe.Protocol.HeaderSync.Client
+  where
+
+import Language.Marlowe.Protocol.HeaderSync.Types
+import Language.Marlowe.Runtime.ChainSync.Api (BlockHeader)
+import Language.Marlowe.Runtime.Discovery.Api (ContractHeader)
+import Network.TypedProtocol
+
+newtype MarloweHeaderSyncClient m a = MarloweHeaderSyncClient { runMarloweHeaderSyncClient :: m (ClientStIdle m a) }
+
+data ClientStIdle m a where
+  SendMsgRequestNext :: ClientStNext m a -> ClientStIdle m a
+  SendMsgIntersect :: [BlockHeader] -> ClientStIntersect m a -> ClientStIdle m a
+  SendMsgDone :: a -> ClientStIdle m a
+
+deriving instance Functor m => Functor (ClientStIdle m)
+
+data ClientStIntersect m a = ClientStIntersect
+  { recvMsgIntersectFound :: BlockHeader -> m (ClientStIdle m a)
+  , recvMsgIntersectNotFound :: m (ClientStIdle m a)
+  } deriving Functor
+
+data ClientStNext m a = ClientStNext
+  { recvMsgNewHeaders :: BlockHeader -> [ContractHeader] -> m (ClientStIdle m a)
+  , recvMsgRollBackward :: BlockHeader -> m (ClientStIdle m a)
+  , recvMsgWait :: m (ClientStWait m a)
+  } deriving Functor
+
+data ClientStWait m a where
+  SendMsgPoll :: ClientStNext m a -> ClientStWait m a
+  SendMsgCancel :: ClientStIdle m a -> ClientStWait m a
+
+deriving instance Functor m => Functor (ClientStWait m)
+
+hoistMarloweHeaderSyncClient
+  :: forall m n a
+   . Functor m
+  => (forall x. m x -> n x)
+  -> MarloweHeaderSyncClient m a
+  -> MarloweHeaderSyncClient n a
+hoistMarloweHeaderSyncClient nat = MarloweHeaderSyncClient . nat . fmap hoistIdle . runMarloweHeaderSyncClient
+  where
+    hoistIdle :: ClientStIdle m a -> ClientStIdle n a
+    hoistIdle = \case
+      SendMsgRequestNext next -> SendMsgRequestNext $ hoistNext next
+      SendMsgIntersect blocks intersect -> SendMsgIntersect blocks $ hoistIntersect intersect
+      SendMsgDone a -> SendMsgDone a
+
+    hoistIntersect :: ClientStIntersect m a -> ClientStIntersect n a
+    hoistIntersect ClientStIntersect{..} = ClientStIntersect
+      { recvMsgIntersectFound = nat . fmap hoistIdle . recvMsgIntersectFound
+      , recvMsgIntersectNotFound = nat $ hoistIdle <$> recvMsgIntersectNotFound
+      }
+
+    hoistNext :: ClientStNext m a -> ClientStNext n a
+    hoistNext ClientStNext{..} = ClientStNext
+      { recvMsgNewHeaders = fmap (nat . fmap hoistIdle) . recvMsgNewHeaders
+      , recvMsgRollBackward = nat . fmap hoistIdle . recvMsgRollBackward
+      , recvMsgWait = nat $ hoistWait <$> recvMsgWait
+      }
+
+    hoistWait :: ClientStWait m a -> ClientStWait n a
+    hoistWait = \case
+      SendMsgPoll next -> SendMsgPoll $ hoistNext next
+      SendMsgCancel idle -> SendMsgCancel $ hoistIdle idle
+
+marloweHeaderSyncClientPeer :: forall m a. Functor m => MarloweHeaderSyncClient m a -> Peer MarloweHeaderSync 'AsClient 'StIdle m a
+marloweHeaderSyncClientPeer = Effect . fmap peerIdle . runMarloweHeaderSyncClient
+  where
+    peerIdle :: ClientStIdle m a -> Peer MarloweHeaderSync 'AsClient 'StIdle m a
+    peerIdle = \case
+      SendMsgDone a -> Yield (ClientAgency TokIdle) MsgDone $ Done TokDone a
+      SendMsgIntersect blocks intersect-> Yield (ClientAgency TokIdle) (MsgIntersect blocks) $ peerIntersect intersect
+      SendMsgRequestNext next -> Yield (ClientAgency TokIdle) MsgRequestNext $ peerNext next
+
+    peerIntersect :: ClientStIntersect m a -> Peer MarloweHeaderSync 'AsClient 'StIntersect m a
+    peerIntersect ClientStIntersect{..} = Await (ServerAgency TokIntersect) $ Effect . \case
+      MsgIntersectFound block -> peerIdle <$> recvMsgIntersectFound block
+      MsgIntersectNotFound -> peerIdle <$> recvMsgIntersectNotFound
+
+    peerNext :: ClientStNext m a -> Peer MarloweHeaderSync 'AsClient 'StNext m a
+    peerNext ClientStNext{..} = Await (ServerAgency TokNext) $ Effect . \case
+      MsgNewHeaders block headers -> peerIdle <$> recvMsgNewHeaders block headers
+      MsgRollBackward block -> peerIdle <$> recvMsgRollBackward block
+      MsgWait -> peerWait <$> recvMsgWait
+
+    peerWait :: ClientStWait m a -> Peer MarloweHeaderSync 'AsClient 'StWait m a
+    peerWait = \case
+      SendMsgPoll next -> Yield (ClientAgency TokWait) MsgPoll $ peerNext next
+      SendMsgCancel idle -> Yield (ClientAgency TokWait) MsgCancel $ peerIdle idle

marlowe-runtime/src/Language/Marlowe/Protocol/HeaderSync/Codec.hs

@@ -0,0 +1,89 @@
+{-# LANGUAGE GADTs #-}
+
+module Language.Marlowe.Protocol.HeaderSync.Codec
+  where
+
+import Data.Binary (get, getWord8, put, putWord8)
+import qualified Data.ByteString.Lazy as LBS
+import Language.Marlowe.Protocol.HeaderSync.Types
+import Network.Protocol.Codec (DeserializeError, GetMessage, PutMessage, binaryCodec)
+import Network.TypedProtocol.Codec (Codec, PeerHasAgency(..), SomeMessage(SomeMessage))
+
+codecMarloweHeaderSync :: Applicative m => Codec MarloweHeaderSync DeserializeError m LBS.ByteString
+codecMarloweHeaderSync = binaryCodec putMessage getMessage
+  where
+  putMessage :: PutMessage MarloweHeaderSync
+  putMessage = \case
+    ClientAgency TokIdle -> \case
+      MsgRequestNext -> putWord8 0x01
+      MsgIntersect blocks -> putWord8 0x02 *> put blocks
+      MsgDone -> putWord8 0x03
+
+    ServerAgency TokNext -> \case
+      MsgNewHeaders block headers -> do
+        putWord8 0x04
+        put block
+        put headers
+      MsgRollBackward block -> do
+        putWord8 0x05
+        put block
+
+      MsgWait -> putWord8 0x06
+
+    ClientAgency TokWait -> \case
+      MsgPoll -> putWord8 0x07
+      MsgCancel -> putWord8 0x08
+
+    ServerAgency TokIntersect -> \case
+      MsgIntersectFound block -> do
+        putWord8 0x09
+        put block
+      MsgIntersectNotFound -> putWord8 0x0a
+
+  getMessage :: GetMessage MarloweHeaderSync
+  getMessage tok = do
+    tag <- getWord8
+    case tag of
+      0x01 -> case tok of
+        ClientAgency TokIdle -> pure $ SomeMessage MsgRequestNext
+        _                        -> fail "Invalid protocol state for MsgRequestNext"
+
+      0x02 -> case tok of
+        ClientAgency TokIdle -> SomeMessage .MsgIntersect <$> get
+        _ -> fail "Invalid protocol state for MsgNewHeaders"
+
+      0x03 -> case tok of
+        ClientAgency TokIdle -> pure $ SomeMessage MsgDone
+        _                        -> fail "Invalid protocol state for MsgDone"
+
+      0x04 -> case tok of
+        ServerAgency TokNext -> do
+          block <- get
+          SomeMessage . MsgNewHeaders block <$> get
+        _ -> fail "Invalid protocol state for MsgNewHeaders"
+
+      0x05 -> case tok of
+        ServerAgency TokNext -> SomeMessage . MsgRollBackward <$> get
+        _                        -> fail "Invalid protocol state for MsgRollBackward"
+
+      0x06 -> case tok of
+        ServerAgency TokNext -> pure $ SomeMessage MsgWait
+        _                        -> fail "Invalid protocol state for MsgWait"
+
+      0x07 -> case tok of
+        ClientAgency TokWait -> pure $ SomeMessage MsgPoll
+        _                        -> fail "Invalid protocol state for MsgPoll"
+
+      0x08 -> case tok of
+        ClientAgency TokWait -> pure $ SomeMessage MsgCancel
+        _                        -> fail "Invalid protocol state for MsgCancel"
+
+      0x09 -> case tok of
+        ServerAgency TokIntersect -> SomeMessage . MsgIntersectFound <$> get
+        _                             -> fail "Invalid protocol state for MsgIntersectFound"
+
+      0x0a -> case tok of
+        ServerAgency TokIntersect -> pure $ SomeMessage MsgIntersectNotFound
+        _                             -> fail "Invalid protocol state for MsgIntersectNotFound"
+
+      _ -> fail $ "Invalid message tag " <> show tag

marlowe-runtime/src/Language/Marlowe/Protocol/HeaderSync/Server.hs

@@ -0,0 +1,104 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Language.Marlowe.Protocol.HeaderSync.Server
+  where
+
+import Language.Marlowe.Protocol.HeaderSync.Types
+import Language.Marlowe.Runtime.ChainSync.Api (BlockHeader)
+import Language.Marlowe.Runtime.Discovery.Api (ContractHeader)
+import Network.TypedProtocol
+
+newtype MarloweHeaderSyncServer m a = MarloweHeaderSyncServer { runMarloweHeaderSyncServer :: m (ServerStIdle m a) }
+
+data ServerStIdle m a = ServerStIdle
+  { recvMsgRequestNext :: m (ServerStNext m a)
+  , recvMsgIntersect :: [BlockHeader] -> m (ServerStIntersect m a)
+  , recvMsgDone :: m a
+  } deriving Functor
+
+data ServerStIntersect m a where
+  SendMsgIntersectFound :: BlockHeader -> ServerStIdle m a -> ServerStIntersect m a
+  SendMsgIntersectNotFound :: ServerStIdle m a -> ServerStIntersect m a
+
+deriving instance Functor m => Functor (ServerStIntersect m)
+
+data ServerStNext m a where
+  SendMsgNewHeaders :: BlockHeader -> [ContractHeader] -> ServerStIdle m a -> ServerStNext m a
+  SendMsgRollBackward :: BlockHeader -> ServerStIdle m a -> ServerStNext m a
+  SendMsgWait :: ServerStWait m a -> ServerStNext m a
+
+deriving instance Functor m => Functor (ServerStNext m)
+
+data ServerStWait m a = ServerStWait
+  { recvMsgPoll   :: m (ServerStNext m a)
+  , recvMsgCancel :: m (ServerStIdle m a)
+  } deriving Functor
+
+hoistMarloweHeaderSyncServer
+  :: forall m n a
+   . Functor m
+  => (forall x. m x -> n x)
+  -> MarloweHeaderSyncServer m a
+  -> MarloweHeaderSyncServer n a
+hoistMarloweHeaderSyncServer nat = MarloweHeaderSyncServer . nat . fmap hoistIdle . runMarloweHeaderSyncServer
+  where
+    hoistIdle :: ServerStIdle m a -> ServerStIdle n a
+    hoistIdle ServerStIdle{..} = ServerStIdle
+      { recvMsgRequestNext = nat $ fmap hoistNext recvMsgRequestNext
+      , recvMsgIntersect = nat . fmap hoistIntersect . recvMsgIntersect
+      , recvMsgDone = nat recvMsgDone
+      }
+
+    hoistIntersect :: ServerStIntersect m a -> ServerStIntersect n a
+    hoistIntersect = \case
+      SendMsgIntersectFound block idle -> SendMsgIntersectFound block $ hoistIdle idle
+      SendMsgIntersectNotFound idle             -> SendMsgIntersectNotFound $ hoistIdle idle
+
+    hoistNext :: ServerStNext m a -> ServerStNext n a
+    hoistNext = \case
+      SendMsgNewHeaders block headers idle -> SendMsgNewHeaders block headers $ hoistIdle idle
+      SendMsgRollBackward block idle      -> SendMsgRollBackward block $ hoistIdle idle
+      SendMsgWait wait                          -> SendMsgWait $ hoistWait wait
+
+    hoistWait :: ServerStWait m a -> ServerStWait n a
+    hoistWait ServerStWait{..} = ServerStWait
+      { recvMsgPoll = nat $ fmap hoistNext recvMsgPoll
+      , recvMsgCancel = nat $ fmap hoistIdle recvMsgCancel
+      }
+
+marloweHeaderSyncServerPeer :: forall m a. Functor m => MarloweHeaderSyncServer m a -> Peer MarloweHeaderSync 'AsServer 'StIdle m a
+marloweHeaderSyncServerPeer = Effect . fmap peerIdle . runMarloweHeaderSyncServer
+  where
+    peerIdle :: ServerStIdle m a -> Peer MarloweHeaderSync 'AsServer 'StIdle m a
+    peerIdle ServerStIdle{..} = Await (ClientAgency TokIdle) $ Effect . \case
+      MsgDone -> Done TokDone <$> recvMsgDone
+      MsgIntersect blocks -> peerIntersect <$> recvMsgIntersect blocks
+      MsgRequestNext -> peerNext <$> recvMsgRequestNext
+
+    peerIntersect :: ServerStIntersect m a -> Peer MarloweHeaderSync 'AsServer 'StIntersect m a
+    peerIntersect = \case
+      SendMsgIntersectFound block idle ->
+        Yield (ServerAgency TokIntersect) (MsgIntersectFound block) $
+        peerIdle idle
+      SendMsgIntersectNotFound idle ->
+        Yield (ServerAgency TokIntersect) MsgIntersectNotFound $
+        peerIdle idle
+
+    peerNext :: ServerStNext m a -> Peer MarloweHeaderSync 'AsServer 'StNext m a
+    peerNext = \case
+      SendMsgNewHeaders block headers idle ->
+        Yield (ServerAgency TokNext) (MsgNewHeaders block headers) $
+        peerIdle idle
+      SendMsgRollBackward block idle ->
+        Yield (ServerAgency TokNext) (MsgRollBackward block) $
+        peerIdle idle
+      SendMsgWait wait ->
+        Yield (ServerAgency TokNext) MsgWait $
+        peerWait wait
+
+    peerWait :: ServerStWait m a -> Peer MarloweHeaderSync 'AsServer 'StWait m a
+    peerWait ServerStWait{..} = Await (ClientAgency TokWait) $ Effect . \case
+      MsgPoll   -> peerNext <$> recvMsgPoll
+      MsgCancel -> peerIdle <$> recvMsgCancel

marlowe-runtime/src/Language/Marlowe/Protocol/HeaderSync/Types.hs

@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Language.Marlowe.Protocol.HeaderSync.Types
+  where
+
+import Language.Marlowe.Runtime.ChainSync.Api (BlockHeader)
+import Language.Marlowe.Runtime.Discovery.Api (ContractHeader)
+import Network.TypedProtocol (Protocol(..))
+
+data MarloweHeaderSync where
+  StIdle :: MarloweHeaderSync
+  StIntersect :: MarloweHeaderSync
+  StNext :: MarloweHeaderSync
+  StWait :: MarloweHeaderSync
+  StDone :: MarloweHeaderSync
+
+instance Protocol MarloweHeaderSync where
+  data Message MarloweHeaderSync from to where
+    MsgIntersect :: [BlockHeader] -> Message MarloweHeaderSync
+      'StIdle
+      'StIntersect
+    MsgDone :: Message MarloweHeaderSync
+      'StIdle
+      'StDone
+    MsgRequestNext :: Message MarloweHeaderSync
+      'StIdle
+      'StNext
+    MsgNewHeaders :: BlockHeader -> [ContractHeader] -> Message MarloweHeaderSync
+      'StNext
+      'StIdle
+    MsgRollBackward :: BlockHeader -> Message MarloweHeaderSync
+      'StNext
+      'StIdle
+    MsgWait :: Message MarloweHeaderSync
+      'StNext
+      'StWait
+    MsgPoll :: Message MarloweHeaderSync
+      'StWait
+      'StNext
+    MsgCancel :: Message MarloweHeaderSync
+      'StWait
+      'StIdle
+    MsgIntersectFound :: BlockHeader -> Message MarloweHeaderSync
+      'StIntersect
+      'StIdle
+    MsgIntersectNotFound :: Message MarloweHeaderSync
+      'StIntersect
+      'StIdle
+
+  data ClientHasAgency st where
+    TokIdle :: ClientHasAgency 'StIdle
+    TokWait :: ClientHasAgency 'StWait
+
+  data ServerHasAgency st where
+    TokNext :: ServerHasAgency 'StNext
+    TokIntersect :: ServerHasAgency 'StIntersect
+
+  data NobodyHasAgency st where
+    TokDone :: NobodyHasAgency 'StDone
+
+  exclusionLemma_ClientAndServerHaveAgency TokIdle = \case
+  exclusionLemma_ClientAndServerHaveAgency TokWait = \case
+
+  exclusionLemma_NobodyAndClientHaveAgency TokDone = \case
+
+  exclusionLemma_NobodyAndServerHaveAgency TokDone = \case