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

-- | Epoch change registration.
--
-- The rules of this module determine how the update subsystem of the ledger
-- handles the epoch transitions.
module Cardano.Ledger.Shelley.Rules.Upec where

import Cardano.Ledger.BaseTypes (Globals (..), ProtVer, ShelleyBase, StrictMaybe)
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Era)
import Cardano.Ledger.Shelley.Constraints
  ( UsesAuxiliary,
    UsesPParams (mergePPUpdates),
    UsesScript,
    UsesTxBody,
    UsesValue,
  )
import Cardano.Ledger.Shelley.LedgerState
  ( EpochState,
    PPUPState (..),
    UpecState (..),
    esAccountState,
    esLState,
    lsDPState,
    lsUTxOState,
    _ppups,
    pattern DPState,
    pattern EpochState,
  )
import Cardano.Ledger.Shelley.PParams (ProposedPPUpdates (..))
import Cardano.Ledger.Shelley.Rules.Newpp (NEWPP, NewppEnv (..), NewppState (..))
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    judgmentContext,
    liftSTS,
    trans,
  )
import Data.Default.Class (Default)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy (..))
import GHC.Generics (Generic)
import GHC.Records
import NoThunks.Class (NoThunks (..))
import Numeric.Natural (Natural)

-- | Update epoch change
data UPEC era

newtype UpecPredicateFailure era
  = NewPpFailure (PredicateFailure (NEWPP era))
  deriving (UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
(UpecPredicateFailure era -> UpecPredicateFailure era -> Bool)
-> (UpecPredicateFailure era -> UpecPredicateFailure era -> Bool)
-> Eq (UpecPredicateFailure era)
forall era.
UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
$c/= :: forall era.
UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
== :: UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
$c== :: forall era.
UpecPredicateFailure era -> UpecPredicateFailure era -> Bool
Eq, Int -> UpecPredicateFailure era -> ShowS
[UpecPredicateFailure era] -> ShowS
UpecPredicateFailure era -> String
(Int -> UpecPredicateFailure era -> ShowS)
-> (UpecPredicateFailure era -> String)
-> ([UpecPredicateFailure era] -> ShowS)
-> Show (UpecPredicateFailure era)
forall era. Int -> UpecPredicateFailure era -> ShowS
forall era. [UpecPredicateFailure era] -> ShowS
forall era. UpecPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UpecPredicateFailure era] -> ShowS
$cshowList :: forall era. [UpecPredicateFailure era] -> ShowS
show :: UpecPredicateFailure era -> String
$cshow :: forall era. UpecPredicateFailure era -> String
showsPrec :: Int -> UpecPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> UpecPredicateFailure era -> ShowS
Show, (forall x.
 UpecPredicateFailure era -> Rep (UpecPredicateFailure era) x)
-> (forall x.
    Rep (UpecPredicateFailure era) x -> UpecPredicateFailure era)
-> Generic (UpecPredicateFailure era)
forall x.
Rep (UpecPredicateFailure era) x -> UpecPredicateFailure era
forall x.
UpecPredicateFailure era -> Rep (UpecPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (UpecPredicateFailure era) x -> UpecPredicateFailure era
forall era x.
UpecPredicateFailure era -> Rep (UpecPredicateFailure era) x
$cto :: forall era x.
Rep (UpecPredicateFailure era) x -> UpecPredicateFailure era
$cfrom :: forall era x.
UpecPredicateFailure era -> Rep (UpecPredicateFailure era) x
Generic)

instance NoThunks (UpecPredicateFailure era)

instance
  ( UsesAuxiliary era,
    UsesTxBody era,
    UsesScript era,
    UsesValue era,
    UsesPParams era,
    Default (Core.PParams era),
    State (Core.EraRule "PPUP" era) ~ PPUPState era,
    HasField "_keyDeposit" (Core.PParams era) Coin,
    HasField "_maxBBSize" (Core.PParams era) Natural,
    HasField "_maxTxSize" (Core.PParams era) Natural,
    HasField "_maxBHSize" (Core.PParams era) Natural,
    HasField "_poolDeposit" (Core.PParams era) Coin,
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_protocolVersion" (Core.PParamsDelta era) (StrictMaybe ProtVer)
  ) =>
  STS (UPEC era)
  where
  type State (UPEC era) = UpecState era
  type Signal (UPEC era) = ()
  type Environment (UPEC era) = EpochState era
  type BaseM (UPEC era) = ShelleyBase
  type PredicateFailure (UPEC era) = UpecPredicateFailure era
  initialRules :: [InitialRule (UPEC era)]
