{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

-- | Tests for the hard fork summary.
--
-- This module verifies the property that /no matter how the summary is
-- constructed/, as long as it satisfies its invariants, we should have
-- roundtrip properties:
--
-- * Converting time to a slot and then back to time should be an identity
--   (modulo the time spent in that slot).
-- * Converting a slot to time and then back should be an identity.
-- * Converting slot to an epoch and then back to a slot should be an identity
--   (modulo the time spent in that epoch).
-- * Converting an epoch to a slot and then back should be an identity.
-- * Converting a Peras round number to a slot and then back should be an identity.
module Test.Consensus.HardFork.Summary (tests) where

import Data.Time
import Data.Word
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.BlockchainTime
import qualified Ouroboros.Consensus.HardFork.History as HF
import Test.Consensus.HardFork.Infra
import Test.QuickCheck
import Test.Tasty
import Test.Tasty.QuickCheck
import Test.Util.Orphans.Arbitrary ()
import Test.Util.QuickCheck

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Summary"
    [ TestName -> [TestTree] -> TestTree
testGroup
        TestName
"Sanity"
        [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"generator" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ (ArbitrarySummary -> Property) -> Property
forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkGenerator ((ArbitrarySummary -> Property) -> Property)
-> (ArbitrarySummary -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
..} ->
            (Summary xs -> Except TestName ()) -> Summary xs -> Property
forall a. (a -> Except TestName ()) -> a -> Property
checkInvariant Summary xs -> Except TestName ()
forall (xs :: [*]). Summary xs -> Except TestName ()
HF.invariantSummary Summary xs
arbitrarySummary
        , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"shrinker" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ (ArbitrarySummary -> Property) -> Property
forall a. (Arbitrary a, Show a) => (a -> Property) -> Property
checkShrinker ((ArbitrarySummary -> Property) -> Property)
-> (ArbitrarySummary -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} ->
            (Summary xs -> Except TestName ()) -> Summary xs -> Property
forall a. (a -> Except TestName ()) -> a -> Property
checkInvariant Summary xs -> Except TestName ()
forall (xs :: [*]). Summary xs -> Except TestName ()
HF.invariantSummary Summary xs
arbitrarySummary
        ]
    , TestName -> [TestTree] -> TestTree
testGroup
        TestName
"Conversions"
        [ TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"roundtripWallclockSlot" ArbitrarySummary -> Property
roundtripWallclockSlot
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"roundtripSlotWallclock" ArbitrarySummary -> Property
roundtripSlotWallclock
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"roundtripSlotEpoch" ArbitrarySummary -> Property
roundtripSlotEpoch
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"roundtripEpochSlot" ArbitrarySummary -> Property
roundtripEpochSlot
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"roundtripPerasRoundSlot" ArbitrarySummary -> Property
roundtripPerasRoundSlot
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reportsPastHorizonWallclockToSlot" ArbitrarySummary -> Property
reportsPastHorizonWallclockToSlot
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reportsPastHorizonSlotToWallclock" ArbitrarySummary -> Property
reportsPastHorizonSlotToWallclock
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reportsPastHorizonSlotToEpoch" ArbitrarySummary -> Property
reportsPastHorizonSlotToEpoch
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reportsPastHorizonEpochToSlot" ArbitrarySummary -> Property
reportsPastHorizonEpochToSlot
        , TestName -> (ArbitrarySummary -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"reportsPastHorizonPerasRoundNoToSlot" ArbitrarySummary -> Property
reportsPastHorizonPerasRoundNoToSlot
        ]
    ]

{-------------------------------------------------------------------------------
  Dealing with the 'PastHorizonException'
-------------------------------------------------------------------------------}

noPastHorizonException ::
  ArbitrarySummary ->
  HF.Qry Property ->
  Property
noPastHorizonException :: ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} Qry Property
p =
  case Qry Property -> Summary xs -> Either PastHorizonException Property
forall a (xs :: [*]).
HasCallStack =>
Qry a -> Summary xs -> Either PastHorizonException a
HF.runQuery Qry Property
p Summary xs
arbitrarySummary of
    Right Property
prop -> Property
prop
    Left PastHorizonException
ex ->
      TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"Unexpected " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ PastHorizonException -> TestName
forall a. Show a => a -> TestName
show PastHorizonException
ex) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False

