{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Epoch
  ( EPOCH,
    EpochPredicateFailure (..),
    EpochEvent (..),
    PredicateFailure,
  )
where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin (..))
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Era (Crypto))
import Cardano.Ledger.Shelley.Constraints (UsesTxOut, UsesValue)
import Cardano.Ledger.Shelley.EpochBoundary (SnapShots, obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( EpochState,
    LedgerState,
    PState (..),
    UpecState (..),
    esAccountState,
    esLState,
    esNonMyopic,
    esPp,
    esPrevPp,
    esSnapshots,
    lsDPState,
    lsUTxOState,
    rewards,
    _deposited,
    _ppups,
    _reserves,
    pattern DPState,
    pattern EpochState,
  )
import Cardano.Ledger.Shelley.Rewards ()
import Cardano.Ledger.Shelley.Rules.PoolReap (POOLREAP, PoolreapEvent, PoolreapPredicateFailure, PoolreapState (..))
import Cardano.Ledger.Shelley.Rules.Snap (SNAP, SnapEvent, SnapPredicateFailure)
import Cardano.Ledger.Shelley.Rules.Upec (UPEC, UpecPredicateFailure)
import Cardano.Ledger.Slot (EpochNo)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    trans,
  )
import Data.Default.Class (Default)
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import GHC.Generics (Generic)
import GHC.Records
import NoThunks.Class (NoThunks (..))

data EPOCH era

data EpochPredicateFailure era
  = PoolReapFailure (PredicateFailure (Core.EraRule "POOLREAP" era)) -- Subtransition Failures
  | SnapFailure (PredicateFailure (Core.EraRule "SNAP" era)) -- Subtransition Failures
  | UpecFailure (PredicateFailure (Core.EraRule "UPEC" 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 (Core.EraRule "POOLREAP" era)),
    Eq (PredicateFailure (Core.EraRule "SNAP" era)),
    Eq (PredicateFailure (Core.EraRule "UPEC" era))
  ) =>
  Eq (EpochPredicateFailure era)

deriving stock instance
  ( Show (PredicateFailure (Core.EraRule "POOLREAP" era)),
    Show (PredicateFailure (Core.EraRule "SNAP" era)),
    Show (PredicateFailure (Core.EraRule "UPEC" era))
  ) =>
  Show (EpochPredicateFailure era)

data EpochEvent era
  = PoolReapEvent (Event (Core.EraRule "POOLREAP" era))
  | SnapEvent (Event (Core.EraRule "SNAP" era))
  | UpecEvent (Event (Core.EraRule "UPEC" era))

instance
  ( UsesTxOut era,
    UsesValue era,
    Embed (Core.EraRule "SNAP" era) (EPOCH era),
    Environment (Core.EraRule "SNAP" era) ~ LedgerState era,
    State (Core.EraRule "SNAP" era) ~ SnapShots (Crypto era),
    Signal (Core.EraRule "SNAP" era) ~ (),
    Embed (Core.EraRule "POOLREAP" era) (EPOCH era),
    Environment (Core.EraRule "POOLREAP" era) ~ Core.PParams era,
    State (Core.EraRule "POOLREAP" era) ~ PoolreapState era,
    Signal (Core.EraRule "POOLREAP" era) ~ EpochNo,
    Embed (Core.EraRule "UPEC" era) (EPOCH era),
    Environment (Core.EraRule "UPEC" era) ~ EpochState era,
    State (Core.EraRule "UPEC" era) ~ UpecState era,
    Signal (Core.EraRule "UPEC" era) ~ (),
    Default (State (Core.EraRule "PPUP" era)),
    Default (Core.PParams era),
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin
  ) =>
  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
  type Event (EPOCH era) = EpochEvent era
  transitionRules :: [TransitionRule (EPOCH era)]
transitionRules = [TransitionRule (EPOCH era)
forall era.
(Embed (EraRule "SNAP" era) (EPOCH era),
 Environment (EraRule "SNAP" era) ~ LedgerState era,
 State (EraRule "SNAP" era) ~ SnapShots (Crypto era),
 Signal (EraRule "SNAP" era) ~ (),
 Embed (EraRule "POOLREAP" era) (EPOCH era),
 Environment (EraRule "POOLREAP" era) ~ PParams era,
 State (EraRule "POOLREAP" era) ~ PoolreapState era,
 Signal (EraRule "POOLREAP" era) ~ EpochNo,
 Embed (EraRule "UPEC" era) (EPOCH era),
 Environment (EraRule "UPEC" era) ~ EpochState era,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 HasField "_keyDeposit" (PParams era) Coin,
 HasField "_poolDeposit" (PParams era) Coin) =>
TransitionRule (EPOCH era)
epochTransition]

