{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module Ouroboros.Network.Protocol.KeepAlive.Test where

import Control.Monad.Class.MonadAsync
import Control.Monad.Class.MonadST
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 Codec.CBOR.Read qualified as CBOR
import Data.ByteString.Lazy (ByteString)
import Data.ByteString.Lazy qualified as BL

import Network.TypedProtocol.Codec hiding (prop_codec)
import Network.TypedProtocol.Proofs

import Ouroboros.Network.Channel
import Ouroboros.Network.Driver.Limits
import Ouroboros.Network.Driver.Simple (runConnectedPeers)

import Ouroboros.Network.Protocol.KeepAlive.Client
import Ouroboros.Network.Protocol.KeepAlive.Codec
import Ouroboros.Network.Protocol.KeepAlive.Direct
import Ouroboros.Network.Protocol.KeepAlive.Examples
import Ouroboros.Network.Protocol.KeepAlive.Server
import Ouroboros.Network.Protocol.KeepAlive.Type

import Test.Ouroboros.Network.Testing.Utils (prop_codec_valid_cbor_encoding,
           splits2, splits3)


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 :: TestTree
tests = TestName -> [TestTree] -> TestTree
testGroup TestName
"Ouroboros.Network.Protocol.KeepAlive"
  [ TestName
-> ((Int -> Int) -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"direct"              (Int -> Int) -> NonNegative Int -> Property
prop_direct
  , TestName -> ((Int -> Int) -> NonNegative Int -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"connect"             (Int -> Int) -> NonNegative Int -> Bool
prop_connect
  , TestName
-> ((Int -> Int) -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"channel ST"          (Int -> Int) -> NonNegative Int -> Property
prop_channel_ST
  , TestName
-> ((Int -> Int) -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"channel IO"          (Int -> Int) -> NonNegative Int -> Property
prop_channel_IO
  , TestName -> (AnyMessage KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2"            AnyMessage KeepAlive -> Bool
prop_codec_v2
  , TestName -> (AnyMessage KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 2-splits"   AnyMessage KeepAlive -> Bool
prop_codec_v2_splits2
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 3-splits"   (Int -> (AnyMessage KeepAlive -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
33 AnyMessage KeepAlive -> Bool
prop_codec_v2_splits3)
  , TestName -> (AnyMessage KeepAlive -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 valid CBOR" AnyMessage KeepAlive -> Property
prop_codec_v2_valid_cbor
  , TestName -> (AnyMessage KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"byteLimits"          AnyMessage KeepAlive -> Bool
prop_byteLimits
  ]

--
-- Properties going directly, not via Peer.
--

prop_direct :: (Int -> Int) -> NonNegative Int -> Property
prop_direct :: (Int -> Int) -> NonNegative Int -> Property
prop_direct Int -> Int
f (NonNegative Int
n) =
      (forall s. IOSim s (Int, Int)) -> (Int, Int)
forall a. (forall s. IOSim s a) -> a
runSimOrThrow
        (KeepAliveServer (IOSim s) Int
-> KeepAliveClient (IOSim s) Int -> IOSim s (Int, Int)
forall a b (m :: * -> *).
Monad m =>
KeepAliveServer m a -> KeepAliveClient m b -> m (a, b)
direct
          KeepAliveServer (IOSim s) Int
forall (m :: * -> *). Applicative m => KeepAliveServer m Int
keepAliveServerCount
          ((Int -> Int) -> Int -> Int -> KeepAliveClient (IOSim s) Int
forall acc (m :: * -> *).
Monad m =>
(acc -> acc) -> acc -> Int -> KeepAliveClient m acc
keepAliveClientApply Int -> Int
f Int
0 Int
n))
   (Int, Int) -> (Int, Int) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===
      (Int
n, ((Int -> Int) -> (Int -> Int) -> Int -> Int)
-> (Int -> Int) -> [Int -> Int] -> Int -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Int -> Int
forall a. a -> a
id (Int -> (Int -> Int) -> [Int -> Int]
forall a. Int -> a -> [a]
replicate Int
n Int -> Int
f) Int
0)

--
-- Properties using connect
--

prop_connect :: (Int -> Int)
             -> NonNegative Int
             -> Bool
prop_connect :: (Int -> Int) -> NonNegative Int -> Bool
prop_connect Int -> Int
f (NonNegative Int
n) =
   case (forall s. IOSim s (Int, Int, TerminalStates KeepAlive))
-> (Int, Int, TerminalStates KeepAlive)
forall a. (forall s. IOSim s a) -> a
runSimOrThrow
          (Peer KeepAlive 'AsServer 'NonPipelined 'StClient (IOSim s) Int
-> Peer
     KeepAlive
     (FlipAgency 'AsServer)
     'NonPipelined
     'StClient
     (IOSim s)
     Int
-> IOSim s (Int, Int, TerminalStates KeepAlive)
forall ps (pr :: PeerRole) (initSt :: ps) (m :: * -> *) a b.
(Monad m, SingI pr) =>
Peer ps pr 'NonPipelined initSt m a
-> Peer ps (FlipAgency pr) 'NonPipelined initSt m b
-> m (a, b, TerminalStates ps)
connect
            (KeepAliveServer (IOSim s) Int
-> Peer KeepAlive 'AsServer 'NonPipelined 'StClient (IOSim s) Int
forall (m :: * -> *) a.
Functor m =>
KeepAliveServer m a -> Server KeepAlive 'NonPipelined 'StClient m a
keepAliveServerPeer   KeepAliveServer (IOSim s) Int
forall (m :: * -> *). Applicative m => KeepAliveServer m Int
keepAliveServerCount)
            (KeepAliveClient (IOSim s) Int
-> Client KeepAlive 'NonPipelined 'StClient (IOSim s) Int
forall (m :: * -> *) a.
MonadThrow m =>
KeepAliveClient m a -> Client KeepAlive 'NonPipelined 'StClient m a
keepAliveClientPeer (KeepAliveClient (IOSim s) Int
 -> Client KeepAlive 'NonPipelined 'StClient (IOSim s) Int)
-> KeepAliveClient (IOSim s) Int
-> Client KeepAlive 'NonPipelined 'StClient (IOSim s) Int
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Int -> Int -> KeepAliveClient (IOSim s) Int
forall acc (m :: * -> *).
Monad m =>
(acc -> acc) -> acc -> Int -> KeepAliveClient m acc
keepAliveClientApply Int -> Int
f Int
0 Int
n))

     of (Int
s, Int
c, TerminalStates SingKeepAlive st
StateToken st
SingDone SingKeepAlive 'StDone
StateToken st
SingDone) ->
          (Int
s, Int
c) (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
n, ((Int -> Int) -> (Int -> Int) -> Int -> Int)
-> (Int -> Int) -> [Int -> Int] -> Int -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Int -> Int
forall a. a -> a
id (Int -> (Int -> Int) -> [Int -> Int]
forall a. Int -> a -> [a]
replicate Int
n Int -> Int
f) Int
0)

--
-- Properties using channels, codecs and drivers.
--

prop_channel :: ( MonadST    m
                , MonadSTM   m
                , MonadAsync m
                , MonadCatch m
                )
             => (Int -> Int)
             -> Int
             -> m Property
prop_channel :: forall (m :: * -> *).
(MonadST m, MonadSTM m, MonadAsync m, MonadCatch m) =>
(Int -> Int) -> Int -> m Property
prop_channel Int -> Int
f Int
n = do
    (s, c) <- m (Channel m ByteString, Channel m ByteString)
-> Tracer m (Role, TraceSendRecv KeepAlive)
-> Codec KeepAlive DeserialiseFailure m ByteString
-> Peer KeepAlive 'AsServer 'NonPipelined 'StClient m Int
-> Peer
     KeepAlive (FlipAgency 'AsServer) 'NonPipelined 'StClient m Int
-> m (Int, Int)
forall ps (pr :: PeerRole) (st :: ps) failure bytes (m :: * -> *) a
       b.
(MonadAsync m, MonadThrow m, ShowProxy ps,
 forall (st' :: ps) stok. (stok ~ StateToken st') => Show stok,
 Show 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 m (Channel m ByteString, Channel m ByteString)
forall (m :: * -> *) a. MonadSTM m => m (Channel m a, Channel m a)
createConnectedChannels
                                Tracer m (Role, TraceSendRecv KeepAlive)
forall (m :: * -> *) a. Applicative m => Tracer m a
nullTracer
                                Codec KeepAlive DeserialiseFailure m ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2
                                Peer KeepAlive 'AsServer 'NonPipelined 'StClient m Int
server Peer KeepAlive (FlipAgency 'AsServer) 'NonPipelined 'StClient m Int
Client KeepAlive 'NonPipelined 'StClient m Int
client
    return ((s, c) === (n, foldr (.) id (replicate n f) 0))
  where
    server :: Peer KeepAlive 'AsServer 'NonPipelined 'StClient m Int
server = KeepAliveServer m Int
-> Peer KeepAlive 'AsServer 'NonPipelined 'StClient m Int
forall (m :: * -> *) a.
Functor m =>
KeepAliveServer m a -> Server KeepAlive 'NonPipelined 'StClient m a
keepAliveServerPeer KeepAliveServer m Int
forall (m :: * -> *). Applicative m => KeepAliveServer m Int
keepAliveServerCount
    client :: Client KeepAlive 'NonPipelined 'StClient m Int
client = KeepAliveClient m Int
-> Client KeepAlive 'NonPipelined 'StClient m Int
forall (m :: * -> *) a.
MonadThrow m =>
KeepAliveClient m a -> Client KeepAlive 'NonPipelined 'StClient m a
keepAliveClientPeer ((Int -> Int) -> Int -> Int -> KeepAliveClient m Int
forall acc (m :: * -> *).
Monad m =>
(acc -> acc) -> acc -> Int -> KeepAliveClient m acc
keepAliveClientApply Int -> Int
f Int
0 Int
n)

prop_channel_ST :: (Int -> Int)
                -> NonNegative Int
                -> Property
prop_channel_ST :: (Int -> Int) -> NonNegative Int -> Property
prop_channel_ST Int -> Int
f (NonNegative Int
n) =
    (forall s. IOSim s Property) -> Property
forall a. (forall s. IOSim s a) -> a
runSimOrThrow ((Int -> Int) -> Int -> IOSim s Property
forall (m :: * -> *).
(MonadST m, MonadSTM m, MonadAsync m, MonadCatch m) =>
(Int -> Int) -> Int -> m Property
prop_channel Int -> Int
f Int
n)

prop_channel_IO :: (Int -> Int)
                -> NonNegative Int
                -> Property
prop_channel_IO :: (Int -> Int) -> NonNegative Int -> Property
prop_channel_IO Int -> Int
f (NonNegative Int
n) =
    IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty ((Int -> Int) -> Int -> IO Property
forall (m :: * -> *).
(MonadST m, MonadSTM m, MonadAsync m, MonadCatch m) =>
(Int -> Int) -> Int -> m Property
prop_channel Int -> Int
f Int
n)


--
-- Codec tests
--

instance Arbitrary (AnyMessage KeepAlive) where
  arbitrary :: Gen (AnyMessage KeepAlive)
arbitrary = do
    c <- Gen Word16
forall a. Arbitrary a => Gen a
arbitrary
    oneof
      [ pure $ AnyMessage (MsgKeepAlive $ Cookie c)
      , pure $ AnyMessage (MsgKeepAliveResponse $ Cookie c)
      , pure $ AnyMessage MsgDone
      ]

instance Eq (AnyMessage KeepAlive) where
    AnyMessage (MsgKeepAlive Cookie
cookieA)         == :: AnyMessage KeepAlive -> AnyMessage KeepAlive -> Bool
== AnyMessage (MsgKeepAlive Cookie
cookieB)         = Cookie
cookieA Cookie -> Cookie -> Bool
forall a. Eq a => a -> a -> Bool
== Cookie
cookieB
    AnyMessage (MsgKeepAliveResponse Cookie
cookieA) == AnyMessage (MsgKeepAliveResponse Cookie
cookieB) = Cookie
cookieA Cookie -> Cookie -> Bool
forall a. Eq a => a -> a -> Bool
== Cookie
cookieB
    AnyMessage Message KeepAlive st st'
R:MessageKeepAlivefromto st st'
MsgDone                        == AnyMessage Message KeepAlive st st'
R:MessageKeepAlivefromto st st'
MsgDone                        = Bool
True
    AnyMessage KeepAlive
_ == AnyMessage KeepAlive
_ = Bool
False

prop_codec_v2 :: AnyMessage KeepAlive -> Bool
prop_codec_v2 :: AnyMessage KeepAlive -> Bool
prop_codec_v2 AnyMessage KeepAlive
msg =
    (forall s. ST s Bool) -> Bool
forall a. (forall s. ST s a) -> a
runST (Codec KeepAlive DeserialiseFailure (ST s) ByteString
-> AnyMessage KeepAlive -> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
Codec ps failure m bytes -> AnyMessage ps -> m Bool
prop_codecM Codec KeepAlive DeserialiseFailure (ST s) ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 AnyMessage KeepAlive
msg)

prop_codec_v2_splits2 :: AnyMessage KeepAlive -> Bool
prop_codec_v2_splits2 :: AnyMessage KeepAlive -> Bool
prop_codec_v2_splits2 AnyMessage KeepAlive
msg =
    (forall s. ST s Bool) -> Bool
forall a. (forall s. ST s a) -> a
runST ((ByteString -> [[ByteString]])
-> Codec KeepAlive DeserialiseFailure (ST s) ByteString
-> AnyMessage KeepAlive
-> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
(bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessage ps -> m Bool
prop_codec_splitsM ByteString -> [[ByteString]]
splits2 Codec KeepAlive DeserialiseFailure (ST s) ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 AnyMessage KeepAlive
msg)

prop_codec_v2_splits3 :: AnyMessage KeepAlive -> Bool
prop_codec_v2_splits3 :: AnyMessage KeepAlive -> Bool
prop_codec_v2_splits3 AnyMessage KeepAlive
msg =
    (forall s. ST s Bool) -> Bool
forall a. (forall s. ST s a) -> a
runST ((ByteString -> [[ByteString]])
-> Codec KeepAlive DeserialiseFailure (ST s) ByteString
-> AnyMessage KeepAlive
-> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
(bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessage ps -> m Bool
prop_codec_splitsM ByteString -> [[ByteString]]
splits3 Codec KeepAlive DeserialiseFailure (ST s) ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 AnyMessage KeepAlive
msg)

prop_codec_v2_valid_cbor :: AnyMessage KeepAlive -> Property
prop_codec_v2_valid_cbor :: AnyMessage KeepAlive -> Property
prop_codec_v2_valid_cbor AnyMessage KeepAlive
msg =
    Codec KeepAlive DeserialiseFailure IO ByteString
-> AnyMessage KeepAlive -> Property
forall ps.
Codec ps DeserialiseFailure IO ByteString
-> AnyMessage ps -> Property
prop_codec_valid_cbor_encoding Codec KeepAlive DeserialiseFailure IO ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 AnyMessage KeepAlive
msg

prop_byteLimits :: AnyMessage KeepAlive
                -> Bool
prop_byteLimits :: AnyMessage KeepAlive -> Bool
prop_byteLimits (AnyMessage (Message KeepAlive st st'
msg :: Message KeepAlive st st')) =
        ByteString -> Word
dataSize (Message KeepAlive st st' -> ByteString
forall (st :: KeepAlive) (st' :: KeepAlive).
(StateTokenI st, IsActiveState st (StateAgency st)) =>
Message KeepAlive st st' -> ByteString
encode Message KeepAlive st st'
msg)
     Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
<= SingKeepAlive st -> Word
forall (st :: KeepAlive).
IsActiveState st (StateAgency st) =>
SingKeepAlive st -> Word
sizeLimitForState (StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken :: StateToken st)
  where
    Codec { forall (st :: KeepAlive) (st' :: KeepAlive).
(StateTokenI st, IsActiveState st (StateAgency st)) =>
Message KeepAlive st st' -> ByteString
encode :: forall (st :: KeepAlive) (st' :: KeepAlive).
(StateTokenI st, IsActiveState st (StateAgency st)) =>
Message KeepAlive st st' -> ByteString
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   Message ps st st' -> bytes
encode } = Codec KeepAlive DeserialiseFailure IO ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 :: Codec KeepAlive CBOR.DeserialiseFailure IO ByteString
    ProtocolSizeLimits { forall (st :: KeepAlive).
IsActiveState st (StateAgency st) =>
StateToken st -> Word
sizeLimitForState :: forall (st :: KeepAlive).
IsActiveState st (StateAgency st) =>
StateToken st -> Word
sizeLimitForState :: forall ps bytes.
ProtocolSizeLimits ps bytes
-> forall (st :: ps). ActiveState st => StateToken st -> Word
sizeLimitForState, ByteString -> Word
dataSize :: ByteString -> Word
dataSize :: forall ps bytes. ProtocolSizeLimits ps bytes -> bytes -> Word
dataSize } = (ByteString -> Word) -> ProtocolSizeLimits KeepAlive ByteString
forall bytes. (bytes -> Word) -> ProtocolSizeLimits KeepAlive bytes
byteLimitsKeepAlive (Int64 -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Word) -> (ByteString -> Int64) -> ByteString -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length)