typed-protocols 1.0.0.0 → 1.2.2.0
raw patch · 26 files changed
Files
- CHANGELOG.md +40/−0
- NOTICE +1/−1
- README.md +3/−3
- cborg/Network/TypedProtocol/Codec/CBOR.hs +16/−14
- examples/Network/TypedProtocol/Driver/Simple.hs +163/−13
- examples/Network/TypedProtocol/PingPong/Codec.hs +2/−0
- examples/Network/TypedProtocol/ReqResp/Codec.hs +70/−2
- examples/Network/TypedProtocol/ReqResp/Server.hs +56/−0
- examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs +1/−2
- examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs +1/−1
- properties/Network/TypedProtocol/Codec/Properties.hs +573/−0
- properties/Network/TypedProtocol/Stateful/Codec/Properties.hs +154/−0
- properties/Test/QuickCheck/Monoids/Compat.hs +85/−0
- src/Network/TypedProtocol/Codec.hs +88/−210
- src/Network/TypedProtocol/Core.hs +29/−6
- src/Network/TypedProtocol/Driver.hs +226/−6
- src/Network/TypedProtocol/Peer.hs +92/−1
- src/Network/TypedProtocol/Peer/Client.hs +4/−1
- src/Network/TypedProtocol/Peer/Server.hs +126/−1
- src/Network/TypedProtocol/Proofs.hs +127/−0
- stateful/Network/TypedProtocol/Stateful/Codec.hs +4/−125
- stateful/Network/TypedProtocol/Stateful/Driver.hs +19/−6
- stateful/Network/TypedProtocol/Stateful/Peer.hs +3/−3
- test/Network/TypedProtocol/PingPong/Tests.hs +19/−8
- test/Network/TypedProtocol/ReqResp/Tests.hs +193/−12
- typed-protocols.cabal +126/−141
CHANGELOG.md view
@@ -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`.
NOTICE view
@@ -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.
README.md view
@@ -1,5 +1,5 @@-[](https://github.com/input-output-hk/typed-protocols/actions/workflows/haskell.yml)-[](https://input-output-hk.github.io/cardano-engineering-handbook)+[](https://github.com/intersectmbo/typed-protocols/actions/workflows/haskell.yml)+[](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
cborg/Network/TypedProtocol/Codec/CBOR.hs view
@@ -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
examples/Network/TypedProtocol/Driver/Simple.hs view
@@ -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)
examples/Network/TypedProtocol/PingPong/Codec.hs view
@@ -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)
examples/Network/TypedProtocol/ReqResp/Codec.hs view
@@ -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
examples/Network/TypedProtocol/ReqResp/Server.hs view
@@ -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')
examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs view
@@ -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 =
examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs view
@@ -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
+ properties/Network/TypedProtocol/Codec/Properties.hs view
@@ -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
+ properties/Network/TypedProtocol/Stateful/Codec/Properties.hs view
@@ -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
+ properties/Test/QuickCheck/Monoids/Compat.hs view
@@ -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
src/Network/TypedProtocol/Codec.hs view
@@ -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
src/Network/TypedProtocol/Core.hs view
@@ -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'.
src/Network/TypedProtocol/Driver.hs view
@@ -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
src/Network/TypedProtocol/Peer.hs view
@@ -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)
src/Network/TypedProtocol/Peer/Client.hs view
@@ -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
src/Network/TypedProtocol/Peer/Server.hs view
@@ -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 #-}
src/Network/TypedProtocol/Proofs.hs view
@@ -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
stateful/Network/TypedProtocol/Stateful/Codec.hs view
@@ -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
stateful/Network/TypedProtocol/Stateful/Driver.hs view
@@ -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
stateful/Network/TypedProtocol/Stateful/Peer.hs view
@@ -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
test/Network/TypedProtocol/PingPong/Tests.hs view
@@ -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
test/Network/TypedProtocol/ReqResp/Tests.hs view
@@ -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
typed-protocols.cabal view
@@ -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