From 78d6c6dbcd201adcc8eca701ef53a1f932be3164 Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 28 Jul 2025 10:59:40 +0200 Subject: [PATCH 1/5] Generalised Codec to provide AnnotatedCodec --- typed-protocols/CHANGELOG.md | 14 + .../cborg/Network/TypedProtocol/Codec/CBOR.hs | 30 +- .../src/Network/TypedProtocol/Codec.hs | 486 +++++++++++++++--- .../Network/TypedProtocol/Stateful/Codec.hs | 2 + 4 files changed, 450 insertions(+), 82 deletions(-) diff --git a/typed-protocols/CHANGELOG.md b/typed-protocols/CHANGELOG.md index 2fa7a36..701f7b7 100644 --- a/typed-protocols/CHANGELOG.md +++ b/typed-protocols/CHANGELOG.md @@ -1,5 +1,19 @@ # Revision history for typed-protocols +## next release + +### 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`. + +### Non-breaking changes + +## 1.0.0.0 + +* Hackage release. + ## 0.3.0.0 * `AnyMessageWithAgency` pattern synonym is exported as a constructor of `AnyMessage`. diff --git a/typed-protocols/cborg/Network/TypedProtocol/Codec/CBOR.hs b/typed-protocols/cborg/Network/TypedProtocol/Codec/CBOR.hs index a0ff3a2..b948390 100644 --- a/typed-protocols/cborg/Network/TypedProtocol/Codec/CBOR.hs +++ b/typed-protocols/cborg/Network/TypedProtocol/Codec/CBOR.hs @@ -25,10 +25,10 @@ import Network.TypedProtocol.Codec 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 @@ import Network.TypedProtocol.Core -- 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 @@ mkCodecCborStrictBS -> (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 @@ mkCodecCborStrictBS cborMsgEncode cborMsgDecode = . 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 @@ convertCborDecoderBS cborDecode liftST = 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 @@ mkCodecCborLazyBS -> (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,11 +127,12 @@ mkCodecCborLazyBS cborMsgEncode cborMsgDecode = . 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 => CBOR.Decoder s a diff --git a/typed-protocols/src/Network/TypedProtocol/Codec.hs b/typed-protocols/src/Network/TypedProtocol/Codec.hs index 7fdf440..a7e71ea 100644 --- a/typed-protocols/src/Network/TypedProtocol/Codec.hs +++ b/typed-protocols/src/Network/TypedProtocol/Codec.hs @@ -8,7 +8,12 @@ module Network.TypedProtocol.Codec ( -- * Defining and using Codecs -- ** Codec type - Codec (..) + CodecF (..) + , Codec + , Annotator (..) + , AnnotatedCodec + , hoistAnnotation + , unAnnotateCodec , hoistCodec , isoCodec , mapFailureCodec @@ -36,6 +41,7 @@ module Network.TypedProtocol.Codec -- * CodecFailure , CodecFailure (..) -- * Testing codec properties + -- ** Codec , AnyMessage (AnyMessage, AnyMessageAndAgency) , prop_codecM , prop_codec @@ -45,6 +51,28 @@ module Network.TypedProtocol.Codec , prop_codec_binary_compat , prop_codecs_compatM , prop_codecs_compat + + -- ** AnnotatedCodec + , 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 + , prop_codecFM + , prop_codecF + , prop_codecF_splitsM + , prop_codecF_splits + , prop_codecF_binary_compatM + , prop_codecF_binary_compat + , prop_codecsF_compatM + , prop_codecsF_compat + + -- ** SomeState , SomeState (..) ) where @@ -66,10 +94,21 @@ import Network.TypedProtocol.Driver (SomeMessage (..)) -- * 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 +162,77 @@ import Network.TypedProtocol.Driver (SomeMessage (..)) -- 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 +244,9 @@ isoCodec :: Functor m -- ^ 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 +258,8 @@ mapFailureCodec :: 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 +292,11 @@ data DecodeStep bytes failure m a = -- @'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') @@ -348,6 +435,31 @@ getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateTok getAgency msg = (msg, stateToken) +-- | 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) + ) + => (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 Bool +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 _ -> False + + -- | The 'Codec' round-trip property: decode after encode gives the same -- message. Every codec must satisfy this property. -- @@ -362,11 +474,35 @@ prop_codecM -- ^ 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 +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) + ) + => AnnotatedCodec ps failure m bytes + -- ^ annotated codec + -> AnyMessage ps + -- ^ some message + -> m Bool +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)) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Bool +prop_codecF runF runM codec msg = runM (prop_codecFM runF codec msg) -- | The 'Codec' round-trip property in a pure monad. -- @@ -377,8 +513,44 @@ prop_codec -> Codec ps failure m bytes -> AnyMessage ps -> Bool -prop_codec runM codec msg = - runM (prop_codecM codec msg) +prop_codec = prop_codecF const + + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_anncodec + :: forall ps failure m bytes. + (Monad m, Eq (AnyMessage ps)) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Bool +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), 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 Bool +prop_codecF_splitsM runF splits + Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do + and <$> 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 _ -> return False + + | let bytes = encode msg + , bytes' <- splits bytes ] -- | A variant on the codec round-trip property: given the encoding of a @@ -394,37 +566,66 @@ prop_codec runM codec msg = -- prop_codec_splitsM :: forall ps failure m bytes. - (Monad m, Eq (AnyMessage ps)) + (Monad m, Eq (AnyMessage ps), Monoid bytes) => (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 +prop_codec_splitsM = prop_codecF_splitsM const - | let bytes = encode msg - , bytes' <- splits bytes ] +-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'. +-- +prop_anncodec_splitsM + :: forall ps failure m bytes. + (Monad m, Eq (AnyMessage ps), Monoid bytes) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> m Bool +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), 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 + -> Bool +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)) + (Monad m, Eq (AnyMessage ps), Monoid bytes) => (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 +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), Monoid bytes) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Bool +prop_anncodec_splits = prop_codecF_splits runAnnotator -- | Auxiliary definition for 'prop_codec_binary_compatM'. @@ -440,6 +641,47 @@ data SomeState (ps :: Type) where -- ^ state token for some active state 'st' -> SomeState ps +-- | 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) + ) + => (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 Bool +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 _ -> return 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 _ -> return 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: @@ -464,29 +706,47 @@ prop_codec_binary_compatM -- ^ 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 +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) + ) + => 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 Bool +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) + ) + => (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 + -> Bool +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 @@ -499,9 +759,59 @@ prop_codec_binary_compat -- ^ 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 +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) + ) + => (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 + -> Bool +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) + , 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 Bool +prop_codecsF_compatM runF codecA codecB + (AnyMessage (msg :: Message ps st st')) = + + getAll <$> 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 $! All $ AnyMessage msg' == AnyMessage msg + Left _ -> return $! All 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 $! All $ AnyMessage msg' == AnyMessage msg + Left _ -> return $! All 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 @@ -520,16 +830,42 @@ prop_codecs_compatM -> 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 +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) + , 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 Bool +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) + , 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 + -> Bool +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@. -- @@ -544,5 +880,19 @@ prop_codecs_compat -> Codec ps failure m bytes -> AnyMessage ps -> Bool -prop_codecs_compat run codecA codecB msg = - run $ prop_codecs_compatM codecA codecB msg +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) + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Bool +prop_anncodecs_compat = prop_codecsF_compat runAnnotator diff --git a/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs b/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs index 84f5c23..572466a 100644 --- a/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs +++ b/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs @@ -55,6 +55,8 @@ import Network.TypedProtocol.Core -- | 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 From cc1e72eda46f3715d39bb20090c8428728629e23 Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 21 Jul 2025 13:11:45 +0200 Subject: [PATCH 2/5] typed-protocols:codec-properties library Moved `prop_codec` properties to a sublibrary. All properties return QuickCheck's `Property` type. --- cabal.project | 6 +- typed-protocols-doc/typed-protocols-doc.cabal | 2 +- typed-protocols/CHANGELOG.md | 2 + .../Network/TypedProtocol/Codec/Properties.hs | 561 ++++++++++++++++++ .../Stateful/Codec/Properties.hs | 150 +++++ .../src/Network/TypedProtocol/Codec.hs | 479 --------------- .../Network/TypedProtocol/Stateful/Codec.hs | 123 ---- .../Network/TypedProtocol/PingPong/Tests.hs | 13 +- .../Network/TypedProtocol/ReqResp/Tests.hs | 13 +- typed-protocols/typed-protocols.cabal | 14 +- 10 files changed, 746 insertions(+), 617 deletions(-) create mode 100644 typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs create mode 100644 typed-protocols/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs diff --git a/cabal.project b/cabal.project index 6e1a548..9a445df 100644 --- a/cabal.project +++ b/cabal.project @@ -1,4 +1,4 @@ -index-state: 2025-05-21T15:48:46Z +index-state: 2025-07-08T15:23:02Z packages: ./typed-protocols ./typed-protocols-doc @@ -10,6 +10,10 @@ if impl(ghc >= 9.12) , serdoc-core:template-haskell , serdoc-core:th-abstraction +allow-newer: + , serdoc-core:QuickCheck + , serdoc-core:tasty-quickcheck + if os(windows) package text flags: -simdutf diff --git a/typed-protocols-doc/typed-protocols-doc.cabal b/typed-protocols-doc/typed-protocols-doc.cabal index 373d50d..93c6c00 100644 --- a/typed-protocols-doc/typed-protocols-doc.cabal +++ b/typed-protocols-doc/typed-protocols-doc.cabal @@ -89,7 +89,7 @@ test-suite typed-protocols-doc-test build-depends: base >=4.14.0.0 && <5 , blaze-html >=0.9.1.2 && <0.10 , tasty >=1.5 && <1.6 - , tasty-quickcheck >=0.10.3 && <0.11 + , tasty-quickcheck >=0.10.3 && <0.12 , typed-protocols , typed-protocols-doc , serdoc-core diff --git a/typed-protocols/CHANGELOG.md b/typed-protocols/CHANGELOG.md index 701f7b7..2ebc336 100644 --- a/typed-protocols/CHANGELOG.md +++ b/typed-protocols/CHANGELOG.md @@ -7,6 +7,8 @@ * 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). ### Non-breaking changes diff --git a/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs b/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs new file mode 100644 index 0000000..f31b28f --- /dev/null +++ b/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs @@ -0,0 +1,561 @@ +{-# 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 + + +-- | 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. +-- +prop_anncodec + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + ) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodec = prop_codecF runAnnotator + + +-- | A more general version of 'prop_codec_splitsM' for 'CodecF'. +-- +prop_codecF_splitsM + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> m Property +prop_codecF_splitsM runF splits + Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do + property . foldMap Every <$> sequence + [ do r <- decode stateToken >>= runDecoder bytes' + case r :: Either failure (f st) of + Right f -> case runF f (mconcat bytes') of + SomeMessage msg' -> + return $! AnyMessage msg' === AnyMessage msg + Left err -> return $ counterexample (show err) False + + | let bytes = encode msg + , bytes' <- splits bytes ] + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> Codec ps failure m bytes + -> AnyMessage ps + -> m Property +prop_codec_splitsM = prop_codecF_splitsM const + +-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'. +-- +prop_anncodec_splitsM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> m Property +prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator + + +-- | A more general version of 'prop_codec_splits' for 'CodecF'. +-- +prop_codecF_splits + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Property +prop_codecF_splits runF splits runM codec msg = + runM $ prop_codecF_splitsM runF splits codec msg + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> Codec ps failure m bytes + -> AnyMessage ps + -> Property +prop_codec_splits = prop_codecF_splits const + +-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'. +prop_anncodec_splits + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , Monoid bytes + ) + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form + -> (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodec_splits = prop_codecF_splits runAnnotator + +-- | A more general version of 'prop_codec_binary_compatM' for 'CodecF'. +-- +prop_codecF_binary_compatM + :: forall psA psB failure m fA fB bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall (st :: psA). fA st -> bytes -> SomeMessage st) + -> (forall (st :: psB). fB st -> bytes -> SomeMessage st) + -> CodecF psA failure m fA bytes + -> CodecF psB failure m fB bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_codecF_binary_compatM + runFA runFB codecA codecB stokEq + (AnyMessage (msgA :: Message psA stA stA')) = + let stokA :: StateToken stA + stokA = stateToken + in case stokEq stokA of + SomeState (stokB :: StateToken stB) -> do + -- 1. + let bytesA = encode codecA msgA + -- 2. + r1 <- decode codecB stokB >>= runDecoder [bytesA] + case r1 :: Either failure (fB stB) of + Left err -> return $ counterexample (show err) False + Right fB -> + case runFB fB bytesA of + (SomeMessage msgB) -> do + -- 3. + let bytesB = encode codecB msgB + -- 4. + r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB] + case r2 :: Either failure (fA stA) of + Left err -> return $ counterexample (show err) False + Right fA -> + case runFA fA bytesB of + SomeMessage msgA' -> return $ AnyMessage msgA' === AnyMessage msgA + +-- | Binary compatibility of two protocols +-- +-- We check the following property: +-- +-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@. +-- +-- 2. When we decode those @bytes@ using codec B, we get a message of protocol +-- @ps@B. +-- +-- 3. When we encode that message again using codec B, we get @bytes@. +-- +-- 4. When we decode those @bytes@ using codec A, we get the original message +-- again. +prop_codec_binary_compatM + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_codec_binary_compatM = prop_codecF_binary_compatM const const + + +-- | A version of 'prop_codec_binary_compatM' for 'AnnotatedCodec'. +-- +prop_anncodec_binary_compatM + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => AnnotatedCodec psA failure m bytes + -> AnnotatedCodec psB failure m bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Property +prop_anncodec_binary_compatM = prop_codecF_binary_compatM runAnnotator runAnnotator + + +-- | A more general version of 'prop_codec_binary_compat' for 'CodecF'. +-- +prop_codecF_binary_compat + :: forall psA psB failure m fA fB bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall (st :: psA). fA st -> bytes -> SomeMessage st) + -> (forall (st :: psB). fB st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF psA failure m fA bytes + -> CodecF psB failure m fB bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_codecF_binary_compat runFA runFB runM codecA codecB stokEq msg = + runM $ prop_codecF_binary_compatM runFA runFB codecA codecB stokEq msg + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_binary_compat + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall a. m a -> a) + -> Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_codec_binary_compat = + prop_codecF_binary_compat const const + +-- | A 'prop_codec_binary_compat' version for 'AnnotatedCodec'. +-- +prop_anncodec_binary_compat + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + , Show (AnyMessage psA) + , Show failure + ) + => (forall a. m a -> a) + -> AnnotatedCodec psA failure m bytes + -> AnnotatedCodec psB failure m bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Property +prop_anncodec_binary_compat runM codecA codecB stokEq msgA = + runM $ prop_anncodec_binary_compatM codecA codecB stokEq msgA + + +-- | A more general version of 'prop_codecs_compatM' for 'CodecF'. +-- +prop_codecsF_compatM + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> CodecF ps failure m f bytes + -- ^ first codec + -> CodecF ps failure m f bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_codecsF_compatM runF codecA codecB + (AnyMessage (msg :: Message ps st st')) = + + property + <$> do let bytes = encode codecA msg + r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [bytes] + case r :: Either failure (f st) of + Right f -> case runF f bytes of + SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg + Left err -> return $! Every $ counterexample (show err) False + + <> do let bytes = encode codecB msg + r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [bytes] + case r :: Either failure (f st) of + Right f -> case runF f bytes of + SomeMessage msg' -> return $! Every $ AnyMessage msg' === AnyMessage msg + Left err -> return $! Every $ counterexample (show err) False + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => Codec ps failure m bytes + -- ^ first codec + -> Codec ps failure m bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_codecs_compatM = prop_codecsF_compatM const + +-- | A version of 'prop_codec_compatM' for 'AnnotatedCodec'. +-- +prop_anncodecs_compatM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => AnnotatedCodec ps failure m bytes + -- ^ first codec + -> AnnotatedCodec ps failure m bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Property +prop_anncodecs_compatM = prop_codecsF_compatM runAnnotator + + +-- | A more general version of 'prop_codecs_compat' for 'CodecF'. +-- +prop_codecsF_compat + :: forall ps failure m f bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall (st :: ps). f st -> bytes -> SomeMessage st) + -> (forall a. m a -> a) + -> CodecF ps failure m f bytes + -> CodecF ps failure m f bytes + -> AnyMessage ps + -> Property +prop_codecsF_compat runF runM codecA codecB msg = + runM $ prop_codecsF_compatM runF codecA codecB msg + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> Codec ps failure m bytes + -> Codec ps failure m bytes + -> AnyMessage ps + -> Property +prop_codecs_compat = prop_codecsF_compat const + +-- | A version of 'prop_codecs_compat' for 'AnnotatedCodec'. +-- +prop_anncodecs_compat + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , Show (AnyMessage ps) + , Show failure + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> AnnotatedCodec ps failure m bytes + -> AnnotatedCodec ps failure m bytes + -> AnyMessage ps + -> Property +prop_anncodecs_compat = prop_codecsF_compat runAnnotator diff --git a/typed-protocols/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs b/typed-protocols/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs new file mode 100644 index 0000000..d177304 --- /dev/null +++ b/typed-protocols/properties/Network/TypedProtocol/Stateful/Codec/Properties.hs @@ -0,0 +1,150 @@ +{-# 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 + + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' === a + Left err -> return $ counterexample (show err) False + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_codec + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codec runM codec msg = + runM (prop_codecM codec msg) + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codec_splitsM splits + Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + property . foldMap Every <$> sequence + [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' === a + Left err -> return $ counterexample (show err) False + + | let bytes = encode f msg + , bytes' <- splits bytes ] + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , Show failure + ) + => (bytes -> [[bytes]]) + -> (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codec_splits splits runM codec msg = + runM $ prop_codec_splitsM splits codec msg + + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + , Show failure + ) + => Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Property +prop_codecs_compatM codecA codecB + a@(AnyMessage f (msg :: Message ps st st')) = + property + <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' === a + Left err -> return $ Every $ counterexample (show err) False + <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ Every $ AnyMessage f msg' == a + Left _ -> return $ Every False + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , Show (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + , Show failure + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Property +prop_codecs_compat run codecA codecB msg = + run $ prop_codecs_compatM codecA codecB msg diff --git a/typed-protocols/src/Network/TypedProtocol/Codec.hs b/typed-protocols/src/Network/TypedProtocol/Codec.hs index a7e71ea..7b707c6 100644 --- a/typed-protocols/src/Network/TypedProtocol/Codec.hs +++ b/typed-protocols/src/Network/TypedProtocol/Codec.hs @@ -43,42 +43,12 @@ module Network.TypedProtocol.Codec -- * 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 - - -- ** AnnotatedCodec - , 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 - , prop_codecFM - , prop_codecF - , prop_codecF_splitsM - , prop_codecF_splits - , prop_codecF_binary_compatM - , prop_codecF_binary_compat - , prop_codecsF_compatM - , prop_codecsF_compat - -- ** SomeState , SomeState (..) ) where import Control.Exception (Exception) import Data.Kind (Type) -import Data.Monoid (All (..)) import Network.TypedProtocol.Core import Network.TypedProtocol.Driver (SomeMessage (..)) @@ -435,199 +405,6 @@ getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateTok getAgency msg = (msg, stateToken) --- | 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) - ) - => (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 Bool -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 _ -> 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) - ) - => Codec ps failure m bytes - -- ^ codec - -> AnyMessage ps - -- ^ some message - -> m Bool - -- ^ 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) - ) - => AnnotatedCodec ps failure m bytes - -- ^ annotated codec - -> AnyMessage ps - -- ^ some message - -> m Bool -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)) - => (forall (st :: ps). f st -> bytes -> SomeMessage st) - -> (forall a. m a -> a) - -> CodecF ps failure m f bytes - -> AnyMessage ps - -> Bool -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)) - => (forall a. m a -> a) - -> Codec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_codec = prop_codecF const - - --- | The 'Codec' round-trip property in a pure monad. --- -prop_anncodec - :: forall ps failure m bytes. - (Monad m, Eq (AnyMessage ps)) - => (forall a. m a -> a) - -> AnnotatedCodec ps failure m bytes - -> AnyMessage ps - -> Bool -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), 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 Bool -prop_codecF_splitsM runF splits - Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do - and <$> 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 _ -> return 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), Monoid bytes) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> Codec ps failure m bytes - -> AnyMessage ps - -> m Bool -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), Monoid bytes) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> AnnotatedCodec ps failure m bytes - -> AnyMessage ps - -> m Bool -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), 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 - -> Bool -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), Monoid bytes) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> (forall a. m a -> a) - -> Codec ps failure m bytes - -> AnyMessage ps - -> Bool -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), Monoid bytes) - => (bytes -> [[bytes]]) - -- ^ alternative re-chunkings of serialised form - -> (forall a. m a -> a) - -> AnnotatedCodec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_anncodec_splits = prop_codecF_splits runAnnotator - - -- | Auxiliary definition for 'prop_codec_binary_compatM'. -- -- Used for the existential @st :: ps@ parameter when expressing that for each @@ -640,259 +417,3 @@ data SomeState (ps :: Type) where => StateToken st -- ^ state token for some active state 'st' -> SomeState ps - --- | 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) - ) - => (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 Bool -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 _ -> return 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 _ -> return 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) - ) - => 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 = 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) - ) - => 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 Bool -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) - ) - => (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 - -> Bool -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) - ) - => (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 = - 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) - ) - => (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 - -> Bool -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) - , 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 Bool -prop_codecsF_compatM runF codecA codecB - (AnyMessage (msg :: Message ps st st')) = - - getAll <$> 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 $! All $ AnyMessage msg' == AnyMessage msg - Left _ -> return $! All 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 $! All $ AnyMessage msg' == AnyMessage msg - Left _ -> return $! All 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) - , 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 = 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) - , 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 Bool -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) - , 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 - -> Bool -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) - , 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 = 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) - , forall a. Monoid a => Monoid (m a) - ) - => (forall a. m a -> a) - -> AnnotatedCodec ps failure m bytes - -> AnnotatedCodec ps failure m bytes - -> AnyMessage ps - -> Bool -prop_anncodecs_compat = prop_codecsF_compat runAnnotator diff --git a/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs b/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs index 572466a..7371006 100644 --- a/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs +++ b/typed-protocols/stateful/Network/TypedProtocol/Stateful/Codec.hs @@ -35,16 +35,9 @@ module Network.TypedProtocol.Stateful.Codec -- * 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, @@ -179,119 +172,3 @@ pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, -- getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st) getAgency msg = (msg, stateToken) - - --- | The 'Codec' round-trip property: decode after encode gives the same --- message. Every codec must satisfy this property. --- -prop_codecM - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - ) - => Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do - r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ AnyMessage f msg' == a - Left _ -> return False - --- | The 'Codec' round-trip property in a pure monad. --- -prop_codec - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (forall a. m a -> a) - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codec runM codec msg = - runM (prop_codecM codec msg) - - --- | A variant on the codec round-trip property: given the encoding of a --- message, check that decode always gives the same result irrespective --- of how the chunks of input are fed to the incremental decoder. --- --- This property guards against boundary errors in incremental decoders. --- It is not necessary to check this for every message type, just for each --- generic codec construction. For example given some binary serialisation --- library one would write a generic adaptor to the codec interface. This --- adaptor has to deal with the incremental decoding and this is what needs --- to be checked. --- -prop_codec_splitsM - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codec_splitsM splits - Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do - and <$> sequence - [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ AnyMessage f msg' == a - Left _ -> return False - - | let bytes = encode f msg - , bytes' <- splits bytes ] - - --- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codec_splits - :: forall ps failure f m bytes. - (Monad m, Eq (AnyMessage ps f)) - => (bytes -> [[bytes]]) - -> (forall a. m a -> a) - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codec_splits splits runM codec msg = - runM $ prop_codec_splitsM splits codec msg - - --- | Compatibility between two codecs of the same protocol. Encode a message --- with one codec and decode it with the other one, then compare if the result --- is the same as initial message. --- -prop_codecs_compatM - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - , forall a. Monoid a => Monoid (m a) - ) - => Codec ps failure f m bytes - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> m Bool -prop_codecs_compatM codecA codecB - a@(AnyMessage f (msg :: Message ps st st')) = - getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a - Left _ -> return $ All False - <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg] - case r :: Either failure (SomeMessage st) of - Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a - Left _ -> return $ All False - --- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. --- -prop_codecs_compat - :: forall ps failure f m bytes. - ( Monad m - , Eq (AnyMessage ps f) - , forall a. Monoid a => Monoid (m a) - ) - => (forall a. m a -> a) - -> Codec ps failure f m bytes - -> Codec ps failure f m bytes - -> AnyMessage ps f - -> Bool -prop_codecs_compat run codecA codecB msg = - run $ prop_codecs_compatM codecA codecB msg diff --git a/typed-protocols/test/Network/TypedProtocol/PingPong/Tests.hs b/typed-protocols/test/Network/TypedProtocol/PingPong/Tests.hs index 2a48679..96c31f1 100644 --- a/typed-protocols/test/Network/TypedProtocol/PingPong/Tests.hs +++ b/typed-protocols/test/Network/TypedProtocol/PingPong/Tests.hs @@ -13,6 +13,7 @@ module Network.TypedProtocol.PingPong.Tests import Network.TypedProtocol.Channel import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.Properties import Network.TypedProtocol.Driver.Simple import Network.TypedProtocol.Proofs @@ -390,20 +391,20 @@ instance Eq (AnyMessage PingPong) where 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 +417,13 @@ prop_codec_splits3_PingPong = 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 +432,7 @@ prop_codec_cbor_splits2_PingPong msg = prop_codec_cbor_splits3_PingPong :: AnyMessage PingPong - -> Bool + -> Property prop_codec_cbor_splits3_PingPong msg = runST $ prop_codec_splitsM splits3BS diff --git a/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs b/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs index 3916c69..513d62e 100644 --- a/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs +++ b/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs @@ -6,6 +6,7 @@ module Network.TypedProtocol.ReqResp.Tests (tests) where import Network.TypedProtocol.Channel import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.Properties import Network.TypedProtocol.Driver.Simple import Network.TypedProtocol.Proofs @@ -314,14 +315,14 @@ instance (Eq req, Eq resp) => Eq (AnyMessage (ReqResp req resp)) where (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 @@ -329,7 +330,7 @@ prop_codec_splits2_ReqResp = codecReqResp prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_splits3_ReqResp = prop_codec_splits splits3 @@ -338,13 +339,13 @@ prop_codec_splits3_ReqResp = 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 @@ -353,7 +354,7 @@ prop_codec_cbor_splits2_ReqResp msg = prop_codec_cbor_splits3_ReqResp :: AnyMessage (ReqResp String String) - -> Bool + -> Property prop_codec_cbor_splits3_ReqResp msg = runST $ prop_codec_splitsM splits3BS diff --git a/typed-protocols/typed-protocols.cabal b/typed-protocols/typed-protocols.cabal index 5951b40..f7d5d25 100644 --- a/typed-protocols/typed-protocols.cabal +++ b/typed-protocols/typed-protocols.cabal @@ -51,6 +51,18 @@ library default-extensions: DataKinds GADTs +library codec-properties + import: GHC + visibility: public + exposed-modules: Network.TypedProtocol.Codec.Properties + Network.TypedProtocol.Stateful.Codec.Properties + build-depends: base >=4.12 && <4.22, + typed-protocols:{stateful, typed-protocols}, + QuickCheck >= 2.16 + hs-source-dirs: properties + default-extensions: GADTs + ImportQualifiedPost + library cborg import: GHC visibility: public @@ -150,7 +162,7 @@ test-suite test build-depends: base , bytestring , contra-tracer - , typed-protocols:{typed-protocols,examples} + , typed-protocols:{typed-protocols,codec-properties,examples} , io-classes:io-classes , io-sim , QuickCheck From ee44dd027647395b71a2903a3869f604560e596b Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 21 Jul 2025 13:23:11 +0200 Subject: [PATCH 3/5] typed-protocols:test - added prop_anncodec for ReqResp mini-protocol --- typed-protocols/CHANGELOG.md | 3 +- .../Network/TypedProtocol/ReqResp/Codec.hs | 64 +++++++++++++++++++ .../Network/TypedProtocol/Codec/Properties.hs | 8 +++ .../Network/TypedProtocol/ReqResp/Tests.hs | 16 +++++ 4 files changed, 90 insertions(+), 1 deletion(-) diff --git a/typed-protocols/CHANGELOG.md b/typed-protocols/CHANGELOG.md index 2ebc336..886840f 100644 --- a/typed-protocols/CHANGELOG.md +++ b/typed-protocols/CHANGELOG.md @@ -8,7 +8,8 @@ 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). + (`Network.TypedProtocol.Codec.Properties` module). They now return the + `QuickCheck`'s `Property` rather than a `Bool`. ### Non-breaking changes diff --git a/typed-protocols/examples/Network/TypedProtocol/ReqResp/Codec.hs b/typed-protocols/examples/Network/TypedProtocol/ReqResp/Codec.hs index ae61427..17b0f79 100644 --- a/typed-protocols/examples/Network/TypedProtocol/ReqResp/Codec.hs +++ b/typed-protocols/examples/Network/TypedProtocol/ReqResp/Codec.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE BlockArguments #-} + module Network.TypedProtocol.ReqResp.Codec where import Network.TypedProtocol.Codec @@ -43,6 +45,68 @@ codecReqResp = 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 + + (_ , _ ) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + + codecReqRespId :: forall req resp m . (Monad m, Show req, Show resp) diff --git a/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs b/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs index f31b28f..9686dae 100644 --- a/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs +++ b/typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs @@ -136,6 +136,14 @@ 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 diff --git a/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs b/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs index 513d62e..c161e2c 100644 --- a/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs +++ b/typed-protocols/test/Network/TypedProtocol/ReqResp/Tests.hs @@ -73,6 +73,9 @@ tests = testGroup "Network.TypedProtocol.ReqResp" , testProperty "codec 3-splits" $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp ] ] + , testGroup "AnnotatedCodec" + [ testProperty "codec" prop_anncodec_ReqResp + ] ] @@ -360,3 +363,16 @@ prop_codec_cbor_splits3_ReqResp msg = 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 From da96ddeab7712bb96cf46bb02f95aeacf6f25dda Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Sat, 26 Jul 2025 18:56:08 +0200 Subject: [PATCH 4/5] typed-protocols: bump version --- typed-protocols-doc/typed-protocols-doc.cabal | 2 +- typed-protocols/CHANGELOG.md | 2 +- typed-protocols/typed-protocols.cabal | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/typed-protocols-doc/typed-protocols-doc.cabal b/typed-protocols-doc/typed-protocols-doc.cabal index 93c6c00..3155502 100644 --- a/typed-protocols-doc/typed-protocols-doc.cabal +++ b/typed-protocols-doc/typed-protocols-doc.cabal @@ -54,7 +54,7 @@ library , th-abstraction >=0.6.0.0 && <0.8 , time >=1.12 && <1.14 , serdoc-core - , typed-protocols ^>= 1.0 + , typed-protocols ^>= 1.0 || ^>= 1.1 hs-source-dirs: src default-language: GHC2021 default-extensions: DataKinds diff --git a/typed-protocols/CHANGELOG.md b/typed-protocols/CHANGELOG.md index 886840f..6442966 100644 --- a/typed-protocols/CHANGELOG.md +++ b/typed-protocols/CHANGELOG.md @@ -1,6 +1,6 @@ # Revision history for typed-protocols -## next release +## 1.1.0.0 -- 05.08.2025 ### Breaking changes diff --git a/typed-protocols/typed-protocols.cabal b/typed-protocols/typed-protocols.cabal index f7d5d25..e1a7faf 100644 --- a/typed-protocols/typed-protocols.cabal +++ b/typed-protocols/typed-protocols.cabal @@ -1,6 +1,6 @@ cabal-version: 3.4 name: typed-protocols -version: 1.0.0.0 +version: 1.1.0.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/) From ee05d80e86420471bb1af65536cbd4cae0d924ba Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 28 Jul 2025 12:29:05 +0200 Subject: [PATCH 5/5] Updated stylish-haskell to 0.14.6.0 --- .github/workflows/haskell.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml index 6f4bca6..f4fc4b1 100644 --- a/.github/workflows/haskell.yml +++ b/.github/workflows/haskell.yml @@ -100,7 +100,7 @@ jobs: runs-on: ubuntu-22.04 env: - STYLISH_HASKELL_VERSION: "0.14.4.0" + STYLISH_HASKELL_VERSION: "0.14.6.0" steps: - name: Set cache version @@ -116,8 +116,8 @@ jobs: uses: haskell-actions/setup@v2 id: setup-haskell with: - ghc-version: 9.2.5 - cabal-version: 3.8.1.0 + ghc-version: 9.8 + cabal-version: 3.12.1.0 - name: "Setup cabal bin path" run: |