{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TypeOperators #-}

-- | Definitions used in ThreadNet tests that involve two eras.
module Test.ThreadNet.Infra.TwoEras (
    -- * Generators
    Partition (..)
  , genNonce
  , genPartition
  , genTestConfig
    -- * Era inspection
  , ReachesEra2 (..)
  , activeSlotCoeff
  , isFirstEraBlock
  , ledgerReachesEra2
  , mkMessageDelay
  , numFirstEraEpochs
  , partitionExclusiveUpperBound
  , secondEraOverlaySlots
  , shelleyEpochSize
    -- * Properties
  , label_ReachesEra2
  , label_hadActiveNonOverlaySlots
  , prop_ReachesEra2
  , tabulateFinalIntersectionDepth
  , tabulatePartitionDuration
  , tabulatePartitionPosition
  ) where

import qualified Cardano.Chain.Common as CC.Common
import           Cardano.Chain.ProtocolConstants (kEpochSlots)
import           Cardano.Chain.Slotting (unEpochSlots)
import qualified Cardano.Ledger.BaseTypes as SL
import qualified Cardano.Protocol.TPraos.Rules.Overlay as SL
import           Cardano.Slotting.EpochInfo
import           Cardano.Slotting.Slot (EpochNo (..), EpochSize (..),
                     SlotNo (..))
import           Control.Exception (assert)
import           Data.Functor ((<&>))
import qualified Data.Map.Strict as Map
import           Data.Maybe (isJust)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.SOP.Strict (NS (..))
import           Data.Word (Word64)
import           GHC.Generics (Generic)
import           Ouroboros.Consensus.Config.SecurityParam
import           Ouroboros.Consensus.HardFork.Combinator (HardForkBlock (..),
                     OneEraBlock (..))
import qualified Ouroboros.Consensus.HardFork.History.Util as Util
import           Ouroboros.Consensus.Node.ProtocolInfo
import           Ouroboros.Consensus.NodeId
import           Test.QuickCheck
import           Test.ThreadNet.General
import qualified Test.ThreadNet.Infra.Shelley as Shelley
import           Test.ThreadNet.Network (CalcMessageDelay (..), NodeOutput (..))
import           Test.ThreadNet.Util.Expectations (NumBlocks (..))
import qualified Test.ThreadNet.Util.NodeTopology as Topo
import qualified Test.Util.BoolProps as BoolProps
import           Test.Util.Orphans.Arbitrary ()
import           Test.Util.Slots (NumSlots (..))

-- | When and for how long the nodes are partitioned
--
-- The nodes are divided via message delays into two sub-networks by the parity
-- of their 'CoreNodeId'.
data Partition = Partition SlotNo NumSlots
  -- ^ the scheduled start slot and duration (which includes the start slot)
  deriving (Int -> Partition -> ShowS
[Partition] -> ShowS
Partition -> String
(Int -> Partition -> ShowS)
-> (Partition -> String)
-> ([Partition] -> ShowS)
-> Show Partition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Partition -> ShowS
showsPrec :: Int -> Partition -> ShowS
$cshow :: Partition -> String
show :: Partition -> String
$cshowList :: [Partition] -> ShowS
showList :: [Partition] -> ShowS
Show)

partitionExclusiveUpperBound :: Partition -> SlotNo
partitionExclusiveUpperBound :: Partition -> SlotNo
partitionExclusiveUpperBound (Partition SlotNo
s (NumSlots Word64
dur)) =
    Word64 -> SlotNo -> SlotNo
Util.addSlots Word64
dur SlotNo
s

genNonce :: Gen SL.Nonce
genNonce :: Gen Nonce
genNonce = [(Int, Gen Nonce)] -> Gen Nonce
forall a. (?callStack::CallStack) => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, Nonce -> Gen Nonce
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nonce
SL.NeutralNonce)
      , (Int
9, Word64 -> Nonce
SL.mkNonceFromNumber (Word64 -> Nonce) -> Gen Word64 -> Gen Nonce
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary)
      ]

-- | Generate a 'setupTestConfig' relevant to the case where the first era (eg
-- Byron) lasts for one epoch and the second era (eg Shelley) lasts for an
-- interesting number of slots.
genTestConfig :: SecurityParam -> (EpochSize, EpochSize) -> Gen TestConfig
genTestConfig :: SecurityParam -> (EpochSize, EpochSize) -> Gen TestConfig
genTestConfig SecurityParam
k (EpochSize Word64
epochSize1, EpochSize Word64
epochSize2) = do
    Seed
initSeed <- Gen Seed
forall a. Arbitrary a => Gen a
arbitrary

    NumSlots
numSlots <- do
      let wiggle :: Word64
wiggle = Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
min Word64
epochSize1 (Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* SecurityParam -> Word64
maxRollbacks SecurityParam
k)

          approachSecondEra :: Gen Word64
approachSecondEra     =
              (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
wiggle)     Gen Word64 -> (Word64 -> Word64) -> Gen Word64
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Word64
t -> Word64
epochSize1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
t Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
wiggle
          reachSecondEra :: Gen Word64
