{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Dijkstra's SNAP rule. Like Shelley's, but the fresh mark snapshot records
-- the epoch, @leiosCommitteeSize@ protocol parameter, and the maximum honoured
-- voting key age, from which the Leios voting committee (CIP-0164) is selected
-- and memoized in the mark snapshot, carrying whichever registered BLS keys are
-- still honoured. The committee is moved into the set position when the mark
-- snapshot rotates.
module Cardano.Ledger.Dijkstra.Rules.Snap (
  maxKeyAgeEpochs,
  kesMaxKeyAgeEpochs,
) where

import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  EpochSize (..),
  Globals (..),
  ShelleyBase,
  epochInfoPure,
  unNonZero,
 )
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Compactible (fromCompact)
import Cardano.Ledger.Conway.Rules (ConwayTickfEvent (..), TICKF)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Dijkstra.Core
import Cardano.Ledger.Dijkstra.Era (SNAP)
import Cardano.Ledger.Dijkstra.PParams (DijkstraEraPParams, ppLeiosCommitteeSizeL)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..), UTxOState (..))
import Cardano.Ledger.Shelley.Rules (SnapEnv (..), SnapEvent (..))
import Cardano.Ledger.Slot (EpochNo)
import Cardano.Ledger.State (
  EraCertState,
  EraStake,
  SnapShot (..),
  SnapShots (..),
  certDStateL,
  certPStateL,
  emptySnapShots,
  instantStakeG,
  mkGoSnapShot,
  mkMarkSnapShot,
  mkSetSnapShot,
  snapShotFromInstantStake,
  swdDelegation,
  swdStake,
  unActiveStake,
 )
import Cardano.Slotting.EpochInfo (epochInfoSize)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  tellEvent,
 )
import Data.Functor.Identity (runIdentity)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Ratio ((%))
import qualified Data.VMap as VMap
import Data.Void (Void)
import Data.Word (Word64)
import Lens.Micro ((^.))

instance
  (EraTxOut era, EraStake era, EraCertState era, DijkstraEraPParams era) =>
  STS (SNAP era)
  where
  type State (SNAP era) = SnapShots era
  type Signal (SNAP era) = EpochNo
  type Environment (SNAP era) = SnapEnv era
  type BaseM (SNAP era) = ShelleyBase
  type PredicateFailure (SNAP era) = Void
  type Event (SNAP era) = SnapEvent era
  initialRules :: [InitialRule (SNAP era)]
