{-# 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.Era (EraCrypto)
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.Class (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 (EraCrypto era))
|
NoMirTransfer (InstantaneousRewards (EraCrypto era)) 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
(EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
r = forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (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
}
, ()
) <-
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 (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards' = forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards DState era
ds
reserves :: Coin
reserves = AccountState -> Coin
asReserves AccountState
acnt
treasury :: Coin
treasury = AccountState -> Coin
asTreasury AccountState
acnt
irwdR :: RewardAccounts (EraCrypto era)
irwdR = UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards' forall c k v u. UView c k v -> Map k u -> Map k u
UM.◁ forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) :: RewardAccounts (EraCrypto era)
irwdT :: RewardAccounts (EraCrypto era)
irwdT = UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards' forall c k v u. UView c k v -> Map k u -> Map k u
UM.◁ forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) :: RewardAccounts (EraCrypto era)
totR :: Coin
totR = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (EraCrypto era)
irwdR
totT :: Coin
totT = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts (EraCrypto era)
irwdT
availableReserves :: Coin
availableReserves = Coin
reserves Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall c. InstantaneousRewards c -> DeltaCoin
deltaReserves (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds)
availableTreasury :: Coin
availableTreasury = Coin
treasury Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall c. InstantaneousRewards c -> DeltaCoin
deltaTreasury (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds)
update :: RewardAccounts (EraCrypto era)
update = forall s t. Embed s t => Exp t -> s
eval (RewardAccounts (EraCrypto era)
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 (EraCrypto era)
irwdT) :: RewardAccounts (EraCrypto era)
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 (EraCrypto era) -> ShelleyMirEvent era
MirTransfer ((forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) {iRReserves :: RewardAccounts (EraCrypto era)
iRReserves = RewardAccounts (EraCrypto era)
irwdR, iRTreasury :: RewardAccounts (EraCrypto era)
iRTreasury = RewardAccounts (EraCrypto era)
irwdT})
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
{ 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 (EraCrypto era)
dsUnified = UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards' forall c.
UView c (Credential 'Staking c) RDPair
-> Map (Credential 'Staking c) (CompactForm Coin) -> UMap c
UM.∪+ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
compactCoinOrError RewardAccounts (EraCrypto era)
update
, dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards = forall c. InstantaneousRewards c
emptyInstantaneousRewards
}
}
}
SnapShots (EraCrypto era)
ss
NonMyopic (EraCrypto era)
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 (EraCrypto era)
-> Coin -> Coin -> ShelleyMirEvent era
NoMirTransfer
((forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) {iRReserves :: RewardAccounts (EraCrypto era)
iRReserves = RewardAccounts (EraCrypto era)
irwdR, iRTreasury :: RewardAccounts (EraCrypto era)
iRTreasury = RewardAccounts (EraCrypto era)
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 (EraCrypto era)
-> NonMyopic (EraCrypto era)
-> EpochState era
EpochState
AccountState
acnt
LedgerState era
ls
{ lsCertState :: CertState era
lsCertState =
CertState era
dpState
{ certDState :: DState era
certDState =
DState era
ds {dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards = forall c. InstantaneousRewards c
emptyInstantaneousRewards}
}
}
SnapShots (EraCrypto era)
ss
NonMyopic (EraCrypto era)
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 c
emptyInstantaneousRewards :: forall c. InstantaneousRewards c
emptyInstantaneousRewards = forall c.
Map (Credential 'Staking c) Coin
-> Map (Credential 'Staking c) Coin
-> DeltaCoin
-> DeltaCoin
-> InstantaneousRewards c
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