reachSecondEra        =
              (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
epochSize2) Gen Word64 -> (Word64 -> Word64) -> Gen Word64
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Word64
t -> Word64
epochSize1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
t
          reachThirdEpochOfSecondEra :: Gen Word64
reachThirdEpochOfSecondEra =
              (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
epochSize2) Gen Word64 -> (Word64 -> Word64) -> Gen Word64
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Word64
t -> Word64
epochSize1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
epochSize2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
t

      (Word64 -> NumSlots) -> Gen Word64 -> Gen NumSlots
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word64 -> NumSlots
NumSlots (Gen Word64 -> Gen NumSlots) -> Gen Word64 -> Gen NumSlots
forall a b. (a -> b) -> a -> b
$ [(Int, Gen Word64)] -> Gen Word64
forall a. (?callStack::CallStack) => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen Word64)] -> Gen Word64)
-> [(Int, Gen Word64)] -> Gen Word64
forall a b. (a -> b) -> a -> b
$
        [ (Int
05, Gen Word64
approachSecondEra)
        , (Int
64, Gen Word64
reachSecondEra)
        , (Int
31, Gen Word64
reachThirdEpochOfSecondEra)
        ]

    -- This test has more slots than most, so we de-emphasize the relatively
    -- expensive n=5 case. For example:
    --
    -- > 250 tests with 30% 2, 30% 3, 30% 4, and 10% 5 took 500s
    -- > 250 tests with 100% 5 took 1000s
    Word64
ncn <- [(Int, Gen Word64)] -> Gen Word64
forall a. (?callStack::CallStack) => [(Int, Gen a)] -> Gen a
frequency [(Int
9, (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
2, Word64
4)), (Int
1, Word64 -> Gen Word64
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
5)]

    -- Ensure that each partition class is internally connected.
    NodeTopology
nodeTopology <- do
      NodeTopology
topo0   <- (?callStack::CallStack) => NumCoreNodes -> Gen NodeTopology
NumCoreNodes -> Gen NodeTopology
Topo.genNodeTopology (NumCoreNodes -> Gen NodeTopology)
-> NumCoreNodes -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$ Word64 -> NumCoreNodes
NumCoreNodes Word64
ncn
      NodeTopology
oddTopo <- do
        -- eg nodes 1 3 for ncn = 5
        NodeTopology
topo <- (?callStack::CallStack) => NumCoreNodes -> Gen NodeTopology
NumCoreNodes -> Gen NodeTopology
Topo.genNodeTopology (NumCoreNodes -> Gen NodeTopology)
-> NumCoreNodes -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$ Word64 -> NumCoreNodes
NumCoreNodes (Word64 -> NumCoreNodes) -> Word64 -> NumCoreNodes
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
div Word64
ncn Word64
2
        let rename :: CoreNodeId -> CoreNodeId
rename (CoreNodeId Word64
i) = Word64 -> CoreNodeId
CoreNodeId (Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
        NodeTopology -> Gen NodeTopology
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeTopology -> Gen NodeTopology)
-> NodeTopology -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$ (CoreNodeId -> CoreNodeId) -> NodeTopology -> NodeTopology
Topo.mapNodeTopology CoreNodeId -> CoreNodeId
rename NodeTopology
topo
      NodeTopology
evenTopo <- do
        -- eg nodes 0 2 4 for ncn = 5
        NodeTopology
topo <- (?callStack::CallStack) => NumCoreNodes -> Gen NodeTopology
NumCoreNodes -> Gen NodeTopology
Topo.genNodeTopology (NumCoreNodes -> Gen NodeTopology)
-> NumCoreNodes -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$ Word64 -> NumCoreNodes
NumCoreNodes (Word64 -> NumCoreNodes) -> Word64 -> NumCoreNodes
forall a b. (a -> b) -> a -> b
$ Word64
ncn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
div Word64
ncn Word64
2
        let rename :: CoreNodeId -> CoreNodeId
rename (CoreNodeId Word64
i) = Word64 -> CoreNodeId
CoreNodeId (Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
i)
        NodeTopology -> Gen NodeTopology
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeTopology -> Gen NodeTopology)
-> NodeTopology -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$ (CoreNodeId -> CoreNodeId) -> NodeTopology -> NodeTopology
Topo.mapNodeTopology CoreNodeId -> CoreNodeId
rename NodeTopology
topo
      NodeTopology -> Gen NodeTopology
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeTopology -> Gen NodeTopology)
-> NodeTopology -> Gen NodeTopology
forall a b. (a -> b) -> a -> b
$
        NodeTopology -> NodeTopology -> NodeTopology
Topo.unionNodeTopology NodeTopology
evenTopo (NodeTopology -> NodeTopology) -> NodeTopology -> NodeTopology
forall a b. (a -> b) -> a -> b
$
        NodeTopology -> NodeTopology -> NodeTopology
