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

module Cardano.Ledger.Shelley.Rules.Epoch (
  ShelleyEPOCH,
  ShelleyEpochPredFailure (..),
  ShelleyEpochEvent (..),
  PredicateFailure,
  UpecPredFailure,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.EpochBoundary (SnapShots)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEPOCH)
import Cardano.Ledger.Shelley.LedgerState (
  EpochState,
  LedgerState,
  PState (..),
  UTxOState (utxosDeposited, utxosGovState),
  curPParamsEpochStateL,
  esAccountState,
  esLState,
  esLStateL,
  esNonMyopic,
  esSnapshots,
  lsCertState,
  lsUTxOState,
  lsUTxOStateL,
  totalObligation,
  utxosGovStateL,
  pattern CertState,
  pattern EpochState,
 )
import Cardano.Ledger.Shelley.LedgerState.Types (prevPParamsEpochStateL)
import Cardano.Ledger.Shelley.Rewards ()
import Cardano.Ledger.Shelley.Rules.PoolReap (
  ShelleyPOOLREAP,
  ShelleyPoolreapEnv (..),
  ShelleyPoolreapEvent,
  ShelleyPoolreapPredFailure,
  ShelleyPoolreapState (..),
 )
import Cardano.Ledger.Shelley.Rules.Snap (
  ShelleySNAP,
  ShelleySnapPredFailure,
  SnapEnv (..),
  SnapEvent,
 )
import Cardano.Ledger.Shelley.Rules.Upec (ShelleyUPEC, ShelleyUpecPredFailure, UpecState (..))
import Cardano.Ledger.Slot (EpochNo)
import Control.DeepSeq (NFData)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
 )
import Data.Default (Default)
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))

type UpecPredFailure era = UpecPredFailurePV (ProtVerLow era) era

type family UpecPredFailurePV pv era where
  UpecPredFailurePV 2 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 3 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 4 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 5 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 6 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 7 era = ShelleyUpecPredFailure era
  UpecPredFailurePV 8 era = ShelleyUpecPredFailure era
  UpecPredFailurePV _ era = Void

data ShelleyEpochPredFailure era
  = PoolReapFailure (PredicateFailure (EraRule "POOLREAP" era)) -- Subtransition Failures
  | SnapFailure (PredicateFailure (EraRule "SNAP" era)) -- Subtransition Failures
  | UpecFailure (UpecPredFailure era) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyEpochPredFailure era) x -> ShelleyEpochPredFailure era
forall era x.
ShelleyEpochPredFailure era -> Rep (ShelleyEpochPredFailure era) x
$cto :: forall era x.
Rep (ShelleyEpochPredFailure era) x -> ShelleyEpochPredFailure era
$cfrom :: forall era x.
ShelleyEpochPredFailure era -> Rep (ShelleyEpochPredFailure era) x
Generic)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "POOLREAP" era))
  , Eq (PredicateFailure (EraRule "SNAP" era))
  , Eq (UpecPredFailure era)
  ) =>
  Eq (ShelleyEpochPredFailure era)

deriving stock instance
  ( Show (PredicateFailure (EraRule "POOLREAP" era))
  , Show (PredicateFailure (EraRule "SNAP" era))
  , Show (UpecPredFailure era)
  ) =>
  Show (ShelleyEpochPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "POOLREAP" era))
  , NFData (PredicateFailure (EraRule "SNAP" era))
  , NFData (UpecPredFailure era)
  ) =>
  NFData (ShelleyEpochPredFailure era)