instance
  ( NoThunks (PredicateFailure (Core.EraRule "POOLREAP" era)),
    NoThunks (PredicateFailure (Core.EraRule "SNAP" era)),
    NoThunks (PredicateFailure (Core.EraRule "UPEC" era))
  ) =>
  NoThunks (EpochPredicateFailure era)

epochTransition ::
  forall era.
  ( Embed (Core.EraRule "SNAP" era) (EPOCH era),
    Environment (Core.EraRule "SNAP" era) ~ LedgerState era,
    State (Core.EraRule "SNAP" era) ~ SnapShots (Crypto era),
    Signal (Core.EraRule "SNAP" era) ~ (),
    Embed (Core.EraRule "POOLREAP" era) (EPOCH era),
    Environment (Core.EraRule "POOLREAP" era) ~ Core.PParams era,
    State (Core.EraRule "POOLREAP" era) ~ PoolreapState era,
    Signal (Core.EraRule "POOLREAP" era) ~ EpochNo,
    Embed (Core.EraRule "UPEC" era) (EPOCH era),
    Environment (Core.EraRule "UPEC" era) ~ EpochState era,
    State (Core.EraRule "UPEC" era) ~ UpecState era,
    Signal (Core.EraRule "UPEC" era) ~ (),
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin
  ) =>
  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
lsUTxOState LedgerState era
ls
  let DPState DState (Crypto era)
dstate PState (Crypto era)
pstate = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
lsDPState LedgerState era
ls
  SnapShots (Crypto era)
ss' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "SNAP" era) super =>
RuleContext rtype (EraRule "SNAP" era)
-> Rule super rtype (State (EraRule "SNAP" era))
trans @(Core.EraRule "SNAP" era) (RuleContext 'Transition (EraRule "SNAP" era)
 -> Rule (EPOCH era) 'Transition (State (EraRule "SNAP" era)))
-> RuleContext 'Transition (EraRule "SNAP" era)
-> Rule (EPOCH era) 'Transition (State (EraRule "SNAP" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "SNAP" era), State (EraRule "SNAP" era),
 Signal (EraRule "SNAP" era))
-> TRC (EraRule "SNAP" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "SNAP" era)
LedgerState era
ls, State (EraRule "SNAP" era)
SnapShots (Crypto era)
ss, ())

  let PState Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