Topo.unionNodeTopology NodeTopology
oddTopo (NodeTopology -> NodeTopology) -> NodeTopology -> NodeTopology
forall a b. (a -> b) -> a -> b
$
        NodeTopology
topo0

    TestConfig -> Gen TestConfig
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TestConfig
      { Seed
initSeed :: Seed
initSeed :: Seed
initSeed
      , NodeTopology
nodeTopology :: NodeTopology
nodeTopology :: NodeTopology
nodeTopology
      , numCoreNodes :: NumCoreNodes
numCoreNodes = Word64 -> NumCoreNodes
NumCoreNodes Word64
ncn
      , NumSlots
numSlots :: NumSlots
numSlots :: NumSlots
numSlots
      }

-- | Generate 'setupPartition'
genPartition :: NumCoreNodes -> NumSlots -> SecurityParam -> Gen Partition
genPartition :: NumCoreNodes -> NumSlots -> SecurityParam -> Gen Partition
genPartition (NumCoreNodes Word64
n) (NumSlots Word64
t) (SecurityParam Word64
k) = do
    let ultimateSlot :: Word64
        ultimateSlot :: Word64
ultimateSlot = Bool -> Word64 -> Word64
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Word64
t Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0) (Word64 -> Word64) -> Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Word64
t Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1

        crop :: Word64 -> Word64
        crop :: Word64 -> Word64
crop Word64
s = Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
min Word64
ultimateSlot Word64
s

    -- Fundamental plan: all @MsgRollForward@ sent during the partition only
    -- arrive at the onset of slot after it. The partition begins at the onset
    -- of @firstSlotIn@ and ends at the onset of @firstSlotAfter@.

    -- FACT (A) The leader of @firstSlotAfter@ will forge before fully reacting
    -- to the @MsgRollForward@s that just arrived, due to a race in the test
    -- infrastructure that is consistently won by the forge. Thus the two
    -- class's unique extensions consist of the blocks forged in the slots from
    -- @firstSlotIn@ to @firstSlotAfter@ /inclusive/.

    -- @w@ is defined below this large comment to be how long the partition
    -- should last (this may be 'crop'ped farther below if the partition ends
    -- up near the end of the test)
    --
    -- Because of FACT (A), we limit the partition duration so that at least
    -- one of the two partition classes will forge /strictly/ /less/ /than/ @k@
    -- such blocks. While both classes would be able to rollback if we let them
    -- forge @k@ such blocks, they might (TODO "might" or "will"?) not able to
    -- /decide/ that they need to rollback, since the relevant ChainSync client
    -- might (TODO will?) not be able to forecast a ledger view far-enough into
    -- the future to validate the @k+1@st header from the other class after the
    -- partition ends. It will remain unaware that a longer chain exists and
    -- end up stuck on its own distinct chain. Hence it's a Common Prefix
    -- violation.
    --
    -- We therefore motivate an upper bound on the partition duration @w@ for a
    -- net with @n@ nodes by considering the two variables' parities.
    --
    -- o For @n = 2h@ nodes and @w = 2u@ slots, the classes respectively forge
    --   @u@ and @u+1@ blocks. (The @+1@th block is forged in
    --   @firstSlotAfter@.) The preceding paragraph requires @u < k@ requires
    --   @u <= k-1@ requires @w <= 2k-2@. So @w <= 2k-2@ when @w@ is even.
    --
    -- o For @n = 2h@ nodes and @w = 2u+1@ slots, the classes both forge @u+1@
    --   blocks. (The second @+1@th block is forged in @firstSlotAfter@.) The
    --   preceding paragraph requires @u+1 < k@ requires @u <= k-2@ requires @w
    --   <= 2k-3@. So @w <= 2k-3@ when @w@ is odd. Note that @w <= 2k-2@ is
    --   equivalent since @w@ is assumed odd.
    --
    -- o For @n = 2h+1@ nodes, the smaller class forges at most the number of
    --   blocks considered in the above cases for even @n@, so this case
    --   doesn't contribute anything novel to the upper bound. The smaller
    --   class has less than half of the nodes and so will violate Chain Growth
    --   /if/ /given/ /enough/ /time/ /alone/. But for Byron at least, the
    --   logic for avoiding a Common Prefix violation already establishes a
    --   sufficiently strict upper bound to preclude a Chain Growth violation,
    --   since Chain Growth isn't technically violated until @2k@ slots have
    --   passed (it's also relevant that the net forges at full round-robin
    --   speed until the partition starts). (TODO does that cover Shelley too?)
    --
    -- Thus @w@ can range from @0@ to @2k-2@ inclusive.
    Word64
w <- Bool -> Gen Word64 -> Gen Word64
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Word64
k Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0) (Gen Word64 -> Gen Word64) -> Gen Word64 -> Gen Word64
forall a b. (a -> b) -> a -> b
$ (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
2)

    -- Each of the the following milestones happens at the listed slot in the
    -- absence of a partition.
    --
    -- o In slots 0 and 1 the proposal and the votes confirm it
    --
    -- o In slot 2k+1 the confirmation becomes stable
    --
    -- o In slot 2k+1+quorum the nodes endorse it
    --
    -- o In slot 4k+1+quorum the endorsement is stable
    --
    -- o In slot 10k the update is adopted.
    --
    -- We are most interested in what happens when the partition is near these
    -- milestones.
    Maybe Word64
