{-# 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 -- The total outstanding deposits
      !Coin -- The deposit pot
  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
        -- Note that instantaneous rewards from the treasury are irrelevant here,
        -- since changes in the protocol parameters do not change how much is needed from the treasury
        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