{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE NamedFieldPuns  #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns    #-}
module Ouroboros.Network.InboundGovernor.Test.Utils where

import Test.QuickCheck
import Test.QuickCheck.Monoids

import Ouroboros.Network.ConnectionManager.Types
import Ouroboros.Network.InboundGovernor (InboundGovernorTrace (..),
           RemoteSt (..))
import Ouroboros.Network.InboundGovernor qualified as IG
import Ouroboros.Network.Server2 (RemoteTransition, ServerTrace (..))


-- | Pattern synonym which matches either 'RemoteHotEst' or 'RemoteWarmSt'.
--
pattern RemoteEstSt :: RemoteSt
pattern $mRemoteEstSt :: forall {r}. RemoteSt -> ((# #) -> r) -> ((# #) -> r) -> r
RemoteEstSt <- (\ case
                            RemoteSt
RemoteHotSt  -> Bool
True
                            RemoteSt
RemoteWarmSt -> Bool
True
                            RemoteSt
_            -> Bool
False -> True
                        )

{-# COMPLETE RemoteEstSt, RemoteIdleSt, RemoteColdSt #-}


-- | Specification of the transition table of the inbound governor.
--
verifyRemoteTransition :: RemoteTransition -> Bool
verifyRemoteTransition :: RemoteTransition -> Bool
verifyRemoteTransition Transition {Maybe RemoteSt
fromState :: Maybe RemoteSt
fromState :: forall state. Transition' state -> state
fromState, Maybe RemoteSt
toState :: Maybe RemoteSt
toState :: forall state. Transition' state -> state
toState} =
    case (Maybe RemoteSt
fromState, Maybe RemoteSt
toState) of
      -- The initial state must be 'RemoteIdleSt'.
      (Maybe RemoteSt
Nothing,           Just RemoteSt
RemoteIdleSt) -> Bool
True

      --
      -- Promotions
      --

      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteEstSt)  -> Bool
True
      (Just RemoteSt
RemoteColdSt, Just RemoteSt
RemoteEstSt)  -> Bool
True
      (Just RemoteSt
RemoteWarmSt, Just RemoteSt
RemoteHotSt)  -> Bool
True

      --
      -- Demotions
      --

      (Just RemoteSt
RemoteHotSt,  Just RemoteSt
RemoteWarmSt) -> Bool
True
      -- demotion to idle state can happen from any established state
      (Just RemoteSt
RemoteEstSt,  Just RemoteSt
RemoteIdleSt) -> Bool
True
      -- demotion to cold can only be done from idle state; We explicitly rule
      -- out demotions to cold from warm or hot states.
      (Just RemoteSt
RemoteEstSt,  Just RemoteSt
RemoteColdSt) -> Bool
False
      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteColdSt) -> Bool
True
      -- normal termination (if outbound side is not using that connection)
      (Just RemoteSt
RemoteIdleSt, Maybe RemoteSt
Nothing)           -> Bool
True
      -- This transition corresponds to connection manager's:
      -- @
      --   Commit^{Duplex}_{Local} : OutboundIdleState Duplex
      --                           → TerminatingState
      -- @
      (Just RemoteSt
RemoteColdSt, Maybe RemoteSt
Nothing)           -> Bool
True
      -- any of the mini-protocols errored
      (Just RemoteSt
RemoteEstSt, Maybe RemoteSt
Nothing)            -> Bool
True

      --
      -- We are conservative to name all the identity transitions.
      --

      -- This might happen if starting any of the responders errored.
      (Maybe RemoteSt
Nothing,           Maybe RemoteSt
Nothing)           -> Bool
True
      -- @RemoteWarmSt → RemoteWarmSt@, @RemoteIdleSt → RemoteIdleSt@ and
      -- @RemoteColdSt → RemoteColdSt@ transition are observed if a hot or
      -- warm protocol terminates (which triggers @RemoteEstSt -> RemoteWarmSt@)
      (Just RemoteSt
RemoteWarmSt, Just RemoteSt
RemoteWarmSt) -> Bool
True
      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteIdleSt) -> Bool
True
      (Just RemoteSt
RemoteColdSt, Just RemoteSt
RemoteColdSt) -> Bool
True

      (Maybe RemoteSt
_,                 Maybe RemoteSt
_)                 -> Bool
False



-- | Maps each valid remote transition into one number. Collapses all invalid
-- transition into a single number.
--
-- NOTE: Should be in sync with 'verifyRemoteTransition'
--
validRemoteTransitionMap :: RemoteTransition -> (Int, String)
validRemoteTransitionMap :: RemoteTransition -> (Int, String)
validRemoteTransitionMap t :: RemoteTransition
t@Transition { Maybe RemoteSt
fromState :: forall state. Transition' state -> state
fromState :: Maybe RemoteSt
fromState, Maybe RemoteSt
toState :: forall state. Transition' state -> state
toState :: Maybe RemoteSt
toState } =
    case (Maybe RemoteSt
fromState, Maybe RemoteSt
toState) of
      (Maybe RemoteSt
Nothing          , Just RemoteSt
RemoteIdleSt) -> (Int
00, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteEstSt)  -> (Int
01, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteColdSt, Just RemoteSt
RemoteEstSt)  -> (Int
02, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteWarmSt, Just RemoteSt
RemoteHotSt)  -> (Int
03, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteHotSt , Just RemoteSt
RemoteWarmSt) -> (Int
04, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteEstSt , Just RemoteSt
RemoteIdleSt) -> (Int
05, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteColdSt) -> (Int
06, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteIdleSt, Maybe RemoteSt
Nothing)           -> (Int
07, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteColdSt, Maybe RemoteSt
Nothing)           -> (Int
08, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteEstSt , Maybe RemoteSt
Nothing)           -> (Int
09, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Maybe RemoteSt
Nothing          , Maybe RemoteSt
Nothing)           -> (Int
10, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteWarmSt, Just RemoteSt
RemoteWarmSt) -> (Int
11, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteIdleSt, Just RemoteSt
RemoteIdleSt) -> (Int
12, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Just RemoteSt
RemoteColdSt, Just RemoteSt
RemoteColdSt) -> (Int
13, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)
      (Maybe RemoteSt
_                , Maybe RemoteSt
_)                 -> (Int
99, RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
t)

-- | List of all valid transition's names.
--
-- NOTE: Should be in sync with 'verifyAbstractTransition'.
--
allValidRemoteTransitionsNames :: [String]
allValidRemoteTransitionsNames :: [String]
allValidRemoteTransitionsNames =
  (RemoteTransition -> String) -> [RemoteTransition] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map RemoteTransition -> String
forall a. Show a => a -> String
show
  [ Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition Maybe RemoteSt
forall a. Maybe a
Nothing             (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteIdleSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteIdleSt) (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteWarmSt)
  -- , Transition (Just RemoteIdleSt) (Just RemoteHotSt)
  -- , Transition (Just RemoteColdSt) (Just RemoteWarmSt)
  -- , Transition (Just RemoteColdSt) (Just RemoteHotSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteWarmSt) (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteHotSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteHotSt ) (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteWarmSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteWarmSt) (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteIdleSt)
  -- , Transition (Just RemoteHotSt)  (Just RemoteIdleSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteIdleSt) (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteColdSt)
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteIdleSt) Maybe RemoteSt
forall a. Maybe a
Nothing
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteColdSt) Maybe RemoteSt
forall a. Maybe a
Nothing
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteWarmSt) Maybe RemoteSt
forall a. Maybe a
Nothing
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition (RemoteSt -> Maybe RemoteSt
forall a. a -> Maybe a
Just RemoteSt
RemoteHotSt)  Maybe RemoteSt
forall a. Maybe a
Nothing
  , Maybe RemoteSt -> Maybe RemoteSt -> RemoteTransition
