{-# 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,
  ShelleyMirPredFailure,
  ShelleyMirEvent (..),
  emptyInstantaneousRewards,
)
where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.CertState (EraCertState)
import Cardano.Ledger.Coin (Coin, addDeltaCoin)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyRole (..))
import Cardano.Ledger.Shelley.Era (ShelleyMIR)
import Cardano.Ledger.Shelley.Governance (EraGov)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  EpochState,
  InstantaneousRewards (..),
  certDStateL,
  curPParamsEpochStateL,
  dsIRewards,
  dsIRewardsL,
  dsUnifiedL,
  esAccountState,
  esLState,
  esLStateL,
  esNonMyopic,
  esSnapshots,
  lsCertStateL,
  prevPParamsEpochStateL,
  rewards,
  pattern EpochState,
 )
import Cardano.Ledger.UMap (compactCoinOrError)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.Val ((<->))
import Control.DeepSeq (NFData)
import Control.SetAlgebra (eval, (∪+))
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 GHC.Generics (Generic)
import Lens.Micro ((&), (.~), (^.))
import NoThunks.Class (NoThunks (..))

data ShelleyMirPredFailure era
  deriving (Int -> ShelleyMirPredFailure era -> ShowS
forall era. Int -> ShelleyMirPredFailure era -> ShowS
forall era. [ShelleyMirPredFailure era] -> ShowS
forall era. ShelleyMirPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyMirPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyMirPredFailure era] -> ShowS
show :: ShelleyMirPredFailure era -> String
$cshow :: forall era. ShelleyMirPredFailure era -> String
showsPrec :: Int -> ShelleyMirPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyMirPredFailure era -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyMirPredFailure era) x -> ShelleyMirPredFailure era
forall era x.
ShelleyMirPredFailure era -> Rep (ShelleyMirPredFailure era) x
$cto :: forall era x.
Rep (ShelleyMirPredFailure era) x -> ShelleyMirPredFailure era
$cfrom :: forall era x.
ShelleyMirPredFailure era -> Rep (ShelleyMirPredFailure era) x
Generic, ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
forall era.
ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
$c/= :: forall era.
ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
== :: ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
$c== :: forall era.
ShelleyMirPredFailure era -> ShelleyMirPredFailure era -> Bool
Eq)

instance NFData (ShelleyMirPredFailure era)

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 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
$cto :: forall era x. Rep (ShelleyMirEvent era) x -> ShelleyMirEvent era
$cfrom :: forall era x. ShelleyMirEvent era -> Rep (ShelleyMirEvent era) x
Generic)

deriving instance Eq (ShelleyMirEvent era)

instance NFData (ShelleyMirEvent era)

instance NoThunks (ShelleyMirPredFailure 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) = ShelleyMirPredFailure era

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

  assertions :: [Assertion (ShelleyMIR era)]
