packages feed

typed-protocols 1.0.0.0 → 1.2.1.0

raw patch · 16 files changed

Files

CHANGELOG.md view
@@ -1,5 +1,35 @@ # Revision history for typed-protocols +## 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`.
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'@.@@ -30,6 +31,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 +74,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 +125,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 +151,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@@ -159,16 +176,22 @@ -- | 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 +206,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 +230,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@@ -225,8 +260,12 @@ -- 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/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 =
+ 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/Driver.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP          #-} {-# LANGUAGE TypeFamilies #-}  -- | Actions for running 'Peer's with a 'Driver'@@ -20,9 +21,11 @@ import Network.TypedProtocol.Peer  import Control.Concurrent.Class.MonadSTM.TQueue+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@@ -114,9 +117,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 +144,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,18 +183,23 @@ -- 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
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@@ -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) @@ -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
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 @@ -289,7 +290,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 +396,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 +422,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 +437,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 @@ -21,7 +22,6 @@ import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM import Control.Monad.Class.MonadThrow-import Control.Monad.Class.MonadTimer.SI import Control.Monad.IOSim import Control.Monad.ST (runST) import Control.Tracer (nullTracer)@@ -73,6 +73,9 @@       , testProperty "codec 3-splits"  $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp       ]     ]+  , testGroup "AnnotatedCodec"+    [ testProperty "codec"             prop_anncodec_ReqResp+    ]   ]  @@ -169,7 +172,12 @@ -- 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 +200,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@@ -315,14 +327,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 +342,7 @@       codecReqResp  prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String)-                           -> Bool+                           -> Property prop_codec_splits3_ReqResp =     prop_codec_splits       splits3@@ -339,13 +351,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 +366,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,26 @@ cabal-version:       3.4 name:                typed-protocols-version:             1.0.0.0+version:             1.2.1.0 synopsis:            A framework for strongly typed protocols description:         A robust session type framework which supports protocol pipelining.+                     Haddocks are published [here](https://input-output-hk.github.io/typed-protocols/) license:             Apache-2.0-license-files:-  LICENSE-  NOTICE+license-files:       LICENSE NOTICE copyright:           2019-2025 Input Output Global Inc (IOG) 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 -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--  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 +29,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.9 || ^>= 1.10,+                      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 +90,93 @@                     , 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+                    , 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