forall state. state -> state -> Transition' state
Transition Maybe RemoteSt
forall a. Maybe a
Nothing             Maybe RemoteSt
forall a. Maybe a
Nothing
  -- , Transition (Just RemoteWarmSt) (Just RemoteWarmSt)
  -- , Transition (Just RemoteIdleSt) (Just RemoteIdleSt)
  -- , Transition (Just RemoteColdSt) (Just RemoteColdSt)
  ]

-- Assuming all transitions in the transition list are valid, we only need to
-- look at the 'toState' of the current transition and the 'fromState' of the
-- next transition.
verifyRemoteTransitionOrder :: Bool -- ^ Check last transition: useful for
                                    --    distinguish Diffusion layer tests
                                    --    vs non-Diffusion ones.
                            -> [RemoteTransition]
                            -> All
verifyRemoteTransitionOrder :: Bool -> [RemoteTransition] -> All
verifyRemoteTransitionOrder Bool
_ [] = All
forall a. Monoid a => a
mempty
verifyRemoteTransitionOrder Bool
checkLast (RemoteTransition
h:[RemoteTransition]
t) = [RemoteTransition] -> RemoteTransition -> All
go [RemoteTransition]
t RemoteTransition
h
  where
    go :: [RemoteTransition] -> RemoteTransition -> All
    -- All transitions must end in the 'Nothing' (final) state, and since
    -- we assume all transitions are valid we do not have to check the
    -- 'fromState' .
    go :: [RemoteTransition] -> RemoteTransition -> All
