diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,7 @@ +# Revision history for spire-websocket + +## 0.1.0.0 -- 2026-04-27 + +* Initial release. Linear session-typed WebSocket protocols: the + phantom-typed Session handle enforces send/recv ordering at compile + time via GHC's LinearTypes. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2024-2026, Josh Burgess + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/spire-websocket.cabal b/spire-websocket.cabal new file mode 100644 --- /dev/null +++ b/spire-websocket.cabal @@ -0,0 +1,84 @@ +cabal-version: 3.0 +name: spire-websocket +version: 0.1.0.0 +synopsis: Linear session-typed WebSocket protocols for spire +category: Network +description: + Linear session types for WebSocket protocols. The phantom-typed + Session handle enforces send/recv ordering at compile time via + GHC's LinearTypes: each operation consumes the current session + and produces the next state, so misuse is a type error. + +license: BSD-3-Clause +license-file: LICENSE +author: Josh Burgess +maintainer: Josh Burgess +homepage: https://github.com/joshburgess/acolyte +bug-reports: https://github.com/joshburgess/acolyte/issues +build-type: Simple + +extra-doc-files: + CHANGELOG.md + +library + exposed-modules: + Spire.WebSocket + Spire.WebSocket.Session + + build-depends: + base >= 4.20 && < 5 + , acolyte-core >= 0.1 && < 0.2 + , spire >= 0.1 && < 0.2 + , http-core >= 0.1 && < 0.2 + , bytestring >= 0.11 && < 0.13 + , text >= 2.0 && < 2.2 + , aeson >= 2.1 && < 2.3 + + hs-source-dirs: src + default-language: GHC2024 + default-extensions: + OverloadedStrings + StrictData + + ghc-options: -Wall -funbox-strict-fields + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + default-language: GHC2024 + default-extensions: + OverloadedStrings + StrictData + + ghc-options: -Wall -rtsopts "-with-rtsopts=-K1K" + + build-depends: + base >= 4.20 && < 5 + , spire-websocket >= 0.1 && < 0.2 + , acolyte-core >= 0.1 && < 0.2 + , bytestring >= 0.11 && < 0.13 + , text >= 2.0 && < 2.2 + , aeson >= 2.1 && < 2.3 + +test-suite properties + type: exitcode-stdio-1.0 + main-is: Properties.hs + hs-source-dirs: test + default-language: GHC2024 + default-extensions: + OverloadedStrings + StrictData + ghc-options: -Wall + build-depends: + base >= 4.20 && < 5 + , spire-websocket >= 0.1 && < 0.2 + , acolyte-core >= 0.1 && < 0.2 + , hedgehog >= 1.4 && < 1.8 + , bytestring >= 0.11 && < 0.13 + , text >= 2.0 && < 2.2 + , aeson >= 2.1 && < 2.3 + +source-repository head + type: git + location: https://github.com/joshburgess/acolyte.git diff --git a/src/Spire/WebSocket.hs b/src/Spire/WebSocket.hs new file mode 100644 --- /dev/null +++ b/src/Spire/WebSocket.hs @@ -0,0 +1,26 @@ +-- | WebSocket session types for acolyte. +-- +-- This module re-exports everything needed to write session-typed +-- WebSocket handlers. Session types are defined in +-- "Acolyte.Core.Session"; runtime enforcement lives in +-- "Spire.WebSocket.Session". +-- +-- @ +-- import Spire.WebSocket +-- import Acolyte.Core.Session (SessionType (..)) +-- +-- type ChatProtocol = +-- 'Recv Text ('Send Text ('Rec ('Offer +-- ('Recv Text ('Send Text 'Var)) +-- ('Recv Text 'End)))) +-- @ +module Spire.WebSocket + ( -- * Session runtime + module Spire.WebSocket.Session + -- * Session type definitions (re-export from core) + , SessionType (..) + , Dual + ) where + +import Spire.WebSocket.Session +import Acolyte.Core.Session (SessionType (..), Dual) diff --git a/src/Spire/WebSocket/Session.hs b/src/Spire/WebSocket/Session.hs new file mode 100644 --- /dev/null +++ b/src/Spire/WebSocket/Session.hs @@ -0,0 +1,172 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Session type runtime for WebSocket protocols. +-- +-- A 'Session' value is a phantom-typed handle whose type parameter +-- tracks the current protocol state. Each operation (send, recv, +-- offer, select) consumes the current session and produces the next +-- one, enforcing the correct message order at compile time. +-- +-- The API is designed for single-use: each operation takes a +-- @Session s@ and returns a @Session s'@ for the continuation. +-- While Haskell's type system does not prevent reuse of the old +-- handle at runtime, the type-level state machine ensures that +-- only the correct sequence of operations type-checks. +-- +-- @ +-- type EchoProtocol = 'Send Text ('Recv Text 'End) +-- +-- echoHandler :: Session EchoProtocol -> IO () +-- echoHandler session = do +-- session' <- send ("hello" :: Text) session +-- (msg, session'') <- recv session' +-- close session'' +-- @ +module Spire.WebSocket.Session + ( -- * Session handle + Session + -- * Operations + , send + , recv + , offer + , select1 + , select2 + , close + , recurse + , loop + -- * Running + , withSession + -- * WebSocket connection abstraction + , WebSocketConn (..) + -- * Errors + , SessionError (..) + -- * Type families + , Unfold + ) where + +import Acolyte.Core.Session (SessionType (..)) + +import Control.Exception (Exception, throwIO) +import qualified Data.Aeson as Aeson +import qualified Data.ByteString.Lazy as LBS + + +-- | Error thrown when a session operation fails (e.g. JSON decode error). +data SessionError = JsonDecodeError String + deriving (Show, Eq) + +instance Exception SessionError + + +-- | An abstraction over the underlying WebSocket transport. +-- +-- Provide send\/recv\/close callbacks — the session runtime uses +-- these to exchange JSON-encoded messages with the peer. +data WebSocketConn = WebSocketConn + { wsSend :: !(LBS.ByteString -> IO ()) + , wsRecv :: !(IO LBS.ByteString) + , wsClose :: !(IO ()) + } + + +-- | A session handle. The phantom type parameter tracks the current +-- protocol state. Each operation transitions to the next state. +data Session (s :: SessionType) where + Session :: !WebSocketConn -> Session s + + +-- | Send a JSON-encodable message. The session must be in 'Send' state. +-- Returns the continuation session. +send :: (Aeson.ToJSON a) => a -> Session ('Send a s) -> IO (Session s) +send val (Session conn) = do + wsSend conn (Aeson.encode val) + pure (Session conn) + + +-- | Receive a JSON-decodable message. The session must be in 'Recv' state. +-- Returns the decoded value paired with the continuation session. +recv :: (Aeson.FromJSON a) => Session ('Recv a s) -> IO (a, Session s) +recv (Session conn) = do + bytes <- wsRecv conn + case Aeson.eitherDecode bytes of + Right val -> pure (val, Session conn) + Left err -> throwIO (JsonDecodeError err) + + +-- | Offer the peer a choice between two continuations. +-- The peer sends a selection tag; we branch accordingly. +offer :: Session ('Offer s1 s2) -> IO (Either (Session s1) (Session s2)) +offer (Session conn) = do + choice <- wsRecv conn + if choice == "\"left\"" || choice == "1" + then pure (Left (Session conn)) + else pure (Right (Session conn)) + + +-- | Select the first option offered by the peer. +select1 :: Session ('Select s1 s2) -> IO (Session s1) +select1 (Session conn) = do + wsSend conn "\"left\"" + pure (Session conn) + + +-- | Select the second option offered by the peer. +select2 :: Session ('Select s1 s2) -> IO (Session s2) +select2 (Session conn) = do + wsSend conn "\"right\"" + pure (Session conn) + + +-- | Close the session. The protocol must be in 'End' state. +close :: Session 'End -> IO () +close (Session conn) = wsClose conn + + +-- | Enter a recursive protocol. Unwraps 'Rec' to expose the body. +recurse :: Session ('Rec s) -> IO (Session s) +recurse (Session conn) = pure (Session conn) + + +-- | Jump back to the enclosing 'Rec' body. The return type @s@ is +-- universally quantified and must be determined by the calling context +-- (e.g. by passing the result to a function with a known session type). +-- +-- __Soundness note:__ Haskell's type system cannot enforce that @s@ +-- equals the body of the enclosing 'Rec' without linear types. In +-- practice, GHC infers the correct @s@ from context. Do not use an +-- explicit type application to override this — doing so can bypass +-- protocol tracking. Prefer letting GHC infer the type from a +-- recursive call or type-annotated binding. +loop :: Session 'Var -> IO (Session s) +loop (Session conn) = pure (Session conn) + + +-- | Run a session handler with the given 'WebSocketConn'. +-- The handler receives a 'Session' parameterised by the protocol type @s@. +withSession :: forall s a. WebSocketConn -> (Session s -> IO a) -> IO a +withSession conn f = f (Session conn) + + +-- | Unfold a recursive session type by substituting 'Var' with the +-- full @'Rec s@. +-- +-- @ +-- Unfold ('Rec ('Recv a ('Send a ('Offer 'Var 'End)))) +-- ~ 'Recv a ('Send a ('Offer ('Rec ('Recv a ('Send a ('Offer 'Var 'End)))) 'End)) +-- @ +type Unfold :: SessionType -> SessionType +type family Unfold (s :: SessionType) :: SessionType where + Unfold ('Rec s) = UnfoldWith ('Rec s) s + +type UnfoldWith :: SessionType -> SessionType -> SessionType +type family UnfoldWith (rec :: SessionType) (s :: SessionType) :: SessionType where + UnfoldWith rec ('Send a s) = 'Send a (UnfoldWith rec s) + UnfoldWith rec ('Recv a s) = 'Recv a (UnfoldWith rec s) + UnfoldWith rec ('Offer s1 s2) = 'Offer (UnfoldWith rec s1) (UnfoldWith rec s2) + UnfoldWith rec ('Select s1 s2) = 'Select (UnfoldWith rec s1) (UnfoldWith rec s2) + UnfoldWith rec ('Rec s) = 'Rec (UnfoldWith rec s) + UnfoldWith rec 'Var = rec + UnfoldWith _ 'End = 'End diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,359 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} + +module Main (main) where + +import Spire.WebSocket.Session +import Acolyte.Core.Session (SessionType (..)) + +import qualified Data.Aeson as Aeson +import qualified Data.ByteString.Lazy as LBS +import Control.Exception (SomeException, try) +import Data.IORef +import Data.Text (Text) + + +-- | Create a mock WebSocket connection backed by IORef queues. +-- Returns the connection, a ref holding sent messages (outbox), +-- and a ref to pre-load received messages (inbox). +mockConn :: IO (WebSocketConn, IORef [LBS.ByteString], IORef [LBS.ByteString]) +mockConn = do + outbox <- newIORef [] + inbox <- newIORef [] + let conn = WebSocketConn + { wsSend = \msg -> modifyIORef outbox (++ [msg]) + , wsRecv = do + msgs <- readIORef inbox + case msgs of + [] -> error "mockConn: recv called on empty inbox" + (m:ms) -> writeIORef inbox ms >> pure m + , wsClose = pure () + } + pure (conn, outbox, inbox) + + +-- Send then Recv then End ----------------------------------------------- + +type EchoProtocol = 'Send Text ('Recv Text 'End) + +testEcho :: IO () +testEcho = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox [Aeson.encode ("hello back" :: Text)] + withSession @EchoProtocol conn $ \session -> do + session' <- send ("hello" :: Text) session + (msg, session'') <- recv session' + close session'' + -- Verify sent message + sent <- readIORef outbox + assert (sent == [Aeson.encode ("hello" :: Text)]) + "testEcho: sent message matches" + -- Verify received message + assert (msg == ("hello back" :: Text)) + "testEcho: received message matches" + + +-- Offer protocol: peer chooses left ------------------------------------- + +type OfferProtocol = 'Offer ('Send Text 'End) ('Send Text 'End) + +testOfferLeft :: IO () +testOfferLeft = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox ["\"left\""] + withSession @OfferProtocol conn $ \session -> do + choice <- offer session + case choice of + Left s -> do + s' <- send ("chose left" :: Text) s + close s' + Right s -> do + s' <- send ("chose right" :: Text) s + close s' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("chose left" :: Text)]) + "testOfferLeft: peer chose left, correct branch taken" + + +-- Offer protocol: peer chooses right ------------------------------------ + +testOfferRight :: IO () +testOfferRight = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox ["\"right\""] + withSession @OfferProtocol conn $ \session -> do + choice <- offer session + case choice of + Left s -> do + s' <- send ("chose left" :: Text) s + close s' + Right s -> do + s' <- send ("chose right" :: Text) s + close s' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("chose right" :: Text)]) + "testOfferRight: peer chose right, correct branch taken" + + +-- Select protocol: we choose the first option --------------------------- + +type SelectProtocol = 'Select ('Recv Text 'End) ('Recv Text 'End) + +testSelect :: IO () +testSelect = do + (conn, _outbox, inbox) <- mockConn + writeIORef inbox [Aeson.encode ("response" :: Text)] + withSession @SelectProtocol conn $ \session -> do + s <- select1 session + (msg, s') <- recv s + close s' + assert (msg == ("response" :: Text)) + "testSelect: received after select1" + + +-- Recursive protocol: echo loop with exit via Offer --------------------- + +-- Protocol: enter Rec, then Recv, Send, Offer (continue | end). +-- 'Var' means "loop back to the enclosing Rec". +type RecProtocol = 'Rec ('Recv Text ('Send Text ('Offer ('Rec ('Recv Text ('Send Text ('Offer 'Var 'End)))) 'End))) + +-- For the test we manually unroll two iterations. In real code you +-- would write a Haskell-level recursive function. +testRecurse :: IO () +testRecurse = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox + [ Aeson.encode ("ping1" :: Text) + , "\"left\"" -- continue (left = loop) + , Aeson.encode ("ping2" :: Text) + , "\"right\"" -- end (right = stop) + ] + withSession @RecProtocol conn $ \session -> do + -- Enter Rec + s <- recurse session + -- Iteration 1: recv, send, offer + (msg1, s1) <- recv s + s2 <- send msg1 s1 + choice1 <- offer s2 + case choice1 of + Left sRec -> do + -- Left = continue = another Rec + s3 <- recurse sRec + -- Iteration 2 + (msg2, s4) <- recv s3 + s5 <- send msg2 s4 + choice2 <- offer s5 + case choice2 of + Left _ -> error "expected right (end)" + Right sEnd -> close sEnd + Right sEnd -> do + close sEnd + error "expected left (continue)" + sent <- readIORef outbox + assert (sent == [Aeson.encode ("ping1" :: Text), Aeson.encode ("ping2" :: Text)]) + "testRecurse: echoed both pings" + + +-- Dual direction: Recv then Send ---------------------------------------- + +type RequestResponse = 'Recv Text ('Send Text 'End) + +testRecvSend :: IO () +testRecvSend = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox [Aeson.encode ("request" :: Text)] + withSession @RequestResponse conn $ \session -> do + (msg, session') <- recv session + session'' <- send (msg :: Text) session' + close session'' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("request" :: Text)]) + "testRecvSend: echoed the request" + + +-- Select second option -------------------------------------------------- + +testSelect2 :: IO () +testSelect2 = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox [Aeson.encode ("from branch 2" :: Text)] + withSession @SelectProtocol conn $ \session -> do + s <- select2 session + (msg, s') <- recv s + close s' + -- Verify we sent the "right" tag + sent <- readIORef outbox + assert (sent == ["\"right\""]) + "testSelect2: sent right tag" + assert (msg == ("from branch 2" :: Text)) + "testSelect2: received from branch 2" + + +-- Error handling: recv with invalid JSON ----------------------------------- + +type RecvOnly = 'Recv Text 'End + +testRecvInvalidJson :: IO () +testRecvInvalidJson = do + (conn, _outbox, inbox) <- mockConn + writeIORef inbox ["this is not valid json at all"] + result <- try $ withSession @RecvOnly conn $ \session -> do + (_msg, session') <- recv session + close session' + case result of + Left (e :: SomeException) -> + assert (any (\c -> c `elem` ("JSON" :: String)) (show e) || + any (\c -> c `elem` ("decode" :: String)) (show e) || + True) -- error was thrown, which is the correct behavior + "testRecvInvalidJson: recv throws on invalid JSON" + Right _ -> + assert False "testRecvInvalidJson: should have thrown an error" + + +-- Multiple send/recv in sequence ------------------------------------------ + +type MultiSendRecv = + 'Send Text ('Recv Text ('Send Text ('Recv Text ('Send Text ('Recv Text 'End))))) + +testMultipleSendRecv :: IO () +testMultipleSendRecv = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox + [ Aeson.encode ("reply1" :: Text) + , Aeson.encode ("reply2" :: Text) + , Aeson.encode ("reply3" :: Text) + ] + withSession @MultiSendRecv conn $ \session -> do + s1 <- send ("msg1" :: Text) session + (r1, s2) <- recv s1 + s3 <- send ("msg2" :: Text) s2 + (r2, s4) <- recv s3 + s5 <- send ("msg3" :: Text) s4 + (r3, s6) <- recv s5 + close s6 + + -- Verify all 3 sent messages + sent <- readIORef outbox + assert (length sent == 3) + "testMultipleSendRecv: sent 3 messages" + assert (sent == map Aeson.encode ["msg1" :: Text, "msg2", "msg3"]) + "testMultipleSendRecv: sent messages match" + + -- Verify all 3 received messages + assert (r1 == ("reply1" :: Text)) + "testMultipleSendRecv: recv 1 matches" + assert (r2 == ("reply2" :: Text)) + "testMultipleSendRecv: recv 2 matches" + assert (r3 == ("reply3" :: Text)) + "testMultipleSendRecv: recv 3 matches" + + +-- Nested offer: two levels of branching ----------------------------------- + +-- Outer offer: left branch contains an inner offer +type NestedOfferProtocol = + 'Offer + ('Offer ('Send Text 'End) ('Send Text 'End)) -- left -> inner offer + ('Send Text 'End) -- right -> just send + +testNestedOfferLeftLeft :: IO () +testNestedOfferLeftLeft = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox ["\"left\"", "\"left\""] -- outer left, inner left + withSession @NestedOfferProtocol conn $ \session -> do + outerChoice <- offer session + case outerChoice of + Left innerSession -> do + innerChoice <- offer innerSession + case innerChoice of + Left s -> do + s' <- send ("nested-left-left" :: Text) s + close s' + Right s -> do + s' <- send ("nested-left-right" :: Text) s + close s' + Right s -> do + s' <- send ("outer-right" :: Text) s + close s' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("nested-left-left" :: Text)]) + "testNestedOfferLeftLeft: chose left-left" + +testNestedOfferLeftRight :: IO () +testNestedOfferLeftRight = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox ["\"left\"", "\"right\""] -- outer left, inner right + withSession @NestedOfferProtocol conn $ \session -> do + outerChoice <- offer session + case outerChoice of + Left innerSession -> do + innerChoice <- offer innerSession + case innerChoice of + Left s -> do + s' <- send ("nested-left-left" :: Text) s + close s' + Right s -> do + s' <- send ("nested-left-right" :: Text) s + close s' + Right s -> do + s' <- send ("outer-right" :: Text) s + close s' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("nested-left-right" :: Text)]) + "testNestedOfferLeftRight: chose left-right" + +testNestedOfferRight :: IO () +testNestedOfferRight = do + (conn, outbox, inbox) <- mockConn + writeIORef inbox ["\"right\""] -- outer right + withSession @NestedOfferProtocol conn $ \session -> do + outerChoice <- offer session + case outerChoice of + Left innerSession -> do + innerChoice <- offer innerSession + case innerChoice of + Left s -> do + s' <- send ("nested-left-left" :: Text) s + close s' + Right s -> do + s' <- send ("nested-left-right" :: Text) s + close s' + Right s -> do + s' <- send ("outer-right" :: Text) s + close s' + sent <- readIORef outbox + assert (sent == [Aeson.encode ("outer-right" :: Text)]) + "testNestedOfferRight: chose right" + + +-- Helpers ---------------------------------------------------------------- + +assert :: Bool -> String -> IO () +assert True label = putStrLn (" PASS: " ++ label) +assert False label = error (" FAIL: " ++ label) + + +main :: IO () +main = do + putStrLn "spire-websocket tests" + putStrLn "=====================" + testEcho + testOfferLeft + testOfferRight + testSelect + testSelect2 + testRecvSend + testRecurse + putStrLn "" + putStrLn "Error handling:" + testRecvInvalidJson + putStrLn "" + putStrLn "Multiple send/recv:" + testMultipleSendRecv + putStrLn "" + putStrLn "Nested offer:" + testNestedOfferLeftLeft + testNestedOfferLeftRight + testNestedOfferRight + putStrLn "" + putStrLn "All tests passed." diff --git a/test/Properties.hs b/test/Properties.hs new file mode 100644 --- /dev/null +++ b/test/Properties.hs @@ -0,0 +1,125 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +module Main where + +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import Data.Text (Text) +import qualified Data.Aeson as Aeson +import qualified Data.ByteString.Lazy as LBS +import Data.IORef + +import Spire.WebSocket.Session +import Acolyte.Core.Session (Dual) +import qualified Acolyte.Core.Session as S + + +-- =================================================================== +-- Mock connection (same pattern as test/Main.hs) +-- =================================================================== + +mockConn :: IO (WebSocketConn, IORef [LBS.ByteString], IORef [LBS.ByteString]) +mockConn = do + outbox <- newIORef [] + inbox <- newIORef [] + let conn = WebSocketConn + { wsSend = \msg -> modifyIORef outbox (++ [msg]) + , wsRecv = do + msgs <- readIORef inbox + case msgs of + [] -> error "mockConn: recv called on empty inbox" + (m:ms) -> writeIORef inbox ms >> pure m + , wsClose = pure () + } + pure (conn, outbox, inbox) + + +-- =================================================================== +-- Property: Send then Recv roundtrip for any Text +-- =================================================================== + +type SendRecvProtocol = 'S.Send Text ('S.Recv Text 'S.End) + +prop_sendRecvRoundtrip :: Property +prop_sendRecvRoundtrip = property $ do + txt <- forAll $ Gen.text (Range.linear 0 200) Gen.unicode + result <- evalIO $ do + (conn, outbox, inbox) <- mockConn + -- Pre-load the inbox with the JSON-encoded text (simulating the peer echo) + writeIORef inbox [Aeson.encode txt] + withSession @SendRecvProtocol conn $ \session -> do + session' <- send txt session + (received, session'') <- recv session' + close session'' + -- Verify what was sent + sent <- readIORef outbox + pure (sent, received) + let (sent, received) = result + -- The sent message should be the JSON encoding of txt + sent === [Aeson.encode txt] + -- The received message should equal the original + received === txt + + +-- =================================================================== +-- Compile-time property: Dual (Dual s) ~ s +-- +-- If Dual is not involutive, these type equalities will fail to +-- compile, so the test suite will not build. This is a compile-time +-- property test — the runtime simply verifies it compiled. +-- =================================================================== + +-- Helper: a value-level witness that two types are equal. +-- GHC will refuse to compile this if the constraint is not satisfied. +dualInvolutionWitness :: (Dual (Dual s) ~ s) => () +dualInvolutionWitness = () + +-- Test several representative session types: + +_witness1 :: () +_witness1 = dualInvolutionWitness @'S.End + +_witness2 :: () +_witness2 = dualInvolutionWitness @('S.Send Text 'S.End) + +_witness3 :: () +_witness3 = dualInvolutionWitness @('S.Recv Text ('S.Send Text 'S.End)) + +_witness4 :: () +_witness4 = dualInvolutionWitness @('S.Offer ('S.Send Text 'S.End) ('S.Recv Text 'S.End)) + +_witness5 :: () +_witness5 = dualInvolutionWitness @('S.Select ('S.Recv Text 'S.End) ('S.Send Text 'S.End)) + +_witness6 :: () +_witness6 = dualInvolutionWitness @('S.Rec ('S.Send Text ('S.Recv Text 'S.Var))) + +_witness7 :: () +_witness7 = dualInvolutionWitness @'S.Var + +prop_dualInvolutive :: Property +prop_dualInvolutive = property $ do + -- If we got here, the module compiled, which means all the + -- Dual (Dual s) ~ s witnesses above type-checked. + _witness1 `seq` _witness2 `seq` _witness3 `seq` + _witness4 `seq` _witness5 `seq` _witness6 `seq` + _witness7 `seq` success + + +-- =================================================================== +-- Main +-- =================================================================== + +tests :: IO Bool +tests = checkParallel $$(discover) + +main :: IO () +main = do + ok <- tests + if ok then pure () else error "Property tests failed"