| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.ThreadNet.Infra.TwoEras
Description
Definitions used in ThreadNet tests that involve two eras.
Synopsis
- data Partition = Partition SlotNo NumSlots
- genNonce ∷ Gen Nonce
- genPartition ∷ NumCoreNodes → NumSlots → SecurityParam → Gen Partition
- genTestConfig ∷ SecurityParam → (EpochSize, EpochSize) → Gen TestConfig
- data ReachesEra2 = ReachesEra2 {}
- activeSlotCoeff ∷ Rational
- isFirstEraBlock ∷ HardForkBlock (era ': eras) → Bool
- ledgerReachesEra2 ∷ ReachesEra2 → Bool
- mkMessageDelay ∷ Partition → CalcMessageDelay blk
- numFirstEraEpochs ∷ Num a ⇒ a
- partitionExclusiveUpperBound ∷ Partition → SlotNo
- secondEraOverlaySlots ∷ NumSlots → NumSlots → UnitInterval → EpochSize → Set SlotNo
- shelleyEpochSize ∷ SecurityParam → Word64
- label_ReachesEra2 ∷ ReachesEra2 → String
- label_hadActiveNonOverlaySlots ∷ TestOutput (HardForkBlock (era ': eras)) → Set SlotNo → String
- prop_ReachesEra2 ∷ ReachesEra2 → Property
- tabulateFinalIntersectionDepth ∷ SecurityParam → NumBlocks → String → Property → Property
- tabulatePartitionDuration ∷ SecurityParam → Partition → Property → Property
- tabulatePartitionPosition ∷ NumSlots → Partition → Bool → Property → Property
Generators
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.
genPartition ∷ NumCoreNodes → NumSlots → SecurityParam → Gen Partition Source #
Generate setupPartition
genTestConfig ∷ SecurityParam → (EpochSize, EpochSize) → Gen TestConfig Source #
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.
Era inspection
data ReachesEra2 Source #
Whether the test included second era blocks and (pre)reqs relevant to that
Note these fields are ordered alphabetically not semantically; see
label_ReachesEra2.
Constructors
| ReachesEra2 | |
Fields
| |
Instances
activeSlotCoeff ∷ Rational Source #
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.
isFirstEraBlock ∷ HardForkBlock (era ': eras) → Bool Source #
ledgerReachesEra2 ∷ ReachesEra2 → Bool Source #
Is the update proposal adopted?
mkMessageDelay ∷ Partition → CalcMessageDelay blk Source #
The temporary partition as a CalcMessageDelay
Calculates the delays that implement setupPartition.
numFirstEraEpochs ∷ Num a ⇒ a Source #
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.
secondEraOverlaySlots ∷ NumSlots → NumSlots → UnitInterval → EpochSize → Set SlotNo Source #
All OBFT overlay slots in the second era.
Properties
label_ReachesEra2 ∷ ReachesEra2 → String Source #
List the (pre)reqs in semantic order, followed by the observation
label_hadActiveNonOverlaySlots ∷ TestOutput (HardForkBlock (era ': eras)) → Set SlotNo → String Source #
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.
prop_ReachesEra2 ∷ ReachesEra2 → Property Source #
Checks if the observation satisfies the (pre)reqs