{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Cardano.Protocol.TPraos.Rules.Prtcl (
PRTCL,
State,
PrtclEnv (..),
PrtclState (..),
PrtclPredicateFailure (..),
PredicateFailure,
PrtlSeqFailure (..),
prtlSeqChecks,
) where
import qualified Cardano.Crypto.KES as KES
import qualified Cardano.Crypto.VRF as VRF
import Cardano.Ledger.BaseTypes (
Nonce,
Seed,
ShelleyBase,
UnitInterval,
)
import Cardano.Ledger.Binary (DecCBOR, EncCBOR)
import Cardano.Ledger.Binary.Plain (
FromCBOR (..),
ToCBOR (..),
decodeRecordNamed,
encodeListLen,
)
import Cardano.Ledger.Keys (GenDelegs (..), KeyHash, KeyRole (..))
import Cardano.Ledger.Slot (BlockNo, SlotNo)
import Cardano.Ledger.State (PoolDistr)
import Cardano.Protocol.Crypto
import Cardano.Protocol.TPraos.BHeader (
BHBody (..),
BHeader (..),
LastAppliedBlock (..),
PrevHash,
bhbody,
bnonce,
lastAppliedHash,
)
import Cardano.Protocol.TPraos.Rules.Overlay (OVERLAY, OverlayEnv (..))
import Cardano.Protocol.TPraos.Rules.Updn (UPDN, UpdnEnv (..), UpdnState (..))
import Cardano.Slotting.Slot (WithOrigin (..))
import Control.Monad (unless)
import Control.Monad.Except (MonadError, throwError)
import Control.State.Transition
import Data.Map.Strict (Map)
import Data.Void (Void)
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
data PRTCL c
data PrtclState
= PrtclState
!(Map (KeyHash 'BlockIssuer) Word64)
!Nonce
!Nonce
deriving ((forall x. PrtclState -> Rep PrtclState x)
-> (forall x. Rep PrtclState x -> PrtclState) -> Generic PrtclState
forall x. Rep PrtclState x -> PrtclState
forall x. PrtclState -> Rep PrtclState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrtclState -> Rep PrtclState x
from :: forall x. PrtclState -> Rep PrtclState x
$cto :: forall x. Rep PrtclState x -> PrtclState
to :: forall x. Rep PrtclState x -> PrtclState
Generic, Int -> PrtclState -> ShowS
[PrtclState] -> ShowS
PrtclState -> String
(Int -> PrtclState -> ShowS)
-> (PrtclState -> String)
-> ([PrtclState] -> ShowS)
-> Show PrtclState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrtclState -> ShowS
showsPrec :: Int -> PrtclState -> ShowS
$cshow :: PrtclState -> String
show :: PrtclState -> String
$cshowList :: [PrtclState] -> ShowS
showList :: [PrtclState] -> ShowS
Show, PrtclState -> PrtclState -> Bool
(PrtclState -> PrtclState -> Bool)
-> (PrtclState -> PrtclState -> Bool) -> Eq PrtclState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrtclState -> PrtclState -> Bool
== :: PrtclState -> PrtclState -> Bool
$c/= :: PrtclState -> PrtclState -> Bool
/= :: PrtclState -> PrtclState -> Bool
Eq)
instance EncCBOR PrtclState
instance ToCBOR PrtclState where
toCBOR :: PrtclState -> Encoding
toCBOR (PrtclState Map (KeyHash 'BlockIssuer) Word64
m Nonce
n1 Nonce
n2) =
[Encoding] -> Encoding
forall a. Monoid a => [a] -> a
mconcat
[ Word -> Encoding
encodeListLen Word
3
, Map (KeyHash 'BlockIssuer) Word64 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Map (KeyHash 'BlockIssuer) Word64
m
, Nonce -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n1
, Nonce -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Nonce
n2
]
instance DecCBOR PrtclState
instance FromCBOR PrtclState where
fromCBOR :: forall s. Decoder s PrtclState
fromCBOR =
Text
-> (PrtclState -> Int)
-> Decoder s PrtclState
-> Decoder s PrtclState
forall a s. Text -> (a -> Int) -> Decoder s a -> Decoder s a
decodeRecordNamed
Text
"PrtclState"
(Int -> PrtclState -> Int
forall a b. a -> b -> a
const Int
3)
( Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState
(Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState)
-> Decoder s (Map (KeyHash 'BlockIssuer) Word64)
-> Decoder s (Nonce -> Nonce -> PrtclState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (Map (KeyHash 'BlockIssuer) Word64)
forall s. Decoder s (Map (KeyHash 'BlockIssuer) Word64)
forall a s. FromCBOR a => Decoder s a
fromCBOR
Decoder s (Nonce -> Nonce -> PrtclState)
-> Decoder s Nonce -> Decoder s (Nonce -> PrtclState)
forall a b. Decoder s (a -> b) -> Decoder s a -> Decoder s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Decoder s Nonce
forall s. Decoder s Nonce
forall a s. FromCBOR a => Decoder s a
fromCBOR
Decoder s (Nonce -> PrtclState)
-> Decoder s Nonce -> Decoder s PrtclState
forall a b. Decoder s (a -> b) -> Decoder s a -> Decoder s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Decoder s Nonce
forall s. Decoder s Nonce
forall a s. FromCBOR a => Decoder s a
fromCBOR
)
instance NoThunks PrtclState
data PrtclEnv
= PrtclEnv
UnitInterval
PoolDistr
GenDelegs
Nonce
deriving ((forall x. PrtclEnv -> Rep PrtclEnv x)
-> (forall x. Rep PrtclEnv x -> PrtclEnv) -> Generic PrtclEnv
forall x. Rep PrtclEnv x -> PrtclEnv
forall x. PrtclEnv -> Rep PrtclEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrtclEnv -> Rep PrtclEnv x
from :: forall x. PrtclEnv -> Rep PrtclEnv x
$cto :: forall x. Rep PrtclEnv x -> PrtclEnv
to :: forall x. Rep PrtclEnv x -> PrtclEnv
Generic)
instance NoThunks PrtclEnv
data PrtclPredicateFailure c
= OverlayFailure (PredicateFailure (OVERLAY c))
| UpdnFailure (PredicateFailure (UPDN c))
deriving ((forall x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x)
-> (forall x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c)
-> Generic (PrtclPredicateFailure c)
forall x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
forall x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
forall c x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
$cfrom :: forall c x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
from :: forall x.
PrtclPredicateFailure c -> Rep (PrtclPredicateFailure c) x
$cto :: forall c x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
to :: forall x.
Rep (PrtclPredicateFailure c) x -> PrtclPredicateFailure c
Generic)
data PrtclEvent c
= UpdnEvent (Event (UPDN c))
| NoEvent Void
deriving instance
VRF.VRFAlgorithm (VRF c) =>
Show (PrtclPredicateFailure c)
deriving instance
VRF.VRFAlgorithm (VRF c) =>
Eq (PrtclPredicateFailure c)
instance
( Crypto c
, KES.Signable (KES c) (BHBody c)
, VRF.Signable (VRF c) Seed
) =>
STS (PRTCL c)
where
type State (PRTCL c) = PrtclState
type Signal (PRTCL c) = BHeader c
type Environment (PRTCL c) = PrtclEnv
type BaseM (PRTCL c) = ShelleyBase
type PredicateFailure (PRTCL c) = PrtclPredicateFailure c
type Event (PRTCL c) = PrtclEvent c
initialRules :: [InitialRule (PRTCL c)]
initialRules = []
transitionRules :: [TransitionRule (PRTCL c)]
transitionRules = [TransitionRule (PRTCL c)
forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (PRTCL c)
prtclTransition]
prtclTransition ::
forall c.
( Crypto c
, KES.Signable (KES c) (BHBody c)
, VRF.Signable (VRF c) Seed
) =>
TransitionRule (PRTCL c)
prtclTransition :: forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (PRTCL c)
prtclTransition = do
TRC
( PrtclEnv UnitInterval
dval PoolDistr
pd GenDelegs
dms Nonce
eta0
, PrtclState Map (KeyHash 'BlockIssuer) Word64
cs Nonce
etaV Nonce
etaC
, Signal (PRTCL c)
bh
) <-
Rule (PRTCL c) 'Transition (RuleContext 'Transition (PRTCL c))
F (Clause (PRTCL c) 'Transition) (TRC (PRTCL c))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
let bhb :: BHBody c
bhb = BHeader c -> BHBody c
forall c. Crypto c => BHeader c -> BHBody c
bhbody Signal (PRTCL c)
BHeader c
bh
slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
eta :: Nonce
eta = BHBody c -> Nonce
forall c. BHBody c -> Nonce
bnonce BHBody c
bhb
UpdnState Nonce
etaV' Nonce
etaC' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(UPDN c) (RuleContext 'Transition (UPDN c)
-> Rule (PRTCL c) 'Transition (State (UPDN c)))
-> RuleContext 'Transition (UPDN c)
-> Rule (PRTCL c) 'Transition (State (UPDN c))
forall a b. (a -> b) -> a -> b
$
(Environment (UPDN c), State (UPDN c), Signal (UPDN c))
-> TRC (UPDN c)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
( Nonce -> UpdnEnv
UpdnEnv Nonce
eta
, Nonce -> Nonce -> UpdnState
UpdnState Nonce
etaV Nonce
etaC
, SlotNo
Signal (UPDN c)
slot
)
Map (KeyHash 'BlockIssuer) Word64
cs' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(OVERLAY c) (RuleContext 'Transition (OVERLAY c)
-> Rule (PRTCL c) 'Transition (State (OVERLAY c)))
-> RuleContext 'Transition (OVERLAY c)
-> Rule (PRTCL c) 'Transition (State (OVERLAY c))
forall a b. (a -> b) -> a -> b
$
(Environment (OVERLAY c), State (OVERLAY c), Signal (OVERLAY c))
-> TRC (OVERLAY c)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UnitInterval -> PoolDistr -> GenDelegs -> Nonce -> OverlayEnv
OverlayEnv UnitInterval
dval PoolDistr
pd GenDelegs
dms Nonce
eta0, Map (KeyHash 'BlockIssuer) Word64
State (OVERLAY c)
cs, Signal (OVERLAY c)
Signal (PRTCL c)
bh)
PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState
forall a. a -> F (Clause (PRTCL c) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState)
-> PrtclState -> F (Clause (PRTCL c) 'Transition) PrtclState
forall a b. (a -> b) -> a -> b
$
Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState
Map (KeyHash 'BlockIssuer) Word64
cs'
Nonce
etaV'
Nonce
etaC'
instance Crypto c => NoThunks (PrtclPredicateFailure c)
instance
( Crypto c
, KES.Signable (KES c) (BHBody c)
, VRF.Signable (VRF c) Seed
) =>
Embed (OVERLAY c) (PRTCL c)
where
wrapFailed :: PredicateFailure (OVERLAY c) -> PredicateFailure (PRTCL c)
wrapFailed = PredicateFailure (OVERLAY c) -> PredicateFailure (PRTCL c)
PredicateFailure (OVERLAY c) -> PrtclPredicateFailure c
forall c. PredicateFailure (OVERLAY c) -> PrtclPredicateFailure c
OverlayFailure
wrapEvent :: Event (OVERLAY c) -> Event (PRTCL c)
wrapEvent = Void -> PrtclEvent c
Event (OVERLAY c) -> Event (PRTCL c)
forall c. Void -> PrtclEvent c
NoEvent
instance
( Crypto c
, KES.Signable (KES c) (BHBody c)
, VRF.Signable (VRF c) Seed
) =>
Embed (UPDN c) (PRTCL c)
where
wrapFailed :: PredicateFailure (UPDN c) -> PredicateFailure (PRTCL c)
wrapFailed = PredicateFailure (UPDN c) -> PredicateFailure (PRTCL c)
PredicateFailure (UPDN c) -> PrtclPredicateFailure c
forall c. PredicateFailure (UPDN c) -> PrtclPredicateFailure c
UpdnFailure
wrapEvent :: Event (UPDN c) -> Event (PRTCL c)
wrapEvent = Event (UPDN c) -> Event (PRTCL c)
Event (UPDN c) -> PrtclEvent c
forall c. Event (UPDN c) -> PrtclEvent c
UpdnEvent
data PrtlSeqFailure
= WrongSlotIntervalPrtclSeq
SlotNo
SlotNo
| WrongBlockNoPrtclSeq
(WithOrigin LastAppliedBlock)
BlockNo
| WrongBlockSequencePrtclSeq
PrevHash
PrevHash
deriving (Int -> PrtlSeqFailure -> ShowS
[PrtlSeqFailure] -> ShowS
PrtlSeqFailure -> String
(Int -> PrtlSeqFailure -> ShowS)
-> (PrtlSeqFailure -> String)
-> ([PrtlSeqFailure] -> ShowS)
-> Show PrtlSeqFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrtlSeqFailure -> ShowS
showsPrec :: Int -> PrtlSeqFailure -> ShowS
$cshow :: PrtlSeqFailure -> String
show :: PrtlSeqFailure -> String
$cshowList :: [PrtlSeqFailure] -> ShowS
showList :: [PrtlSeqFailure] -> ShowS
Show, PrtlSeqFailure -> PrtlSeqFailure -> Bool
(PrtlSeqFailure -> PrtlSeqFailure -> Bool)
-> (PrtlSeqFailure -> PrtlSeqFailure -> Bool) -> Eq PrtlSeqFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
== :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
$c/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
/= :: PrtlSeqFailure -> PrtlSeqFailure -> Bool
Eq, (forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x)
-> (forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure)
-> Generic PrtlSeqFailure
forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
from :: forall x. PrtlSeqFailure -> Rep PrtlSeqFailure x
$cto :: forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
to :: forall x. Rep PrtlSeqFailure x -> PrtlSeqFailure
Generic)
instance NoThunks PrtlSeqFailure
prtlSeqChecks ::
(MonadError PrtlSeqFailure m, Crypto c) =>
WithOrigin LastAppliedBlock ->
BHeader c ->
m ()
prtlSeqChecks :: forall (m :: * -> *) c.
(MonadError PrtlSeqFailure m, Crypto c) =>
WithOrigin LastAppliedBlock -> BHeader c -> m ()
prtlSeqChecks WithOrigin LastAppliedBlock
lab BHeader c
bh =
case WithOrigin LastAppliedBlock
lab of
WithOrigin LastAppliedBlock
Origin -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
At (LastAppliedBlock BlockNo
bL SlotNo
sL HashHeader
_) -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SlotNo
sL SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
slot) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ SlotNo -> SlotNo -> PrtlSeqFailure
WrongSlotIntervalPrtclSeq SlotNo
sL SlotNo
slot
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BlockNo
bL BlockNo -> BlockNo -> BlockNo
forall a. Num a => a -> a -> a
+ BlockNo
1 BlockNo -> BlockNo -> Bool
forall a. Eq a => a -> a -> Bool
== BlockNo
bn) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ WithOrigin LastAppliedBlock -> BlockNo -> PrtlSeqFailure
WrongBlockNoPrtclSeq WithOrigin LastAppliedBlock
lab BlockNo
bn
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrevHash
ph PrevHash -> PrevHash -> Bool
forall a. Eq a => a -> a -> Bool
== BHBody c -> PrevHash
forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb) (m () -> m ())
-> (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrtlSeqFailure -> m ()
forall a. PrtlSeqFailure -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (PrtlSeqFailure -> m ()) -> PrtlSeqFailure -> m ()
forall a b. (a -> b) -> a -> b
$ PrevHash -> PrevHash -> PrtlSeqFailure
WrongBlockSequencePrtclSeq PrevHash
ph (BHBody c -> PrevHash
forall c. BHBody c -> PrevHash
bheaderPrev BHBody c
bhb)
where
bhb :: BHBody c
bhb = BHeader c -> BHBody c
forall c. Crypto c => BHeader c -> BHBody c
bhbody BHeader c
bh
bn :: BlockNo
bn = BHBody c -> BlockNo
forall c. BHBody c -> BlockNo
bheaderBlockNo BHBody c
bhb
slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
ph :: PrevHash
ph = WithOrigin LastAppliedBlock -> PrevHash
lastAppliedHash WithOrigin LastAppliedBlock
lab