{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# 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 seated
-- when the snapshot rotates into the set position, carrying whichever
-- registered BLS keys are still honoured.
module Cardano.Ledger.Dijkstra.Rules.Snap (
  maxKeyAgeEpochs,
) where

import Cardano.Ledger.BaseTypes (
  EpochInterval (..),
  EpochSize (..),
  Globals (..),
  ShelleyBase,
  epochInfoPure,
  unNonZero,
 )
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Compactible (fromCompact)
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,
  MarkSnapShot (..),
  SnapShot (..),
  SnapShots (..),
  calculatePoolDistr,
  certDStateL,
  certPStateL,
  emptySnapShots,
  instantStakeG,
  mkGoSnapShot,
  mkSetSnapShot,
  snapShotFromInstantStake,
  swdDelegation,
  swdStake,
  unActiveStake,
 )
import Cardano.Slotting.EpochInfo (epochInfoSize)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  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 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]

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

  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)
  -- 'maxKeyAge' is derived from 'Globals', which the pure snapshot rotation
  -- cannot read, so compute it here and seat the committee for the mark that is
  -- now rotating into the set position, judging keys for @eNo@. 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.
  maxKeyAge <- liftSTS $ asks (`maxKeyAgeEpochs` eNo)

  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 records the committee size; the Leios committee is seated
        -- from it when this snapshot rotates into the set position (CIP-0164).
        ssStakeMark = MarkSnapShot istakeSnap eNo (pp ^. ppLeiosCommitteeSizeL)
      , -- ssStakeMarkPoolDistr exists for performance reasons, see ADR-7
        ssStakeMarkPoolDistr = calculatePoolDistr istakeSnap
      , ssStakeSet = mkSetSnapShot (ssStakeMark s) maxKeyAge
      , 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 =
  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
  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 Word64
slotsPerEpoch = 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