go [] (Transition Maybe RemoteSt
_ Maybe RemoteSt
Nothing) = All
forall a. Monoid a => a
mempty
    go [] tr :: RemoteTransition
tr@(Transition Maybe RemoteSt
_ Maybe RemoteSt
_)          =
      Property -> All
forall p. Testable p => p -> All
All
        (Property -> All) -> Property -> All
forall a b. (a -> b) -> a -> b
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
            (String
"\nUnexpected last transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
tr)
            (Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Bool
not Bool
checkLast))
    -- All transitions have to be in a correct order, which means that the
    -- current state we are looking at (current toState) needs to be equal to
    -- the next 'fromState', in order for the transition chain to be correct.
    go (next :: RemoteTransition
next@(Transition Maybe RemoteSt
nextFromState Maybe RemoteSt
_) : [RemoteTransition]
ts)
        curr :: RemoteTransition
curr@(Transition Maybe RemoteSt
_ Maybe RemoteSt
currToState) =
         Property -> All
forall p. Testable p => p -> All
All
           (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              (String
"\nUnexpected transition order!\nWent from: "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
curr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nto: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RemoteTransition -> String
forall a. Show a => a -> String
show RemoteTransition
next)
              (Bool -> Property
forall prop. Testable prop => prop -> Property
property (Maybe RemoteSt
currToState Maybe RemoteSt -> Maybe RemoteSt -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe RemoteSt
nextFromState)))
         All -> All -> All
forall a. Semigroup a => a -> a -> a
<> [RemoteTransition] -> RemoteTransition -> All
go [RemoteTransition]
ts RemoteTransition
next

remoteStrIsFinalTransition :: Transition' (Maybe RemoteSt) -> Bool
remoteStrIsFinalTransition :: RemoteTransition -> Bool
remoteStrIsFinalTransition (Transition Maybe RemoteSt
_ Maybe RemoteSt
Nothing) = Bool
True
remoteStrIsFinalTransition RemoteTransition
_                      = Bool
False

inboundGovernorTraceMap :: InboundGovernorTrace ntnAddr -> String
inboundGovernorTraceMap :: forall ntnAddr. InboundGovernorTrace ntnAddr -> String
inboundGovernorTraceMap (TrNewConnection Provenance
p ConnectionId ntnAddr
_)            =
  String
"TrNewConnection " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Provenance -> String
forall a. Show a => a -> String
show Provenance
p
inboundGovernorTraceMap (TrResponderRestarted ConnectionId ntnAddr
_ MiniProtocolNum
mpn)         =
  String
"TrResponderRestarted " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MiniProtocolNum -> String
forall a. Show a => a -> String
show MiniProtocolNum
mpn
inboundGovernorTraceMap (TrResponderStartFailure ConnectionId ntnAddr
_ MiniProtocolNum
mpn SomeException
se)   =
  String
"TrResponderStartFailure " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MiniProtocolNum -> String
forall a. Show a => a -> String
show MiniProtocolNum
mpn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
se
inboundGovernorTraceMap (TrResponderErrored ConnectionId ntnAddr
_ MiniProtocolNum
mpn SomeException
se)        =
  String
"TrResponderErrored " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MiniProtocolNum -> String
forall a. Show a => a -> String
show MiniProtocolNum
mpn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
se
inboundGovernorTraceMap (TrResponderStarted ConnectionId ntnAddr
_ MiniProtocolNum
mpn)           =
  String
