{-# 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 (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)) -- Subtransition Failures
  | RupdFailure (PredicateFailure (RUPD era)) -- Subtransition Failures
  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 era
dp = LedgerState era -> DPState era
forall era. LedgerState era -> DPState era
_delegationState LedgerState era
ls
    ds :: DState era
ds = DPState era -> DState era
forall era. DPState era -> DState era
_dstate DPState era
dp
    fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs = DState era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall era.
DState era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs DState era
ds
    GenDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs = DState era -> GenDelegs (Crypto era)
forall era. DState era -> GenDelegs (Crypto era)
_genDelegs DState 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 era
ds' =
      DState 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 era
dp' = DPState era
dp {_dstate :: DState era
_dstate = DState era
ds'}
    ls' :: LedgerState era
ls' = LedgerState era
ls {_delegationState :: DPState era
_delegationState = DPState era
dp'}
    es' :: EpochState era
es' = EpochState era
es {esLState :: LedgerState era
esLState = LedgerState era
ls'}

-- | This is a limited version of 'bheadTransition' which is suitable for the
-- future ledger view.
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 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 era -> EpochState era -> RupdEnv era
forall era. BlocksMade era -> EpochState era -> RupdEnv era
RupdEnv BlocksMade era
bprev EpochState era
es, NewEpochState era -> StrictMaybe (RewardUpdate era)
forall era. NewEpochState era -> StrictMaybe (RewardUpdate era)
nesRu NewEpochState era
nes', Signal (RUPD era)
Signal (TICK era)
slot)

  let nes'' :: NewEpochState era
nes'' = NewEpochState era
nes' {nesRu :: StrictMaybe (RewardUpdate era)
nesRu = StrictMaybe (RewardUpdate 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

{------------------------------------------------------------------------------
-- TICKF transition

-- This is a variant on the TICK transition called only by the consensus layer
to tick the ledger state to a future slot.
------------------------------------------------------------------------------}

data TICKF era

data TickfPredicateFailure era
  = TickfNewEpochFailure (PredicateFailure (NEWEPOCH era)) -- Subtransition Failures
  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