pParams Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
fPParams Map (KeyHash 'StakePool (Crypto era)) EpochNo
_ = PState (Crypto era)
pstate
      ppp :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
ppp = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
pParams Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (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 'StakePool (Crypto era)) (PoolParams (Crypto era))
fPParams)
      pstate' :: PState (Crypto era)
pstate' =
        PState (Crypto era)
pstate
          { _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_pParams = Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
ppp,
            _fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_fPParams = Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall k a. Map k a
Map.empty
          }
  PoolreapState UTxOState era
utxoSt' AccountState
acnt' DState (Crypto era)
dstate' PState (Crypto era)
pstate'' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "POOLREAP" era) super =>
RuleContext rtype (EraRule "POOLREAP" era)
-> Rule super rtype (State (EraRule "POOLREAP" era))
trans @(Core.EraRule "POOLREAP" era) (RuleContext 'Transition (EraRule "POOLREAP" era)
 -> Rule (EPOCH era) 'Transition (State (EraRule "POOLREAP" era)))
-> RuleContext 'Transition (EraRule "POOLREAP" era)
-> Rule (EPOCH era) 'Transition (State (EraRule "POOLREAP" era))
forall a b. (a -> b) -> a -> b
$
      (Environment (EraRule "POOLREAP" era),
 State (EraRule "POOLREAP" era), Signal (EraRule "POOLREAP" era))
-> TRC (EraRule "POOLREAP" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (PParams era
Environment (EraRule "POOLREAP" era)
pp, UTxOState era
-> AccountState
-> DState (Crypto era)
-> PState (Crypto era)
-> PoolreapState era
forall era.
UTxOState era
-> AccountState
-> DState (Crypto era)
-> PState (Crypto era)
-> PoolreapState era
PoolreapState UTxOState era
utxoSt AccountState
acnt DState (Crypto era)
dstate PState (Crypto era)
pstate', Signal (EraRule "POOLREAP" era)
Signal (EPOCH era)
e)

  let epochState' :: EpochState era
epochState' =
        AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
          AccountState
acnt'
          SnapShots (Crypto era)
ss'
          (LedgerState era
ls {lsUTxOState :: UTxOState era
lsUTxOState = UTxOState era
utxoSt', lsDPState :: DPState (Crypto era)
lsDPState = DState (Crypto era) -> PState (Crypto era) -> DPState (Crypto era)
forall crypto. DState crypto -> PState crypto -> DPState crypto
DPState DState (Crypto era)
dstate' PState (Crypto era)
pstate''})
          PParams era
pr
          PParams era
pp
          NonMyopic (Crypto era)
nm

  UpecState PParams era
pp' State (EraRule "PPUP" era)
ppupSt' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "UPEC" era) super =>
RuleContext rtype (EraRule "UPEC" era)
-> Rule super rtype (State (EraRule "UPEC" era))
trans @(Core.EraRule "UPEC" era) (RuleContext 'Transition (EraRule "UPEC" era)
 -> Rule (EPOCH era) 'Transition (State (EraRule "UPEC" era)))
-> RuleContext 'Transition (EraRule "UPEC" era)
-> Rule (EPOCH era) 'Transition (State (EraRule "UPEC" era))
forall a b. (a -> b) -> a -> b
$
      (Environment (EraRule "UPEC" era), State (EraRule "UPEC" era),
 Signal (EraRule "UPEC" era))
-> TRC (EraRule "UPEC" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "UPEC" era)
EpochState era
epochState', PParams era -> State (EraRule "PPUP" era) -> UpecState era
forall era.
PParams era -> State (EraRule "PPUP" era) -> UpecState era
UpecState PParams era
pp (UTxOState era -> State (EraRule "PPUP" era)
forall era. UTxOState era -> State (EraRule "PPUP" era)
_ppups UTxOState era
utxoSt'), ())
  let utxoSt'' :: UTxOState era
utxoSt'' = UTxOState era
utxoSt' {_ppups :: State (EraRule "PPUP" era)
_ppups = State (EraRule "PPUP" era)
ppupSt'}

  let Coin Integer
oblgCurr = PParams era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
pp (DState (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
dstate') (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
pstate'')
      Coin Integer
oblgNew = PParams era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
pp' (DState (Crypto era)
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
dstate') (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
pstate'')
      Coin Integer
reserves = AccountState -> Coin
_reserves AccountState
acnt'
      utxoSt''' :: UTxOState era
utxoSt''' = UTxOState era
utxoSt'' {_deposited :: Coin
_deposited = Integer -> Coin
Coin Integer
oblgNew}
      acnt'' :: AccountState
acnt'' = AccountState
acnt' {_reserves :: Coin
_reserves = Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Integer
reserves Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
oblgCurr Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
oblgNew}
  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
$
    EpochState era
epochState'
      { esAccountState :: AccountState
esAccountState = AccountState
acnt'',
        esLState :: LedgerState era
esLState = (EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
epochState') {lsUTxOState :: UTxOState era
lsUTxOState = UTxOState era
utxoSt'''},
        esPrevPp :: PParams era
esPrevPp = PParams era
pp,
        esPp :: PParams era
esPp = PParams era
pp'
      }

instance
  ( UsesTxOut era,
    UsesValue era,
    PredicateFailure (Core.EraRule "SNAP" era) ~ SnapPredicateFailure era,
    Event (Core.EraRule "SNAP" era) ~ SnapEvent era
  ) =>
  Embed (SNAP era) (EPOCH era)
  where
  wrapFailed :: PredicateFailure (SNAP era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (SNAP era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (EraRule "SNAP" era) -> EpochPredicateFailure era
SnapFailure
  wrapEvent :: Event (SNAP era) -> Event (EPOCH era)
wrapEvent = Event (SNAP era) -> Event (EPOCH era)
forall era. Event (EraRule "SNAP" era) -> EpochEvent era
SnapEvent

instance
  ( Era era,
    STS (POOLREAP era),
    PredicateFailure (Core.EraRule "POOLREAP" era) ~ PoolreapPredicateFailure era,
    Event (Core.EraRule "POOLREAP" era) ~ PoolreapEvent era
  ) =>
  Embed (POOLREAP era) (EPOCH era)
  where
  wrapFailed :: PredicateFailure (POOLREAP era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (POOLREAP era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (EraRule "POOLREAP" era)
-> EpochPredicateFailure era
PoolReapFailure
  wrapEvent :: Event (POOLREAP era) -> Event (EPOCH era)
wrapEvent = Event (POOLREAP era) -> Event (EPOCH era)
forall era. Event (EraRule "POOLREAP" era) -> EpochEvent era
PoolReapEvent

instance
  ( Era era,
    STS (UPEC era),
    PredicateFailure (Core.EraRule "UPEC" era) ~ UpecPredicateFailure era,
    Event (Core.EraRule "UPEC" era) ~ Void
  ) =>
  Embed (UPEC era) (EPOCH era)
  where
  wrapFailed :: PredicateFailure (UPEC era) -> PredicateFailure (EPOCH era)
wrapFailed = PredicateFailure (UPEC era) -> PredicateFailure (EPOCH era)
forall era.
PredicateFailure (EraRule "UPEC" era) -> EpochPredicateFailure era
UpecFailure
  wrapEvent :: Event (UPEC era) -> Event (EPOCH era)
wrapEvent = Event (UPEC era) -> Event (EPOCH era)
forall era. Event (EraRule "UPEC" era) -> EpochEvent era
UpecEvent