{-# 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.Class (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 (EraCrypto era)
  , 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 (EraCrypto era),
 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 (EraCrypto era)
  , 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 (EraCrypto era),
 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 (EraCrypto era)
esSnapshots = SnapShots (EraCrypto era)
ss
          , esLState :: forall era. EpochState era -> LedgerState era
esLState = LedgerState era
ls
          , esNonMyopic :: forall era. EpochState era -> NonMyopic (EraCrypto era)
esNonMyopic = NonMyopic (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era)
ss, ())

  let PState Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
pParams Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
fPParams Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
_ Map (KeyHash 'StakePool (EraCrypto era)) Coin
_ = PState era
pstate
      ppp :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
ppp = forall s t. Embed s t => Exp t -> s
eval (Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era)) (PoolParams (EraCrypto era))
fPParams)
      pstate' :: PState era
pstate' =
        PState era
pstate
          { psStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams = Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
ppp
          , psFutureStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era)
-> NonMyopic (EraCrypto era)
-> EpochState era
EpochState AccountState
acnt' LedgerState era
ls' SnapShots (EraCrypto era)
ss' NonMyopic (EraCrypto era)
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