data ShelleyEpochEvent era
  = PoolReapEvent (Event (EraRule "POOLREAP" era))
  | SnapEvent (Event (EraRule "SNAP" era))
  | UpecEvent (Event (EraRule "UPEC" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
forall era x.
ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
$cto :: forall era x.
Rep (ShelleyEpochEvent era) x -> ShelleyEpochEvent era
$cfrom :: forall era x.
ShelleyEpochEvent era -> Rep (ShelleyEpochEvent era) x
Generic)

deriving instance
  ( Eq (Event (EraRule "POOLREAP" era))
  , Eq (Event (EraRule "SNAP" era))
  , Eq (Event (EraRule "UPEC" era))
  ) =>
  Eq (ShelleyEpochEvent era)

instance
  ( NFData (Event (EraRule "POOLREAP" era))
  , NFData (Event (EraRule "SNAP" era))
  , NFData (Event (EraRule "UPEC" era))
  ) =>
  NFData (ShelleyEpochEvent era)

instance
  ( EraTxOut era
  , EraGov era
  , GovState era ~ ShelleyGovState era
  , Embed (EraRule "SNAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "SNAP" era) ~ SnapEnv era
  , State (EraRule "SNAP" era) ~ SnapShots
  , Signal (EraRule "SNAP" era) ~ ()
  , Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "POOLREAP" era) ~ ShelleyPoolreapEnv era
  , State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era
  , Signal (EraRule "POOLREAP" era) ~ EpochNo
  , Embed (EraRule "UPEC" era) (ShelleyEPOCH era)
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , State (EraRule "UPEC" era) ~ UpecState era
  , Signal (EraRule "UPEC" era) ~ ()
  , Default (PParams era)
  , Eq (UpecPredFailure era)
  , Show (UpecPredFailure era)
  ) =>
  STS (ShelleyEPOCH era)
  where
  type State (ShelleyEPOCH era) = EpochState era
  type Signal (ShelleyEPOCH era) = EpochNo
  type Environment (ShelleyEPOCH era) = ()
  type BaseM (ShelleyEPOCH era) = ShelleyBase
  type PredicateFailure (ShelleyEPOCH era) = ShelleyEpochPredFailure era
  type Event (ShelleyEPOCH era) = ShelleyEpochEvent era
  transitionRules :: [TransitionRule (ShelleyEPOCH era)]
transitionRules = [forall era.
(Embed (EraRule "SNAP" era) (ShelleyEPOCH era),
 Environment (EraRule "SNAP" era) ~ SnapEnv era,
 State (EraRule "SNAP" era) ~ SnapShots,
 Signal (EraRule "SNAP" era) ~ (),
 Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era),
 Environment (EraRule "POOLREAP" era) ~ ShelleyPoolreapEnv era,
 State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era,
 Signal (EraRule "POOLREAP" era) ~ EpochNo,
 Embed (EraRule "UPEC" era) (ShelleyEPOCH era),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 GovState era ~ ShelleyGovState era, EraGov era) =>
TransitionRule (ShelleyEPOCH era)
epochTransition]

instance
  ( NoThunks (PredicateFailure (EraRule "POOLREAP" era))
  , NoThunks (PredicateFailure (EraRule "SNAP" era))
  , NoThunks (UpecPredFailure era)
  ) =>
  NoThunks (ShelleyEpochPredFailure era)

epochTransition ::
  forall era.
  ( Embed (EraRule "SNAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "SNAP" era) ~ SnapEnv era
  , State (EraRule "SNAP" era) ~ SnapShots
  , Signal (EraRule "SNAP" era) ~ ()
  , Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era)
  , Environment (EraRule "POOLREAP" era) ~ ShelleyPoolreapEnv era
  , State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era
  , Signal (EraRule "POOLREAP" era) ~ EpochNo
  , Embed (EraRule "UPEC" era) (ShelleyEPOCH era)
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , State (EraRule "UPEC" era) ~ UpecState era
  , Signal (EraRule "UPEC" era) ~ ()
  , GovState era ~ ShelleyGovState era
  , EraGov era
  ) =>
  TransitionRule (ShelleyEPOCH era)
epochTransition :: forall era.
(Embed (EraRule "SNAP" era) (ShelleyEPOCH era),
 Environment (EraRule "SNAP" era) ~ SnapEnv era,
 State (EraRule "SNAP" era) ~ SnapShots,
 Signal (EraRule "SNAP" era) ~ (),
 Embed (EraRule "POOLREAP" era) (ShelleyEPOCH era),
 Environment (EraRule "POOLREAP" era) ~ ShelleyPoolreapEnv era,
 State (EraRule "POOLREAP" era) ~ ShelleyPoolreapState era,
 Signal (EraRule "POOLREAP" era) ~ EpochNo,
 Embed (EraRule "UPEC" era) (ShelleyEPOCH era),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 GovState era ~ ShelleyGovState era, EraGov era) =>