initialRules = [SnapShots era -> F (Clause (SNAP era) 'Initial) (SnapShots era)
forall a. a -> F (Clause (SNAP era) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SnapShots era
forall era. SnapShots era
emptySnapShots]
  transitionRules :: [TransitionRule (SNAP era)]
transitionRules = [TransitionRule (SNAP era)
forall era.
(EraTxOut era, EraStake era, EraCertState era,
 DijkstraEraPParams era) =>
TransitionRule (SNAP era)
snapTransition]

instance
  ( EraTxOut era
  , EraStake era
  , EraCertState era
  , DijkstraEraPParams era
  , Event (EraRule "SNAP" era) ~ SnapEvent era
  ) =>
  Embed (SNAP era) (TICKF era)
  where
  wrapFailed :: PredicateFailure (SNAP era) -> PredicateFailure (TICKF era)
wrapFailed = \case {}
  wrapEvent :: Event (SNAP era) -> Event (TICKF era)
wrapEvent = Event (EraRule "SNAP" era) -> ConwayTickfEvent era
Event (SNAP era) -> Event (TICKF era)
forall era. Event (EraRule "SNAP" era) -> ConwayTickfEvent era
TickfSnapEvent

snapTransition ::
  (EraTxOut era, EraStake era, EraCertState era, DijkstraEraPParams era) =>
  TransitionRule (SNAP era)
snapTransition :: forall era.
(EraTxOut era, EraStake era, EraCertState era,
 DijkstraEraPParams era) =>
TransitionRule (SNAP era)
snapTransition = do
  TRC (snapEnv, s, eNo) <- Rule (SNAP era) 'Transition (RuleContext 'Transition (SNAP era))
F (Clause (SNAP era) 'Transition) (TRC (SNAP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  -- 'maxKeyAge' is derived from 'Globals', which the pure snapshot construction
  -- cannot read, so compute it here and memoize in the fresh mark snapshot the
  -- committee it will seat once it rotates into the set position. Measure against
  -- @eNo@ (the epoch we are entering), not a later one: this only needs an epoch
  -- /length/ to turn the KES lifetime into a count of epochs, and a future
  -- epoch's length is past the forecast horizon whenever the stability window is
  -- shorter than an epoch. Note that this measures the key age against the epoch
  -- the mark is created in, rather than the one after it, which is totally fine,
  -- because it cannot be changed without major changes to Ledger and Consensus.
  -- This value depends solely on a config option from 'Globals', which was set
  -- when we entered Shelley era.
  maxKeyAge <- liftSTS $ asks (`maxKeyAgeEpochs` eNo)

  let SnapEnv ls@(LedgerState (UTxOState _utxo _ fees _ _ _) certState) pp = snapEnv
      instantStake = LedgerState era
ls LedgerState era
-> Getting (InstantStake era) (LedgerState era) (InstantStake era)
-> InstantStake era
forall s a. s -> Getting a s a -> a
^. Getting (InstantStake era) (LedgerState era) (InstantStake era)
forall era. SimpleGetter (LedgerState era) (InstantStake era)
forall (t :: * -> *) era.
CanGetInstantStake t =>
SimpleGetter (t era) (InstantStake era)
instantStakeG
      istakeSnap =
        InstantStake era -> DState era -> PState era -> SnapShot
forall era.
EraStake era =>
InstantStake era -> DState era -> PState era -> SnapShot
snapShotFromInstantStake InstantStake era
instantStake (CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL) (CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL)
      markSnapShot = SnapShot -> EpochNo -> Word16 -> EpochInterval -> MarkSnapShot
mkMarkSnapShot SnapShot
istakeSnap EpochNo
Signal (SNAP era)
eNo (PParams era
pp PParams era -> Getting Word16 (PParams era) Word16 -> Word16
forall s a. s -> Getting a s a -> a
^. Getting Word16 (PParams era) Word16
forall era. DijkstraEraPParams era => Lens' (PParams era) Word16
Lens' (PParams era) Word16
ppLeiosCommitteeSizeL) EpochInterval
maxKeyAge

  tellEvent $
    let stakeMap :: Map (Credential Staking) (Coin, KeyHash StakePool)
        stakeMap =
          (StakeWithDelegation -> (Coin, KeyHash StakePool))
-> Map (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) (Coin, KeyHash StakePool)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
            (\StakeWithDelegation
swd -> (CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin) -> CompactForm Coin -> Coin
forall a b. (a -> b) -> a -> b
$ NonZero (CompactForm Coin) -> CompactForm Coin
forall a. NonZero a -> a
unNonZero (NonZero (CompactForm Coin) -> CompactForm Coin)
-> NonZero (CompactForm Coin) -> CompactForm Coin
forall a b. (a -> b) -> a -> b
$ StakeWithDelegation -> NonZero (CompactForm Coin)
swdStake StakeWithDelegation
swd, StakeWithDelegation -> KeyHash StakePool
swdDelegation StakeWithDelegation
swd))
            (VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap (VMap VB VS (Credential Staking) StakeWithDelegation
 -> Map (Credential Staking) StakeWithDelegation)
-> VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall a b. (a -> b) -> a -> b
$ ActiveStake -> VMap VB VS (Credential Staking) StakeWithDelegation
unActiveStake (ActiveStake
 -> VMap VB VS (Credential Staking) StakeWithDelegation)
-> ActiveStake
-> VMap VB VS (Credential Staking) StakeWithDelegation
forall a b. (a -> b) -> a -> b
$ SnapShot -> ActiveStake
ssActiveStake SnapShot
istakeSnap)
     in StakeDistEvent stakeMap

  pure $
    SnapShots
      { -- The mark memoizes the Leios committee (CIP-0164), which is moved into
        -- the 'set' position together with the snapshot upon rotation.
        ssStakeMark = markSnapShot
      , ssStakeSet = mkSetSnapShot (ssStakeMark s)
      , ssStakeGo = mkGoSnapShot (ssStakeSet s)
      , ssFee = fees
      }

-- | Maximum age of a registered Leios voting key (CIP-0164): the KES key
-- lifetime rounded up to whole epochs, plus two epochs of activation delay — a
-- registered key enters the mark snapshot at the next epoch boundary and the
-- active committee at the one after. Deriving the bound from the KES setup keeps
-- voting key rotation in step with the operational key rotation pools do anyway,
-- instead of governing a second cadence through a parameter.
-- The epoch argument only fixes the epoch /length/ used for the conversion, so
-- pass one that is already known -- asking for a future epoch's size can fall
-- past the hard-fork forecast horizon and throw.
maxKeyAgeEpochs :: Globals -> EpochNo -> EpochInterval
maxKeyAgeEpochs :: Globals -> EpochNo -> EpochInterval
maxKeyAgeEpochs Globals
globals EpochNo
e = Word64 -> Word64 -> EpochSize -> EpochInterval
kesMaxKeyAgeEpochs Word64
maxKESEvo Word64
slotsPerKESPeriod EpochSize
epochSize
  where
    -- Safe against the forecast horizon as long as @e@ is an already-known
    -- epoch (see the note above); 'epochInfoPure' is the only handle on the
    -- epoch length 'Globals' offers.
    epochSize :: EpochSize
epochSize = Identity EpochSize -> EpochSize
forall a. Identity a -> a
runIdentity (Identity EpochSize -> EpochSize)
-> Identity EpochSize -> EpochSize
forall a b. (a -> b) -> a -> b
$ EpochInfo Identity -> EpochNo -> Identity EpochSize
forall (m :: * -> *).
HasCallStack =>
EpochInfo m -> EpochNo -> m EpochSize
epochInfoSize (Globals -> EpochInfo Identity
epochInfoPure Globals
globals) EpochNo
e

    Globals {Word64
maxKESEvo :: Word64
maxKESEvo :: Globals -> Word64
maxKESEvo, Word64
slotsPerKESPeriod :: Word64
slotsPerKESPeriod :: Globals -> Word64
slotsPerKESPeriod} = Globals
globals

-- | Same as 'maxKeyAgeEpochs', but computed directly from the KES parameters and the epoch
-- length, for when 'Globals' are not available, e.g. at genesis.
kesMaxKeyAgeEpochs ::
  -- | Maximum number of KES key evolutions
  Word64 ->
  -- | Number of slots per KES period
  Word64 ->
  -- | Epoch length
  EpochSize ->
  EpochInterval
kesMaxKeyAgeEpochs :: Word64 -> Word64 -> EpochSize -> EpochInterval
kesMaxKeyAgeEpochs Word64
maxKESEvo Word64
slotsPerKESPeriod (EpochSize Word64
slotsPerEpoch) =
  Word32 -> EpochInterval
EpochInterval (Word32 -> EpochInterval) -> Word32 -> EpochInterval
forall a b. (a -> b) -> a -> b
$
    Ratio Word64 -> Word32
forall b. Integral b => Ratio Word64 -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling ((Word64
maxKESEvo Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
slotsPerKESPeriod) Word64 -> Word64 -> Ratio Word64
forall a. Integral a => a -> a -> Ratio a
% Word64
slotsPerEpoch) Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+ Word32
2