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

module Cardano.Ledger.Shelley.Rules.Mir (
  ShelleyMIR,
  PredicateFailure,
  ShelleyMirEvent (..),
  emptyInstantaneousRewards,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin, addDeltaCoin, compactCoinOrError)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyRole (..))
import Cardano.Ledger.Shelley.Era (ShelleyMIR)
import Cardano.Ledger.Shelley.LedgerState (
  EpochState,
  curPParamsEpochStateL,
  esChainAccountState,
  esLState,
  esLStateL,
  esNonMyopic,
  esSnapshots,
  lsCertStateL,
  prevPParamsEpochStateL,
  pattern EpochState,
 )
import Cardano.Ledger.State
import Cardano.Ledger.Val ((<->))
import Control.DeepSeq (NFData)
import Control.State.Transition (
  Assertion (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  tellEvent,
 )
import Data.Default (Default)
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro

data ShelleyMirEvent era
  = MirTransfer InstantaneousRewards
  | -- | We were not able to perform an MIR transfer due to insufficient funds.
    --   This event gives the rewards we wanted to pay, plus the available
    --   reserves and treasury.
    NoMirTransfer InstantaneousRewards Coin Coin
  deriving ((forall x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x)
-> (forall x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era)
-> Generic (ShelleyMirEvent era)
forall x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era
forall x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era
forall era x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x
$cfrom :: forall era x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x
from :: forall x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x
$cto :: forall era x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era
to :: forall x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era
Generic)

deriving instance Eq (ShelleyMirEvent era)

instance NFData (ShelleyMirEvent era)

instance
  ( Default (EpochState era)
  , EraGov era
  , EraCertState era
  ) =>
  STS (ShelleyMIR era)
  where
  type State (ShelleyMIR era) = EpochState era
  type Signal (ShelleyMIR era) = ()
  type Environment (ShelleyMIR era) = ()
  type BaseM (ShelleyMIR era) = ShelleyBase
  type Event (ShelleyMIR era) = ShelleyMirEvent era
  type PredicateFailure (ShelleyMIR era) = Void

  transitionRules :: [TransitionRule (ShelleyMIR era)]
transitionRules = [TransitionRule (ShelleyMIR era)
forall era.
(EraGov era, EraCertState era) =>
TransitionRule (ShelleyMIR era)
mirTransition]

  assertions :: [Assertion (ShelleyMIR era)]
assertions =
    [ String
-> (TRC (ShelleyMIR era) -> State (ShelleyMIR era) -> Bool)
-> Assertion (ShelleyMIR era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"MIR may not create or remove reward accounts"
        ( \(TRC (Environment (ShelleyMIR era)
_, State (ShelleyMIR era)
st, Signal (ShelleyMIR era)
_)) State (ShelleyMIR era)
st' ->
            let accountsCount :: EpochState era -> Int
accountsCount EpochState era
esl =
                  Map (Credential Staking) (AccountState era) -> Int
forall k a. Map k a -> Int
Map.size (EpochState era
esl EpochState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (EpochState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (LedgerState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (LedgerState era))
-> EpochState era
-> Const
     (Map (Credential Staking) (AccountState era)) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era
  -> Const
       (Map (Credential Staking) (AccountState era)) (LedgerState era))
 -> EpochState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (EpochState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> LedgerState era
    -> Const
         (Map (Credential Staking) (AccountState era)) (LedgerState era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (EpochState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (CertState era))
-> LedgerState era
-> Const
     (Map (Credential Staking) (AccountState era)) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const
       (Map (Credential Staking) (AccountState era)) (CertState era))
 -> LedgerState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (LedgerState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> CertState era
    -> Const
         (Map (Credential Staking) (AccountState era)) (CertState era))
-> (Map (Credential Staking) (AccountState era)
    -> Const
         (Map (Credential Staking) (AccountState era))
         (Map (Credential Staking) (AccountState era)))
-> LedgerState era
-> Const
     (Map (Credential Staking) (AccountState era)) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (CertState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential Staking) (AccountState era)) (DState era))
-> (Map (Credential Staking) (AccountState era)
    -> Const
         (Map (Credential Staking) (AccountState era))
         (Map (Credential Staking) (AccountState era)))
-> CertState era
-> Const
     (Map (Credential Staking) (AccountState era)) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> (Map (Credential Staking) (AccountState era)
    -> Const
         (Map (Credential Staking) (AccountState era))
         (Map (Credential Staking) (AccountState era)))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL)
             in EpochState era -> Int
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
EpochState era -> Int
accountsCount State (ShelleyMIR era)
EpochState era
st Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== EpochState era -> Int
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
EpochState era -> Int
accountsCount State (ShelleyMIR era)
EpochState era
st'
        )
    ]

mirTransition ::
  forall era.
  (EraGov era, EraCertState era) =>
  TransitionRule (ShelleyMIR era)
mirTransition :: forall era.
(EraGov era, EraCertState era) =>
TransitionRule (ShelleyMIR era)
mirTransition = do
  TRC
    ( _
      , es@EpochState
          { esChainAccountState = chainAccountState
          , esSnapshots = ss
          , esLState = ls
          , esNonMyopic = nm
          }
      , ()
      ) <-
    Rule
  (ShelleyMIR era)
  'Transition
  (RuleContext 'Transition (ShelleyMIR era))
F (Clause (ShelleyMIR era) 'Transition) (TRC (ShelleyMIR era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pr = State (ShelleyMIR era)
EpochState era
es EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL
      pp = State (ShelleyMIR era)
EpochState era
es EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
      dpState = LedgerState era
ls LedgerState era
-> Getting (CertState era) (LedgerState era) (CertState era)
-> CertState era
forall s a. s -> Getting a s a -> a
^. Getting (CertState era) (LedgerState era) (CertState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL
      ds = CertState era
dpState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      accountsMap = DState era
ds DState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
      reserves = ChainAccountState -> Coin
casReserves ChainAccountState
chainAccountState
      treasury = ChainAccountState -> Coin
casTreasury ChainAccountState
chainAccountState
      irwdR = InstantaneousRewards -> Map (Credential Staking) Coin
iRReserves (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) Map (Credential Staking) Coin
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.intersection` Map (Credential Staking) (AccountState era)
accountsMap
      irwdT = InstantaneousRewards -> Map (Credential Staking) Coin
iRTreasury (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) Map (Credential Staking) Coin
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) Coin
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.intersection` Map (Credential Staking) (AccountState era)
accountsMap
      totR = Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) Coin
irwdR
      totT = Map (Credential Staking) Coin -> Coin
forall m. Monoid m => Map (Credential Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential Staking) Coin
irwdT
      availableReserves = Coin
reserves Coin -> DeltaCoin -> Coin
`addDeltaCoin` InstantaneousRewards -> DeltaCoin
deltaReserves (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds)
      availableTreasury = Coin
treasury Coin -> DeltaCoin -> Coin
`addDeltaCoin` InstantaneousRewards -> DeltaCoin
deltaTreasury (DState era -> InstantaneousRewards
forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds)
      update = (Coin -> Coin -> Coin)
-> Map (Credential Staking) Coin
-> Map (Credential Staking) Coin
-> Map (Credential Staking) Coin
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Map (Credential Staking) Coin
irwdR Map (Credential Staking) Coin
irwdT :: Map.Map (Credential Staking) Coin

  if totR <= availableReserves && totT <= availableTreasury
    then do
      tellEvent $ MirTransfer ((dsIRewards ds) {iRReserves = irwdR, iRTreasury = irwdT})
      pure $
        EpochState
          ChainAccountState
            { casReserves = availableReserves <-> totR
            , casTreasury = availableTreasury <-> totT
            }
          ( ls
              & lsCertStateL . certDStateL . accountsL
                %~ addToBalanceAccounts (Map.map compactCoinOrError update)
              & lsCertStateL . certDStateL . dsIRewardsL .~ emptyInstantaneousRewards
          )
          ss
          nm
          & prevPParamsEpochStateL .~ pr
          & curPParamsEpochStateL .~ pp
    else do
      tellEvent $
        NoMirTransfer
          ((dsIRewards ds) {iRReserves = irwdR, iRTreasury = irwdT})
          availableReserves
          availableTreasury
      pure $
        EpochState
          chainAccountState
          ( ls
              & lsCertStateL . certDStateL . dsIRewardsL .~ emptyInstantaneousRewards
          )
          ss
          nm
          & prevPParamsEpochStateL .~ pr
          & curPParamsEpochStateL .~ pp

emptyInstantaneousRewards :: InstantaneousRewards
emptyInstantaneousRewards :: InstantaneousRewards
emptyInstantaneousRewards = Map (Credential Staking) Coin
-> Map (Credential Staking) Coin
-> DeltaCoin
-> DeltaCoin
-> InstantaneousRewards
InstantaneousRewards Map (Credential Staking) Coin
forall k a. Map k a
Map.empty Map (Credential Staking) Coin
forall k a. Map k a
Map.empty DeltaCoin
forall a. Monoid a => a
mempty DeltaCoin
forall a. Monoid a => a
mempty