{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Newpp
  ( NEWPP,
    NewppState (..),
    NewppEnv (..),
    NewppPredicateFailure (..),
    PredicateFailure,
  )
where

import Cardano.Ledger.BaseTypes (ProtVer, ShelleyBase, StrictMaybe)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core (PParamsDelta)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Shelley.EpochBoundary (obligation)
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState,
    DState (..),
    PPUPState (..),
    PState (..),
    UTxOState,
    availableAfterMIR,
    pvCanFollow,
    _deposited,
    _irwd,
  )
import Cardano.Ledger.Shelley.PParams
  ( ProposedPPUpdates (..),
    emptyPPPUpdates,
  )
import Cardano.Ledger.Shelley.TxBody (MIRPot (..))
import Control.State.Transition
  ( STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    (?!),
  )
import Data.Default.Class (Default, def)
import Data.Typeable (Typeable)
import Data.UMap (rewView)
import GHC.Generics (Generic)
import GHC.Natural (Natural)
import GHC.Records
import NoThunks.Class (NoThunks (..))

data NEWPP era

data NewppState era
  = NewppState (Core.PParams era) (PPUPState era)

data NewppEnv era
  = NewppEnv
      (DState (Crypto era))
      (PState (Crypto era))
      (UTxOState era)
      AccountState

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
  ( Default (Core.PParams era),
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_maxTxSize" (Core.PParams era) Natural,
    HasField "_maxBHSize" (Core.PParams era) Natural,
    HasField "_maxBBSize" (Core.PParams era) Natural,
    HasField "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer),
    Typeable era
  ) =>
  STS (NEWPP era)
  where
  type State (NEWPP era) = NewppState era
  type Signal (NEWPP era) = Maybe (Core.PParams era)
  type Environment (NEWPP era) = NewppEnv era
  type BaseM (NEWPP era) = ShelleyBase
  type PredicateFailure (NEWPP era) = NewppPredicateFailure era
  transitionRules :: [TransitionRule (NEWPP era)]
