{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

module Ouroboros.Network.Protocol.Handshake.Type
  ( -- * Handshake Protocol
    Handshake (..)
  , Message (..)
  , ClientHasAgency (..)
  , ServerHasAgency (..)
  , NobodyHasAgency (..)
    -- $simultanous-open
  , RefuseReason (..)
  , HandshakeProtocolError (..)
  , HandshakeResult (..)
  ) where


import Control.Exception
import Data.Map (Map)
import Data.Text (Text)
import Data.Typeable (Typeable)

import Control.DeepSeq
import GHC.Generics
import Network.TypedProtocol.Core
import Ouroboros.Network.Util.ShowProxy (ShowProxy (..))

-- |
-- The handshake mini-protocol is used initially to agree the version and
-- associated parameters of the protocol to use for all subsequent
-- communication.
--
data Handshake vNumber vParams where
    StPropose :: Handshake vNumber vParams
    StConfirm :: Handshake vNumber vParams
    StDone    :: Handshake vNumber vParams

instance ShowProxy (Handshake vNumber vParams) where
    showProxy :: Proxy (Handshake vNumber vParams) -> String
showProxy Proxy (Handshake vNumber vParams)
_ = String
"Handshake"

-- |
-- Reasons by which a server can refuse proposed version.
--
data RefuseReason vNumber
  -- | All of the prosed versions where not known to the server.
  -- Since the server sends all versions that it can knows about, some of them
  -- we might not be able to decode, so we include raw tags @[Int]@.
  --
  = VersionMismatch [vNumber] [Int]

  -- | The server failed to decode version parameters.
  --
  | HandshakeDecodeError vNumber Text

  -- | The server refused to run the proposed version parameters
  --
  | Refused vNumber Text
  deriving (RefuseReason vNumber -> RefuseReason vNumber -> Bool
(RefuseReason vNumber -> RefuseReason vNumber -> Bool)
-> (RefuseReason vNumber -> RefuseReason vNumber -> Bool)
-> Eq (RefuseReason vNumber)
forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
== :: RefuseReason vNumber -> RefuseReason vNumber -> Bool
$c/= :: forall vNumber.
Eq vNumber =>
RefuseReason vNumber -> RefuseReason vNumber -> Bool
/= :: RefuseReason vNumber -> RefuseReason vNumber -> Bool
Eq, Int -> RefuseReason vNumber -> ShowS
[RefuseReason vNumber] -> ShowS
RefuseReason vNumber -> String
(Int -> RefuseReason vNumber -> ShowS)
-> (RefuseReason vNumber -> String)
-> ([RefuseReason vNumber] -> ShowS)
-> Show (RefuseReason vNumber)
forall vNumber.
Show vNumber =>
Int -> RefuseReason vNumber -> ShowS
forall vNumber. Show vNumber => [RefuseReason vNumber] -> ShowS
forall vNumber. Show vNumber => RefuseReason vNumber -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall vNumber.
Show vNumber =>
Int -> RefuseReason vNumber -> ShowS
showsPrec :: Int -> RefuseReason vNumber -> ShowS
$cshow :: forall vNumber. Show vNumber => RefuseReason vNumber -> String
show :: RefuseReason vNumber -> String
$cshowList :: forall vNumber. Show vNumber => [RefuseReason vNumber] -> ShowS
showList :: [RefuseReason vNumber] -> ShowS
Show, (forall x. RefuseReason vNumber -> Rep (RefuseReason vNumber) x)
-> (forall x. Rep (RefuseReason vNumber) x -> RefuseReason vNumber)
-> Generic (RefuseReason vNumber)
forall x. Rep (RefuseReason vNumber) x -> RefuseReason vNumber
forall x. RefuseReason vNumber -> Rep (RefuseReason vNumber) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall vNumber x.
Rep (RefuseReason vNumber) x -> RefuseReason vNumber
forall vNumber x.
RefuseReason vNumber -> Rep (RefuseReason vNumber) x
$cfrom :: forall vNumber x.
RefuseReason vNumber -> Rep (RefuseReason vNumber) x
from :: forall x. RefuseReason vNumber -> Rep (RefuseReason vNumber) x
$cto :: forall vNumber x.
Rep (RefuseReason vNumber) x -> RefuseReason vNumber
to :: forall x. Rep (RefuseReason vNumber) x -> RefuseReason vNumber
Generic, RefuseReason vNumber -> ()
(RefuseReason vNumber -> ()) -> NFData (RefuseReason vNumber)
forall vNumber. NFData vNumber => RefuseReason vNumber -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall vNumber. NFData vNumber => RefuseReason vNumber -> ()
rnf :: RefuseReason vNumber -> ()
NFData)

instance (Typeable vNumber, Show vNumber) => Exception (RefuseReason vNumber)


instance Protocol (Handshake vNumber vParams) where

    data Message (Handshake vNumber vParams) from to where

      -- |
      -- Propose versions together with version parameters.  It must be
      -- encoded to a sorted list.
      --
      MsgProposeVersions
        :: Map vNumber vParams
        -> Message (Handshake vNumber vParams) StPropose StConfirm

      -- |
      -- `MsgReplyVersions` received as a response to 'MsgProposeVersions'.  It
      -- is not supported to explicitly send this message. It can only be
      -- received as a copy of 'MsgProposeVersions' in a simultaneous open
      -- scenario.
      --
      MsgReplyVersions
        :: Map vNumber vParams
        -> Message (Handshake vNumber vParams) StConfirm StDone

      -- |
      -- `MsgQueryReply` received as a response to 'MsgProposeVersions'.  It
      -- is only sent when a version query was received. This will cause the
      -- connection to terminate.
      --
      MsgQueryReply
        :: Map vNumber vParams
        -> Message (Handshake vNumber vParams) StConfirm StDone

      -- |
      -- The remote end decides which version to use and sends chosen version.
      -- The server is allowed to modify version parameters.
      --
      MsgAcceptVersion
        :: vNumber
        -> vParams
        -> Message (Handshake vNumber vParams) StConfirm StDone

      -- |
      -- or it refuses to run any version,
      --
      MsgRefuse
        :: RefuseReason vNumber
        -> Message (Handshake vNumber vParams) StConfirm StDone

    data ClientHasAgency st where
      TokPropose :: ClientHasAgency StPropose

    data ServerHasAgency st where
      TokConfirm :: ServerHasAgency StConfirm

    data NobodyHasAgency st where
      TokDone    :: NobodyHasAgency StDone

    exclusionLemma_ClientAndServerHaveAgency :: forall (st :: Handshake vNumber vParams).
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st
R:ClientHasAgencyHandshakest k k vNumber vParams st
TokPropose ServerHasAgency st
tok = case ServerHasAgency st
tok of {}
    exclusionLemma_NobodyAndClientHaveAgency :: forall (st :: Handshake vNumber vParams).
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st
R:NobodyHasAgencyHandshakest k k vNumber vParams st
TokDone    ClientHasAgency st
tok = case ClientHasAgency st
tok of {}
    exclusionLemma_NobodyAndServerHaveAgency :: forall (st :: Handshake vNumber vParams).
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st
R:NobodyHasAgencyHandshakest k k vNumber vParams st
TokDone    ServerHasAgency st
tok = case ServerHasAgency st
tok of {}

instance forall vNumber vParams (st :: Handshake vNumber vParams). NFData (ClientHasAgency st) where
  rnf :: ClientHasAgency st -> ()
rnf ClientHasAgency st
R:ClientHasAgencyHandshakest k k vNumber vParams st
TokPropose = ()

instance forall vNumber vParams (st :: Handshake vNumber vParams). NFData (ServerHasAgency st) where
  rnf :: ServerHasAgency st -> ()
rnf ServerHasAgency st
R:ServerHasAgencyHandshakest k k vNumber vParams st
TokConfirm = ()

instance forall vNumber vParams (st :: Handshake vNumber vParams). NFData (NobodyHasAgency st) where
  rnf :: NobodyHasAgency st -> ()
rnf NobodyHasAgency st
R:NobodyHasAgencyHandshakest k k vNumber vParams st
TokDone = ()

instance forall vNumber vParams (st :: Handshake vNumber vParams) pr. NFData (PeerHasAgency pr st) where
  rnf :: PeerHasAgency pr st -> ()
rnf (ClientAgency ClientHasAgency st
x) = ClientHasAgency st -> ()
forall a. NFData a => a -> ()
rnf ClientHasAgency st
x
  rnf (ServerAgency ServerHasAgency st
x) = ServerHasAgency st -> ()
forall a. NFData a => a -> ()
rnf ServerHasAgency st
x

instance ( NFData vNumber
         , NFData vParams
         ) => NFData (Message (Handshake vNumber vParams) from to) where
  rnf :: Message (Handshake vNumber vParams) from to -> ()
rnf (MsgProposeVersions Map vNumber vParams
m)   = Map vNumber vParams -> ()
forall a. NFData a => a -> ()
rnf Map vNumber vParams
m
  rnf (MsgReplyVersions Map vNumber vParams
m)     = Map vNumber vParams -> ()
forall a. NFData a => a -> ()
rnf Map vNumber vParams
m
  rnf (MsgQueryReply Map vNumber vParams
m)        = Map vNumber vParams -> ()
forall a. NFData a => a -> ()
rnf Map vNumber vParams
m
  rnf (MsgAcceptVersion vNumber
vn vParams
vp) = vNumber -> ()
forall a. NFData a => a -> ()
rnf vNumber
vn () -> () -> ()
forall a b. a -> b -> b
`seq` vParams -> ()
forall a. NFData a => a -> ()
rnf vParams
vp
  rnf (MsgRefuse RefuseReason vNumber
rf)           = RefuseReason vNumber -> ()
forall a. NFData a => a -> ()
rnf RefuseReason vNumber
rf

-- $simultanous-open
--
-- On simultaneous open both sides will send `MsgProposeVersions`, which will be
-- decoded as `MsgReplyVersions`.  It is a terminal message of the protocol.  It
-- is important to stress that in this case both sides will make the choice
-- which version and parameters to pick.  Our algorithm for picking version is
-- symmetric, which ensures that both sides will end up with the same choice.
-- If one side decides to refuse the version it will close the connection,
-- without sending the reason to the other side.

deriving instance (Show vNumber, Show vParams)
    => Show (Message (Handshake vNumber vParams) from to)

instance Show (ClientHasAgency (st :: Handshake vNumber vParams)) where
    show :: ClientHasAgency st -> String
show ClientHasAgency st
R:ClientHasAgencyHandshakest k k vNumber vParams st
TokPropose       = String
"TokPropose"

instance Show (ServerHasAgency (st :: Handshake vNumber vParams)) where
    show :: ServerHasAgency st -> String
show ServerHasAgency st
R:ServerHasAgencyHandshakest k k vNumber vParams st
TokConfirm = String
"TokConfirm"

-- | Extends handshake error @'RefuseReason'@ type, by client specific errors.
--
data HandshakeProtocolError vNumber
  = HandshakeError (RefuseReason vNumber)
  | NotRecognisedVersion vNumber
  | InvalidServerSelection vNumber Text
  | QueryNotSupported
  deriving (HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
(HandshakeProtocolError vNumber
 -> HandshakeProtocolError vNumber -> Bool)
-> (HandshakeProtocolError vNumber
    -> HandshakeProtocolError vNumber -> Bool)
-> Eq (HandshakeProtocolError vNumber)
forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
== :: HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
$c/= :: forall vNumber.
Eq vNumber =>
HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
/= :: HandshakeProtocolError vNumber
-> HandshakeProtocolError vNumber -> Bool
Eq, Int -> HandshakeProtocolError vNumber -> ShowS
[HandshakeProtocolError vNumber] -> ShowS
HandshakeProtocolError vNumber -> String
(Int -> HandshakeProtocolError vNumber -> ShowS)
-> (HandshakeProtocolError vNumber -> String)
-> ([HandshakeProtocolError vNumber] -> ShowS)
-> Show (HandshakeProtocolError vNumber)
forall vNumber.
Show vNumber =>
Int -> HandshakeProtocolError vNumber -> ShowS
forall vNumber.
Show vNumber =>
[HandshakeProtocolError vNumber] -> ShowS
forall vNumber.
Show vNumber =>
HandshakeProtocolError vNumber -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall vNumber.
Show vNumber =>
Int -> HandshakeProtocolError vNumber -> ShowS
showsPrec :: Int -> HandshakeProtocolError vNumber -> ShowS
$cshow :: forall vNumber.
Show vNumber =>
HandshakeProtocolError vNumber -> String
show :: HandshakeProtocolError vNumber -> String
$cshowList :: forall vNumber.
Show vNumber =>
[HandshakeProtocolError vNumber] -> ShowS
showList :: [HandshakeProtocolError vNumber] -> ShowS
Show)

-- | The result of a handshake.
--
data HandshakeResult r vNumber vData
  = HandshakeNegotiationResult r vNumber vData
  | HandshakeQueryResult (Map vNumber (Either Text vData))

instance (Typeable vNumber, Show vNumber)
    => Exception (HandshakeProtocolError vNumber)