isPastHorizonException ::
  Show a =>
  ArbitrarySummary ->
  HF.Qry a ->
  Property
isPastHorizonException :: forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} Qry a
ma =
  case Qry a -> Summary xs -> Either PastHorizonException a
forall a (xs :: [*]).
HasCallStack =>
Qry a -> Summary xs -> Either PastHorizonException a
HF.runQuery Qry a
ma Summary xs
arbitrarySummary of
    Left PastHorizonException
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    Right a
a ->
      TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"Unexpected " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ a -> TestName
forall a. Show a => a -> TestName
show a
a) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False

{-------------------------------------------------------------------------------
  Tests using just 'Summary'
-------------------------------------------------------------------------------}

roundtripWallclockSlot :: ArbitrarySummary -> Property
roundtripWallclockSlot :: ArbitrarySummary -> Property
roundtripWallclockSlot s :: ArbitrarySummary
s@ArbitrarySummary{beforeHorizonTime :: ArbitrarySummary -> RelativeTime
beforeHorizonTime = RelativeTime
time} =
  ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary
s (Qry Property -> Property) -> Qry Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    (slot, inSlot, timeLeft) <- RelativeTime -> Qry (SlotNo, NominalDiffTime, NominalDiffTime)
HF.wallclockToSlot RelativeTime
time
    (time', slotLen) <- HF.slotToWallclock slot
    return $
      conjoin
        [ addRelTime inSlot time' === time
        , inSlot + timeLeft === getSlotLength slotLen
        ]

roundtripSlotWallclock :: ArbitrarySummary -> Property
roundtripSlotWallclock :: ArbitrarySummary -> Property
roundtripSlotWallclock s :: ArbitrarySummary
s@ArbitrarySummary{beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonSlot = SlotNo
slot} =
  ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary
s (Qry Property -> Property) -> Qry Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    (time, slotLen) <- SlotNo -> Qry (RelativeTime, SlotLength)
HF.slotToWallclock SlotNo
slot
    (slot', inSlot, timeLeft) <- HF.wallclockToSlot time
    return $
      conjoin
        [ slot' === slot
        , inSlot === 0
        , inSlot + timeLeft === getSlotLength slotLen
        ]

roundtripSlotEpoch :: ArbitrarySummary -> Property
roundtripSlotEpoch :: ArbitrarySummary -> Property
roundtripSlotEpoch s :: ArbitrarySummary
s@ArbitrarySummary{beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonSlot = SlotNo
slot} =
  ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary
s (Qry Property -> Property) -> Qry Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    (epoch, inEpoch, slotsLeft) <- SlotNo -> Qry (EpochNo, Word64, Word64)
HF.slotToEpoch SlotNo
slot
    (slot', epochSize) <- HF.epochToSlot epoch
    return $
      conjoin
        [ HF.addSlots inEpoch slot' === slot
        , inEpoch + slotsLeft === unEpochSize epochSize
        ]

roundtripEpochSlot :: ArbitrarySummary -> Property
roundtripEpochSlot :: ArbitrarySummary -> Property
roundtripEpochSlot s :: ArbitrarySummary
s@ArbitrarySummary{beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonEpoch = EpochNo
epoch} =
  ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary
s (Qry Property -> Property) -> Qry Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    (slot, epochSize) <- EpochNo -> Qry (SlotNo, EpochSize)
HF.epochToSlot EpochNo
epoch
    (epoch', inEpoch, slotsLeft) <- HF.slotToEpoch slot
    return $
      conjoin
        [ epoch' === epoch
        , inEpoch === 0
        , inEpoch + slotsLeft === unEpochSize epochSize
        ]

-- | Test that conversion between Peras rounds and slots roundtips.
--   Additionally, test that the relative slot in round and remaining
--   slots in round are withing the round length.
roundtripPerasRoundSlot :: ArbitrarySummary -> Property
roundtripPerasRoundSlot :: ArbitrarySummary -> Property
roundtripPerasRoundSlot ArbitrarySummary{mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mBeforeHorizonPerasRoundNo = Maybe PerasRoundNo
Nothing} =
  Property
forall a. a
discard
roundtripPerasRoundSlot
  s :: ArbitrarySummary
s@ArbitrarySummary{mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mBeforeHorizonPerasRoundNo = Just PerasRoundNo
perasRoundNo} =
    ArbitrarySummary -> Qry Property -> Property
noPastHorizonException ArbitrarySummary
s (Qry Property -> Property) -> Qry Property -> Property
forall a b. (a -> b) -> a -> b
$
      PerasRoundNo -> Qry (PerasEnabled (SlotNo, PerasRoundLength))
HF.perasRoundNoToSlot PerasRoundNo
perasRoundNo Qry (PerasEnabled (SlotNo, PerasRoundLength))
-> (PerasEnabled (SlotNo, PerasRoundLength) -> Qry Property)
-> Qry Property
forall a b. Qry a -> (a -> Qry b) -> Qry b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        PerasEnabled (SlotNo, PerasRoundLength)
HF.NoPerasEnabled ->
          Property -> Qry Property
forall a. a -> Qry a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Qry Property) -> Property -> Qry Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"perasRoundNoToSlot returned NoPerasEnabled" Bool
False
        HF.PerasEnabled (SlotNo
slot, PerasRoundLength Word64
perasRoundLength) -> do
          SlotNo -> Qry (PerasEnabled (PerasRoundNo, Word64, Word64))
HF.slotToPerasRoundNo SlotNo
slot Qry (PerasEnabled (PerasRoundNo, Word64, Word64))
-> (PerasEnabled (PerasRoundNo, Word64, Word64) -> Qry Property)
-> Qry Property
forall a b. Qry a -> (a -> Qry b) -> Qry b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            PerasEnabled (PerasRoundNo, Word64, Word64)
HF.NoPerasEnabled ->
              Property -> Qry Property
forall a. a -> Qry a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Qry Property) -> Property -> Qry Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"slotToPerasRoundNo returned NoPerasEnabled" Bool
False
            HF.PerasEnabled (PerasRoundNo
perasRoundNo', Word64
slotInRound, Word64
remainingSlotsInRound) ->
              Property -> Qry Property
forall a. a -> Qry a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Qry Property) -> Property -> Qry Property
forall a b. (a -> b) -> a -> b
$
                [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
                  [ PerasRoundNo
perasRoundNo' PerasRoundNo -> PerasRoundNo -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PerasRoundNo
perasRoundNo
                  , Word64
slotInRound Word64 -> Word64 -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`lt` Word64
perasRoundLength
                  , Word64
remainingSlotsInRound Word64 -> Word64 -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`le` Word64
perasRoundLength
                  ]

reportsPastHorizonWallclockToSlot :: ArbitrarySummary -> Property
reportsPastHorizonWallclockToSlot :: ArbitrarySummary -> Property
reportsPastHorizonWallclockToSlot s :: ArbitrarySummary
s@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
  case Maybe RelativeTime
mPastHorizonTime of
    Just RelativeTime
x -> ArbitrarySummary
-> Qry (SlotNo, NominalDiffTime, NominalDiffTime) -> Property
forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary
s (Qry (SlotNo, NominalDiffTime, NominalDiffTime) -> Property)
-> Qry (SlotNo, NominalDiffTime, NominalDiffTime) -> Property
forall a b. (a -> b) -> a -> b
$ RelativeTime -> Qry (SlotNo, NominalDiffTime, NominalDiffTime)
HF.wallclockToSlot RelativeTime
x
    Maybe RelativeTime
Nothing -> Property
forall a. a
discard

reportsPastHorizonSlotToWallclock :: ArbitrarySummary -> Property
reportsPastHorizonSlotToWallclock :: ArbitrarySummary -> Property
reportsPastHorizonSlotToWallclock s :: ArbitrarySummary
s@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
  case Maybe SlotNo
mPastHorizonSlot of
    Just SlotNo
x -> ArbitrarySummary -> Qry (RelativeTime, SlotLength) -> Property
forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary
s (Qry (RelativeTime, SlotLength) -> Property)
-> Qry (RelativeTime, SlotLength) -> Property
forall a b. (a -> b) -> a -> b
$ SlotNo -> Qry (RelativeTime, SlotLength)
HF.slotToWallclock SlotNo
x
    Maybe SlotNo
Nothing -> Property
forall a. a
discard

reportsPastHorizonSlotToEpoch :: ArbitrarySummary -> Property
reportsPastHorizonSlotToEpoch :: ArbitrarySummary -> Property
reportsPastHorizonSlotToEpoch s :: ArbitrarySummary
s@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
  case Maybe SlotNo
mPastHorizonSlot of
    Just SlotNo
x -> ArbitrarySummary -> Qry (EpochNo, Word64, Word64) -> Property
forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary
s (Qry (EpochNo, Word64, Word64) -> Property)
-> Qry (EpochNo, Word64, Word64) -> Property
forall a b. (a -> b) -> a -> b
$ SlotNo -> Qry (EpochNo, Word64, Word64)
HF.slotToEpoch SlotNo
x
    Maybe SlotNo
Nothing -> Property
forall a. a
discard

reportsPastHorizonEpochToSlot :: ArbitrarySummary -> Property
reportsPastHorizonEpochToSlot :: ArbitrarySummary -> Property
reportsPastHorizonEpochToSlot s :: ArbitrarySummary
s@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
  case Maybe EpochNo
mPastHorizonEpoch of
    Just EpochNo
x -> ArbitrarySummary -> Qry (SlotNo, EpochSize) -> Property
forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary
s (Qry (SlotNo, EpochSize) -> Property)
-> Qry (SlotNo, EpochSize) -> Property
forall a b. (a -> b) -> a -> b
$ EpochNo -> Qry (SlotNo, EpochSize)
HF.epochToSlot EpochNo
x
    Maybe EpochNo
Nothing -> Property
forall a. a
discard

reportsPastHorizonPerasRoundNoToSlot :: ArbitrarySummary -> Property
reportsPastHorizonPerasRoundNoToSlot :: ArbitrarySummary -> Property
reportsPastHorizonPerasRoundNoToSlot s :: ArbitrarySummary
s@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
  case Maybe PerasRoundNo
mPastHorizonPerasRoundNo of
    Just PerasRoundNo
x -> ArbitrarySummary
-> Qry (PerasEnabled (SlotNo, PerasRoundLength)) -> Property
forall a. Show a => ArbitrarySummary -> Qry a -> Property
isPastHorizonException ArbitrarySummary
s (Qry (PerasEnabled (SlotNo, PerasRoundLength)) -> Property)
-> Qry (PerasEnabled (SlotNo, PerasRoundLength)) -> Property
forall a b. (a -> b) -> a -> b
$ PerasRoundNo -> Qry (PerasEnabled (SlotNo, PerasRoundLength))
HF.perasRoundNoToSlot PerasRoundNo
x
    Maybe PerasRoundNo
Nothing -> Property
forall a. a
discard

{-------------------------------------------------------------------------------
  Arbitrary 'Summary'

  We should be able to show properties of the conversion functions independent
  of how the 'Summary' that they use is derived.
-------------------------------------------------------------------------------}

data ArbitrarySummary = forall xs. ArbitrarySummary
  { ()
arbitrarySummary :: HF.Summary xs
  , ArbitrarySummary -> RelativeTime
beforeHorizonTime :: RelativeTime
  , ArbitrarySummary -> SlotNo
beforeHorizonSlot :: SlotNo
  , ArbitrarySummary -> EpochNo
beforeHorizonEpoch :: EpochNo
  , ArbitrarySummary -> Maybe PerasRoundNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
  , ArbitrarySummary -> Maybe RelativeTime
mPastHorizonTime :: Maybe RelativeTime
  , ArbitrarySummary -> Maybe SlotNo
mPastHorizonSlot :: Maybe SlotNo
  , ArbitrarySummary -> Maybe EpochNo
mPastHorizonEpoch :: Maybe EpochNo
  , ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
  }

deriving instance Show ArbitrarySummary

instance Arbitrary ArbitrarySummary where
  arbitrary :: Gen ArbitrarySummary
arbitrary = (forall (xs :: [*]).
 (SListI xs, IsNonEmpty xs) =>
 Eras xs -> Gen ArbitrarySummary)
-> Gen ArbitrarySummary
forall r.
(forall (xs :: [*]).
 (SListI xs, IsNonEmpty xs) =>
 Eras xs -> Gen r)
-> Gen r
chooseEras ((forall (xs :: [*]).
  (SListI xs, IsNonEmpty xs) =>
  Eras xs -> Gen ArbitrarySummary)
 -> Gen ArbitrarySummary)
-> (forall (xs :: [*]).
    (SListI xs, IsNonEmpty xs) =>
    Eras xs -> Gen ArbitrarySummary)
-> Gen ArbitrarySummary
forall a b. (a -> b) -> a -> b
$ \is :: Eras xs
is@(Eras Exactly (x : xs) Era
_) -> do
    summary <- Eras xs -> Gen (Summary xs)
forall (xs :: [*]). Eras xs -> Gen (Summary xs)
genSummary Eras xs
is

    let summaryStart :: HF.Bound
        mSummaryEnd :: HF.EraEnd
        (summaryStart, mSummaryEnd) = HF.summaryBounds summary

    -- Genuine Peras bounds cannot be computed in the same way as regular slot
    -- bounds using 'HF.summaryBounds', because some eras may not have Peras
    -- enabled. Instead, we rely on 'HF.summaryPerasBounds' and derive arbitrary
    -- before and past horizon round numbers from it.
    (mBeforeHorizonPerasRoundNo, mPastHorizonPerasRoundNo) <- do
      case HF.summaryPerasBounds summary of
        -- No era supports Peras, so every round number is past the horizon.
        PerasEnabled (PerasRoundNo, Maybe PerasRoundNo)
NoPerasEnabled -> do
          pastHorizonPerasRound :: Word64 <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
1_000)
          pure
            ( Nothing
            , Just (PerasRoundNo pastHorizonPerasRound)
            )
        -- Peras is enabled for /at least/ the (last unbounded) era, so there is
        -- no 'PerasRoundNo' that is past the horizon.
        PerasEnabled (PerasRoundNo
summaryPerasStart, Maybe PerasRoundNo
Nothing) -> do
          beforeHorizonNextPerasRounds <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
1_000)
          pure
            ( Just (HF.addPerasRounds beforeHorizonNextPerasRounds summaryPerasStart)
            , Nothing
            )
        -- Peras is enabled for /at least/ one era, where the last one of those
        -- is bounded. Therefore, we have a definite horizon for 'PerasRoundNo'.
        PerasEnabled (PerasRoundNo
summaryPerasStart, Just PerasRoundNo
summaryPerasEnd) -> do
          let summaryPerasRounds :: Word64