mbFocus <- do
      let quorum :: Word64
quorum = Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
div Word64
n Word64
2   -- in the right ballpark
      [(Int, Gen (Maybe Word64))] -> Gen (Maybe Word64)
forall a. (?callStack::CallStack) => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Maybe Word64))] -> Gen (Maybe Word64))
-> [(Int, Gen (Maybe Word64))] -> Gen (Maybe Word64)
forall a b. (a -> b) -> a -> b
$
        ((Int, Maybe Word64) -> (Int, Gen (Maybe Word64)))
-> [(Int, Maybe Word64)] -> [(Int, Gen (Maybe Word64))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
wgt, Maybe Word64
mbDur) -> (Int
wgt, Maybe Word64 -> Gen (Maybe Word64)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Word64
mbDur)) ([(Int, Maybe Word64)] -> [(Int, Gen (Maybe Word64))])
-> [(Int, Maybe Word64)] -> [(Int, Gen (Maybe Word64))]
forall a b. (a -> b) -> a -> b
$
        ((Int, Maybe Word64) -> Bool)
-> [(Int, Maybe Word64)] -> [(Int, Maybe Word64)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> (Word64 -> Bool) -> Maybe Word64 -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
t) (Maybe Word64 -> Bool)
-> ((Int, Maybe Word64) -> Maybe Word64)
-> (Int, Maybe Word64)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Maybe Word64) -> Maybe Word64
forall a b. (a, b) -> b
snd)
          [ (Int
5,  Maybe Word64
forall a. Maybe a
Nothing)
          , (Int
1,  Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
0)
          , (Int
1,  Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
          , (Int
1,  Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
quorum)
          , (Int
1,  Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ Word64
4 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
          , (Int
1,  Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ Word64
4 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
quorum)
          , (Int
20, Bool -> Maybe Word64 -> Maybe Word64
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
forall a. Num a => a
numFirstEraEpochs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (Int
1 :: Int)) (Maybe Word64 -> Maybe Word64) -> Maybe Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$
                 Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> Word64
byronEpochSize (Word64 -> SecurityParam
SecurityParam Word64
k))
          ]

    -- Position the partition so that it at least abuts the focus slot.
    Word64
firstSlotIn <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose ((Word64, Word64) -> Gen Word64) -> (Word64, Word64) -> Gen Word64
forall a b. (a -> b) -> a -> b
$
      case Maybe Word64
mbFocus of
        Maybe Word64
Nothing    -> (Word64
0,                            Word64
ultimateSlot    )
        Just Word64
focus -> (Word64 -> Word64
crop (Word64 -> Word64) -> Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Word64
focus Word64 -> Word64 -> Word64
forall a. (Num a, Ord a) => a -> a -> a
`monus` (Word64
w Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1), Word64 -> Word64
crop (Word64 -> Word64) -> Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Word64
focus Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)

    let -- Because of FACT (A), we require there to be at least one slot after
        -- the partition. This doesn't ensure full consensus, because the block
        -- forged in @firstSlotAfter@ may create a chain as long as that of the
        -- other partition (first era) or even multiple such chains (second
        -- era). But it does ensure that all final chains will be the same
        -- length.
        firstSlotAfter :: Word64
        firstSlotAfter :: Word64
firstSlotAfter = Word64 -> Word64
crop (Word64 -> Word64) -> Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Word64
firstSlotIn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
w

        dur :: Word64
        dur :: Word64
dur = (?callStack::CallStack) => SlotNo -> SlotNo -> Word64
SlotNo -> SlotNo -> Word64
Util.countSlots (Word64 -> SlotNo
SlotNo Word64
firstSlotAfter) (Word64 -> SlotNo
SlotNo Word64
firstSlotIn)

    Partition -> Gen Partition
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Partition -> Gen Partition) -> Partition -> Gen Partition
forall a b. (a -> b) -> a -> b
$ SlotNo -> NumSlots -> Partition
Partition (Word64 -> SlotNo
SlotNo Word64
firstSlotIn) (Word64 -> NumSlots
NumSlots Word64
dur)

