{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Shelley.Spec.Ledger.STS.Epoch
( EPOCH,
EpochPredicateFailure (..),
PredicateFailure,
)
where
import Cardano.Ledger.Shelley (ShelleyBased)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition (Embed (..), InitialRule, STS (..), TRC (..), TransitionRule, judgmentContext, liftSTS, trans)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (Globals (..), ShelleyBase)
import Shelley.Spec.Ledger.EpochBoundary (emptySnapShots)
import Shelley.Spec.Ledger.LedgerState
( EpochState,
PPUPState (..),
PState (..),
emptyAccount,
emptyLedgerState,
esAccountState,
esLState,
esNonMyopic,
esPp,
esPrevPp,
esSnapshots,
_delegationState,
_ppups,
_utxoState,
pattern DPState,
pattern EpochState,
)
import Shelley.Spec.Ledger.PParams (PParams, PParamsUpdate, ProposedPPUpdates (..), emptyPParams, updatePParams)
import Shelley.Spec.Ledger.Rewards (emptyNonMyopic)
import Shelley.Spec.Ledger.STS.Newpp (NEWPP, NewppEnv (..), NewppState (..))
import Shelley.Spec.Ledger.STS.PoolReap (POOLREAP, PoolreapState (..))
import Shelley.Spec.Ledger.STS.Snap (SNAP)
import Shelley.Spec.Ledger.Slot (EpochNo)
data EPOCH era
data EpochPredicateFailure era
= PoolReapFailure (PredicateFailure (POOLREAP era))
| SnapFailure (PredicateFailure (SNAP era))
| NewPpFailure (PredicateFailure (NEWPP era))
deriving ((forall x.
EpochPredicateFailure era -> Rep (EpochPredicateFailure era) x)
-> (forall x.
Rep (EpochPredicateFailure era) x -> EpochPredicateFailure era)
-> Generic (EpochPredicateFailure era)
forall x.
Rep (EpochPredicateFailure era) x -> EpochPredicateFailure era
forall x.
EpochPredicateFailure era -> Rep (EpochPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (EpochPredicateFailure era) x -> EpochPredicateFailure era
forall era x.
EpochPredicateFailure era -> Rep (EpochPredicateFailure era) x
$cto :: forall era x.
Rep (EpochPredicateFailure era) x -> EpochPredicateFailure era
$cfrom :: forall era x.
EpochPredicateFailure era -> Rep (EpochPredicateFailure era) x
Generic)
deriving stock instance
(Eq (PredicateFailure (SNAP era))) =>
Eq (EpochPredicateFailure era)
deriving stock instance
(Show (PredicateFailure (SNAP era))) =>
Show (EpochPredicateFailure era)
instance ShelleyBased era => STS (EPOCH era) where
type State (EPOCH era) = EpochState era
type Signal (EPOCH era) = EpochNo
type Environment (EPOCH era) = ()
type BaseM (EPOCH era) = ShelleyBase
type PredicateFailure (EPOCH era) = EpochPredicateFailure era
initialRules :: [InitialRule (EPOCH era)]
initialRules = [InitialRule (EPOCH era)
forall era. InitialRule (EPOCH era)
initialEpoch]
transitionRules :: [TransitionRule (EPOCH era)]
transitionRules = [TransitionRule (EPOCH era)
forall era. ShelleyBased era => TransitionRule (EPOCH era)
epochTransition]
instance NoThunks (EpochPredicateFailure era)
initialEpoch :: InitialRule (EPOCH era)
initialEpoch :: InitialRule (EPOCH era)
initialEpoch =
EpochState era -> F (Clause (EPOCH era) 'Initial) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
-> F (Clause (EPOCH era) 'Initial) (EpochState era))
-> EpochState era
-> F (Clause (EPOCH era) 'Initial) (EpochState era)
forall a b. (a -> b) -> a -> b
$
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
EpochState
AccountState
emptyAccount
SnapShots era
forall era. SnapShots era
emptySnapShots
LedgerState era
forall era. LedgerState era
emptyLedgerState
PParams era
forall era. PParams era
emptyPParams
PParams era
forall era. PParams era
emptyPParams
NonMyopic era
forall era. NonMyopic era
emptyNonMyopic
votedValue ::
ProposedPPUpdates era ->
PParams era ->
Int ->
Maybe (PParams era)
votedValue :: ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
votedValue (ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
pup) PParams era
pps Int
quorumN =
let incrTally :: k -> Map k a -> a
incrTally k
vote Map k a
tally = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
0 k
vote Map k a
tally
votes :: Map (PParamsUpdate era) Int
votes =
(PParamsUpdate era
-> Map (PParamsUpdate era) Int -> Map (PParamsUpdate era) Int)
-> Map (PParamsUpdate era) Int
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Map (PParamsUpdate era) Int
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr
(\PParamsUpdate era
vote Map (PParamsUpdate era) Int
tally -> PParamsUpdate era
-> Int
-> Map (PParamsUpdate era) Int
-> Map (PParamsUpdate era) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert PParamsUpdate era
vote (PParamsUpdate era -> Map (PParamsUpdate era) Int -> Int
forall a k. (Num a, Ord k) => k -> Map k a -> a
incrTally PParamsUpdate era
vote Map (PParamsUpdate era) Int
tally) Map (PParamsUpdate era) Int
tally)
(forall era. Map (PParamsUpdate era) Int
forall k a. Map k a
Map.empty :: Map (PParamsUpdate era) Int)
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
pup
consensus :: Map (PParamsUpdate era) Int
consensus = (Int -> Bool)
-> Map (PParamsUpdate era) Int -> Map (PParamsUpdate era) Int
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
quorumN) Map (PParamsUpdate era) Int
votes
in case Map (PParamsUpdate era) Int -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map (PParamsUpdate era) Int
consensus of
Int
1 -> (PParams era -> Maybe (PParams era)
forall a. a -> Maybe a
Just (PParams era -> Maybe (PParams era))
-> (Map (PParamsUpdate era) Int -> PParams era)
-> Map (PParamsUpdate era) Int
-> Maybe (PParams era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PParams era -> PParamsUpdate era -> PParams era
forall era. PParams era -> PParamsUpdate era -> PParams era
updatePParams PParams era
pps (PParamsUpdate era -> PParams era)
-> (Map (PParamsUpdate era) Int -> PParamsUpdate era)
-> Map (PParamsUpdate era) Int
-> PParams era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PParamsUpdate era, Int) -> PParamsUpdate era
forall a b. (a, b) -> a
fst ((PParamsUpdate era, Int) -> PParamsUpdate era)
-> (Map (PParamsUpdate era) Int -> (PParamsUpdate era, Int))
-> Map (PParamsUpdate era) Int
-> PParamsUpdate era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(PParamsUpdate era, Int)] -> (PParamsUpdate era, Int)
forall a. [a] -> a
head ([(PParamsUpdate era, Int)] -> (PParamsUpdate era, Int))
-> (Map (PParamsUpdate era) Int -> [(PParamsUpdate era, Int)])
-> Map (PParamsUpdate era) Int
-> (PParamsUpdate era, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (PParamsUpdate era) Int -> [(PParamsUpdate era, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList) Map (PParamsUpdate era) Int
consensus
Int
_ -> Maybe (PParams era)
forall a. Maybe a
Nothing
epochTransition ::
forall era.
ShelleyBased era =>
TransitionRule (EPOCH era)
epochTransition :: TransitionRule (EPOCH era)
epochTransition = do
TRC
( Environment (EPOCH era)
_,
EpochState
{ esAccountState = acnt,
esSnapshots = ss,
esLState = ls,
esPrevPp = _pr,
esPp = pp,
esNonMyopic = nm
},
Signal (EPOCH era)
e
) <-
F (Clause (EPOCH era) 'Transition) (TRC (EPOCH era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
let utxoSt :: UTxOState era
utxoSt = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
_utxoState LedgerState era
ls
let DPState DState era
dstate PState era
pstate = LedgerState era -> DPState era
forall era. LedgerState era -> DPState era
_delegationState LedgerState era
ls
SnapShots era
ss' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (SNAP era) super =>
RuleContext rtype (SNAP era) -> Rule super rtype (State (SNAP era))
trans @(SNAP era) (RuleContext 'Transition (SNAP era)
-> Rule (EPOCH era) 'Transition (State (SNAP era)))
-> RuleContext 'Transition (SNAP era)
-> Rule (EPOCH era) 'Transition (State (SNAP era))
forall a b. (a -> b) -> a -> b
$ (Environment (SNAP era), State (SNAP era), Signal (SNAP era))
-> TRC (SNAP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (SNAP era)
LedgerState era
ls, State (SNAP era)
SnapShots era
ss, ())
let PState Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
pParams Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
fPParams Map (KeyHash 'StakePool (Crypto era)) EpochNo
_ = PState era
pstate
ppp :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
ppp = Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
pParams Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams 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 'StakePool (Crypto era)) (PoolParams era)
fPParams)
pstate' :: PState era
pstate' =
PState era
pstate
{ _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams = Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
ppp,
_fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_fPParams = Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall k a. Map k a
Map.empty
}
PoolreapState UTxOState era
utxoSt' AccountState
acnt' DState era
dstate' PState era
pstate'' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (POOLREAP era) super =>
RuleContext rtype (POOLREAP era)
-> Rule super rtype (State (POOLREAP era))
trans @(POOLREAP era) (RuleContext 'Transition (POOLREAP era)
-> Rule (EPOCH era) 'Transition (State (POOLREAP era)))
-> RuleContext 'Transition (POOLREAP era)
-> Rule (EPOCH era) 'Transition (State (POOLREAP era))
forall a b. (a -> b) -> a -> b
$ (Environment (POOLREAP era), State (POOLREAP era),
Signal (POOLREAP era))
-> TRC (POOLREAP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (POOLREAP era)
PParams era
pp, UTxOState era
-> AccountState -> DState era -> PState era -> PoolreapState era
forall era.
UTxOState era
-> AccountState -> DState era -> PState era -> PoolreapState era
PoolreapState UTxOState era
utxoSt AccountState
acnt DState era
dstate PState era
pstate', Signal (POOLREAP era)
Signal (EPOCH era)
e)
Word64
coreNodeQuorum <- BaseM (EPOCH era) Word64 -> Rule (EPOCH era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (EPOCH era) Word64 -> Rule (EPOCH era) 'Transition Word64)
-> BaseM (EPOCH era) Word64 -> Rule (EPOCH era) '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
quorum
let pup :: ProposedPPUpdates era
pup = PPUPState era -> ProposedPPUpdates era
forall era. PPUPState era -> ProposedPPUpdates era
proposals (PPUPState era -> ProposedPPUpdates era)
-> (UTxOState era -> PPUPState era)
-> UTxOState era
-> ProposedPPUpdates era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState era -> PPUPState era
forall era. UTxOState era -> PPUPState era
_ppups (UTxOState era -> ProposedPPUpdates era)
-> UTxOState era -> ProposedPPUpdates era
forall a b. (a -> b) -> a -> b
$ UTxOState era
utxoSt'
let ppNew :: Maybe (PParams era)
ppNew = ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
forall era.
ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
votedValue ProposedPPUpdates era
pup PParams era
pp (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
coreNodeQuorum)
NewppState UTxOState era
utxoSt'' AccountState
acnt'' PParams era
pp' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (NEWPP era) super =>
RuleContext rtype (NEWPP era)
-> Rule super rtype (State (NEWPP era))
trans @(NEWPP era) (RuleContext 'Transition (NEWPP era)
-> Rule (EPOCH era) 'Transition (State (NEWPP era)))
-> RuleContext 'Transition (NEWPP era)
-> Rule (EPOCH era) 'Transition (State (NEWPP era))
forall a b. (a -> b) -> a -> b
$
(Environment (NEWPP era), State (NEWPP era), Signal (NEWPP era))
-> TRC (NEWPP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (DState era -> PState era -> NewppEnv era
forall era. DState era -> PState era -> NewppEnv era
NewppEnv DState era
dstate' PState era
pstate'', UTxOState era -> AccountState -> PParams era -> NewppState era
forall era.
UTxOState era -> AccountState -> PParams era -> NewppState era
NewppState UTxOState era
utxoSt' AccountState
acnt' PParams era
pp, Maybe (PParams era)
Signal (NEWPP era)
ppNew)
EpochState era
-> F (Clause (EPOCH era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
-> F (Clause (EPOCH era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (EPOCH era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
EpochState
AccountState
acnt''
SnapShots era
ss'
(LedgerState era
ls {_utxoState :: UTxOState era
_utxoState = UTxOState era
utxoSt'', _delegationState :: DPState era
_delegationState = DState era -> PState era -> DPState era
forall era. DState era -> PState era -> DPState era
DPState DState era
dstate' PState era
pstate''})
PParams era
pp
PParams era
pp'
NonMyopic era
nm
instance ShelleyBased era => Embed (SNAP era) (EPOCH era) where
wrapFailed :: PredicateFailure (SNAP era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (SNAP era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (SNAP era) -> EpochPredicateFailure era
SnapFailure
instance ShelleyBased era => Embed (POOLREAP era) (EPOCH era) where
wrapFailed :: PredicateFailure (POOLREAP era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (POOLREAP era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (POOLREAP era) -> EpochPredicateFailure era
PoolReapFailure
instance ShelleyBased era => Embed (NEWPP era) (EPOCH era) where
wrapFailed :: PredicateFailure (NEWPP era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (NEWPP era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (NEWPP era) -> EpochPredicateFailure era
NewPpFailure