{-# 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.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 era r = DState era -> RewardAccounts era forall era. DState era -> RewardAccounts era _rewards (DState era -> RewardAccounts era) -> (EpochState era -> DState era) -> EpochState era -> RewardAccounts era forall b c a. (b -> c) -> (a -> b) -> a -> c . DPState era -> DState era forall era. DPState era -> DState era _dstate (DPState era -> DState era) -> (EpochState era -> DPState era) -> EpochState era -> DState era forall b c a. (b -> c) -> (a -> b) -> a -> c . LedgerState era -> DPState era forall era. LedgerState era -> DPState era _delegationState (LedgerState era -> DPState era) -> (EpochState era -> LedgerState era) -> EpochState era -> DPState 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 era) Coin -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (EpochState era -> Map (Credential 'Staking era) Coin forall era. EpochState era -> RewardAccounts era r State (MIR era) EpochState era st) Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Map (Credential 'Staking era) Coin -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (EpochState era -> Map (Credential 'Staking era) Coin forall era. EpochState era -> RewardAccounts 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 era -> LedgerState era -> PParams era -> PParams era -> NonMyopic era -> EpochState era forall era. AccountState -> SnapShots era -> LedgerState era -> PParams era -> PParams era -> NonMyopic era -> EpochState era EpochState AccountState emptyAccount SnapShots era forall era. SnapShots era emptySnapShots LedgerState era forall era. LedgerState era emptyLedgerState PParams era forall era. PParams era emptyPParams PParams era forall era. PParams era emptyPParams NonMyopic era forall era. NonMyopic era 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 era dpState = LedgerState era -> DPState era forall era. LedgerState era -> DPState era _delegationState LedgerState era ls ds :: DState era ds = DPState era -> DState era forall era. DPState era -> DState era _dstate DPState era dpState rewards :: RewardAccounts era rewards = DState era -> RewardAccounts era forall era. DState era -> RewardAccounts era _rewards DState era ds reserves :: Coin reserves = AccountState -> Coin _reserves AccountState acnt treasury :: Coin treasury = AccountState -> Coin _treasury AccountState acnt irwdR :: RewardAccounts era irwdR = Exp (RewardAccounts era) -> RewardAccounts era forall s t. Embed s t => Exp t -> s eval (Exp (RewardAccounts era) -> RewardAccounts era) -> Exp (RewardAccounts era) -> RewardAccounts era forall a b. (a -> b) -> a -> b $ (RewardAccounts era -> Exp (Sett (Credential 'Staking era) ()) forall k s (f :: * -> * -> *) v. (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ()) dom RewardAccounts era rewards) Exp (Sett (Credential 'Staking era) ()) -> RewardAccounts era -> Exp (RewardAccounts 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 era -> RewardAccounts era forall era. InstantaneousRewards era -> Map (Credential 'Staking era) Coin iRReserves (InstantaneousRewards era -> RewardAccounts era) -> InstantaneousRewards era -> RewardAccounts era forall a b. (a -> b) -> a -> b $ DState era -> InstantaneousRewards era forall era. DState era -> InstantaneousRewards era _irwd DState era ds) :: RewardAccounts era irwdT :: RewardAccounts era irwdT = Exp (RewardAccounts era) -> RewardAccounts era forall s t. Embed s t => Exp t -> s eval (Exp (RewardAccounts era) -> RewardAccounts era) -> Exp (RewardAccounts era) -> RewardAccounts era forall a b. (a -> b) -> a -> b $ (RewardAccounts era -> Exp (Sett (Credential 'Staking era) ()) forall k s (f :: * -> * -> *) v. (Ord k, HasExp s (f k v)) => s -> Exp (Sett k ()) dom RewardAccounts era rewards) Exp (Sett (Credential 'Staking era) ()) -> RewardAccounts era -> Exp (RewardAccounts 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 era -> RewardAccounts era forall era. InstantaneousRewards era -> Map (Credential 'Staking era) Coin iRTreasury (InstantaneousRewards era -> RewardAccounts era) -> InstantaneousRewards era -> RewardAccounts era forall a b. (a -> b) -> a -> b $ DState era -> InstantaneousRewards era forall era. DState era -> InstantaneousRewards era _irwd DState era ds) :: RewardAccounts era totR :: Coin totR = RewardAccounts era -> Coin forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m fold RewardAccounts era irwdR totT :: Coin totT = RewardAccounts era -> Coin forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m fold RewardAccounts era irwdT update :: RewardAccounts era update = (Exp (RewardAccounts era) -> RewardAccounts era forall s t. Embed s t => Exp t -> s eval (RewardAccounts era irwdR RewardAccounts era -> RewardAccounts era -> Exp (RewardAccounts 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 era irwdT)) :: RewardAccounts 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 era -> LedgerState era -> PParams era -> PParams era -> NonMyopic era -> EpochState era forall era. AccountState -> SnapShots era -> LedgerState era -> PParams era -> PParams era -> NonMyopic 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 era ss LedgerState era ls { _delegationState :: DPState era _delegationState = DPState era dpState { _dstate :: DState era _dstate = DState era ds { _rewards :: RewardAccounts era _rewards = Exp (RewardAccounts era) -> RewardAccounts era forall s t. Embed s t => Exp t -> s eval ((DState era -> RewardAccounts era forall era. DState era -> RewardAccounts era _rewards DState era ds) RewardAccounts era -> RewardAccounts era -> Exp (RewardAccounts 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 era update), _irwd :: InstantaneousRewards era _irwd = InstantaneousRewards era forall era. InstantaneousRewards era emptyInstantaneousRewards } } } PParams era pr PParams era pp NonMyopic 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 era -> LedgerState era -> PParams era -> PParams era -> NonMyopic era -> EpochState era forall era. AccountState -> SnapShots era -> LedgerState era -> PParams era -> PParams era -> NonMyopic era -> EpochState era EpochState AccountState acnt SnapShots era ss LedgerState era ls { _delegationState :: DPState era _delegationState = DPState era dpState { _dstate :: DState era _dstate = DState era ds {_irwd :: InstantaneousRewards era _irwd = InstantaneousRewards era forall era. InstantaneousRewards era emptyInstantaneousRewards} } } PParams era pr PParams era pp NonMyopic era nm