{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Shelley.Spec.Ledger.STS.Tick
( TICK,
State,
TickPredicateFailure (..),
PredicateFailure,
adoptGenesisDelegs,
TICKF,
TickfPredicateFailure (..),
)
where
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, epochInfo)
import Shelley.Spec.Ledger.Keys (GenDelegs (..))
import Shelley.Spec.Ledger.LedgerState
( DPState (..),
DState (..),
EpochState (..),
FutureGenDeleg (..),
LedgerState (..),
NewEpochState (..),
)
import Shelley.Spec.Ledger.STS.NewEpoch (NEWEPOCH)
import Shelley.Spec.Ledger.STS.Rupd (RUPD, RupdEnv (..))
import Shelley.Spec.Ledger.Slot (SlotNo, epochInfoEpoch)
data TICK era
data TickPredicateFailure era
= NewEpochFailure (PredicateFailure (NEWEPOCH era))
| RupdFailure (PredicateFailure (RUPD era))
deriving ((forall x.
TickPredicateFailure era -> Rep (TickPredicateFailure era) x)
-> (forall x.
Rep (TickPredicateFailure era) x -> TickPredicateFailure era)
-> Generic (TickPredicateFailure era)
forall x.
Rep (TickPredicateFailure era) x -> TickPredicateFailure era
forall x.
TickPredicateFailure era -> Rep (TickPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (TickPredicateFailure era) x -> TickPredicateFailure era
forall era x.
TickPredicateFailure era -> Rep (TickPredicateFailure era) x
$cto :: forall era x.
Rep (TickPredicateFailure era) x -> TickPredicateFailure era
$cfrom :: forall era x.
TickPredicateFailure era -> Rep (TickPredicateFailure era) x
Generic)
deriving stock instance Show (TickPredicateFailure era)
deriving stock instance Eq (TickPredicateFailure era)
instance NoThunks (TickPredicateFailure era)
instance
( ShelleyBased era
) =>
STS (TICK era)
where
type
State (TICK era) =
NewEpochState era
type
Signal (TICK era) =
SlotNo
type Environment (TICK era) = ()
type BaseM (TICK era) = ShelleyBase
type PredicateFailure (TICK era) = TickPredicateFailure era
initialRules :: [InitialRule (TICK era)]
initialRules = []
transitionRules :: [TransitionRule (TICK era)]
transitionRules = [TransitionRule (TICK era)
forall era. ShelleyBased era => TransitionRule (TICK era)
bheadTransition]
adoptGenesisDelegs ::
EpochState era ->
SlotNo ->
EpochState era
adoptGenesisDelegs :: EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
slot = EpochState era
es'
where
ls :: LedgerState era
ls = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
es
dp :: DPState (Crypto era)
dp = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
_delegationState LedgerState era
ls
ds :: DState (Crypto era)
ds = DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
_dstate DPState (Crypto era)
dp
fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs = DState (Crypto era)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall crypto.
DState crypto -> Map (FutureGenDeleg crypto) (GenDelegPair crypto)
_fGenDelegs DState (Crypto era)
ds
GenDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs = DState (Crypto era) -> GenDelegs (Crypto era)
forall crypto. DState crypto -> GenDelegs crypto
_genDelegs DState (Crypto era)
ds
(Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
curr, Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs') = (FutureGenDeleg (Crypto era) -> GenDelegPair (Crypto era) -> Bool)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)),
Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\(FutureGenDeleg SlotNo
s KeyHash 'Genesis (Crypto era)
_) GenDelegPair (Crypto era)
_ -> SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs
latestPerGKey :: FutureGenDeleg crypto
-> b
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
latestPerGKey (FutureGenDeleg SlotNo
s KeyHash 'Genesis crypto
genKeyHash) b
delegate Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest =
case KeyHash 'Genesis crypto
-> Map (KeyHash 'Genesis crypto) (SlotNo, b) -> Maybe (SlotNo, b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis crypto
genKeyHash Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest of
Maybe (SlotNo, b)
Nothing -> KeyHash 'Genesis crypto
-> (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis crypto
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest
Just (SlotNo
t, b
_) ->
if SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> SlotNo
t
then KeyHash 'Genesis crypto
-> (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis crypto
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest
else Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest
genDelegs' :: Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs' = ((SlotNo, GenDelegPair (Crypto era)) -> GenDelegPair (Crypto era))
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (SlotNo, GenDelegPair (Crypto era)) -> GenDelegPair (Crypto era)
forall a b. (a, b) -> b
snd (Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall a b. (a -> b) -> a -> b
$ (FutureGenDeleg (Crypto era)
-> GenDelegPair (Crypto era)
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map
(KeyHash 'Genesis (Crypto era))
(SlotNo, GenDelegPair (Crypto era)))
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey FutureGenDeleg (Crypto era)
-> GenDelegPair (Crypto era)
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall crypto b.
FutureGenDeleg crypto
-> b
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
latestPerGKey Map
(KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall k a. Map k a
Map.empty Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
curr
ds' :: DState (Crypto era)
ds' =
DState (Crypto era)
ds
{ _fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs = Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs',
_genDelegs :: GenDelegs (Crypto era)
_genDelegs = Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era)
forall crypto.
Map (KeyHash 'Genesis crypto) (GenDelegPair crypto)
-> GenDelegs crypto
GenDelegs (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era)
forall a b. (a -> b) -> a -> b
$ Exp
(Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Exp
(Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
⨃ Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs')
}
dp' :: DPState (Crypto era)
dp' = DPState (Crypto era)
dp {_dstate :: DState (Crypto era)
_dstate = DState (Crypto era)
ds'}
ls' :: LedgerState era
ls' = LedgerState era
ls {_delegationState :: DPState (Crypto era)
_delegationState = DPState (Crypto era)
dp'}
es' :: EpochState era
es' = EpochState era
es {esLState :: LedgerState era
esLState = LedgerState era
ls'}
validatingTickTransition ::
forall tick era.
( Embed (NEWEPOCH era) (tick era),
STS (tick era),
State (tick era) ~ NewEpochState era,
BaseM (tick era) ~ ShelleyBase
) =>
NewEpochState era ->
SlotNo ->
TransitionRule (tick era)
validatingTickTransition :: NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition NewEpochState era
nes SlotNo
slot = do
EpochNo
epoch <- BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo)
-> BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ do
EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfo
HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
NewEpochState era
nes' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (NEWEPOCH era) super =>
RuleContext rtype (NEWEPOCH era)
-> Rule super rtype (State (NEWEPOCH era))
trans @(NEWEPOCH era) (RuleContext 'Transition (NEWEPOCH era)
-> Rule (tick era) 'Transition (State (NEWEPOCH era)))
-> RuleContext 'Transition (NEWEPOCH era)
-> Rule (tick era) 'Transition (State (NEWEPOCH era))
forall a b. (a -> b) -> a -> b
$ (Environment (NEWEPOCH era), State (NEWEPOCH era),
Signal (NEWEPOCH era))
-> TRC (NEWEPOCH era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State (NEWEPOCH era)
NewEpochState era
nes, EpochNo
Signal (NEWEPOCH era)
epoch)
let es'' :: EpochState era
es'' = EpochState era -> SlotNo -> EpochState era
forall era. EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs (NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes') SlotNo
slot
NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era))
-> NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes' {nesEs :: EpochState era
nesEs = EpochState era
es''}
bheadTransition ::
forall era.
( ShelleyBased era
) =>
TransitionRule (TICK era)
bheadTransition :: TransitionRule (TICK era)
bheadTransition = do
TRC ((), nes :: State (TICK era)
nes@(NewEpochState _ bprev _ es _ _), Signal (TICK era)
slot) <-
F (Clause (TICK era) 'Transition) (TRC (TICK era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
NewEpochState era
nes' <- NewEpochState era -> SlotNo -> TransitionRule (TICK era)
forall (tick :: * -> *) era.
(Embed (NEWEPOCH era) (tick era), STS (tick era),
State (tick era) ~ NewEpochState era,
BaseM (tick era) ~ ShelleyBase) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition State (TICK era)
NewEpochState era
nes SlotNo
Signal (TICK era)
slot
StrictMaybe (RewardUpdate (Crypto era))
ru'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (RUPD era) super =>
RuleContext rtype (RUPD era) -> Rule super rtype (State (RUPD era))
trans @(RUPD era) (RuleContext 'Transition (RUPD era)
-> Rule (TICK era) 'Transition (State (RUPD era)))
-> RuleContext 'Transition (RUPD era)
-> Rule (TICK era) 'Transition (State (RUPD era))
forall a b. (a -> b) -> a -> b
$ (Environment (RUPD era), State (RUPD era), Signal (RUPD era))
-> TRC (RUPD era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (BlocksMade (Crypto era) -> EpochState era -> RupdEnv era
forall era.
BlocksMade (Crypto era) -> EpochState era -> RupdEnv era
RupdEnv BlocksMade (Crypto era)
bprev EpochState era
es, NewEpochState era -> StrictMaybe (RewardUpdate (Crypto era))
forall era.
NewEpochState era -> StrictMaybe (RewardUpdate (Crypto era))
nesRu NewEpochState era
nes', Signal (RUPD era)
Signal (TICK era)
slot)
let nes'' :: NewEpochState era
nes'' = NewEpochState era
nes' {nesRu :: StrictMaybe (RewardUpdate (Crypto era))
nesRu = StrictMaybe (RewardUpdate (Crypto era))
ru''}
NewEpochState era
-> F (Clause (TICK era) 'Transition) (NewEpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NewEpochState era
nes''
instance
ShelleyBased era =>
Embed (NEWEPOCH era) (TICK era)
where
wrapFailed :: PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICK era)
wrapFailed = PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICK era)
forall era.
PredicateFailure (NEWEPOCH era) -> TickPredicateFailure era
NewEpochFailure
instance
(ShelleyBased era) =>
Embed (RUPD era) (TICK era)
where
wrapFailed :: PredicateFailure (RUPD era) -> PredicateFailure (TICK era)
wrapFailed = PredicateFailure (RUPD era) -> PredicateFailure (TICK era)
forall era. PredicateFailure (RUPD era) -> TickPredicateFailure era
RupdFailure
data TICKF era
data TickfPredicateFailure era
= TickfNewEpochFailure (PredicateFailure (NEWEPOCH era))
deriving (Int -> TickfPredicateFailure era -> ShowS
[TickfPredicateFailure era] -> ShowS
TickfPredicateFailure era -> String
(Int -> TickfPredicateFailure era -> ShowS)
-> (TickfPredicateFailure era -> String)
-> ([TickfPredicateFailure era] -> ShowS)
-> Show (TickfPredicateFailure era)
forall era. Int -> TickfPredicateFailure era -> ShowS
forall era. [TickfPredicateFailure era] -> ShowS
forall era. TickfPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TickfPredicateFailure era] -> ShowS
$cshowList :: forall era. [TickfPredicateFailure era] -> ShowS
show :: TickfPredicateFailure era -> String
$cshow :: forall era. TickfPredicateFailure era -> String
showsPrec :: Int -> TickfPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> TickfPredicateFailure era -> ShowS
Show, (forall x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x)
-> (forall x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era)
-> Generic (TickfPredicateFailure era)
forall x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
forall x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
forall era x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
$cto :: forall era x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
$cfrom :: forall era x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
Generic, TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
(TickfPredicateFailure era -> TickfPredicateFailure era -> Bool)
-> (TickfPredicateFailure era -> TickfPredicateFailure era -> Bool)
-> Eq (TickfPredicateFailure era)
forall era.
TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
$c/= :: forall era.
TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
== :: TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
$c== :: forall era.
TickfPredicateFailure era -> TickfPredicateFailure era -> Bool
Eq)
instance NoThunks (TickfPredicateFailure era)
instance
ShelleyBased era =>
STS (TICKF era)
where
type
State (TICKF era) =
NewEpochState era
type
Signal (TICKF era) =
SlotNo
type Environment (TICKF era) = ()
type BaseM (TICKF era) = ShelleyBase
type PredicateFailure (TICKF era) = TickfPredicateFailure era
initialRules :: [InitialRule (TICKF era)]
initialRules = []
transitionRules :: [TransitionRule (TICKF era)]
transitionRules =
[ do
TRC ((), State (TICKF era)
nes, Signal (TICKF era)
slot) <- F (Clause (TICKF era) 'Transition) (TRC (TICKF era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
NewEpochState era -> SlotNo -> TransitionRule (TICKF era)
forall (tick :: * -> *) era.
(Embed (NEWEPOCH era) (tick era), STS (tick era),
State (tick era) ~ NewEpochState era,
BaseM (tick era) ~ ShelleyBase) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition State (TICKF era)
NewEpochState era
nes SlotNo
Signal (TICKF era)
slot
]
instance
ShelleyBased era =>
Embed (NEWEPOCH era) (TICKF era)
where
wrapFailed :: PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICKF era)
wrapFailed = PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICKF era)
forall era.
PredicateFailure (NEWEPOCH era) -> TickfPredicateFailure era
TickfNewEpochFailure