summaryPerasRounds = HasCallStack => PerasRoundNo -> PerasRoundNo -> Word64
PerasRoundNo -> PerasRoundNo -> Word64
HF.countPerasRounds PerasRoundNo
summaryPerasEnd PerasRoundNo
summaryPerasStart
          beforeHorizonPerasRounds <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
summaryPerasRounds Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1)
          pastHorizonPerasRounds :: Word64 <- choose (0, 10)
          pure
            ( Just (HF.addPerasRounds beforeHorizonPerasRounds summaryPerasStart)
            , Just (HF.addPerasRounds pastHorizonPerasRounds summaryPerasEnd)
            )

    case mSummaryEnd of
      EraEnd
HF.EraUnbounded -> do
        -- Don't pick /too/ large numbers to avoid overflow
        beforeHorizonSlots <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
100_000_000)
        beforeHorizonEpochs <- choose (0, 1_000_000)
        beforeHorizonSeconds <- choose (0, 1_000_000_000)

        let beforeHorizonSlot :: SlotNo
            beforeHorizonEpoch :: EpochNo
            beforeHorizonTime :: RelativeTime

            beforeHorizonSlot =
              Word64 -> SlotNo -> SlotNo
HF.addSlots
                Word64
beforeHorizonSlots
                (Bound -> SlotNo
HF.boundSlot Bound
summaryStart)
            beforeHorizonEpoch =
              Word64 -> EpochNo -> EpochNo