assertions =
    [ 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 r :: EpochState era -> UView (Credential 'Staking) RDPair
r EpochState era
esl = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (EpochState era
esl forall s a. s -> Getting a s a -> a
^. forall era. Lens' (EpochState era) (LedgerState era)
esLStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL)
             in forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {era}.
EraCertState era =>
EpochState era -> UView (Credential 'Staking) RDPair
r State (ShelleyMIR era)
st) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {era}.
EraCertState era =>
EpochState era -> UView (Credential 'Staking) RDPair
r State (ShelleyMIR 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
    ( Environment (ShelleyMIR era)
_
      , es :: State (ShelleyMIR 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
          }
      , ()
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pr :: PParams era
pr = State (ShelleyMIR era)
es forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL
      pp :: PParams era
pp = State (ShelleyMIR era)
es forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
      dpState :: CertState era
dpState = LedgerState era
ls forall s a. s -> Getting a s a -> a
^. forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL
      ds :: DState era
ds = CertState era
dpState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL
      rewards' :: UView (Credential 'Staking) RDPair
rewards' = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
ds
      reserves :: Coin
reserves = AccountState -> Coin
asReserves AccountState
acnt
      treasury :: Coin
treasury = AccountState -> Coin
asTreasury AccountState
acnt
      irwdR :: Map (Credential 'Staking) Coin
irwdR = UView (Credential 'Staking) RDPair
rewards' forall k v u. UView k v -> Map k u -> Map k u
UM.◁ InstantaneousRewards -> Map (Credential 'Staking) Coin
iRReserves (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) :: Map.Map (Credential 'Staking) Coin
      irwdT :: Map (Credential 'Staking) Coin
irwdT = UView (Credential 'Staking) RDPair
rewards' forall k v u. UView k v -> Map k u -> Map k u
UM.◁ InstantaneousRewards -> Map (Credential 'Staking) Coin
iRTreasury (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) :: Map.Map (Credential 'Staking) Coin
      totR :: Coin
totR = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
irwdR
      totT :: Coin
totT = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
irwdT
      availableReserves :: Coin
availableReserves = Coin
reserves Coin -> DeltaCoin -> Coin
`addDeltaCoin` InstantaneousRewards -> DeltaCoin
deltaReserves (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds)
      availableTreasury :: Coin
availableTreasury = Coin
treasury Coin -> DeltaCoin -> Coin
`addDeltaCoin` InstantaneousRewards -> DeltaCoin
deltaTreasury (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds)
      update :: Map (Credential 'Staking) Coin
update = forall s t. Embed s t => Exp t -> s
eval (Map (Credential 'Staking) Coin
irwdR forall k n s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) =>
s1 -> s2 -> Exp (f k n)
∪+ Map (Credential 'Staking) Coin
irwdT) :: Map.Map (Credential 'Staking) Coin

  if Coin
totR forall a. Ord a => a -> a -> Bool
<= Coin
availableReserves Bool -> Bool -> Bool
&& Coin
totT forall a. Ord a => a -> a -> Bool
<= Coin
availableTreasury
    then do
      forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. InstantaneousRewards -> ShelleyMirEvent era
MirTransfer ((forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) {iRReserves :: Map (Credential 'Staking) Coin
iRReserves = Map (Credential 'Staking) Coin
irwdR, iRTreasury :: Map (Credential 'Staking) Coin
iRTreasury = Map (Credential 'Staking) Coin
irwdT})
      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
            { asReserves :: Coin
asReserves = Coin
availableReserves forall t. Val t => t -> t -> t
<-> Coin
totR
            , asTreasury :: Coin
asTreasury = Coin
availableTreasury forall t. Val t => t -> t -> t
<-> Coin
totT
            }
          ( LedgerState era
ls
              forall a b. a -> (a -> b) -> b
& forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL forall s t a b. ASetter s t a b -> b -> s -> t
.~ (UView (Credential 'Staking) RDPair
rewards' UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) (CompactForm Coin) -> UMap
UM.∪+ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
compactCoinOrError Map (Credential 'Staking) Coin
update)
              forall a b. a -> (a -> b) -> b
& forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) InstantaneousRewards
dsIRewardsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ InstantaneousRewards
emptyInstantaneousRewards
          )
          SnapShots
ss
          NonMyopic
nm
          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
pr
          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
    else do
      forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$
        forall era.
InstantaneousRewards -> Coin -> Coin -> ShelleyMirEvent era
NoMirTransfer
          ((forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) {iRReserves :: Map (Credential 'Staking) Coin
iRReserves = Map (Credential 'Staking) Coin
irwdR, iRTreasury :: Map (Credential 'Staking) Coin
iRTreasury = Map (Credential 'Staking) Coin
irwdT})
          Coin
availableReserves
          Coin
availableTreasury
      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
              forall a b. a -> (a -> b) -> b
& forall era. Lens' (LedgerState era) (CertState era)
lsCertStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) InstantaneousRewards
dsIRewardsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ InstantaneousRewards
emptyInstantaneousRewards
          )
          SnapShots
ss
          NonMyopic
nm
          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
pr
          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

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