{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Mir
  ( MIR,
    PredicateFailure,
    MirPredicateFailure,
    MirEvent (..),
    emptyInstantaneousRewards,
  )
where

import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Coin (Coin, addDeltaCoin)
import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState (..),
    EpochState,
    InstantaneousRewards (..),
    RewardAccounts,
    dpsDState,
    esAccountState,
    esLState,
    esNonMyopic,
    esPp,
    esPrevPp,
    esSnapshots,
    lsDPState,
    rewards,
    _irwd,
    _unified,
    pattern EpochState,
  )
import Cardano.Ledger.Val ((<->))
import Control.SetAlgebra (dom, eval, (∪+), (◁))
import Control.State.Transition
  ( Assertion (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    tellEvent,
  )
import Data.Default.Class (Default)
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import Data.Typeable (Typeable)
import qualified Data.UMap as UM
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data MIR era

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

data MirEvent era
  = MirTransfer (InstantaneousRewards (Crypto era))
  | -- | 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 (Crypto era)) Coin Coin

instance NoThunks (MirPredicateFailure era)

instance (Typeable era, Default (EpochState era)) => STS (MIR era) where
  type State (MIR era) = EpochState era
  type Signal (MIR era) = ()
  type Environment (MIR era) = ()
  type BaseM (MIR era) = ShelleyBase
  type Event (MIR era) = MirEvent era
  type PredicateFailure (MIR era) = MirPredicateFailure era

  transitionRules :: [TransitionRule (MIR era)]
transitionRules = [TransitionRule (MIR era)
forall era. TransitionRule (MIR era)
mirTransition]

  assertions :: [Assertion (MIR era)]
assertions =
    [ String
-> (TRC (MIR era) -> State (MIR era) -> Bool)
-> Assertion (MIR era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
        String
"MIR may not create or remove reward accounts"
        ( \(TRC (Environment (MIR era)
_, State (MIR era)
st, Signal (MIR era)
_)) State (MIR era)
st' ->
            let r :: EpochState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r = DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards (DState (Crypto era)
 -> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin)
-> (EpochState era -> DState (Crypto era))
-> EpochState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
dpsDState (DPState (Crypto era) -> DState (Crypto era))
-> (EpochState era -> DPState (Crypto era))
-> EpochState era
-> DState (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
lsDPState (LedgerState era -> DPState (Crypto era))
-> (EpochState era -> LedgerState era)
-> EpochState era
-> DPState (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState
             in View
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (Credential 'Staking (Crypto era))
  Coin
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall era.
EpochState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r State (MIR era)
EpochState era
st) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== View
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (Credential 'Staking (Crypto era))
  Coin
-> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EpochState era
-> View
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (Credential 'Staking (Crypto era))
     Coin
forall era.
EpochState era
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
r State (MIR era)
EpochState era
st')
        )
    ]

mirTransition :: forall era. TransitionRule (MIR era)
mirTransition :: TransitionRule (MIR era)
mirTransition = do
  TRC
    ( Environment (MIR era)
_,
      EpochState
        { esAccountState = acnt,
          esSnapshots = ss,
          esLState = ls,
          esPrevPp = pr,
          esPp = pp,
          esNonMyopic = nm
        },
      ()
      ) <-
    F (Clause (MIR era) 'Transition) (TRC (MIR era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let dpState :: DPState (Crypto era)
dpState = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
lsDPState LedgerState era
ls
      ds :: DState (Crypto era)
ds = DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
dpsDState DPState (Crypto era)
dpState
      rewards' :: ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' = DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
ds
      reserves :: Coin
reserves = AccountState -> Coin
_reserves AccountState
acnt
      treasury :: Coin
treasury = AccountState -> Coin
_treasury AccountState
acnt
      irwdR :: RewardAccounts (Crypto era)
irwdR = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era))
-> Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' Exp (Sett (Credential 'Staking (Crypto era)) ())
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era))
forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
◁ InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRReserves (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) :: RewardAccounts (Crypto era)
      irwdT :: RewardAccounts (Crypto era)
