{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Ouroboros.Consensus.HardFork.History.Summary ( -- * Bounds Bound (..) , initBound , mkUpperBound , slotToEpochBound -- * Per-era summary , EraEnd (..) , EraSummary (..) , mkEraEnd -- * Overall summary , Summary (..) -- ** Construction , neverForksSummary , summaryWithExactly -- *** Summarize , Shape (..) , Transitions (..) , invariantShape , invariantSummary , singletonShape , summarize , transitionsUnknown -- ** Query , summaryBounds , summaryInit ) where import Codec.CBOR.Decoding (TokenType (TypeNull), decodeNull, peekTokenType) import Codec.CBOR.Encoding (encodeListLen, encodeNull) import Codec.Serialise import Control.Monad.Except import Data.Bifunctor import Data.Foldable (toList) import Data.Kind (Type) import Data.Proxy import Data.SOP.Strict (SListI, lengthSList) import Data.Time hiding (UTCTime) import Data.Word import GHC.Generics (Generic) import GHC.Stack import NoThunks.Class (InspectHeapNamed (..), NoThunks) import Cardano.Binary (enforceSize) import Ouroboros.Consensus.Block import Ouroboros.Consensus.BlockchainTime.WallClock.Types import Ouroboros.Consensus.Util.Counting import Ouroboros.Consensus.HardFork.History.EraParams import Ouroboros.Consensus.HardFork.History.Util {------------------------------------------------------------------------------- Bounds -------------------------------------------------------------------------------} -- | Detailed information about the time bounds of an era data Bound = Bound { Bound -> RelativeTime boundTime :: !RelativeTime , Bound -> SlotNo boundSlot :: !SlotNo , Bound -> EpochNo boundEpoch :: !EpochNo } deriving stock (Int -> Bound -> ShowS [Bound] -> ShowS Bound -> String (Int -> Bound -> ShowS) -> (Bound -> String) -> ([Bound] -> ShowS) -> Show Bound forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Bound] -> ShowS $cshowList :: [Bound] -> ShowS show :: Bound -> String $cshow :: Bound -> String showsPrec :: Int -> Bound -> ShowS $cshowsPrec :: Int -> Bound -> ShowS Show, Bound -> Bound -> Bool (Bound -> Bound -> Bool) -> (Bound -> Bound -> Bool) -> Eq Bound forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Bound -> Bound -> Bool $c/= :: Bound -> Bound -> Bool == :: Bound -> Bound -> Bool $c== :: Bound -> Bound -> Bool Eq, (forall x. Bound -> Rep Bound x) -> (forall x. Rep Bound x -> Bound) -> Generic Bound forall x. Rep Bound x -> Bound forall x. Bound -> Rep Bound x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep Bound x -> Bound $cfrom :: forall x. Bound -> Rep Bound x Generic) deriving anyclass (Context -> Bound -> IO (Maybe ThunkInfo) Proxy Bound -> String (Context -> Bound -> IO (Maybe ThunkInfo)) -> (Context -> Bound -> IO (Maybe ThunkInfo)) -> (Proxy Bound -> String) -> NoThunks Bound forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a showTypeOf :: Proxy Bound -> String $cshowTypeOf :: Proxy Bound -> String wNoThunks :: Context -> Bound -> IO (Maybe ThunkInfo) $cwNoThunks :: Context -> Bound -> IO (Maybe ThunkInfo) noThunks :: Context -> Bound -> IO (Maybe ThunkInfo) $cnoThunks :: Context -> Bound -> IO (Maybe ThunkInfo) NoThunks) initBound :: Bound initBound :: Bound initBound = Bound :: RelativeTime -> SlotNo -> EpochNo -> Bound Bound { boundTime :: RelativeTime boundTime = NominalDiffTime -> RelativeTime RelativeTime NominalDiffTime 0 , boundSlot :: SlotNo boundSlot = Word64 -> SlotNo SlotNo Word64 0 , boundEpoch :: EpochNo boundEpoch = Word64 -> EpochNo EpochNo Word64 0 } -- | Version of 'mkUpperBound' when the upper bound may not be known -- -- If passed 'Nothing', assumes 'EraUnbounded'. This is /NOT/ -- suitable for eras where the transition is simply unknown. mkEraEnd :: EraParams -> Bound -- ^ Lower bound -> Maybe EpochNo -- ^ Upper bound -> EraEnd mkEraEnd :: EraParams -> Bound -> Maybe EpochNo -> EraEnd mkEraEnd EraParams params Bound lo = EraEnd -> (EpochNo -> EraEnd) -> Maybe EpochNo -> EraEnd forall b a. b -> (a -> b) -> Maybe a -> b maybe EraEnd EraUnbounded (Bound -> EraEnd EraEnd (Bound -> EraEnd) -> (EpochNo -> Bound) -> EpochNo -> EraEnd forall b c a. (b -> c) -> (a -> b) -> a -> c . HasCallStack => EraParams -> Bound -> EpochNo -> Bound EraParams -> Bound -> EpochNo -> Bound mkUpperBound EraParams params Bound lo) -- | Compute upper bound given just the epoch number and era parameters mkUpperBound :: HasCallStack => EraParams -> Bound -- ^ Lower bound -> EpochNo -- ^ Upper bound -> Bound mkUpperBound :: EraParams -> Bound -> EpochNo -> Bound mkUpperBound EraParams{SlotLength EpochSize SafeZone eraSafeZone :: EraParams -> SafeZone eraSlotLength :: EraParams -> SlotLength eraEpochSize :: EraParams -> EpochSize eraSafeZone :: SafeZone eraSlotLength :: SlotLength eraEpochSize :: EpochSize ..} Bound lo EpochNo hiEpoch = Bound :: RelativeTime -> SlotNo -> EpochNo -> Bound Bound { boundTime :: RelativeTime boundTime = NominalDiffTime -> RelativeTime -> RelativeTime addRelTime NominalDiffTime inEraTime (RelativeTime -> RelativeTime) -> RelativeTime -> RelativeTime forall a b. (a -> b) -> a -> b $ Bound -> RelativeTime boundTime Bound lo , boundSlot :: SlotNo boundSlot = Word64 -> SlotNo -> SlotNo addSlots Word64 inEraSlots (SlotNo -> SlotNo) -> SlotNo -> SlotNo forall a b. (a -> b) -> a -> b $ Bound -> SlotNo boundSlot Bound lo , boundEpoch :: EpochNo boundEpoch = EpochNo hiEpoch } where inEraEpochs, inEraSlots :: Word64 inEraEpochs :: Word64 inEraEpochs = HasCallStack => EpochNo -> EpochNo -> Word64 EpochNo -> EpochNo -> Word64 countEpochs EpochNo hiEpoch (Bound -> EpochNo boundEpoch Bound lo) inEraSlots :: Word64 inEraSlots = Word64 inEraEpochs Word64 -> Word64 -> Word64 forall a. Num a => a -> a -> a * EpochSize -> Word64 unEpochSize EpochSize eraEpochSize inEraTime :: NominalDiffTime inEraTime :: NominalDiffTime inEraTime = Word64 -> NominalDiffTime forall a b. (Integral a, Num b) => a -> b fromIntegral Word64 inEraSlots NominalDiffTime -> NominalDiffTime -> NominalDiffTime forall a. Num a => a -> a -> a * SlotLength -> NominalDiffTime getSlotLength SlotLength eraSlotLength -- Given the 'SlotNo' of the first /slot/ in which a transition could take -- place, compute the first /epoch/ in which this could happen (since -- transitions only take place at epoch boundaries). If the 'SlotNo' happens -- to be the first slot in an epoch, it will be that 'EpochNo'; if it isn't, -- however, it will be the /next/ epoch. slotToEpochBound :: EraParams -> Bound -> SlotNo -> EpochNo slotToEpochBound :: EraParams -> Bound -> SlotNo -> EpochNo slotToEpochBound EraParams{eraEpochSize :: EraParams -> EpochSize eraEpochSize = EpochSize Word64 epochSize} Bound lo SlotNo hiSlot = Word64 -> EpochNo -> EpochNo addEpochs (if Word64 inEpoch Word64 -> Word64 -> Bool forall a. Eq a => a -> a -> Bool == Word64 0 then Word64 epochs else Word64 epochs Word64 -> Word64 -> Word64 forall a. Num a => a -> a -> a + Word64 1) (Bound -> EpochNo boundEpoch Bound lo) where slots :: Word64 slots = HasCallStack => SlotNo -> SlotNo -> Word64 SlotNo -> SlotNo -> Word64 countSlots SlotNo hiSlot (Bound -> SlotNo boundSlot Bound lo) (Word64 epochs, Word64 inEpoch) = Word64 slots Word64 -> Word64 -> (Word64, Word64) forall a. Integral a => a -> a -> (a, a) `divMod` Word64 epochSize {------------------------------------------------------------------------------- Summary This is what we use internally for all translations. -------------------------------------------------------------------------------} -- | Information about a specific era -- -- The 'eraEnd' of the final era in the summary will be determined by the -- safe zone considerations discussed above. -- -- Let the start of the summary be @(t, s, e)@ (time, slot epoch), and the -- end of the summary be @(t', s', e')@. We have one invariant relating -- epochs and slots: -- -- > INV-1a e' == e + ((s' - s) / epochSize) -- > INV-1b: s' == s + ((e' - e) * epochSize) -- -- And another invariant relating time and slots: -- -- > INV-2a: s' == s + ((t' - t) / slotLen) -- > INV-2b: t' == t + ((s' - s) * slotLen) -- -- Note that these aren't really two sets of independent invariants. @INV-1a@ -- follows from @INV-1b@: -- -- > s' == s + ((e' - e) * epochSize) -- > s' - s == ((e' - e) * epochSize) -- > (s' - s) / epochSize == e' - e -- > e + ((s' - s) / epochSize) == e' -- -- Similarly, @INV-2a@ follows from @INV-2b@: -- -- > t' == t + ((s' - s) * slotLen) -- > t' - t == ((s' - s) * slotLen) -- > (t' - t) / slotLen == s' - s -- > s + ((t' - t) / slotLen) == s' data EraSummary = EraSummary { EraSummary -> Bound eraStart :: !Bound -- ^ Inclusive lower bound , EraSummary -> EraEnd eraEnd :: !EraEnd -- ^ Exclusive upper bound , EraSummary -> EraParams eraParams :: !EraParams -- ^ Active parameters } deriving stock (Int -> EraSummary -> ShowS [EraSummary] -> ShowS EraSummary -> String (Int -> EraSummary -> ShowS) -> (EraSummary -> String) -> ([EraSummary] -> ShowS) -> Show EraSummary forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [EraSummary] -> ShowS $cshowList :: [EraSummary] -> ShowS show :: EraSummary -> String $cshow :: EraSummary -> String showsPrec :: Int -> EraSummary -> ShowS $cshowsPrec :: Int -> EraSummary -> ShowS Show, EraSummary -> EraSummary -> Bool (EraSummary -> EraSummary -> Bool) -> (EraSummary -> EraSummary -> Bool) -> Eq EraSummary forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: EraSummary -> EraSummary -> Bool $c/= :: EraSummary -> EraSummary -> Bool == :: EraSummary -> EraSummary -> Bool $c== :: EraSummary -> EraSummary -> Bool Eq, (forall x. EraSummary -> Rep EraSummary x) -> (forall x. Rep EraSummary x -> EraSummary) -> Generic EraSummary forall x. Rep EraSummary x -> EraSummary forall x. EraSummary -> Rep EraSummary x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep EraSummary x -> EraSummary $cfrom :: forall x. EraSummary -> Rep EraSummary x Generic) deriving anyclass (Context -> EraSummary -> IO (Maybe ThunkInfo) Proxy EraSummary -> String (Context -> EraSummary -> IO (Maybe ThunkInfo)) -> (Context -> EraSummary -> IO (Maybe ThunkInfo)) -> (Proxy EraSummary -> String) -> NoThunks EraSummary forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a showTypeOf :: Proxy EraSummary -> String $cshowTypeOf :: Proxy EraSummary -> String wNoThunks :: Context -> EraSummary -> IO (Maybe ThunkInfo) $cwNoThunks :: Context -> EraSummary -> IO (Maybe ThunkInfo) noThunks :: Context -> EraSummary -> IO (Maybe ThunkInfo) $cnoThunks :: Context -> EraSummary -> IO (Maybe ThunkInfo) NoThunks) -- | Exclusive upper bound on the era data EraEnd = -- | Bounded era EraEnd !Bound -- | Unbounded era -- -- This arises from the use of 'UnsafeIndefiniteSafeZone'. | EraUnbounded deriving stock (Int -> EraEnd -> ShowS [EraEnd] -> ShowS EraEnd -> String (Int -> EraEnd -> ShowS) -> (EraEnd -> String) -> ([EraEnd] -> ShowS) -> Show EraEnd forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [EraEnd] -> ShowS $cshowList :: [EraEnd] -> ShowS show :: EraEnd -> String $cshow :: EraEnd -> String showsPrec :: Int -> EraEnd -> ShowS $cshowsPrec :: Int -> EraEnd -> ShowS Show, EraEnd -> EraEnd -> Bool (EraEnd -> EraEnd -> Bool) -> (EraEnd -> EraEnd -> Bool) -> Eq EraEnd forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: EraEnd -> EraEnd -> Bool $c/= :: EraEnd -> EraEnd -> Bool == :: EraEnd -> EraEnd -> Bool $c== :: EraEnd -> EraEnd -> Bool Eq, (forall x. EraEnd -> Rep EraEnd x) -> (forall x. Rep EraEnd x -> EraEnd) -> Generic EraEnd forall x. Rep EraEnd x -> EraEnd forall x. EraEnd -> Rep EraEnd x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep EraEnd x -> EraEnd $cfrom :: forall x. EraEnd -> Rep EraEnd x Generic) deriving anyclass (Context -> EraEnd -> IO (Maybe ThunkInfo) Proxy EraEnd -> String (Context -> EraEnd -> IO (Maybe ThunkInfo)) -> (Context -> EraEnd -> IO (Maybe ThunkInfo)) -> (Proxy EraEnd -> String) -> NoThunks EraEnd forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a showTypeOf :: Proxy EraEnd -> String $cshowTypeOf :: Proxy EraEnd -> String wNoThunks :: Context -> EraEnd -> IO (Maybe ThunkInfo) $cwNoThunks :: Context -> EraEnd -> IO (Maybe ThunkInfo) noThunks :: Context -> EraEnd -> IO (Maybe ThunkInfo) $cnoThunks :: Context -> EraEnd -> IO (Maybe ThunkInfo) NoThunks) -- | Summary of the /confirmed/ part of the ledger -- -- The summary zips 'Shape' with 'Forks', and provides detailed information -- about the start and end of each era. -- -- We have at most one summary for each era, and at least one newtype Summary xs = Summary { Summary xs -> NonEmpty xs EraSummary getSummary :: NonEmpty xs EraSummary } deriving (Summary xs -> Summary xs -> Bool (Summary xs -> Summary xs -> Bool) -> (Summary xs -> Summary xs -> Bool) -> Eq (Summary xs) forall (xs :: [*]). Summary xs -> Summary xs -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Summary xs -> Summary xs -> Bool $c/= :: forall (xs :: [*]). Summary xs -> Summary xs -> Bool == :: Summary xs -> Summary xs -> Bool $c== :: forall (xs :: [*]). Summary xs -> Summary xs -> Bool Eq, Int -> Summary xs -> ShowS [Summary xs] -> ShowS Summary xs -> String (Int -> Summary xs -> ShowS) -> (Summary xs -> String) -> ([Summary xs] -> ShowS) -> Show (Summary xs) forall (xs :: [*]). Int -> Summary xs -> ShowS forall (xs :: [*]). [Summary xs] -> ShowS forall (xs :: [*]). Summary xs -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Summary xs] -> ShowS $cshowList :: forall (xs :: [*]). [Summary xs] -> ShowS show :: Summary xs -> String $cshow :: forall (xs :: [*]). Summary xs -> String showsPrec :: Int -> Summary xs -> ShowS $cshowsPrec :: forall (xs :: [*]). Int -> Summary xs -> ShowS Show) deriving Context -> Summary xs -> IO (Maybe ThunkInfo) Proxy (Summary xs) -> String (Context -> Summary xs -> IO (Maybe ThunkInfo)) -> (Context -> Summary xs -> IO (Maybe ThunkInfo)) -> (Proxy (Summary xs) -> String) -> NoThunks (Summary xs) forall (xs :: [*]). Context -> Summary xs -> IO (Maybe ThunkInfo) forall (xs :: [*]). Proxy (Summary xs) -> String forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a showTypeOf :: Proxy (Summary xs) -> String $cshowTypeOf :: forall (xs :: [*]). Proxy (Summary xs) -> String wNoThunks :: Context -> Summary xs -> IO (Maybe ThunkInfo) $cwNoThunks :: forall (xs :: [*]). Context -> Summary xs -> IO (Maybe ThunkInfo) noThunks :: Context -> Summary xs -> IO (Maybe ThunkInfo) $cnoThunks :: forall (xs :: [*]). Context -> Summary xs -> IO (Maybe ThunkInfo) NoThunks via InspectHeapNamed "Summary" (Summary xs) {------------------------------------------------------------------------------- Trivial summary -------------------------------------------------------------------------------} -- | 'Summary' for a ledger that never forks neverForksSummary :: EpochSize -> SlotLength -> Summary '[x] neverForksSummary :: EpochSize -> SlotLength -> Summary '[x] neverForksSummary EpochSize epochSize SlotLength slotLen = NonEmpty '[x] EraSummary -> Summary '[x] forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs Summary (NonEmpty '[x] EraSummary -> Summary '[x]) -> NonEmpty '[x] EraSummary -> Summary '[x] forall a b. (a -> b) -> a -> b $ EraSummary -> NonEmpty '[x] EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (EraSummary -> NonEmpty '[x] EraSummary) -> EraSummary -> NonEmpty '[x] EraSummary forall a b. (a -> b) -> a -> b $ EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound initBound , eraEnd :: EraEnd eraEnd = EraEnd EraUnbounded , eraParams :: EraParams eraParams = EraParams :: EpochSize -> SlotLength -> SafeZone -> EraParams EraParams { eraEpochSize :: EpochSize eraEpochSize = EpochSize epochSize , eraSlotLength :: SlotLength eraSlotLength = SlotLength slotLen , eraSafeZone :: SafeZone eraSafeZone = SafeZone UnsafeIndefiniteSafeZone } } {------------------------------------------------------------------------------- Basic API for 'Summary' -------------------------------------------------------------------------------} -- | Outer bounds of the summary summaryBounds :: Summary xs -> (Bound, EraEnd) summaryBounds :: Summary xs -> (Bound, EraEnd) summaryBounds (Summary NonEmpty xs EraSummary summary) = (EraSummary -> Bound eraStart (NonEmpty xs EraSummary -> EraSummary forall (xs :: [*]) a. NonEmpty xs a -> a nonEmptyHead NonEmpty xs EraSummary summary), EraSummary -> EraEnd eraEnd (NonEmpty xs EraSummary -> EraSummary forall (xs :: [*]) a. NonEmpty xs a -> a nonEmptyLast NonEmpty xs EraSummary summary)) -- | Analogue of 'Data.List.init' for 'Summary' (i.e., split off the final era) -- -- This is primarily useful for tests. summaryInit :: Summary xs -> (Maybe (Summary xs), EraSummary) summaryInit :: Summary xs -> (Maybe (Summary xs), EraSummary) summaryInit (Summary NonEmpty xs EraSummary summary) = (Maybe (NonEmpty xs EraSummary) -> Maybe (Summary xs)) -> (Maybe (NonEmpty xs EraSummary), EraSummary) -> (Maybe (Summary xs), EraSummary) forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ((NonEmpty xs EraSummary -> Summary xs) -> Maybe (NonEmpty xs EraSummary) -> Maybe (Summary xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap NonEmpty xs EraSummary -> Summary xs forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs Summary) ((Maybe (NonEmpty xs EraSummary), EraSummary) -> (Maybe (Summary xs), EraSummary)) -> (Maybe (NonEmpty xs EraSummary), EraSummary) -> (Maybe (Summary xs), EraSummary) forall a b. (a -> b) -> a -> b $ NonEmpty xs EraSummary -> (Maybe (NonEmpty xs EraSummary), EraSummary) forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a) nonEmptyInit NonEmpty xs EraSummary summary -- | Construct 'Summary' with an exact number of 'EraSummary' -- -- Primarily useful for tests. summaryWithExactly :: Exactly (x ': xs) EraSummary -> Summary (x ': xs) summaryWithExactly :: Exactly (x : xs) EraSummary -> Summary (x : xs) summaryWithExactly = NonEmpty (x : xs) EraSummary -> Summary (x : xs) forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs Summary (NonEmpty (x : xs) EraSummary -> Summary (x : xs)) -> (Exactly (x : xs) EraSummary -> NonEmpty (x : xs) EraSummary) -> Exactly (x : xs) EraSummary -> Summary (x : xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly (x : xs) EraSummary -> NonEmpty (x : xs) EraSummary forall x (xs :: [*]) a. Exactly (x : xs) a -> NonEmpty (x : xs) a exactlyWeakenNonEmpty {------------------------------------------------------------------------------- Shape and Transitions This is used only for 'summarize'. -------------------------------------------------------------------------------} -- | The shape of the chain (old to new) -- -- The shape determines how many hard forks we expect as well as the parameters -- for each era. The type argument is a type-level list containing one entry -- per era, emphasizing that this information is statically known. -- -- The entry indices themselves are not used here, but the idea is that they -- look something like @'[ByronBlock, ShelleyBlock, GoguenBlock]@ and do affect -- the hard fork combinator. So far this is a list of block types, since most -- of consensus is indexed by block types. newtype Shape xs = Shape { Shape xs -> Exactly xs EraParams getShape :: Exactly xs EraParams } deriving (Int -> Shape xs -> ShowS [Shape xs] -> ShowS Shape xs -> String (Int -> Shape xs -> ShowS) -> (Shape xs -> String) -> ([Shape xs] -> ShowS) -> Show (Shape xs) forall (xs :: [*]). Int -> Shape xs -> ShowS forall (xs :: [*]). [Shape xs] -> ShowS forall (xs :: [*]). Shape xs -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Shape xs] -> ShowS $cshowList :: forall (xs :: [*]). [Shape xs] -> ShowS show :: Shape xs -> String $cshow :: forall (xs :: [*]). Shape xs -> String showsPrec :: Int -> Shape xs -> ShowS $cshowsPrec :: forall (xs :: [*]). Int -> Shape xs -> ShowS Show) deriving Context -> Shape xs -> IO (Maybe ThunkInfo) Proxy (Shape xs) -> String (Context -> Shape xs -> IO (Maybe ThunkInfo)) -> (Context -> Shape xs -> IO (Maybe ThunkInfo)) -> (Proxy (Shape xs) -> String) -> NoThunks (Shape xs) forall (xs :: [*]). Context -> Shape xs -> IO (Maybe ThunkInfo) forall (xs :: [*]). Proxy (Shape xs) -> String forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a showTypeOf :: Proxy (Shape xs) -> String $cshowTypeOf :: forall (xs :: [*]). Proxy (Shape xs) -> String wNoThunks :: Context -> Shape xs -> IO (Maybe ThunkInfo) $cwNoThunks :: forall (xs :: [*]). Context -> Shape xs -> IO (Maybe ThunkInfo) noThunks :: Context -> Shape xs -> IO (Maybe ThunkInfo) $cnoThunks :: forall (xs :: [*]). Context -> Shape xs -> IO (Maybe ThunkInfo) NoThunks via InspectHeapNamed "Shape" (Shape xs) -- | There is only one era singletonShape :: EraParams -> Shape '[x] singletonShape :: EraParams -> Shape '[x] singletonShape EraParams params = Exactly '[x] EraParams -> Shape '[x] forall (xs :: [*]). Exactly xs EraParams -> Shape xs Shape (EraParams -> Exactly '[x] EraParams forall a x. a -> Exactly '[x] a exactlyOne EraParams params) -- | The exact point of each confirmed hard fork transition (old to new) -- -- Unlike the 'Shape' of the chain, which is statically known, the 'Transitions' -- are derived from the state of the ledger (hard fork transition points only -- become known after a voting procedure). -- -- Any transition listed here must be "certain". How certainty is established is -- ledger dependent, but it should imply that this is no longer subject to -- rollback. data Transitions :: [Type] -> Type where -- | If the indices are, say, @'[Byron, Shelley, Goguen]@, then we can have -- have at most two transitions: one to Shelley, and one to Goguen. There -- cannot be a transition /to/ the initial ledger. Transitions :: AtMost xs EpochNo -> Transitions (x ': xs) deriving instance Show (Transitions xs) -- | No known transitions yet transitionsUnknown :: Transitions (x ': xs) transitionsUnknown :: Transitions (x : xs) transitionsUnknown = AtMost xs EpochNo -> Transitions (x : xs) forall (xs :: [*]) x. AtMost xs EpochNo -> Transitions (x : xs) Transitions AtMost xs EpochNo forall (xs :: [*]) a. AtMost xs a AtMostNil {------------------------------------------------------------------------------- Constructing the summary NOTE: In practice, when using the hard fork combinator, we never ever call 'summarize', and instead read off a summary from the 'HardForkState'. In that case, this serves primarily as a reference implementation. -------------------------------------------------------------------------------} -- | Construct hard fork 'Summary' -- -- NOTE (on epoch to slot translation). In order to translate 'SlotNo' to -- 'EpochNo', we simply "line up" all slots. For example, suppose we have -- an initial 'EpochSize' of 10, and then an 'EpochSize' of 20 from 'EpochNo' -- 3 onwards. We end up with something like -- -- > Epoch | 0 | 1 | 2 | 3 | 4 | .. -- > Slot | 0 .. 9 | 10 .. 19 | 20 .. 29 | 30 .. 49 | 50 .. 69 | .. -- -- We do this translation /independent/ from the 'minimumPossibleSlotNo' -- for a particular ledger. This means that for ledgers where the -- 'minimumPossibleSlotNo' is not zero (e.g., some ledgers might set it to 1), -- the maximum number of blocks (aka filled slots) in an epoch is just 1 (or -- more) less than the other epochs. summarize :: WithOrigin SlotNo -- ^ Slot at the tip of the ledger -> Shape xs -> Transitions xs -> Summary xs summarize :: WithOrigin SlotNo -> Shape xs -> Transitions xs -> Summary xs summarize WithOrigin SlotNo ledgerTip = \(Shape Exactly xs EraParams shape) (Transitions AtMost xs EpochNo transitions) -> NonEmpty (x : xs) EraSummary -> Summary (x : xs) forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs Summary (NonEmpty (x : xs) EraSummary -> Summary (x : xs)) -> NonEmpty (x : xs) EraSummary -> Summary (x : xs) forall a b. (a -> b) -> a -> b $ Bound -> Exactly (x : xs) EraParams -> AtMost xs EpochNo -> NonEmpty (x : xs) EraSummary forall x (xs :: [*]). Bound -> Exactly (x : xs) EraParams -> AtMost xs EpochNo -> NonEmpty (x : xs) EraSummary go Bound initBound Exactly xs EraParams Exactly (x : xs) EraParams shape AtMost xs EpochNo transitions where go :: Bound -- Lower bound for current era -> Exactly (x ': xs) EraParams -- params for all eras -> AtMost xs EpochNo -- transitions -> NonEmpty (x ': xs) EraSummary -- CASE (ii) from 'EraParams' Haddock -- NOTE: Ledger tip might be close to the end of this era (or indeed past -- it) but this doesn't matter for the summary of /this/ era. go :: Bound -> Exactly (x : xs) EraParams -> AtMost xs EpochNo -> NonEmpty (x : xs) EraSummary go Bound lo (ExactlyCons EraParams params Exactly xs EraParams ss) (AtMostCons EpochNo epoch AtMost xs EpochNo fs) = EraSummary -> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons (Bound -> EraEnd -> EraParams -> EraSummary EraSummary Bound lo (Bound -> EraEnd EraEnd Bound hi) EraParams params) (NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary) -> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary forall a b. (a -> b) -> a -> b $ Bound -> Exactly (x : xs) EraParams -> AtMost xs EpochNo -> NonEmpty (x : xs) EraSummary forall x (xs :: [*]). Bound -> Exactly (x : xs) EraParams -> AtMost xs EpochNo -> NonEmpty (x : xs) EraSummary go Bound hi Exactly xs EraParams Exactly (x : xs) EraParams ss AtMost xs EpochNo fs where hi :: Bound hi = HasCallStack => EraParams -> Bound -> EpochNo -> Bound EraParams -> Bound -> EpochNo -> Bound mkUpperBound EraParams params Bound lo EpochNo epoch -- CASE (i) or (iii) from 'EraParams' Haddock go Bound lo (ExactlyCons params :: EraParams params@EraParams{SlotLength EpochSize SafeZone eraSafeZone :: SafeZone eraSlotLength :: SlotLength eraEpochSize :: EpochSize eraSafeZone :: EraParams -> SafeZone eraSlotLength :: EraParams -> SlotLength eraEpochSize :: EraParams -> EpochSize ..} Exactly xs EraParams _) AtMost xs EpochNo AtMostNil = EraSummary -> NonEmpty (x : xs) EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (Bound -> EraEnd -> EraParams -> EraSummary EraSummary Bound lo EraEnd hi EraParams params) where hi :: EraEnd hi :: EraEnd hi = case SafeZone eraSafeZone of SafeZone UnsafeIndefiniteSafeZone -> EraEnd EraUnbounded StandardSafeZone Word64 safeFromTip -> Bound -> EraEnd EraEnd (Bound -> EraEnd) -> (SlotNo -> Bound) -> SlotNo -> EraEnd forall b c a. (b -> c) -> (a -> b) -> a -> c . HasCallStack => EraParams -> Bound -> EpochNo -> Bound EraParams -> Bound -> EpochNo -> Bound mkUpperBound EraParams params Bound lo (EpochNo -> Bound) -> (SlotNo -> EpochNo) -> SlotNo -> Bound forall b c a. (b -> c) -> (a -> b) -> a -> c . EraParams -> Bound -> SlotNo -> EpochNo slotToEpochBound EraParams params Bound lo (SlotNo -> EpochNo) -> (SlotNo -> SlotNo) -> SlotNo -> EpochNo forall b c a. (b -> c) -> (a -> b) -> a -> c . Word64 -> SlotNo -> SlotNo addSlots Word64 safeFromTip -- If the tip is already in this era, safe zone applies from the -- ledger tip (CASE (i) from 'EraParams' Haddock). If the ledger -- tip is in the /previous/ era, but the transition to /this/ era -- is already known, the safe zone applies from the start of this -- era (CASE (iii) from 'EraParams' Haddock). -- -- NOTE: The upper bound is /exclusive/: -- -- o Suppose the ledger tip is at slot 10, and 'safeFromTip' is 2. -- Then we should be able to make accurate predictions for slots -- 10 (of course), as well as (the safe zone) slots 11 and 12. -- Since the upper bound is /exclusive/, this means that the -- upper bound becomes 13. (Case i) -- o If the ledger tip is in the previous era (case iii), and the -- start of this era is slot 100, then we should be able to -- give accurate predictions for the first two slots in this era -- (100 and 101), and the upper bound becomes 102. -- -- This explains the use of the extra addition ('next') for -- case (i) but not for case (iii). (SlotNo -> EraEnd) -> SlotNo -> EraEnd forall a b. (a -> b) -> a -> b $ SlotNo -> SlotNo -> SlotNo forall a. Ord a => a -> a -> a max (WithOrigin SlotNo -> SlotNo next WithOrigin SlotNo ledgerTip) (Bound -> SlotNo boundSlot Bound lo) -- Upper bound is exclusive, so we count from the /next/ ledger tip next :: WithOrigin SlotNo -> SlotNo next :: WithOrigin SlotNo -> SlotNo next WithOrigin SlotNo Origin = Word64 -> SlotNo SlotNo Word64 0 next (NotOrigin SlotNo s) = SlotNo -> SlotNo forall a. Enum a => a -> a succ SlotNo s {------------------------------------------------------------------------------- Invariants -------------------------------------------------------------------------------} -- | Check 'Shape' invariants -- -- The only part of the 'Shape' that must make sense is the 'safeBeforeEpoch' -- values (they must be strictly increasing). -- -- NOTE: We assume eras cannot be empty. This will be satisfied by any ledger -- we are interested in since transitions must be voted on (safe zones will -- be non-empty). invariantShape :: Shape xs -> Except String () invariantShape :: Shape xs -> Except String () invariantShape = \(Shape Exactly xs EraParams shape) -> EpochNo -> Exactly xs EraParams -> Except String () forall (xs :: [*]). EpochNo -> Exactly xs EraParams -> Except String () go (Word64 -> EpochNo EpochNo Word64 0) Exactly xs EraParams shape where go :: EpochNo -- Lower bound on the start of the era -> Exactly xs EraParams -> Except String () go :: EpochNo -> Exactly xs EraParams -> Except String () go EpochNo _ Exactly xs EraParams ExactlyNil = () -> Except String () forall (m :: * -> *) a. Monad m => a -> m a return () go EpochNo lowerBound (ExactlyCons EraParams _ Exactly xs EraParams shape') = let nextLowerBound :: EpochNo nextLowerBound = Word64 -> EpochNo -> EpochNo addEpochs Word64 1 EpochNo lowerBound in EpochNo -> Exactly xs EraParams -> Except String () forall (xs :: [*]). EpochNo -> Exactly xs EraParams -> Except String () go EpochNo nextLowerBound Exactly xs EraParams shape' -- | Check 'Summary' invariants invariantSummary :: Summary xs -> Except String () invariantSummary :: Summary xs -> Except String () invariantSummary = \(Summary NonEmpty xs EraSummary summary) -> -- Pretend the start of the first era is the "end of the previous" one Bound -> [EraSummary] -> Except String () go (EraSummary -> Bound eraStart (NonEmpty xs EraSummary -> EraSummary forall (xs :: [*]) a. NonEmpty xs a -> a nonEmptyHead NonEmpty xs EraSummary summary)) (NonEmpty xs EraSummary -> [EraSummary] forall (t :: * -> *) a. Foldable t => t a -> [a] toList NonEmpty xs EraSummary summary) where go :: Bound -- ^ End of the previous era -> [EraSummary] -> Except String () go :: Bound -> [EraSummary] -> Except String () go Bound _ [] = () -> Except String () forall (m :: * -> *) a. Monad m => a -> m a return () go Bound prevEnd (EraSummary curSummary : [EraSummary] next) = do Bool -> Except String () -> Except String () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (Bound curStart Bound -> Bound -> Bool forall a. Eq a => a -> a -> Bool == Bound prevEnd) (Except String () -> Except String ()) -> Except String () -> Except String () forall a b. (a -> b) -> a -> b $ String -> Except String () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (String -> Except String ()) -> String -> Except String () forall a b. (a -> b) -> a -> b $ Context -> String forall a. Monoid a => [a] -> a mconcat [ String "Bounds don't line up: end of previous era " , Bound -> String forall a. Show a => a -> String show Bound prevEnd , String " /= start of current era " , Bound -> String forall a. Show a => a -> String show Bound curStart ] case EraEnd mCurEnd of EraEnd EraUnbounded -> Bool -> Except String () -> Except String () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless ([EraSummary] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [EraSummary] next) (Except String () -> Except String ()) -> Except String () -> Except String () forall a b. (a -> b) -> a -> b $ String -> Except String () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError String "Unbounded non-final era" EraEnd Bound curEnd -> do -- Check the invariants mentioned at 'EraSummary' -- -- o @epochsInEra@ corresponds to @e' - e@ -- o @slotsInEra@ corresponds to @(e' - e) * epochSize)@ -- o @timeInEra@ corresponds to @((e' - e) * epochSize * slotLen@ -- which, if INV-1b holds, equals @(s' - s) * slotLen@ let epochsInEra, slotsInEra :: Word64 epochsInEra :: Word64 epochsInEra = HasCallStack => EpochNo -> EpochNo -> Word64 EpochNo -> EpochNo -> Word64 countEpochs (Bound -> EpochNo boundEpoch Bound curEnd) (Bound -> EpochNo boundEpoch Bound curStart) slotsInEra :: Word64 slotsInEra = Word64 epochsInEra Word64 -> Word64 -> Word64 forall a. Num a => a -> a -> a * EpochSize -> Word64 unEpochSize (EraParams -> EpochSize eraEpochSize EraParams curParams) timeInEra :: NominalDiffTime timeInEra :: NominalDiffTime timeInEra = Word64 -> NominalDiffTime forall a b. (Integral a, Num b) => a -> b fromIntegral Word64 slotsInEra NominalDiffTime -> NominalDiffTime -> NominalDiffTime forall a. Num a => a -> a -> a * SlotLength -> NominalDiffTime getSlotLength (EraParams -> SlotLength eraSlotLength EraParams curParams) Bool -> Except String () -> Except String () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (Bound -> EpochNo boundEpoch Bound curEnd EpochNo -> EpochNo -> Bool forall a. Ord a => a -> a -> Bool > Bound -> EpochNo boundEpoch Bound curStart) (Except String () -> Except String ()) -> Except String () -> Except String () forall a b. (a -> b) -> a -> b $ String -> Except String () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError String "Empty era" Bool -> Except String () -> Except String () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (Bound -> SlotNo boundSlot Bound curEnd SlotNo -> SlotNo -> Bool forall a. Eq a => a -> a -> Bool == Word64 -> SlotNo -> SlotNo addSlots Word64 slotsInEra (Bound -> SlotNo boundSlot Bound curStart)) (Except String () -> Except String ()) -> Except String () -> Except String () forall a b. (a -> b) -> a -> b $ String -> Except String () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (String -> Except String ()) -> String -> Except String () forall a b. (a -> b) -> a -> b $ Context -> String forall a. Monoid a => [a] -> a mconcat [ String "Invalid final boundSlot in " , EraSummary -> String forall a. Show a => a -> String show EraSummary curSummary , String " (INV-1b)" ] Bool -> Except String () -> Except String () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (Bound -> RelativeTime boundTime Bound curEnd RelativeTime -> RelativeTime -> Bool forall a. Eq a => a -> a -> Bool == NominalDiffTime -> RelativeTime -> RelativeTime addRelTime NominalDiffTime timeInEra (Bound -> RelativeTime boundTime Bound curStart)) (Except String () -> Except String ()) -> Except String () -> Except String () forall a b. (a -> b) -> a -> b $ String -> Except String () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (String -> Except String ()) -> String -> Except String () forall a b. (a -> b) -> a -> b $ Context -> String forall a. Monoid a => [a] -> a mconcat [ String "Invalid final boundTime in " , EraSummary -> String forall a. Show a => a -> String show EraSummary curSummary , String " (INV-2b)" ] Bound -> [EraSummary] -> Except String () go Bound curEnd [EraSummary] next where curStart :: Bound mCurEnd :: EraEnd curParams :: EraParams EraSummary Bound curStart EraEnd mCurEnd EraParams curParams = EraSummary curSummary {------------------------------------------------------------------------------- Serialisation -------------------------------------------------------------------------------} instance Serialise Bound where encode :: Bound -> Encoding encode Bound{SlotNo RelativeTime EpochNo boundEpoch :: EpochNo boundSlot :: SlotNo boundTime :: RelativeTime boundEpoch :: Bound -> EpochNo boundSlot :: Bound -> SlotNo boundTime :: Bound -> RelativeTime ..} = [Encoding] -> Encoding forall a. Monoid a => [a] -> a mconcat [ Word -> Encoding encodeListLen Word 3 , RelativeTime -> Encoding forall a. Serialise a => a -> Encoding encode RelativeTime boundTime , SlotNo -> Encoding forall a. Serialise a => a -> Encoding encode SlotNo boundSlot , EpochNo -> Encoding forall a. Serialise a => a -> Encoding encode EpochNo boundEpoch ] decode :: Decoder s Bound decode = do Text -> Int -> Decoder s () forall s. Text -> Int -> Decoder s () enforceSize Text "Bound" Int 3 RelativeTime boundTime <- Decoder s RelativeTime forall a s. Serialise a => Decoder s a decode SlotNo boundSlot <- Decoder s SlotNo forall a s. Serialise a => Decoder s a decode EpochNo boundEpoch <- Decoder s EpochNo forall a s. Serialise a => Decoder s a decode Bound -> Decoder s Bound forall (m :: * -> *) a. Monad m => a -> m a return Bound :: RelativeTime -> SlotNo -> EpochNo -> Bound Bound{SlotNo RelativeTime EpochNo boundEpoch :: EpochNo boundSlot :: SlotNo boundTime :: RelativeTime boundEpoch :: EpochNo boundSlot :: SlotNo boundTime :: RelativeTime ..} instance Serialise EraEnd where encode :: EraEnd -> Encoding encode EraEnd EraUnbounded = Encoding encodeNull encode (EraEnd Bound bound) = Bound -> Encoding forall a. Serialise a => a -> Encoding encode Bound bound decode :: Decoder s EraEnd decode = Decoder s TokenType forall s. Decoder s TokenType peekTokenType Decoder s TokenType -> (TokenType -> Decoder s EraEnd) -> Decoder s EraEnd forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \case TokenType TypeNull -> do Decoder s () forall s. Decoder s () decodeNull EraEnd -> Decoder s EraEnd forall (m :: * -> *) a. Monad m => a -> m a return EraEnd EraUnbounded TokenType _ -> Bound -> EraEnd EraEnd (Bound -> EraEnd) -> Decoder s Bound -> Decoder s EraEnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Decoder s Bound forall a s. Serialise a => Decoder s a decode instance Serialise EraSummary where encode :: EraSummary -> Encoding encode EraSummary{EraParams EraEnd Bound eraParams :: EraParams eraEnd :: EraEnd eraStart :: Bound eraParams :: EraSummary -> EraParams eraEnd :: EraSummary -> EraEnd eraStart :: EraSummary -> Bound ..} = [Encoding] -> Encoding forall a. Monoid a => [a] -> a mconcat [ Word -> Encoding encodeListLen Word 3 , Bound -> Encoding forall a. Serialise a => a -> Encoding encode Bound eraStart , EraEnd -> Encoding forall a. Serialise a => a -> Encoding encode EraEnd eraEnd , EraParams -> Encoding forall a. Serialise a => a -> Encoding encode EraParams eraParams ] decode :: Decoder s EraSummary decode = do Text -> Int -> Decoder s () forall s. Text -> Int -> Decoder s () enforceSize Text "EraSummary" Int 3 Bound eraStart <- Decoder s Bound forall a s. Serialise a => Decoder s a decode EraEnd eraEnd <- Decoder s EraEnd forall a s. Serialise a => Decoder s a decode EraParams eraParams <- Decoder s EraParams forall a s. Serialise a => Decoder s a decode EraSummary -> Decoder s EraSummary forall (m :: * -> *) a. Monad m => a -> m a return EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary{EraParams EraEnd Bound eraParams :: EraParams eraEnd :: EraEnd eraStart :: Bound eraParams :: EraParams eraEnd :: EraEnd eraStart :: Bound ..} instance SListI xs => Serialise (Summary xs) where encode :: Summary xs -> Encoding encode (Summary NonEmpty xs EraSummary eraSummaries) = [EraSummary] -> Encoding forall a. Serialise a => a -> Encoding encode (NonEmpty xs EraSummary -> [EraSummary] forall (t :: * -> *) a. Foldable t => t a -> [a] toList NonEmpty xs EraSummary eraSummaries) -- @xs@ is the list of eras that is statically known to us; the server has a -- similar list @ys@ of eras that /it/ statically knows about. We do not know -- what @ys@ is here, but we can nonetheless reason about how @|xs|@ and -- @|ys|@ might relate: -- -- - @|xs| == |ys|@: this is the normal case; we and the server know about the -- same (number of) eras. No special care needs to be taken. -- -- - @|xs| > |ys|@: we know about more eras than the server does. The server -- will send us era summaries for @1 <= n <= |ys|@ eras. For sure @n < -- |xs|@, so decoding will be unproblematic. -- -- - @|xs| < |ys|@: we know about fewer eras than the server does. This will -- happen when the server has been upgraded for the next hard fork, but the -- client hasn't yet. Pattern match on the number @n@ of eras that the -- server sends us summaries for: -- -- o @n < |xs|@: Although the server knows about more eras than us, they -- actually only send us era summaries for fewer eras than we know about. -- This means that the transition to what _we_ believe is the final era is -- not yet known; the summary sent to us by the server is fine as is. -- -- o @n == |xs|@: The server does not yet know about the transition out of -- what (we believe to be) the final era. -- -- o @n > |xs|@: the server already knows about the transition to the next -- era after our final era. In this case we must drop all eras that we -- don't know about. -- -- Since we do not know @|ys|@, we cannot actually implement the outermost -- case statement. However: -- -- - If @|xs| > |ys|@, by definition @n < |xs|@, and hence we will not modify -- the era summary: this is what we wanted. -- -- - If @|xs| == |ys|@, then at most @n == |xs|@. decode :: Decoder s (Summary xs) decode = do -- Drop all eras we don't know about [EraSummary] eraSummaries <- Int -> [EraSummary] -> [EraSummary] forall a. Int -> [a] -> [a] take Int nbXs ([EraSummary] -> [EraSummary]) -> Decoder s [EraSummary] -> Decoder s [EraSummary] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Decoder s [EraSummary] forall a s. Serialise a => Decoder s a decode case NonEmpty xs EraSummary -> Summary xs forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs Summary (NonEmpty xs EraSummary -> Summary xs) -> Maybe (NonEmpty xs EraSummary) -> Maybe (Summary xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [EraSummary] -> Maybe (NonEmpty xs EraSummary) forall (xs :: [*]) a. SListI xs => [a] -> Maybe (NonEmpty xs a) nonEmptyFromList [EraSummary] eraSummaries of Just Summary xs summary -> Summary xs -> Decoder s (Summary xs) forall (m :: * -> *) a. Monad m => a -> m a return Summary xs summary Maybe (Summary xs) Nothing -> String -> Decoder s (Summary xs) forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Summary: expected at least one era summary" where -- @|xs|@ nbXs :: Int nbXs :: Int nbXs = Proxy xs -> Int forall k (xs :: [k]) (proxy :: [k] -> *). SListI xs => proxy xs -> Int lengthSList (Proxy xs forall k (t :: k). Proxy t Proxy @xs)