{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE NamedFieldPuns    #-}
{-# LANGUAGE TypeApplications  #-}

{-# 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 -> (AnyMessageAndAgency KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2"            AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2
  , TestName -> (AnyMessageAndAgency KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 2-splits"   AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits2
  , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 3-splits"   (Int -> (AnyMessageAndAgency KeepAlive -> Bool) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
33 AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits3)
  , TestName -> (AnyMessageAndAgency KeepAlive -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"codec v2 valid CBOR" AnyMessageAndAgency KeepAlive -> Property
prop_codec_v2_valid_cbor
  , TestName -> (AnyMessageAndAgency KeepAlive -> Bool) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"byteLimits"          AnyMessageAndAgency 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 'StClient (IOSim s) Int
-> Peer KeepAlive (FlipAgency 'AsServer) 'StClient (IOSim s) Int
-> IOSim s (Int, Int, TerminalStates KeepAlive)
forall ps (pr :: PeerRole) (st :: ps) (m :: * -> *) a b.
(Monad m, Protocol ps) =>
Peer ps pr st m a
-> Peer ps (FlipAgency pr) st m b -> m (a, b, TerminalStates ps)
connect
            (KeepAliveServer (IOSim s) Int
-> Peer KeepAlive 'AsServer 'StClient (IOSim s) Int
forall (m :: * -> *) a.
Functor m =>
KeepAliveServer m a -> Peer KeepAlive 'AsServer 'StClient m a
keepAliveServerPeer   KeepAliveServer (IOSim s) Int
forall (m :: * -> *). Applicative m => KeepAliveServer m Int
keepAliveServerCount)
            (KeepAliveClient (IOSim s) Int
-> Peer KeepAlive 'AsClient 'StClient (IOSim s) Int
forall (m :: * -> *) a.
MonadThrow m =>
KeepAliveClient m a -> Peer KeepAlive 'AsClient 'StClient m a
keepAliveClientPeer (KeepAliveClient (IOSim s) Int
 -> Peer KeepAlive 'AsClient 'StClient (IOSim s) Int)
-> KeepAliveClient (IOSim s) Int
-> Peer KeepAlive 'AsClient '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 NobodyHasAgency st
R:NobodyHasAgencyKeepAlivest st
TokDone NobodyHasAgency st
R:NobodyHasAgencyKeepAlivest 'StDone
TokDone) ->
          (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 'StClient m Int
-> Peer KeepAlive (FlipAgency 'AsServer) 'StClient m Int
-> m (Int, Int)
forall (m :: * -> *) failure ps bytes (pr :: PeerRole) (st :: ps) a
       b.
(MonadAsync m, MonadCatch m, Show failure,
 forall (st' :: ps). Show (ClientHasAgency st'),
 forall (st' :: ps). Show (ServerHasAgency st'), ShowProxy ps) =>
m (Channel m bytes, Channel m bytes)
-> Tracer m (Role, TraceSendRecv ps)
-> Codec ps failure m bytes
-> Peer ps pr st m a
-> Peer ps (FlipAgency pr) 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 'StClient m Int
server Peer KeepAlive (FlipAgency 'AsServer) 'StClient m Int
Peer KeepAlive 'AsClient 'StClient m Int
client
    return ((s, c) === (n, foldr (.) id (replicate n f) 0))
  where
    server :: Peer KeepAlive 'AsServer 'StClient m Int
server = KeepAliveServer m Int -> Peer KeepAlive 'AsServer 'StClient m Int
forall (m :: * -> *) a.
Functor m =>
KeepAliveServer m a -> Peer KeepAlive 'AsServer 'StClient m a
keepAliveServerPeer KeepAliveServer m Int
forall (m :: * -> *). Applicative m => KeepAliveServer m Int
keepAliveServerCount
    client :: Peer KeepAlive 'AsClient 'StClient m Int
client = KeepAliveClient m Int -> Peer KeepAlive 'AsClient 'StClient m Int
forall (m :: * -> *) a.
MonadThrow m =>
KeepAliveClient m a -> Peer KeepAlive 'AsClient '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 (AnyMessageAndAgency KeepAlive) where
  arbitrary :: Gen (AnyMessageAndAgency KeepAlive)
arbitrary = do
    c <- Gen Word16
forall a. Arbitrary a => Gen a
arbitrary
    oneof
      [ pure $ AnyMessageAndAgency (ClientAgency TokClient) (MsgKeepAlive $ Cookie c)
      , pure $ AnyMessageAndAgency (ServerAgency TokServer) (MsgKeepAliveResponse $ Cookie c)
      , pure $ AnyMessageAndAgency (ClientAgency TokClient) 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 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2 AnyMessageAndAgency KeepAlive
msg =
    (forall s. ST s Bool) -> Bool
forall a. (forall s. ST s a) -> a
runST (Codec KeepAlive DeserialiseFailure (ST s) ByteString
-> AnyMessageAndAgency KeepAlive -> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
Codec ps failure m bytes -> AnyMessageAndAgency ps -> m Bool
prop_codecM Codec KeepAlive DeserialiseFailure (ST s) ByteString
forall (m :: * -> *).
MonadST m =>
Codec KeepAlive DeserialiseFailure m ByteString
codecKeepAlive_v2 AnyMessageAndAgency KeepAlive
msg)

prop_codec_v2_splits2 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits2 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits2 AnyMessageAndAgency 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
-> AnyMessageAndAgency KeepAlive
-> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
(bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessageAndAgency 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 AnyMessageAndAgency KeepAlive
msg)

prop_codec_v2_splits3 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits3 :: AnyMessageAndAgency KeepAlive -> Bool
prop_codec_v2_splits3 AnyMessageAndAgency 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
-> AnyMessageAndAgency KeepAlive
-> ST s Bool
forall ps failure (m :: * -> *) bytes.
(Monad m, Eq (AnyMessage ps)) =>
(bytes -> [[bytes]])
-> Codec ps failure m bytes -> AnyMessageAndAgency 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 AnyMessageAndAgency KeepAlive
msg)

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

prop_byteLimits :: AnyMessageAndAgency KeepAlive
                         -> Bool
prop_byteLimits :: AnyMessageAndAgency KeepAlive -> Bool
prop_byteLimits (AnyMessageAndAgency PeerHasAgency pr st
agency Message KeepAlive st st'
msg) =
        ByteString -> Word
dataSize (PeerHasAgency pr st -> Message KeepAlive st st' -> ByteString
forall (pr :: PeerRole) (st :: KeepAlive) (st' :: KeepAlive).
PeerHasAgency pr st -> Message KeepAlive st st' -> ByteString
encode PeerHasAgency pr st
agency Message KeepAlive st st'
msg)
     Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
<= PeerHasAgency pr st -> Word
forall (pr :: PeerRole) (st :: KeepAlive).
PeerHasAgency pr st -> Word
sizeLimitForState PeerHasAgency pr st
agency
  where
    Codec { forall (pr :: PeerRole) (st :: KeepAlive) (st' :: KeepAlive).
PeerHasAgency pr st -> Message KeepAlive st st' -> ByteString
encode :: forall (pr :: PeerRole) (st :: KeepAlive) (st' :: KeepAlive).
PeerHasAgency pr st -> Message KeepAlive st st' -> ByteString
encode :: forall ps failure (m :: * -> *) bytes.
Codec ps failure m bytes
-> forall (pr :: PeerRole) (st :: ps) (st' :: ps).
   PeerHasAgency pr 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 (pr :: PeerRole) (st :: KeepAlive).
PeerHasAgency pr st -> Word
sizeLimitForState :: forall (pr :: PeerRole) (st :: KeepAlive).
PeerHasAgency pr st -> Word
sizeLimitForState :: forall ps bytes.
ProtocolSizeLimits ps bytes
-> forall (pr :: PeerRole) (st :: ps). PeerHasAgency pr 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)