irwdT = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era))
-> Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall a b. (a -> b) -> a -> b
$ ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Exp (Sett (Credential 'Staking (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' Exp (Sett (Credential 'Staking (Crypto era)) ())
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era))
forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
◁ InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRTreasury (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) :: RewardAccounts (Crypto era)
      totR :: Coin
totR = RewardAccounts (Crypto era) -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (Crypto era)
irwdR
      totT :: Coin
totT = RewardAccounts (Crypto era) -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (Crypto era)
irwdT
      availableReserves :: Coin
availableReserves = Coin
reserves Coin -> DeltaCoin -> Coin
`addDeltaCoin` (InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaReserves (InstantaneousRewards (Crypto era) -> DeltaCoin)
-> (DState (Crypto era) -> InstantaneousRewards (Crypto era))
-> DState (Crypto era)
-> DeltaCoin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd (DState (Crypto era) -> DeltaCoin)
-> DState (Crypto era) -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era)
ds)
      availableTreasury :: Coin
availableTreasury = Coin
treasury Coin -> DeltaCoin -> Coin
`addDeltaCoin` (InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaTreasury (InstantaneousRewards (Crypto era) -> DeltaCoin)
-> (DState (Crypto era) -> InstantaneousRewards (Crypto era))
-> DState (Crypto era)
-> DeltaCoin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd (DState (Crypto era) -> DeltaCoin)
-> DState (Crypto era) -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era)
ds)
      update :: RewardAccounts (Crypto era)
update = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (RewardAccounts (Crypto era)
irwdR RewardAccounts (Crypto era)
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era))
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 (Crypto era)
irwdT) :: RewardAccounts (Crypto era)

  if Coin
totR Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
availableReserves Bool -> Bool -> Bool
&& Coin
totT Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
availableTreasury
    then do
      Event (MIR era) -> Rule (MIR era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (MIR era) -> Rule (MIR era) 'Transition ())
-> Event (MIR era) -> Rule (MIR era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ InstantaneousRewards (Crypto era) -> MirEvent era
forall era. InstantaneousRewards (Crypto era) -> MirEvent era
MirTransfer ((DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) {iRReserves :: RewardAccounts (Crypto era)
iRReserves = RewardAccounts (Crypto era)
irwdR, iRTreasury :: RewardAccounts (Crypto era)
iRTreasury = RewardAccounts (Crypto era)
irwdT})
      EpochState era -> F (Clause (MIR era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
 -> F (Clause (MIR era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (MIR era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$
        AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
          AccountState
acnt
            { _reserves :: Coin
_reserves = Coin
availableReserves Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
totR,
              _treasury :: Coin
_treasury = Coin
availableTreasury Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
totT
            }
          SnapShots (Crypto era)
ss
          LedgerState era
ls
            { lsDPState :: DPState (Crypto era)
lsDPState =
                DPState (Crypto era)
dpState
                  { dpsDState :: DState (Crypto era)
dpsDState =
                      DState (Crypto era)
ds
                        { _unified :: UnifiedMap (Crypto era)
_unified = (ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> RewardAccounts (Crypto era) -> UnifiedMap (Crypto era)
forall cred coin pool ptr k.
(Ord cred, Monoid coin) =>
View coin cred pool ptr k coin
-> Map k coin -> UMap coin cred pool ptr
UM.∪+ RewardAccounts (Crypto era)
update),
                          _irwd :: InstantaneousRewards (Crypto era)
_irwd = InstantaneousRewards (Crypto era)
forall crypto. InstantaneousRewards crypto
emptyInstantaneousRewards
                        }
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic (Crypto era)
nm
    else do
      Event (MIR era) -> Rule (MIR era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (MIR era) -> Rule (MIR era) 'Transition ())
-> Event (MIR era) -> Rule (MIR era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
        InstantaneousRewards (Crypto era) -> Coin -> Coin -> MirEvent era
forall era.
InstantaneousRewards (Crypto era) -> Coin -> Coin -> MirEvent era
NoMirTransfer
          ((DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto era)
ds) {iRReserves :: RewardAccounts (Crypto era)
iRReserves = RewardAccounts (Crypto era)
irwdR, iRTreasury :: RewardAccounts (Crypto era)
iRTreasury = RewardAccounts (Crypto era)
irwdT})
          Coin
availableReserves
          Coin
availableTreasury
      EpochState era -> F (Clause (MIR era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
 -> F (Clause (MIR era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (MIR era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$
        AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
forall era.
AccountState
-> SnapShots (Crypto era)
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic (Crypto era)
-> EpochState era
EpochState
          AccountState
acnt
          SnapShots (Crypto era)
ss
          LedgerState era
ls
            { lsDPState :: DPState (Crypto era)
lsDPState =
                DPState (Crypto era)
dpState
                  { dpsDState :: DState (Crypto era)
dpsDState =
                      DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = InstantaneousRewards (Crypto era)
forall crypto. InstantaneousRewards crypto
emptyInstantaneousRewards}
                  }
            }
          PParams era
pr
          PParams era
pp
          NonMyopic (Crypto era)
nm

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