initialRules = []
  transitionRules :: [TransitionRule (UPEC era)]
transitionRules =
    [ do
        TRC
          ( EpochState
              { esAccountState = acnt,
                esLState = ls
              },
            UpecState pp ppupSt,
            Signal (UPEC era)
_
            ) <-
          F (Clause (UPEC era) 'Transition) (TRC (UPEC era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

        Word64
coreNodeQuorum <- BaseM (UPEC era) Word64 -> Rule (UPEC era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (UPEC era) Word64 -> Rule (UPEC era) 'Transition Word64)
-> BaseM (UPEC era) Word64 -> Rule (UPEC era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum

        let utxoSt :: UTxOState era
utxoSt = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls
            DPState DState (Crypto era)
dstate PState (Crypto era)
pstate = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
lsDPState LedgerState era
ls
            pup :: ProposedPPUpdates era
pup = PPUPState era -> ProposedPPUpdates era
forall era. PPUPState era -> ProposedPPUpdates era
proposals (PPUPState era -> ProposedPPUpdates era)
-> (UTxOState era -> PPUPState era)
-> UTxOState era
-> ProposedPPUpdates era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState era -> PPUPState era
forall era. UTxOState era -> State (EraRule "PPUP" era)
_ppups (UTxOState era -> ProposedPPUpdates era)
-> UTxOState era -> ProposedPPUpdates era
forall a b. (a -> b) -> a -> b
$ UTxOState era
utxoSt
            ppNew :: Maybe (PParams era)
ppNew = ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
forall era.
UsesPParams era =>
ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
votedValue ProposedPPUpdates era
pup PParams era
pp (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
coreNodeQuorum)
        NewppState PParams era
pp' PPUPState era
ppupSt' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (NEWPP era) super =>
RuleContext rtype (NEWPP era)
-> Rule super rtype (State (NEWPP era))
trans @(NEWPP era) (RuleContext 'Transition (NEWPP era)
 -> Rule (UPEC era) 'Transition (State (NEWPP era)))
-> RuleContext 'Transition (NEWPP era)
-> Rule (UPEC era) 'Transition (State (NEWPP era))
forall a b. (a -> b) -> a -> b
$
            (Environment (NEWPP era), State (NEWPP era), Signal (NEWPP era))
-> TRC (NEWPP era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (DState (Crypto era)
-> PState (Crypto era)
-> UTxOState era
-> AccountState
-> NewppEnv era
forall era.
DState (Crypto era)
-> PState (Crypto era)
-> UTxOState era
-> AccountState
-> NewppEnv era
NewppEnv DState (Crypto era)
dstate PState (Crypto era)
pstate UTxOState era
utxoSt AccountState
acnt, PParams era -> PPUPState era -> NewppState era
forall era. PParams era -> PPUPState era -> NewppState era
NewppState PParams era
pp State (EraRule "PPUP" era)
PPUPState era
ppupSt, Maybe (PParams era)
Signal (NEWPP era)
ppNew)
        UpecState era -> F (Clause (UPEC era) 'Transition) (UpecState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpecState era
 -> F (Clause (UPEC era) 'Transition) (UpecState era))
-> UpecState era
-> F (Clause (UPEC era) 'Transition) (UpecState era)
forall a b. (a -> b) -> a -> b
$
          PParams era -> State (EraRule "PPUP" era) -> UpecState era
forall era.
PParams era -> State (EraRule "PPUP" era) -> UpecState era
UpecState PParams era
pp' State (EraRule "PPUP" era)
PPUPState era
ppupSt'
    ]

-- | If at least @n@ nodes voted to change __the same__ protocol parameters to
-- __the same__ values, return the given protocol parameters updated to these
-- values. Here @n@ is the quorum needed.
votedValue ::
  forall era.
  UsesPParams era =>
  ProposedPPUpdates era ->
  -- | Protocol parameters to which the change will be applied.
  Core.PParams era ->
  -- | Quorum needed to change the protocol parameters.
  Int ->
  Maybe (Core.PParams era)
votedValue :: ProposedPPUpdates era -> PParams era -> Int -> Maybe (PParams era)
votedValue (ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pup) PParams era
pps Int
quorumN =
  let incrTally :: k -> Map k a -> a
incrTally k
vote Map k a
tally = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
0 k
vote Map k a
tally
      votes :: Map (PParamsDelta era) Int
votes =
        (PParamsDelta era
 -> Map (PParamsDelta era) Int -> Map (PParamsDelta era) Int)
-> Map (PParamsDelta era) Int
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Map (PParamsDelta era) Int
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr
          (\PParamsDelta era
vote Map (PParamsDelta era) Int
tally -> PParamsDelta era
-> Int -> Map (PParamsDelta era) Int -> Map (PParamsDelta era) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert PParamsDelta era
vote (PParamsDelta era -> Map (PParamsDelta era) Int -> Int
forall a k. (Num a, Ord k) => k -> Map k a -> a
incrTally PParamsDelta era
vote Map (PParamsDelta era) Int
tally) Map (PParamsDelta era) Int
tally)
          (Map (PParamsDelta era) Int
forall k a. Map k a
Map.empty :: Map (Core.PParamsDelta era) Int)
          Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pup
      consensus :: Map (PParamsDelta era) Int
consensus = (Int -> Bool)
-> Map (PParamsDelta era) Int -> Map (PParamsDelta era) Int
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
quorumN) Map (PParamsDelta era) Int
votes
   in case Map (PParamsDelta era) Int -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map (PParamsDelta era) Int
consensus of
        -- NOTE that `quorumN` is a global constant, and that we require
        -- it to be strictly greater than half the number of genesis nodes.
        -- The keys in the `pup` correspond to the genesis nodes,
        -- and therefore either:
        --   1) `consensus` is empty, or
        --   2) `consensus` has exactly one element.
        Int
1 ->
          (PParams era -> Maybe (PParams era)
forall a. a -> Maybe a
Just (PParams era -> Maybe (PParams era))
-> (Map (PParamsDelta era) Int -> PParams era)
-> Map (PParamsDelta era) Int
-> Maybe (PParams era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy era -> PParams era -> PParamsDelta era -> PParams era
forall era (proxy :: * -> *).
UsesPParams era =>
proxy era -> PParams era -> PParamsDelta era -> PParams era
mergePPUpdates (Proxy era
forall k (t :: k). Proxy t
Proxy @era) PParams era
pps (PParamsDelta era -> PParams era)
-> (Map (PParamsDelta era) Int -> PParamsDelta era)
-> Map (PParamsDelta era) Int
-> PParams era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PParamsDelta era, Int) -> PParamsDelta era
forall a b. (a, b) -> a
fst ((PParamsDelta era, Int) -> PParamsDelta era)
-> (Map (PParamsDelta era) Int -> (PParamsDelta era, Int))
-> Map (PParamsDelta era) Int
-> PParamsDelta era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(PParamsDelta era, Int)] -> (PParamsDelta era, Int)
forall a. [a] -> a
head ([(PParamsDelta era, Int)] -> (PParamsDelta era, Int))
-> (Map (PParamsDelta era) Int -> [(PParamsDelta era, Int)])
-> Map (PParamsDelta era) Int
-> (PParamsDelta era, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (PParamsDelta era) Int -> [(PParamsDelta era, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList)
            Map (PParamsDelta era) Int
consensus
        -- NOTE that `updatePParams` corresponds to the union override right
        -- operation in the formal spec.
        Int
_ -> Maybe (PParams era)
forall a. Maybe a
Nothing

instance
  (Era era, STS (NEWPP era)) =>
  Embed (NEWPP era) (UPEC era)
  where
  wrapFailed :: PredicateFailure (NEWPP era) -> PredicateFailure (UPEC era)
wrapFailed = PredicateFailure (NEWPP era) -> PredicateFailure (UPEC era)
forall era.
PredicateFailure (NEWPP era) -> UpecPredicateFailure era
NewPpFailure