transitionRules = [TransitionRule (NEWPP era)
forall era.
(HasField "_keyDeposit" (PParams era) Coin,
 HasField "_poolDeposit" (PParams era) Coin,
 HasField "_protocolVersion" (PParams era) ProtVer,
 HasField "_maxTxSize" (PParams era) Natural,
 HasField "_maxBHSize" (PParams era) Natural,
 HasField "_maxBBSize" (PParams era) Natural,
 HasField
   "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)) =>
TransitionRule (NEWPP era)
newPpTransition]

instance Default (Core.PParams era) => Default (NewppState era) where
  def :: NewppState era
def = PParams era -> PPUPState era -> NewppState era
forall era. PParams era -> PPUPState era -> NewppState era
NewppState PParams era
forall a. Default a => a
def PPUPState era
forall a. Default a => a
def

newPpTransition ::
  forall era.
  ( HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_maxTxSize" (Core.PParams era) Natural,
    HasField "_maxBHSize" (Core.PParams era) Natural,
    HasField "_maxBBSize" (Core.PParams era) Natural,
    HasField "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)
  ) =>
  TransitionRule (NEWPP era)
newPpTransition :: TransitionRule (NEWPP era)
newPpTransition = do
  TRC
    ( NewppEnv dstate pstate utxoSt acnt,
      NewppState pp ppupSt,
      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 (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
pp (UMap
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
-> Map (Credential 'Staking (Crypto era)) Coin
forall coin cred pool ptr. UMap coin cred pool ptr -> Map cred coin
rewView (DState (Crypto era)
-> UMap
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
forall crypto. DState crypto -> UnifiedMap crypto
_unified DState (Crypto era)
dstate)) (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
pstate)
          Coin Integer
oblgNew = PParams era
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Coin
forall crypto pp (anymap :: * -> * -> *).
(HasField "_keyDeposit" pp Coin, HasField "_poolDeposit" pp Coin,
 Foldable (anymap (Credential 'Staking crypto))) =>
pp
-> anymap (Credential 'Staking crypto) Coin
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Coin
obligation PParams era
ppNew' (UMap
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
-> Map (Credential 'Staking (Crypto era)) Coin
forall coin cred pool ptr. UMap coin cred pool ptr -> Map cred coin
rewView (DState (Crypto era)
-> UMap
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
forall crypto. DState crypto -> UnifiedMap crypto
_unified DState (Crypto era)
dstate)) (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams PState (Crypto era)
pstate)
          diff :: Integer
diff = Integer
oblgCurr Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
oblgNew
          Coin Integer
availableReserves = MIRPot -> AccountState -> InstantaneousRewards (Crypto era) -> Coin
forall crypto.
MIRPot -> AccountState -> InstantaneousRewards crypto -> Coin
availableAfterMIR MIRPot
ReservesMIR AccountState
acnt (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd DState (Crypto 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
availableReserves Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
diff Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
        -- 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 -> Natural
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_maxTxSize" PParams era
ppNew' Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ PParams era -> Natural
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_maxBHSize" PParams era
ppNew')
          Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< PParams era -> Natural
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_maxBBSize" PParams era
ppNew'
        then 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
$ PParams era -> PPUPState era -> NewppState era
forall era. PParams era -> PPUPState era -> NewppState era
NewppState PParams era
ppNew' (PPUPState era -> PParams era -> PPUPState era
forall era.
(HasField "_protocolVersion" (PParams era) ProtVer,
 HasField
   "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)) =>
PPUPState era -> PParams era -> PPUPState era
updatePpup PPUPState era
ppupSt 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
$ PParams era -> PPUPState era -> NewppState era
forall era. PParams era -> PPUPState era -> NewppState era
NewppState PParams era
pp (PPUPState era -> PParams era -> PPUPState era
forall era.
(HasField "_protocolVersion" (PParams era) ProtVer,
 HasField
   "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)) =>
PPUPState era -> PParams era -> PPUPState era
updatePpup PPUPState era
ppupSt 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
$ PParams era -> PPUPState era -> NewppState era
forall era. PParams era -> PPUPState era -> NewppState era
NewppState PParams era
pp (PPUPState era -> PParams era -> PPUPState era
forall era.
(HasField "_protocolVersion" (PParams era) ProtVer,
 HasField
   "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)) =>
PPUPState era -> PParams era -> PPUPState era
updatePpup PPUPState era
ppupSt PParams era
pp)

-- | Update the protocol parameter updates by clearing out the proposals
-- and making the future proposals become the new proposals,
-- provided the new proposals can follow (otherwise reset them).
updatePpup ::
  ( HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)
  ) =>
  PPUPState era ->
  Core.PParams era ->
  PPUPState era
updatePpup :: PPUPState era -> PParams era -> PPUPState era
updatePpup PPUPState era
ppupSt PParams era
pp = ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
forall era.
ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
PPUPState ProposedPPUpdates era
ps ProposedPPUpdates era
forall era. ProposedPPUpdates era
emptyPPPUpdates
  where
    (ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
newProposals) = PPUPState era -> ProposedPPUpdates era
forall era. PPUPState era -> ProposedPPUpdates era
futureProposals PPUPState era
ppupSt
    goodPV :: PParamsDelta era -> Bool
goodPV =
      ProtVer -> StrictMaybe ProtVer -> Bool
pvCanFollow (PParams era -> ProtVer
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_protocolVersion" PParams era
pp)
        (StrictMaybe ProtVer -> Bool)
-> (PParamsDelta era -> StrictMaybe ProtVer)
-> PParamsDelta era
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "_protocolVersion" r a => r -> a
getField @"_protocolVersion"
    ps :: ProposedPPUpdates era
ps =
      if (PParamsDelta era -> Bool)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PParamsDelta era -> Bool
goodPV Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
newProposals
        then Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
newProposals
        else ProposedPPUpdates era
forall era. ProposedPPUpdates era
emptyPPPUpdates