-- | Whether there was a block forged in a non-overlay slot in the second era.
--
-- This event evidences that the stake pools were correctly created and
-- delegated to.
label_hadActiveNonOverlaySlots ::
     TestOutput (HardForkBlock (era ': eras))
  -> Set SlotNo
  -> String
label_hadActiveNonOverlaySlots :: forall era (eras :: [*]).
TestOutput (HardForkBlock (era : eras)) -> Set SlotNo -> String
label_hadActiveNonOverlaySlots TestOutput (HardForkBlock (era : eras))
testOutput Set SlotNo
overlaySlots =
    Bool -> String
forall a. Show a => a -> String
show (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$
    [ SlotNo -> Set SlotNo -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember SlotNo
slot Set SlotNo
overlaySlots
    | (NodeId
_nid, NodeOutput (HardForkBlock (era : eras))
no) <- Map NodeId (NodeOutput (HardForkBlock (era : eras)))
-> [(NodeId, NodeOutput (HardForkBlock (era : eras)))]
forall k a. Map k a -> [(k, a)]
Map.toList Map NodeId (NodeOutput (HardForkBlock (era : eras)))
testOutputNodes
    , let NodeOutput{Map SlotNo (HardForkBlock (era : eras))
nodeOutputForges :: Map SlotNo (HardForkBlock (era : eras))
nodeOutputForges :: forall blk. NodeOutput blk -> Map SlotNo blk
nodeOutputForges} = NodeOutput (HardForkBlock (era : eras))
no
    , (SlotNo
slot, HardForkBlock (era : eras)
blk) <- Map SlotNo (HardForkBlock (era : eras))
-> [(SlotNo, HardForkBlock (era : eras))]
forall k a. Map k a -> [(k, a)]
Map.toDescList Map SlotNo (HardForkBlock (era : eras))
nodeOutputForges
    , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ HardForkBlock (era : eras) -> Bool
forall era (eras :: [*]). HardForkBlock (era : eras) -> Bool
isFirstEraBlock HardForkBlock (era : eras)
blk
    ]
  where
    TestOutput{Map NodeId (NodeOutput (HardForkBlock (era : eras)))
testOutputNodes :: Map NodeId (NodeOutput (HardForkBlock (era : eras)))
testOutputNodes :: forall blk. TestOutput blk -> Map NodeId (NodeOutput blk)
testOutputNodes} = TestOutput (HardForkBlock (era : eras))
testOutput

-- | All OBFT overlay slots in the second era.
secondEraOverlaySlots ::
     NumSlots
  -> NumSlots
  -> SL.UnitInterval
  -> EpochSize
  -> Set SlotNo
secondEraOverlaySlots :: NumSlots -> NumSlots -> UnitInterval -> EpochSize -> Set SlotNo
secondEraOverlaySlots NumSlots
numSlots (NumSlots Word64
numFirstEraSlots) UnitInterval
d EpochSize
secondEraEpochSize =
    (SlotNo -> Bool) -> Set SlotNo -> Set SlotNo
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< Word64 -> SlotNo
SlotNo Word64
t) (Set SlotNo -> Set SlotNo) -> Set SlotNo -> Set SlotNo
forall a b. (a -> b) -> a -> b
$
    [Set SlotNo] -> Set SlotNo
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SlotNo] -> Set SlotNo) -> [Set SlotNo] -> Set SlotNo
forall a b. (a -> b) -> a -> b
$
    (Set SlotNo -> Bool) -> [Set SlotNo] -> [Set SlotNo]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Maybe SlotNo -> Bool
forall a. Maybe a -> Bool
isJust (Maybe SlotNo -> Bool)
-> (Set SlotNo -> Maybe SlotNo) -> Set SlotNo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Set SlotNo -> Maybe SlotNo
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLT (Word64 -> SlotNo
SlotNo Word64
t)) ([Set SlotNo] -> [Set SlotNo]) -> [Set SlotNo] -> [Set SlotNo]
forall a b. (a -> b) -> a -> b
$
    (Word64 -> Set SlotNo) -> [Word64] -> [Set SlotNo]
forall a b. (a -> b) -> [a] -> [b]
map Word64 -> Set SlotNo
overlayOffsets [Word64
0..]
  where
    NumSlots Word64
t = NumSlots
numSlots

    -- The overlay slots in the ith epoch of the second era.
    --
    -- TODO: This function conceptually should be simpler if we created a
    -- sufficiently accurate 'EpochInfo' and so didn't need the shift. But
    -- doing so (eg by constructing a HardFork @Summary@) is currently
    -- significantly more involved than this workaround.
    overlayOffsets :: Word64 -> Set SlotNo
    overlayOffsets :: Word64 -> Set SlotNo
overlayOffsets Word64
i =
        -- Shift to account for the first era.
        (SlotNo -> SlotNo) -> Set SlotNo -> Set SlotNo
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (Word64 -> SlotNo -> SlotNo
Util.addSlots Word64
numFirstEraSlots) (Set SlotNo -> Set SlotNo)
-> ([SlotNo] -> Set SlotNo) -> [SlotNo] -> Set SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        [SlotNo] -> Set SlotNo
forall a. Ord a => [a] -> Set a
Set.fromList ([SlotNo] -> Set SlotNo) -> [SlotNo] -> Set SlotNo
forall a b. (a -> b) -> a -> b
$
        -- Note: this is only correct if each epoch uses the same value for @d@
        SlotNo -> UnitInterval -> EpochSize -> [SlotNo]