HF.addEpochs
                Word64
beforeHorizonEpochs
                (Bound -> EpochNo
HF.boundEpoch Bound
summaryStart)
            beforeHorizonTime =
              NominalDiffTime -> RelativeTime -> RelativeTime
addRelTime
                (Double -> NominalDiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Double
beforeHorizonSeconds :: Double))
                (Bound -> RelativeTime
HF.boundTime Bound
summaryStart)
        return
          ArbitrarySummary
            { arbitrarySummary = summary
            , beforeHorizonTime
            , beforeHorizonSlot
            , beforeHorizonEpoch
            , mBeforeHorizonPerasRoundNo
            , mPastHorizonTime = Nothing
            , mPastHorizonSlot = Nothing
            , mPastHorizonEpoch = Nothing
            , mPastHorizonPerasRoundNo = Nothing
            }
      HF.EraEnd Bound
summaryEnd -> do
        let summarySlots, summaryEpochs :: Word64
            summarySlots :: Word64
summarySlots =
              HasCallStack => SlotNo -> SlotNo -> Word64
SlotNo -> SlotNo -> Word64
HF.countSlots
                (Bound -> SlotNo
HF.boundSlot Bound
summaryEnd)
                (Bound -> SlotNo
HF.boundSlot Bound
summaryStart)
            summaryEpochs :: Word64
