diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,45 @@ # Revision history for typed-protocols +## 1.2.2.0 -- 2026-08-21 + +### Non-breaking changes + +* Repository moved to https://github.com/IntersectMBO/typed-protocols +* Added `Lookahead`, a dual of `Pipelined`: a peer defers its sends to + background `Sender`s and receives ahead (`AwaitLookahead` / `FlushSender`), + with supporting proofs, drivers, and `Server` pattern synonyms. +* Support `QuickCheck >= 2.18`, `io-classes-1.11`. + +## 1.2.1.0 -- 2026-04-16 + +* Support GHC-9.14, io-classes >=1.8 && < 1.11 + +## 1.2.0.0 -- 2025-02-05 + +* Make `runPeerWithDriver` strict, it evaluates the result and `dstate` to + normal form. + +## 1.1.0.1 -- 2025-10-14 + +* Support QuickCheck <= 2.15 + +## 1.1.0.0 -- 2025-08-03 + +### Breaking changes + +* Annotated codecs which allow to retain original bytes received from the network. + The `Codec` type evolved into a new `CodecF` data type, and two type aliases + `AnnotatedCodec`, `Codec`. +* `prop_codec` properties moved to `typed-protocols:codec-properties` library + (`Network.TypedProtocol.Codec.Properties` module). They now return the + `QuickCheck`'s `Property` rather than a `Bool`. + +### Non-breaking changes + +## 1.0.0.0 + +* Hackage release. + ## 0.3.0.0 * `AnyMessageWithAgency` pattern synonym is exported as a constructor of `AnyMessage`. diff --git a/NOTICE b/NOTICE --- a/NOTICE +++ b/NOTICE @@ -1,4 +1,4 @@ -Copyright 2019-2025 Input Output Global Inc (IOG) +Copyright 2019-2026 Input Output Global Inc (IOG), 2026 Intersect Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -[![Haskell CI](https://img.shields.io/github/actions/workflow/status/input-output-hk/typed-protocols/haskell.yml?branch=main&label=Build&style=for-the-badge)](https://github.com/input-output-hk/typed-protocols/actions/workflows/haskell.yml) -[![handbook](https://img.shields.io/badge/policy-Cardano%20Engineering%20Handbook-informational?style=for-the-badge)](https://input-output-hk.github.io/cardano-engineering-handbook) +[![Haskell CI](https://img.shields.io/github/actions/workflow/status/intersectmbo/typed-protocols/haskell.yml?branch=main&label=Build&style=for-the-badge)](https://github.com/intersectmbo/typed-protocols/actions/workflows/haskell.yml) +[![handbook](https://img.shields.io/badge/policy-Cardano%20Engineering%20Handbook-informational?style=for-the-badge)](https://intersectmbo.github.io/cardano-engineering-handbook) typed-protocols @@ -36,4 +36,4 @@ [typed-protocols-agda]: https://coot.me/agda/posts.agda.typed-protocols.html [coot]: https://github.com/coot [dcoutts]: https://github.com/dcoutts -[haddocks]: https://input-output-hk.github.io/typed-protocols +[haddocks]: https://intersectmbo.github.io/typed-protocols diff --git a/cborg/Network/TypedProtocol/Codec/CBOR.hs b/cborg/Network/TypedProtocol/Codec/CBOR.hs --- a/cborg/Network/TypedProtocol/Codec/CBOR.hs +++ b/cborg/Network/TypedProtocol/Codec/CBOR.hs @@ -25,10 +25,10 @@ import Network.TypedProtocol.Core --- | Construct a 'Codec' for a CBOR based serialisation format, using strict +-- | Construct a 'CodecF' for a CBOR based serialisation format, using strict -- 'BS.ByteString's. -- --- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- This is an adaptor between the @cborg@ library and the 'CodecF' abstraction. -- -- It takes encode and decode functions for the protocol messages that use the -- CBOR library encoder and decoder. @@ -38,7 +38,7 @@ -- natively produces chunks). -- mkCodecCborStrictBS - :: forall ps m. MonadST m + :: forall ps m f. MonadST m => (forall (st :: ps) (st' :: ps). StateTokenI st @@ -49,10 +49,10 @@ -> (forall (st :: ps) s. ActiveState st => StateToken st - -> CBOR.Decoder s (SomeMessage st)) + -> CBOR.Decoder s (f st)) -- ^ cbor decoder - -> Codec ps CBOR.DeserialiseFailure m BS.ByteString + -> CodecF ps CBOR.DeserialiseFailure m f BS.ByteString mkCodecCborStrictBS cborMsgEncode cborMsgDecode = Codec { encode = \msg -> convertCborEncoder cborMsgEncode msg, @@ -65,11 +65,12 @@ . cborEncode convertCborDecoder - :: (forall s. CBOR.Decoder s a) - -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a) + :: (forall s. CBOR.Decoder s (f a)) + -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m (f a)) convertCborDecoder cborDecode = convertCborDecoderBS cborDecode stToIO + convertCborDecoderBS :: forall s m a. Functor m => CBOR.Decoder s a @@ -89,16 +90,16 @@ go (CBOR.Partial k) = DecodePartial (fmap go . liftST . k) --- | Construct a 'Codec' for a CBOR based serialisation format, using lazy +-- | Construct a 'CodecF' for a CBOR based serialisation format, using lazy -- 'BS.ByteString's. -- --- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- This is an adaptor between the @cborg@ library and the 'CodecF' abstraction. -- -- It takes encode and decode functions for the protocol messages that use the -- CBOR library encoder and decoder. -- mkCodecCborLazyBS - :: forall ps m. MonadST m + :: forall ps m f. MonadST m => (forall (st :: ps) (st' :: ps). StateTokenI st @@ -109,10 +110,10 @@ -> (forall (st :: ps) s. ActiveState st => StateToken st - -> CBOR.Decoder s (SomeMessage st)) + -> CBOR.Decoder s (f st)) -- ^ cbor decoder - -> Codec ps CBOR.DeserialiseFailure m LBS.ByteString + -> CodecF ps CBOR.DeserialiseFailure m f LBS.ByteString mkCodecCborLazyBS cborMsgEncode cborMsgDecode = Codec { encode = \msg -> convertCborEncoder cborMsgEncode msg, @@ -126,10 +127,11 @@ . cborEncode convertCborDecoder - :: (forall s. CBOR.Decoder s a) - -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) + :: (forall s. CBOR.Decoder s (f a)) + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m (f a)) convertCborDecoder cborDecode = convertCborDecoderLBS cborDecode stToIO + convertCborDecoderLBS :: forall s m a. Monad m diff --git a/examples/Network/TypedProtocol/Driver/Simple.hs b/examples/Network/TypedProtocol/Driver/Simple.hs --- a/examples/Network/TypedProtocol/Driver/Simple.hs +++ b/examples/Network/TypedProtocol/Driver/Simple.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} -- @UndecidableInstances@ extensions is required for defining @Show@ instance -- of @'TraceSendRecv'@. @@ -14,9 +15,14 @@ , Role (..) -- * Pipelined peers , runPipelinedPeer + -- * Lookahead peers + , runLookaheadPeer + , runLookaheadFixedSenderPeer -- * Connected peers , runConnectedPeers , runConnectedPeersPipelined + , runConnectedPeersLookahead + , runConnectedPeersLookaheadFixedSender , runConnectedPeersAsymmetric -- * Driver utilities -- | This may be useful if you want to write your own driver. @@ -30,6 +36,7 @@ import Network.TypedProtocol.Driver import Network.TypedProtocol.Peer +import Control.DeepSeq (NFData, force) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadThrow import Control.Tracer (Tracer (..), contramap, traceWith) @@ -72,7 +79,11 @@ driverSimple :: forall ps pr failure bytes m. - (MonadThrow m, Exception failure) + ( MonadEvaluate m + , MonadThrow m + , Exception failure + , NFData failure + ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes @@ -119,7 +130,12 @@ -- runPeer :: forall ps (st :: ps) pr failure bytes m a. - (MonadThrow m, Exception failure) + ( MonadEvaluate m + , MonadThrow m + , Exception failure + , NFData failure + , NFData a + ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes @@ -140,7 +156,13 @@ -- runPipelinedPeer :: forall ps (st :: ps) pr failure bytes m a. - (MonadAsync m, MonadThrow m, Exception failure) + ( MonadAsync m + , MonadEvaluate m + , MonadThrow m + , Exception failure + , NFData failure + , NFData a + ) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes @@ -152,23 +174,76 @@ driver = driverSimple tracer codec channel +-- | Run a lookahead 'Peer' with the given 'Channel' and 'Codec'. -- +-- Like pipelined peers, lookahead peers rely on concurrency (the 'Sender's run +-- in parallel with the main peer), hence the 'MonadAsync' constraint. +-- +runLookaheadPeer + :: forall ps (st :: ps) pr failure bytes m a. + ( MonadAsync m + , MonadEvaluate m + , MonadThrow m + , Exception failure + , NFData failure + , NFData a + ) + => Tracer m (TraceSendRecv ps) + -> Codec ps failure m bytes + -> Channel m bytes + -> PeerLookahead ps pr st m a + -> m (a, Maybe bytes) +runLookaheadPeer tracer codec channel peer = + runLookaheadPeerWithDriver driver peer + where + driver = driverSimple tracer codec channel + + +-- | Run a fixed-'Sender' lookahead 'Peer' with the given 'Channel' and 'Codec'. +-- +runLookaheadFixedSenderPeer + :: forall ps (st :: ps) pr failure bytes m a. + ( MonadAsync m + , MonadEvaluate m + , MonadThrow m + , Exception failure + , NFData failure + , NFData a + ) + => Tracer m (TraceSendRecv ps) + -> Codec ps failure m bytes + -> Channel m bytes + -> PeerLookaheadFixedSender ps pr st m a + -> m (a, Maybe bytes) +runLookaheadFixedSenderPeer tracer codec channel peer = + runLookaheadFixedSenderPeerWithDriver driver peer + where + driver = driverSimple tracer codec channel + + +-- -- Utils -- -- | Run a codec incremental decoder 'DecodeStep' against a channel. It also -- takes any extra input data and returns any unused trailing data. -- -runDecoderWithChannel :: Monad m - => Channel m bytes - -> Maybe bytes - -> DecodeStep bytes failure m a - -> m (Either failure (a, Maybe bytes)) +runDecoderWithChannel + :: ( MonadEvaluate m +#if !MIN_VERSION_io_classes(1,10,0) + , Monad m +#endif + , NFData failure + ) + => Channel m bytes + -> Maybe bytes + -> DecodeStep bytes failure m a + -> m (Either failure (a, Maybe bytes)) runDecoderWithChannel Channel{recv} = go where go _ (DecodeDone x trailing) = return (Right (x, trailing)) - go _ (DecodeFail failure) = return (Left failure) + go _ (DecodeFail failure) = Left <$> evaluate (force failure) go Nothing (DecodePartial k) = recv >>= k >>= go Nothing go (Just trailing) (DecodePartial k) = k (Just trailing) >>= go Nothing @@ -183,8 +258,14 @@ -- The first argument is expected to create two channels that are connected, -- for example 'createConnectedChannels'. -- -runConnectedPeers :: (MonadAsync m, MonadCatch m, - Exception failure) +runConnectedPeers :: ( MonadAsync m + , MonadCatch m + , MonadEvaluate m + , Exception failure + , NFData failure + , NFData a + , NFData b + ) => m (Channel m bytes, Channel m bytes) -> Tracer m (Role, TraceSendRecv ps) -> Codec ps failure m bytes @@ -201,8 +282,14 @@ tracerClient = contramap ((,) Client) tracer tracerServer = contramap ((,) Server) tracer -runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m, - Exception failure) +runConnectedPeersPipelined :: ( MonadAsync m + , MonadCatch m + , MonadEvaluate m + , Exception failure + , NFData failure + , NFData a + , NFData b + ) => m (Channel m bytes, Channel m bytes) -> Tracer m (PeerRole, TraceSendRecv ps) -> Codec ps failure m bytes @@ -220,13 +307,76 @@ tracerServer = contramap ((,) AsServer) tracer +-- | Run a pipelined client against a lookahead server over a pair of connected +-- 'Channel's. Both rely on concurrency — the client's receivers and the +-- server's 'Sender's each run in parallel with their main thread — so this is +-- where the interleavings lookahead exploits actually occur (unlike @connect@, +-- which forgets them). +-- +runConnectedPeersLookahead :: ( MonadAsync m + , MonadCatch m + , MonadEvaluate m + , Exception failure + , NFData failure + , NFData a + , NFData b + ) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (PeerRole, TraceSendRecv ps) + -> Codec ps failure m bytes + -> PeerPipelined ps pr st m a + -> PeerLookahead ps (FlipAgency pr) st m b + -> m (a, b) +runConnectedPeersLookahead createChannels tracer codec client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runLookaheadPeer tracerServer codec serverChannel server) + where + tracerClient = contramap ((,) AsClient) tracer + tracerServer = contramap ((,) AsServer) tracer + + +-- | As 'runConnectedPeersLookahead', but the server is a fixed-'Sender' +-- lookahead peer run via 'runLookaheadFixedSenderPeer'. +-- +runConnectedPeersLookaheadFixedSender :: ( MonadAsync m + , MonadCatch m + , MonadEvaluate m + , Exception failure + , NFData failure + , NFData a + , NFData b + ) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (PeerRole, TraceSendRecv ps) + -> Codec ps failure m bytes + -> PeerPipelined ps pr st m a + -> PeerLookaheadFixedSender ps (FlipAgency pr) st m b + -> m (a, b) +runConnectedPeersLookaheadFixedSender createChannels tracer codec client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runLookaheadFixedSenderPeer tracerServer codec serverChannel server) + where + tracerClient = contramap ((,) AsClient) tracer + tracerServer = contramap ((,) AsServer) tracer + + -- Run the same protocol with different codes. This is useful for testing -- 'Handshake' protocol which knows how to decode different versions. -- runConnectedPeersAsymmetric :: ( MonadAsync m + , MonadEvaluate m , MonadMask m , Exception failure + , NFData failure + , NFData a + , NFData b ) => m (Channel m bytes, Channel m bytes) -> Tracer m (Role, TraceSendRecv ps) diff --git a/examples/Network/TypedProtocol/PingPong/Codec.hs b/examples/Network/TypedProtocol/PingPong/Codec.hs --- a/examples/Network/TypedProtocol/PingPong/Codec.hs +++ b/examples/Network/TypedProtocol/PingPong/Codec.hs @@ -31,6 +31,8 @@ DecodeDone (SomeMessage MsgPing) trailing (SingIdle, "done") -> DecodeDone (SomeMessage MsgDone) trailing + (SingDone, _) -> + notActiveState stok (_ , _ ) -> DecodeFail failure where failure = CodecFailure ("unexpected server message: " ++ str) diff --git a/examples/Network/TypedProtocol/ReqResp/Codec.hs b/examples/Network/TypedProtocol/ReqResp/Codec.hs --- a/examples/Network/TypedProtocol/ReqResp/Codec.hs +++ b/examples/Network/TypedProtocol/ReqResp/Codec.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE BlockArguments #-} + module Network.TypedProtocol.ReqResp.Codec where import Network.TypedProtocol.Codec @@ -38,11 +40,77 @@ (SingBusy, ("MsgResp", str')) | Just resp <- readMaybe str' -> DecodeDone (SomeMessage (MsgResp resp)) trailing + (SingDone, _) -> + notActiveState stok (_ , _ ) -> DecodeFail failure where failure = CodecFailure ("unexpected server message: " ++ str) +data WithBytes a = WithBytes { + bytes :: String, + message :: a + } + deriving (Show, Eq) + +mkWithBytes :: Show a => a -> WithBytes a +mkWithBytes message = WithBytes { bytes = show message, message } + + +anncodecReqResp :: + forall req resp m + . (Monad m, Show req, Show resp, Read req, Read resp) + => AnnotatedCodec (ReqResp (WithBytes req) (WithBytes resp)) CodecFailure m String +anncodecReqResp = + Codec{encode, decode} + where + encode :: forall req' resp' + (st :: ReqResp (WithBytes req') (WithBytes resp')) + (st' :: ReqResp (WithBytes req') (WithBytes resp')) + . ( Show req' + , Show resp' + ) + => Message (ReqResp (WithBytes req') (WithBytes resp')) st st' + -> String + -- NOTE: we're not using 'Show (Message ...)' instance. If `req ~ Int`, + -- then negative numbers will be surrounded with braces (e.g. @"(-1)"@) and + -- the `Read` type class doesn't have a way to see that brackets were consumed + -- from the input string. + encode (MsgReq WithBytes { message }) + = "MsgReq " ++ show message ++ "\n" + encode (MsgResp WithBytes { message }) + = "MsgResp " ++ show message ++ "\n" + encode MsgDone + = "MsgDone" ++ "\n" + + decode :: forall req' resp' m' + (st :: ReqResp (WithBytes req') (WithBytes resp')) + . (Monad m', Read req', Read resp', ActiveState st) + => StateToken st + -> m' (DecodeStep String CodecFailure m' (Annotator String st)) + decode stok = + decodeTerminatedFrame '\n' $ \str trailing -> + case (stok, break (==' ') str) of + (SingIdle, ("MsgReq", str')) + | Just req <- readMaybe @req' str' + -> DecodeDone (Annotator \str'' -> + let used = init $ drop 7 str'' in + SomeMessage (MsgReq (WithBytes used req))) trailing + (SingIdle, ("MsgDone", "")) + -> DecodeDone (Annotator \_str'' -> SomeMessage MsgDone) trailing + (SingBusy, ("MsgResp", str')) + | Just resp <- readMaybe @resp' str' + -> DecodeDone (Annotator \str'' -> + let used = init $ drop 8 str'' in + SomeMessage (MsgResp (WithBytes used resp))) trailing + (SingDone, _) -> + notActiveState stok + + (_ , _ ) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + + codecReqRespId :: forall req resp m . (Monad m, Show req, Show resp) @@ -81,5 +149,5 @@ (SingBusy, _) -> DecodeFail failure where failure = CodecFailure ("unexpected server message: " ++ show msg) - - (a@SingDone, _) -> notActiveState a + (SingDone, _) -> + notActiveState stok diff --git a/examples/Network/TypedProtocol/ReqResp/Server.hs b/examples/Network/TypedProtocol/ReqResp/Server.hs --- a/examples/Network/TypedProtocol/ReqResp/Server.hs +++ b/examples/Network/TypedProtocol/ReqResp/Server.hs @@ -6,6 +6,7 @@ import Network.TypedProtocol.Core import Network.TypedProtocol.Peer.Server +import Network.TypedProtocol.Proofs (embedLookaheadUsingFixedSender) import Network.TypedProtocol.ReqResp.Type @@ -45,3 +46,58 @@ MsgReq req -> Effect $ do (resp, next) <- recvMsgReq req pure $ Yield (MsgResp resp) (reqRespServerPeer next) + + +-- | A lookahead 'ReqResp' server (the dual of a pipelined client). +-- +-- It is exactly 'reqRespServerPeerLookaheadFixedSender' with its single +-- 'Sender' plugged in at each 'AwaitLookahead' (via +-- 'embedLookaheadUsingFixedSender'), so the two never drift apart. +-- +reqRespServerPeerLookahead + :: forall resp m. Functor m + => m resp + -- ^ produce (and record) the next reply + -> ServerLookahead (ReqResp () resp) StIdle m () +reqRespServerPeerLookahead = + embedLookaheadUsingFixedSender . reqRespServerPeerLookaheadFixedSender + + +-- | A lookahead 'ReqResp' server that receives requests ahead of sending their +-- replies: each 'AwaitLookahead' hands the reply to the /previous/ request off +-- to the sender thread (via 'TheSender', the one 'Sender' carried by the +-- 'ServerLookaheadFixedSender' wrapper — it runs @nextResp@, which typically +-- reads and advances some state), while immediately awaiting the next request. +-- The request payload is ignored (hence @()@); replies come solely from +-- @nextResp@. This is the peer that +-- 'Network.TypedProtocol.Driver.runLookaheadFixedSenderPeerWithDriver' runs. +-- +reqRespServerPeerLookaheadFixedSender + :: forall resp m. Functor m + => m resp + -- ^ produce (and record) the next reply + -> ServerLookaheadFixedSender (ReqResp () resp) StIdle m () +reqRespServerPeerLookaheadFixedSender nextResp = + ServerLookaheadFixedSender sender start + where + sender :: Sender (ReqResp () resp) VariableSender StBusy StIdle m + sender = SenderEffect $ + (\resp -> SenderYield (MsgResp resp) SenderDone) <$> nextResp + + start :: Server (ReqResp () resp) (Lookahead Z (FixedSender StBusy StIdle)) StIdle m () + start = Await $ \msg -> case msg of + MsgReq _ -> busy Zero + MsgDone -> Done () + + busy :: forall n. + Nat n + -> Server (ReqResp () resp) (Lookahead n (FixedSender StBusy StIdle)) StBusy m () + busy n = AwaitLookahead TheSender $ \msg -> case msg of + MsgReq _ -> busy (Succ n) + MsgDone -> drain (Succ n) + + drain :: forall n. + Nat n + -> Server (ReqResp () resp) (Lookahead n (FixedSender StBusy StIdle)) StDone m () + drain Zero = Done () + drain (Succ n') = FlushSender Nothing (drain n') diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs --- a/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs @@ -36,8 +36,7 @@ encode (StateBusy req) (MsgResp resp) = "MsgResp " ++ encodeResp req resp ++ "\n" decode :: forall (st :: ReqResp req). - ActiveState st - => StateToken st + StateToken st -> State st -> m (DecodeStep String CodecFailure m (SomeMessage st)) decode stok state = diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs --- a/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs @@ -88,6 +88,6 @@ WriteFile :: FilePath -> String -> FileAPI () -- write to a file --- TODO: input-output-hk/typed-protocols#57 +-- TODO: intersectmbo/typed-protocols#57 type FileRPC = ReqResp FileAPI diff --git a/properties/Network/TypedProtocol/Codec/Properties.hs b/properties/Network/TypedProtocol/Codec/Properties.hs new file mode 100644 --- /dev/null +++ b/properties/Network/TypedProtocol/Codec/Properties.hs @@ -0,0 +1,573 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module Network.TypedProtocol.Codec.Properties + ( -- * Codec Properties + prop_codecM + , prop_codec + , prop_codec_splitsM + , prop_codec_splits + , prop_codec_binary_compatM + , prop_codec_binary_compat + , prop_codecs_compatM + , prop_codecs_compat + -- ** AnnotatedCodec Properties + , prop_anncodecM + , prop_anncodec + , prop_anncodec_splitsM + , prop_anncodec_splits + , prop_anncodec_binary_compatM + , prop_anncodec_binary_compat + , prop_anncodecs_compatM + , prop_anncodecs_compat + -- ** CodecF Properties + , prop_codecFM + , prop_codecF + , prop_codecF_splitsM + , prop_codecF_splits + , prop_codecF_binary_compatM + , prop_codecF_binary_compat + , prop_codecsF_compatM + , prop_codecsF_compat + -- * Re-exports + , AnyMessage (..) + , SomeState (..) + ) where + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core + +import Test.QuickCheck +#if !MIN_VERSION_QuickCheck(2,16,0) +import Test.QuickCheck.Monoids.Compat +#endif + + +-- | The 'CodecF' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecFM + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -- ^ extract message from the functor + -> CodecF ps failure m f bytes + -- ^ annotated codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_codecFM runF Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do + let bytes = encode msg + r <- decode stateToken >>= runDecoder [bytes] + return $ case r :: Either failure (f st) of + Right f -> case runF f bytes of + SomeMessage msg' -> + AnyMessage msg' === AnyMessage msg + Left err -> counterexample (show err) False + + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => Codec ps failure m bytes + -- ^ codec + -> AnyMessage ps + -- ^ some message + -> m Property + -- ^ returns 'True' iff round trip returns the exact same message +prop_codecM = prop_codecFM const + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_anncodecM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => AnnotatedCodec ps failure m bytes + -- ^ annotated codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_anncodecM = prop_codecFM runAnnotator + + +-- | The 'CodecF' round-trip property in a pure monad. +-- +prop_codecF + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Property +prop_codecF runF runM codec msg = runM (prop_codecFM runF codec msg) + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_codec + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => (forall a. m a -> a) + -> Codec ps failure m bytes + -> AnyMessage ps + -> Property +prop_codec = prop_codecF const + + +-- | The 'Codec' round-trip property in a pure monad. +-- +-- NOTE: when a message is annotated with bytes (e.g. `WithBytes` in +-- `Network.TypedProtocol.ReqResp.Codec.anncodecReqResp`), this property will +-- assess that the decoded bytes are equal to the supplied bytes with +-- `msg :: AnyMessage ps`. It is important to use the bytes in `WithBytes` when +-- encoding the `msg`. Verifying this property is especially important if the +-- bytes are used to check a cryptographic signature, when the exact same bytes +-- received from the network must be used. +-- +prop_anncodec + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodec = prop_codecF runAnnotator + + +-- | A more general version of 'prop_codec_splitsM' for 'CodecF'. +-- +prop_codecF_splitsM + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> m Property +prop_codecF_splitsM runF splits + Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do + property . foldMap Every <$> sequence + [ do r <- decode stateToken >>= runDecoder bytes' + case r :: Either failure (f st) of + Right f -> case runF f (mconcat bytes') of + SomeMessage msg' -> + return $! AnyMessage msg' === AnyMessage msg + Left err -> return $ counterexample (show err) False + + | let bytes = encode msg + , bytes' <- splits bytes ] + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> Codec ps failure m bytes + -> AnyMessage ps + -> m Property +prop_codec_splitsM = prop_codecF_splitsM const + +-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'. +-- +prop_anncodec_splitsM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> m Property +prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator + + +-- | A more general version of 'prop_codec_splits' for 'CodecF'. +-- +prop_codecF_splits + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Property +prop_codecF_splits runF splits runM codec msg = + runM $ prop_codecF_splitsM runF splits codec msg + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> Codec ps failure m bytes + -> AnyMessage ps + -> Property +prop_codec_splits = prop_codecF_splits const + +-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'. +prop_anncodec_splits + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodec_splits = prop_codecF_splits runAnnotator + +-- | A more general version of 'prop_codec_binary_compatM' for 'CodecF'. +-- +prop_codecF_binary_compatM + :: forall psA psB failure m fA fB bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall (st :: psA). fA st -> bytes -> SomeMessage st) + -> (forall (st :: psB). fB st -> bytes -> SomeMessage st) + -> CodecF psA failure m fA bytes + -> CodecF psB failure m fB bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_codecF_binary_compatM + runFA runFB codecA codecB stokEq + (AnyMessage (msgA :: Message psA stA stA')) = + let stokA :: StateToken stA + stokA = stateToken + in case stokEq stokA of + SomeState (stokB :: StateToken stB) -> do + -- 1. + let bytesA = encode codecA msgA + -- 2. + r1 <- decode codecB stokB >>= runDecoder [bytesA] + case r1 :: Either failure (fB stB) of + Left err -> return $ counterexample (show err) False + Right fB -> + case runFB fB bytesA of + (SomeMessage msgB) -> do + -- 3. + let bytesB = encode codecB msgB + -- 4. + r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB] + case r2 :: Either failure (fA stA) of + Left err -> return $ counterexample (show err) False + Right fA -> + case runFA fA bytesB of + SomeMessage msgA' -> return $ AnyMessage msgA' === AnyMessage msgA + +-- | Binary compatibility of two protocols +-- +-- We check the following property: +-- +-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@. +-- +-- 2. When we decode those @bytes@ using codec B, we get a message of protocol +-- @ps@B. +-- +-- 3. When we encode that message again using codec B, we get @bytes@. +-- +-- 4. When we decode those @bytes@ using codec A, we get the original message +-- again. +prop_codec_binary_compatM + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_codec_binary_compatM = prop_codecF_binary_compatM const const + + +-- | A version of 'prop_codec_binary_compatM' for 'AnnotatedCodec'. +-- +prop_anncodec_binary_compatM + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => AnnotatedCodec psA failure m bytes + -> AnnotatedCodec psB failure m bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_anncodec_binary_compatM = prop_codecF_binary_compatM runAnnotator runAnnotator + + +-- | A more general version of 'prop_codec_binary_compat' for 'CodecF'. +-- +prop_codecF_binary_compat + :: forall psA psB failure m fA fB bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall (st :: psA). fA st -> bytes -> SomeMessage st) + -> (forall (st :: psB). fB st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF psA failure m fA bytes + -> CodecF psB failure m fB bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_codecF_binary_compat runFA runFB runM codecA codecB stokEq msg = + runM $ prop_codecF_binary_compatM runFA runFB codecA codecB stokEq msg + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_binary_compat + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall a. m a -> a) + -> Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_codec_binary_compat = + prop_codecF_binary_compat const const + +-- | A 'prop_codec_binary_compat' version for 'AnnotatedCodec'. +-- +prop_anncodec_binary_compat + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall a. m a -> a) + -> AnnotatedCodec psA failure m bytes + -> AnnotatedCodec psB failure m bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_anncodec_binary_compat runM codecA codecB stokEq msgA = + runM $ prop_anncodec_binary_compatM codecA codecB stokEq msgA + + +-- | A more general version of 'prop_codecs_compatM' for 'CodecF'. +-- +prop_codecsF_compatM + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> CodecF ps failure m f bytes + -- ^ first codec + -> CodecF ps failure m f bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_codecsF_compatM runF codecA codecB + (AnyMessage (msg :: Message ps st st')) = + + property + <$> do let bytes = encode codecA msg + r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [bytes] + case r :: Either failure (f st) of + Right f -> case runF f bytes of + SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg + Left err -> return $! Every $ counterexample (show err) False + + <> do let bytes = encode codecB msg + r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [bytes] + case r :: Either failure (f st) of + Right f -> case runF f bytes of + SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg + Left err -> return $! Every $ counterexample (show err) False + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => Codec ps failure m bytes + -- ^ first codec + -> Codec ps failure m bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_codecs_compatM = prop_codecsF_compatM const + +-- | A version of 'prop_codec_compatM' for 'AnnotatedCodec'. +-- +prop_anncodecs_compatM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => AnnotatedCodec ps failure m bytes + -- ^ first codec + -> AnnotatedCodec ps failure m bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_anncodecs_compatM = prop_codecsF_compatM runAnnotator + + +-- | A more general version of 'prop_codecs_compat' for 'CodecF'. +-- +prop_codecsF_compat + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Property +prop_codecsF_compat runF runM codecA codecB msg = + runM $ prop_codecsF_compatM runF codecA codecB msg + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> Codec ps failure m bytes + -> Codec ps failure m bytes + -> AnyMessage ps + -> Property +prop_codecs_compat = prop_codecsF_compat const + +-- | A version of 'prop_codecs_compat' for 'AnnotatedCodec'. +-- +prop_anncodecs_compat + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodecs_compat = prop_codecsF_compat runAnnotator diff --git a/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs b/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs new file mode 100644 --- /dev/null +++ b/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs @@ -0,0 +1,154 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module Network.TypedProtocol.Stateful.Codec.Properties + ( prop_codecM + , prop_codec + , prop_codec_splitsM + , prop_codec_splits + , prop_codecs_compatM + , prop_codecs_compat + ) where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Codec + +import Test.QuickCheck +#if !MIN_VERSION_QuickCheck(2,16,0) +import Test.QuickCheck.Monoids.Compat +#endif + + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' === a + Left err -> return $ counterexample (show err) False + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_codec + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codec runM codec msg = + runM (prop_codecM codec msg) + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codec_splitsM splits + Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + property . foldMap Every <$> sequence + [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' === a + Left err -> return $ counterexample (show err) False + + | let bytes = encode f msg + , bytes' <- splits bytes ] + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (bytes -> [[bytes]]) + -> (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codec_splits splits runM codec msg = + runM $ prop_codec_splitsM splits codec msg + + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + , Show failure + ) + => Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codecs_compatM codecA codecB + a@(AnyMessage f (msg :: Message ps st st')) = + property + <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' === a + Left err -> return $ Every $ counterexample (show err) False + <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' == a + Left _ -> return $ Every False + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + , Show failure + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codecs_compat run codecA codecB msg = + run $ prop_codecs_compatM codecA codecB msg diff --git a/properties/Test/QuickCheck/Monoids/Compat.hs b/properties/Test/QuickCheck/Monoids/Compat.hs new file mode 100644 --- /dev/null +++ b/properties/Test/QuickCheck/Monoids/Compat.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE PatternSynonyms #-} + +-- | Monoids using `.&&.` and `.||.`. +-- +-- They satisfy monoid laws with respect to the `isSuccess` unless one is using +-- `checkCoverage` (see test for a counterexample). +-- +module Test.QuickCheck.Monoids.Compat +#if !MIN_VERSION_QuickCheck(2,16,0) + ( type Every + , All(Every, getEvery, ..) + , type Some + , Any(Some, getSome, ..) +#else + ( All (..) + , Any (..) + , Every (..) + , Some (..) +#endif + ) where + +import Data.List.NonEmpty as NonEmpty +import Data.Semigroup (Semigroup (..)) +import Test.QuickCheck + +-- | Conjunction monoid build with `.&&.`. +-- +-- Use `property @All` as an accessor which doesn't leak +-- existential variables. +-- +data All = forall p. Testable p => All { getAll :: p } + +#if !MIN_VERSION_QuickCheck(2,16,0) +type Every = All + +pattern Every :: () + => Testable p + => p + -> All +pattern Every { getEvery } = All getEvery +#endif + +instance Testable All where + property (All p) = property p + +instance Semigroup All where + All p <> All p' = All (p .&&. p') + sconcat = All . conjoin . NonEmpty.toList + +instance Monoid All where + mempty = All True + mconcat = All . conjoin + + +-- | Disjunction monoid build with `.||.`. +-- +-- Use `property @Any` as an accessor which doesn't leak +-- existential variables. +-- +data Any = forall p. Testable p => Any { getAny :: p } + +#if !MIN_VERSION_QuickCheck(2,16,0) +type Some = Any + +pattern Some :: () + => Testable p + => p + -> Any +pattern Some { getSome } = Any getSome +#endif + +instance Testable Any where + property (Any p) = property p + +instance Semigroup Any where + Any p <> Any p' = Any (p .||. p') + sconcat = Any . disjoin . NonEmpty.toList + +instance Monoid Any where + mempty = Any False + mconcat = Any . disjoin diff --git a/src/Network/TypedProtocol/Codec.hs b/src/Network/TypedProtocol/Codec.hs --- a/src/Network/TypedProtocol/Codec.hs +++ b/src/Network/TypedProtocol/Codec.hs @@ -8,7 +8,12 @@ module Network.TypedProtocol.Codec ( -- * Defining and using Codecs -- ** Codec type - Codec (..) + CodecF (..) + , Codec + , Annotator (..) + , AnnotatedCodec + , hoistAnnotation + , unAnnotateCodec , hoistCodec , isoCodec , mapFailureCodec @@ -36,21 +41,15 @@ -- * CodecFailure , CodecFailure (..) -- * Testing codec properties + -- ** Codec , AnyMessage (AnyMessage, AnyMessageAndAgency) - , prop_codecM - , prop_codec - , prop_codec_splitsM - , prop_codec_splits - , prop_codec_binary_compatM - , prop_codec_binary_compat - , prop_codecs_compatM - , prop_codecs_compat + -- ** SomeState , SomeState (..) ) where +import Control.DeepSeq (NFData (..)) import Control.Exception (Exception) import Data.Kind (Type) -import Data.Monoid (All (..)) import Network.TypedProtocol.Core import Network.TypedProtocol.Driver (SomeMessage (..)) @@ -66,10 +65,21 @@ -- * The protocol -- * the type of decoding failures -- * the monad in which the decoder runs --- * the type of the encoded data (typically strings or bytes) +-- * a functor which wraps the decoder result, e.g. `SomeMessage` or `Annotator`. +-- * the type of the encoded data (typically strings or bytes, or +-- `AnyMessage` for testing purposes with no codec overhead). -- -- A codec consists of a message encoder and a decoder. -- +-- The `CodecF` type comes with two useful type aliases: +-- * `Codec` - which can decode protocol messages +-- * `AnnotatedCodec` - which also has access to bytes which were fed to the +-- codec when decoding a message. +-- +-- `AnnotatedCodec` is useful if one wants to decode data structures and retain +-- their CBOR encoding (`decodeWithByteSpan` from `cborg` can be used for that +-- purpose). +-- -- The encoder is supplied both with the message to encode and the current -- protocol state (matching the message). The protocol state can be either -- a client or server state, but for either peer role it is a protocol state @@ -123,31 +133,77 @@ -- This toy example format uses newlines @\n@ as a framing format. See -- 'DecodeStep' for suggestions on how to use it for more realistic formats. -- -data Codec ps failure m bytes = Codec { +data CodecF ps failure m (f :: ps -> Type) bytes = Codec { encode :: forall (st :: ps) (st' :: ps). StateTokenI st => ActiveState st - -- evidence that the state 'st' is active => Message ps st st' - -- message to encode -> bytes, + -- ^ encode a message into `bytes` decode :: forall (st :: ps). ActiveState st => StateToken st -- evidence for an active state - -> m (DecodeStep bytes failure m (SomeMessage st)) + -> m (DecodeStep bytes failure m (f st)) + -- ^ decode a message knowing that the current state is `st` } --- TODO: input-output-hk/typed-protocols#57 -- | Change functor in which the codec is running. -- +-- | The type of a standard `Codec` for `typed-protocols`. +-- +type Codec ps failure m bytes = CodecF ps failure m SomeMessage bytes + +-- | A continuation for a decoder which is fed with whole bytes that were used +-- to parse the message. +-- +newtype Annotator bytes st = Annotator { runAnnotator :: bytes -> SomeMessage st } + +-- | Codec which has access to bytes received from the network to annotate +-- decoded structure. +-- +-- AnnotatedCodec works in two stages. First it is decoding the structure as +-- bytes are received from the network, like a `Codec` does. The codec returns +-- a continuation `Annotator` which is fed with all bytes used to parse the +-- message. It is the driver which is responsible for passing bytes which were +-- fed to the incremental codec. +-- +type AnnotatedCodec ps failure m bytes = CodecF ps failure m (Annotator bytes) bytes + + +-- | Transform annotation. +-- +hoistAnnotation :: forall ps failure m f g bytes. + Functor m + => (forall st. f st -> g st) + -> CodecF ps failure m f bytes + -> CodecF ps failure m g bytes +hoistAnnotation nat codec@Codec { decode } = codec { decode = decode' } + where + decode' :: forall (st :: ps). + ActiveState st + => StateToken st + -> m (DecodeStep bytes failure m (g st)) + decode' tok = fmap nat <$> decode tok + + +-- | Remove annotation. It is only safe if the `Annotator` treats empty input +-- in a safe way. +-- +unAnnotateCodec :: forall ps failure m bytes. + (Functor m, Monoid bytes) + => AnnotatedCodec ps failure m bytes + -> Codec ps failure m bytes +unAnnotateCodec = hoistAnnotation (($ mempty) . runAnnotator) + + hoistCodec :: ( Functor n ) => (forall x . m x -> n x) -- ^ a natural transformation - -> Codec ps failure m bytes - -> Codec ps failure n bytes + -> CodecF ps failure m f bytes + -> CodecF ps failure n f bytes hoistCodec nat codec = codec { decode = fmap (hoistDecodeStep nat) . nat . decode codec } @@ -159,9 +215,9 @@ -- ^ map from 'bytes' to `bytes'` -> (bytes' -> bytes) -- ^ its inverse - -> Codec ps failure m bytes + -> CodecF ps failure m f bytes -- ^ codec - -> Codec ps failure m bytes' + -> CodecF ps failure m f bytes' isoCodec f finv Codec {encode, decode} = Codec { encode = \msg -> f $ encode msg, decode = \tok -> isoDecodeStep f finv <$> decode tok @@ -173,8 +229,8 @@ :: Functor m => (failure -> failure') -- ^ a function to apply to failure - -> Codec ps failure m bytes - -> Codec ps failure' m bytes + -> CodecF ps failure m f bytes + -> CodecF ps failure' m f bytes mapFailureCodec f Codec {encode, decode} = Codec { encode = encode, decode = \tok -> mapFailureDecodeStep f <$> decode tok @@ -207,9 +263,11 @@ -- @'fail'@ or was not provided enough input. | DecodeFail failure +deriving instance Functor m => Functor (DecodeStep bytes failure m) -- | Change bytes of 'DecodeStep'. -- + isoDecodeStep :: Functor m => (bytes -> bytes') @@ -259,6 +317,10 @@ | CodecFailure String deriving (Eq, Show) +instance NFData CodecFailure where + rnf CodecFailureOutOfInput = () + rnf (CodecFailure failure) = rnf failure + -- safe instance with @UndecidableInstances@ in scope instance Exception CodecFailure @@ -322,8 +384,10 @@ -- requires @UndecidableInstances@ and @QuantifiedConstraints@. instance (forall (st :: ps) (st' :: ps). Show (Message ps st st')) => Show (AnyMessage ps) where - show (AnyMessage (msg :: Message ps st st')) = - "AnyMessage " ++ show msg + showsPrec d (AnyMessage (msg :: Message ps st st')) = + showParen (d > app_prec) (showString "AnyMessage " . showsPrec (app_prec + 1) msg) + where + app_prec = 10 -- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the @@ -346,85 +410,6 @@ getAgency msg = (msg, stateToken) --- | The 'Codec' round-trip property: decode after encode gives the same --- message. Every codec must satisfy this property. --- -prop_codecM - :: forall ps failure m bytes. - ( Monad m - , Eq (AnyMessage ps) - ) - => Codec ps failure m bytes - -- ^ codec - -> AnyMessage ps - -- ^ some message - -> m Bool - -- ^ returns 'True' iff round trip returns the exact same message -prop_codecM Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do - r <- decode stateToken >>= runDecoder [encode msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ AnyMessage msg' == AnyMessage msg - Left _ -> return False - --- | The 'Codec' round-trip property in a pure monad. --- -prop_codec - :: forall ps failure m bytes. - (Monad m, Eq (AnyMessage ps)) - => (forall a. m a -> a) - -> Codec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_codec runM codec msg = - runM (prop_codecM codec msg) - - --- | A variant on the codec round-trip property: given the encoding of a --- message, check that decode always gives the same result irrespective --- of how the chunks of input are fed to the incremental decoder. --- --- This property guards against boundary errors in incremental decoders. --- It is not necessary to check this for every message type, just for each --- generic codec construction. For example given some binary serialisation --- library one would write a generic adaptor to the codec interface. This --- adaptor has to deal with the incremental decoding and this is what needs --- to be checked. --- -prop_codec_splitsM - :: forall ps failure m bytes. - (Monad m, Eq (AnyMessage ps)) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> Codec ps failure m bytes - -> AnyMessage ps - -> m Bool -prop_codec_splitsM splits - Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do - and <$> sequence - [ do r <- decode stateToken >>= runDecoder bytes' - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $! AnyMessage msg' == AnyMessage msg - Left _ -> return False - - | let bytes = encode msg - , bytes' <- splits bytes ] - - --- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codec_splits - :: forall ps failure m bytes. - (Monad m, Eq (AnyMessage ps)) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> (forall a. m a -> a) - -> Codec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_codec_splits splits runM codec msg = - runM $ prop_codec_splitsM splits codec msg - - -- | Auxiliary definition for 'prop_codec_binary_compatM'. -- -- Used for the existential @st :: ps@ parameter when expressing that for each @@ -437,110 +422,3 @@ => StateToken st -- ^ state token for some active state 'st' -> SomeState ps - --- | Binary compatibility of two protocols --- --- We check the following property: --- --- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@. --- --- 2. When we decode those @bytes@ using codec B, we get a message of protocol --- @ps@B. --- --- 3. When we encode that message again using codec B, we get @bytes@. --- --- 4. When we decode those @bytes@ using codec A, we get the original message --- again. -prop_codec_binary_compatM - :: forall psA psB failure m bytes. - ( Monad m - , Eq (AnyMessage psA) - ) - => Codec psA failure m bytes - -> Codec psB failure m bytes - -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) - -- ^ the states of A map directly to states of B. - -> AnyMessage psA - -> m Bool -prop_codec_binary_compatM - codecA codecB stokEq - (AnyMessage (msgA :: Message psA stA stA')) = - let stokA :: StateToken stA - stokA = stateToken - in case stokEq stokA of - SomeState (stokB :: StateToken stB) -> do - -- 1. - let bytesA = encode codecA msgA - -- 2. - r1 <- decode codecB stokB >>= runDecoder [bytesA] - case r1 :: Either failure (SomeMessage stB) of - Left _ -> return False - Right (SomeMessage msgB) -> do - -- 3. - let bytesB = encode codecB msgB - -- 4. - r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB] - case r2 :: Either failure (SomeMessage stA) of - Left _ -> return False - Right (SomeMessage msgA') -> return $ AnyMessage msgA' == AnyMessage msgA - --- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. -prop_codec_binary_compat - :: forall psA psB failure m bytes. - ( Monad m - , Eq (AnyMessage psA) - ) - => (forall a. m a -> a) - -> Codec psA failure m bytes - -> Codec psB failure m bytes - -> (forall (stA :: psA). StateToken stA -> SomeState psB) - -- ^ the states of A map directly to states of B. - -> AnyMessage psA - -> Bool -prop_codec_binary_compat runM codecA codecB stokEq msgA = - runM $ prop_codec_binary_compatM codecA codecB stokEq msgA - - --- | Compatibility between two codecs of the same protocol. Encode a message --- with one codec and decode it with the other one, then compare if the result --- is the same as initial message. --- -prop_codecs_compatM - :: forall ps failure m bytes. - ( Monad m - , Eq (AnyMessage ps) - , forall a. Monoid a => Monoid (m a) - ) - => Codec ps failure m bytes - -- ^ first codec - -> Codec ps failure m bytes - -- ^ second codec - -> AnyMessage ps - -- ^ some message - -> m Bool -prop_codecs_compatM codecA codecB - (AnyMessage (msg :: Message ps st st')) = - getAll <$> do r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [encode codecA msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg - Left _ -> return $! All False - <> do r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [encode codecB msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg - Left _ -> return $! All False - --- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codecs_compat - :: forall ps failure m bytes. - ( Monad m - , Eq (AnyMessage ps) - , forall a. Monoid a => Monoid (m a) - ) - => (forall a. m a -> a) - -> Codec ps failure m bytes - -> Codec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_codecs_compat run codecA codecB msg = - run $ prop_codecs_compatM codecA codecB msg diff --git a/src/Network/TypedProtocol/Core.hs b/src/Network/TypedProtocol/Core.hs --- a/src/Network/TypedProtocol/Core.hs +++ b/src/Network/TypedProtocol/Core.hs @@ -42,8 +42,10 @@ -- ** Pipelining -- *** IsPipelined , IsPipelined (..) + , SenderVariability (..) -- *** Outstanding , Outstanding + , OutstandingSenders -- *** N and Nat , N (..) , Nat (Succ, Zero) @@ -272,7 +274,7 @@ TheyHaveAgency :: RelativeAgency -- evidence of protocol termination NobodyHasAgency :: RelativeAgency --- TODO: input-output-hk/typed-protocols#57 +-- TODO: intersectmbo/typed-protocols#57 -- | Compute effective agency with respect to the peer role, for client role, @@ -491,25 +493,46 @@ -- | Promoted data type which indicates if 'Peer' is used in -- pipelined mode or not. -- -data IsPipelined where +type IsPipelined :: Type -> Type +data IsPipelined ps where -- | Pipelined peer which is using `c :: Type` for collecting responses -- from a pipelined messages. 'N' indicates depth of pipelining. - Pipelined :: N -> Type -> IsPipelined + Pipelined :: N -> Type -> IsPipelined ps -- | Non-pipelined peer. - NonPipelined :: IsPipelined + NonPipelined :: IsPipelined ps + -- | The dual of 'Pipelined': defers sends to background 'Sender's while + -- receiving ahead. 'N' counts unflushed 'Sender's. + Lookahead :: N -> SenderVariability ps -> IsPipelined ps + +-- | Whether each lookahead 'Sender' is supplied per-step or reused with fixed +-- endpoints. +type SenderVariability :: Type -> Type +data SenderVariability ps where + VariableSender :: SenderVariability ps + FixedSender :: ps -> ps -> SenderVariability ps + -- | Type level count of the number of outstanding pipelined yields for which -- we have not yet collected a receiver result. Used to -- ensure that 'Collect' is only used when there are outstanding results to -- collect (e.g. after 'YieldPipeliend' was used); -- and to ensure that the non-pipelined primitives 'Yield', 'Await' and 'Done' -- are only used when there are none unsatisfied pipelined requests. --- -type Outstanding :: IsPipelined -> N +type Outstanding :: IsPipelined ps -> N type family Outstanding pl where Outstanding 'NonPipelined = Z Outstanding ('Pipelined n _) = n + Outstanding ('Lookahead _ _) = Z + +-- | Dual of 'Outstanding': count of outstanding 'Sender's; blocks 'Yield' and +-- 'Done' (an inline send would race them). +-- +type OutstandingSenders :: IsPipelined ps -> N +type family OutstandingSenders pl where + OutstandingSenders 'NonPipelined = Z + OutstandingSenders ('Pipelined _ _) = Z + OutstandingSenders ('Lookahead n _) = n -- | A value level inductive natural number, indexed by the corresponding type -- level natural number 'N'. diff --git a/src/Network/TypedProtocol/Driver.hs b/src/Network/TypedProtocol/Driver.hs --- a/src/Network/TypedProtocol/Driver.hs +++ b/src/Network/TypedProtocol/Driver.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} -- | Actions for running 'Peer's with a 'Driver' @@ -12,17 +13,25 @@ , runPeerWithDriver -- * Pipelined peers , runPipelinedPeerWithDriver + -- * Lookahead peers + , runLookaheadPeerWithDriver + , runLookaheadFixedSenderPeerWithDriver ) where +import Control.Monad (forever, join) import Data.Void (Void) +import Numeric.Natural (Natural) import Network.TypedProtocol.Core import Network.TypedProtocol.Peer import Control.Concurrent.Class.MonadSTM.TQueue +import Control.Concurrent.Class.MonadSTM.TVar +import Control.DeepSeq (NFData, force) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadFork import Control.Monad.Class.MonadSTM +import Control.Monad.Class.MonadThrow -- $intro @@ -90,7 +99,7 @@ , -- | Initial state of the driver initialDState :: dstate } --- TODO: input-output-hk/typed-protocols#57 +-- TODO: intersectmbo/typed-protocols#57 -- | When decoding a 'Message' we only know the expected \"from\" state. We @@ -114,9 +123,22 @@ -- -- This runs the peer to completion (if the protocol allows for termination). -- +-- The returned value `a` is evaluated to normal form, any pure exceptions will +-- be raised by `runPeerWithDriver`. +-- +-- The returned `dstate` should be fed back into `runPeerWithDriver`, where it +-- will be evaluated incrementally. +-- runPeerWithDriver :: forall ps (st :: ps) pr dstate m a. - Monad m +#if MIN_VERSION_io_classes(1,10,0) + ( MonadEvaluate m +#else + ( Monad m + , MonadEvaluate m +#endif + , NFData a + ) => Driver ps pr dstate m -> Peer ps pr NonPipelined st m a -> m (a, dstate) @@ -128,7 +150,9 @@ -> Peer ps pr 'NonPipelined st' m a -> m (a, dstate) go dstate (Effect k) = k >>= go dstate - go dstate (Done _ x) = return (x, dstate) + go dstate (Done _ x) = do + x' <- evaluate (force x) + return (x', dstate) go dstate (Yield refl msg k) = do sendMessage refl msg @@ -165,19 +189,24 @@ -- runPipelinedPeerWithDriver :: forall ps (st :: ps) pr dstate m a. - MonadAsync m + ( MonadAsync m + , MonadEvaluate m + , NFData a + ) => Driver ps pr dstate m -> PeerPipelined ps pr st m a -> m (a, dstate) runPipelinedPeerWithDriver driver@Driver{initialDState} (PeerPipelined peer) = do receiveQueue <- atomically newTQueue collectQueue <- atomically newTQueue - a <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver + r@(a, _dstate) <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver `withAsyncLoop` runPipelinedPeerSender receiveQueue collectQueue driver peer initialDState - return a + _ <- evaluate (force a) + return r + where withAsyncLoop :: m Void -> m x -> m x withAsyncLoop left right = do @@ -340,3 +369,194 @@ go dstate (ReceiverAwait refl k) = do (SomeMessage msg, dstate') <- recvMessage refl dstate go dstate' (k msg) + + +-- +-- Running lookahead peers +-- + +-- | A 'Sender' whose states are hidden, so it can be queued. +-- +data SomeSender ps pr m where + SomeSender :: Sender ps pr VariableSender st stdone m + -> SomeSender ps pr m + +-- | Run a lookahead peer with the given driver. +-- +-- Dual to 'runPipelinedPeerWithDriver': where a pipelined peer sends ahead and +-- defers its receives to a parallel receiver thread, a lookahead peer receives +-- ahead and defers its sends to a parallel sender thread. +-- +-- There is no trailing-data handoff: the peer thread performs every +-- 'recvMessage' (so it owns @dstate@ outright), and the sender thread performs +-- every 'sendMessage'. The two only ever touch opposite directions of the +-- channel, and the 'OutstandingSenders' index guarantees the peer thread's own +-- sends ('Yield'\/'Done') happen only when the sender thread is idle. +-- +runLookaheadPeerWithDriver + :: forall ps (st :: ps) pr dstate m a. + ( MonadAsync m + , MonadEvaluate m + , NFData a + ) + => Driver ps pr dstate m + -> PeerLookahead ps pr st m a + -> m (a, dstate) +runLookaheadPeerWithDriver driver@Driver{initialDState} (PeerLookahead peer) = do + senderQueue <- atomically newTQueue + doneVar <- newTVarIO 0 + r@(a, _dstate) <- runLookaheadPeerSender (readTQueue senderQueue) doneVar driver + `withAsyncLoop` + runLookaheadPeerMain + (\sender -> writeTQueue senderQueue (SomeSender sender)) + doneVar driver peer initialDState + + _ <- evaluate (force a) + return r + + where + withAsyncLoop :: m Void -> m x -> m x + withAsyncLoop left right = do + res <- race left right + case res of + Left v -> case v of {} + Right a -> return a + + +-- | The peer (main) thread shared by both lookahead drivers. It differs only +-- in how it hands off the 'Sender' deferred at each 'AwaitLookahead', which is +-- the @registerSender@ argument: the variable driver enqueues it, the fixed +-- driver bumps a counter (ignoring the abstract 'TheSender'). +-- +runLookaheadPeerMain + :: forall ps (sv :: SenderVariability ps) (st :: ps) pr dstate m a. + ( MonadSTM m + , MonadThread m + ) + => (forall stA stZ. Sender ps pr sv stA stZ m -> STM m ()) + -- ^ register the 'Sender' deferred by an 'AwaitLookahead' + -> TVar m Natural + -- ^ count of 'Sender's that have since finished, consumed by 'FlushSender'. + -- + -- The role of this 'TVar' is the same as the queue of results in the + -- pipelining case, but since a 'Sender' doesn't return any result we just + -- count how many 'Sender's have finished: the sender increments it when it + -- finishes running, and 'FlushSender' decrements it. + -> Driver ps pr dstate m + -> Peer ps pr ('Lookahead Z sv) st m a + -> dstate + -> m (a, dstate) +runLookaheadPeerMain registerSender doneVar + Driver{sendMessage, recvMessage} + peer0 dstate0 = do + threadId <- myThreadId + labelThread threadId "lookahead-peer-main" + go dstate0 peer0 + where + go :: forall st' n. + dstate + -> Peer ps pr ('Lookahead n sv) st' m a + -> m (a, dstate) + go dstate (Effect k) = k >>= go dstate + go dstate (Done _ x) = return (x, dstate) + + -- Only reachable at 'Lookahead Z' (the constructor demands + -- @OutstandingSenders ~ Z@), i.e. when the sender thread is provably idle. + go dstate (Yield refl msg k) = do + sendMessage refl msg + go dstate k + + -- Legal at any 'OutstandingSenders': receiving ahead is the whole point. + go dstate (Await refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl dstate + go dstate' (k msg) + + go dstate (AwaitLookahead refl sender k) = do + atomically (registerSender sender) + (SomeMessage msg, dstate') <- recvMessage refl dstate + go dstate' (k msg) + + go dstate (FlushSender mbNonBlocking k) = + join $ atomically $ do + d <- readTVar doneVar + if d > 0 + then do writeTVar doneVar (d - 1); pure (go dstate k) + else case mbNonBlocking of + Nothing -> retry + Just k' -> pure (go dstate k') + + +-- | The sender thread shared by both lookahead drivers. It differs only in +-- how it obtains the next 'Sender' to run, which is the @nextSender@ argument: +-- the variable driver reads one off a queue, the fixed driver waits for its +-- counter and yields the one fixed 'Sender'. +-- +runLookaheadPeerSender + :: forall ps pr dstate m. + ( MonadSTM m + , MonadThread m + ) + => STM m (SomeSender ps pr m) + -- ^ obtain the next 'Sender' to run (blocking until one is available) + -> TVar m Natural + -> Driver ps pr dstate m + -> m Void +runLookaheadPeerSender nextSender doneVar + Driver{sendMessage} = do + threadId <- myThreadId + labelThread threadId "lookahead-sender" + forever $ do + SomeSender sender <- atomically nextSender + runSender sender + atomically $ modifyTVar' doneVar (+ 1) + where + runSender :: forall stA stZ. Sender ps pr VariableSender stA stZ m -> m () + runSender = \case + SenderEffect k -> k >>= runSender + SenderDone -> return () + SenderYield refl msg k -> do + sendMessage refl msg + runSender k + + +-- | Run a fixed-'Sender' lookahead peer with the given driver. +-- +-- Like 'runLookaheadPeerWithDriver', but every 'AwaitLookahead' reuses the one +-- 'Sender' supplied here, so the driver tracks outstanding sends with a plain +-- counter rather than a queue. ('embedLookaheadUsingFixedSender' could instead +-- reduce this to 'runLookaheadPeerWithDriver', but that would allocate and +-- queue a redundant 'Sender' per step.) +-- +runLookaheadFixedSenderPeerWithDriver + :: forall ps (st :: ps) pr dstate m a. + ( MonadAsync m + , MonadEvaluate m + , NFData a + ) + => Driver ps pr dstate m + -> PeerLookaheadFixedSender ps pr st m a + -> m (a, dstate) +runLookaheadFixedSenderPeerWithDriver driver@Driver{initialDState} (PeerLookaheadFixedSender sender peer) = do + sendVar <- newTVarIO (0 :: Natural) + doneVar <- newTVarIO 0 + let -- wait for the counter, then yield the one fixed 'Sender' + nextSender = do n <- readTVar sendVar + check (0 < n) + writeTVar sendVar $! n - 1 + return (SomeSender sender) + r@(a, _dstate) <- runLookaheadPeerSender nextSender doneVar driver + `withAsyncLoop` + runLookaheadPeerMain + (\TheSender -> modifyTVar' sendVar (+ 1)) + doneVar driver peer initialDState + + _ <- evaluate (force a) + return r + + where + withAsyncLoop :: m Void -> m x -> m x + withAsyncLoop left right = do + res <- race left right + case res of + Left v -> case v of {} + Right a -> return a diff --git a/src/Network/TypedProtocol/Peer.hs b/src/Network/TypedProtocol/Peer.hs --- a/src/Network/TypedProtocol/Peer.hs +++ b/src/Network/TypedProtocol/Peer.hs @@ -5,8 +5,12 @@ module Network.TypedProtocol.Peer ( Peer (..) , PeerPipelined (..) + , PeerLookahead (..) + , PeerLookaheadFixedSender (..) , Receiver (..) + , Sender (..) , Outstanding + , OutstandingSenders , N (..) , Nat (Zero, Succ) , natToInt @@ -79,7 +83,7 @@ -- type Peer :: forall ps -> PeerRole - -> IsPipelined + -> IsPipelined ps -> ps -> (Type -> Type) -- ^ monad's kind @@ -115,6 +119,7 @@ , StateTokenI st' , ActiveState st , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => WeHaveAgencyProof pr st -- ^ agency proof @@ -146,6 +151,7 @@ ( StateTokenI st , ActiveState st , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => TheyHaveAgencyProof pr st -- ^ agency proof @@ -169,6 +175,7 @@ ( StateTokenI st , StateAgency st ~ NobodyAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => NobodyHasAgencyProof pr st -- ^ (no) agency proof @@ -214,6 +221,38 @@ -- ^ continuation -> Peer ps pr (Pipelined (S n) c) st m a + -- + -- Lookahead primitives + -- + + -- | The dual of 'YieldPipelined'. Defer the send @st -> st'@ to a background + -- 'Sender', then await ahead at @st'@. + -- + AwaitLookahead + :: forall ps pr (sv :: SenderVariability ps) (st :: ps) (st' :: ps) n m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + , ActiveState st' + ) + => TheyHaveAgencyProof pr st' + -> Sender ps pr sv st st' m + -> (forall st''. Message ps st' st'' + -> Peer ps pr (Lookahead (S n) sv) st'' m a) + -> Peer ps pr (Lookahead n sv) st m a + + -- | The dual of 'Collect': await one deferred 'Sender' to finish. Unlike + -- 'Collect', this can also be used at a terminal state (to drain before + -- 'Done'), so it does not require 'ActiveState'. + -- + FlushSender + :: forall ps pr n (sv :: SenderVariability ps) st m a. + ( StateTokenI st + ) + => Maybe (Peer ps pr (Lookahead (S n) sv) st m a) + -> (Peer ps pr (Lookahead n sv) st m a) + -> Peer ps pr (Lookahead (S n) sv) st m a + deriving instance Functor m => Functor (Peer ps pr pl st m) @@ -260,6 +299,32 @@ deriving instance Functor m => Functor (Receiver ps pr st stdone m) +-- | The 'Lookahead' analog of 'Receiver' +type Sender :: forall ps + -> PeerRole + -> SenderVariability ps + -> ps + -> ps + -> (Type -> Type) + -> Type +data Sender ps pr sv st stdone m where + + TheSender :: Sender ps pr (FixedSender st stdone) st stdone m + + SenderEffect :: m (Sender ps pr VariableSender st stdone m) + -> Sender ps pr VariableSender st stdone m + + SenderDone :: Sender ps pr VariableSender stdone stdone m + + SenderYield :: ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => !(WeHaveAgencyProof pr st) + -> Message ps st st' + -> Sender ps pr VariableSender st' stdone m + -> Sender ps pr VariableSender st stdone m + -- | A description of a peer that engages in a protocol in a pipelined fashion. -- -- This type is useful for wrapping pipelined peers to hide information which @@ -271,3 +336,29 @@ -> PeerPipelined ps pr st m a deriving instance Functor m => Functor (PeerPipelined ps pr st m) + +-- | Wrapper for a lookahead peer that supplies its own 'Sender' at each +-- 'AwaitLookahead'. Expected by +-- 'Network.TypedProtocol.Driver.runLookaheadPeerWithDriver'. +-- +data PeerLookahead ps pr (st :: ps) m a where + PeerLookahead :: { runPeerLookahead :: Peer ps pr (Lookahead Z VariableSender) st m a } + -> PeerLookahead ps pr st m a + +deriving instance Functor m => Functor (PeerLookahead ps pr st m) + +-- | Wrapper for a lookahead peer whose 'AwaitLookahead's all use 'TheSender', +-- i.e. reuse the one 'Sender' carried here (with fixed endpoints @apst -> +-- apst'@). Expected by +-- 'Network.TypedProtocol.Driver.runLookaheadFixedSenderPeerWithDriver', which +-- can then track outstanding sends with a counter rather than a queue. +-- +-- The carried 'Sender' is a 'VariableSender' — the concrete one the driver +-- actually runs; the peer only refers to it abstractly via 'TheSender'. +-- +data PeerLookaheadFixedSender ps pr (st :: ps) m a where + PeerLookaheadFixedSender :: Sender ps pr VariableSender apst apst' m + -> Peer ps pr (Lookahead Z (FixedSender apst apst')) st m a + -> PeerLookaheadFixedSender ps pr st m a + +deriving instance Functor m => Functor (PeerLookaheadFixedSender ps pr st m) diff --git a/src/Network/TypedProtocol/Peer/Client.hs b/src/Network/TypedProtocol/Peer/Client.hs --- a/src/Network/TypedProtocol/Peer/Client.hs +++ b/src/Network/TypedProtocol/Peer/Client.hs @@ -36,7 +36,7 @@ type Client :: forall ps - -> IsPipelined + -> IsPipelined ps -> ps -> (Type -> Type) -> Type @@ -76,6 +76,7 @@ , StateTokenI st' , StateAgency st ~ ClientAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => Message ps st st' -- ^ protocol message @@ -92,6 +93,7 @@ => ( StateTokenI st , StateAgency st ~ ServerAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => (forall st'. Message ps st st' -> Client ps pl st' m a) @@ -107,6 +109,7 @@ => ( StateTokenI st , StateAgency st ~ NobodyAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => a -- ^ protocol return value diff --git a/src/Network/TypedProtocol/Peer/Server.hs b/src/Network/TypedProtocol/Peer/Server.hs --- a/src/Network/TypedProtocol/Peer/Server.hs +++ b/src/Network/TypedProtocol/Peer/Server.hs @@ -14,17 +14,32 @@ , pattern Done , pattern YieldPipelined , pattern Collect + , pattern AwaitLookahead + , pattern FlushSender -- * Receiver type alias and its pattern synonyms , Receiver , pattern ReceiverEffect , pattern ReceiverAwait , pattern ReceiverDone + -- * Sender type alias and its pattern synonyms + , Sender + , pattern TheSender + , pattern SenderEffect + , pattern SenderYield + , pattern SenderDone -- * ServerPipelined type alias and its pattern synonym , ServerPipelined , TP.PeerPipelined (ServerPipelined, runServerPipelined) + -- * ServerLookahead type aliases and their pattern synonyms + , ServerLookahead + , TP.PeerLookahead (ServerLookahead, runServerLookahead) + , ServerLookaheadFixedSender + , pattern ServerLookaheadFixedSender -- * re-exports , IsPipelined (..) + , SenderVariability (..) , Outstanding + , OutstandingSenders , N (..) , Nat (..) ) where @@ -37,7 +52,7 @@ type Server :: forall ps - -> IsPipelined + -> IsPipelined ps -> ps -> (Type -> Type) -> Type @@ -60,6 +75,41 @@ {-# COMPLETE ServerPipelined #-} +-- TODO: mirror these lookahead pattern synonyms in +-- 'Network.TypedProtocol.Peer.Client' (a 'ClientLookahead' / +-- 'ClientLookaheadFixedSender'). They are not strictly needed since the API is +-- symmetric, but they would let a user work in terms of 'Client' as well as +-- 'Server'. + +-- | A lookahead server that supplies its own 'Sender' at each 'AwaitLookahead'. +-- +type ServerLookahead ps st m a = TP.PeerLookahead ps AsServer st m a + +pattern ServerLookahead :: forall ps st m a. + () + => Server ps (Lookahead Z VariableSender) st m a + -> ServerLookahead ps st m a +pattern ServerLookahead { runServerLookahead } = TP.PeerLookahead runServerLookahead + +{-# COMPLETE ServerLookahead #-} + + +-- | A lookahead server that reuses one 'Sender' at each 'AwaitLookaheadFixedSender'. +-- +type ServerLookaheadFixedSender ps st m a = TP.PeerLookaheadFixedSender ps AsServer st m a + +pattern ServerLookaheadFixedSender :: forall ps st m a. + () + => forall apst apst'. + () + => Sender ps VariableSender apst apst' m + -> Server ps (Lookahead Z (FixedSender apst apst')) st m a + -> ServerLookaheadFixedSender ps st m a +pattern ServerLookaheadFixedSender sender peer = TP.PeerLookaheadFixedSender sender peer + +{-# COMPLETE ServerLookaheadFixedSender #-} + + -- | Server role pattern for 'TP.Effect'. -- pattern Effect :: forall ps pl st m a. @@ -78,6 +128,7 @@ , StateTokenI st' , StateAgency st ~ ServerAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => Message ps st st' -- ^ protocol message @@ -94,6 +145,7 @@ => ( StateTokenI st , StateAgency st ~ ClientAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => (forall st'. Message ps st st' -> Server ps pl st' m a) @@ -109,6 +161,7 @@ => ( StateTokenI st , StateAgency st ~ NobodyAgency , Outstanding pl ~ Z + , OutstandingSenders pl ~ Z ) => a -- ^ protocol return value @@ -152,6 +205,45 @@ {-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-} +-- | Server role pattern for 'TP.AwaitLookahead' +-- +-- Use 'TheSender' as the first argument for a fixed-'Sender' peer, or a +-- concrete 'VariableSender' for a per-step one. +-- +pattern AwaitLookahead :: forall ps sv st n m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + , StateAgency st' ~ ClientAgency + ) + => Sender ps sv st st' m + -- ^ sender for the deferred send @st -> st'@ + -> (forall st''. Message ps st' st'' + -> Server ps (Lookahead (S n) sv) st'' m a) + -- ^ continuation, awaiting ahead at @st'@ + -> Server ps (Lookahead n sv) st m a +pattern AwaitLookahead sender k = TP.AwaitLookahead ReflClientAgency sender k + + +-- | Server role pattern for 'TP.FlushSender' +-- +pattern FlushSender :: forall ps st n sv m a. + () + => ( StateTokenI st + ) + => Maybe (Server ps (Lookahead (S n) sv) st m a) + -- ^ continuation if no 'Sender' has finished so far + -> (Server ps (Lookahead n sv) st m a) + -- ^ continuation once a 'Sender' has finished + -> Server ps (Lookahead (S n) sv) st m a +pattern FlushSender mk k = TP.FlushSender mk k + + +{-# COMPLETE Effect, Yield, Await, Done, AwaitLookahead, FlushSender #-} + + type Receiver ps st stdone m c = TP.Receiver ps AsServer st stdone m c pattern ReceiverEffect :: forall ps st stdone m c. @@ -177,3 +269,36 @@ pattern ReceiverDone c = TP.ReceiverDone c {-# COMPLETE ReceiverEffect, ReceiverAwait, ReceiverDone #-} + + +type Sender ps sv st stdone m = TP.Sender ps AsServer sv st stdone m + +pattern TheSender :: forall ps sv st stdone m. + () + => (sv ~ FixedSender st stdone) + => Sender ps sv st stdone m +pattern TheSender = TP.TheSender + +pattern SenderEffect :: forall ps st stdone m. + m (Sender ps VariableSender st stdone m) + -> Sender ps VariableSender st stdone m +pattern SenderEffect k = TP.SenderEffect k + +pattern SenderYield :: forall ps st stdone m. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + ) + => Message ps st st' + -> Sender ps VariableSender st' stdone m + -> Sender ps VariableSender st stdone m +pattern SenderYield msg k = TP.SenderYield ReflServerAgency msg k + +pattern SenderDone :: forall ps stdone m. + Sender ps VariableSender stdone stdone m +pattern SenderDone = TP.SenderDone + +{-# COMPLETE TheSender #-} +{-# COMPLETE SenderEffect, SenderYield, SenderDone #-} diff --git a/src/Network/TypedProtocol/Proofs.hs b/src/Network/TypedProtocol/Proofs.hs --- a/src/Network/TypedProtocol/Proofs.hs +++ b/src/Network/TypedProtocol/Proofs.hs @@ -12,11 +12,17 @@ ( -- * Connect proofs connect , connectPipelined + , connectLookahead , TerminalStates (..) -- * Pipelining proofs -- | Additional proofs specific to the pipelining features , forgetPipelined , promoteToPipelined + -- * Lookahead proofs + -- | Additional proofs specific to the lookahead features + , forgetLookahead + , promoteToLookahead + , embedLookaheadUsingFixedSender -- ** Pipeline proof helpers , Queue (..) , enqueue @@ -224,6 +230,127 @@ -- ^ peers results and an evidence of their termination connectPipelined csA a b = connect (forgetPipelined csA a) b + + +-- +-- Remove Lookahead +-- + + +-- | Total conversion from lookahead peers to regular peers: the lookahead +-- analogue of 'forgetPipelined'. +-- +-- Where 'forgetPipelined' inlines each 'Receiver' at the point it is collected, +-- this inlines the 'Sender' supplied at each 'AwaitLookahead': its sends, which +-- the sender thread would have performed asynchronously, are performed +-- synchronously just before the fused receive. +-- +-- Dually to 'forgetPipelined', the @[Bool]@ chooses the interleaving at each +-- 'FlushSender': a @True@ pretends the 'Sender' has not finished yet, so the +-- peer takes its non-blocking continuation (when it has one) and leaves the +-- send outstanding; a @False@ (or @[]@) flushes it. +-- +forgetLookahead + :: forall ps (pr :: PeerRole) (st :: ps) m a. + Functor m + => [Bool] + -- ^ interleaving choices allowed by the 'FlushSender' primitive; @False@ + -- values or @[]@ leave nothing outstanding. + -> PeerLookahead ps pr st m a + -> Peer ps pr NonPipelined st m a +forgetLookahead cs0 (PeerLookahead peer0) = + goPeer cs0 peer0 + where + goPeer :: forall st' n. + [Bool] + -> Peer ps pr ('Lookahead n VariableSender) st' m a + -> Peer ps pr 'NonPipelined st' m a + goPeer cs (Effect k) = Effect (goPeer cs <$> k) + goPeer _ (Done refl k) = Done refl k + goPeer cs (Yield refl m k) = Yield refl m (goPeer cs k) + goPeer cs (Await refl k) = Await refl (goPeer cs . k) + goPeer cs (AwaitLookahead refl sender k) = + goSender sender (Await refl (goPeer cs . k)) + goPeer (True:cs') (FlushSender (Just k) _) = goPeer cs' k + goPeer (_:cs) (FlushSender _ k) = goPeer cs k + goPeer cs@[] (FlushSender _ k) = goPeer cs k + + goSender :: forall sst sst'. + Sender ps pr VariableSender sst sst' m + -> Peer ps pr 'NonPipelined sst' m a + -> Peer ps pr 'NonPipelined sst m a + goSender SenderDone k = k + goSender (SenderEffect ks) k = Effect ((`goSender` k) <$> ks) + goSender (SenderYield refl m ks) k = Yield refl m (goSender ks k) + + +-- | Promote a peer to a lookahead one, using an empty 'Sender'. +-- +-- This is a right inverse of 'forgetLookahead', e.g. +-- +-- >>> forgetLookahead . promoteToLookahead = id +-- +promoteToLookahead + :: forall ps (pr :: PeerRole) (st :: ps) m a. + Functor m + => Peer ps pr NonPipelined st m a + -- ^ a peer + -> PeerLookahead ps pr st m a + -- ^ a lookahead peer +promoteToLookahead p = PeerLookahead (go p) + where + go :: forall st'. + Peer ps pr 'NonPipelined st' m a + -> Peer ps pr ('Lookahead 'Z VariableSender) st' m a + go (Effect k) = Effect (go <$> k) + go (Yield refl m k) = Yield refl m (go k) + go (Await refl k) = Await refl (go . k) + go (Done refl k) = Done refl k + + +-- | Embed a fixed-'Sender' lookahead peer as a variable-'Sender' one, by +-- plugging the carried 'Sender' in for each 'TheSender'. This lets the +-- 'PeerLookahead' machinery (proofs, driver) subsume 'PeerLookaheadFixedSender' — +-- though a dedicated fixed driver is still preferable, as it can track +-- outstanding sends with a counter rather than a queue. +-- +embedLookaheadUsingFixedSender + :: forall ps (pr :: PeerRole) (st :: ps) m a. + Functor m + => PeerLookaheadFixedSender ps pr st m a + -> PeerLookahead ps pr st m a +embedLookaheadUsingFixedSender (PeerLookaheadFixedSender (sender :: Sender ps pr VariableSender apst apst' m) peer0) = + PeerLookahead (go peer0) + where + go :: forall st' n. + Peer ps pr ('Lookahead n (FixedSender apst apst')) st' m a + -> Peer ps pr ('Lookahead n VariableSender) st' m a + go (Effect k) = Effect (go <$> k) + go (Done refl k) = Done refl k + go (Yield refl m k) = Yield refl m (go k) + go (Await refl k) = Await refl (go . k) + go (AwaitLookahead refl TheSender k) = + AwaitLookahead refl sender (go . k) + go (FlushSender mk k) = FlushSender (go <$> mk) (go k) + + +-- | Analogous to 'connectPipelined' but for lookahead peers. +-- +connectLookahead + :: forall ps (pr :: PeerRole) + (st :: ps) m a b. + (Monad m, SingI pr) + => [Bool] + -- ^ an interleaving + -> PeerLookahead ps pr st m a + -- ^ a lookahead peer + -> Peer ps (FlipAgency pr) NonPipelined st m b + -- ^ a non-pipelined peer with flipped agency + -> m (a, b, TerminalStates ps) + -- ^ peers results and an evidence of their termination +connectLookahead cs a b = + connect (forgetLookahead cs a) b + -- | A reference specification for interleaving of requests and responses -- with pipelining, where the environment can choose whether a response is diff --git a/stateful/Network/TypedProtocol/Stateful/Codec.hs b/stateful/Network/TypedProtocol/Stateful/Codec.hs --- a/stateful/Network/TypedProtocol/Stateful/Codec.hs +++ b/stateful/Network/TypedProtocol/Stateful/Codec.hs @@ -35,16 +35,9 @@ -- * Testing codec properties , AnyMessage (.., AnyMessageAndAgency) , showAnyMessage - , prop_codecM - , prop_codec - , prop_codec_splitsM - , prop_codec_splits - , prop_codecs_compatM - , prop_codecs_compat ) where import Data.Kind (Type) -import Data.Monoid (All (..)) import Network.TypedProtocol.Codec (CodecFailure (..), DecodeStep (..), SomeMessage (..), hoistDecodeStep, isoDecodeStep, @@ -55,6 +48,8 @@ -- | A stateful codec. -- +-- TODO: provide CodecF as in typed-protocols:typed-protocols library. +-- data Codec ps failure (f :: ps -> Type) m bytes = Codec { encode :: forall (st :: ps) (st' :: ps). StateTokenI st @@ -63,7 +58,7 @@ -- local state, which contain extra context for the encoding -- process. -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> Message ps st st' -- message to be encoded -> bytes, @@ -75,7 +70,7 @@ -- local state, which can contain extra context from the -- previous message. -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> m (DecodeStep bytes failure m (SomeMessage st)) } @@ -177,119 +172,3 @@ -- getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st) getAgency msg = (msg, stateToken) - - --- | The 'Codec' round-trip property: decode after encode gives the same --- message. Every codec must satisfy this property. --- -prop_codecM - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - ) - => Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do - r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ AnyMessage f msg' == a - Left _ -> return False - --- | The 'Codec' round-trip property in a pure monad. --- -prop_codec - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (forall a. m a -> a) - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codec runM codec msg = - runM (prop_codecM codec msg) - - --- | A variant on the codec round-trip property: given the encoding of a --- message, check that decode always gives the same result irrespective --- of how the chunks of input are fed to the incremental decoder. --- --- This property guards against boundary errors in incremental decoders. --- It is not necessary to check this for every message type, just for each --- generic codec construction. For example given some binary serialisation --- library one would write a generic adaptor to the codec interface. This --- adaptor has to deal with the incremental decoding and this is what needs --- to be checked. --- -prop_codec_splitsM - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codec_splitsM splits - Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do - and <$> sequence - [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ AnyMessage f msg' == a - Left _ -> return False - - | let bytes = encode f msg - , bytes' <- splits bytes ] - - --- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codec_splits - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (bytes -> [[bytes]]) - -> (forall a. m a -> a) - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codec_splits splits runM codec msg = - runM $ prop_codec_splitsM splits codec msg - - --- | Compatibility between two codecs of the same protocol. Encode a message --- with one codec and decode it with the other one, then compare if the result --- is the same as initial message. --- -prop_codecs_compatM - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - , forall a. Monoid a => Monoid (m a) - ) - => Codec ps failure f m bytes - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codecs_compatM codecA codecB - a@(AnyMessage f (msg :: Message ps st st')) = - getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a - Left _ -> return $ All False - <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a - Left _ -> return $ All False - --- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codecs_compat - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - , forall a. Monoid a => Monoid (m a) - ) - => (forall a. m a -> a) - -> Codec ps failure f m bytes - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codecs_compat run codecA codecB msg = - run $ prop_codecs_compatM codecA codecB msg diff --git a/stateful/Network/TypedProtocol/Stateful/Driver.hs b/stateful/Network/TypedProtocol/Stateful/Driver.hs --- a/stateful/Network/TypedProtocol/Stateful/Driver.hs +++ b/stateful/Network/TypedProtocol/Stateful/Driver.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + -- | Actions for running 'Peer's with a 'Driver'. This module should be -- imported qualified. -- @@ -11,7 +13,11 @@ , DecodeStep (..) ) where +import Control.DeepSeq (NFData, force) +#if !MIN_VERSION_io_classes(1,10,0) import Control.Monad.Class.MonadSTM +#endif +import Control.Monad.Class.MonadThrow import Data.Kind (Type) @@ -35,11 +41,11 @@ -- local state should not be sent to the remote side. -- However it provide extra context for the encoder. -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> Message ps st st' -- message to send -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> m () , -- | Receive a message, a blocking action which reads from the network @@ -55,12 +61,12 @@ -- local state which provides extra context for the -- decoder. -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> dstate -- decoder state, e.g. bytes left from decoding of -- a previous message. -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> m (SomeMessage st, dstate) , -- | Initial decoder state. @@ -82,7 +88,12 @@ -- runPeerWithDriver :: forall ps (st :: ps) pr bytes failure dstate (f :: ps -> Type) m a. - MonadSTM m + ( MonadEvaluate m +#if !MIN_VERSION_io_classes(1,10,0) + , MonadSTM m +#endif + , NFData a + ) => Driver ps pr bytes failure dstate f m -> f st -> Peer ps pr st f m a @@ -100,7 +111,9 @@ -> m (a, dstate) go !dstate !f (Effect k) = k >>= go dstate f - go !dstate _ (Done _ x) = return (x, dstate) + go !dstate _ (Done _ x) = do + x' <- evaluate (force x) + return (x', dstate) go !dstate _ (Yield refl !f !f' msg k) = do sendMessage refl f msg diff --git a/stateful/Network/TypedProtocol/Stateful/Peer.hs b/stateful/Network/TypedProtocol/Stateful/Peer.hs --- a/stateful/Network/TypedProtocol/Stateful/Peer.hs +++ b/stateful/Network/TypedProtocol/Stateful/Peer.hs @@ -154,7 +154,7 @@ f st -- associated local state to the source protocol state 'st' -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 -> Message ps st st' -> ( Peer ps pr st' f m a , f st' @@ -164,9 +164,9 @@ -- -- NOTE: the API is limited to pure transition of local state e.g. -- `f st -> Message ps st st' -> f st'`, - -- see https://github.com/input-output-hk/typed-protocols/discussions/63 + -- see https://github.com/intersectmbo/typed-protocols/discussions/63 -- - -- TODO: input-output-hk/typed-protocols#57 + -- TODO: intersectmbo/typed-protocols#57 ) -- ^ continuation -> Peer ps pr st f m a diff --git a/test/Network/TypedProtocol/PingPong/Tests.hs b/test/Network/TypedProtocol/PingPong/Tests.hs --- a/test/Network/TypedProtocol/PingPong/Tests.hs +++ b/test/Network/TypedProtocol/PingPong/Tests.hs @@ -13,6 +13,7 @@ import Network.TypedProtocol.Channel import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.Properties import Network.TypedProtocol.Driver.Simple import Network.TypedProtocol.Proofs @@ -46,6 +47,11 @@ import Test.Tasty.QuickCheck (testProperty) +#if !MIN_VERSION_QuickCheck(2, 18, 0) +withNumTests :: Testable prop => Int -> prop -> Property +withNumTests = withMaxSuccess +#endif + -- -- The list of all properties -- @@ -74,7 +80,7 @@ , testGroup "CBOR" [ testProperty "codec" prop_codec_cbor_PingPong , testProperty "codec 2-splits" prop_codec_cbor_splits2_PingPong - , testProperty "codec 3-splits" $ withMaxSuccess 30 prop_codec_cbor_splits3_PingPong + , testProperty "codec 3-splits" $ withNumTests 30 prop_codec_cbor_splits3_PingPong ] ] ] @@ -289,7 +295,12 @@ -- | Run a non-pipelined client and server over a channel using a codec. -- -prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) +prop_channel :: ( MonadLabelledSTM m + , MonadTraceSTM m + , MonadAsync m + , MonadCatch m + , MonadEvaluate m + ) => NonNegative Int -> m Bool prop_channel (NonNegative n) = do @@ -390,20 +401,20 @@ AnyMessage MsgDone == AnyMessage MsgDone = True _ == _ = False -prop_codec_PingPong :: AnyMessage PingPong -> Bool +prop_codec_PingPong :: AnyMessage PingPong -> Property prop_codec_PingPong = prop_codec runIdentity codecPingPong -prop_codec_splits2_PingPong :: AnyMessage PingPong -> Bool +prop_codec_splits2_PingPong :: AnyMessage PingPong -> Property prop_codec_splits2_PingPong = prop_codec_splits splits2 runIdentity codecPingPong -prop_codec_splits3_PingPong :: AnyMessage PingPong -> Bool +prop_codec_splits3_PingPong :: AnyMessage PingPong -> Property prop_codec_splits3_PingPong = prop_codec_splits splits3 @@ -416,13 +427,13 @@ prop_codec_cbor_PingPong :: AnyMessage PingPong - -> Bool + -> Property prop_codec_cbor_PingPong msg = runST $ prop_codecM CBOR.codecPingPong msg prop_codec_cbor_splits2_PingPong :: AnyMessage PingPong - -> Bool + -> Property prop_codec_cbor_splits2_PingPong msg = runST $ prop_codec_splitsM splits2BS @@ -431,7 +442,7 @@ prop_codec_cbor_splits3_PingPong :: AnyMessage PingPong - -> Bool + -> Property prop_codec_cbor_splits3_PingPong msg = runST $ prop_codec_splitsM splits3BS diff --git a/test/Network/TypedProtocol/ReqResp/Tests.hs b/test/Network/TypedProtocol/ReqResp/Tests.hs --- a/test/Network/TypedProtocol/ReqResp/Tests.hs +++ b/test/Network/TypedProtocol/ReqResp/Tests.hs @@ -6,6 +6,7 @@ import Network.TypedProtocol.Channel import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.Properties import Network.TypedProtocol.Driver.Simple import Network.TypedProtocol.Proofs @@ -16,14 +17,16 @@ import Network.TypedProtocol.ReqResp.Server import Network.TypedProtocol.ReqResp.Type +import Control.Concurrent.Class.MonadSTM.TVar (newTVarIO, readTVar, writeTVar) import Control.Exception (throw) import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM +import Control.Monad.Class.MonadTest (MonadTest (exploreRaces)) import Control.Monad.Class.MonadThrow -import Control.Monad.Class.MonadTimer.SI import Control.Monad.IOSim import Control.Monad.ST (runST) +import Control.Monad.Trans.State.Strict (State, runState, state) import Control.Tracer (nullTracer) import Data.Functor.Identity (Identity (..)) @@ -45,6 +48,11 @@ import Text.Show.Functions () +#if !MIN_VERSION_QuickCheck(2, 18, 0) +withNumTests :: Testable prop => Int -> prop -> Property +withNumTests = withMaxSuccess +#endif + -- -- The list of all properties -- @@ -55,10 +63,16 @@ , testProperty "directPipelined" prop_directPipelined , testProperty "connect" prop_connect , testProperty "connectPipelined" prop_connectPipelined + , testProperty "connectLookahead" prop_connectLookahead , testProperty "channel ST" prop_channel_ST , testProperty "channel IO" prop_channel_IO , testProperty "channelPipelined ST" prop_channelPipelined_ST , testProperty "channelPipelined IO" prop_channelPipelined_IO + , testProperty "channelLookahead ST" prop_channelLookahead_ST + , testProperty "channelLookahead IO" prop_channelLookahead_IO + , testProperty "channelLookahead IOSimPOR" prop_channelLookahead_IOSimPOR + , testProperty "lookaheadFixedEquiv ST" prop_lookaheadFixedEquiv_ST + , testProperty "lookaheadFixedEquiv IO" prop_lookaheadFixedEquiv_IO #if !defined(mingw32_HOST_OS) , testProperty "namedPipePipelined" prop_namedPipePipelined_IO , testProperty "socketPipelined" prop_socketPipelined_IO @@ -66,13 +80,16 @@ , testGroup "Codec" [ testProperty "codec" prop_codec_ReqResp , testProperty "codec 2-splits" prop_codec_splits2_ReqResp - , testProperty "codec 3-splits" (withMaxSuccess 33 prop_codec_splits3_ReqResp) + , testProperty "codec 3-splits" (withNumTests 33 prop_codec_splits3_ReqResp) , testGroup "CBOR" [ testProperty "codec" prop_codec_cbor_ReqResp , testProperty "codec 2-splits" prop_codec_cbor_splits2_ReqResp - , testProperty "codec 3-splits" $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp + , testProperty "codec 3-splits" $ withNumTests 30 prop_codec_cbor_splits3_ReqResp ] ] + , testGroup "AnnotatedCodec" + [ testProperty "codec" prop_anncodec_ReqResp + ] ] @@ -165,11 +182,35 @@ (s, c) == mapAccumL f 0 xs +-- | The dual of 'prop_connectPipelined': a lookahead server (which ignores the +-- request payload and reads each reply from the state) against a non-pipelined +-- client. The result must not depend on the interleaving choices. -- +prop_connectLookahead :: [Bool] -> (Int -> (Int, Int)) -> NonNegative Int -> Bool +prop_connectLookahead cs g (NonNegative n) = + case runState + (connectLookahead cs + (reqRespServerPeerLookahead nextResp) + (reqRespClientPeer (reqRespClientMap (replicate n ())))) + 0 + + of ((_, resps, TerminalStates SingDone SingDone), acc) -> + (acc, resps) == mapAccumL (\a () -> g a) 0 (replicate n ()) + where + nextResp :: State Int Int + nextResp = state (\a -> let (a', r) = g a in (r, a')) + + +-- -- Properties using channels, codecs and drivers. -- -prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) +prop_channel :: ( MonadLabelledSTM m + , MonadTraceSTM m + , MonadAsync m + , MonadCatch m + , MonadEvaluate m + ) => (Int -> Int -> (Int, Int)) -> [Int] -> m Bool prop_channel f xs = do @@ -192,8 +233,12 @@ runSimOrThrow (prop_channel f xs) -prop_channelPipelined :: ( MonadLabelledSTM m, MonadAsync m, MonadCatch m - , MonadDelay m, MonadST m) +prop_channelPipelined :: ( MonadLabelledSTM m + , MonadAsync m + , MonadCatch m + , MonadEvaluate m + , MonadST m + ) => (Int -> Int -> (Int, Int)) -> [Int] -> m Bool prop_channelPipelined f xs = do @@ -221,6 +266,129 @@ Right res -> res +-- | The channel/driver sibling of 'prop_connectLookahead': a pipelined client +-- against a lookahead server, run through the real 'runPipelinedPeer' / +-- 'runLookaheadPeer' drivers over a channel. Unlike @connect@, this genuinely +-- runs the 'Sender's concurrently with the main peer's receive-ahead, so the +-- lookahead machinery is actually exercised. The collected replies must equal +-- the reference sequence regardless of the interleaving the runtime picks. +-- +prop_channelLookahead :: ( MonadLabelledSTM m + , MonadAsync m + , MonadCatch m + , MonadEvaluate m + , MonadST m + , MonadTest m + ) + => (Int -> (Int, Int)) -> NonNegative Int + -> m Bool +prop_channelLookahead g (NonNegative n) = do + -- mark all threads forked from here on as system threads, so IOSimPOR will + -- reverse races between the client's receivers and the server's 'Sender's + -- (a no-op under IO / plain IOSim) + exploreRaces + accVar <- newTVarIO 0 + let nextResp = atomically $ do + a <- readTVar accVar + let (a', r) = g a + writeTVar accVar a' + return r + client = reqRespClientPeerPipelined (reqRespClientMapPipelined (replicate n ())) + server = reqRespServerPeerLookahead nextResp + (resps, ()) <- runConnectedPeersLookahead + (createPipelineTestChannels 100) + nullTracer + CBOR.codecReqResp + client server + return (resps == snd (mapAccumL (\a () -> g a) 0 (replicate n ()))) + +prop_channelLookahead_IO :: (Int -> (Int, Int)) -> NonNegative Int -> Property +prop_channelLookahead_IO g n = + ioProperty (prop_channelLookahead g n) + +prop_channelLookahead_ST :: (Int -> (Int, Int)) -> NonNegative Int -> Property +prop_channelLookahead_ST g n = + let tr = runSimTrace (prop_channelLookahead g n) in + counterexample (intercalate "\n" $ map show $ traceEvents tr) + $ case traceResult True tr of + Left err -> throw err + Right res -> res + +-- | Have IOSimPOR systematically explore the interleavings of the client's +-- receivers and the server's 'Sender's, checking that the lookahead driver +-- produces the reference result under every schedule. The request count is kept +-- small so the schedule space stays tractable. +-- +prop_channelLookahead_IOSimPOR :: (Int -> (Int, Int)) -> NonNegative Int -> Property +prop_channelLookahead_IOSimPOR g (NonNegative n) = + withNumTests 20 $ + exploreSimTrace id (prop_channelLookahead g (NonNegative (min n 6))) $ \_ tr -> + case traceResult False tr of + Left failure -> counterexample (show failure) (property False) + Right res -> property res + + +-- | 'runLookaheadFixedSenderPeerWithDriver' and +-- @'runLookaheadPeerWithDriver' . 'embedLookaheadUsingFixedSender'@ run the same +-- fixed-'Sender' peer two different ways — the former tracking outstanding sends +-- with a counter, the latter with a queue of (degenerate) 'Sender's. This runs +-- a pipelined client against the same fixed server via each and checks both +-- collect the same replies, matching the reference sequence. +-- +prop_lookaheadFixedEquiv :: ( MonadLabelledSTM m + , MonadAsync m + , MonadCatch m + , MonadEvaluate m + , MonadST m + ) + => (Int -> (Int, Int)) -> NonNegative Int + -> m Bool +prop_lookaheadFixedEquiv g (NonNegative n) = do + viaFixed <- runFixed + viaEmbed <- runEmbed + return (viaFixed == reference && viaEmbed == reference) + where + reqs = replicate n () + reference = snd (mapAccumL (\a () -> g a) 0 reqs) + + client = reqRespClientPeerPipelined (reqRespClientMapPipelined reqs) + + -- a fresh stateful reply source (so each run starts from the same state) + mkNextResp = do + accVar <- newTVarIO 0 + return $ atomically $ do + a <- readTVar accVar + let (a', r) = g a + writeTVar accVar a' + return r + + runFixed = do + nextResp <- mkNextResp + (resps, ()) <- runConnectedPeersLookaheadFixedSender + (createPipelineTestChannels 100) nullTracer CBOR.codecReqResp + client (reqRespServerPeerLookaheadFixedSender nextResp) + return resps + + runEmbed = do + nextResp <- mkNextResp + (resps, ()) <- runConnectedPeersLookahead + (createPipelineTestChannels 100) nullTracer CBOR.codecReqResp + client (embedLookaheadUsingFixedSender (reqRespServerPeerLookaheadFixedSender nextResp)) + return resps + +prop_lookaheadFixedEquiv_IO :: (Int -> (Int, Int)) -> NonNegative Int -> Property +prop_lookaheadFixedEquiv_IO g n = + ioProperty (prop_lookaheadFixedEquiv g n) + +prop_lookaheadFixedEquiv_ST :: (Int -> (Int, Int)) -> NonNegative Int -> Property +prop_lookaheadFixedEquiv_ST g n = + let tr = runSimTrace (prop_lookaheadFixedEquiv g n) in + counterexample (intercalate "\n" $ map show $ traceEvents tr) + $ case traceResult True tr of + Left err -> throw err + Right res -> res + + #if !defined(mingw32_HOST_OS) prop_namedPipePipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] -> Property @@ -315,14 +483,14 @@ (AnyMessage MsgDone) == (AnyMessage MsgDone) = True _ == _ = False -prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Bool +prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Property prop_codec_ReqResp = prop_codec runIdentity codecReqResp prop_codec_splits2_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_splits2_ReqResp = prop_codec_splits splits2 @@ -330,7 +498,7 @@ codecReqResp prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_splits3_ReqResp = prop_codec_splits splits3 @@ -339,13 +507,13 @@ prop_codec_cbor_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_cbor_ReqResp msg = runST $ prop_codecM CBOR.codecReqResp msg prop_codec_cbor_splits2_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_cbor_splits2_ReqResp msg = runST $ prop_codec_splitsM splits2BS @@ -354,9 +522,22 @@ prop_codec_cbor_splits3_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_cbor_splits3_ReqResp msg = runST $ prop_codec_splitsM splits3BS CBOR.codecReqResp msg + + +instance (Show a, Arbitrary a) => Arbitrary (WithBytes a) where + arbitrary = mkWithBytes <$> arbitrary + shrink WithBytes { message } = mkWithBytes <$> shrink message + +prop_anncodec_ReqResp + :: AnyMessage (ReqResp (WithBytes Int) (WithBytes Int)) + -> Property +prop_anncodec_ReqResp = + prop_anncodec + runIdentity + anncodecReqResp diff --git a/typed-protocols.cabal b/typed-protocols.cabal --- a/typed-protocols.cabal +++ b/typed-protocols.cabal @@ -1,40 +1,32 @@ cabal-version: 3.4 name: typed-protocols -version: 1.0.0.0 +version: 1.2.2.0 synopsis: A framework for strongly typed protocols description: A robust session type framework which supports protocol pipelining. + Haddocks are published [here](https://intersectmbo.github.io/typed-protocols/) license: Apache-2.0 -license-files: - LICENSE - NOTICE -copyright: 2019-2025 Input Output Global Inc (IOG) +license-files: LICENSE NOTICE +copyright: 2019-2026 Input Output Global Inc (IOG), 2026 Intersect author: Alexander Vieth, Duncan Coutts, Marcin Szamotulski maintainer: alex@well-typed.com, duncan@well-typed.com, marcin.szamotulski@iohk.io category: Control build-type: Simple -tested-with: GHC == {9.6, 9.8, 9.10, 9.12} +tested-with: GHC == {9.6, 9.8, 9.10, 9.12, 9.14} extra-doc-files: CHANGELOG.md README.md +bug-reports: https://github.com/intersectmbo/typed-protocols/issues -library - exposed-modules: Network.TypedProtocol - , Network.TypedProtocol.Core - , Network.TypedProtocol.Peer - , Network.TypedProtocol.Peer.Client - , Network.TypedProtocol.Peer.Server - , Network.TypedProtocol.Codec - , Network.TypedProtocol.Driver - , Network.TypedProtocol.Proofs - other-modules: Network.TypedProtocol.Lemmas - build-depends: base >=4.12 && <4.22, - io-classes:io-classes ^>= 1.8, - singletons ^>= 3.0 +source-repository head + type: git + location: https://github.com/intersectmbo/typed-protocols + subdir: typed-protocols - hs-source-dirs: src - default-language: GHC2021 - default-extensions: DataKinds - GADTs - LambdaCase +-- Minimal GHC setup, additional extensions are enabled per package (e.g. +-- pervasive type level extensions in the code base like `GADTs` or +-- `DataKinds`, etc), or per module (e.g. `CPP` or other more exotic ones). +common GHC + default-language: GHC2021 + default-extensions: LambdaCase ghc-options: -Wall -Wno-unticked-promoted-constructors -Wcompat @@ -43,33 +35,59 @@ -Wpartial-fields -Widentities -Wredundant-constraints + -Wunused-packages -library cborg - visibility: public - exposed-modules: Network.TypedProtocol.Codec.CBOR + -- In ghc-9.14 the `pattern` namespace specifier is deprecated. + if impl(ghc >=9.14) + ghc-options: + -Wno-pattern-namespace-specifier - build-depends: base, - bytestring >=0.10 && <0.13, - cborg >=0.2.1 && <0.3, - singletons, - primitive, +library + import: GHC + exposed-modules: Network.TypedProtocol + , Network.TypedProtocol.Core + , Network.TypedProtocol.Peer + , Network.TypedProtocol.Peer.Client + , Network.TypedProtocol.Peer.Server + , Network.TypedProtocol.Codec + , Network.TypedProtocol.Driver + , Network.TypedProtocol.Proofs + other-modules: Network.TypedProtocol.Lemmas + build-depends: base >=4.12 && <4.23, + deepseq, + io-classes:io-classes >=1.8 && <1.12 , + singletons ^>= 3.0 + hs-source-dirs: src + default-extensions: DataKinds + GADTs - io-classes:io-classes, - typed-protocols:typed-protocols +library codec-properties + import: GHC + visibility: public + exposed-modules: Network.TypedProtocol.Codec.Properties + Network.TypedProtocol.Stateful.Codec.Properties + other-modules: Test.QuickCheck.Monoids.Compat + build-depends: base >=4.12 && <4.23, + typed-protocols:{stateful, typed-protocols}, + QuickCheck + hs-source-dirs: properties + default-extensions: GADTs + ImportQualifiedPost - hs-source-dirs: cborg - default-language: GHC2021 - default-extensions: LambdaCase - ghc-options: -Wall - -Wno-unticked-promoted-constructors - -Wcompat - -Wincomplete-uni-patterns - -Wincomplete-record-updates - -Wpartial-fields - -Widentities - -Wredundant-constraints +library cborg + import: GHC + visibility: public + exposed-modules: Network.TypedProtocol.Codec.CBOR + build-depends: base, + bytestring >=0.10 && <0.13, + cborg >=0.2.1 && <0.3, + io-classes:io-classes, + typed-protocols:typed-protocols + hs-source-dirs: cborg + library stateful + import: GHC visibility: public exposed-modules: Network.TypedProtocol.Stateful.Peer , Network.TypedProtocol.Stateful.Peer.Client @@ -78,127 +96,94 @@ , Network.TypedProtocol.Stateful.Proofs , Network.TypedProtocol.Stateful.Codec build-depends: base, + deepseq, singletons, io-classes:io-classes, typed-protocols:typed-protocols - hs-source-dirs: stateful - default-language: GHC2021 default-extensions: DataKinds GADTs ImportQualifiedPost - ghc-options: -Wall - -Wno-unticked-promoted-constructors - -Wcompat - -Wincomplete-uni-patterns - -Wincomplete-record-updates - -Wpartial-fields - -Widentities - -Wredundant-constraints library stateful-cborg - visibility: public - exposed-modules: Network.TypedProtocol.Stateful.Codec.CBOR - - build-depends: base, - bytestring, - cborg, - singletons, + import: GHC + visibility: public + exposed-modules: Network.TypedProtocol.Stateful.Codec.CBOR - io-classes:io-classes, - typed-protocols:{typed-protocols,cborg,stateful} + build-depends: base, + bytestring, + cborg, - hs-source-dirs: stateful-cborg - default-language: GHC2021 + io-classes:io-classes, + typed-protocols:{typed-protocols,cborg,stateful} + hs-source-dirs: stateful-cborg default-extensions: ImportQualifiedPost - ghc-options: -Wall - -Wno-unticked-promoted-constructors - -Wcompat - -Wincomplete-uni-patterns - -Wincomplete-record-updates - -Wpartial-fields - -Widentities - -Wredundant-constraints library examples - visibility: public - exposed-modules: Network.TypedProtocol.Channel - , Network.TypedProtocol.Driver.Simple - - , Network.TypedProtocol.PingPong.Type - , Network.TypedProtocol.PingPong.Client - , Network.TypedProtocol.PingPong.Server - , Network.TypedProtocol.PingPong.Codec - , Network.TypedProtocol.PingPong.Codec.CBOR - , Network.TypedProtocol.PingPong.Examples + import: GHC + visibility: public + exposed-modules: Network.TypedProtocol.Channel + , Network.TypedProtocol.Driver.Simple - , Network.TypedProtocol.ReqResp.Type - , Network.TypedProtocol.ReqResp.Client - , Network.TypedProtocol.ReqResp.Server - , Network.TypedProtocol.ReqResp.Codec - , Network.TypedProtocol.ReqResp.Codec.CBOR - , Network.TypedProtocol.ReqResp.Examples + , Network.TypedProtocol.PingPong.Type + , Network.TypedProtocol.PingPong.Client + , Network.TypedProtocol.PingPong.Server + , Network.TypedProtocol.PingPong.Codec + , Network.TypedProtocol.PingPong.Codec.CBOR + , Network.TypedProtocol.PingPong.Examples - , Network.TypedProtocol.ReqResp2.Type - , Network.TypedProtocol.ReqResp2.Client + , Network.TypedProtocol.ReqResp.Type + , Network.TypedProtocol.ReqResp.Client + , Network.TypedProtocol.ReqResp.Server + , Network.TypedProtocol.ReqResp.Codec + , Network.TypedProtocol.ReqResp.Codec.CBOR + , Network.TypedProtocol.ReqResp.Examples - , Network.TypedProtocol.Stateful.ReqResp.Type - , Network.TypedProtocol.Stateful.ReqResp.Client - , Network.TypedProtocol.Stateful.ReqResp.Server - , Network.TypedProtocol.Stateful.ReqResp.Codec - , Network.TypedProtocol.Stateful.ReqResp.Examples + , Network.TypedProtocol.ReqResp2.Type + , Network.TypedProtocol.ReqResp2.Client - , Network.TypedProtocol.Trans.Wedge - build-depends: base, - bytestring, - cborg, - serialise, - singletons, - contra-tracer, - io-classes:{io-classes, si-timers}, - network, - time, - typed-protocols:{typed-protocols,cborg,stateful} + , Network.TypedProtocol.Stateful.ReqResp.Type + , Network.TypedProtocol.Stateful.ReqResp.Client + , Network.TypedProtocol.Stateful.ReqResp.Server + , Network.TypedProtocol.Stateful.ReqResp.Codec + , Network.TypedProtocol.Stateful.ReqResp.Examples - hs-source-dirs: examples - default-language: GHC2021 + , Network.TypedProtocol.Trans.Wedge + build-depends: base, + bytestring, + cborg, + deepseq, + serialise, + singletons, + contra-tracer, + io-classes:{io-classes, si-timers}, + typed-protocols:{typed-protocols,cborg,stateful} + if !os(windows) + build-depends: network + hs-source-dirs: examples default-extensions: DataKinds GADTs - LambdaCase - ghc-options: -Wall - -Wno-unticked-promoted-constructors - -Wcompat - -Wincomplete-uni-patterns - -Wincomplete-record-updates - -Wpartial-fields - -Widentities - -Wredundant-constraints test-suite test - type: exitcode-stdio-1.0 - main-is: Main.hs - hs-source-dirs: test - default-language: GHC2021 + import: GHC + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test default-extensions: GADTs - LambdaCase - other-modules: Network.TypedProtocol.PingPong.Tests - , Network.TypedProtocol.ReqResp.Tests - build-depends: base - , bytestring - , contra-tracer - , typed-protocols:{typed-protocols,cborg,examples} - , io-classes:{io-classes,si-timers} - , io-sim - , QuickCheck - , tasty - , tasty-quickcheck - + other-modules: Network.TypedProtocol.PingPong.Tests + , Network.TypedProtocol.ReqResp.Tests + build-depends: base + , bytestring + , contra-tracer + , transformers + , typed-protocols:{typed-protocols,codec-properties,examples} + , io-classes:io-classes + , io-sim + , QuickCheck + , tasty + , tasty-quickcheck if !os(windows) build-depends: directory , network , unix - - ghc-options: -rtsopts - -Wall - -Wno-unticked-promoted-constructors - -Wno-orphans + ghc-options: -rtsopts