SL.overlaySlots
          -- Suitable only for this narrow context
          (EpochSize -> EpochNo -> SlotNo
fixedEpochInfoFirst EpochSize
secondEraEpochSize (Word64 -> EpochNo
EpochNo Word64
i))
          -- notably contains setupD
          UnitInterval
d
            -- NB 0 <-> the first epoch of the second era
          EpochSize
secondEraEpochSize

tabulatePartitionPosition ::
     NumSlots -> Partition -> Bool -> Property -> Property
tabulatePartitionPosition :: NumSlots -> Partition -> Bool -> Property -> Property
tabulatePartitionPosition (NumSlots Word64
numFirstEraSlots) Partition
part Bool
transitions =
    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"partition in or abuts era (First era, Second era)"
      [ (Bool, Bool) -> String
forall a. Show a => a -> String
show (Bool
inclFirstEra, Bool
inclSecondEra) ]
  where
    Partition (SlotNo Word64
firstSlotIn) (NumSlots Word64
dur) = Partition
part
    firstSlotAfter :: Word64
firstSlotAfter                                = Word64
firstSlotIn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
dur

    inclFirstEra :: Bool
inclFirstEra  =
        Word64
dur Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0 Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
transitions Bool -> Bool -> Bool
|| Word64
firstSlotIn    Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
numFirstEraSlots)
    inclSecondEra :: Bool
inclSecondEra =
        Word64
dur Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
0 Bool -> Bool -> Bool
&& (Bool
transitions     Bool -> Bool -> Bool
&& Word64
firstSlotAfter Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
numFirstEraSlots)

tabulateFinalIntersectionDepth :: SecurityParam -> NumBlocks -> String -> Property -> Property
tabulateFinalIntersectionDepth :: SecurityParam -> NumBlocks -> String -> Property -> Property
tabulateFinalIntersectionDepth SecurityParam
k (NumBlocks Word64
finalIntersectionDepth) String
finalBlockEra =
    String -> String -> Property -> Property
tabul String
"count"  (Word64 -> String
forall a. Show a => a -> String
show          Word64
finalIntersectionDepth) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> String -> Property -> Property
tabul String
"k frac" (SecurityParam -> Word64 -> String
approxFracK SecurityParam
k Word64
finalIntersectionDepth) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> String -> Property -> Property
tabul String
"k diff" (SecurityParam -> Word64 -> String
diffK       SecurityParam
k Word64
finalIntersectionDepth)
  where
    lbl :: String
lbl = String
"final intersection depth"
    tabul :: String -> String -> Property -> Property
tabul String
s String
x = String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate
        (String
lbl String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
finalBlockEra String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s)
        [String
x String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" blocks"]

tabulatePartitionDuration :: SecurityParam -> Partition -> Property -> Property
tabulatePartitionDuration :: SecurityParam -> Partition -> Property -> Property
tabulatePartitionDuration SecurityParam
k Partition
part =
    String -> String -> Property -> Property
forall {prop}.
Testable prop =>
String -> String -> prop -> Property
tabul String
"count"  (Word64 -> String
forall a. Show a => a -> String
show          Word64
dur) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> String -> Property -> Property
forall {prop}.
Testable prop =>
String -> String -> prop -> Property
tabul String
"k frac" (SecurityParam -> Word64 -> String
approxFracK SecurityParam
k Word64
dur)
  where
    tabul :: String -> String -> prop -> Property
tabul String
s String
x =
        String -> [String] -> prop -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate (String
"partition duration, " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s) [String
x String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" slots"]

    Partition SlotNo
_ (NumSlots Word64
dur) = Partition
part

{-------------------------------------------------------------------------------
  Constants
-------------------------------------------------------------------------------}

-- | The active slot coefficient, @f@.
--
-- Some of these tests include epochs in the second era in which stakepools are
-- actually leading. In that case, the @k@, @d@, and @f@ parameters and the
-- length of any scheduled network partitions need to be balanced so that Common
-- Prefix violations (in particular, wedges) are extremely unlikely.
activeSlotCoeff :: Rational
activeSlotCoeff :: Rational
activeSlotCoeff = Rational
0.2   -- c.f. mainnet is more conservative, using 0.05

-- | The number of epochs in the first era in this test
--
-- All nodes join in slot 0, we generate the proposal in slot 0, we also
-- generate the votes in slot 0, and the nodes are endorsing the proposal as of
-- slot 0. Thus we expect that the first era will end after one epoch. Otherwise
-- it would indicate some sort of protocol failure.
numFirstEraEpochs :: Num a => a
numFirstEraEpochs :: forall a. Num a => a
numFirstEraEpochs = a
1

{-------------------------------------------------------------------------------
  ReachesEra2 property
-------------------------------------------------------------------------------}