summaryEpochs =
              HasCallStack => EpochNo -> EpochNo -> Word64
EpochNo -> EpochNo -> Word64
HF.countEpochs
                (Bound -> EpochNo
HF.boundEpoch Bound
summaryEnd)
                (Bound -> EpochNo
HF.boundEpoch Bound
summaryStart)
            summaryTimeSpan :: NominalDiffTime
            summaryTimeSpan :: NominalDiffTime
summaryTimeSpan =
              RelativeTime -> RelativeTime -> NominalDiffTime
diffRelTime
                (Bound -> RelativeTime
HF.boundTime Bound
summaryEnd)
                (Bound -> RelativeTime
HF.boundTime Bound
summaryStart)

            summaryTimeSpanSeconds :: Double
            summaryTimeSpanSeconds :: Double
summaryTimeSpanSeconds = NominalDiffTime -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac NominalDiffTime
summaryTimeSpan

        -- Pick arbitrary values before the horizon

        beforeHorizonSlots <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
summarySlots Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1)
        beforeHorizonEpochs <- choose (0, summaryEpochs - 1)
        beforeHorizonSeconds <-
          choose (0, summaryTimeSpanSeconds)
            `suchThat` \Double
x -> Double
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
/= Double
summaryTimeSpanSeconds
        let beforeHorizonSlot :: SlotNo
            beforeHorizonEpoch :: EpochNo
            beforeHorizonTime :: RelativeTime

            beforeHorizonSlot =
              Word64 -> SlotNo -> SlotNo
