{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
module Shelley.Spec.Ledger.STS.Newpp
( NEWPP,
NewppState (..),
NewppEnv (..),
NewppPredicateFailure (..),
PredicateFailure,
)
where
import Control.State.Transition
( InitialRule,
STS (..),
TRC (..),
TransitionRule,
judgmentContext,
(?!),
)
import qualified Data.Map.Strict as Map
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase)
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.EpochBoundary (obligation)
import Shelley.Spec.Ledger.LedgerState
( AccountState,
DState (..),
PState (..),
UTxOState,
emptyAccount,
emptyPPUPState,
totalInstantaneousReservesRewards,
updatePpup,
_deposited,
_irwd,
_reserves,
pattern UTxOState,
)
import Shelley.Spec.Ledger.PParams (PParams, PParams' (..), emptyPParams)
import Shelley.Spec.Ledger.UTxO (UTxO (..))
data NEWPP era
data NewppState era
= NewppState (UTxOState era) AccountState (PParams era)
data NewppEnv era
= NewppEnv (DState era) (PState era)
data NewppPredicateFailure era
= UnexpectedDepositPot
!Coin
!Coin
deriving (Int -> NewppPredicateFailure era -> ShowS
[NewppPredicateFailure era] -> ShowS
NewppPredicateFailure era -> String
(Int -> NewppPredicateFailure era -> ShowS)
-> (NewppPredicateFailure era -> String)
-> ([NewppPredicateFailure era] -> ShowS)
-> Show (NewppPredicateFailure era)
forall era. Int -> NewppPredicateFailure era -> ShowS
forall era. [NewppPredicateFailure era] -> ShowS
forall era. NewppPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NewppPredicateFailure era] -> ShowS
$cshowList :: forall era. [NewppPredicateFailure era] -> ShowS
show :: NewppPredicateFailure era -> String
$cshow :: forall era. NewppPredicateFailure era -> String
showsPrec :: Int -> NewppPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> NewppPredicateFailure era -> ShowS
Show, NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
(NewppPredicateFailure era -> NewppPredicateFailure era -> Bool)
-> (NewppPredicateFailure era -> NewppPredicateFailure era -> Bool)
-> Eq (NewppPredicateFailure era)
forall era.
NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
$c/= :: forall era.
NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
== :: NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
$c== :: forall era.
NewppPredicateFailure era -> NewppPredicateFailure era -> Bool
Eq, (forall x.
NewppPredicateFailure era -> Rep (NewppPredicateFailure era) x)
-> (forall x.
Rep (NewppPredicateFailure era) x -> NewppPredicateFailure era)
-> Generic (NewppPredicateFailure era)
forall x.
Rep (NewppPredicateFailure era) x -> NewppPredicateFailure era
forall x.
NewppPredicateFailure era -> Rep (NewppPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (NewppPredicateFailure era) x -> NewppPredicateFailure era
forall era x.
NewppPredicateFailure era -> Rep (NewppPredicateFailure era) x
$cto :: forall era x.
Rep (NewppPredicateFailure era) x -> NewppPredicateFailure era
$cfrom :: forall era x.
NewppPredicateFailure era -> Rep (NewppPredicateFailure era) x
Generic)
instance NoThunks (NewppPredicateFailure era)
instance Typeable era => STS (NEWPP era) where
type State (NEWPP era) = NewppState era
type Signal (NEWPP era) = Maybe (PParams era)
type Environment (NEWPP era) = NewppEnv era
type BaseM (NEWPP era) = ShelleyBase
type PredicateFailure (NEWPP era) = NewppPredicateFailure era
initialRules :: [InitialRule (NEWPP era)]
initialRules = [InitialRule (NEWPP era)
forall era. InitialRule (NEWPP era)
initialNewPp]
transitionRules :: [TransitionRule (NEWPP era)]
transitionRules = [TransitionRule (NEWPP era)
forall era. TransitionRule (NEWPP era)
newPpTransition]
initialNewPp :: InitialRule (NEWPP era)
initialNewPp :: InitialRule (NEWPP era)
initialNewPp =
NewppState era -> F (Clause (NEWPP era) 'Initial) (NewppState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewppState era
-> F (Clause (NEWPP era) 'Initial) (NewppState era))
-> NewppState era
-> F (Clause (NEWPP era) 'Initial) (NewppState era)
forall a b. (a -> b) -> a -> b
$
UTxOState era -> AccountState -> PParams era -> NewppState era
forall era.
UTxOState era -> AccountState -> PParams era -> NewppState era
NewppState
(UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
forall era.
UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
UTxOState (Map (TxIn era) (TxOut era) -> UTxO era
forall era. Map (TxIn era) (TxOut era) -> UTxO era
UTxO Map (TxIn era) (TxOut era)
forall k a. Map k a
Map.empty) (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) PPUPState era
forall era. PPUPState era
emptyPPUPState)
AccountState
emptyAccount
PParams era
forall era. PParams era
emptyPParams
newPpTransition :: TransitionRule (NEWPP era)
newPpTransition :: TransitionRule (NEWPP era)
newPpTransition = do
TRC (NewppEnv dstate pstate, NewppState utxoSt acnt pp, Signal (NEWPP era)
ppNew) <- F (Clause (NEWPP era) 'Transition) (TRC (NEWPP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case Signal (NEWPP era)
ppNew of
Just ppNew' -> do
let Coin Integer
oblgCurr = PParams era
-> Map (Credential 'Staking era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
forall era.
PParams era
-> Map (Credential 'Staking era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
obligation PParams era
pp (DState era -> Map (Credential 'Staking era) Coin
forall era. DState era -> RewardAccounts era
_rewards DState era
dstate) (PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams PState era
pstate)
Coin Integer
oblgNew = PParams era
-> Map (Credential 'Staking era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
forall era.
PParams era
-> Map (Credential 'Staking era) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Coin
obligation PParams era
ppNew' (DState era -> Map (Credential 'Staking era) Coin
forall era. DState era -> RewardAccounts era
_rewards DState era
dstate) (PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams PState era
pstate)
diff :: Integer
diff = Integer
oblgCurr Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
oblgNew
Coin Integer
reserves = AccountState -> Coin
_reserves AccountState
acnt
Coin Integer
requiredInstantaneousRewards = InstantaneousRewards era -> Coin
forall era. InstantaneousRewards era -> Coin
totalInstantaneousReservesRewards (DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd DState era
dstate)
(Integer -> Coin
Coin Integer
oblgCurr) Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== (UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
utxoSt) Bool
-> PredicateFailure (NEWPP era) -> Rule (NEWPP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Coin -> Coin -> NewppPredicateFailure era
forall era. Coin -> Coin -> NewppPredicateFailure era
UnexpectedDepositPot (Integer -> Coin
Coin Integer
oblgCurr) (UTxOState era -> Coin
forall era. UTxOState era -> Coin
_deposited UTxOState era
utxoSt)
if Integer
reserves Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
diff Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
requiredInstantaneousRewards
Bool -> Bool -> Bool
&& (PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxTxSize PParams era
ppNew' Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxBHSize PParams era
ppNew') Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxBBSize PParams era
ppNew'
then
let utxoSt' :: UTxOState era
utxoSt' = UTxOState era
utxoSt {_deposited :: Coin
_deposited = Integer -> Coin
Coin Integer
oblgNew}
in let acnt' :: AccountState
acnt' = AccountState
acnt {_reserves :: Coin
_reserves = Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Integer
reserves Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
diff}
in NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era))
-> NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> AccountState -> PParams era -> NewppState era
forall era.
UTxOState era -> AccountState -> PParams era -> NewppState era
NewppState (UTxOState era -> PParams era -> UTxOState era
forall era. UTxOState era -> PParams era -> UTxOState era
updatePpup UTxOState era
utxoSt' PParams era
ppNew') AccountState
acnt' PParams era
ppNew'
else NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era))
-> NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> AccountState -> PParams era -> NewppState era
forall era.
UTxOState era -> AccountState -> PParams era -> NewppState era
NewppState (UTxOState era -> PParams era -> UTxOState era
forall era. UTxOState era -> PParams era -> UTxOState era
updatePpup UTxOState era
utxoSt PParams era
pp) AccountState
acnt PParams era
pp
Signal (NEWPP era)
Nothing -> NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era))
-> NewppState era
-> F (Clause (NEWPP era) 'Transition) (NewppState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> AccountState -> PParams era -> NewppState era
forall era.
UTxOState era -> AccountState -> PParams era -> NewppState era
NewppState (UTxOState era -> PParams era -> UTxOState era
forall era. UTxOState era -> PParams era -> UTxOState era
updatePpup UTxOState era
utxoSt PParams era
pp) AccountState
acnt PParams era
pp