{-# 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)) -- Subtransition Failures
  | SnapFailure (PredicateFailure (SNAP era)) -- Subtransition Failures
  | NewPpFailure (PredicateFailure (NEWPP era)) -- Subtransition Failures
  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
        -- NOTE that `quorumN` is a global constant, and that we require
        -- it to be strictly greater than half the number of genesis nodes.
        -- The keys in the `pup` correspond to the genesis nodes,
        -- and therefore either:
        --   1) `consensus` is empty, or
        --   2) `consensus` has exactly one element.
        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
        -- NOTE that `updatePParams` corresponds to the union override right
        -- operation in the formal spec.
        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