HF.addSlots
                Word64
beforeHorizonSlots
                (Bound -> SlotNo
HF.boundSlot Bound
summaryStart)
            beforeHorizonEpoch =
              Word64 -> EpochNo -> EpochNo
HF.addEpochs
                Word64
beforeHorizonEpochs
                (Bound -> EpochNo
HF.boundEpoch Bound
summaryStart)
            beforeHorizonTime =
              NominalDiffTime -> RelativeTime -> RelativeTime
addRelTime
                (Double -> NominalDiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
beforeHorizonSeconds)
                (Bound -> RelativeTime
HF.boundTime Bound
summaryStart)

        -- Pick arbitrary values past the horizon

        pastHorizonSlots :: Word64 <- choose (0, 10)
        pastHorizonEpochs :: Word64 <- choose (0, 10)
        pastHorizonSeconds :: Double <- choose (0, 10)

        let pastHorizonSlot :: SlotNo
            pastHorizonEpoch :: EpochNo
            pastHorizonTime :: RelativeTime

            pastHorizonSlot =
              Word64 -> SlotNo -> SlotNo
HF.addSlots
                Word64
pastHorizonSlots
                (Bound -> SlotNo
HF.boundSlot Bound
summaryEnd)
            pastHorizonEpoch =
              Word64 -> EpochNo -> EpochNo
HF.addEpochs
                Word64
pastHorizonEpochs
                (Bound -> EpochNo
HF.boundEpoch Bound
summaryEnd)
            pastHorizonTime =
              NominalDiffTime -> RelativeTime -> RelativeTime
addRelTime
                (Double -> NominalDiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
pastHorizonSeconds)
                (Bound -> RelativeTime
HF.boundTime Bound
summaryEnd)
        return
          ArbitrarySummary
            { arbitrarySummary = summary
            , beforeHorizonTime
            , beforeHorizonSlot
            , beforeHorizonEpoch
            , mBeforeHorizonPerasRoundNo
            , mPastHorizonTime = Just pastHorizonTime
            , mPastHorizonSlot = Just pastHorizonSlot
            , mPastHorizonEpoch = Just pastHorizonEpoch
            , mPastHorizonPerasRoundNo = mPastHorizonPerasRoundNo
            }

  shrink :: ArbitrarySummary -> [ArbitrarySummary]
