diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,41 @@ +# Revision history for typed-protocols + +## 0.3.0.0 + +* `AnyMessageWithAgency` pattern synonym is exported as a constructor of `AnyMessage`. +* Bumped version to agree with `typed-protocols-stateful`. + +## 0.2.0.0 + +* A major redesign of `typed-protocols`. + * `Protocol` class does not require to provide proof obligations for agency. + Proofs are now provided by the framework for all protocols. Agency is now + provided by an associated type family `StateAgency`, and evidence for it, + in form of a singleton, by `StateToken` type family + (similar to `Sing` from the `singletons` package). + * `Peer` takes a different evidence type for agency, + `Network.TypedProtocol.Peer.{Client,Server}` modules provide pattern synonyms + which provide agency evidence and thus are easier to use. + * One `Peer` is provided for both non- and pipelined protocol evolution. + An extra parameter is added of kind `IsPipelined`. As a result + `Outstanding` is now a type family rather than a type alias. + * `ActiveAgency` type class is used to distinguish states in which one side + has an agency (e.g. the protocol hasn't yet terminated), `nonActiveState` can + be used in the same way as `Data.Void.absurd` - which is useful when writing + codecs. + +## 0.1.1.1 +* unbuildable (with `base < 0` constraint in CHaP); We cannot support +`io-classes-1.{6,7}` until `Haskell.Nix` support for public sublibraries is + merged. + +## 0.1.0.7 -- 2023-10-20 + +* Improved performance of `prop_codecs_splitsM` and `prop_codecs_compatM`. + +## 0.1.0.5 -- 2023-03-08 + +* Support `ghc-9.6.1`. +* Use `io-classes-1.1.0.0`. + +[singletons-3.0.1]: https://hackage.haskell.org/package/singletons diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,177 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/NOTICE b/NOTICE new file mode 100644 --- /dev/null +++ b/NOTICE @@ -0,0 +1,14 @@ +Copyright 2019-2025 Input Output Global Inc (IOG) + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,39 @@ +[![Haskell CI](https://img.shields.io/github/actions/workflow/status/input-output-hk/typed-protocols/haskell.yml?branch=main&label=Build&style=for-the-badge)](https://github.com/input-output-hk/typed-protocols/actions/workflows/haskell.yml) +[![handbook](https://img.shields.io/badge/policy-Cardano%20Engineering%20Handbook-informational?style=for-the-badge)](https://input-output-hk.github.io/cardano-engineering-handbook) + + +typed-protocols +=============== + + +A robust session type framework which supports [protocol pipelining][protocol-pipelining]. + +Haddocks are published [here][haddocks]. + + +Public content +-------------- + +[Duncan Coutts][dcoutts] Haskell eXchange 2019 [talk][haskell-eXchange]. + +Monadic party workshop by Marcin Szamotulski ([coot]): +* [part 1][monadic-party-part-1] +* [part 2][monadic-party-part-2] +* [part 2][monadic-party-part-3] + +Talk at [Haskell Love 2021][haskell-love] by Marcin Szamotulski ([coot]), [slides][haskell-love-slides]. + +An [Agda][typed-protocols-agda] implementation by Marcin Szamotulski ([coot]). + + +[protocol-pipelining]: https://www.wikiwand.com/en/Protocol_pipelining +[haskell-eXchange]: https://www.youtube.com/watch?v=kkynmgwa7gE +[monadic-party-part-1]: https://www.youtube.com/watch?v=j8gza2L61nM +[monadic-party-part-2]: https://www.youtube.com/watch?v=oV6KSl1srL8 +[monadic-party-part-3]: https://www.youtube.com/watch?v=nOIQCRPwmPA +[haskell-love-slides]: https://coot.me/posts/typed-protocols-at-haskell-love.html +[haskell-love]: https://www.youtube.com/watch?v=EbK6VAqYh3g +[typed-protocols-agda]: https://coot.me/agda/posts.agda.typed-protocols.html +[coot]: https://github.com/coot +[dcoutts]: https://github.com/dcoutts +[haddocks]: https://input-output-hk.github.io/typed-protocols diff --git a/cborg/Network/TypedProtocol/Codec/CBOR.hs b/cborg/Network/TypedProtocol/Codec/CBOR.hs new file mode 100644 --- /dev/null +++ b/cborg/Network/TypedProtocol/Codec/CBOR.hs @@ -0,0 +1,174 @@ +module Network.TypedProtocol.Codec.CBOR + ( module Network.TypedProtocol.Codec + , mkCodecCborLazyBS + , mkCodecCborStrictBS + , convertCborDecoderBS + , convertCborDecoderLBS + -- * Re-exports + , CBOR.DeserialiseFailure (..) + ) where + +import Control.Monad.Class.MonadST (MonadST (..)) +import Control.Monad.ST hiding (stToIO) + +import Codec.CBOR.Decoding qualified as CBOR (Decoder) +import Codec.CBOR.Encoding qualified as CBOR (Encoding) +import Codec.CBOR.Read qualified as CBOR +import Codec.CBOR.Write qualified as CBOR +import Data.ByteString qualified as BS +import Data.ByteString.Builder qualified as BS +import Data.ByteString.Builder.Extra qualified as BS +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Internal qualified as LBS (smallChunkSize) + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core + + +-- | Construct a 'Codec' for a CBOR based serialisation format, using strict +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- +-- It takes encode and decode functions for the protocol messages that use the +-- CBOR library encoder and decoder. +-- +-- Note that this is /less/ efficient than the 'mkCodecCborLazyBS' variant +-- because it has to copy and concatenate the result of the encoder (which +-- natively produces chunks). +-- +mkCodecCborStrictBS + :: forall ps m. MonadST m + + => (forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps CBOR.DeserialiseFailure m BS.ByteString +mkCodecCborStrictBS cborMsgEncode cborMsgDecode = + Codec { + encode = \msg -> convertCborEncoder cborMsgEncode msg, + decode = \stok -> convertCborDecoder (cborMsgDecode stok) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString + convertCborEncoder cborEncode = + CBOR.toStrictByteString + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderBS cborDecode stToIO + +convertCborDecoderBS + :: forall s m a. Functor m + => CBOR.Decoder s a + -- ^ cbor decoder + -> (forall b. ST s b -> m b) + -- ^ lift ST computation (e.g. 'Control.Monad.ST.stToIO', 'stToPrim', etc) + -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a) +convertCborDecoderBS cborDecode liftST = + go <$> liftST (CBOR.deserialiseIncremental cborDecode) + where + go :: CBOR.IDecode s a + -> DecodeStep BS.ByteString CBOR.DeserialiseFailure m a + go (CBOR.Done trailing _ x) + | BS.null trailing = DecodeDone x Nothing + | otherwise = DecodeDone x (Just trailing) + go (CBOR.Fail _ _ failure) = DecodeFail failure + go (CBOR.Partial k) = DecodePartial (fmap go . liftST . k) + + +-- | Construct a 'Codec' for a CBOR based serialisation format, using lazy +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' 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 (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps CBOR.DeserialiseFailure m LBS.ByteString +mkCodecCborLazyBS cborMsgEncode cborMsgDecode = + Codec { + encode = \msg -> convertCborEncoder cborMsgEncode msg, + decode = \stok -> convertCborDecoder (cborMsgDecode stok) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> LBS.ByteString + convertCborEncoder cborEncode = + toLazyByteString + . CBOR.toBuilder + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderLBS cborDecode stToIO + +convertCborDecoderLBS + :: forall s m a. Monad m + => CBOR.Decoder s a + -- ^ cbor decoder + -> (forall b. ST s b -> m b) + -- ^ lift ST computation (e.g. 'Control.Monad.ST.stToIO', 'stToPrim', etc) + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) +convertCborDecoderLBS cborDecode liftST = + go [] =<< liftST (CBOR.deserialiseIncremental cborDecode) + where + -- Have to mediate between a CBOR decoder that consumes strict bytestrings + -- and our choice here that consumes lazy bytestrings. + go :: [BS.ByteString] -> CBOR.IDecode s a + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) + go [] (CBOR.Done trailing _ x) + | BS.null trailing = return (DecodeDone x Nothing) + | otherwise = return (DecodeDone x (Just trailing')) + where trailing' = LBS.fromStrict trailing + go cs (CBOR.Done trailing _ x) = return (DecodeDone x (Just trailing')) + where trailing' = LBS.fromChunks (trailing : cs) + go _ (CBOR.Fail _ _ e) = return (DecodeFail e) + + -- We keep a bunch of chunks and supply the CBOR decoder with them + -- until we run out, when we go get another bunch. + go (c:cs) (CBOR.Partial k) = go cs =<< liftST (k (Just c)) + go [] (CBOR.Partial k) = return $ DecodePartial $ \case + Nothing -> go [] =<< liftST (k Nothing) + Just bs -> go cs (CBOR.Partial k) + where cs = LBS.toChunks bs + +{-# NOINLINE toLazyByteString #-} +toLazyByteString :: BS.Builder -> LBS.ByteString +toLazyByteString = BS.toLazyByteStringWith strategy LBS.empty + where + -- Buffer strategy and sizes better tuned to our network protocol situation. + -- + -- The LBS.smallChunkSize is 4k - heap object overheads, so that + -- it does fit in a 4k overall. + -- + strategy = BS.untrimmedStrategy 800 LBS.smallChunkSize + diff --git a/examples/Network/TypedProtocol/Channel.hs b/examples/Network/TypedProtocol/Channel.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Channel.hs @@ -0,0 +1,332 @@ +{-# LANGUAGE CPP #-} + +module Network.TypedProtocol.Channel + ( Channel (..) + , hoistChannel + , isoKleisliChannel + , fixedInputChannel + , mvarsAsChannel + , handlesAsChannel +#if !defined(mingw32_HOST_OS) + , socketAsChannel +#endif + , createConnectedChannels + , createConnectedBufferedChannels + , createConnectedBufferedChannelsUnbounded + , createPipelineTestChannels + , channelEffect + , delayChannel + , loggingChannel + ) where + +import Control.Concurrent.Class.MonadSTM +import Control.Monad ((>=>)) +import Control.Monad.Class.MonadSay +import Control.Monad.Class.MonadTimer.SI +import Data.ByteString qualified as BS +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Internal (smallChunkSize) +import Data.Proxy +import Numeric.Natural + +#if !defined(mingw32_HOST_OS) +import Network.Socket (Socket) +import Network.Socket.ByteString.Lazy qualified as Socket +#endif + +import System.IO qualified as IO (Handle, hFlush, hIsEOF) + + +-- | One end of a duplex channel. It is a reliable, ordered channel of some +-- medium. The medium does not imply message boundaries, it can be just bytes. +-- +data Channel m a = Channel { + + -- | Write output to the channel. + -- + -- It may raise exceptions (as appropriate for the monad and kind of + -- channel). + -- + send :: a -> m (), + + -- | Read some input from the channel, or @Nothing@ to indicate EOF. + -- + -- Note that having received EOF it is still possible to send. + -- The EOF condition is however monotonic. + -- + -- It may raise exceptions (as appropriate for the monad and kind of + -- channel). + -- + recv :: m (Maybe a) + } + + +-- | Given an isomorphism between @a@ and @b@ (in Kleisli category), transform +-- a @'Channel' m a@ into @'Channel' m b@. +-- +isoKleisliChannel + :: forall a b m. Monad m + => (a -> m b) + -> (b -> m a) + -> Channel m a + -> Channel m b +isoKleisliChannel f finv Channel{send, recv} = Channel { + send = finv >=> send, + recv = recv >>= traverse f + } + + +hoistChannel + :: (forall x . m x -> n x) + -> Channel m a + -> Channel n a +hoistChannel nat channel = Channel + { send = nat . send channel + , recv = nat (recv channel) + } + +-- | A 'Channel' with a fixed input, and where all output is discarded. +-- +-- The input is guaranteed to be supplied via 'read' with the given chunk +-- boundaries. +-- +-- This is only useful for testing. In particular the fixed chunk boundaries +-- can be used to test that framing and other codecs work with any possible +-- chunking. +-- +fixedInputChannel :: MonadSTM m => [a] -> m (Channel m a) +fixedInputChannel xs0 = do + v <- atomically $ newTVar xs0 + return Channel {send, recv = recv v} + where + recv v = atomically $ do + xs <- readTVar v + case xs of + [] -> return Nothing + (x:xs') -> writeTVar v xs' >> return (Just x) + + send _ = return () + + +-- | Make a 'Channel' from a pair of 'TMVar's, one for reading and one for +-- writing. +-- +mvarsAsChannel :: MonadSTM m + => TMVar m a + -> TMVar m a + -> Channel m a +mvarsAsChannel bufferRead bufferWrite = + Channel{send, recv} + where + send x = atomically (putTMVar bufferWrite x) + recv = atomically (Just <$> takeTMVar bufferRead) + + +-- | Create a pair of channels that are connected via one-place buffers. +-- +-- This is primarily useful for testing protocols. +-- +createConnectedChannels :: forall m a. (MonadLabelledSTM m, MonadTraceSTM m, Show a) => m (Channel m a, Channel m a) +createConnectedChannels = do + -- Create two TMVars to act as the channel buffer (one for each direction) + -- and use them to make both ends of a bidirectional channel + bufferA <- atomically $ do + v <- newEmptyTMVar + labelTMVar v "buffer-a" + traceTMVar (Proxy @m) v $ \_ a -> pure $ TraceString ("buffer-a: " ++ show a) + return v + bufferB <- atomically $ do + v <- newEmptyTMVar + traceTMVar (Proxy @m) v $ \_ a -> pure $ TraceString ("buffer-b: " ++ show a) + labelTMVar v "buffer-b" + return v + + return (mvarsAsChannel bufferB bufferA, + mvarsAsChannel bufferA bufferB) + + +-- | Create a pair of channels that are connected via N-place buffers. +-- +-- This variant /blocks/ when 'send' would exceed the maximum buffer size. +-- Use this variant when you want the environment rather than the 'Peer' to +-- limit the pipelining. +-- +-- This is primarily useful for testing protocols. +-- +createConnectedBufferedChannels :: MonadSTM m + => Natural -> m (Channel m a, Channel m a) +createConnectedBufferedChannels sz = do + -- Create two TBQueues to act as the channel buffers (one for each + -- direction) and use them to make both ends of a bidirectional channel + bufferA <- atomically $ newTBQueue sz + bufferB <- atomically $ newTBQueue sz + + return (queuesAsChannel bufferB bufferA, + queuesAsChannel bufferA bufferB) + where + queuesAsChannel bufferRead bufferWrite = + Channel{send, recv} + where + send x = atomically (writeTBQueue bufferWrite x) + recv = atomically (Just <$> readTBQueue bufferRead) + + +-- | Create a pair of channels that are connected via two unbounded buffers. +-- +-- This is primarily useful for testing protocols. +-- +createConnectedBufferedChannelsUnbounded :: forall m a. MonadSTM m + => m (Channel m a, Channel m a) +createConnectedBufferedChannelsUnbounded = do + -- Create two TQueues to act as the channel buffers (one for each + -- direction) and use them to make both ends of a bidirectional channel + bufferA <- newTQueueIO + bufferB <- newTQueueIO + + return (queuesAsChannel bufferB bufferA, + queuesAsChannel bufferA bufferB) + where + queuesAsChannel bufferRead bufferWrite = + Channel{send, recv} + where + send x = atomically (writeTQueue bufferWrite x) + recv = atomically ( Just <$> readTQueue bufferRead) + +-- | Create a pair of channels that are connected via N-place buffers. +-- +-- This variant /fails/ when 'send' would exceed the maximum buffer size. +-- Use this variant when you want the 'Peer' to limit the pipelining itself, +-- and you want to check that it does not exceed the expected level of +-- pipelining. +-- +-- This is primarily useful for testing protocols. +-- +createPipelineTestChannels :: MonadSTM m + => Natural -> m (Channel m a, Channel m a) +createPipelineTestChannels sz = do + -- Create two TBQueues to act as the channel buffers (one for each + -- direction) and use them to make both ends of a bidirectional channel + bufferA <- atomically $ newTBQueue sz + bufferB <- atomically $ newTBQueue sz + + return (queuesAsChannel bufferB bufferA, + queuesAsChannel bufferA bufferB) + where + queuesAsChannel bufferRead bufferWrite = + Channel{send, recv} + where + send x = atomically $ do + full <- isFullTBQueue bufferWrite + if full then error failureMsg + else writeTBQueue bufferWrite x + recv = atomically (Just <$> readTBQueue bufferRead) + + failureMsg = "createPipelineTestChannels: " + ++ "maximum pipeline depth exceeded: " ++ show sz + + +-- | Make a 'Channel' from a pair of IO 'Handle's, one for reading and one +-- for writing. +-- +-- The Handles should be open in the appropriate read or write mode, and in +-- binary mode. Writes are flushed after each write, so it is safe to use +-- a buffering mode. On unix named pipes can be used, see +-- 'Network.TypedProtocol.ReqResp.Test.prop_namedPipePipelined_IO' +-- +-- For bidirectional handles it is safe to pass the same handle for both. +-- +handlesAsChannel :: IO.Handle -- ^ Read handle + -> IO.Handle -- ^ Write handle + -> Channel IO LBS.ByteString +handlesAsChannel hndRead hndWrite = + Channel{send, recv} + where + send :: LBS.ByteString -> IO () + send chunk = do + LBS.hPut hndWrite chunk + IO.hFlush hndWrite + + recv :: IO (Maybe LBS.ByteString) + recv = do + eof <- IO.hIsEOF hndRead + if eof + then return Nothing + else Just . LBS.fromStrict <$> BS.hGetSome hndRead smallChunkSize + + +-- | Transform a channel to add an extra action before /every/ send and after +-- /every/ receive. +-- +channelEffect :: forall m a. + Monad m + => (a -> m ()) -- ^ Action before 'send' + -> (Maybe a -> m ()) -- ^ Action after 'recv' + -> Channel m a + -> Channel m a +channelEffect beforeSend afterRecv Channel{send, recv} = + Channel{ + send = \x -> do + beforeSend x + send x + + , recv = do + mx <- recv + afterRecv mx + return mx + } + +-- | Delay a channel on the receiver end. +-- +-- This is intended for testing, as a crude approximation of network delays. +-- More accurate models along these lines are of course possible. +-- +delayChannel :: MonadDelay m + => DiffTime + -> Channel m a + -> Channel m a +delayChannel delay = channelEffect (\_ -> return ()) + (\_ -> threadDelay delay) + + +#if !defined(mingw32_HOST_OS) +socketAsChannel :: Socket + -> Channel IO LBS.ByteString +socketAsChannel sock = + Channel{send, recv} + where + send :: LBS.ByteString -> IO () + send = Socket.sendAll sock + + recv :: IO (Maybe LBS.ByteString) + recv = do + bs <- Socket.recv sock (fromIntegral smallChunkSize) + if LBS.null bs + then return Nothing + else return (Just bs) +#endif + +-- | Channel which logs sent and received messages. +-- +loggingChannel :: ( MonadSay m + , Show id + , Show a + ) + => id + -> Channel m a + -> Channel m a +loggingChannel ident Channel{send,recv} = + Channel { + send = loggingSend, + recv = loggingRecv + } + where + loggingSend a = do + say (show ident ++ ":send:" ++ show a) + send a + + loggingRecv = do + msg <- recv + case msg of + Nothing -> return () + Just a -> say (show ident ++ ":recv:" ++ show a) + return msg diff --git a/examples/Network/TypedProtocol/Driver/Simple.hs b/examples/Network/TypedProtocol/Driver/Simple.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Driver/Simple.hs @@ -0,0 +1,246 @@ +{-# LANGUAGE TypeFamilies #-} +-- @UndecidableInstances@ extensions is required for defining @Show@ instance +-- of @'TraceSendRecv'@. +{-# LANGUAGE UndecidableInstances #-} + +-- | Drivers for running 'Peer's with a 'Codec' and a 'Channel'. +-- +module Network.TypedProtocol.Driver.Simple + ( -- * Introduction + -- $intro + -- * Normal peers + runPeer + , TraceSendRecv (..) + , Role (..) + -- * Pipelined peers + , runPipelinedPeer + -- * Connected peers + , runConnectedPeers + , runConnectedPeersPipelined + , runConnectedPeersAsymmetric + -- * Driver utilities + -- | This may be useful if you want to write your own driver. + , driverSimple + , runDecoderWithChannel + ) where + +import Network.TypedProtocol.Channel +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core +import Network.TypedProtocol.Driver +import Network.TypedProtocol.Peer + +import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadThrow +import Control.Tracer (Tracer (..), contramap, traceWith) + + +-- $intro +-- +-- A 'Peer' is a particular implementation of an agent that engages in a +-- typed protocol. To actualy run one we need a source and sink for the typed +-- protocol messages. These are provided by a 'Channel' and a 'Codec'. The +-- 'Channel' represents one end of an untyped duplex message transport, and +-- the 'Codec' handles conversion between the typed protocol messages and +-- the untyped channel. +-- +-- So given the 'Peer' and a compatible 'Codec' and 'Channel' we can run the +-- peer in some appropriate monad. The peer and codec have to agree on +-- the same protocol and role in that protocol. The codec and channel have to +-- agree on the same untyped medium, e.g. text or bytes. All three have to +-- agree on the same monad in which they will run. +-- +-- This module provides drivers for normal and pipelined peers. There is +-- very little policy involved here so typically it should be possible to +-- use these drivers, and customise things by adjusting the peer, or codec +-- or channel. +-- +-- It is of course possible to write custom drivers and the code for these ones +-- may provide a useful starting point. The 'runDecoder' function may be a +-- helpful utility for use in custom drives. +-- + +-- | Structured 'Tracer' output for 'runPeer' and derivitives. +-- +data TraceSendRecv ps where + TraceSendMsg :: AnyMessage ps -> TraceSendRecv ps + TraceRecvMsg :: AnyMessage ps -> TraceSendRecv ps + +instance Show (AnyMessage ps) => Show (TraceSendRecv ps) where + show (TraceSendMsg msg) = "Send " ++ show msg + show (TraceRecvMsg msg) = "Recv " ++ show msg + + +driverSimple :: forall ps pr failure bytes m. + (MonadThrow m, Exception failure) + => Tracer m (TraceSendRecv ps) + -> Codec ps failure m bytes + -> Channel m bytes + -> Driver ps pr (Maybe bytes) m +driverSimple tracer Codec{encode, decode} channel@Channel{send} = + Driver { sendMessage, recvMessage, initialDState = Nothing } + where + sendMessage :: forall (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => ReflRelativeAgency (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) + -> Message ps st st' + -> m () + sendMessage !_refl msg = do + send (encode msg) + traceWith tracer (TraceSendMsg (AnyMessage msg)) + + recvMessage :: forall (st :: ps). + ( StateTokenI st + , ActiveState st + ) + => ReflRelativeAgency (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) + -> Maybe bytes + -> m (SomeMessage st, Maybe bytes) + recvMessage !_refl trailing = do + decoder <- decode stateToken + result <- runDecoderWithChannel channel trailing decoder + case result of + Right x@(SomeMessage msg, _trailing') -> do + traceWith tracer (TraceRecvMsg (AnyMessage msg)) + return x + Left failure -> + throwIO failure + + +-- | Run a peer with the given channel via the given codec. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +runPeer + :: forall ps (st :: ps) pr failure bytes m a. + (MonadThrow m, Exception failure) + => Tracer m (TraceSendRecv ps) + -> Codec ps failure m bytes + -> Channel m bytes + -> Peer ps pr 'NonPipelined st m a + -> m (a, Maybe bytes) +runPeer tracer codec channel peer = + runPeerWithDriver driver peer + where + driver = driverSimple tracer codec channel + + +-- | Run a pipelined peer with the given channel via the given codec. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +-- Unlike normal peers, running pipelined peers rely on concurrency, hence the +-- 'MonadSTM' constraint. +-- +runPipelinedPeer + :: forall ps (st :: ps) pr failure bytes m a. + (MonadAsync m, MonadThrow m, Exception failure) + => Tracer m (TraceSendRecv ps) + -> Codec ps failure m bytes + -> Channel m bytes + -> PeerPipelined ps pr st m a + -> m (a, Maybe bytes) +runPipelinedPeer tracer codec channel peer = + runPipelinedPeerWithDriver driver peer + where + driver = driverSimple tracer codec channel + + +-- +-- Utils +-- + +-- | Run a codec incremental decoder 'DecodeStep' against a channel. It also +-- takes any extra input data and returns any unused trailing data. +-- +runDecoderWithChannel :: Monad m + => Channel m bytes + -> Maybe bytes + -> DecodeStep bytes failure m a + -> m (Either failure (a, Maybe bytes)) + +runDecoderWithChannel Channel{recv} = go + where + go _ (DecodeDone x trailing) = return (Right (x, trailing)) + go _ (DecodeFail failure) = return (Left failure) + go Nothing (DecodePartial k) = recv >>= k >>= go Nothing + go (Just trailing) (DecodePartial k) = k (Just trailing) >>= go Nothing + + +data Role = Client | Server + deriving Show + +-- | Run two 'Peer's via a pair of connected 'Channel's and a common 'Codec'. +-- +-- This is useful for tests and quick experiments. +-- +-- The first argument is expected to create two channels that are connected, +-- for example 'createConnectedChannels'. +-- +runConnectedPeers :: (MonadAsync m, MonadCatch m, + Exception failure) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (Role, TraceSendRecv ps) + -> Codec ps failure m bytes + -> Peer ps pr 'NonPipelined st m a + -> Peer ps (FlipAgency pr) 'NonPipelined st m b + -> m (a, b) +runConnectedPeers createChannels tracer codec client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runPeer tracerServer codec serverChannel server) + where + tracerClient = contramap ((,) Client) tracer + tracerServer = contramap ((,) Server) tracer + +runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m, + Exception failure) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (PeerRole, TraceSendRecv ps) + -> Codec ps failure m bytes + -> PeerPipelined ps pr st m a + -> Peer ps (FlipAgency pr) 'NonPipelined st m b + -> m (a, b) +runConnectedPeersPipelined createChannels tracer codec client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runPeer tracerServer codec serverChannel server) + where + tracerClient = contramap ((,) AsClient) tracer + tracerServer = contramap ((,) AsServer) tracer + + +-- Run the same protocol with different codes. This is useful for testing +-- 'Handshake' protocol which knows how to decode different versions. +-- +runConnectedPeersAsymmetric + :: ( MonadAsync m + , MonadMask m + , Exception failure + ) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (Role, TraceSendRecv ps) + -> Codec ps failure m bytes + -> Codec ps failure m bytes + -> PeerPipelined ps pr st m a + -> Peer ps (FlipAgency pr) 'NonPipelined st m b + -> m (a, b) +runConnectedPeersAsymmetric createChannels tracer codec codec' client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runPeer tracerServer codec' serverChannel server) + where + tracerClient = contramap ((,) Client) tracer + tracerServer = contramap ((,) Server) tracer diff --git a/examples/Network/TypedProtocol/PingPong/Client.hs b/examples/Network/TypedProtocol/PingPong/Client.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Client.hs @@ -0,0 +1,168 @@ +module Network.TypedProtocol.PingPong.Client + ( -- * Normal client + PingPongClient (..) + , pingPongClientPeer + -- * Pipelined client + , PingPongClientPipelined (..) + , PingPongClientIdle (..) + , pingPongClientPeerPipelined + ) where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client +import Network.TypedProtocol.PingPong.Type + +-- | A ping-pong client, on top of some effect 'm'. +-- +-- At each step the client has a choice: ping or stop. +-- +-- This type encodes the pattern of state transitions the client can go through. +-- For the ping\/pong case this is trivial. We start from one main state, +-- issue a ping and move into a state where we expect a single response, +-- bringing us back to the same main state. +-- +-- If we had another state in which a different set of options were available +-- then we would need a second type like this. The two would be mutually +-- recursive if we can get in both directions, or perhaps just one way such +-- as a special initialising state or special terminating state. +-- +data PingPongClient m a where + -- | Choose to go for sending a ping message. The ping has no body so + -- all we have to provide here is a continuation for the single legal + -- reply message. + -- + SendMsgPing :: m (PingPongClient m a) -- continuation for Pong response + -> PingPongClient m a + + -- | Choose to terminate the protocol. This is an actual but nullary message, + -- we terminate with the local result value. So this ends up being much like + -- 'return' in this case, but in general the termination is a message that + -- can communicate final information. + -- + SendMsgDone :: a -> PingPongClient m a + + +-- | Interpret a particular client action sequence into the client side of the +-- 'PingPong' protocol. +-- +pingPongClientPeer + :: Functor m + => PingPongClient m a + -> Client PingPong NonPipelined StIdle m a + +pingPongClientPeer (SendMsgDone result) = + -- We do an actual transition using 'yield', to go from the 'StIdle' to + -- 'StDone' state. Once in the 'StDone' state we can actually stop using + -- 'done', with a return value. + Yield MsgDone (Done result) + +pingPongClientPeer (SendMsgPing next) = + + -- Send our message. + Yield MsgPing $ + + -- The type of our protocol means that we're now into the 'StBusy' state + -- and the only thing we can do next is local effects or wait for a reply. + -- We'll wait for a reply. + Await $ \MsgPong -> + + -- Now in this case there is only one possible response, and we have + -- one corresponding continuation 'kPong' to handle that response. + -- The pong reply has no content so there's nothing to pass to our + -- continuation, but if there were we would. + Effect $ pingPongClientPeer <$> next + + +-- +-- Pipelined client +-- + +-- | A ping-pong client designed for running the 'PingPong' protocol in +-- a pipelined way. +-- +data PingPongClientPipelined c m a where + -- | A 'PingPongSender', but starting with zero outstanding pipelined + -- responses, and for any internal collect type @c@. + PingPongClientPipelined :: + PingPongClientIdle Z c m a + -> PingPongClientPipelined c m a + + +data PingPongClientIdle (n :: N) c m a where + -- | Send a `Ping` message but alike in `PingPongClient` do not await for the + -- response, instead supply a monadic action which will run on a received + -- `Pong` message. + -- + SendMsgPingPipelined + :: m c + -> PingPongClientIdle (S n) c m a -- continuation + -> PingPongClientIdle n c m a + + -- | Collect the result of a previous pipelined receive action. + -- + -- This (optionally) provides two choices: + -- + -- * Continue without a pipelined result + -- * Continue with a pipelined result, which allows to run a monadic action + -- when 'MsgPong' is received. + -- + -- Since presenting the first choice is optional, this allows expressing + -- both a blocking collect and a non-blocking collect. This allows + -- implementations to express policies such as sending a short sequence + -- of messages and then waiting for all replies, but also a maximum pipelining + -- policy that keeps a large number of messages in flight but collects results + -- eagerly. + -- + CollectPipelined + :: Maybe (PingPongClientIdle (S n) c m a) + -> (c -> (PingPongClientIdle n c m a)) + -> PingPongClientIdle (S n) c m a + + -- | Termination of the ping-pong protocol. + -- + -- Note that all pipelined results must be collected before terminating. + -- + SendMsgDonePipelined + :: a -> PingPongClientIdle Z c m a + + + +-- | Interpret a pipelined client as a pipelined 'Peer' on the client side of +-- the 'PingPong' protocol. +-- +pingPongClientPeerPipelined + :: Functor m + => PingPongClientPipelined c m a + -> ClientPipelined PingPong StIdle m a +pingPongClientPeerPipelined (PingPongClientPipelined peer) = + ClientPipelined $ pingPongClientPeerIdle peer + + +pingPongClientPeerIdle + :: forall (n :: N) c m a. Functor m + => PingPongClientIdle n c m a + -> Client PingPong (Pipelined n c) StIdle m a +pingPongClientPeerIdle = go + where + go :: forall (n' :: N). + PingPongClientIdle n' c m a + -> Client PingPong (Pipelined n' c) StIdle m a + + go (SendMsgPingPipelined receive next) = + -- Pipelined yield: send `MsgPing`, immediately follow with the next step. + YieldPipelined + MsgPing + (ReceiverAwait $ \MsgPong -> + ReceiverEffect $ ReceiverDone <$> receive) + (go next) + + go (CollectPipelined mNone collect) = + Collect + (go <$> mNone) + (go . collect) + + go (SendMsgDonePipelined result) = + -- Send `MsgDone` and complete the protocol + Yield + MsgDone + (Done result) diff --git a/examples/Network/TypedProtocol/PingPong/Codec.hs b/examples/Network/TypedProtocol/PingPong/Codec.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Codec.hs @@ -0,0 +1,97 @@ +module Network.TypedProtocol.PingPong.Codec where + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core +import Network.TypedProtocol.PingPong.Type + + +codecPingPong + :: forall m. Monad m + => Codec PingPong CodecFailure m String +codecPingPong = + Codec{encode, decode} + where + encode :: forall (st :: PingPong) (st' :: PingPong). + Message PingPong st st' + -> String + encode MsgPing = "ping\n" + encode MsgDone = "done\n" + encode MsgPong = "pong\n" + + decode :: forall (st :: PingPong). + ActiveState st + => StateToken st + -> m (DecodeStep String CodecFailure m (SomeMessage st)) + decode stok = + decodeTerminatedFrame '\n' $ \str trailing -> + case (stok, str) of + (SingBusy, "pong") -> + DecodeDone (SomeMessage MsgPong) trailing + (SingIdle, "ping") -> + DecodeDone (SomeMessage MsgPing) trailing + (SingIdle, "done") -> + DecodeDone (SomeMessage MsgDone) trailing + + (_ , _ ) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + +decodeTerminatedFrame :: forall m a. + Monad m + => Char + -> (String -> Maybe String -> DecodeStep String CodecFailure m a) + -> m (DecodeStep String CodecFailure m a) +decodeTerminatedFrame terminator k = go [] + where + go :: [String] -> m (DecodeStep String CodecFailure m a) + go chunks = + return $ DecodePartial $ \mchunk -> + case mchunk of + Nothing -> return $ DecodeFail CodecFailureOutOfInput + Just chunk -> + case break (==terminator) chunk of + (c, _:c') -> return $ k (concat (reverse (c:chunks))) + (if null c' then Nothing else Just c) + _ -> go (chunk : chunks) + + + +codecPingPongId + :: forall m. Monad m + => Codec PingPong CodecFailure m (AnyMessage PingPong) +codecPingPongId = + Codec{encode,decode} + where + encode :: forall (st :: PingPong) (st' :: PingPong) + . ( StateTokenI st + , ActiveState st + ) + => Message PingPong st st' + -> AnyMessage PingPong + encode msg = AnyMessage msg + + decode :: forall (st :: PingPong). + ActiveState st + => StateToken st + -> m (DecodeStep (AnyMessage PingPong) CodecFailure m (SomeMessage st)) + decode stok = + pure $ DecodePartial $ \mb -> + case mb of + Nothing -> return $ DecodeFail (CodecFailure "expected more data") + Just (AnyMessage msg) -> return $ + case (stok, msg) of + (SingBusy, MsgPong) -> + DecodeDone (SomeMessage msg) Nothing + (SingIdle, MsgPing) -> + DecodeDone (SomeMessage msg) Nothing + (SingIdle, MsgDone) -> + DecodeDone (SomeMessage msg) Nothing + + (SingIdle, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected client message: " ++ show msg) + (SingBusy, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ show msg) + + (a@SingDone, _) -> notActiveState a diff --git a/examples/Network/TypedProtocol/PingPong/Codec/CBOR.hs b/examples/Network/TypedProtocol/PingPong/Codec/CBOR.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Codec/CBOR.hs @@ -0,0 +1,43 @@ +module Network.TypedProtocol.PingPong.Codec.CBOR where + +import Control.Monad.Class.MonadST + +import Data.ByteString.Lazy (ByteString) + +import Codec.CBOR.Decoding qualified as CBOR (Decoder, decodeWord) +import Codec.CBOR.Encoding qualified as CBOR (Encoding, encodeWord) +import Codec.CBOR.Read qualified as CBOR + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.CBOR +import Network.TypedProtocol.Core +import Network.TypedProtocol.PingPong.Type + +codecPingPong + :: forall m. + MonadST m + => Codec PingPong CBOR.DeserialiseFailure m ByteString +codecPingPong = mkCodecCborLazyBS encodeMsg decodeMsg + where + encodeMsg :: forall st st'. + Message PingPong st st' + -> CBOR.Encoding + encodeMsg MsgPing = CBOR.encodeWord 0 + encodeMsg MsgPong = CBOR.encodeWord 1 + encodeMsg MsgDone = CBOR.encodeWord 2 + + decodeMsg :: forall s (st :: PingPong). + ActiveState st + => StateToken st + -> CBOR.Decoder s (SomeMessage st) + decodeMsg stok = do + key <- CBOR.decodeWord + case (stok, key) of + (SingIdle, 0) -> return $ SomeMessage MsgPing + (SingBusy, 1) -> return $ SomeMessage MsgPong + (SingIdle, 2) -> return $ SomeMessage MsgDone + + -- TODO proper exceptions + (SingIdle, _) -> fail "codecPingPong.StIdle: unexpected key" + (SingBusy, _) -> fail "codecPingPong.StBusy: unexpected key" + (a@SingDone, _) -> notActiveState a diff --git a/examples/Network/TypedProtocol/PingPong/Examples.hs b/examples/Network/TypedProtocol/PingPong/Examples.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Examples.hs @@ -0,0 +1,145 @@ +module Network.TypedProtocol.PingPong.Examples where + +import Network.TypedProtocol.PingPong.Client +import Network.TypedProtocol.PingPong.Server + +import Network.TypedProtocol.Peer.Client + + +-- | The standard stateless ping-pong server instance. +-- +pingPongServerStandard + :: Applicative m + => PingPongServer m () +pingPongServerStandard = + PingPongServer { + recvMsgPing = pure pingPongServerStandard, + recvMsgDone = () + } + + +-- | An example ping-pong server instance that counts the number of ping +-- messages. +-- +pingPongServerCount + :: Applicative m + => PingPongServer m Int +pingPongServerCount = go 0 + where + go !c = PingPongServer { + recvMsgPing = pure $ go (succ c), + recvMsgDone = c + } + + +-- | An example ping-pong client that sends pings as fast as possible forever‽ +-- +-- This may not be a good idea‼ +-- +pingPongClientFlood :: Applicative m => PingPongClient m a +pingPongClientFlood = SendMsgPing (pure pingPongClientFlood) + + +-- | An example ping-pong client that sends a fixed number of ping messages +-- and then stops. +-- +pingPongClientCount :: Applicative m => Int -> PingPongClient m () +pingPongClientCount 0 = SendMsgDone () +pingPongClientCount n = SendMsgPing (pure (pingPongClientCount (n-1))) + + +-- +-- Pipelined examples +-- + +-- | A pipelined ping-pong client that sends eagerly rather than waiting to +-- collect any replies. This is maximum pipelining in some sense, and +-- correspondingly it gives minimum choice to the environment (drivers). +-- +-- It returns the interleaving of ping indexes sent, and collected. +-- +pingPongClientPipelinedMax + :: forall m. Monad m + => Int + -> PingPongClientPipelined Int m [Either Int Int] +pingPongClientPipelinedMax c = + PingPongClientPipelined (go [] Zero 0) + where + go :: [Either Int Int] -> Nat o -> Int + -> PingPongClientIdle o Int m [Either Int Int] + go acc o n | n < c + = SendMsgPingPipelined + (return n) + (go (Left n : acc) (Succ o) (succ n)) + go acc Zero _ = SendMsgDonePipelined (reverse acc) + go acc (Succ o) n = CollectPipelined + Nothing + (\n' -> go (Right n' : acc) o n) + + +-- | A pipelined ping-pong client that sends eagerly but always tries to +-- collect any replies if they are available. This allows pipelining but +-- keeps it to a minimum, and correspondingly it gives maximum choice to the +-- environment (drivers). +-- +-- It returns the interleaving of ping indexes sent, and collected. +-- +pingPongClientPipelinedMin + :: forall m. Monad m + => Int + -> PingPongClientPipelined Int m [Either Int Int] +pingPongClientPipelinedMin c = + PingPongClientPipelined (go [] Zero 0) + where + go :: [Either Int Int] -> Nat o -> Int + -> PingPongClientIdle o Int m [Either Int Int] + go acc (Succ o) n = CollectPipelined + (if n < c then Just (ping acc (Succ o) n) + else Nothing) + (\n' -> go (Right n' : acc) o n) + go acc Zero n | n < c + = ping acc Zero n + go acc Zero _ = SendMsgDonePipelined (reverse acc) + + ping :: [Either Int Int] -> Nat o -> Int + -> PingPongClientIdle o Int m [Either Int Int] + ping acc o n = SendMsgPingPipelined + (return n) + (go (Left n : acc) (Succ o) (succ n)) + + +-- | A pipelined ping-pong client that sends eagerly up to some maximum limit +-- of outstanding requests. It is also always ready to collect any replies if +-- they are available. This allows limited pipelining and correspondingly +-- limited choice to the environment (drivers). +-- +-- It returns the interleaving of ping indexes sent, and collected. +-- +pingPongClientPipelinedLimited + :: forall m. Monad m + => Int -> Int + -> PingPongClientPipelined Int m [Either Int Int] +pingPongClientPipelinedLimited omax c = + PingPongClientPipelined (go [] Zero 0) + where + go :: [Either Int Int] -> Nat o -> Int + -> PingPongClientIdle o Int m [Either Int Int] + go acc (Succ o) n = CollectPipelined + (if n < c && int (Succ o) < omax + then Just (ping acc (Succ o) n) + else Nothing) + (\n' -> go (Right n' : acc) o n) + go acc Zero n | n < c + = ping acc Zero n + go acc Zero _ = SendMsgDonePipelined (reverse acc) + + ping :: [Either Int Int] -> Nat o -> Int + -> PingPongClientIdle o Int m [Either Int Int] + ping acc o n = SendMsgPingPipelined + (return n) + (go (Left n : acc) (Succ o) (succ n)) + + -- this isn't supposed to be efficient, it's just for the example + int :: Nat n -> Int + int Zero = 0 + int (Succ n) = succ (int n) diff --git a/examples/Network/TypedProtocol/PingPong/Server.hs b/examples/Network/TypedProtocol/PingPong/Server.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Server.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE RecordWildCards #-} + +module Network.TypedProtocol.PingPong.Server where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Server +import Network.TypedProtocol.PingPong.Type + + +data PingPongServer m a = PingPongServer { + -- | The client sent us a ping message. We have no choices here, and + -- the response is nullary, all we have are local effects. + recvMsgPing :: m (PingPongServer m a) + + -- | The client terminated. Here we have a pure return value, but we + -- could have done another action in 'm' if we wanted to. + , recvMsgDone :: a + } + + +-- | Interpret a particular server action sequence into the server side of the +-- 'PingPong' protocol. +-- +pingPongServerPeer + :: Monad m + => PingPongServer m a + -> Server PingPong NonPipelined StIdle m a +pingPongServerPeer PingPongServer{..} = + + -- In the 'StIdle' the server is awaiting a request message + Await $ \req -> + + -- The client got to choose between two messages and we have to handle + -- either of them + case req of + + -- The client sent the done transition, so we're in the 'StDone' state + -- so all we can do is stop using 'done', with a return value. + MsgDone -> Done recvMsgDone + + -- The client sent us a ping request, so now we're in the 'StBusy' state + -- which means it's the server's turn to send. + MsgPing -> Effect $ do + next <- recvMsgPing + pure $ Yield MsgPong (pingPongServerPeer next) diff --git a/examples/Network/TypedProtocol/PingPong/Type.hs b/examples/Network/TypedProtocol/PingPong/Type.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/PingPong/Type.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE TypeFamilies #-} + +module Network.TypedProtocol.PingPong.Type where + +import Network.TypedProtocol.Core + + +-- | The ping\/pong protocol and the states in its protocol state machine. +-- +-- This protocol serves as a simple example of the typed protocols framework +-- to help understand the framework and as a template for writing other +-- protocols. +-- +-- For a slightly more realistic example, see the request\/response protocol +-- "Network.TypedProtocol.ResResp.Type". +-- +-- This declares the protocol itself. It is used both as a type level tag for +-- the protocol and as the kind of the types of the states in the protocol +-- state machine. That is @PingPong@ is a kind, and @StIdle@ is a type of +-- that kind. +-- +-- If the protocol needs any type parameters (e.g. for thing that end up in +-- the messages) then those type parameters go here. See the request\/response +-- protocol for an example. It is parametrised over the types of the request +-- and response. +-- +data PingPong where + StIdle :: PingPong + StBusy :: PingPong + StDone :: PingPong + +data SPingPong (st :: PingPong) where + SingIdle :: SPingPong StIdle + SingBusy :: SPingPong StBusy + SingDone :: SPingPong StDone + +deriving instance Show (SPingPong st) + +instance StateTokenI StIdle where stateToken = SingIdle +instance StateTokenI StBusy where stateToken = SingBusy +instance StateTokenI StDone where stateToken = SingDone + +instance Protocol PingPong where + + -- | The actual messages in our protocol. + -- + -- These involve transitions between different states within the 'PingPong' + -- states. A ping request goes from idle to busy, and a pong response go from + -- busy to idle. + -- + -- This example is so simple that we have all the messages directly as + -- constructors within this type. In more complex cases it may be better to + -- factor all (or related) requests and all responses within one case (in + -- which case the state transitions may depend on the particular message via + -- the usual GADT tricks). + -- + data Message PingPong from to where + MsgPing :: Message PingPong StIdle StBusy + MsgPong :: Message PingPong StBusy StIdle + MsgDone :: Message PingPong StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SPingPong + + +deriving instance Show (Message PingPong from to) diff --git a/examples/Network/TypedProtocol/ReqResp/Client.hs b/examples/Network/TypedProtocol/ReqResp/Client.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Client.hs @@ -0,0 +1,152 @@ +module Network.TypedProtocol.ReqResp.Client + ( -- * Normal client + ReqRespClient (..) + , reqRespClientPeer + -- * Pipelined client + , ReqRespClientPipelined (..) + , reqRespClientPeerPipelined + , ReqRespIdle (..) + , reqRespClientPeerIdle + -- * Request once + , requestOnce + ) where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client +import Network.TypedProtocol.Peer.Server (Server) +import Network.TypedProtocol.Proofs (connect) +import Network.TypedProtocol.ReqResp.Type + +data ReqRespClient req resp m a where + SendMsgReq :: req + -> (resp -> m (ReqRespClient req resp m a)) + -> ReqRespClient req resp m a + + SendMsgDone :: m a -> ReqRespClient req resp m a + + +-- | Interpret a particular client action sequence into the client side of the +-- 'ReqResp' protocol. +-- +reqRespClientPeer + :: Monad m + => ReqRespClient req resp m a + -> Client (ReqResp req resp) NonPipelined StIdle m a + +reqRespClientPeer (SendMsgDone result) = + -- We do an actual transition using 'yield', to go from the 'StIdle' to + -- 'StDone' state. Once in the 'StDone' state we can actually stop using + -- 'done', with a return value. + Effect $ + Yield MsgDone . Done <$> result + +reqRespClientPeer (SendMsgReq req next) = + + -- Send our message. + Yield (MsgReq req) $ + + -- The type of our protocol means that we're now into the 'StBusy' state + -- and the only thing we can do next is local effects or wait for a reply. + -- We'll wait for a reply. + Await $ \(MsgResp resp) -> + + -- Now in this case there is only one possible response, and we have + -- one corresponding continuation 'kPong' to handle that response. + -- The pong reply has no content so there's nothing to pass to our + -- continuation, but if there were we would. + Effect $ do + client <- next resp + pure $ reqRespClientPeer client + + + +requestOnce :: forall req resp m. + Monad m + => (forall x. Server (ReqResp req resp) NonPipelined StIdle m x) + -> (req -> m resp) +requestOnce server req = (\(resp, _, _) -> resp) + <$> reqRespClientPeer client `connect` server + where + client :: ReqRespClient req resp m resp + client = SendMsgReq req $ \resp -> pure $ SendMsgDone (pure resp) + + +-- +-- Pipelined client +-- + +-- | A request-response client designed for running the 'ReqResp' protocol in +-- a pipelined way. +-- +data ReqRespClientPipelined req resp m a where + -- | A 'PingPongSender', but starting with zero outstanding pipelined + -- responses, and for any internal collect type @c@. + ReqRespClientPipelined :: + ReqRespIdle req resp Z c m a + -> ReqRespClientPipelined req resp m a + + +data ReqRespIdle req resp n c m a where + -- | Send a `Req` message but alike in `ReqRespClient` do not await for the + -- resopnse, instead supply a monadic action which will run on a received + -- `Pong` message. + SendMsgReqPipelined + :: req + -> (resp -> m c) -- receive action + -> ReqRespIdle req resp (S n) c m a -- continuation + -> ReqRespIdle req resp n c m a + + CollectPipelined + :: Maybe (ReqRespIdle req resp (S n) c m a) + -> (c -> m (ReqRespIdle req resp n c m a)) + -> ReqRespIdle req resp (S n) c m a + + -- | Termination of the req-resp protocol. + SendMsgDonePipelined + :: a -> ReqRespIdle req resp Z c m a + + +-- | Interpret a pipelined client as a 'Peer' on the client side of +-- the 'ReqResp' protocol. +-- +reqRespClientPeerPipelined + :: Functor m + => ReqRespClientPipelined req resp m a + -> ClientPipelined (ReqResp req resp) StIdle m a +reqRespClientPeerPipelined (ReqRespClientPipelined peer) = + ClientPipelined $ reqRespClientPeerIdle peer + + +reqRespClientPeerIdle + :: forall req resp n c m a. + Functor m + => ReqRespIdle req resp n c m a + -> Client (ReqResp req resp) (Pipelined n c) StIdle m a + +reqRespClientPeerIdle = go + where + go :: forall n'. + ReqRespIdle req resp n' c m a + -> Client (ReqResp req resp) (Pipelined n' c) StIdle m a + + go (SendMsgReqPipelined req receive next) = + -- Pipelined yield: send `MsgReq`, immediately follow with the next step. + -- Await for a response in a continuation. + YieldPipelined + (MsgReq req) + (ReceiverAwait $ \(MsgResp resp) -> + ReceiverEffect $ + ReceiverDone <$> receive resp + ) + (go next) + + go (CollectPipelined mNone collect) = + Collect + (go <$> mNone) + (\c -> Effect $ go <$> collect c) + + go (SendMsgDonePipelined result) = + -- Send `MsgDone` and complete the protocol + Yield + MsgDone + (Done result) diff --git a/examples/Network/TypedProtocol/ReqResp/Codec.hs b/examples/Network/TypedProtocol/ReqResp/Codec.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Codec.hs @@ -0,0 +1,85 @@ +module Network.TypedProtocol.ReqResp.Codec where + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core +import Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame) +import Network.TypedProtocol.ReqResp.Type +import Text.Read (readMaybe) + + +codecReqResp :: + forall req resp m + . (Monad m, Show req, Show resp, Read req, Read resp) + => Codec (ReqResp req resp) CodecFailure m String +codecReqResp = + Codec{encode, decode} + where + encode :: forall req' resp' + (st :: ReqResp req' resp') + (st' :: ReqResp req' resp') + . ( Show (Message (ReqResp req' resp') st st') ) + => Message (ReqResp req' resp') st st' + -> String + encode msg = show msg ++ "\n" + + decode :: forall req' resp' m' + (st :: ReqResp req' resp') + . (Monad m', Read req', Read resp', ActiveState st) + => StateToken st + -> m' (DecodeStep String CodecFailure m' (SomeMessage st)) + decode stok = + decodeTerminatedFrame '\n' $ \str trailing -> + case (stok, break (==' ') str) of + (SingIdle, ("MsgReq", str')) + | Just req <- readMaybe str' + -> DecodeDone (SomeMessage (MsgReq req)) trailing + (SingIdle, ("MsgDone", "")) + -> DecodeDone (SomeMessage MsgDone) trailing + (SingBusy, ("MsgResp", str')) + | Just resp <- readMaybe str' + -> DecodeDone (SomeMessage (MsgResp resp)) trailing + + (_ , _ ) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + +codecReqRespId :: + forall req resp m + . (Monad m, Show req, Show resp) + => Codec (ReqResp req resp) CodecFailure m (AnyMessage (ReqResp req resp)) +codecReqRespId = + Codec{encode, decode} + where + encode :: forall (st :: ReqResp req resp) + (st' :: ReqResp req resp) + . StateTokenI st + => ActiveState st + => Message (ReqResp req resp) st st' + -> AnyMessage (ReqResp req resp) + encode msg = AnyMessage msg + + decode :: forall (st :: ReqResp req resp) + . ActiveState st + => StateToken st + -> m (DecodeStep (AnyMessage (ReqResp req resp)) CodecFailure m (SomeMessage st)) + decode stok = + pure $ DecodePartial $ \mb -> + case mb of + Nothing -> return $ DecodeFail (CodecFailure "expected more data") + Just (AnyMessage msg) -> return $ + case (stok, msg) of + (SingIdle, MsgReq{}) + -> DecodeDone (SomeMessage msg) Nothing + (SingIdle, MsgDone) + -> DecodeDone (SomeMessage msg) Nothing + (SingBusy, MsgResp{}) + -> DecodeDone (SomeMessage msg) Nothing + + (SingIdle, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected client message: " ++ show msg) + (SingBusy, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ show msg) + + (a@SingDone, _) -> notActiveState a diff --git a/examples/Network/TypedProtocol/ReqResp/Codec/CBOR.hs b/examples/Network/TypedProtocol/ReqResp/Codec/CBOR.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Codec/CBOR.hs @@ -0,0 +1,55 @@ +module Network.TypedProtocol.ReqResp.Codec.CBOR where + +import Control.Monad.Class.MonadST + +import Data.ByteString.Lazy (ByteString) + +import Codec.CBOR.Decoding qualified as CBOR (Decoder, decodeListLen, + decodeWord) +import Codec.CBOR.Encoding qualified as CBOR (Encoding, encodeListLen, + encodeWord) +import Codec.CBOR.Read qualified as CBOR +import Codec.Serialise.Class (Serialise) +import Codec.Serialise.Class qualified as CBOR + +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Codec.CBOR +import Network.TypedProtocol.Core +import Network.TypedProtocol.ReqResp.Type + +codecReqResp + :: forall req resp m. + ( MonadST m + , Serialise req + , Serialise resp + ) + => Codec (ReqResp req resp) CBOR.DeserialiseFailure m ByteString +codecReqResp = mkCodecCborLazyBS encodeMsg decodeMsg + where + encodeMsg :: forall st st'. + Message (ReqResp req resp) st st' + -> CBOR.Encoding + encodeMsg (MsgReq req) = + CBOR.encodeListLen 2 <> CBOR.encodeWord 0 <> CBOR.encode req + encodeMsg (MsgResp resp) = + CBOR.encodeListLen 2 <> CBOR.encodeWord 1 <> CBOR.encode resp + encodeMsg MsgDone = + CBOR.encodeListLen 1 <> CBOR.encodeWord 2 + + decodeMsg :: forall s (st :: ReqResp req resp). + ActiveState st + => StateToken st + -> CBOR.Decoder s (SomeMessage st) + decodeMsg stok = do + _ <- CBOR.decodeListLen + key <- CBOR.decodeWord + case (stok, key) of + (SingIdle, 0) -> SomeMessage . MsgReq <$> CBOR.decode + (SingBusy, 1) -> SomeMessage . MsgResp <$> CBOR.decode + (SingIdle, 2) -> return $ SomeMessage MsgDone + + -- TODO proper exceptions + (SingIdle, _) -> fail "codecReqResp.StIdle: unexpected key" + (SingBusy, _) -> fail "codecReqResp.StBusy: unexpected key" + (a@SingDone, _) -> notActiveState a + diff --git a/examples/Network/TypedProtocol/ReqResp/Examples.hs b/examples/Network/TypedProtocol/ReqResp/Examples.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Examples.hs @@ -0,0 +1,87 @@ +module Network.TypedProtocol.ReqResp.Examples where + +import Network.TypedProtocol.ReqResp.Client +import Network.TypedProtocol.ReqResp.Server + +import Network.TypedProtocol.Peer.Client + +-- | An example request\/response client which ignores received responses. +-- +reqRespClient :: Monad m + => [req] + -> ReqRespClient req resp m () +reqRespClient = go + where + go [] = SendMsgDone (pure ()) + go (req:reqs) = SendMsgReq req (\_resp -> return (go reqs)) + + +-- | A request\/response server instance that computes a 'Data.List.mapAccumL' +-- over the stream of requests. +-- +reqRespServerMapAccumL :: Monad m + => (acc -> req -> m (acc, resp)) + -> acc + -> ReqRespServer req resp m acc +reqRespServerMapAccumL f !acc = + ReqRespServer { + recvMsgReq = \req -> do (acc', resp) <- f acc req + return (resp, reqRespServerMapAccumL f acc'), + recvMsgDone = pure acc + } + + +-- | An example request\/response client that sends the given list of requests +-- and collects the list of responses. +-- +reqRespClientMap :: Monad m + => [req] + -> ReqRespClient req resp m [resp] +reqRespClientMap = go [] + where + go resps [] = SendMsgDone (pure $ reverse resps) + go resps (req:reqs) = + SendMsgReq req $ \resp -> + return (go (resp:resps) reqs) + +-- +-- Pipelined example +-- + +-- | An example request\/response client that sends the given list of requests +-- and collects the list of responses. +-- +-- It is pipelined and tries to collect any replies if they are available. +-- This allows pipelining but keeps it to a minimum, and correspondingly it +-- gives maximum choice to the environment (drivers). +-- +-- In theory, with enough and large enough requests and responses, this should +-- be able to saturate any channel of any bandwidth and latency, because it +-- should be able to have both peers send essentially continuously. +-- +reqRespClientMapPipelined :: forall req resp m. + Monad m + => [req] + -> ReqRespClientPipelined req resp m [resp] +reqRespClientMapPipelined reqs0 = + ReqRespClientPipelined (go [] Zero reqs0) + where + go :: [resp] -> Nat o -> [req] -> ReqRespIdle req resp o resp m [resp] + go resps Zero reqs = + case reqs of + [] -> SendMsgDonePipelined (reverse resps) + req:reqs' -> sendReq resps Zero req reqs' + + go resps (Succ o) reqs = + CollectPipelined + (case reqs of + [] -> Nothing + req:reqs' -> Just (sendReq resps (Succ o) req reqs')) + (\resp -> return $ go (resp:resps) o reqs) + + sendReq :: [resp] -> Nat o -> req -> [req] + -> ReqRespIdle req resp o resp m [resp] + sendReq resps o req reqs' = + SendMsgReqPipelined req + (\resp -> return resp) + (go resps (Succ o) reqs') diff --git a/examples/Network/TypedProtocol/ReqResp/Server.hs b/examples/Network/TypedProtocol/ReqResp/Server.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Server.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RecordWildCards #-} + +module Network.TypedProtocol.ReqResp.Server where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Server +import Network.TypedProtocol.ReqResp.Type + + +data ReqRespServer req resp m a = ReqRespServer { + -- | The client sent us a ping message. We have no choices here, and + -- the response is nullary, all we have are local effects. + recvMsgReq :: req -> m (resp, ReqRespServer req resp m a) + + -- | The client terminated. Here we have a pure return value, but we + -- could have done another action in 'm' if we wanted to. + , recvMsgDone :: m a + } + + +-- | Interpret a particular server action sequence into the server side of the +-- 'ReqResp' protocol. +-- +reqRespServerPeer + :: Monad m + => ReqRespServer req resp m a + -> Server (ReqResp req resp) NonPipelined StIdle m a +reqRespServerPeer ReqRespServer{..} = + + -- In the 'StIdle' the server is awaiting a request message + Await $ \msg -> + + -- The client got to choose between two messages and we have to handle + -- either of them + case msg of + + -- The client sent the done transition, so we're in the 'StDone' state + -- so all we can do is stop using 'done', with a return value. + MsgDone -> Effect $ Done <$> recvMsgDone + + -- The client sent us a ping request, so now we're in the 'StBusy' state + -- which means it's the server's turn to send. + MsgReq req -> Effect $ do + (resp, next) <- recvMsgReq req + pure $ Yield (MsgResp resp) (reqRespServerPeer next) diff --git a/examples/Network/TypedProtocol/ReqResp/Type.hs b/examples/Network/TypedProtocol/ReqResp/Type.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp/Type.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE TypeFamilies #-} + +module Network.TypedProtocol.ReqResp.Type where + +import Network.TypedProtocol.Core + + +data ReqResp req resp where + StIdle :: ReqResp req resp + StBusy :: ReqResp req resp + StDone :: ReqResp req resp + +data SReqResp (st :: ReqResp req resp) where + SingIdle :: SReqResp StIdle + SingBusy :: SReqResp StBusy + SingDone :: SReqResp StDone + +deriving instance Show (SReqResp st) + +instance StateTokenI StIdle where + stateToken = SingIdle +instance StateTokenI StBusy where + stateToken = SingBusy +instance StateTokenI StDone where + stateToken = SingDone + + +instance Protocol (ReqResp req resp) where + + data Message (ReqResp req resp) from to where + MsgReq :: req -> Message (ReqResp req resp) StIdle StBusy + MsgResp :: resp -> Message (ReqResp req resp) StBusy StIdle + MsgDone :: Message (ReqResp req resp) StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SReqResp + + +deriving instance (Show req, Show resp) + => Show (Message (ReqResp req resp) from to) + +deriving instance (Eq req, Eq resp) + => Eq (Message (ReqResp req resp) from to) diff --git a/examples/Network/TypedProtocol/ReqResp2/Client.hs b/examples/Network/TypedProtocol/ReqResp2/Client.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp2/Client.hs @@ -0,0 +1,49 @@ +module Network.TypedProtocol.ReqResp2.Client where + +import Network.TypedProtocol.ReqResp2.Type + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client + + +reqResp2Client :: forall req resp m. + () + => [Either req req] + -> Client (ReqResp2 req resp) (Pipelined Z (Either resp resp)) StIdle m [Either resp resp] +reqResp2Client = send Zero + where + -- pipeline all the requests, either through `MsgReq` or `MsgReq'`. + send :: forall (n :: N). + Nat n + -> [Either req req] -- requests to send + -> Client (ReqResp2 req resp) (Pipelined n (Either resp resp)) StIdle m [Either resp resp] + + send !n (Left req : reqs) = + YieldPipelined (MsgReq req) receiver (send (Succ n) reqs) + + send !n (Right req : reqs) = + YieldPipelined (MsgReq' req) receiver' (send (Succ n) reqs) + + send !n [] = collect n [] + + + receiver :: Receiver (ReqResp2 req resp) StBusy StIdle m (Either resp resp) + receiver = ReceiverAwait (\(MsgResp resp) -> ReceiverDone (Left resp)) + + + receiver' :: Receiver (ReqResp2 req resp) StBusy' StIdle m (Either resp resp) + receiver' = ReceiverAwait (\(MsgResp' resp) -> ReceiverDone (Right resp)) + + + -- collect all the responses + collect :: Nat n + -> [Either resp resp] -- all the responses received so far + -> Client (ReqResp2 req resp) (Pipelined n (Either resp resp)) StIdle m [Either resp resp] + + collect Zero !resps = Yield MsgDone (Done (reverse resps)) + + collect (Succ n) !resps = + Collect Nothing $ \c -> collect n (c : resps) + + + diff --git a/examples/Network/TypedProtocol/ReqResp2/Type.hs b/examples/Network/TypedProtocol/ReqResp2/Type.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/ReqResp2/Type.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE TypeFamilies #-} + +module Network.TypedProtocol.ReqResp2.Type where + +import Network.TypedProtocol.Core + + +data ReqResp2 req resp where + StIdle :: ReqResp2 req resp + StBusy :: ReqResp2 req resp + StBusy' :: ReqResp2 req resp + StDone :: ReqResp2 req resp + +data SReqResp2 (st :: ReqResp2 req resp) where + SingIdle :: SReqResp2 StIdle + SingBusy :: SReqResp2 StBusy + SingBusy' :: SReqResp2 StBusy' + SingDone :: SReqResp2 StDone + +deriving instance Show (SReqResp2 st) + +instance StateTokenI StIdle where + stateToken = SingIdle +instance StateTokenI StBusy where + stateToken = SingBusy +instance StateTokenI StBusy' where + stateToken = SingBusy' +instance StateTokenI StDone where + stateToken = SingDone + + +instance Protocol (ReqResp2 req resp) where + + data Message (ReqResp2 req resp) from to where + MsgReq :: req -> Message (ReqResp2 req resp) StIdle StBusy + MsgResp :: resp -> Message (ReqResp2 req resp) StBusy StIdle + + MsgReq' :: req -> Message (ReqResp2 req resp) StIdle StBusy' + MsgResp' :: resp -> Message (ReqResp2 req resp) StBusy' StIdle + + MsgDone :: Message (ReqResp2 req resp) StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StBusy' = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SReqResp2 + + +deriving instance (Show req, Show resp) + => Show (Message (ReqResp2 req resp) from to) + +deriving instance (Eq req, Eq resp) + => Eq (Message (ReqResp2 req resp) from to) + diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Client.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Client.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Client.hs @@ -0,0 +1,35 @@ +module Network.TypedProtocol.Stateful.ReqResp.Client + ( ReqRespClient (..) + , reqRespClientPeer + ) where + +import Data.Typeable +import Network.TypedProtocol.Stateful.Peer.Client +import Network.TypedProtocol.Stateful.ReqResp.Type + +data ReqRespClient req m a where + SendMsgReq :: Typeable resp + => req resp + -> (resp -> m (ReqRespClient req m a)) + -> ReqRespClient req m a + + SendMsgDone :: a + -> ReqRespClient req m a + + +reqRespClientPeer + :: Monad m + => ReqRespClient req m a + -> Client (ReqResp req) StIdle State m a + +reqRespClientPeer (SendMsgDone a) = + Yield StateIdle StateDone MsgDone (Done a) + +reqRespClientPeer (SendMsgReq req next) = + Yield StateIdle (StateBusy req) + (MsgReq req) $ + Await $ \_ (MsgResp resp) -> + let client = next resp + in ( Effect $ reqRespClientPeer <$> client + , StateIdle + ) diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs @@ -0,0 +1,105 @@ +module Network.TypedProtocol.Stateful.ReqResp.Codec where + +import Data.Kind (Type) +import Data.Singletons.Decide +import Data.Typeable +import Network.TypedProtocol.Core +import Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame) +import Network.TypedProtocol.Stateful.Codec +import Network.TypedProtocol.Stateful.ReqResp.Type + +data Some (f :: k -> Type) where + Some :: Typeable a => f a -> Some f + + +-- | Codec polymorphic in the RPC (e.g. `req` type) +-- +codecReqResp + :: forall req m. Monad m + => (forall resp. req resp -> String) + -- ^ encode `req resp` + -> (String -> Maybe (Some req)) + -- ^ decode `req resp` + -> (forall resp. req resp -> resp -> String) + -- ^ encode resp + -> (forall resp. req resp -> String -> Maybe resp) + -- ^ decode resp + -> Codec (ReqResp req) CodecFailure State m String +codecReqResp encodeReq decodeReq encodeResp decodeResp = + Codec { encode, decode } + where + encode :: State st + -> Message (ReqResp req) st st' + -> String + encode _ (MsgReq req) = "MsgReq " ++ encodeReq req ++ "\n" + encode _ MsgDone = "MsgDone\n" + encode (StateBusy req) (MsgResp resp) = "MsgResp " ++ encodeResp req resp ++ "\n" + + decode :: forall (st :: ReqResp req). + ActiveState st + => StateToken st + -> State st + -> m (DecodeStep String CodecFailure m (SomeMessage st)) + decode stok state = + decodeTerminatedFrame '\n' $ \str trailing -> + case (stok, state, break (==' ') str) of + (SingIdle, StateIdle, ("MsgReq", str')) + | Just (Some req) <- decodeReq str' + -> DecodeDone (SomeMessage (MsgReq req)) trailing + (SingIdle, StateIdle, ("MsgDone", "")) + -> DecodeDone (SomeMessage MsgDone) trailing + (SingBusy, StateBusy req, ("MsgResp", str')) + -- note that we need `req` to decode response of the given type + | Just resp <- decodeResp req str' + -> DecodeDone (SomeMessage (MsgResp resp)) trailing + (_, _, _) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + +data Bytes where + Bytes :: Message (ReqResp FileAPI) st st' -> Bytes + +-- | An identity codec which wraps messages into `AnyMessage`. +-- +codecReqRespId + :: forall m. + Applicative m + => (forall (res1 :: Type) (res2 :: Type). + (Typeable res1, Typeable res2) + => Proxy res1 + -> Proxy res2 + -> Maybe (res1 :~: res2) + ) + -> Codec FileRPC String State m Bytes +codecReqRespId eqRespTypes = Codec { encode, decode } + where + encode _ = Bytes + + decode :: forall (st :: ReqResp FileAPI). + ActiveState st + => StateToken st + -> State st + -> m (DecodeStep Bytes String m (SomeMessage st)) + decode stok state = pure $ DecodePartial $ \bytes -> pure $ + case (stok, state, bytes) of + (SingIdle, StateIdle, Just (Bytes msg@MsgDone)) + -> DecodeDone (SomeMessage msg) Nothing + (SingIdle, StateIdle, Just (Bytes msg@MsgReq{})) + -> DecodeDone (SomeMessage msg) Nothing + (SingBusy, StateBusy req, Just (Bytes msg@MsgResp{})) + -- the codec needs to verify that response type of `req` and `msg` agrees + | Just Refl <- eqRespTypes (reqRespType req) (msgRespType msg) + -> DecodeDone (SomeMessage msg) Nothing + + (SingDone, _, _) -> notActiveState stok + (_, _, Nothing) -> DecodeFail "no bytes" + (_, _, _) -> DecodeFail "no matching message" + + msgRespType :: forall resp. Message (ReqResp FileAPI) (StBusy resp) StIdle + -> Proxy resp + msgRespType (MsgResp _) = Proxy + + reqRespType :: forall resp. FileAPI resp -> Proxy resp + reqRespType _ = Proxy + + diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Examples.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Examples.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Examples.hs @@ -0,0 +1,26 @@ +module Network.TypedProtocol.Stateful.ReqResp.Examples where + +import Network.TypedProtocol.Stateful.ReqResp.Server +import Network.TypedProtocol.Stateful.ReqResp.Type + + +fileRPCServer :: Monad m + => (forall resp. FileAPI resp -> m resp) + -- ^ execute `FileAPI` locally + -> ReqRespServer FileAPI m () +fileRPCServer run = ReqRespServer { + reqRespServerDone = (), + reqRespHandleReq = \req -> do + resp <- run req + return (resp, fileRPCServer run) + } + +-- | Example of a file API +-- +simpleFileAPI :: Monad m => FileAPI resp -> m resp +simpleFileAPI (ReadFile filepath) = return filepath +simpleFileAPI (WriteFile _ _) = return () + +simpleFileRPCServer :: Monad m => ReqRespServer FileAPI m () +simpleFileRPCServer = fileRPCServer simpleFileAPI + diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Server.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Server.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Server.hs @@ -0,0 +1,28 @@ +module Network.TypedProtocol.Stateful.ReqResp.Server + ( ReqRespServer (..) + , reqRespServerPeer + ) where + +import Data.Typeable +import Network.TypedProtocol.Stateful.Peer.Server +import Network.TypedProtocol.Stateful.ReqResp.Type + + +data ReqRespServer req m a = ReqRespServer { + reqRespServerDone :: a, + reqRespHandleReq :: forall resp. Typeable resp => req resp -> m (resp, ReqRespServer req m a) + } + +reqRespServerPeer :: Functor m + => ReqRespServer req m a + -> Server (ReqResp req) StIdle State m a +reqRespServerPeer ReqRespServer { reqRespServerDone = a, + reqRespHandleReq = k } = + Await $ \_ -> \case + MsgDone -> (Done a, StateDone) + MsgReq req -> + ( Effect $ + (\(resp, k') -> Yield (StateBusy req) StateIdle (MsgResp resp) (reqRespServerPeer k')) + <$> k req + , StateBusy req + ) diff --git a/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs b/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | An RPC protocol which in which request type determines respond time. +-- Unlike in the `Network.TypedProtocol.ReqResp.Type` where `req` and `resp` +-- types where statically defined, here the respond type is dynamically +-- determined by the type of request. +-- +module Network.TypedProtocol.Stateful.ReqResp.Type where + +import Data.Kind (Type) +import Data.Typeable +import Network.TypedProtocol.Core + + +type ReqResp :: (Type -> Type) -> Type +data ReqResp req where + StIdle :: ReqResp req + StBusy :: res + -> ReqResp req + StDone :: ReqResp req + +type SReqResp :: ReqResp req -> Type +data SReqResp st where + SingIdle :: SReqResp StIdle + SingBusy :: SReqResp (StBusy res :: ReqResp req) + SingDone :: SReqResp StDone + +deriving instance Show (SReqResp st) + +instance StateTokenI StIdle where stateToken = SingIdle +instance StateTokenI (StBusy res) where stateToken = SingBusy +instance StateTokenI StDone where stateToken = SingDone + + +instance Protocol (ReqResp req) where + + -- Messages for the `ReqResp` protocol. + -- + -- Typeable constraint is used to support + -- `Network.TypeProtocol.Stateful.ReqResp.Codec.codecReqRespId' - an + -- efficient encoder / decoder useful for testing purposes. + -- + data Message (ReqResp req) from to where + MsgReq :: Typeable resp + => req resp -- ^ request which expects `resp` as a result, `resp` is + -- promoted to the state `StBusy` state. + -> Message (ReqResp req) StIdle (StBusy resp) + MsgResp :: Typeable resp + => resp -- ^ respond + -> Message (ReqResp req) (StBusy resp) StIdle + MsgDone :: Message (ReqResp req) StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency (StBusy _) = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SReqResp + + +-- deriving instance Show req +-- => Show (Message (ReqResp req) from to) +-- +-- deriving instance Eq req +-- => Eq (Message (ReqResp req) from to) + +type State :: ReqResp req -> Type +data State st where + StateIdle :: State StIdle + -- fancy type signature is needed to help GHC infer that when pattern + -- matching on `StateBusy resp` then `resp :: Type` + StateBusy :: forall (req :: Type -> Type) + (result :: Type). + Typeable result + => req result + -> State (StBusy result :: ReqResp req) + StateDone :: State StDone + +-- +-- A simple example RPC +-- + +-- | An example RPC, e.g. the `req` type. +-- +type FileAPI :: Type -> Type +data FileAPI result where + ReadFile :: FilePath -> FileAPI String + -- read a file + + WriteFile :: FilePath -> String -> FileAPI () + -- write to a file +-- TODO: input-output-hk/typed-protocols#57 + +type FileRPC = ReqResp FileAPI diff --git a/examples/Network/TypedProtocol/Trans/Wedge.hs b/examples/Network/TypedProtocol/Trans/Wedge.hs new file mode 100644 --- /dev/null +++ b/examples/Network/TypedProtocol/Trans/Wedge.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Network.TypedProtocol.Trans.Wedge where + +import Network.TypedProtocol.Core + +import Network.TypedProtocol.Peer.Client qualified as Client +import Network.TypedProtocol.PingPong.Type qualified as PingPong + + +-- | A [wedge](https://hackage.haskell.org/package/smash-0.1.2/docs/Data-Wedge.html) +-- sum of two protocols. +-- +-- One can interleave both protocols using protocol pipelining. Termination +-- must be done by terminating one of the protocols. +-- +data Wedge ps (stIdle :: ps) ps' (stIdle' :: ps') where + StIdle :: Wedge ps stIdle ps' stIdle' + StFst :: ps -> Wedge ps stIdle ps' stIdle' + StSnd :: ps' -> Wedge ps stIdle ps' stIdle' + + +data SingWedge (st :: Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where + SingStIdle :: SingWedge StIdle + SingStFst :: StateToken st + -> SingWedge (StFst st) + SingStSnd :: StateToken st' + -> SingWedge (StSnd st') + +instance Show (SingWedge StIdle) where + show SingStIdle = "SingStIdle" +instance Show (StateToken st) => Show (SingWedge (StFst st)) where + show (SingStFst s) = "SingStFst " ++ show s +instance Show (StateToken st) => Show (SingWedge (StSnd st)) where + show (SingStSnd s) = "SingStSnd " ++ show s + +instance StateTokenI StIdle where + stateToken = SingStIdle +instance StateTokenI st => StateTokenI (StFst st) where + stateToken = SingStFst (stateToken @st) +instance StateTokenI st => StateTokenI (StSnd st) where + stateToken = SingStSnd (stateToken @st) + + +-- | A Singleton type which allows to pick the starting protocol state. +-- +data SingStart (st :: Wedge ps stIdle ps' stIdle') where + AtFst :: SingStart (StFst stIdle) + AtSnd :: SingStart (StSnd stIdle) + + +-- Note: This does not require @(Protocol ps, Protocol ps')@, ghc is not +-- requiring class constraints for associated type families / data types the +-- same way as for terms. +-- +instance Protocol (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where + + data Message (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) from to where + -- | Signal that starts one of the protocols. + -- + MsgStart :: SingStart st + -> Message (Wedge ps stIdle ps' stIdle') + StIdle st + + -- | Embed any @ps@ message. + -- + MsgFst :: Message ps st st' + -> Message (Wedge ps stIdle ps' stIdle') + (StFst st) (StFst st') + + + -- | Embed any @ps'@ message. + MsgSnd :: Message ps' st st' + -> Message (Wedge ps stIdle ps' stIdle') + (StSnd st) (StSnd st') + + -- | Switch from @ps@ to @ps'@. + -- + MsgFstToSnd :: Message (Wedge ps stIdle ps' stIdle') + (StFst stIdle) (StSnd stIdle') + + -- | Switch from @ps'@ to @ps@. + -- + MsgSndToFst :: Message (Wedge ps stIdle ps' stIdle') + (StSnd stIdle') (StFst stIdle) + + + type StateAgency StIdle = ClientAgency + type StateAgency (StFst st) = StateAgency st + type StateAgency (StSnd st) = StateAgency st + + type StateToken = SingWedge + + +type PingPong2 = Wedge PingPong.PingPong PingPong.StIdle + PingPong.PingPong PingPong.StIdle + + +pingPong2Client :: Client.Client PingPong2 NonPipelined StIdle m () +pingPong2Client = + Client.Yield (MsgStart AtFst) + $ Client.Yield (MsgFst PingPong.MsgPing) + $ Client.Await $ \(MsgFst PingPong.MsgPong) -> + Client.Yield MsgFstToSnd + $ Client.Yield (MsgSnd PingPong.MsgPing) + $ Client.Await $ \(MsgSnd PingPong.MsgPong) -> + -- terminate, through the second protocol + Client.Yield (MsgSnd PingPong.MsgDone) + $ Client.Done () + + +pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined Client.Z ()) StIdle m () +pingPong2Client' = + -- + -- Pipeline first protocol + -- + + Client.YieldPipelined (MsgStart AtFst) + (Client.ReceiverDone ()) + $ Client.YieldPipelined (MsgFst PingPong.MsgPing) + (Client.ReceiverAwait (\(MsgFst PingPong.MsgPong) -> Client.ReceiverDone ())) + + -- + -- Pipeline second protocol + -- + + $ Client.YieldPipelined MsgFstToSnd + (Client.ReceiverDone ()) + $ Client.YieldPipelined (MsgSnd PingPong.MsgPing) + (Client.ReceiverAwait (\(MsgSnd PingPong.MsgPong) -> Client.ReceiverDone ())) + + -- + -- Collect responses from the first protocol + -- + + $ Client.Collect Nothing $ \() -> -- collect transition pushed by `MsgStartFst` + Client.Collect Nothing $ \() -> -- collect reply received with `MsgFst MsgPong` + + -- + -- Collect responses from the second protocol + -- + + Client.Collect Nothing $ \() -> -- collect transition pushed by MsgFstToSnd + Client.Collect Nothing $ \() -> -- collect reply received with `MsgSnd MsgPong` + + -- + -- Terminate the protocol + -- + + Client.Yield (MsgSnd PingPong.MsgDone) + $ Client.Done () diff --git a/src/Network/TypedProtocol.hs b/src/Network/TypedProtocol.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol.hs @@ -0,0 +1,134 @@ + +-- | This package defines the typed protocol framework. This module re-exports +-- the public API. +-- +module Network.TypedProtocol + ( -- * Introduction + -- $intro + -- * Defining and implementing protocols + -- $defining + module Network.TypedProtocol.Core + -- ** Protocol proofs and tests + -- $tests + , module Network.TypedProtocol.Proofs + -- * Running protocols + -- $running + , module Network.TypedProtocol.Driver + ) where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Driver +import Network.TypedProtocol.Proofs + + +-- $intro +-- +-- The typed protocol framework is used to define, test and execute protocols. +-- +-- It guarantees: +-- +-- * agreement on which messages can be sent and received; +-- * the absence of race conditions; and +-- * the absence of deadlock. +-- +-- The trade-off to achieve these guarantees is that it places constraints on +-- the kinds of protocol that can be expressed. In particular it requires that +-- protocols be defined as a state transition system. It requires for each +-- protocol state that exactly one of the two peers be able to send and the +-- other must be ready to receive. +-- +-- This means it is not possible to express protocols such as TCP where there +-- are protocol states where a single peer can both send and receive, however +-- it is suitable for most application-level protocols. In particular many +-- application-level protocols are completely in-order and synchronous. That +-- said, in many (but not all) cases it is possible to pipeline these protocols +-- so that network latency can be hidden and full use made of the available +-- bandwidth. Special support is provided to run protocols in a pipelined way, +-- without having to change the protocol definition. +-- +-- The protocols in this framework assume an underlying \"reliable ordered\" +-- connection. A \"reliable ordered\" connection is a term of art meaning one +-- where the receiving end receives any prefix of the messages sent by the +-- sending end. It is not reliable in the colloquial sense as it does not +-- ensure that anything actually arrives, only that /if/ any message arrives, +-- all the previous messages did too, and that they arrive in the order in +-- which they were sent. +-- +-- The framework also provides: +-- +-- * an abstraction for untyped channels; +-- * a codec abstraction for encoding and decoding protocol messages; and +-- * drivers for running protocol peers with a channel and a codec. + + +-- $defining +-- +-- The "Network.TypedProtocol.Core" module defines the core of the system. +-- +-- Start reading here to understand: +-- +-- * how to define new protocols; or +-- * to write peers that engage in a protocol. +-- +-- Typed protocol messages need to be converted to and from untyped +-- serialised forms to send over a transport channel. So part of defining a new +-- protocol is to define the message encoding and the codec for doing the +-- encoding and decoding. This is somewhat (but not significantly) more complex +-- than defining normal data type serialisation because of the need to decode +-- typed protocol messages. The "Network.TypedProtocol.Codec" module provides +-- the codec abstraction to capture this. + + +-- $tests +-- +-- There are a few proofs about the framework that we can state and implement +-- as Haskell functions (using GADTs and evaluation). A couple of these proofs +-- rely on a few lemmas that should be proved for each protocol. The +-- "Network.TypedProtocol.Proofs" module describes these proof and provides +-- the infrastructure for the simple lemmas that need to be implemented for +-- each protocol. +-- +-- This module also provides utilities helpful for testing protocols. + + +-- $running +-- +-- Typed protocols need to be able to send messages over untyped transport +-- channels. The "Network.TypedProtocol.Channel" module provides such an +-- abstraction. You can use existing example implementations of this interface +-- or define your own to run over other transports. +-- +-- Given a protocol peer, and a channel and a codec we can run the protocol +-- peer so that it engages in the protocol sending and receiving messages +-- over the channel. The "Network.TypedProtocol.Driver" module provides drivers +-- for normal and pipelined peers. + + +-- $pipelining +-- Protocol pipelining is a technique to make effective use of network +-- resources. +-- +-- <> +-- +-- As in the above diagram, instead of sending a request and waiting for the +-- response before sending the next request, pipelining involves sending all +-- three requests back-to-back and waiting for the three replies. The server +-- still simply processes the requests in order and the replies come back in +-- the same order as the requests were made. +-- +-- Not only does this save network latency, one round trip versus three in +-- the diagram above, but it also makes effective use of the bandwidth by +-- sending requests and replies back-to-back. +-- +-- In the example in the diagram it stops after three requests, but such a +-- pattern can go on indefinately with messages going in both directions, +-- which can saturate the available bandwidth. +-- +-- For many (but not all) protocols that can be defined in the @typed-protocol@ +-- framework it is possible to take the protocol, without changing the +-- protocol's state machine, and to engage in the protocol in a pipelined way. +-- Only the pipelined client has to be written specially. The server side can +-- be used unaltered and can be used with either pipelined or non-pipelined +-- clients. + + diff --git a/src/Network/TypedProtocol/Codec.hs b/src/Network/TypedProtocol/Codec.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Codec.hs @@ -0,0 +1,546 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +-- @UndecidableInstances@ extension is required for defining @Show@ instance of +-- @'AnyMessage'@ and @'AnyMessage'@. +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +module Network.TypedProtocol.Codec + ( -- * Defining and using Codecs + -- ** Codec type + Codec (..) + , hoistCodec + , isoCodec + , mapFailureCodec + -- ** Incremental decoding + , DecodeStep (..) + , runDecoder + , runDecoderPure + , hoistDecodeStep + , isoDecodeStep + , mapFailureDecodeStep + -- ** Related types + -- *** SomeMessage + , SomeMessage (..) + -- *** StateToken + , StateToken + , StateTokenI (..) + -- *** ActiveState + , IsActiveState (..) + , ActiveState + , ActiveAgency + , ActiveAgency' (..) + , notActiveState + -- *** PeerRole + , PeerRole (..) + -- * CodecFailure + , CodecFailure (..) + -- * Testing codec properties + , 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 (..) + ) where + +import Control.Exception (Exception) +import Data.Kind (Type) +import Data.Monoid (All (..)) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Driver (SomeMessage (..)) + + +-- | A codec for a 'Protocol' handles the encoding and decoding of typed +-- protocol messages. This is typically used when sending protocol messages +-- over untyped channels. The codec chooses the exact encoding, for example +-- encoding in some text-based syntax, or some choice of binary format. +-- +-- The codec is parametrised by: +-- +-- * 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 codec consists of a message encoder and a decoder. +-- +-- 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 +-- in which the peer has agency, since those are the only states where a +-- peer needs to encode a message to be able to send it. +-- +-- For example a simple text encoder for the ping\/pong protocol could be: +-- +-- > encode :: SingI st +-- > => Message PingPong st st' +-- > -> String +-- > encode MsgPing = "ping\n" +-- > encode MsgDone = "done\n" +-- > encode MsgPong = "pong\n" +-- +-- The decoder is also given the current protocol state and it is expected to +-- be able to decode /any/ message that is valid in that state, but /only/ +-- messages that are valid in that state. Messages that are unexpected for the +-- current state should be treated like any other decoding format error. +-- +-- While the current protocol state is known, the state that the message will +-- have the peer transition to is not known. For this reason the decoded +-- message is wrapped in the 'SomeMessage' constructor which hides the \"to\" +-- state. +-- +-- The decoder uses an incremental decoding interface 'DecodeStep' so that +-- input can be supplied (e.g. from a Channel) bit by bit. This style of +-- decoder allows but does not require a format with message framing where the +-- decoder input matches exactly with the message boundaries. +-- +-- > decode :: forall st m. SingI st +-- > => StateToken st +-- > -> m (DecodeStep String String m (SomeMessage st)) +-- > decode stok = +-- > decodeTerminatedFrame '\n' $ \str trailing -> +-- > case (stok, str) of +-- > (SingBusy, "pong") -> +-- > DecodeDone (SomeMessage MsgPong) trailing +-- > (SingIdle, "ping") -> +-- > DecodeDone (SomeMessage MsgPing) trailing +-- > (SingIdle, "done") -> +-- > DecodeDone (SomeMessage MsgDone) trailing +-- > _ -> DecodeFail ("unexpected message: " ++ str) +-- +-- See "typed-protocols-examples" for the full example. +-- +-- Note that the pattern matching on the combination of the message string and +-- the protocol state. This neatly fulfils the requirement that we only return +-- messages that are of the correct type for the given protocol state. +-- +-- 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 { + 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, + + decode :: forall (st :: ps). + ActiveState st + => StateToken st + -- evidence for an active state + -> m (DecodeStep bytes failure m (SomeMessage st)) + } +-- TODO: input-output-hk/typed-protocols#57 + +-- | Change functor in which the codec is running. +-- +hoistCodec + :: ( Functor n ) + => (forall x . m x -> n x) + -- ^ a natural transformation + -> Codec ps failure m bytes + -> Codec ps failure n bytes +hoistCodec nat codec = codec + { decode = fmap (hoistDecodeStep nat) . nat . decode codec + } + +-- | Change bytes of a codec. +-- +isoCodec :: Functor m + => (bytes -> bytes') + -- ^ map from 'bytes' to `bytes'` + -> (bytes' -> bytes) + -- ^ its inverse + -> Codec ps failure m bytes + -- ^ codec + -> Codec ps failure m bytes' +isoCodec f finv Codec {encode, decode} = Codec { + encode = \msg -> f $ encode msg, + decode = \tok -> isoDecodeStep f finv <$> decode tok + } + +-- | Modify failure type. +-- +mapFailureCodec + :: Functor m + => (failure -> failure') + -- ^ a function to apply to failure + -> Codec ps failure m bytes + -> Codec ps failure' m bytes +mapFailureCodec f Codec {encode, decode} = Codec { + encode = encode, + decode = \tok -> mapFailureDecodeStep f <$> decode tok + } + + +-- | An incremental decoder with return a value of type @a@. +-- +-- This interface is not designed to be used directly for implementing +-- decoders, only for running them. In real applications it is expected to use +-- libraries for text or binary decoding and to implement appropriate wrappers +-- to match up with this incremental decoder interface. +-- +-- This style of interface already closely matches that provided by libraries +-- such as @attoparsec@ for text formats, and @binary@, @cereal@ and @cborg@ +-- for binary formats. +-- +data DecodeStep bytes failure m a = + + -- | The decoder has consumed the available input and needs more + -- to continue. Provide @'Just'@ if more input is available and + -- @'Nothing'@ otherwise, and you will get a new @'DecodeStep'@. + DecodePartial (Maybe bytes -> m (DecodeStep bytes failure m a)) + + -- | The decoder has successfully finished. This provides the decoded + -- result value plus any unused input. + | DecodeDone a (Maybe bytes) + + -- | The decoder ran into an error. The decoder either used + -- @'fail'@ or was not provided enough input. + | DecodeFail failure + + +-- | Change bytes of 'DecodeStep'. +-- +isoDecodeStep + :: Functor m + => (bytes -> bytes') + -- ^ map from 'bytes' to `bytes'` + -> (bytes' -> bytes) + -- its inverse + -> DecodeStep bytes failure m a + -> DecodeStep bytes' failure m a +isoDecodeStep f finv (DecodePartial g) = DecodePartial (fmap (isoDecodeStep f finv) . g . fmap finv) +isoDecodeStep f _finv (DecodeDone a bytes) = DecodeDone a (fmap f bytes) +isoDecodeStep _f _finv (DecodeFail failure) = DecodeFail failure + + +-- | Change functor in which the codec is running. +-- +hoistDecodeStep + :: ( Functor n ) + => (forall x . m x -> n x) + -- ^ a natural transformation + -> DecodeStep bytes failure m a + -> DecodeStep bytes failure n a +hoistDecodeStep nat step = case step of + DecodeDone a mb -> DecodeDone a mb + DecodeFail fail_AvoidNameShadow -> DecodeFail fail_AvoidNameShadow + DecodePartial k -> DecodePartial (fmap (hoistDecodeStep nat) . nat . k) + + +-- | Modify failure type. +-- +mapFailureDecodeStep + :: Functor m + => (failure -> failure') + -- ^ a function to apply to failure + -> DecodeStep bytes failure m a + -> DecodeStep bytes failure' m a +mapFailureDecodeStep f step = case step of + DecodeDone a mb -> DecodeDone a mb + DecodeFail failure -> DecodeFail (f failure) + DecodePartial k -> DecodePartial (fmap (mapFailureDecodeStep f) . k) + + +-- | Each 'Codec' can use whatever @failure@ type is appropriate. This simple +-- exception type is provided for use by simple codecs (e.g. \"identity\") when +-- nothing more than a 'String' is needed. It is an instance of 'Exception'. +-- +data CodecFailure = CodecFailureOutOfInput + | CodecFailure String + deriving (Eq, Show) + +-- safe instance with @UndecidableInstances@ in scope +instance Exception CodecFailure + + +-- +-- Running decoders +-- + +-- | Run a codec incremental decoder 'DecodeStep' against a list of input. +-- +-- It ignores any unused trailing data. This is useful for demos, quick +-- experiments and tests. +-- +-- See also 'Network.TypedProtocol.Driver.runDecoderWithChannel' +-- +runDecoder :: Monad m + => [bytes] + -- ^ bytes to be fed into the incremental 'DecodeStep' + -> DecodeStep bytes failure m a + -- ^ decoder + -> m (Either failure a) +runDecoder _ (DecodeDone x _trailing) = return (Right x) +runDecoder _ (DecodeFail failure) = return (Left failure) +runDecoder [] (DecodePartial k) = k Nothing >>= runDecoder [] +runDecoder (b:bs) (DecodePartial k) = k (Just b) >>= runDecoder bs + + +-- | A variant of 'runDecoder' that is suitable for \"pure\" monads that have +-- a run function. This includes 'ST', using 'Control.Monad.ST.runST'. +-- +runDecoderPure :: Monad m + => (forall b. m b -> b) + -- ^ run monad 'm' in a pure way, e.g. 'runIdentity' + -> m (DecodeStep bytes failure m a) + -> [bytes] + -- ^ input bytes + -> Either failure a +runDecoderPure runM decoder bs = runM (runDecoder bs =<< decoder) + + +-- +-- Codec properties +-- + +-- | Any message for a protocol, with a 'StateTokenI' constraint which gives access to +-- protocol state. +-- +-- Used where we don't know statically what the state type is, but need the +-- agency and message to match each other. +-- +data AnyMessage ps where + AnyMessage :: forall ps (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => Message ps (st :: ps) (st' :: ps) + -- ^ 'Message' between some states + -> AnyMessage ps + + +-- 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 + + +-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the +-- singleton for the state and the message. +-- +pattern AnyMessageAndAgency :: forall ps. () + => forall (st :: ps) (st' :: ps). + (StateTokenI st, ActiveState st) + => StateToken st + -> Message ps st st' + -> AnyMessage ps +pattern AnyMessageAndAgency stateToken msg <- AnyMessage (getAgency -> (msg, stateToken)) + where + AnyMessageAndAgency _ msg = AnyMessage msg +{-# COMPLETE AnyMessageAndAgency #-} + +-- | Internal view pattern for 'AnyMessageAndAgency' +-- +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 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 +-- value of 'PeerHasAgency' for protocol A, there is a corresponding +-- 'PeerHasAgency' for protocol B of some @st :: ps@. +data SomeState (ps :: Type) where + SomeState + :: forall ps (st :: ps). + ActiveState st + => StateToken st + -- ^ state token for some active state 'st' + -> SomeState ps + +-- | Binary compatibility of two protocols +-- +-- We check the following property: +-- +-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@. +-- +-- 2. When we decode those @bytes@ using codec B, we get a message of protocol +-- @ps@B. +-- +-- 3. When we encode that message again using codec B, we get @bytes@. +-- +-- 4. When we decode those @bytes@ using codec A, we get the original message +-- again. +prop_codec_binary_compatM + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + ) + => Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> m Bool +prop_codec_binary_compatM + codecA codecB stokEq + (AnyMessage (msgA :: Message psA stA stA')) = + let stokA :: StateToken stA + stokA = stateToken + in case stokEq stokA of + SomeState (stokB :: StateToken stB) -> do + -- 1. + let bytesA = encode codecA msgA + -- 2. + r1 <- decode codecB stokB >>= runDecoder [bytesA] + case r1 :: Either failure (SomeMessage stB) of + Left _ -> return False + Right (SomeMessage msgB) -> do + -- 3. + let bytesB = encode codecB msgB + -- 4. + r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB] + case r2 :: Either failure (SomeMessage stA) of + Left _ -> return False + Right (SomeMessage msgA') -> return $ AnyMessage msgA' == AnyMessage msgA + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +prop_codec_binary_compat + :: forall psA psB failure m bytes. + ( Monad m + , Eq (AnyMessage psA) + ) + => (forall a. m a -> a) + -> Codec psA failure m bytes + -> Codec psB failure m bytes + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA + -> Bool +prop_codec_binary_compat runM codecA codecB stokEq msgA = + runM $ prop_codec_binary_compatM codecA codecB stokEq msgA + + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , forall a. Monoid a => Monoid (m a) + ) + => Codec ps failure m bytes + -- ^ first codec + -> Codec ps failure m bytes + -- ^ second codec + -> AnyMessage ps + -- ^ some message + -> m Bool +prop_codecs_compatM codecA codecB + (AnyMessage (msg :: Message ps st st')) = + getAll <$> do r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [encode codecA msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg + Left _ -> return $! All False + <> do r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [encode codecB msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg + Left _ -> return $! All False + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure m bytes. + ( Monad m + , Eq (AnyMessage ps) + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> Codec ps failure m bytes + -> Codec ps failure m bytes + -> AnyMessage ps + -> Bool +prop_codecs_compat run codecA codecB msg = + run $ prop_codecs_compatM codecA codecB msg diff --git a/src/Network/TypedProtocol/Core.hs b/src/Network/TypedProtocol/Core.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Core.hs @@ -0,0 +1,547 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +-- | This module defines the core of the typed protocol framework. +-- +module Network.TypedProtocol.Core + ( -- * Introduction + -- $intro + + -- * Defining protocols + -- $defining + Protocol (..) + , StateTokenI (..) + -- $lemmas + + -- * Engaging in protocols + -- ** PeerRole + , PeerRole (..) + , SingPeerRole (..) + -- ** Agency and its evidence + -- $agency + , Agency (..) + , SingAgency (..) + , RelativeAgency (..) + , Relative + , ReflRelativeAgency (..) + , WeHaveAgencyProof + , TheyHaveAgencyProof + , NobodyHasAgencyProof + -- *** FlipAgency + , FlipAgency + -- *** ActiveState + , IsActiveState (..) + , ActiveState + , notActiveState + , ActiveAgency + , ActiveAgency' (..) + -- ** Pipelining + -- *** IsPipelined + , IsPipelined (..) + -- *** Outstanding + , Outstanding + -- *** N and Nat + , N (..) + , Nat (Succ, Zero) + , natToInt + , unsafeIntToNat + ) where + +import Data.Kind (Constraint, Type) +import Unsafe.Coerce (unsafeCoerce) + +import Data.Singletons + +-- $intro +-- A typed protocol between two peers is defined via a state machine: a +-- collection of protocol states and protocol messages which are transitions +-- between those states. +-- +-- Start from the idea that a protocol is some language of messages sent +-- between two peers. To specify a protocol is to describe what possible +-- sequences of messages are valid. One simple but still relatively expressive +-- way to do this is via a state machine: starting from some initial state, +-- all possible paths through the state machine gives the set of valid protocol +-- traces. This then dictates what a peer participating in a protocol may +-- produce and what it must accept. +-- +-- In this style we have a fixed number of states and in each state there is +-- some number of valid messages that move us on to the next state. This can be +-- illustrated as a graph, which can be a helpful form of documentation. +-- +-- We further constrain this idea by saying that the two peers will use the +-- same state machine and change states in lock-step by sending\/receiving +-- messages. In this approach, for each protocol state, the description +-- dictates which peer has the agency to choose to send a message, while +-- correspondingly the other must be prepared to receive the message. +-- +-- The views of the two peers are dual. In each state one peer can send any +-- message that is valid for the current protocol state while the other +-- must be prepared to receive any valid message for current protocol state. +-- +-- We can also have terminal protocol states in which neither peer has agency. +-- +-- So part of the protocol description is to label each protocol state with +-- the peer that has the agency in that state, or none for terminal states. +-- We use the labels \"client\" and \"server\" for the two peers, but they are +-- in fact symmetric. + + +-- $defining +-- +-- The 'Protocol' type class bundles up all the requirements for a typed +-- protocol, which are in fact all type level constructs. Defining a new +-- protocol and making it an instance of the 'Protocol' class requires the +-- following language extensions: +-- +-- > {-# LANGUAGE GADTs, TypeFamilies, DataKinds #-} +-- +-- The type class itself is indexed on a protocol \"tag\" type. This type +-- does double duty as the /kind/ of the /types/ of the protocol states. +-- +-- We will use as a running example a simple \"ping\/pong\" protocol. (You can +-- see the example in full in "Network.TypedProtocol.PingPong.Type".) In this +-- example protocol the client sends a ping message and the serve must respond +-- with a pong message. The client can also terminate the protocol. So modelled +-- as a state machine this protocol has three states, the one in which the +-- client can send a ping or terminate message, the one in which the server +-- must send a pong, and the terminal state where neither can send anything. +-- We somewhat arbitrarily choose label these protocol states as \"idle\" +-- \"busy\" and \"done\". +-- +-- For this ping pong example the protocol tag and the protocol state types +-- would be defined (via promoted data kinds) as: +-- +-- > data PingPong where +-- > StIdle :: PingPong +-- > StBusy :: PingPong +-- > StDone :: PingPong +-- +-- We use @DataKinds@ promotion here so @StIdle@, @StBusy@ and @StDone@ are +-- /types/ (of /kind/ @PingPong@) representing the three states in this +-- protocol's state machine. @PingPong@ itself is both the kind of these types +-- and is also the tag for protocol. We only ever use these as types, via the +-- @DataKinds@ promotion, never as value level data constructors. +-- +-- Having defined our protocol tag and states we can instantiate the 'Protocol' +-- type class and fill out the other details. +-- +-- The protocol must define what its messages are. These form the state +-- transitions in the protocol state machine. Each transition specifies a +-- \"from\" and \"to\" state as type parameters. This of course determines in +-- which protocol states each message can appear. +-- +-- In the \"ping\/pong\" protocol example, the messages are of course ping and +-- pong, which transition between the two main states. There is also a done +-- message that moves the system into a terminal state. +-- +-- > instance Protocol PingPong where +-- > data Message PingPong from to where +-- > MsgPing :: Message PingPong StIdle StBusy +-- > MsgPong :: Message PingPong StBusy StIdle +-- > MsgDone :: Message PingPong StIdle StDone +-- +-- This says that in the idle state a ping message takes us to the busy state, +-- while a pong message takes us back to idle. Also in the idle state a done +-- message takes us to the done state. +-- +-- It is not required that protocols have any terminal states or corresponding +-- transitions, as in this example, but it is often useful and it aids testing +-- to have protocols that terminate cleanly as it allows them to return a +-- result. +-- +-- As described above, this style of protocol gives agency to only one peer at +-- once. That is, in each protocol state, one peer has agency (the ability to +-- send) and the other does not (it must only receive). +-- +-- In the \"ping\/pong\" protocol example, the idle state is the one in which +-- the client can send a message, and the busy state is the one in which the +-- server must respond. Finally in the done state, neither peer can send any +-- further messages. This arrangement is defined as so: +-- +-- > -- still within the instance Protocol PingPong +-- > type StateAgency StIdle = ClientAgency +-- > type StateAgency StBusy = ServerAgency +-- > type StateAgency StDone = NobodyAgency +-- +-- In this simple protocol there is exactly one state in each category, but in +-- general for non-trivial protocols there may be several protocol states in +-- each category. +-- +-- Finally we need to point which singletons to use for the protocol states +-- +-- > -- still within the instance Protocol PingPong, 'SPingPong' type is what we define next. +-- > type StateToken = SPingPong +-- +-- Furthermore we use singletons to provide term level reflection of type level +-- states. One is required to provide singletons for all types of kind +-- 'PingPong'. These definitions are provided outside of the 'Protocol' type +-- class. This is as simple as providing a GADT: +-- +-- > data SingPingPong (st :: PingPong) where +-- > SingIdle :: SingPingPong StIdle +-- > SingBusy :: SingPingPong StBusy +-- > SingDone :: SingPingPong StDone +-- +-- together with 'StateTokenI' instance (similar to 'SingI' from the +-- "singletons" package): +-- +-- > instance StateTokenI StIdle where stateToken = SingIdle +-- > instance StateTokenI StBusy where stateToken = SingBusy +-- > instance StateTokenI StDone where stateToken = SingDone +-- +-- This and other example protocols are provided in "typed-protocols-examples" +-- package. + +-- | Types for client and server peer roles. As protocol can be viewed from +-- either client or server side. +-- +-- Note that technically \"client\" and \"server\" are arbitrary labels. The +-- framework is completely symmetric between the two peers. +-- +-- This definition is only used as promoted types and kinds, never as values. +-- +data PeerRole = AsClient | AsServer + +-- | Singletons for 'PeerRole'. We provide 'Sing' and 'SingI' instances from +-- the "singletons" package. +-- +type SingPeerRole :: PeerRole -> Type +data SingPeerRole pr where + SingAsClient :: SingPeerRole AsClient + SingAsServer :: SingPeerRole AsServer + +deriving instance Show (SingPeerRole pr) + +type instance Sing = SingPeerRole +instance SingI AsClient where + sing = SingAsClient +instance SingI AsServer where + sing = SingAsServer + +-- $agency +-- The protocols we consider either give agency to one side (one side can send +-- a message) or the protocol terminated. Agency is a (type-level) function of +-- the protocol state, and thus uniquely determined by it. +-- +-- The following types define the necessary type-level machinery and its +-- term-level evidence to provide type-safe API for `typed-protocols`. +-- Required proofs are hidden in an (unexposed) module +-- @Network.TypedProtocol.Lemmas@. + +-- | A promoted data type which denotes three possible agencies a protocol +-- state might be assigned. +-- +data Agency where + -- | The client has agency. + ClientAgency :: Agency + + -- | The server has agency. + ServerAgency :: Agency + + -- | Nobody has agency, terminal state. + NobodyAgency :: Agency + +type SingAgency :: Agency -> Type +data SingAgency a where + SingClientAgency :: SingAgency ClientAgency + SingServerAgency :: SingAgency ServerAgency + SingNobodyAgency :: SingAgency NobodyAgency + +deriving instance Show (SingAgency a) + +type instance Sing = SingAgency +instance SingI ClientAgency where + sing = SingClientAgency +instance SingI ServerAgency where + sing = SingServerAgency +instance SingI NobodyAgency where + sing = SingNobodyAgency + +-- | A promoted data type which indicates the effective agency (which is +-- relative to current role). It is computed by `Relative` type family. +-- +data RelativeAgency where + -- evidence that we have agency + WeHaveAgency :: RelativeAgency + -- evidence that proof the remote side has agency + TheyHaveAgency :: RelativeAgency + -- evidence of protocol termination + NobodyHasAgency :: RelativeAgency +-- TODO: input-output-hk/typed-protocols#57 + + +-- | Compute effective agency with respect to the peer role, for client role, +-- agency is preserved, while for the server role it is flipped. +-- +type Relative :: PeerRole -> Agency -> RelativeAgency +type family Relative pr a where + Relative AsClient ClientAgency = WeHaveAgency + Relative AsClient ServerAgency = TheyHaveAgency + Relative AsClient NobodyAgency = NobodyHasAgency + Relative AsServer ClientAgency = TheyHaveAgency + Relative AsServer ServerAgency = WeHaveAgency + Relative AsServer NobodyAgency = NobodyHasAgency + + +-- | Type equality for 'RelativeAgency' which also carries information about +-- agency. It is isomorphic to a product of 'Agency' singleton and +-- @r :~: r'@, where both @r@ and @r'@ have kind 'RelativeAgency'. +-- +-- This is a proper type with values used by the 'Peer', however they are +-- hidden by using "Network.TypedProtocol.Peer.Client" and +-- "Network.TypedProtocol.Peer.Server" APIs. +-- +type ReflRelativeAgency :: Agency -> RelativeAgency -> RelativeAgency -> Type +data ReflRelativeAgency a r r' where + ReflClientAgency :: ReflRelativeAgency ClientAgency r r + ReflServerAgency :: ReflRelativeAgency ServerAgency r r + ReflNobodyAgency :: ReflRelativeAgency NobodyAgency r r + +-- | Type of the proof that we have the agency. +-- +-- 'ReflClientAgency' has this type only iff `'StateAgency' st ~ 'ClientAgency'` +-- and `pr ~ 'AsClient'`. +-- +-- 'ReflServerAgency' has this type only iff `'StateAgency' st ~ 'ServerAgency'` +-- and `pr ~ 'AsServer'` +-- +type WeHaveAgencyProof :: PeerRole -> ps -> Type +type WeHaveAgencyProof pr st = ReflRelativeAgency + (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) + +-- | Type of the proof that the remote side has the agency. +-- +-- 'ReflClientAgency' has this type only iff `'StateAgency' st ~ 'ClientAgency'` +-- and `pr ~ 'AsServer'`. +-- +-- 'ReflServerAgency' has this type only iff `'StateAgency' st ~ 'ServerAgency'` +-- and `pr ~ 'AsClient'` +-- +type TheyHaveAgencyProof :: PeerRole -> ps -> Type +type TheyHaveAgencyProof pr st = ReflRelativeAgency + (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) + + +-- | Type of the proof that nobody has agency in this state. +-- +-- Only 'ReflNobodyAgency' can fulfil the proof obligation. +-- +type NobodyHasAgencyProof :: PeerRole -> ps -> Type +type NobodyHasAgencyProof pr st = ReflRelativeAgency (StateAgency st) + NobodyHasAgency + (Relative pr (StateAgency st)) + +-- $lemmas +-- +-- The 'Network.TypedProtocol.connect' proof rely on lemmas about the +-- protocol. Specifically they rely on the property that each protocol state is +-- labelled with the agency of one peer or the other, or neither, but never +-- both. This property is true by construction, since we use a type family +-- 'StateAgency' which maps states to agencies, however we still need an evince +-- that cases where both peer have the agency or neither of them has it can be +-- eliminated. +-- +-- The packages defines lemmas (in a hidden module) which are structured as +-- proofs by contradiction, e.g. stating \"if the client and the server have +-- agency for this state then it leads to contradiction\". Contradiction is +-- represented as the 'Void' type that has no values except ⊥. +-- +-- The framework defines protocol-agnostic proofs (in the hidden module +-- `Network.TypedProtocol.Lemmas`) which excludes that the client and server +-- have agency at the same time. +-- +-- * 'exclusionLemma_ClientAndServerHaveAgency', +-- * 'terminationLemma_1', +-- * 'terminationLemma_2'. +-- + +-- | A type class which hides a state token / singleton inside a class +-- dictionary. +-- +-- This is similar to the 'SingI' instance, but specific to protocol state +-- singletons. +-- +class StateTokenI st where + stateToken :: StateToken st + +-- | The protocol type class bundles up all the requirements for a typed +-- protocol. +-- +-- Each protocol consists of four components: +-- +-- * the protocol itself, which is also expected to be the kind of the types +-- of the protocol states. The class is indexed on the protocol itself; +-- * the protocol messages; +-- * a type level map from the protocol states to agency: in each state either +-- client or server or nobody has the agency. +-- * a singleton type for the protocol states (e.g. `StateToken` type family +-- instance), together with 'StateTokenI' instances. +-- +-- It is required provide 'StateToken' type family instance as well as +-- 'StateTokenI' instances for all protocol states. These singletons allow one +-- to pattern match on the state, which is useful when defining codecs, or +-- providing informative error messages, however they are not necessary for +-- proving correctness of the protocol. These type families are similar to +-- 'Sing' and 'SingI' in the "singletons" package. +-- +class Protocol ps where + + -- | The messages for this protocol. It is expected to be a GADT that is + -- indexed by the @from@ and @to@ protocol states. That is the protocol state + -- the message transitions from, and the protocol state it transitions into. + -- These are the edges of the protocol state transition system. + -- + data Message ps (st :: ps) (st' :: ps) + + -- | Associate an 'Agency' for each state. + -- + type StateAgency (st :: ps) :: Agency + + -- | A type family for protocol state token, e.g. term level representation of + -- type level state (also known as singleton). + -- + -- This type family is similar to 'Sing' type class in the "singletons" + -- package, but specific for protocol states. + -- + type StateToken :: ps -> Type + + +-- | Evidence that one side of the protocol has the agency, and thus that the +-- protocol hasn't yet terminated. +-- +type ActiveAgency' :: ps -> Agency -> Type +data ActiveAgency' st agency where + -- | Evidence that the client has the agency. + ClientHasAgency :: StateAgency st ~ ClientAgency + => ActiveAgency' st ClientAgency + -- | Evidence that the server has the agency. + ServerHasAgency :: StateAgency st ~ ServerAgency + => ActiveAgency' st ServerAgency + +deriving instance Show (ActiveAgency' st agency) + +-- | Evidence that the protocol isn't in a terminal state. +-- +type ActiveAgency :: ps -> Type +type ActiveAgency st = ActiveAgency' st (StateAgency st) + + +-- | A type class which restricts states to ones that have `ClientAgency` or +-- `ServerAgency`, excluding `NobodyAgency`. +-- +-- One can use `notActive' to eliminate cases for which both @'IsActiveState' +-- st@ is in scope and for which we have an evidence that the state is not +-- active (i.e. a singleton). This is useful when writing a 'Codec'. +-- +class IsActiveState st (agency :: Agency) where + activeAgency :: ActiveAgency' st agency + +instance ClientAgency ~ StateAgency st + => IsActiveState st ClientAgency where + activeAgency = ClientHasAgency +instance ServerAgency ~ StateAgency st + => IsActiveState st ServerAgency where + activeAgency = ServerHasAgency + +-- | A constraint which provides an evidence that the protocol isn't in +-- a terminal state. +-- +type ActiveState :: ps -> Constraint +type ActiveState st = IsActiveState st (StateAgency st) + + +-- | This is useful function to eliminate cases where the `ActiveState st` is +-- provided but we are given a state in which neither side has agency +-- (`NobodyAgency`). For example when writing a codec, we only need to encode +-- / decode messages which are in active states, but to make such functions +-- total, `notActiveState` needs to be used to eliminate the states in which +-- nobody has agency. +-- +-- A good analogy for this function is @'Data.Void.absurd' :: 'Void' -> a@. +-- +notActiveState :: forall ps (st :: ps). + StateAgency st ~ NobodyAgency + => ActiveState st + => StateToken st + -> forall a. a +notActiveState (_ :: StateToken st) = + case activeAgency :: ActiveAgency st of {} + + +-- | A type function to flip the client and server roles. +-- +type FlipAgency :: PeerRole -> PeerRole +type family FlipAgency pr where + FlipAgency AsClient = AsServer + FlipAgency AsServer = AsClient + + +-- | A type level inductive natural number. +data N = Z | S N + +-- | Promoted data type which indicates if 'Peer' is used in +-- pipelined mode or not. +-- +data IsPipelined where + -- | Pipelined peer which is using `c :: Type` for collecting responses + -- from a pipelined messages. 'N' indicates depth of pipelining. + Pipelined :: N -> Type -> IsPipelined + + -- | Non-pipelined peer. + NonPipelined :: IsPipelined + +-- | Type level count of the number of outstanding pipelined yields for which +-- we have not yet collected a receiver result. Used to +-- ensure that 'Collect' is only used when there are outstanding results to +-- collect (e.g. after 'YieldPipeliend' was used); +-- and to ensure that the non-pipelined primitives 'Yield', 'Await' and 'Done' +-- are only used when there are none unsatisfied pipelined requests. +-- +type Outstanding :: IsPipelined -> N +type family Outstanding pl where + Outstanding 'NonPipelined = Z + Outstanding ('Pipelined n _) = n + +-- | A value level inductive natural number, indexed by the corresponding type +-- level natural number 'N'. +-- +-- This is often needed when writing pipelined peers to be able to count the +-- number of outstanding pipelined yields, and show to the type checker that +-- 'Network.TypedProtocol.Peer.Collect' and 'Network.TypedProtocol.Peer.Done' +-- are being used correctly. +-- +newtype Nat (n :: N) = UnsafeInt Int + deriving Show via Int + +data IsNat (n :: N) where + IsZero :: IsNat Z + IsSucc :: Nat n -> IsNat (S n) + +toIsNat :: Nat n -> IsNat n +toIsNat (UnsafeInt 0) = unsafeCoerce IsZero +toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n))) + +pattern Zero :: () => Z ~ n => Nat n +pattern Zero <- (toIsNat -> IsZero) where + Zero = UnsafeInt 0 + +pattern Succ :: () => (m ~ S n) => Nat n -> Nat m +pattern Succ n <- (toIsNat -> IsSucc n) where + Succ (UnsafeInt n) = UnsafeInt (succ n) + +{-# COMPLETE Zero, Succ #-} + +natToInt :: Nat n -> Int +natToInt (UnsafeInt n) = n + +unsafeIntToNat :: Int -> Nat n +unsafeIntToNat = UnsafeInt diff --git a/src/Network/TypedProtocol/Driver.hs b/src/Network/TypedProtocol/Driver.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Driver.hs @@ -0,0 +1,342 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | Actions for running 'Peer's with a 'Driver' +-- +module Network.TypedProtocol.Driver + ( -- * Introduction + -- $intro + -- * Driver interface + Driver (..) + , SomeMessage (..) + -- * Normal peers + , runPeerWithDriver + -- * Pipelined peers + , runPipelinedPeerWithDriver + ) where + +import Data.Void (Void) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer + +import Control.Concurrent.Class.MonadSTM.TQueue +import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadFork +import Control.Monad.Class.MonadSTM + + +-- $intro +-- +-- A 'Peer' is a particular implementation of an agent that engages in a +-- typed protocol. To actually run one we need an untyped channel representing +-- one end of an untyped duplex message transport, which allows to send and +-- receive bytes. One will also need a 'Codec' which handles conversion +-- between the typed protocol messages and the untyped channel. +-- +-- Given the 'Peer', a compatible 'Network.TypedProtocol.Codec.Codec' and +-- an untyped channel we can run the peer in some appropriate monad (e.g. 'IO', +-- or a simulation monad for testing purposes). The peer and codec have to +-- agree on the same protocol. The codec and channel have to agree on the same +-- untyped medium, e.g. text or bytes. All three have to agree on the same +-- monad in which they will run. +-- +-- This module provides drivers for normal and pipelined peers. There is +-- very little policy involved here so typically it should be possible to +-- use these drivers, and customise things by adjusting the peer, or codec +-- or channel (together with an implementation of a 'Driver' based on it). +-- +-- For implementing a 'Driver' based on some untyped channel, the +-- 'Network.TypedProtocol.Codec.runDecoder' function may be a helpful utility. +-- +-- For a possible definition of an untyped channel and how to construct +-- a `Driver` from it see @typed-protocols-examples@ package. For production +-- grade examples see https://github.com/IntersectMBO/ouroboros-network +-- repository. + + +-- +-- Driver interface +-- + +data Driver ps (pr :: PeerRole) dstate m = + Driver { + -- | Send a message; the message must transition from an active state. + -- One needs to supply agency evidence. + sendMessage :: forall (st :: ps) (st' :: ps). + StateTokenI st + => StateTokenI st' + => ActiveState st + => WeHaveAgencyProof pr st + -- agency evidence + -> Message ps st st' + -- message to send + -> m () + + -- | Receive some message, since we don't know the final state of + -- the protocol it is wrapped in `SomeMessage` type; the message must + -- transition from an active state. One needs to supply agency + -- evidence. + -- + , recvMessage :: forall (st :: ps). + StateTokenI st + => ActiveState st + => TheyHaveAgencyProof pr st + -- agency evidence + -> dstate + -- current driver state + -> m (SomeMessage st, dstate) + -- received message together with new driver state + + , -- | Initial state of the driver + initialDState :: dstate + } +-- TODO: input-output-hk/typed-protocols#57 + + +-- | When decoding a 'Message' we only know the expected \"from\" state. We +-- cannot know the \"to\" state as this depends on the message we decode. To +-- resolve this we use the 'SomeMessage' wrapper which uses an existential +-- type to hide the \"to"\ state. +-- +data SomeMessage (st :: ps) where + SomeMessage :: ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => Message ps st st' -> SomeMessage st + + +-- +-- Running normal non-pipelined peers +-- + +-- | Run a peer with the given driver. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +runPeerWithDriver + :: forall ps (st :: ps) pr dstate m a. + Monad m + => Driver ps pr dstate m + -> Peer ps pr NonPipelined st m a + -> m (a, dstate) +runPeerWithDriver Driver{sendMessage, recvMessage, initialDState} = + go initialDState + where + go :: forall st'. + dstate + -> 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 (Yield refl msg k) = do + sendMessage refl msg + go dstate k + + go dstate (Await refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl dstate + go dstate' (k msg) + + -- Note that we do not complain about trailing data in any case, neither + -- the 'Await' nor 'Done' cases. + -- + -- We want to be able to use a non-pipelined peer in communication with + -- a pipelined peer, and in that case the non-pipelined peer will in + -- general see trailing data after an 'Await' which is the next incoming + -- message. + -- + -- Likewise for 'Done', we want to allow for one protocols to be run after + -- another on the same channel. It would be legal for the opening message + -- of the next protocol arrives in the same data chunk as the final + -- message of the previous protocol. + + +-- +-- Running pipelined peers +-- + +-- | Run a pipelined peer with the given driver. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +-- Unlike normal peers, running pipelined peers rely on concurrency, hence the +-- 'MonadAsync' constraint. +-- +runPipelinedPeerWithDriver + :: forall ps (st :: ps) pr dstate m a. + MonadAsync m + => 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 + `withAsyncLoop` + runPipelinedPeerSender receiveQueue collectQueue driver + peer initialDState + return a + + where + withAsyncLoop :: m Void -> m x -> m x + withAsyncLoop left right = do + -- race will throw if either of the threads throw + res <- race left right + case res of + Left v -> case v of {} + Right a -> return a + +data ReceiveHandler dstate ps pr m c where + ReceiveHandler :: MaybeDState dstate n + -> Receiver ps pr (st :: ps) (st' :: ps) m c + -> ReceiveHandler dstate ps pr m c + +-- | The handling of trailing data here is quite subtle. Trailing data is data +-- we have read from the channel but the decoder has told us that it comes +-- after the message we decoded. So it potentially belongs to the next message +-- to decode. +-- +-- We read from the channel on both the 'runPipelinedPeerSender' and the +-- 'runPipelinedPeerReceiver', and we synchronise our use of trailing data +-- between the two. The scheme for the sender and receiver threads using the +-- channel ensures that only one can use it at once: +-- +-- * When there are zero outstanding pipelined receiver handlers then the +-- sending side is allowed to access the channel directly (to do synchronous +-- yield\/awaits). Correspondingly the receiver side is idle and not +-- accessing the channel. +-- * When there are non-zero outstanding pipelined receiver handlers then +-- the receiver side can access the channel, but the sending side is not +-- permitted to do operations that access the channel. +-- +-- So the only times we need to synchronise the trailing data are the times +-- when the right to access the channel passes from one side to the other. +-- +-- The transitions are as follows: +-- +-- * There having been Zero outstanding pipelined requests there is now a +-- new pipelined yield. In this case we must pass the trailing data from +-- the sender thread to the receiver thread. We pass it with the +-- 'ReceiveHandler'. +-- +-- * When the last pipelined request is collected. In this case we must pass +-- the trailing data from the receiver thread to the sender thread. We pass +-- it with the collected result. +-- +-- Note that the receiver thread cannot know what the last pipelined request +-- is, that is tracked on the sender side. So the receiver thread always +-- returns the trailing data with every collected result. It is for the sender +-- thread to decide if it needs to use it. For the same reason, the receiver +-- thread ends up retaining the last trailing data (as well as passing it to +-- the sender). So correspondingly when new trailing data is passed to the +-- receiver thread, it simply overrides any trailing data it already had, since +-- we now know that copy to be stale. +-- +data MaybeDState dstate (n :: N) where + HasDState :: dstate -> MaybeDState dstate Z + NoDState :: MaybeDState dstate (S n) + + +runPipelinedPeerSender + :: forall ps (st :: ps) pr dstate c m a. + ( MonadSTM m + , MonadThread m + ) + => TQueue m (ReceiveHandler dstate ps pr m c) + -> TQueue m (c, dstate) + -> Driver ps pr dstate m + -> Peer ps pr ('Pipelined Z c) st m a + -> dstate + -> m (a, dstate) +runPipelinedPeerSender receiveQueue collectQueue + Driver{sendMessage, recvMessage} + peer dstate0 = do + threadId <- myThreadId + labelThread threadId "pipelined-peer-sender" + go Zero (HasDState dstate0) peer + where + go :: forall st' n. + Nat n + -> MaybeDState dstate n + -> Peer ps pr ('Pipelined n c) st' m a + -> m (a, dstate) + go n dstate (Effect k) = k >>= go n dstate + go Zero (HasDState dstate) (Done _ x) = return (x, dstate) + + go Zero dstate (Yield refl msg k) = do + sendMessage refl msg + go Zero dstate k + + go Zero (HasDState dstate) (Await stok k) = do + (SomeMessage msg, dstate') <- recvMessage stok dstate + go Zero (HasDState dstate') (k msg) + + go n dstate (YieldPipelined refl msg receiver k) = do + atomically (writeTQueue receiveQueue (ReceiveHandler dstate receiver)) + sendMessage refl msg + go (Succ n) NoDState k + + go (Succ n) NoDState (Collect Nothing k) = do + (c, dstate) <- atomically (readTQueue collectQueue) + case n of + Zero -> go Zero (HasDState dstate) (k c) + Succ n' -> go (Succ n') NoDState (k c) + + go (Succ n) NoDState (Collect (Just k') k) = do + mc <- atomically (tryReadTQueue collectQueue) + case mc of + Nothing -> go (Succ n) NoDState k' + Just (c, dstate) -> + case n of + Zero -> go Zero (HasDState dstate) (k c) + Succ n' -> go (Succ n') NoDState (k c) + + +runPipelinedPeerReceiverQueue + :: forall ps pr dstate m c. + ( MonadSTM m + , MonadThread m + ) + => TQueue m (ReceiveHandler dstate ps pr m c) + -> TQueue m (c, dstate) + -> Driver ps pr dstate m + -> m Void +runPipelinedPeerReceiverQueue receiveQueue collectQueue + driver@Driver{initialDState} = do + threadId <- myThreadId + labelThread threadId "pipelined-receiver-queue" + go initialDState + where + go :: dstate -> m Void + go receiverDState = do + ReceiveHandler senderDState receiver + <- atomically (readTQueue receiveQueue) + let dstate = case (senderDState, receiverDState) of + (HasDState t, _) -> t + (NoDState, t) -> t + x@(!_c, !dstate') <- runPipelinedPeerReceiver driver dstate receiver + atomically (writeTQueue collectQueue x) + go dstate' + + +runPipelinedPeerReceiver + :: forall ps (st :: ps) (stdone :: ps) pr dstate m c. + Monad m + => Driver ps pr dstate m + -> dstate + -> Receiver ps pr (st :: ps) (stdone :: ps) m c + -> m (c, dstate) +runPipelinedPeerReceiver Driver{recvMessage} = go + where + go :: forall st' st''. + dstate + -> Receiver ps pr st' st'' m c + -> m (c, dstate) + go dstate (ReceiverEffect k) = k >>= go dstate + + go dstate (ReceiverDone x) = return (x, dstate) + + go dstate (ReceiverAwait refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl dstate + go dstate' (k msg) diff --git a/src/Network/TypedProtocol/Lemmas.hs b/src/Network/TypedProtocol/Lemmas.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Lemmas.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use camelCase" #-} + +-- | The module contains exclusion lemmas which are proven using ad absurdum: +-- +-- * it's impossible for both client and server have agency +-- * it's impossible for either side to be in a terminal state (no agency) and +-- the other side have agency +-- +module Network.TypedProtocol.Lemmas where + +import Data.Kind (Type) +import Network.TypedProtocol.Core + + +-- $about +-- +-- Typed languages such as Haskell can embed proofs. In total languages this +-- is straightforward: a value inhabiting a type is a proof of the property +-- corresponding to the type. +-- +-- In languages like Haskell that have ⊥ as a value of every type, things +-- are slightly more complicated. We have to demonstrate that the value that +-- inhabits the type of interest is not ⊥ which we can do by evaluation. +-- +-- This idea crops up frequently in advanced type level programming in Haskell. +-- For example @Refl@ proofs that two types are equal have to have a runtime +-- representation that is evaluated to demonstrate it is not ⊥ before it +-- can be relied upon. +-- +-- The proofs here are about the nature of typed protocols in this framework. +-- The 'connect' and 'connectPipelined' proofs rely on a few internal lemmas. + +-- | An evidence that both relative agencies are equal to 'NobodyHasAgency'. +-- +type ReflNobodyHasAgency :: RelativeAgency -> RelativeAgency -> Type +data ReflNobodyHasAgency ra ra' where + ReflNobodyHasAgency :: ReflNobodyHasAgency + NobodyHasAgency + NobodyHasAgency + + +-- | A proof that if both @Relative pr a@ and @Relative (FlipAgency pr) a@ are +-- equal then nobody has agency. In particular this lemma excludes the +-- possibility that client and server has agency at the same state. +-- +exclusionLemma_ClientAndServerHaveAgency + :: forall (pr :: PeerRole) (a :: Agency) + (ra :: RelativeAgency). + SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -- ^ evidence that `ra` is equal to `Relative pr a`, e.g. that client has + -- agency + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -- ^ evidence that `ra` is equal to `Relative (FlipAgency pr) a`, e.g. that + -- the server has agency + -> ReflNobodyHasAgency (Relative pr a) + (Relative (FlipAgency pr) a) + -- ^ derived evidence that nobody has agency in that case +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency + +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflClientAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflClientAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflServerAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflServerAgency x = case x of {} + + +-- | A proof that if one side has terminated, then the other side terminated as +-- well. +-- +terminationLemma_1 + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -> ReflRelativeAgency a NobodyHasAgency (Relative (FlipAgency pr) a) + -> ReflNobodyHasAgency (Relative pr a) + (Relative (FlipAgency pr) a) +terminationLemma_1 + SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +terminationLemma_1 + SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +terminationLemma_1 SingAsClient ReflClientAgency x = case x of {} +terminationLemma_1 SingAsClient ReflServerAgency x = case x of {} +terminationLemma_1 SingAsServer ReflClientAgency x = case x of {} +terminationLemma_1 SingAsServer ReflServerAgency x = case x of {} + + +-- | Internal; only need to formulate auxiliary lemmas in the proof of +-- 'terminationLemma_2'. +-- +type FlipRelAgency :: RelativeAgency -> RelativeAgency +type family FlipRelAgency ra where + FlipRelAgency WeHaveAgency = TheyHaveAgency + FlipRelAgency TheyHaveAgency = WeHaveAgency + FlipRelAgency NobodyHasAgency = NobodyHasAgency + + +-- | Similar to 'terminationLemma_1'. +-- +-- Note: this could be proven the same way 'terminationLemma_1' is proved, but +-- instead we use two lemmas to reduce the assumptions (arguments) and we apply +-- 'terminationLemma_1'. +-- +terminationLemma_2 + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -> ReflRelativeAgency a NobodyHasAgency (Relative pr a) + -> ReflNobodyHasAgency (Relative (FlipAgency pr) a) + (Relative pr a) + +terminationLemma_2 singPeerRole refl refl' = + case terminationLemma_1 singPeerRole + (lemma_flip singPeerRole refl) + (lemma_flip' singPeerRole refl') + of x@ReflNobodyHasAgency -> x + -- note: if we'd swap arguments of the returned @ReflNobodyHasAgency@ type, + -- we wouldn't need to pattern match on the result. But in this form the + -- lemma is a symmetric version of 'terminationLemma_1'. + where + lemma_flip + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -> ReflRelativeAgency a (FlipRelAgency ra) (Relative pr a) + + lemma_flip' + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -> ReflRelativeAgency a (FlipRelAgency ra) (Relative (FlipAgency pr) a) + + -- both lemmas are identity functions: + lemma_flip SingAsClient ReflClientAgency = ReflClientAgency + lemma_flip SingAsClient ReflServerAgency = ReflServerAgency + lemma_flip SingAsClient ReflNobodyAgency = ReflNobodyAgency + lemma_flip SingAsServer ReflClientAgency = ReflClientAgency + lemma_flip SingAsServer ReflServerAgency = ReflServerAgency + lemma_flip SingAsServer ReflNobodyAgency = ReflNobodyAgency + + lemma_flip' SingAsClient ReflClientAgency = ReflClientAgency + lemma_flip' SingAsClient ReflServerAgency = ReflServerAgency + lemma_flip' SingAsClient ReflNobodyAgency = ReflNobodyAgency + lemma_flip' SingAsServer ReflClientAgency = ReflClientAgency + lemma_flip' SingAsServer ReflServerAgency = ReflServerAgency + lemma_flip' SingAsServer ReflNobodyAgency = ReflNobodyAgency diff --git a/src/Network/TypedProtocol/Peer.hs b/src/Network/TypedProtocol/Peer.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Peer.hs @@ -0,0 +1,273 @@ +{-# LANGUAGE DerivingVia #-} + +-- | Protocol EDSL. +-- +module Network.TypedProtocol.Peer + ( Peer (..) + , PeerPipelined (..) + , Receiver (..) + , Outstanding + , N (..) + , Nat (Zero, Succ) + , natToInt + , unsafeIntToNat + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core as Core + +-- | A description of a peer that engages in a protocol. +-- +-- __Note__: You should use pattern synonyms exposed in +-- "Network.TypedProtocol.Peer.Client" and "Network.TypedProtocol.Peer.Server", +-- however here we provide in-depth documentation. +-- +-- The protocol describes what messages peers /may/ send or /must/ accept. +-- A particular peer implementation decides what to actually do within the +-- constraints of the protocol. +-- +-- Peers engage in a protocol in either the client or server role. Of course +-- the client role can only interact with the serve role for the same protocol +-- and vice versa. +-- +-- 'Peer' has several type arguments: +-- +-- * the protocol itself; +-- * the client\/server role; +-- * whether the peer is using pipelining or not, if pipelined it holds the +-- depth of pipelining and a type used to collect data from pipelined +-- transitions; +-- * the current protocol state; +-- * the monad in which the peer operates (e.g. 'IO'); +-- * the type of the final result once the peer terminates. +-- +-- For example: +-- +-- > pingPongClientExample :: Peer PingPong AsClient (Pipelined Z Int) StIdle IO () +-- > pingPongServerExample :: Peer PingPong AsServer NonPipeliend StIdle IO Int +-- +-- The actions that a non-pipelining peer can take are: +-- +-- * to perform local monadic effects +-- * to terminate with a result (but only in a terminal protocol state) +-- * to send a message (but only in a protocol state in which we have agency) +-- * to wait to receive a message (but only in a protocol state in which the +-- other peer has agency) +-- +-- In addition a pipelining peer can: +-- +-- * pipeline a message, which requires upfront declaration at which state we +-- continue at and passing a receiver which will run in parallel. When +-- receiver terminates it pushes the result into the pipelining queue. +-- * collect a response from the pipelining queue. +-- +-- The 'Yield', 'Await', 'Done', 'YieldPipelined', 'Collect', +-- constructors require to provide an evidence that the +-- peer has agency in the current state. The types guarantee that it is not +-- possible to supply incorrect evidence, however the +-- pattern synonyms exposed in "Network.TypedProtocol.Peer.Client" and +-- "Network.TypedProtocol.Peer.Client" supply this evidence for you, and hence +-- are easier to use and let you avoid some kinds of type errors. +-- +-- __NOTE__: +-- one should not allocate resources within a `Peer` since there's no way to +-- safely clean-up resources in case of an asynchronous exception. The proper +-- way to allocate resources is to call +-- `Network.TypedProtocol.Driver.runPeerWithDriver` (or `runPeer`, +-- `runPipelinedPeer`) within a `Control.Exception.bracket`. +-- +type Peer :: forall ps + -> PeerRole + -> IsPipelined + -> ps + -> (Type -> Type) + -- ^ monad's kind + -> Type + -> Type +data Peer ps pr pl st m a where + + -- | Perform a local monadic effect and then continue. + -- + -- Example: + -- + -- > Effect $ do + -- > ... -- actions in the monad + -- > return $ ... -- another Peer value + -- + Effect + :: forall ps pr pl st m a. + m (Peer ps pr pl st m a) + -- ^ monadic continuation + -> Peer ps pr pl st m a + + -- | Send a message to the other peer and then continue. This takes the + -- message and the continuation. It also requires evidence that we have + -- agency for this protocol state and thus are allowed to send messages. + -- + -- Example: + -- + -- > Yield ReflClientAgency MsgPing $ ... + -- + Yield + :: forall ps pr pl (st :: ps) (st' :: ps) m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + , Outstanding pl ~ Z + ) + => WeHaveAgencyProof pr st + -- ^ agency proof + -> Message ps st st' + -- ^ protocol message + -> Peer ps pr pl st' m a + -- ^ continuation + -> Peer ps pr pl st m a + + -- | Waits to receive a message from the other peer and then continues. + -- This takes the continuation that is supplied with the received message. It + -- also requires evidence that the other peer has agency for this protocol + -- state and thus we are expected to wait to receive messages. + -- + -- Note that the continuation that gets supplied with the message must be + -- prepared to deal with /any/ message that is allowed in /this/ protocol + -- state. This is why the continuation /must/ be polymorphic in the target + -- state of the message (the third type argument of 'Message'). + -- + -- Example: + -- + -- > Await ReflClientAgency $ \msg -> + -- > case msg of + -- > MsgDone -> ... + -- > MsgPing -> ... + -- + Await + :: forall ps pr pl (st :: ps) m a. + ( StateTokenI st + , ActiveState st + , Outstanding pl ~ Z + ) + => TheyHaveAgencyProof pr st + -- ^ agency proof + -> (forall (st' :: ps). Message ps st st' + -> Peer ps pr pl st' m a) + -- ^ continuation + -> Peer ps pr pl st m a + + -- | Terminate with a result. A state token must be provided from the + -- 'NobodyHasAgency' states, to show that this is a state in which we can + -- terminate. + -- + -- Example: + -- + -- > Yield ReflClientAgency + -- > MsgDone + -- > (Done ReflNobodyAgency TokDone result) + -- + Done + :: forall ps pr pl (st :: ps) m a. + ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => NobodyHasAgencyProof pr st + -- ^ (no) agency proof + -> a + -- ^ returned value + -> Peer ps pr pl st m a + + -- + -- Pipelining primitives + -- + + -- | Pipelined send. We statically decide from which state we continue (the + -- `st''` state here), the gap (between `st'` and `st''`) must be fulfilled + -- by 'Receiver' which runs will run in parallel. + -- + YieldPipelined + :: forall ps pr (st :: ps) (st' :: ps) c n st'' m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => WeHaveAgencyProof pr st + -- ^ agency proof + -> Message ps st st' + -- ^ protocol message + -> Receiver ps pr st' st'' m c + -- ^ receiver + -> Peer ps pr (Pipelined (S n) c) st'' m a + -- ^ continuation from state `st''` + -> Peer ps pr (Pipelined n c) st m a + + -- | Collect results returned by a `Receiver`. Results are collected in the + -- first-in-first-out way. + -- + Collect + :: forall ps pr c n st m a. + ( StateTokenI st + , ActiveState st + ) + => Maybe (Peer ps pr (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Peer ps pr (Pipelined n c) st m a) + -- ^ continuation + -> Peer ps pr (Pipelined (S n) c) st m a + +deriving instance Functor m => Functor (Peer ps pr pl st m) + + +-- | Receiver. It is limited to only awaiting for messages and running monadic +-- computations. This means that one can only pipeline messages if they can be +-- connected by state transitions which all have remote agency. +-- +-- The receiver runs in parallel, see `runPipelinedPeerWithDriver`. This makes +-- pipelining quite effective, since the receiver callbacks are called in +-- a separate thread which can effectively use CPU cache and can avoids +-- unnecessary context switches. +-- +type Receiver :: forall ps + -> PeerRole + -> ps + -- ^ initial state + -> ps + -- ^ final state + -> (Type -> Type) + -- ^ monad + -> Type + -- ^ returned type by the receiver + -> Type +data Receiver ps pr st stdone m c where + + -- | Execute a monadic computation. + -- + ReceiverEffect :: m (Receiver ps pr st stdone m c) + -> Receiver ps pr st stdone m c + + -- | Return value. + -- + ReceiverDone :: c -> Receiver ps pr stdone stdone m c + + -- | Await for for a remote transition. + -- + ReceiverAwait :: ( StateTokenI st + , ActiveState st + ) + => TheyHaveAgencyProof pr st + -> (forall st'. Message ps st st' + -> Receiver ps pr st' stdone m c) + -> Receiver ps pr st stdone m c + +deriving instance Functor m => Functor (Receiver ps pr st stdone m) + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +-- This type is useful for wrapping pipelined peers to hide information which +-- is only relevant in peer lift. It is expected by +-- `Network.TypedProtocol.Driver.runPeerPipelinedWithDriver`. +-- +data PeerPipelined ps pr (st :: ps) m a where + PeerPipelined :: { runPeerPipelined :: Peer ps pr (Pipelined Z c) st m a } + -> PeerPipelined ps pr st m a + +deriving instance Functor m => Functor (PeerPipelined ps pr st m) diff --git a/src/Network/TypedProtocol/Peer/Client.hs b/src/Network/TypedProtocol/Peer/Client.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Peer/Client.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsClient'@. The advantage of +-- these patterns is that they automatically provide the 'ReflRelativeAgency' +-- evidence. +-- +module Network.TypedProtocol.Peer.Client + ( -- * Client type alias and its pattern synonyms + Client + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + , pattern YieldPipelined + , pattern Collect + -- * Receiver type alias and its pattern synonyms + , Receiver + , pattern ReceiverEffect + , pattern ReceiverAwait + , pattern ReceiverDone + -- * ClientPipelined type alias and its pattern synonym + , ClientPipelined + , TP.PeerPipelined (ClientPipelined, runClientPipelined) + -- * re-exports + , IsPipelined (..) + , Outstanding + , N (..) + , Nat (..) + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer (Peer) +import Network.TypedProtocol.Peer qualified as TP + + +type Client :: forall ps + -> IsPipelined + -> ps + -> (Type -> Type) + -> Type + -> Type +type Client ps pl st m a = Peer ps AsClient pl st m a + + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +type ClientPipelined ps st m a = TP.PeerPipelined ps AsClient st m a + +pattern ClientPipelined :: forall ps st m a. + () + => forall c. + () + => Client ps (Pipelined Z c) st m a + -> ClientPipelined ps st m a +pattern ClientPipelined { runClientPipelined } = TP.PeerPipelined runClientPipelined + +{-# COMPLETE ClientPipelined #-} + +-- | Client role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps pl st m a. + m (Client ps pl st m a) + -- ^ monadic continuation + -> Client ps pl st m a +pattern Effect mclient = TP.Effect mclient + + +-- | Client role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps pl st m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + , Outstanding pl ~ Z + ) + => Message ps st st' + -- ^ protocol message + -> Client ps pl st' m a + -- ^ continuation + -> Client ps pl st m a +pattern Yield msg k = TP.Yield ReflClientAgency msg k + + +-- | Client role pattern for 'TP.Await' +-- +pattern Await :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ ServerAgency + , Outstanding pl ~ Z + ) + => (forall st'. Message ps st st' + -> Client ps pl st' m a) + -- ^ continuation + -> Client ps pl st m a +pattern Await k = TP.Await ReflServerAgency k + + +-- | Client role pattern for 'TP.Done' +-- +pattern Done :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => a + -- ^ protocol return value + -> Client ps pl st m a +pattern Done a = TP.Done ReflNobodyAgency a + + +-- | Client role pattern for 'TP.YieldPipelined' +-- +pattern YieldPipelined :: forall ps st n c m a. + () + => forall st' st''. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + ) + => Message ps st st' + -- ^ pipelined message + -> Receiver ps st' st'' m c + -> Client ps (Pipelined (S n) c) st'' m a + -- ^ continuation + -> Client ps (Pipelined n c) st m a +pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflClientAgency msg receiver k + + +-- | Client role pattern for 'TP.Collect' +-- +pattern Collect :: forall ps st n c m a. + () + => ( StateTokenI st + , ActiveState st + ) + => Maybe (Client ps (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Client ps (Pipelined n c) st m a) + -- ^ continuation + -> Client ps (Pipelined (S n) c) st m a +pattern Collect k' k = TP.Collect k' k + +{-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-} + + +type Receiver ps st stdone m c = TP.Receiver ps AsClient st stdone m c + +pattern ReceiverEffect :: forall ps st stdone m c. + m (Receiver ps st stdone m c) + -> Receiver ps st stdone m c +pattern ReceiverEffect k = TP.ReceiverEffect k + +pattern ReceiverAwait :: forall ps st stdone m c. + () + => ( StateTokenI st + , ActiveState st + , StateAgency st ~ ServerAgency + ) + => (forall st'. Message ps st st' + -> Receiver ps st' stdone m c + ) + -> Receiver ps st stdone m c +pattern ReceiverAwait k = TP.ReceiverAwait ReflServerAgency k + +pattern ReceiverDone :: forall ps stdone m c. + c + -> Receiver ps stdone stdone m c +pattern ReceiverDone c = TP.ReceiverDone c + +{-# COMPLETE ReceiverEffect, ReceiverAwait, ReceiverDone #-} diff --git a/src/Network/TypedProtocol/Peer/Server.hs b/src/Network/TypedProtocol/Peer/Server.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Peer/Server.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TypeOperators #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsServer'@. The advantage of +-- these patterns is that they automatically provide the 'ReflRelativeAgency' +-- evidence. +-- +module Network.TypedProtocol.Peer.Server + ( -- * Server type alias and its pattern synonyms + Server + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + , pattern YieldPipelined + , pattern Collect + -- * Receiver type alias and its pattern synonyms + , Receiver + , pattern ReceiverEffect + , pattern ReceiverAwait + , pattern ReceiverDone + -- * ServerPipelined type alias and its pattern synonym + , ServerPipelined + , TP.PeerPipelined (ServerPipelined, runServerPipelined) + -- * re-exports + , IsPipelined (..) + , Outstanding + , N (..) + , Nat (..) + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer (Peer) +import Network.TypedProtocol.Peer qualified as TP + + +type Server :: forall ps + -> IsPipelined + -> ps + -> (Type -> Type) + -> Type + -> Type +type Server ps pl st m a = Peer ps AsServer pl st m a + + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +type ServerPipelined ps st m a = TP.PeerPipelined ps AsServer st m a + +pattern ServerPipelined :: forall ps st m a. + () + => forall c. + () + => Server ps (Pipelined Z c) st m a + -> ServerPipelined ps st m a +pattern ServerPipelined { runServerPipelined } = TP.PeerPipelined runServerPipelined + +{-# COMPLETE ServerPipelined #-} + + +-- | Server role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps pl st m a. + m (Server ps pl st m a) + -- ^ monadic continuation + -> Server ps pl st m a +pattern Effect mclient = TP.Effect mclient + + +-- | Server role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps pl st m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + , Outstanding pl ~ Z + ) + => Message ps st st' + -- ^ protocol message + -> Server ps pl st' m a + -- ^ continuation + -> Server ps pl st m a +pattern Yield msg k = TP.Yield ReflServerAgency msg k + + +-- | Server role pattern for 'TP.Await' +-- +pattern Await :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ ClientAgency + , Outstanding pl ~ Z + ) + => (forall st'. Message ps st st' + -> Server ps pl st' m a) + -- ^ continuation + -> Server ps pl st m a +pattern Await k = TP.Await ReflClientAgency k + + +-- | Server role pattern for 'TP.Done' +-- +pattern Done :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => a + -- ^ protocol return value + -> Server ps pl st m a +pattern Done a = TP.Done ReflNobodyAgency a + + +-- | Server role pattern for 'TP.YieldPipelined' +-- +pattern YieldPipelined :: forall ps st n c m a. + () + => forall st' st''. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + ) + => Message ps st st' + -- ^ pipelined message + -> Receiver ps st' st'' m c + -> Server ps (Pipelined (S n) c) st'' m a + -- ^ continuation + -> Server ps (Pipelined n c) st m a +pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflServerAgency msg receiver k + + +-- | Server role pattern for 'TP.Collect' +-- +pattern Collect :: forall ps st n c m a. + () + => ( StateTokenI st + , ActiveState st + ) + => Maybe (Server ps (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Server ps (Pipelined n c) st m a) + -- ^ continuation + -> Server ps (Pipelined (S n) c) st m a +pattern Collect k' k = TP.Collect k' k + + +{-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-} + + +type Receiver ps st stdone m c = TP.Receiver ps AsServer st stdone m c + +pattern ReceiverEffect :: forall ps st stdone m c. + m (Receiver ps st stdone m c) + -> Receiver ps st stdone m c +pattern ReceiverEffect k = TP.ReceiverEffect k + +pattern ReceiverAwait :: forall ps st stdone m c. + () + => ( StateTokenI st + , ActiveState st + , StateAgency st ~ ClientAgency + ) + => (forall st'. Message ps st st' + -> Receiver ps st' stdone m c + ) + -> Receiver ps st stdone m c +pattern ReceiverAwait k = TP.ReceiverAwait ReflClientAgency k + +pattern ReceiverDone :: forall ps stdone m c. + c + -> Receiver ps stdone stdone m c +pattern ReceiverDone c = TP.ReceiverDone c + +{-# COMPLETE ReceiverEffect, ReceiverAwait, ReceiverDone #-} diff --git a/src/Network/TypedProtocol/Proofs.hs b/src/Network/TypedProtocol/Proofs.hs new file mode 100644 --- /dev/null +++ b/src/Network/TypedProtocol/Proofs.hs @@ -0,0 +1,254 @@ +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeFamilies #-} + +-- This is already implied by the -Wall in the .cabal file, but lets just be +-- completely explicit about it too, since we rely on the completeness +-- checking in the cases below for the completeness of our proofs. +{-# OPTIONS_GHC -Wincomplete-patterns #-} + +-- | Proofs and helpful testing utilities. +-- +module Network.TypedProtocol.Proofs + ( -- * Connect proofs + connect + , connectPipelined + , TerminalStates (..) + -- * Pipelining proofs + -- | Additional proofs specific to the pipelining features + , forgetPipelined + , promoteToPipelined + -- ** Pipeline proof helpers + , Queue (..) + , enqueue + -- ** Auxiliary functions + , pipelineInterleaving + ) where + +import Data.Singletons +import Network.TypedProtocol.Core +import Network.TypedProtocol.Lemmas +import Network.TypedProtocol.Peer + + +-- | The 'connect' function takes two peers that agree on a protocol and runs +-- them in lock step, until (and if) they complete. +-- +-- The 'connect' function serves a few purposes. +-- +-- * The fact we can define this function at at all proves some minimal +-- sanity property of the typed protocol framework. +-- +-- * It demonstrates that all protocols defined in the framework can be run +-- with synchronous communication rather than requiring buffered communication. +-- +-- * It is useful for testing peer implementations against each other in a +-- minimalistic setting. +-- +connect + :: forall ps (pr :: PeerRole) (initSt :: ps) m a b. + (Monad m, SingI pr) + => Peer ps pr NonPipelined initSt m a + -- ^ a peer + -> Peer ps (FlipAgency pr) NonPipelined initSt m b + -- ^ a peer with flipped agency + -> m (a, b, TerminalStates ps) + -- ^ peers results and an evidence of their termination +connect = go + where + singPeerRole :: Sing pr + singPeerRole = sing + + go :: forall (st :: ps). + Peer ps pr NonPipelined st m a + -> Peer ps (FlipAgency pr) NonPipelined st m b + -> m (a, b, TerminalStates ps) + go (Done ReflNobodyAgency a) (Done ReflNobodyAgency b) = + return (a, b, terminals) + where + terminals :: TerminalStates ps + terminals = TerminalStates (stateToken :: StateToken st) + (stateToken :: StateToken st) + + go (Effect a ) b = a >>= \a' -> go a' b + go a (Effect b) = b >>= \b' -> go a b' + go (Yield _ msg a) (Await _ b) = go a (b msg) + go (Await _ a) (Yield _ msg b) = go (a msg) b + + -- By appealing to the proofs about agency for this protocol we can + -- show that these other cases are impossible + go (Yield reflA _ _) (Yield reflB _ _) = + case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} + + go (Await reflA _) (Await reflB _) = + case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} + + go (Done reflA _) (Yield reflB _ _) = + case terminationLemma_2 singPeerRole reflB reflA of + ReflNobodyHasAgency -> case reflB of {} + + go (Done reflA _) (Await reflB _) = + case terminationLemma_2 singPeerRole reflB reflA of + ReflNobodyHasAgency -> case reflB of {} + + go (Yield reflA _ _) (Done reflB _) = + case terminationLemma_1 singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} + + go (Await reflA _) (Done reflB _) = + case terminationLemma_1 singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} + + +-- | The terminal states for the protocol. Used in 'connect' and +-- 'connectPipelined' to return the states in which the peers terminated. +-- +data TerminalStates ps where + TerminalStates + :: forall ps (st :: ps). + (StateAgency st ~ NobodyAgency) + => StateToken st + -- ^ state termination evidence for the first peer + -> StateToken st + -- ^ state termination evidence for the second peer + -> TerminalStates ps + +-- +-- Remove Pipelining +-- + + +-- | A size indexed queue. This is useful for proofs, including +-- 'connectPipelined' but also as so-called @direct@ functions for running a +-- client and server wrapper directly against each other. +-- +data Queue (n :: N) a where + EmptyQ :: Queue Z a + ConsQ :: a -> Queue n a -> Queue (S n) a + +-- | At an element to the end of a 'Queue'. This is not intended to be +-- efficient. It is only for proofs and tests. +-- +enqueue :: a -> Queue n a -> Queue (S n) a +enqueue a EmptyQ = ConsQ a EmptyQ +enqueue a (ConsQ b q) = ConsQ b (enqueue a q) + + +-- | Proof that we have a total conversion from pipelined peers to regular +-- peers. This is a sanity property that shows that pipelining did not give +-- us extra expressiveness or to break the protocol state machine. +-- +forgetPipelined + :: forall ps (pr :: PeerRole) (st :: ps) m a. + Functor m + => [Bool] + -- ^ interleaving choices for pipelining allowed by `Collect` primitive. False + -- values or `[]` give no pipelining. + -> PeerPipelined ps pr st m a + -> Peer ps pr NonPipelined st m a +forgetPipelined cs0 (PeerPipelined peer) = goSender EmptyQ cs0 peer + where + goSender :: forall st' n c. + Queue n c + -> [Bool] + -> Peer ps pr ('Pipelined n c) st' m a + -> Peer ps pr 'NonPipelined st' m a + + goSender EmptyQ _cs (Done refl k) = Done refl k + goSender q cs (Effect k) = Effect (goSender q cs <$> k) + goSender q cs (Yield refl m k) = Yield refl m (goSender q cs k) + goSender q cs (Await refl k) = Await refl (goSender q cs <$> k) + goSender q cs (YieldPipelined refl m r k) = Yield refl m (goReceiver q cs k r) + goSender q (True:cs') (Collect (Just k) _) = goSender q cs' k + goSender (ConsQ x q) (_:cs) (Collect _ k) = goSender q cs (k x) + goSender (ConsQ x q) cs@[] (Collect _ k) = goSender q cs (k x) + + goReceiver :: forall stCurrent stNext n c. + Queue n c + -> [Bool] + -> Peer ps pr ('Pipelined (S n) c) stNext m a + -> Receiver ps pr stCurrent stNext m c + -> Peer ps pr 'NonPipelined stCurrent m a + + goReceiver q cs s (ReceiverDone x) = goSender (enqueue x q) cs s + goReceiver q cs s (ReceiverEffect k) = Effect (goReceiver q cs s <$> k) + goReceiver q cs s (ReceiverAwait refl k) = Await refl (goReceiver q cs s . k) + + +-- | Promote a peer to a pipelined one. +-- +-- This is a right inverse of `forgetPipelined`, e.g. +-- +-- >>> forgetPipelined . promoteToPipelined = id +-- +promoteToPipelined + :: forall ps (pr :: PeerRole) st m a. + Functor m + => Peer ps pr NonPipelined st m a + -- ^ a peer + -> PeerPipelined ps pr st m a + -- ^ a pipelined peer +promoteToPipelined p = PeerPipelined (go p) + where + go :: forall st' c. + Peer ps pr NonPipelined st' m a + -> Peer ps pr (Pipelined Z c) st' m a + go (Effect k) = Effect $ go <$> k + go (Yield refl msg k) = Yield refl msg (go k) + go (Await refl k) = Await refl (go . k) + go (Done refl k) = Done refl k + + +-- | Analogous to 'connect' but also for pipelined peers. +-- +-- Since pipelining allows multiple possible interleavings, we provide a +-- @[Bool]@ parameter to control the choices. Each @True@ will trigger picking +-- the first choice in the @SenderCollect@ construct (if possible), leading +-- to more results outstanding. This can also be interpreted as a greater +-- pipeline depth, or more messages in-flight. +-- +-- This can be exercised using a QuickCheck style generator. +-- +connectPipelined + :: forall ps (pr :: PeerRole) + (st :: ps) m a b. + (Monad m, SingI pr) + => [Bool] + -- ^ an interleaving + -> PeerPipelined ps pr st m a + -- ^ a pipelined peer + -> Peer ps (FlipAgency pr) NonPipelined st m b + -- ^ a non-pipelined peer with fliped agency + -> m (a, b, TerminalStates ps) + -- ^ peers results and an evidence of their termination +connectPipelined csA a b = + connect (forgetPipelined csA a) b + +-- | A reference specification for interleaving of requests and responses +-- with pipelining, where the environment can choose whether a response is +-- available yet. +-- +-- This also supports bounded choice where the maximum number of outstanding +-- in-flight responses is limited. +-- +pipelineInterleaving :: Int -- ^ Bound on outstanding responses + -> [Bool] -- ^ Pipelining choices + -> [req] -> [resp] -> [Either req resp] +pipelineInterleaving omax cs0 reqs0 resps0 = + go 0 cs0 (zip [0 :: Int ..] reqs0) + (zip [0 :: Int ..] resps0) + where + go o (c:cs) reqs@((reqNo, req) :reqs') + resps@((respNo,resp):resps') + | respNo == reqNo = Left req : go (o+1) (c:cs) reqs' resps + | c && o < omax = Left req : go (o+1) cs reqs' resps + | otherwise = Right resp : go (o-1) cs reqs resps' + + go o [] reqs@((reqNo, req) :reqs') + resps@((respNo,resp):resps') + | respNo == reqNo = Left req : go (o+1) [] reqs' resps + | otherwise = Right resp : go (o-1) [] reqs resps' + + go _ _ [] resps = map (Right . snd) resps + go _ _ (_:_) [] = error "pipelineInterleaving: not enough responses" diff --git a/stateful-cborg/Network/TypedProtocol/Stateful/Codec/CBOR.hs b/stateful-cborg/Network/TypedProtocol/Stateful/Codec/CBOR.hs new file mode 100644 --- /dev/null +++ b/stateful-cborg/Network/TypedProtocol/Stateful/Codec/CBOR.hs @@ -0,0 +1,126 @@ +module Network.TypedProtocol.Stateful.Codec.CBOR + ( module Network.TypedProtocol.Stateful.Codec + , DeserialiseFailure + , mkCodecCborLazyBS + , mkCodecCborStrictBS + ) where + +import Control.Monad.Class.MonadST (MonadST (..)) + +import Codec.CBOR.Decoding qualified as CBOR (Decoder) +import Codec.CBOR.Encoding qualified as CBOR (Encoding) +import Codec.CBOR.Read qualified as CBOR +import Codec.CBOR.Write qualified as CBOR +import Data.ByteString qualified as BS +import Data.ByteString.Builder qualified as BS +import Data.ByteString.Builder.Extra qualified as BS +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Internal qualified as LBS (smallChunkSize) + +import Network.TypedProtocol.Codec.CBOR (DeserialiseFailure, + convertCborDecoderBS, convertCborDecoderLBS) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Codec + + +-- | Construct a 'Codec' for a CBOR based serialisation format, using strict +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- +-- It takes encode and decode functions for the protocol messages that use the +-- CBOR library encoder and decoder. +-- +-- Note that this is /less/ efficient than the 'mkCodecCborLazyBS' variant +-- because it has to copy and concatenate the result of the encoder (which +-- natively produces chunks). +-- +mkCodecCborStrictBS + :: forall ps f m. MonadST m + + => (forall (st :: ps) (st' :: ps). + StateTokenI st + =>ActiveState st + => f st -> Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> f st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps DeserialiseFailure f m BS.ByteString +mkCodecCborStrictBS cborMsgEncode cborMsgDecode = + Codec { + encode = \f msg -> convertCborEncoder (cborMsgEncode f) msg, + decode = \stok f -> convertCborDecoder (cborMsgDecode stok f) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString + convertCborEncoder cborEncode = + CBOR.toStrictByteString + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep BS.ByteString DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderBS cborDecode stToIO + +-- | Construct a 'Codec' for a CBOR based serialisation format, using lazy +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- +-- It takes encode and decode functions for the protocol messages that use the +-- CBOR library encoder and decoder. +-- +mkCodecCborLazyBS + :: forall ps f m. MonadST m + + => (forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => f st + -> Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> f st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps CBOR.DeserialiseFailure f m LBS.ByteString +mkCodecCborLazyBS cborMsgEncode cborMsgDecode = + Codec { + encode = \f msg -> convertCborEncoder (cborMsgEncode f) msg, + decode = \stok f -> convertCborDecoder (cborMsgDecode stok f) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> LBS.ByteString + convertCborEncoder cborEncode = + toLazyByteString + . CBOR.toBuilder + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderLBS cborDecode stToIO + +{-# NOINLINE toLazyByteString #-} +toLazyByteString :: BS.Builder -> LBS.ByteString +toLazyByteString = BS.toLazyByteStringWith strategy LBS.empty + where + -- Buffer strategy and sizes better tuned to our network protocol situation. + -- + -- The LBS.smallChunkSize is 4k - heap object overheads, so that + -- it does fit in a 4k overall. + -- + strategy = BS.untrimmedStrategy 800 LBS.smallChunkSize + diff --git a/stateful/Network/TypedProtocol/Stateful/Codec.hs b/stateful/Network/TypedProtocol/Stateful/Codec.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Codec.hs @@ -0,0 +1,295 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +-- @UndecidableInstances@ extension is required for defining @Show@ instance of +-- @'AnyMessage'@ and @'AnyMessage'@. +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-dodgy-imports #-} + +-- | Stateful codec. This module is intended to be imported qualified. +-- +module Network.TypedProtocol.Stateful.Codec + ( -- * Defining and using Codecs + Codec (..) + , hoistCodec + , isoCodec + , mapFailureCodec + , liftCodec + -- ** Incremental decoding + , DecodeStep (..) + , runDecoder + , runDecoderPure + -- ** Related types + -- *** SomeMessage + , SomeMessage (..) + -- *** StateToken + , StateToken + , StateTokenI (..) + -- *** ActiveState + , ActiveState + -- *** PeerRole + , PeerRole (..) + -- * CodecFailure + , CodecFailure (..) + -- * 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, + mapFailureDecodeStep, runDecoder, runDecoderPure) +import Network.TypedProtocol.Codec qualified as TP hiding (AnyMessageAndAgency) +import Network.TypedProtocol.Core + + +-- | A stateful codec. +-- +data Codec ps failure (f :: ps -> Type) m bytes = Codec { + encode :: forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => f st + -- local state, which contain extra context for the encoding + -- process. + -- + -- TODO: input-output-hk/typed-protocols#57 + -> Message ps st st' + -- message to be encoded + -> bytes, + + decode :: forall (st :: ps). + ActiveState st + => StateToken st + -> f st + -- local state, which can contain extra context from the + -- previous message. + -- + -- TODO: input-output-hk/typed-protocols#57 + -> m (DecodeStep bytes failure m (SomeMessage st)) + } + +liftCodec :: TP.Codec ps failure m bytes -> Codec ps failure f m bytes +liftCodec codec = Codec { encode = \_ msg -> TP.encode codec msg + , decode = \stok _ -> TP.decode codec stok + } + +hoistCodec + :: ( Functor n ) + => (forall x . m x -> n x) + -> Codec ps failure f m bytes + -> Codec ps failure f n bytes +hoistCodec nat codec = codec + { decode = \stok f -> fmap (hoistDecodeStep nat) . nat $ decode codec stok f + } + +isoCodec :: Functor m + => (bytes -> bytes') + -> (bytes' -> bytes) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes' +isoCodec g finv Codec {encode, decode} = Codec { + encode = \f msg -> g $ encode f msg, + decode = \stok f -> isoDecodeStep g finv <$> decode stok f + } + +mapFailureCodec + :: Functor m + => (failure -> failure') + -> Codec ps failure f m bytes + -> Codec ps failure' f m bytes +mapFailureCodec g Codec {encode, decode} = Codec { + encode = encode, + decode = \stok f -> mapFailureDecodeStep g <$> decode stok f + } + + +-- +-- Codec properties +-- + +-- | Any message for a protocol, with a 'StateTokenI' constraint which gives access +-- to protocol state. +-- +-- Used where we don't know statically what the state type is, but need the +-- agency and message to match each other. +-- +data AnyMessage ps (f :: ps -> Type) where + AnyMessage :: forall ps f (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => f st + -- ^ local state + -> Message ps (st :: ps) (st' :: ps) + -- ^ protocol messsage + -> AnyMessage ps f + + +-- | `showAnyMessage` is can be used to provide `Show` instance for +-- `AnyMessage` if showing `Message` is independent of the state or one accepts +-- showing only partial information included in message constructors or accepts +-- message constructors to carry `Show` instances for its arguments. Note that +-- the proper solution is to define a custom `Show (AnyMessage ps f)` instance +-- for a protocol `ps`, which give access to the state functor `f` in scope of +-- `show`. +-- +showAnyMessage :: forall ps f. + ( forall st st'. Show (Message ps st st') + , forall st. Show (f st) + ) + => AnyMessage ps f + -> String +showAnyMessage (AnyMessage st msg) = + concat [ "AnyMessage " + , show st + , " " + , show msg + ] + + +-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the +-- singleton for the state and the message. +-- +pattern AnyMessageAndAgency :: forall ps f. () + => forall (st :: ps) (st' :: ps). + (StateTokenI st, ActiveState st) + => StateToken st + -> f st + -> Message ps st st' + -> AnyMessage ps f +pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, stateToken)) + where + AnyMessageAndAgency _ msg = AnyMessage msg +{-# COMPLETE AnyMessageAndAgency #-} + +-- | Internal view pattern for 'AnyMessageAndAgency' +-- +getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st) +getAgency msg = (msg, stateToken) + + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + ) + => Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' == a + Left _ -> return False + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_codec + :: forall ps failure f m bytes. + (Monad m, Eq (AnyMessage ps f)) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codec runM codec msg = + runM (prop_codecM codec msg) + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure f m bytes. + (Monad m, Eq (AnyMessage ps f)) + => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codec_splitsM splits + Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do + and <$> sequence + [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ AnyMessage f msg' == a + Left _ -> return False + + | let bytes = encode f msg + , bytes' <- splits bytes ] + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure f m bytes. + (Monad m, Eq (AnyMessage ps f)) + => (bytes -> [[bytes]]) + -> (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codec_splits splits runM codec msg = + runM $ prop_codec_splitsM splits codec msg + + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + ) + => Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codecs_compatM codecA codecB + a@(AnyMessage f (msg :: Message ps st st')) = + getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a + Left _ -> return $ All False + <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a + Left _ -> return $ All False + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure f m bytes. + ( Monad m + , Eq (AnyMessage ps f) + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codecs_compat run codecA codecB msg = + run $ prop_codecs_compatM codecA codecB msg diff --git a/stateful/Network/TypedProtocol/Stateful/Driver.hs b/stateful/Network/TypedProtocol/Stateful/Driver.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Driver.hs @@ -0,0 +1,112 @@ +-- | Actions for running 'Peer's with a 'Driver'. This module should be +-- imported qualified. +-- +module Network.TypedProtocol.Stateful.Driver + ( -- * DriverIngerface + Driver (..) + -- * Running a peer + , runPeerWithDriver + -- * Re-exports + , SomeMessage (..) + , DecodeStep (..) + ) where + +import Control.Monad.Class.MonadSTM + +import Data.Kind (Type) + +import Network.TypedProtocol.Codec (DecodeStep (..), SomeMessage (..)) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer + +data Driver ps (pr :: PeerRole) bytes failure dstate f m = + Driver { + -- | Send a message. + -- + sendMessage :: forall (st :: ps) (st' :: ps). + StateTokenI st + => StateTokenI st' + => ActiveState st + => ReflRelativeAgency (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) + -> f st + -- local state associated to protocol state `st`; + -- local state should not be sent to the remote side. + -- However it provide extra context for the encoder. + -- + -- TODO: input-output-hk/typed-protocols#57 + -> Message ps st st' + -- message to send + -- + -- TODO: input-output-hk/typed-protocols#57 + -> m () + + , -- | Receive a message, a blocking action which reads from the network + -- and runs the incremental decoder until a full message is decoded. + -- + recvMessage :: forall (st :: ps). + StateTokenI st + => ActiveState st + => ReflRelativeAgency (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) + -> f st + -- local state which provides extra context for the + -- decoder. + -- + -- TODO: input-output-hk/typed-protocols#57 + -> dstate + -- decoder state, e.g. bytes left from decoding of + -- a previous message. + -- + -- TODO: input-output-hk/typed-protocols#57 + -> m (SomeMessage st, dstate) + + , -- | Initial decoder state. + -- + initialDState :: dstate + } + + +-- +-- Running peers +-- + +-- | Run a peer with the given driver. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +-- NOTE: this function threads local state (i.e. `f`) through evolution of +-- a protocol (i.e. `Peer`). +-- +runPeerWithDriver + :: forall ps (st :: ps) pr bytes failure dstate (f :: ps -> Type) m a. + MonadSTM m + => Driver ps pr bytes failure dstate f m + -> f st + -> Peer ps pr st f m a + -> m (a, dstate) +runPeerWithDriver Driver{ sendMessage + , recvMessage + , initialDState + } = + go initialDState + where + go :: forall st'. + dstate + -> f st' + -> Peer ps pr st' f m a + -> m (a, dstate) + go !dstate !f (Effect k) = k >>= go dstate f + + go !dstate _ (Done _ x) = return (x, dstate) + + go !dstate _ (Yield refl !f !f' msg k) = do + sendMessage refl f msg + go dstate f' k + + go !dstate !f (Await refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl f dstate + case k f msg of + (k', f') -> go dstate' f' k' diff --git a/stateful/Network/TypedProtocol/Stateful/Peer.hs b/stateful/Network/TypedProtocol/Stateful/Peer.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Peer.hs @@ -0,0 +1,195 @@ +-- TODO: the 'Functor' instance of 'Peer' is undecidable +{-# LANGUAGE UndecidableInstances #-} + +-- | Protocol stateful EDSL. +-- +-- __Note__: 'Network.TypedProtocol.Peer.Client.Client' and +-- 'Network.TypedProtocol.Peer.Server.Server' patterns are easier to use. +-- +module Network.TypedProtocol.Stateful.Peer (Peer (..)) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core as Core + + +-- | A description of a peer that engages in a protocol. +-- +-- The protocol describes what messages peers /may/ send or /must/ accept. +-- A particular peer implementation decides what to actually do within the +-- constraints of the protocol. +-- +-- Peers engage in a protocol in either the client or server role. Of course +-- the client role can only interact with the serve role for the same protocol +-- and vice versa. +-- +-- 'Peer' has several type arguments: +-- +-- * the protocol itself; +-- * the client\/server role; +-- * the current protocol state; +-- * the local state type; +-- * the monad in which the peer operates; and +-- * the type of any final result once the peer terminates. +-- +-- For example: +-- +-- > reqRespClientExample :: Peer (ReqResp FileAPI) AsClient StIdle State m () +-- > reqRespServerExample :: Peer (ReqResp FileAPI) AsServer StIdle State m Int +-- +-- The actions that a peer can take are: +-- +-- * perform a local monadic effect, +-- * terminate with a result (but only in a terminal protocol state), +-- * send a message (but only in a protocol state in which we have agency), +-- * wait to receive a message (but only in a protocol state in which the +-- other peer has agency). +-- +-- The 'Yield', 'Await' and 'Done' constructors require to provide an evidence +-- that the appropriate peer has agency. This information is supplied using +-- one of the constructors of 'ReflRelativeAgency'. +-- +-- While this evidence must be provided, the types guarantee that it is not +-- possible to supply incorrect evidence. The +-- 'Network.TypedProtocol.Peer.Client' or 'Network.TypedProtocol.Peer.Server' +-- pattern synonyms provide this evidence automatically. +-- +-- __NOTE__: +-- one should not allocate resources within a `Peer` since there's no way to +-- safely clean-up resources in case of an asynchronous exception. The proper +-- way to allocate resources is to call +-- `Network.TypedProtocol.Stateful.Driver.runPeerWithDriver` within +-- a `Control.Exception.bracket`. +-- +-- __TODO__: +-- We are not exposing pipelined version, since it is not possible to write +-- a driver & proofs in a type safe which take into account the state when the +-- peer type only tracks depth of pipelining rather than pipelined transitions. +-- +type Peer :: forall ps + -> PeerRole + -> ps + -> (ps -> Type) + -- ^ protocol state + -> (Type -> Type) + -- ^ monad's kind + -> Type + -> Type +data Peer ps pr st f m a where + + -- | Perform a local monadic effect and then continue. + -- + -- Example: + -- + -- > Effect $ do + -- > ... -- actions in the monad + -- > return $ ... -- another Peer value + -- + Effect + :: forall ps pr st f m a. + m (Peer ps pr st f m a) + -- ^ monadic continuation + -> Peer ps pr st f m a + + -- | Send a message to the other peer and then continue. The constructor + -- requires evidence that we have agency for this protocol state and thus are + -- allowed to send messages. It takes local state associated to the source + -- and target protocol state of the message that is sent. This state is only + -- maintained locally, never shared remotely. It also takes the message and + -- the continuation. It also requires evidence that we have agency for this + -- protocol state and thus are allowed to send messages. + -- + -- Example: + -- + -- > Yield ReflClientAgency (StateBusy (ReadFile /etc/os-release)) + -- > StateIdle + -- > $ MsgResp "..." + -- + Yield + :: forall ps pr (st :: ps) (st' :: ps) f m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => WeHaveAgencyProof pr st + -- ^ agency singleton + -> f st + -- ^ associated local state to the source protocol state 'st' + -> f st' + -- ^ associated local state to the target protocol state `st'` + -> Message ps st st' + -- ^ protocol message + -> Peer ps pr st' f m a + -- ^ continuation + -> Peer ps pr st f m a + + -- | Waits to receive a message from the other peer and then continues. + -- This takes the continuation that is supplied with the received message. It + -- also requires evidence that the other peer has agency for this protocol + -- state and thus we are expected to wait to receive messages. + -- + -- Note that the continuation that gets supplied with the message must be + -- prepared to deal with /any/ message that is allowed in /this/ protocol + -- state. This is why the continuation /must/ be polymorphic in the target + -- state of the message (the third type argument of 'Message'). + -- + -- Example: + -- + -- > Await ReflClientAgency $ \f msg -> + -- > case (f, msg) of + -- > (StateBusy (ReadFile path), MsgResp resp) -> + -- > ( _continuation + -- > , StateIdle + -- > ) + -- + -- + Await + :: forall ps pr (st :: ps) f m a. + ( StateTokenI st + , ActiveState st + ) + => TheyHaveAgencyProof pr st + -- ^ agency singleton + -> (forall (st' :: ps). + f st + -- associated local state to the source protocol state 'st' + -- + -- TODO: input-output-hk/typed-protocols#57 + -> Message ps st st' + -> ( Peer ps pr st' f m a + , f st' + ) + -- continuation and associated local state to the target protocol + -- state `st'` + -- + -- NOTE: the API is limited to pure transition of local state e.g. + -- `f st -> Message ps st st' -> f st'`, + -- see https://github.com/input-output-hk/typed-protocols/discussions/63 + -- + -- TODO: input-output-hk/typed-protocols#57 + ) + -- ^ continuation + -> Peer ps pr st f m a + + -- | Terminate with a result. A state token must be provided from the + -- 'NobodyHasAgency' states, to show that this is a state in which we can + -- terminate. + -- + -- Example: + -- + -- > Yield ReflClientAgency + -- > MsgDone + -- > (Done ReflNobodyAgency TokDone result) + -- + Done + :: forall ps pr (st :: ps) f m a. + ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => NobodyHasAgencyProof pr st + -- ^ (no) agency proof + -> a + -- ^ returned value + -> Peer ps pr st f m a + +deriving instance Functor m => Functor (Peer ps pr st f m) diff --git a/stateful/Network/TypedProtocol/Stateful/Peer/Client.hs b/stateful/Network/TypedProtocol/Stateful/Peer/Client.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Peer/Client.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsClient'@. The advantage of +-- these patterns is that they automatically provide the 'RelativeAgencyEq' +-- singleton. +-- +module Network.TypedProtocol.Stateful.Peer.Client + ( -- * Client type alias and its pattern synonyms + Client + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer (Peer) +import Network.TypedProtocol.Stateful.Peer qualified as TP + + +type Client :: forall ps + -> ps + -> (ps -> Type) + -> (Type -> Type) + -> Type + -> Type +type Client ps st f m a = Peer ps AsClient st f m a + + +-- | Client role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps st f m a. + m (Client ps st f m a) + -- ^ monadic continuation + -> Client ps st f m a +pattern Effect mclient = TP.Effect mclient + + +-- | Client role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps st f m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + ) + => f st + -> f st' + -> Message ps st st' + -- ^ protocol message + -> Client ps st' f m a + -- ^ continuation + -> Client ps st f m a +pattern Yield f f' msg k = TP.Yield ReflClientAgency f f' msg k + + +-- | Client role pattern for 'TP.Await' +-- +pattern Await :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ ServerAgency + ) + => (forall st'. + f st + -> Message ps st st' + -> ( Client ps st' f m a + , f st' + ) + ) + -- ^ continuation + -> Client ps st f m a +pattern Await k = TP.Await ReflServerAgency k + + +-- | Client role pattern for 'TP.Done' +-- +pattern Done :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => a + -- ^ protocol return value + -> Client ps st f m a +pattern Done a = TP.Done ReflNobodyAgency a + + +{-# COMPLETE Effect, Yield, Await, Done #-} diff --git a/stateful/Network/TypedProtocol/Stateful/Peer/Server.hs b/stateful/Network/TypedProtocol/Stateful/Peer/Server.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Peer/Server.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsServer'@. The advantage of +-- these patterns is that they automatically provide the 'RelativeAgencyEq' +-- singleton. +-- +module Network.TypedProtocol.Stateful.Peer.Server + ( -- * Server type alias and its pattern synonyms + Server + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer (Peer) +import Network.TypedProtocol.Stateful.Peer qualified as TP + + +type Server :: forall ps + -> ps + -> (ps -> Type) + -> (Type -> Type) + -> Type + -> Type +type Server ps st f m a = Peer ps AsServer st f m a + + +-- | Server role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps st f m a. + m (Server ps st f m a) + -- ^ monadic continuation + -> Server ps st f m a +pattern Effect mclient = TP.Effect mclient + + +-- | Server role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps st f m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + ) + => f st + -> f st' + -> Message ps st st' + -- ^ protocol message + -> Server ps st' f m a + -- ^ continuation + -> Server ps st f m a +pattern Yield f f' msg k = TP.Yield ReflServerAgency f f' msg k + + +-- | Server role pattern for 'TP.Await' +-- +pattern Await :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ ClientAgency + ) + => (forall st'. + f st + -> Message ps st st' + -> ( Server ps st' f m a + , f st' + ) + ) + -- ^ continuation + -> Server ps st f m a +pattern Await k = TP.Await ReflClientAgency k + + +-- | Server role pattern for 'TP.Done' +-- +pattern Done :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => a + -- ^ protocol return value + -> Server ps st f m a +pattern Done a = TP.Done ReflNobodyAgency a + +{-# COMPLETE Effect, Yield, Await, Done #-} diff --git a/stateful/Network/TypedProtocol/Stateful/Proofs.hs b/stateful/Network/TypedProtocol/Stateful/Proofs.hs new file mode 100644 --- /dev/null +++ b/stateful/Network/TypedProtocol/Stateful/Proofs.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE TypeFamilies #-} + +-- This is already implied by the -Wall in the .cabal file, but lets just be +-- completely explicit about it too, since we rely on the completeness +-- checking in the cases below for the completeness of our proofs. +{-# OPTIONS_GHC -Wincomplete-patterns #-} + +-- | Proofs about the typed protocol framework. +-- +-- It also provides helpful testing utilities. +-- +module Network.TypedProtocol.Stateful.Proofs + ( connect + , TerminalStates (..) + , removeState + ) where + +import Control.Monad.Class.MonadSTM + +import Data.Kind (Type) +import Data.Singletons + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer +import Network.TypedProtocol.Proofs (TerminalStates (..)) +import Network.TypedProtocol.Proofs qualified as TP +import Network.TypedProtocol.Stateful.Peer qualified as ST + + + +-- | Remove state for non-pipelined peers. +-- +-- TODO: There's a difficulty to write `removeState` for pipelined peers which +-- is type safe. The `Peer` doesn't track all pipelined transitions, just the +-- depth of pipelining, so we cannot push `f st` to a queue which type is +-- linked to `Peer`. For a similar reason there's no way to write +-- `forgetPipelined` function. +-- +-- However, this is possible if `Peer` tracks all transitions. +-- +removeState + :: Functor m + => f st + -> ST.Peer ps pr st f m a + -> Peer ps pr NonPipelined st m a +removeState = go + where + go + :: forall ps (pr :: PeerRole) + (st :: ps) + (f :: ps -> Type) + m a. + Functor m + => f st + -> ST.Peer ps pr st f m a + -> Peer ps pr NonPipelined st m a + go f (ST.Effect k) = Effect (go f <$> k) + go _ (ST.Yield refl _f f' msg k) = Yield refl msg (go f' k) + go f (ST.Await refl k) = Await refl $ \msg -> + case k f msg of + (k', f') -> go f' k' + go _ (ST.Done refl a) = Done refl a + + +connect + :: forall ps (pr :: PeerRole) + (st :: ps) + (f :: ps -> Type) + m a b. + (MonadSTM m, SingI pr) + => f st + -> ST.Peer ps pr st f m a + -> ST.Peer ps (FlipAgency pr) st f m b + -> m (a, b, TerminalStates ps) +connect f a b = TP.connect (removeState f a) (removeState f b) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,17 @@ +module Main (main) where + +import Test.Tasty + +import Network.TypedProtocol.PingPong.Tests qualified as PingPong +import Network.TypedProtocol.ReqResp.Tests qualified as ReqResp + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = + testGroup "typed-protocols" + [ PingPong.tests + , ReqResp.tests + ] + diff --git a/test/Network/TypedProtocol/PingPong/Tests.hs b/test/Network/TypedProtocol/PingPong/Tests.hs new file mode 100644 --- /dev/null +++ b/test/Network/TypedProtocol/PingPong/Tests.hs @@ -0,0 +1,469 @@ +{-# LANGUAGE CPP #-} +-- orphaned arbitrary instances +{-# OPTIONS_GHC -Wno-orphans #-} + +module Network.TypedProtocol.PingPong.Tests + ( tests + , splits2 + , splits3 + , splits2BS + , splits3BS + ) where + + +import Network.TypedProtocol.Channel +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Driver.Simple +import Network.TypedProtocol.Proofs + +import Network.TypedProtocol.PingPong.Client +import Network.TypedProtocol.PingPong.Codec +import Network.TypedProtocol.PingPong.Codec.CBOR qualified as CBOR +import Network.TypedProtocol.PingPong.Examples +import Network.TypedProtocol.PingPong.Server +import Network.TypedProtocol.PingPong.Type + +import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadSTM +import Control.Monad.Class.MonadThrow +import Control.Monad.IOSim (runSimOrThrow) +import Control.Monad.ST (runST) +import Control.Tracer (nullTracer) + +import Data.Functor.Identity (Identity (..)) +import Data.List (inits, tails) + +import Data.ByteString.Lazy qualified as LBS +#if !defined(mingw32_HOST_OS) +import Network.Socket qualified as Socket +import System.Directory (removeFile) +import System.IO +import System.Posix.Files qualified as Posix +#endif + +import Test.QuickCheck +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) + + +-- +-- The list of all properties +-- + +tests :: TestTree +tests = testGroup "Network.TypedProtocol.PingPong" + [ testProperty "direct" prop_direct + , testProperty "directPipelined 1" prop_directPipelined1 + , testProperty "directPipelined 2" prop_directPipelined2 + , testProperty "connect" prop_connect + , testProperty "connect_pipelined 1" prop_connect_pipelined1 + , testProperty "connect_pipelined 2" prop_connect_pipelined2 + , testProperty "connect_pipelined 3" prop_connect_pipelined3 + , testProperty "connect_pipelined 4" prop_connect_pipelined4 + , testProperty "connect_pipelined 5" prop_connect_pipelined5 + , testProperty "channel ST" prop_channel_ST + , testProperty "channel IO" prop_channel_IO +#if !defined(mingw32_HOST_OS) + , testProperty "namedPipePipelined" prop_namedPipePipelined_IO + , testProperty "socketPipelined" prop_socketPipelined_IO +#endif + , testGroup "Codec" + [ testProperty "codec" prop_codec_PingPong + , testProperty "codec 2-splits" prop_codec_splits2_PingPong + , testProperty "codec 3-splits" prop_codec_splits3_PingPong + , testGroup "CBOR" + [ testProperty "codec" prop_codec_cbor_PingPong + , testProperty "codec 2-splits" prop_codec_cbor_splits2_PingPong + , testProperty "codec 3-splits" $ withMaxSuccess 30 prop_codec_cbor_splits3_PingPong + ] + ] + ] + + +-- +-- Properties going directly, not via Peer. +-- + +-- | The 'PingPongClient m' and 'PingPongServer m' types are complementary. +-- The former can be used to feed the latter directly, in the same thread. +-- That's demonstrated here by constructing 'direct'. +-- +direct :: Monad m + => PingPongClient m a + -> PingPongServer m b + -> m (a, b) + +direct (SendMsgDone clientResult) PingPongServer{recvMsgDone} = + pure (clientResult, recvMsgDone) + +direct (SendMsgPing kPong) PingPongServer{recvMsgPing} = do + server' <- recvMsgPing + client' <- kPong + direct client' server' + + +directPipelined :: Monad m + => PingPongClientPipelined c m a + -> PingPongServer m b + -> m (a, b) +directPipelined (PingPongClientPipelined client0) server0 = + go EmptyQ client0 server0 + where + go :: Monad m + => Queue n c + -> PingPongClientIdle n c m a + -> PingPongServer m b + -> m (a, b) + go EmptyQ (SendMsgDonePipelined clientResult) PingPongServer{recvMsgDone} = + pure (clientResult, recvMsgDone) + + go q (SendMsgPingPipelined kPong client') PingPongServer{recvMsgPing} = do + server' <- recvMsgPing + x <- kPong + go (enqueue x q) client' server' + + go (ConsQ x q) (CollectPipelined _ k) server = do + go q (k x) server + + +-- | Run a simple ping\/pong client and server, without going via the 'Peer' +-- representation at all. +-- +prop_direct :: NonNegative Int -> Bool +prop_direct (NonNegative n) = + runIdentity + (direct (pingPongClientCount n) + pingPongServerCount) + == + ((), n) + + +-- | Run a ping\/pong server and pipelined client, without going via the 'Peer' +-- representation. +-- +-- This uses a client that forces maximum pipeling. It shows that irrespective +-- of the envronment's choices, the interleaving we get is all requests +-- followed by all responses +-- +prop_directPipelined1 :: NonNegative Int -> Bool +prop_directPipelined1 (NonNegative n) = + runIdentity + (directPipelined + (pingPongClientPipelinedMax n) + pingPongServerCount) + == + (reqResps, n) + where + reqResps = map Left [0..n-1] ++ map Right [0..n-1] + + +-- | Run a ping\/pong server and pipelined client, without going via the 'Peer' +-- representation. +-- +-- This uses a client that collects eagerly. It shows that when the environment +-- chooses minimum pipelining, then the interleaving we get is the in-order +-- non-pipelined interleaving of each request followed by its response. +-- +prop_directPipelined2 :: NonNegative Int -> Bool +prop_directPipelined2 (NonNegative n) = + runIdentity + (directPipelined + (pingPongClientPipelinedMin n) + pingPongServerCount) + == + (reqResps, n) + where + reqResps = concat [ [Left n', Right n'] | n' <- [0..n-1] ] + + +-- +-- Properties using connect, without pipelining. +-- + +-- | Run a simple ping\/pong client and server, going via the 'Peer' +-- representation, but without going via a channel. +-- +prop_connect :: NonNegative Int -> Bool +prop_connect (NonNegative n) = + case runIdentity + (connect + (pingPongClientPeer (pingPongClientCount n)) + (pingPongServerPeer pingPongServerCount)) + + of ((), n', TerminalStates SingDone SingDone) -> n == n' + + +-- +-- Properties using connect, with pipelining. +-- + +-- | Run a pipelined ping\/pong client with a normal server. The client +-- should return the interleaving of messages it sent and received. This +-- will be used to exercise various interleavings in properties below. +-- +connect_pipelined :: PingPongClientPipelined Int Identity [Either Int Int] + -> [Bool] + -> (Int, [Either Int Int]) +connect_pipelined client cs = + case runIdentity + (connectPipelined cs + (pingPongClientPeerPipelined client) + (pingPongServerPeer pingPongServerCount)) + of (reqResps, n, TerminalStates SingDone SingDone) -> + (n, reqResps) + + +-- | Using a client that forces maximum pipeling, show that irrespective of +-- the envronment's choices, the interleaving we get is all requests followed +-- by all responses. +-- +prop_connect_pipelined1 :: [Bool] -> NonNegative Int -> Bool +prop_connect_pipelined1 choices (NonNegative n) = + connect_pipelined (pingPongClientPipelinedMax n) choices + == + (n, reqResps) + where + reqResps = map Left [0..n-1] ++ map Right [0..n-1] + + +-- | Using a client that collects eagerly, show that when the environment +-- chooses maximum pipelining, then the interleaving we get is all requests +-- followed by all responses. +-- +prop_connect_pipelined2 :: NonNegative Int -> Bool +prop_connect_pipelined2 (NonNegative n) = + connect_pipelined (pingPongClientPipelinedMin n) choices + == + (n, reqResps) + where + choices = repeat True + reqResps = map Left [0..n-1] ++ map Right [0..n-1] + + +-- | Using a client that collects eagerly, show that when the environment +-- chooses minimum pipelining, then the interleaving we get is the in-order +-- non-pipelined interleaving of each request followed by its response. +-- +prop_connect_pipelined3 :: NonNegative Int -> Bool +prop_connect_pipelined3 (NonNegative n) = + connect_pipelined (pingPongClientPipelinedMin n) choices + == + (n, reqResps) + where + choices = repeat False + reqResps = concat [ [Left n', Right n'] | n' <- [0..n-1] ] + + +-- | Using a client that collects eagerly, but otherwise is always willing +-- to send new messages, show that when the environment chooses arbitrary +-- pipelining, then we get complex interleavings given by the reference +-- specification 'pipelineInterleaving'. +-- +prop_connect_pipelined4 :: [Bool] -> NonNegative Int -> Bool +prop_connect_pipelined4 choices (NonNegative n) = + connect_pipelined (pingPongClientPipelinedMin n) choices + == + (n, reqResps) + where + reqResps = pipelineInterleaving maxBound choices [0..n-1] [0..n-1] + + +-- | Using a client that collects eagerly, and is willing to send new messages +-- up to a fixed limit of outstanding messages, show that when the environment +-- chooses arbitrary pipelining, then we get complex interleavings given by +-- the reference specification 'pipelineInterleaving', for that limit of +-- outstanding messages. +-- +prop_connect_pipelined5 :: [Bool] -> Positive Int -> NonNegative Int -> Bool +prop_connect_pipelined5 choices (Positive omax) (NonNegative n) = + connect_pipelined (pingPongClientPipelinedLimited omax n) choices + == + (n, reqResps) + where + reqResps = pipelineInterleaving omax choices [0..n-1] [0..n-1] + + +-- +-- Properties using channels, codecs and drivers. +-- + +-- | Run a non-pipelined client and server over a channel using a codec. +-- +prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) + => NonNegative Int + -> m Bool +prop_channel (NonNegative n) = do + ((), n') <- runConnectedPeers createConnectedChannels + nullTracer + codecPingPong client server + return (n' == n) + where + client = pingPongClientPeer (pingPongClientCount n) + server = pingPongServerPeer pingPongServerCount + + +prop_channel_IO :: NonNegative Int -> Property +prop_channel_IO n = + ioProperty (prop_channel n) + +prop_channel_ST :: NonNegative Int -> Bool +prop_channel_ST n = + runSimOrThrow (prop_channel n) + + +#if !defined(mingw32_HOST_OS) +prop_namedPipePipelined_IO :: NonNegative Int + -> Property +prop_namedPipePipelined_IO (NonNegative n) = ioProperty $ do + let client = pingPongClientPeer (pingPongClientCount n) + server = pingPongServerPeer pingPongServerCount + + let cliPath = "client.sock" + srvPath = "server.sock" + mode = Posix.ownerModes + + Posix.createNamedPipe cliPath mode + Posix.createNamedPipe srvPath mode + + bracket (openFile cliPath ReadWriteMode) + (\_ -> removeFile cliPath) + $ \cliHandle -> + bracket (openFile srvPath ReadWriteMode) + (\_ -> removeFile srvPath) + $ \srvHandle -> do + ((), n') <- runConnectedPeers (return ( handlesAsChannel cliHandle srvHandle + , handlesAsChannel srvHandle cliHandle + )) + nullTracer + CBOR.codecPingPong client server + return (n' == n) +#endif + + +#if !defined(mingw32_HOST_OS) +prop_socketPipelined_IO :: NonNegative Int + -> Property +prop_socketPipelined_IO (NonNegative n) = ioProperty $ do + ai : _ <- Socket.getAddrInfo (Just Socket.defaultHints + { Socket.addrFamily = Socket.AF_INET, + Socket.addrFlags = [Socket.AI_PASSIVE], + Socket.addrSocketType = Socket.Stream }) + (Just "127.0.0.1") Nothing + bracket + ((,) <$> Socket.openSocket ai + <*> Socket.openSocket ai) + ( \ (sock, sock') -> Socket.close sock + >> Socket.close sock') + $ \ (sock, sock') -> do + Socket.bind sock (Socket.addrAddress ai) + addr <- Socket.getSocketName sock + Socket.listen sock 1 + Socket.connect sock' addr + bracket (fst <$> Socket.accept sock) Socket.close + $ \sock'' -> do + let client = pingPongClientPeer (pingPongClientCount n) + server = pingPongServerPeer pingPongServerCount + + ((), n') <- runConnectedPeers (return ( socketAsChannel sock' + , socketAsChannel sock'' + )) + nullTracer + CBOR.codecPingPong client server + return (n' == n) +#endif + + +-- +-- Codec properties +-- + +instance Arbitrary (AnyMessage PingPong) where + arbitrary = elements + [ AnyMessage MsgPing + , AnyMessage MsgPong + , AnyMessage MsgDone + ] + +instance Eq (AnyMessage PingPong) where + AnyMessage MsgPing == AnyMessage MsgPing = True + AnyMessage MsgPong == AnyMessage MsgPong = True + AnyMessage MsgDone == AnyMessage MsgDone = True + _ == _ = False + +prop_codec_PingPong :: AnyMessage PingPong -> Bool +prop_codec_PingPong = + prop_codec + runIdentity + codecPingPong + +prop_codec_splits2_PingPong :: AnyMessage PingPong -> Bool +prop_codec_splits2_PingPong = + prop_codec_splits + splits2 + runIdentity + codecPingPong + +prop_codec_splits3_PingPong :: AnyMessage PingPong -> Bool +prop_codec_splits3_PingPong = + prop_codec_splits + splits3 + runIdentity + codecPingPong + +-- +-- CBOR codec properties +-- + +prop_codec_cbor_PingPong + :: AnyMessage PingPong + -> Bool +prop_codec_cbor_PingPong msg = + runST $ prop_codecM CBOR.codecPingPong msg + +prop_codec_cbor_splits2_PingPong + :: AnyMessage PingPong + -> Bool +prop_codec_cbor_splits2_PingPong msg = + runST $ prop_codec_splitsM + splits2BS + CBOR.codecPingPong + msg + +prop_codec_cbor_splits3_PingPong + :: AnyMessage PingPong + -> Bool +prop_codec_cbor_splits3_PingPong msg = + runST $ prop_codec_splitsM + splits3BS + CBOR.codecPingPong + msg + +-- +-- Utils +-- + +-- | Generate all 2-splits of a string. +-- +splits2 :: String -> [[String]] +splits2 str = zipWith (\a b -> [a,b]) (inits str) (tails str) + +-- | Generate all 3-splits of a string. +-- +splits3 :: String -> [[String]] +splits3 str = + [ [a,b,c] + | (a,str') <- zip (inits str) (tails str) + , (b,c) <- zip (inits str') (tails str') ] + +-- | Generate all 2-splits of a 'LBS.ByteString'. +-- +splits2BS :: LBS.ByteString -> [[LBS.ByteString]] +splits2BS bs = zipWith (\a b -> [a,b]) (LBS.inits bs) (LBS.tails bs) + +-- | Generate all 3-splits of a 'LBS.ByteString'. +-- +splits3BS :: LBS.ByteString -> [[LBS.ByteString]] +splits3BS bs = + [ [a,b,c] + | (a,bs') <- zip (LBS.inits bs) (LBS.tails bs) + , (b,c) <- zip (LBS.inits bs') (LBS.tails bs') ] diff --git a/test/Network/TypedProtocol/ReqResp/Tests.hs b/test/Network/TypedProtocol/ReqResp/Tests.hs new file mode 100644 --- /dev/null +++ b/test/Network/TypedProtocol/ReqResp/Tests.hs @@ -0,0 +1,362 @@ +{-# LANGUAGE CPP #-} +-- orphaned arbitrary instances +{-# OPTIONS_GHC -Wno-orphans #-} + +module Network.TypedProtocol.ReqResp.Tests (tests) where + +import Network.TypedProtocol.Channel +import Network.TypedProtocol.Codec +import Network.TypedProtocol.Driver.Simple +import Network.TypedProtocol.Proofs + +import Network.TypedProtocol.ReqResp.Client +import Network.TypedProtocol.ReqResp.Codec +import Network.TypedProtocol.ReqResp.Codec.CBOR qualified as CBOR +import Network.TypedProtocol.ReqResp.Examples +import Network.TypedProtocol.ReqResp.Server +import Network.TypedProtocol.ReqResp.Type + +import Control.Exception (throw) +import Control.Monad.Class.MonadAsync +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) + +import Data.Functor.Identity (Identity (..)) +import Data.List (intercalate, mapAccumL) +import Data.Tuple (swap) +#if !defined(mingw32_HOST_OS) +import Network.Socket qualified as Socket +import System.Directory (removeFile) +import System.IO +import System.Posix.Files qualified as Posix +#endif + +import Network.TypedProtocol.PingPong.Tests (splits2, splits2BS, splits3, + splits3BS) + +import Test.QuickCheck +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) +import Text.Show.Functions () + + +-- +-- The list of all properties +-- + +tests :: TestTree +tests = testGroup "Network.TypedProtocol.ReqResp" + [ testProperty "direct" prop_direct + , testProperty "directPipelined" prop_directPipelined + , testProperty "connect" prop_connect + , testProperty "connectPipelined" prop_connectPipelined + , testProperty "channel ST" prop_channel_ST + , testProperty "channel IO" prop_channel_IO + , testProperty "channelPipelined ST" prop_channelPipelined_ST + , testProperty "channelPipelined IO" prop_channelPipelined_IO +#if !defined(mingw32_HOST_OS) + , testProperty "namedPipePipelined" prop_namedPipePipelined_IO + , testProperty "socketPipelined" prop_socketPipelined_IO +#endif + , testGroup "Codec" + [ testProperty "codec" prop_codec_ReqResp + , testProperty "codec 2-splits" prop_codec_splits2_ReqResp + , testProperty "codec 3-splits" (withMaxSuccess 33 prop_codec_splits3_ReqResp) + , testGroup "CBOR" + [ testProperty "codec" prop_codec_cbor_ReqResp + , testProperty "codec 2-splits" prop_codec_cbor_splits2_ReqResp + , testProperty "codec 3-splits" $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp + ] + ] + ] + + +-- +-- Properties going directly, not via Peer. +-- + +direct :: Monad m + => ReqRespClient req resp m a + -> ReqRespServer req resp m b + -> m (a, b) + +direct (SendMsgDone clientResult) ReqRespServer{recvMsgDone} = + (,) <$> clientResult <*> recvMsgDone + +direct (SendMsgReq req kResp) ReqRespServer{recvMsgReq} = do + (resp, server') <- recvMsgReq req + client' <- kResp resp + direct client' server' + + +directPipelined :: Monad m + => ReqRespClientPipelined req resp m a + -> ReqRespServer req resp m b + -> m (a, b) +directPipelined (ReqRespClientPipelined client0) server0 = + go EmptyQ client0 server0 + where + go :: Monad m + => Queue n c + -> ReqRespIdle req resp n c m a + -> ReqRespServer req resp m b + -> m (a, b) + go EmptyQ (SendMsgDonePipelined clientResult) ReqRespServer{recvMsgDone} = + (clientResult,) <$> recvMsgDone + + go q (SendMsgReqPipelined req kResp client') ReqRespServer{recvMsgReq} = do + (resp, server') <- recvMsgReq req + x <- kResp resp + go (enqueue x q) client' server' + + go (ConsQ resp q) (CollectPipelined _ k) server = do + client' <- k resp + go q client' server + + +prop_direct :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool +prop_direct f xs = + runIdentity + (direct + (reqRespClientMap xs) + (reqRespServerMapAccumL (\a -> pure . f a) 0)) + == + swap (mapAccumL f 0 xs) + +prop_directPipelined :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool +prop_directPipelined f xs = + runIdentity + (directPipelined + (reqRespClientMapPipelined xs) + (reqRespServerMapAccumL (\a -> pure . f a) 0)) + == + swap (mapAccumL f 0 xs) + + +-- +-- Properties using connect +-- + +prop_connect :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool +prop_connect f xs = + case runIdentity + (connect + (reqRespClientPeer (reqRespClientMap xs)) + (reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0))) + + of (c, s, TerminalStates SingDone SingDone) -> + (s, c) == mapAccumL f 0 xs + + +prop_connectPipelined :: [Bool] -> (Int -> Int -> (Int, Int)) -> [Int] -> Bool +prop_connectPipelined cs f xs = + case runIdentity + (connectPipelined cs + (reqRespClientPeerPipelined (reqRespClientMapPipelined xs)) + (reqRespServerPeer + (reqRespServerMapAccumL (\a -> pure . f a) 0))) + + of (c, s, TerminalStates SingDone SingDone) -> + (s, c) == mapAccumL f 0 xs + + +-- +-- Properties using channels, codecs and drivers. +-- + +prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) + => (Int -> Int -> (Int, Int)) -> [Int] + -> m Bool +prop_channel f xs = do + (c, s) <- runConnectedPeers createConnectedChannels + nullTracer + codecReqResp client server + return ((s, c) == mapAccumL f 0 xs) + where + client = reqRespClientPeer (reqRespClientMap xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + + +prop_channel_IO :: (Int -> Int -> (Int, Int)) -> [Int] -> Property +prop_channel_IO f xs = + ioProperty (prop_channel f xs) + +prop_channel_ST :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool +prop_channel_ST f xs = + runSimOrThrow (prop_channel f xs) + + +prop_channelPipelined :: ( MonadLabelledSTM m, MonadAsync m, MonadCatch m + , MonadDelay m, MonadST m) + => (Int -> Int -> (Int, Int)) -> [Int] + -> m Bool +prop_channelPipelined f xs = do + (c, s) <- runConnectedPeersPipelined + (createPipelineTestChannels 100) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) + where + client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + +prop_channelPipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] -> Property +prop_channelPipelined_IO f xs = + ioProperty (prop_channelPipelined f xs) + +prop_channelPipelined_ST :: (Int -> Int -> (Int, Int)) -> [Int] -> Property +prop_channelPipelined_ST f xs = + let tr = runSimTrace (prop_channelPipelined f xs) in + counterexample (intercalate "\n" $ map show $ traceEvents tr) + $ case traceResult True tr of + Left err -> throw err + Right res -> res + + +#if !defined(mingw32_HOST_OS) +prop_namedPipePipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] + -> Property +prop_namedPipePipelined_IO f xs = ioProperty $ do + let client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + let cliPath = "client.sock" + srvPath = "server.sock" + mode = Posix.ownerModes + + Posix.createNamedPipe cliPath mode + Posix.createNamedPipe srvPath mode + + bracket (openFile cliPath ReadWriteMode) + (\_ -> removeFile cliPath) + $ \cliHandle -> + bracket (openFile srvPath ReadWriteMode) + (\_ -> removeFile srvPath) + $ \srvHandle -> do + (c, s) <- runConnectedPeersPipelined + (return ( handlesAsChannel cliHandle srvHandle + , handlesAsChannel srvHandle cliHandle + )) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) +#endif + + +#if !defined(mingw32_HOST_OS) +prop_socketPipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] + -> Property +prop_socketPipelined_IO f xs = ioProperty $ do + ai : _ <- Socket.getAddrInfo (Just Socket.defaultHints + { Socket.addrFamily = Socket.AF_INET, + Socket.addrFlags = [Socket.AI_PASSIVE], + Socket.addrSocketType = Socket.Stream }) + (Just "127.0.0.1") Nothing + bracket + ((,) <$> Socket.openSocket ai + <*> Socket.openSocket ai) + ( \ (sock, sock') -> Socket.close sock + >> Socket.close sock') + $ \ (sock, sock') -> do + Socket.bind sock (Socket.addrAddress ai) + addr <- Socket.getSocketName sock + Socket.listen sock 1 + Socket.connect sock' addr + bracket (fst <$> Socket.accept sock) Socket.close + $ \sock'' -> do + let client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + + (c, s) <- runConnectedPeersPipelined + (return ( socketAsChannel sock' + , socketAsChannel sock'' + )) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) +#endif + +-- +-- Codec properties +-- + +instance (Arbitrary req, Arbitrary resp) => + Arbitrary (AnyMessage (ReqResp req resp)) where + arbitrary = oneof + [ AnyMessage . MsgReq <$> arbitrary + , AnyMessage . MsgResp <$> arbitrary + , return (AnyMessage MsgDone) + ] + + shrink (AnyMessage (MsgReq r)) = + [ AnyMessage (MsgReq r') + | r' <- shrink r ] + + shrink (AnyMessage (MsgResp r)) = + [ AnyMessage (MsgResp r') + | r' <- shrink r ] + + shrink (AnyMessage MsgDone) = [] + +instance (Eq req, Eq resp) => Eq (AnyMessage (ReqResp req resp)) where + (AnyMessage (MsgReq r1)) == (AnyMessage (MsgReq r2)) = r1 == r2 + (AnyMessage (MsgResp r1)) == (AnyMessage (MsgResp r2)) = r1 == r2 + (AnyMessage MsgDone) == (AnyMessage MsgDone) = True + _ == _ = False + +prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Bool +prop_codec_ReqResp = + prop_codec + runIdentity + codecReqResp + +prop_codec_splits2_ReqResp :: AnyMessage (ReqResp String String) + -> Bool +prop_codec_splits2_ReqResp = + prop_codec_splits + splits2 + runIdentity + codecReqResp + +prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String) + -> Bool +prop_codec_splits3_ReqResp = + prop_codec_splits + splits3 + runIdentity + codecReqResp + +prop_codec_cbor_ReqResp + :: AnyMessage (ReqResp String String) + -> Bool +prop_codec_cbor_ReqResp msg = + runST $ prop_codecM CBOR.codecReqResp msg + +prop_codec_cbor_splits2_ReqResp + :: AnyMessage (ReqResp String String) + -> Bool +prop_codec_cbor_splits2_ReqResp msg = + runST $ prop_codec_splitsM + splits2BS + CBOR.codecReqResp + msg + +prop_codec_cbor_splits3_ReqResp + :: AnyMessage (ReqResp String String) + -> Bool +prop_codec_cbor_splits3_ReqResp msg = + runST $ prop_codec_splitsM + splits3BS + CBOR.codecReqResp + msg diff --git a/typed-protocols.cabal b/typed-protocols.cabal new file mode 100644 --- /dev/null +++ b/typed-protocols.cabal @@ -0,0 +1,204 @@ +cabal-version: 3.4 +name: typed-protocols +version: 1.0.0.0 +synopsis: A framework for strongly typed protocols +description: A robust session type framework which supports protocol pipelining. +license: Apache-2.0 +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} +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 + ghc-options: -Wall + -Wno-unticked-promoted-constructors + -Wcompat + -Wincomplete-uni-patterns + -Wincomplete-record-updates + -Wpartial-fields + -Widentities + -Wredundant-constraints + +library cborg + visibility: public + exposed-modules: Network.TypedProtocol.Codec.CBOR + + build-depends: base, + bytestring >=0.10 && <0.13, + cborg >=0.2.1 && <0.3, + singletons, + primitive, + + io-classes:io-classes, + typed-protocols:typed-protocols + + 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 stateful + visibility: public + exposed-modules: Network.TypedProtocol.Stateful.Peer + , Network.TypedProtocol.Stateful.Peer.Client + , Network.TypedProtocol.Stateful.Peer.Server + , Network.TypedProtocol.Stateful.Driver + , Network.TypedProtocol.Stateful.Proofs + , Network.TypedProtocol.Stateful.Codec + build-depends: base, + 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, + + io-classes:io-classes, + typed-protocols:{typed-protocols,cborg,stateful} + + hs-source-dirs: stateful-cborg + default-language: GHC2021 + 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 + + , 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.ReqResp2.Type + , Network.TypedProtocol.ReqResp2.Client + + , 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.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} + + hs-source-dirs: examples + default-language: GHC2021 + 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 + 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 + + if !os(windows) + build-depends: directory + , network + , unix + + ghc-options: -rtsopts + -Wall + -Wno-unticked-promoted-constructors + -Wno-orphans