{-# 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.Coin (Coin, addDeltaCoin)
import Cardano.Ledger.Shelley.Era (ShelleyMIR)
import Cardano.Ledger.Shelley.Governance (EraGov)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  EpochState,
  InstantaneousRewards (..),
  RewardAccounts,
  certDState,
  curPParamsEpochStateL,
  dsIRewards,
  dsUnified,
  esAccountState,
  esLState,
  esNonMyopic,
  esSnapshots,
  lsCertState,
  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
  ) =>
  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 => 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 = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState
             in forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {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}. EpochState era -> UView (Credential 'Staking) RDPair
r State (ShelleyMIR era)
st')
        )
    ]

mirTransition ::
  forall era.
  EraGov era =>
  TransitionRule (ShelleyMIR era)
mirTransition :: forall era. EraGov 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 = forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls
      ds :: DState era
ds = forall era. CertState era -> DState era
certDState CertState era
dpState
      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 :: RewardAccounts
irwdR = UView (Credential 'Staking) RDPair
rewards' forall k v u. UView k v -> Map k u -> Map k u
UM.◁ InstantaneousRewards -> RewardAccounts
iRReserves (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) :: RewardAccounts
      irwdT :: RewardAccounts
irwdT = UView (Credential 'Staking) RDPair
rewards' forall k v u. UView k v -> Map k u -> Map k u
UM.◁ InstantaneousRewards -> RewardAccounts
iRTreasury (forall era. DState era -> InstantaneousRewards
dsIRewards DState era
ds) :: RewardAccounts
      totR :: Coin
totR = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts
irwdR
      totT :: Coin
totT = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts
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 :: RewardAccounts
update = forall s t. Embed s t => Exp t -> s
eval (RewardAccounts
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)
∪+ RewardAccounts
irwdT) :: RewardAccounts

  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 :: RewardAccounts
iRReserves = RewardAccounts
irwdR, iRTreasury :: RewardAccounts
iRTreasury = RewardAccounts
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
            { lsCertState :: CertState era
lsCertState =
                CertState era
dpState
                  { certDState :: DState era
certDState =
                      DState era
ds
                        { dsUnified :: UMap
dsUnified = 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 RewardAccounts
update
                        , dsIRewards :: InstantaneousRewards
dsIRewards = 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 :: RewardAccounts
iRReserves = RewardAccounts
irwdR, iRTreasury :: RewardAccounts
iRTreasury = RewardAccounts
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
            { lsCertState :: CertState era
lsCertState =
                CertState era
dpState
                  { certDState :: DState era
certDState =
                      DState era
ds {dsIRewards :: InstantaneousRewards
dsIRewards = 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 = RewardAccounts
-> RewardAccounts -> 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