shrink summary :: ArbitrarySummary
summary@ArbitrarySummary{Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
Summary xs
mPastHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
mPastHorizonEpoch :: ArbitrarySummary -> Maybe EpochNo
mPastHorizonSlot :: ArbitrarySummary -> Maybe SlotNo
mPastHorizonTime :: ArbitrarySummary -> Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: ArbitrarySummary -> Maybe PerasRoundNo
beforeHorizonEpoch :: ArbitrarySummary -> EpochNo
beforeHorizonSlot :: ArbitrarySummary -> SlotNo
beforeHorizonTime :: ArbitrarySummary -> RelativeTime
arbitrarySummary :: ()
arbitrarySummary :: Summary xs
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..} =
    [[ArbitrarySummary]] -> [ArbitrarySummary]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ -- Reduce before-horizon slot
        [ ArbitrarySummary
summary{beforeHorizonSlot = SlotNo s}
        | Word64
s <- Word64 -> [Word64]
forall a. Arbitrary a => a -> [a]
shrink (SlotNo -> Word64
unSlotNo SlotNo
beforeHorizonSlot)
        ]
      , -- Reduce before-horizon epoch
        [ ArbitrarySummary
summary{beforeHorizonEpoch = EpochNo e}
        | Word64
e <- Word64 -> [Word64]
forall a. Arbitrary a => a -> [a]
shrink (EpochNo -> Word64
unEpochNo EpochNo
beforeHorizonEpoch)
        ]
      , -- Reduce before-horizon time
        [ ArbitrarySummary
summary{beforeHorizonTime = RelativeTime t}
        | NominalDiffTime
t <- NominalDiffTime -> [NominalDiffTime]
forall a. Arbitrary a => a -> [a]
shrink (RelativeTime -> NominalDiffTime
getRelativeTime RelativeTime
beforeHorizonTime)
        , NominalDiffTime
t NominalDiffTime -> NominalDiffTime -> Bool
forall a. Ord a => a -> a -> Bool
>= NominalDiffTime
0
        ]
      , -- Drop an era /provided/ this doesn't cause of any of the before
        -- horizon values to become past horizon
        [ ArbitrarySummary{arbitrarySummary :: Summary xs
arbitrarySummary = Summary xs
summary', Maybe EpochNo
Maybe SlotNo
Maybe RelativeTime
Maybe PerasRoundNo
EpochNo
SlotNo
RelativeTime
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonTime :: Maybe RelativeTime
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
beforeHorizonEpoch :: EpochNo
beforeHorizonSlot :: SlotNo
beforeHorizonTime :: RelativeTime
beforeHorizonTime :: RelativeTime
beforeHorizonSlot :: SlotNo
beforeHorizonEpoch :: EpochNo
mBeforeHorizonPerasRoundNo :: Maybe PerasRoundNo
mPastHorizonTime :: Maybe RelativeTime
mPastHorizonSlot :: Maybe SlotNo
mPastHorizonEpoch :: Maybe EpochNo
mPastHorizonPerasRoundNo :: Maybe PerasRoundNo
..}
        | (Just Summary xs
summary', EraSummary
lastEra) <- [Summary xs -> (Maybe (Summary xs), EraSummary)
forall (xs :: [*]). Summary xs -> (Maybe (Summary xs), EraSummary)
HF.summaryInit Summary xs
arbitrarySummary]
        , SlotNo
beforeHorizonSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< Bound -> SlotNo
HF.boundSlot (EraSummary -> Bound
HF.eraStart EraSummary
lastEra)
        , EpochNo
beforeHorizonEpoch EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
< Bound -> EpochNo
HF.boundEpoch (EraSummary -> Bound
HF.eraStart EraSummary
lastEra)
        , RelativeTime
beforeHorizonTime RelativeTime -> RelativeTime -> Bool
forall a. Ord a => a -> a -> Bool
< Bound -> RelativeTime
HF.boundTime (EraSummary -> Bound
HF.eraStart EraSummary
lastEra)
        ]
      ]