TransitionRule (ShelleyEPOCH era)
epochTransition = do
  TRC
    ( Environment (ShelleyEPOCH era)
_
      , es :: State (ShelleyEPOCH era)
es@EpochState
          { esAccountState :: forall era. EpochState era -> AccountState
esAccountState = AccountState
acnt
          , esSnapshots :: forall era. EpochState era -> SnapShots
esSnapshots = SnapShots
ss
          , esLState :: forall era. EpochState era -> LedgerState era
esLState = LedgerState era
ls
          , esNonMyopic :: forall era. EpochState era -> NonMyopic
esNonMyopic = NonMyopic
nm
          }
      , Signal (ShelleyEPOCH era)
e
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pp :: PParams era
pp = State (ShelleyEPOCH era)
es forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
      utxoSt :: UTxOState era
utxoSt = forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls
      CertState VState era
vstate PState era
pstate DState era
dstate = forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls
  SnapShots
ss' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "SNAP" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. LedgerState era -> PParams era -> SnapEnv era
SnapEnv LedgerState era
ls PParams era
pp, SnapShots
ss, ())

  let PState Map (KeyHash 'StakePool) PoolParams
pParams Map (KeyHash 'StakePool) PoolParams
fPParams Map (KeyHash 'StakePool) EpochNo
_ Map (KeyHash 'StakePool) Coin
_ = PState era
pstate
      ppp :: Map (KeyHash 'StakePool) PoolParams
ppp = forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool) PoolParams
pParams 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) PoolParams
fPParams)
      pstate' :: PState era
pstate' =
        PState era
pstate
          { psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams = Map (KeyHash 'StakePool) PoolParams
ppp
          , psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams = 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)
trans @(EraRule "POOLREAP" era) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. VState era -> ShelleyPoolreapEnv era
ShelleyPoolreapEnv VState era
vstate, forall era.
UTxOState era
-> AccountState
-> DState era
-> PState era
-> ShelleyPoolreapState era
PoolreapState UTxOState era
utxoSt AccountState
acnt DState era
dstate PState era
pstate', Signal (ShelleyEPOCH era)
e)

  let adjustedCertState :: CertState era
adjustedCertState = forall era. VState era -> PState era -> DState era -> CertState era
CertState VState era
vstate PState era
pstate'' DState era
dstate'
      ls' :: LedgerState era
ls' = LedgerState era
ls {lsUTxOState :: UTxOState era
lsUTxOState = UTxOState era
utxoSt', lsCertState :: CertState era
lsCertState = CertState era
adjustedCertState}

  UpecState PParams era
pp' ShelleyGovState era
ppupSt' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UPEC" era) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerState era
ls', forall era. PParams era -> ShelleyGovState era -> UpecState era
UpecState PParams era
pp (forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
utxoSt'), ())
  let utxoSt'' :: UTxOState era
utxoSt'' = UTxOState era
utxoSt' {utxosGovState :: GovState era
utxosGovState = ShelleyGovState era
ppupSt'}

  let
    -- At the epoch boundary refunds are made, so we need to change what
    -- the utxosDeposited field is. The other two places where deposits are
    -- kept (dsUnified of DState and psDeposits of PState) are adjusted by
    -- the rules, So we can recompute the utxosDeposited field using adjustedCertState
    -- since we have the invariant that: obligationCertState dpstate == utxosDeposited utxostate
    oblgNew :: Coin
oblgNew = forall era. EraGov era => CertState era -> GovState era -> Coin
totalObligation CertState era
adjustedCertState (UTxOState era
utxoSt'' forall s a. s -> Getting a s a -> a
^. forall era. Lens' (UTxOState era) (GovState era)
utxosGovStateL)
    utxoSt''' :: UTxOState era
utxoSt''' = UTxOState era
utxoSt'' {utxosDeposited :: Coin
utxosDeposited = Coin
oblgNew}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall era.
AccountState
-> LedgerState era -> SnapShots -> NonMyopic -> EpochState era
EpochState AccountState
acnt' LedgerState era
ls' SnapShots
ss' NonMyopic
nm
      forall a b. a -> (a -> b) -> b
& forall era. Lens' (EpochState era) (LedgerState era)
esLStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (LedgerState era) (UTxOState era)
lsUTxOStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ UTxOState era
utxoSt'''
      forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp
      forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp'

instance
  ( EraTxOut era
  , PredicateFailure (EraRule "SNAP" era) ~ ShelleySnapPredFailure era
  , Event (EraRule "SNAP" era) ~ SnapEvent era
  ) =>
  Embed (ShelleySNAP era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleySNAP era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = forall era.
PredicateFailure (EraRule "SNAP" era)
-> ShelleyEpochPredFailure era
SnapFailure
  wrapEvent :: Event (ShelleySNAP era) -> Event (ShelleyEPOCH era)
wrapEvent = forall era. Event (EraRule "SNAP" era) -> ShelleyEpochEvent era
SnapEvent

instance
  ( Era era
  , STS (ShelleyPOOLREAP era)
  , PredicateFailure (EraRule "POOLREAP" era) ~ ShelleyPoolreapPredFailure era
  , Event (EraRule "POOLREAP" era) ~ ShelleyPoolreapEvent era
  ) =>
  Embed (ShelleyPOOLREAP era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyPOOLREAP era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = forall era.
PredicateFailure (EraRule "POOLREAP" era)
-> ShelleyEpochPredFailure era
PoolReapFailure
  wrapEvent :: Event (ShelleyPOOLREAP era) -> Event (ShelleyEPOCH era)
wrapEvent = forall era. Event (EraRule "POOLREAP" era) -> ShelleyEpochEvent era
PoolReapEvent

instance
  ( Era era
  , STS (ShelleyUPEC era)
  , UpecPredFailure era ~ ShelleyUpecPredFailure era
  , Event (EraRule "UPEC" era) ~ Void
  ) =>
  Embed (ShelleyUPEC era) (ShelleyEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyUPEC era)
-> PredicateFailure (ShelleyEPOCH era)
wrapFailed = forall era. UpecPredFailure era -> ShelleyEpochPredFailure era
UpecFailure
  wrapEvent :: Event (ShelleyUPEC era) -> Event (ShelleyEPOCH era)
wrapEvent = forall era. Event (EraRule "UPEC" era) -> ShelleyEpochEvent era
UpecEvent