{-# 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 (..)
, Message (..)
, ClientHasAgency (..)
, ServerHasAgency (..)
, NobodyHasAgency (..)
, 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 (..))
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"
data RefuseReason vNumber
= VersionMismatch [vNumber] [Int]
| HandshakeDecodeError vNumber Text
| 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
MsgProposeVersions
:: Map vNumber vParams
-> Message (Handshake vNumber vParams) StPropose StConfirm
MsgReplyVersions
:: Map vNumber vParams
-> Message (Handshake vNumber vParams) StConfirm StDone
MsgQueryReply
:: Map vNumber vParams
-> Message (Handshake vNumber vParams) StConfirm StDone
MsgAcceptVersion
:: vNumber
-> vParams
-> Message (Handshake vNumber vParams) StConfirm StDone
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
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"
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)
data HandshakeResult r vNumber vData
= HandshakeNegotiationResult r vNumber vData
| HandshakeQueryResult (Map vNumber (Either Text vData))
instance (Typeable vNumber, Show vNumber)
=> Exception (HandshakeProtocolError vNumber)