-- | Whether the test included second era blocks and (pre)reqs relevant to that
--
-- Note these fields are ordered alphabetically not semantically; see
-- 'label_ReachesEra2'.
data ReachesEra2 = ReachesEra2
  { ReachesEra2 -> Prereq
rsEra1Slots  :: BoolProps.Prereq
    -- ^ enough slots in the first era to enable a block in the second era
  , ReachesEra2 -> Prereq
rsPV         :: BoolProps.Prereq
    -- ^ sufficient protocol version to enable a block in the second era
  , ReachesEra2 -> Bool
rsEra2Blocks :: Bool
    -- ^ blocks from the second era included in final chains
  , ReachesEra2 -> Requirement
rsEra2Slots  :: BoolProps.Requirement
    -- ^ enough slots in the second era to necessitate a block in the second era
  }
  deriving ((forall x. ReachesEra2 -> Rep ReachesEra2 x)
-> (forall x. Rep ReachesEra2 x -> ReachesEra2)
-> Generic ReachesEra2
forall x. Rep ReachesEra2 x -> ReachesEra2
forall x. ReachesEra2 -> Rep ReachesEra2 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ReachesEra2 -> Rep ReachesEra2 x
from :: forall x. ReachesEra2 -> Rep ReachesEra2 x
$cto :: forall x. Rep ReachesEra2 x -> ReachesEra2
to :: forall x. Rep ReachesEra2 x -> ReachesEra2
Generic, Int -> ReachesEra2 -> ShowS
[ReachesEra2] -> ShowS
ReachesEra2 -> String
(Int -> ReachesEra2 -> ShowS)
-> (ReachesEra2 -> String)
-> ([ReachesEra2] -> ShowS)
-> Show ReachesEra2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ReachesEra2 -> ShowS
showsPrec :: Int -> ReachesEra2 -> ShowS
$cshow :: ReachesEra2 -> String
show :: ReachesEra2 -> String
$cshowList :: [ReachesEra2] -> ShowS
showList :: [ReachesEra2] -> ShowS
Show)

instance BoolProps.CollectReqs ReachesEra2

-- | List the (pre)reqs in semantic order, followed by the observation
label_ReachesEra2 :: ReachesEra2 -> String
label_ReachesEra2 :: ReachesEra2 -> String
label_ReachesEra2 ReachesEra2
reachesEra2 =
    String -> Prereq -> ShowS
forall a. Show a => String -> a -> ShowS
prepend String
"pv"     Prereq
rsPV ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> Prereq -> ShowS
forall a. Show a => String -> a -> ShowS
prepend String
"slots1" Prereq
rsEra1Slots ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> Requirement -> ShowS
forall a. Show a => String -> a -> ShowS
prepend String
"slots2" Requirement
rsEra2Slots ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String
"blocks2 " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Bool -> String
forall a. Show a => a -> String
show Bool
rsEra2Blocks
  where
    -- incur a GHC warning if the number of fields changes
    ReachesEra2 Prereq
_ Prereq
_ Bool
_ Requirement
_dummy = ReachesEra2
reachesEra2
    -- this pattern should bind each field by name
    ReachesEra2
      { Prereq
rsEra1Slots :: ReachesEra2 -> Prereq
rsEra1Slots :: Prereq
rsEra1Slots
      , Prereq
rsPV :: ReachesEra2 -> Prereq
rsPV :: Prereq
rsPV
      , Bool
rsEra2Blocks :: ReachesEra2 -> Bool
rsEra2Blocks :: Bool
rsEra2Blocks
      , Requirement
rsEra2Slots :: ReachesEra2 -> Requirement
rsEra2Slots :: Requirement
rsEra2Slots
      } = ReachesEra2
reachesEra2

    prepend :: Show a => String -> a -> String -> String
    prepend :: forall a. Show a => String -> a -> ShowS
prepend String
s a
req String
x = String
s String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
req String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
x

-- | Is the update proposal adopted?
ledgerReachesEra2 :: ReachesEra2 -> Bool
ledgerReachesEra2 :: ReachesEra2 -> Bool
ledgerReachesEra2 ReachesEra2
rs = ReachesEra2 -> Maybe Bool
forall a. CollectReqs a => a -> Maybe Bool
BoolProps.checkReqs ReachesEra2
rs Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False

-- | Checks if the observation satisfies the (pre)reqs
prop_ReachesEra2 :: ReachesEra2 -> Property
prop_ReachesEra2 :: ReachesEra2 -> Property
prop_ReachesEra2 ReachesEra2
rs = case ReachesEra2 -> Maybe Bool
forall a. CollectReqs a => a -> Maybe Bool
BoolProps.checkReqs ReachesEra2
rs of
    Maybe Bool
Nothing  -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    Just Bool
req ->
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (ReachesEra2 -> String
forall a. Show a => a -> String
show ReachesEra2
rs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Bool -> String
msg Bool
req) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
        Bool
rsEra2Blocks Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
req
  where
    ReachesEra2{Bool
rsEra2Blocks :: ReachesEra2 -> Bool
rsEra2Blocks :: Bool
rsEra2Blocks} = ReachesEra2
rs

    msg :: Bool -> String
    msg :: Bool -> String
msg Bool
req = if Bool
req
        then String
