{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
module Cardano.Protocol.TPraos.Rules.Updn (
UPDN,
UpdnEnv (..),
UpdnState (..),
PredicateFailure,
UpdnPredicateFailure,
) where
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Slot
import Cardano.Protocol.Crypto
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
data UPDN c
newtype UpdnEnv
=
UpdnEnv
Nonce
data UpdnState = UpdnState Nonce Nonce
deriving (Int -> UpdnState -> ShowS
[UpdnState] -> ShowS
UpdnState -> String
(Int -> UpdnState -> ShowS)
-> (UpdnState -> String)
-> ([UpdnState] -> ShowS)
-> Show UpdnState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UpdnState -> ShowS
showsPrec :: Int -> UpdnState -> ShowS
$cshow :: UpdnState -> String
show :: UpdnState -> String
$cshowList :: [UpdnState] -> ShowS
showList :: [UpdnState] -> ShowS
Show, UpdnState -> UpdnState -> Bool
(UpdnState -> UpdnState -> Bool)
-> (UpdnState -> UpdnState -> Bool) -> Eq UpdnState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UpdnState -> UpdnState -> Bool
== :: UpdnState -> UpdnState -> Bool
$c/= :: UpdnState -> UpdnState -> Bool
/= :: UpdnState -> UpdnState -> Bool
Eq)
data UpdnPredicateFailure c
deriving ((forall x.
UpdnPredicateFailure c -> Rep (UpdnPredicateFailure c) x)
-> (forall x.
Rep (UpdnPredicateFailure c) x -> UpdnPredicateFailure c)
-> Generic (UpdnPredicateFailure c)
forall x. Rep (UpdnPredicateFailure c) x -> UpdnPredicateFailure c
forall x. UpdnPredicateFailure c -> Rep (UpdnPredicateFailure c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x.
Rep (UpdnPredicateFailure c) x -> UpdnPredicateFailure c
forall c x.
UpdnPredicateFailure c -> Rep (UpdnPredicateFailure c) x
$cfrom :: forall c x.
UpdnPredicateFailure c -> Rep (UpdnPredicateFailure c) x
from :: forall x. UpdnPredicateFailure c -> Rep (UpdnPredicateFailure c) x
$cto :: forall c x.
Rep (UpdnPredicateFailure c) x -> UpdnPredicateFailure c
to :: forall x. Rep (UpdnPredicateFailure c) x -> UpdnPredicateFailure c
Generic, Int -> UpdnPredicateFailure c -> ShowS
[UpdnPredicateFailure c] -> ShowS
UpdnPredicateFailure c -> String
(Int -> UpdnPredicateFailure c -> ShowS)
-> (UpdnPredicateFailure c -> String)
-> ([UpdnPredicateFailure c] -> ShowS)
-> Show (UpdnPredicateFailure c)
forall c. Int -> UpdnPredicateFailure c -> ShowS
forall c. [UpdnPredicateFailure c] -> ShowS
forall c. UpdnPredicateFailure c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall c. Int -> UpdnPredicateFailure c -> ShowS
showsPrec :: Int -> UpdnPredicateFailure c -> ShowS
$cshow :: forall c. UpdnPredicateFailure c -> String
show :: UpdnPredicateFailure c -> String
$cshowList :: forall c. [UpdnPredicateFailure c] -> ShowS
showList :: [UpdnPredicateFailure c] -> ShowS
Show, UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
(UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool)
-> (UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool)
-> Eq (UpdnPredicateFailure c)
forall c. UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall c. UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
== :: UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
$c/= :: forall c. UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
/= :: UpdnPredicateFailure c -> UpdnPredicateFailure c -> Bool
Eq)
instance NoThunks (UpdnPredicateFailure c)
newtype UpdnEvent c = NewEpoch EpochNo
instance
Crypto c =>
STS (UPDN c)
where
type State (UPDN c) = UpdnState
type Signal (UPDN c) = SlotNo
type Environment (UPDN c) = UpdnEnv
type BaseM (UPDN c) = ShelleyBase
type PredicateFailure (UPDN c) = UpdnPredicateFailure c
type Event (UPDN c) = UpdnEvent c
initialRules :: [InitialRule (UPDN c)]
initialRules =
[ UpdnState -> F (Clause (UPDN c) 'Initial) UpdnState
forall a. a -> F (Clause (UPDN c) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Nonce -> Nonce -> UpdnState
UpdnState
Nonce
initialNonce
Nonce
initialNonce
)
]
where
initialNonce :: Nonce
initialNonce = Word64 -> Nonce
mkNonceFromNumber Word64
0
transitionRules :: [TransitionRule (UPDN c)]
transitionRules = [TransitionRule (UPDN c)
forall c. Crypto c => TransitionRule (UPDN c)
updTransition]
updTransition :: Crypto c => TransitionRule (UPDN c)
updTransition :: forall c. Crypto c => TransitionRule (UPDN c)
updTransition = do
TRC (UpdnEnv Nonce
eta, UpdnState Nonce
eta_v Nonce
eta_c, Signal (UPDN c)
s) <- Rule (UPDN c) 'Transition (RuleContext 'Transition (UPDN c))
F (Clause (UPDN c) 'Transition) (TRC (UPDN c))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
EpochInfo Identity
ei <- BaseM (UPDN c) (EpochInfo Identity)
-> Rule (UPDN c) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN c) (EpochInfo Identity)
-> Rule (UPDN c) 'Transition (EpochInfo Identity))
-> BaseM (UPDN c) (EpochInfo Identity)
-> Rule (UPDN c) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
Word64
sp <- BaseM (UPDN c) Word64 -> Rule (UPDN c) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPDN c) Word64 -> Rule (UPDN c) 'Transition Word64)
-> BaseM (UPDN c) Word64 -> Rule (UPDN c) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
let curEpochNo :: EpochNo
curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
Signal (UPDN c)
s
nextEpochNo :: EpochNo
nextEpochNo = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
curEpochNo (Word32 -> EpochInterval
EpochInterval Word32
1)
firstSlotNextEpoch :: SlotNo
firstSlotNextEpoch = HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
EpochInfo Identity -> EpochNo -> SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
nextEpochNo
Event (UPDN c) -> Rule (UPDN c) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (UPDN c) -> Rule (UPDN c) 'Transition ())
-> Event (UPDN c) -> Rule (UPDN c) 'Transition ()
forall a b. (a -> b) -> a -> b
$ EpochNo -> UpdnEvent c
forall c. EpochNo -> UpdnEvent c
NewEpoch EpochNo
nextEpochNo
UpdnState -> F (Clause (UPDN c) 'Transition) UpdnState
forall a. a -> F (Clause (UPDN c) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpdnState -> F (Clause (UPDN c) 'Transition) UpdnState)
-> UpdnState -> F (Clause (UPDN c) 'Transition) UpdnState
forall a b. (a -> b) -> a -> b
$
Nonce -> Nonce -> UpdnState
UpdnState
(Nonce
eta_v Nonce -> Nonce -> Nonce
⭒ Nonce
eta)
( if SlotNo
Signal (UPDN c)
s SlotNo -> Duration -> SlotNo
+* Word64 -> Duration
Duration Word64
sp SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
firstSlotNextEpoch
then Nonce
eta_v Nonce -> Nonce -> Nonce
⭒ Nonce
eta
else Nonce
eta_c
)