{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE EmptyDataDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Shelley.Spec.Ledger.STS.Mir ( MIR, PredicateFailure, MirPredicateFailure, ) where import Cardano.Ledger.Era (Crypto) import Cardano.Ledger.Val ((<->)) import Control.SetAlgebra (dom, eval, (∪+), (◁)) import Control.State.Transition ( Assertion (..), InitialRule, STS (..), TRC (..), TransitionRule, judgmentContext, ) import Data.Foldable (fold) import Data.Typeable (Typeable) import GHC.Generics (Generic) import NoThunks.Class (NoThunks (..)) import Shelley.Spec.Ledger.BaseTypes (ShelleyBase) import Shelley.Spec.Ledger.EpochBoundary (emptySnapShots) import Shelley.Spec.Ledger.LedgerState ( AccountState (..), EpochState, InstantaneousRewards (..), RewardAccounts, emptyAccount, emptyInstantaneousRewards, emptyLedgerState, esAccountState, esLState, esNonMyopic, esPp, esPrevPp, esSnapshots, _delegationState, _dstate, _irwd, _rewards, pattern EpochState, ) import Shelley.Spec.Ledger.PParams (emptyPParams) import Shelley.Spec.Ledger.Rewards (emptyNonMyopic) 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) instance NoThunks (MirPredicateFailure era) instance Typeable 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 PredicateFailure (MIR era) = MirPredicateFailure era initialRules :: [InitialRule (MIR era)] initialRules = [InitialRule (MIR era) forall era. InitialRule (MIR era) initialMir] 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 -> RewardAccounts (Crypto era) r = DState (Crypto era) -> RewardAccounts (Crypto era) forall crypto. DState crypto -> RewardAccounts crypto _rewards (DState (Crypto era) -> RewardAccounts (Crypto era)) -> (EpochState era -> DState (Crypto era)) -> EpochState era -> RewardAccounts (Crypto era) forall b c a. (b -> c) -> (a -> b) -> a -> c . DPState (Crypto era) -> DState (Crypto era) forall crypto. DPState crypto -> DState crypto _dstate (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) _delegationState (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 Map (Credential 'Staking (Crypto era)) Coin -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (EpochState era -> Map (Credential 'Staking (Crypto era)) Coin forall era. EpochState era -> RewardAccounts (Crypto era) r State (MIR era) EpochState era st) Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Map (Credential 'Staking (Crypto era)) Coin -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (EpochState era -> Map (Credential 'Staking (Crypto era)) Coin forall era. EpochState era -> RewardAccounts (Crypto era) r State (MIR era) EpochState era st') ) ] initialMir :: InitialRule (MIR era) initialMir :: InitialRule (MIR era) initialMir = EpochState era -> F (Clause (MIR era) 'Initial) (EpochState era) forall (f :: * -> *) a. Applicative f => a -> f a pure (EpochState era -> F (Clause (MIR era) 'Initial) (EpochState era)) -> EpochState era -> F (Clause (MIR era) 'Initial) (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 emptyAccount SnapShots (Crypto era) forall crypto. SnapShots crypto emptySnapShots LedgerState era forall era. LedgerState era emptyLedgerState PParams era forall era. PParams era emptyPParams PParams era forall era. PParams era emptyPParams NonMyopic (Crypto era) forall crypto. NonMyopic crypto emptyNonMyopic 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) _delegationState LedgerState era ls ds :: DState (Crypto era) ds = DPState (Crypto era) -> DState (Crypto era) forall crypto. DPState crypto -> DState crypto _dstate DPState (Crypto era) dpState rewards :: RewardAccounts (Crypto era) rewards = DState (Crypto era) -> RewardAccounts (Crypto era) forall crypto. DState crypto -> RewardAccounts crypto _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 $ (RewardAccounts (Crypto era) -> Exp (Sett (Credential 'Staking (Crypto era)) ()) forall k s (f :: * -> * -> *) v. (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ()) dom RewardAccounts (Crypto era) 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 (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)) -> InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era) forall a b. (a -> b) -> a -> b $ 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 $ (RewardAccounts (Crypto era) -> Exp (Sett (Credential 'Staking (Crypto era)) ()) forall k s (f :: * -> * -> *) v. (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ()) dom RewardAccounts (Crypto era) 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 (InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era)) -> InstantaneousRewards (Crypto era) -> RewardAccounts (Crypto era) forall a b. (a -> b) -> a -> b $ 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 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. (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (f 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 reserves Bool -> Bool -> Bool && Coin totT Coin -> Coin -> Bool forall a. Ord a => a -> a -> Bool <= Coin treasury then 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 reserves Coin -> Coin -> Coin forall t. Val t => t -> t -> t <-> Coin totR, _treasury :: Coin _treasury = Coin treasury Coin -> Coin -> Coin forall t. Val t => t -> t -> t <-> Coin totT } SnapShots (Crypto era) ss LedgerState era ls { _delegationState :: DPState (Crypto era) _delegationState = DPState (Crypto era) dpState { _dstate :: DState (Crypto era) _dstate = DState (Crypto era) ds { _rewards :: RewardAccounts (Crypto era) _rewards = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era) forall s t. Embed s t => Exp t -> s eval ((DState (Crypto era) -> RewardAccounts (Crypto era) forall crypto. DState crypto -> RewardAccounts crypto _rewards DState (Crypto era) ds) RewardAccounts (Crypto era) -> RewardAccounts (Crypto era) -> Exp (RewardAccounts (Crypto era)) forall k n s1 (f :: * -> * -> *) s2. (Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (f k n)) => s1 -> s2 -> Exp (f k n) ∪+ 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 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 { _delegationState :: DPState (Crypto era) _delegationState = DPState (Crypto era) dpState { _dstate :: DState (Crypto era) _dstate = 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