"the final chains should include at least one second era block"
        else String
"the final chains should not include any second era blocks"

{-------------------------------------------------------------------------------
  A short even-odd partition
-------------------------------------------------------------------------------}

-- | The temporary partition as a 'CalcMessageDelay'
--
-- Calculates the delays that implement 'setupPartition'.
mkMessageDelay :: Partition -> CalcMessageDelay blk
mkMessageDelay :: forall blk. Partition -> CalcMessageDelay blk
mkMessageDelay Partition
part = ((CoreNodeId, CoreNodeId) -> SlotNo -> Header blk -> NumSlots)
-> CalcMessageDelay blk
forall blk.
((CoreNodeId, CoreNodeId) -> SlotNo -> Header blk -> NumSlots)
-> CalcMessageDelay blk
CalcMessageDelay (((CoreNodeId, CoreNodeId) -> SlotNo -> Header blk -> NumSlots)
 -> CalcMessageDelay blk)
-> ((CoreNodeId, CoreNodeId) -> SlotNo -> Header blk -> NumSlots)
-> CalcMessageDelay blk
forall a b. (a -> b) -> a -> b
$
    \(CoreNodeId Word64
i, CoreNodeId Word64
j) SlotNo
curSlot Header blk
_hdr -> Word64 -> NumSlots
NumSlots (Word64 -> NumSlots) -> Word64 -> NumSlots
forall a b. (a -> b) -> a -> b
$ if
      | SlotNo
curSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<  SlotNo
firstSlotIn    -> Word64
0
      | SlotNo
curSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= SlotNo
firstSlotAfter -> Word64
0
      | Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod Word64
i Word64
2 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod Word64
j Word64
2        -> Word64
0
      | Bool
otherwise                 -> SlotNo -> Word64
unSlotNo (SlotNo -> Word64) -> SlotNo -> Word64
forall a b. (a -> b) -> a -> b
$ SlotNo
firstSlotAfter SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
- SlotNo
curSlot
  where
    Partition SlotNo
firstSlotIn NumSlots
_ = Partition
part
    firstSlotAfter :: SlotNo
firstSlotAfter          = Partition -> SlotNo
partitionExclusiveUpperBound Partition
part

{-------------------------------------------------------------------------------
  Miscellany
-------------------------------------------------------------------------------}

byronEpochSize :: SecurityParam -> Word64
byronEpochSize :: SecurityParam -> Word64
byronEpochSize (SecurityParam Word64
k) =
    EpochSlots -> Word64
unEpochSlots (EpochSlots -> Word64) -> EpochSlots -> Word64
forall a b. (a -> b) -> a -> b
$ BlockCount -> EpochSlots
kEpochSlots (BlockCount -> EpochSlots) -> BlockCount -> EpochSlots
forall a b. (a -> b) -> a -> b
$ Word64 -> BlockCount
CC.Common.BlockCount Word64
k

shelleyEpochSize :: SecurityParam -> Word64
shelleyEpochSize :: SecurityParam -> Word64
shelleyEpochSize SecurityParam
k = EpochSize -> Word64
unEpochSize (EpochSize -> Word64) -> EpochSize -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> Rational -> EpochSize
Shelley.mkEpochSize SecurityParam
k Rational
activeSlotCoeff

isFirstEraBlock :: HardForkBlock (era ': eras) -> Bool
isFirstEraBlock :: forall era (eras :: [*]). HardForkBlock (era : eras) -> Bool
isFirstEraBlock = \case
    HardForkBlock (OneEraBlock Z{}) -> Bool
True
    HardForkBlock (era : eras)
_                               -> Bool
False

-- | Render a number as a positive difference from @k@
--
-- PREREQUISITE: The number must not be greater than @k@.
diffK :: SecurityParam -> Word64 -> String
diffK :: SecurityParam -> Word64 -> String
diffK (SecurityParam Word64
k) Word64
v =
    Bool -> ShowS
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Word64
k Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
v) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String
"k - " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Word64 -> String
forall a. Show a => a -> String
show (Word64
k Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
v)

-- | Render a number as the nearest tenths of @k@
approxFracK :: SecurityParam -> Word64 -> String
approxFracK :: SecurityParam -> Word64 -> String
approxFracK (SecurityParam Word64
k) Word64
v =
    String
"k * " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Double -> String
forall a. Show a => a -> String
show (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
tenths Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10 :: Double)
  where
    ratio :: Rational
ratio  = Word64 -> Rational
forall a. Real a => a -> Rational
toRational Word64
v Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Word64 -> Rational
forall a. Real a => a -> Rational
toRational Word64
k
    tenths :: Int
tenths = Rational -> Int
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Rational
ratio Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
10) :: Int

-- | <https://en.wikipedia.org/wiki/Monus>
monus :: (Num a, Ord a) => a -> a -> a
monus :: forall a. (Num a, Ord a) => a -> a -> a
monus a
a a
b = if a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b then a
0 else a
a a -> a -> a
forall a. Num a => a -> a -> a
- a
b