"TrResponderStarted " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MiniProtocolNum -> String
forall a. Show a => a -> String
show MiniProtocolNum
mpn
inboundGovernorTraceMap (TrResponderTerminated ConnectionId ntnAddr
_ MiniProtocolNum
mpn)        =
  String
"TrResponderTerminated " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MiniProtocolNum -> String
forall a. Show a => a -> String
show MiniProtocolNum
mpn
inboundGovernorTraceMap (TrPromotedToWarmRemote ConnectionId ntnAddr
_ OperationResult AbstractState
ora)        =
  String
"TrPromotedToWarmRemote " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OperationResult AbstractState -> String
forall a. Show a => a -> String
show OperationResult AbstractState
ora
inboundGovernorTraceMap (TrPromotedToHotRemote ConnectionId ntnAddr
_)            =
  String
"TrPromotedToHotRemote"
inboundGovernorTraceMap (TrDemotedToWarmRemote ConnectionId ntnAddr
_)            =
  String
"TrDemotedToWarmRemote"
inboundGovernorTraceMap (TrDemotedToColdRemote ConnectionId ntnAddr
_ OperationResult DemotedToColdRemoteTr
ora)         =
  String
"TrDemotedToColdRemote " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OperationResult DemotedToColdRemoteTr -> String
forall a. Show a => a -> String
show OperationResult DemotedToColdRemoteTr
ora
inboundGovernorTraceMap (TrWaitIdleRemote ConnectionId ntnAddr
_ OperationResult AbstractState
ora)              =
  String
"TrWaitIdleRemote " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OperationResult AbstractState -> String
forall a. Show a => a -> String
show OperationResult AbstractState
ora
inboundGovernorTraceMap (TrMuxCleanExit ConnectionId ntnAddr
_)                   =
  String
"TrMuxCleanExit"
inboundGovernorTraceMap (TrMuxErrored ConnectionId ntnAddr
_ SomeException
se)                  =
  String
"TrMuxErrored " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
se
inboundGovernorTraceMap (TrInboundGovernorCounters InboundGovernorCounters
_)       =
  String
"TrInboundGovernorCounters"
inboundGovernorTraceMap (TrRemoteState Map (ConnectionId ntnAddr) RemoteSt
_)                   =
  String
"TrRemoteState"
inboundGovernorTraceMap (IG.TrUnexpectedlyFalseAssertion IGAssertionLocation ntnAddr
_) =
  String
"TrUnexpectedlyFalseAssertion"
inboundGovernorTraceMap (TrInboundGovernorError SomeException
se)           =
  String
"TrInboundGovernorError " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
se
inboundGovernorTraceMap TrMaturedConnections {}            =
  String
"TrMaturedConnections"
inboundGovernorTraceMap TrInactive {}                      =
  String
"TrMaturedConnections"


serverTraceMap :: Show ntnAddr => ServerTrace ntnAddr -> String
serverTraceMap :: forall ntnAddr. Show ntnAddr => ServerTrace ntnAddr -> String
serverTraceMap (TrAcceptConnection ntnAddr
_)     = String
"TrAcceptConnection"
serverTraceMap st :: ServerTrace ntnAddr
st@(TrAcceptError SomeException
_)       = ServerTrace ntnAddr -> String
forall a. Show a => a -> String
show ServerTrace ntnAddr
st
serverTraceMap st :: ServerTrace ntnAddr
st@(TrAcceptPolicyTrace AcceptConnectionsPolicyTrace
_) = ServerTrace ntnAddr -> String
forall a. Show a => a -> String
show ServerTrace ntnAddr
st
serverTraceMap (TrServerStarted [ntnAddr]
_)        = String
"TrServerStarted"
serverTraceMap st :: ServerTrace ntnAddr
st@ServerTrace ntnAddr
TrServerStopped         = ServerTrace ntnAddr -> String
forall a. Show a => a -> String
show ServerTrace ntnAddr
st
serverTraceMap st :: ServerTrace ntnAddr
st@(TrServerError SomeException
_)       = ServerTrace ntnAddr -> String
forall a. Show a => a -> String
show ServerTrace ntnAddr
st