Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data ChainSchema base inner = ChainSchema !(Contains SlotE base inner) !(Vector inner SlotE S)
- data CheckedHonestRecipe base hon = UnsafeCheckedHonestRecipe {
- chrScgDensity ∷ !(SomeDensityWindow NotInverted)
- chrWin ∷ !(Contains SlotE base hon)
- data HonestLbl
- data HonestRecipe = HonestRecipe !Kcp !Scg !Delta !Len
- data NoSuchHonestChainSchema
- data SomeCheckedHonestRecipe = ∀ base hon. SomeCheckedHonestRecipe !(Proxy base) !(Proxy hon) !(CheckedHonestRecipe base hon)
- data SomeHonestChainSchema = ∀ base hon. SomeHonestChainSchema !(Proxy base) !(Proxy hon) !(ChainSchema base hon)
- checkHonestRecipe ∷ HonestRecipe → Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
- countChainSchema ∷ ChainSchema base inner → Size inner ActiveSlotE
- genHonestRecipe ∷ Gen HonestRecipe
- uniformTheHonestChain ∷ ∀ base hon g. RandomGen g ⇒ Maybe Asc → CheckedHonestRecipe base hon → g → ChainSchema base hon
- data HonestChainViolation hon
- = BadCount
- | BadScgWindow !(ScgViolation hon)
- | BadLength !(Size hon SlotE)
- data ScgLbl
- data ScgViolation hon = ∀ skolem.ScgViolation {
- scgvPopCount ∷ !(Size (Win ScgLbl skolem) ActiveSlotE)
- scgvWindow ∷ !(Contains SlotE hon (Win ScgLbl skolem))
- checkHonestChain ∷ ∀ base hon. HonestRecipe → ChainSchema base hon → Except (HonestChainViolation hon) ()
- prettyChainSchema ∷ ∀ base inner. ChainSchema base inner → String → [String]
- prettyWindow ∷ Contains SlotE base inner → String → String
Generating
data ChainSchema base inner Source #
The leader schedule of an honest chain
The represented chain grows by one block per active slot. A different data type would represent a leader schedule in which leaders do not necessarily extend the block from the previous active slot.
INVARIANT: at least one active slot
Instances
Read (ChainSchema base inner) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest readsPrec ∷ Int → ReadS (ChainSchema base inner) # readList ∷ ReadS [ChainSchema base inner] # readPrec ∷ ReadPrec (ChainSchema base inner) # readListPrec ∷ ReadPrec [ChainSchema base inner] # | |
Show (ChainSchema base inner) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest showsPrec ∷ Int → ChainSchema base inner → ShowS # show ∷ ChainSchema base inner → String # showList ∷ [ChainSchema base inner] → ShowS # | |
Eq (ChainSchema base inner) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest (==) ∷ ChainSchema base inner → ChainSchema base inner → Bool # (/=) ∷ ChainSchema base inner → ChainSchema base inner → Bool # |
data CheckedHonestRecipe base hon Source #
The argument of uniformTheHonestChain
and the output of checkHonestRecipe
base
the type-level name of the top-level timelinehon
the type-level name of the honest chain's slot interval
TODO: Rename to CheckedHonestSchemaSpec
UnsafeCheckedHonestRecipe | |
|
Instances
Read (CheckedHonestRecipe base hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest readsPrec ∷ Int → ReadS (CheckedHonestRecipe base hon) # readList ∷ ReadS [CheckedHonestRecipe base hon] # readPrec ∷ ReadPrec (CheckedHonestRecipe base hon) # readListPrec ∷ ReadPrec [CheckedHonestRecipe base hon] # | |
Show (CheckedHonestRecipe base hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest showsPrec ∷ Int → CheckedHonestRecipe base hon → ShowS # show ∷ CheckedHonestRecipe base hon → String # showList ∷ [CheckedHonestRecipe base hon] → ShowS # | |
Eq (CheckedHonestRecipe base hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest (==) ∷ CheckedHonestRecipe base hon → CheckedHonestRecipe base hon → Bool # (/=) ∷ CheckedHonestRecipe base hon → CheckedHonestRecipe base hon → Bool # |
data HonestRecipe Source #
The argument of checkHonestRecipe'
HonestRecipe !Kcp !Scg !Delta !Len |
Instances
Read HonestRecipe Source # | |
Show HonestRecipe Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest showsPrec ∷ Int → HonestRecipe → ShowS # show ∷ HonestRecipe → String # showList ∷ [HonestRecipe] → ShowS # | |
Eq HonestRecipe Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest (==) ∷ HonestRecipe → HonestRecipe → Bool # (/=) ∷ HonestRecipe → HonestRecipe → Bool # |
data NoSuchHonestChainSchema Source #
BadKcp | Chosing |
BadLen |
|
data SomeCheckedHonestRecipe Source #
∀ base hon. SomeCheckedHonestRecipe !(Proxy base) !(Proxy hon) !(CheckedHonestRecipe base hon) |
Instances
data SomeHonestChainSchema Source #
∀ base hon. SomeHonestChainSchema !(Proxy base) !(Proxy hon) !(ChainSchema base hon) |
Instances
checkHonestRecipe ∷ HonestRecipe → Except NoSuchHonestChainSchema SomeCheckedHonestRecipe Source #
Checks whether the given HonestRecipe
determines a valid input to
uniformTheHonestChain
countChainSchema ∷ ChainSchema base inner → Size inner ActiveSlotE Source #
uniformTheHonestChain Source #
∷ ∀ base hon g. RandomGen g | |
⇒ Maybe Asc | When |
→ CheckedHonestRecipe base hon | |
→ g | |
→ ChainSchema base hon |
A ChainSchema
that satisfies checkHonestChain
This generator proceeds in three stages to create a random schema that
satisfies the requirement of at least k+1
blocks in every s
slots.
- It begins by drawing a sample of length
Len
from the Bernoulli process induced by the active slot coefficientAsc
, just like in Praos. (IELen
many i.i.d. samples fromUniform(asc)
). - It then visits the first window in that sampled vector. If it has less
than
k+1
active slots, the generator randomly toggles empty slots to be active until the window contains exactlyk+1
active slots. - It then visits the rest of the windows in oldest-to-youngest order. Each
window must contain at least
k
active slots when visited, since it shares all but its youngest slot with the previous window, which was already visited. In particular, when the window contains onlyk
active slots, that youngest slot must be empty, and so the generator will toggle it, thereby re-establishing the required density.
NOTE: This process may add more active slots to the initial sampled vector than strictly necessary---ensuring the minimum number of toggles would be an integer programming optimization problem as far as we can tell. We have settled for this relatively simple algorithm that approaches the minimal number of toggled slots (TODO calculate how tight the bounds are).
NOTE: When visting windows after the first, only the youngest slot can be
toggled. If we activated any other slot in the sliding window, then older
windows, which already have at least k+1
active slots, would unnecessarily
end up with even more active slots.
NOTE: The larger Asc
is, the more active slots there will be when sampling
from the Bernoulli process. When Asc
is much larger than (k+1)/s
the
sample will require toggling very few additional slots.
NOTE: When no Asc
value is provided, we start with a vector with no active
slots, and the second phase causes the first window to end up with k+1
active slots in a pattern that is then repeated exactly for the rest of the
chain. For instance,
k=2, s=6 000000000000000000000000 -- stage 1 1 11 -- stage 2 1 11 1 11 1 11 -- stage 3 101100101100101100101100 -- final
k=2, s=6 000000000000000000000000 -- stage 1 111 -- stage 2 111 111 111 -- stage 3 000111000111000111000111 -- final
NOTE: When
is close to 0, the sample will have a few active slots.
In the relatively common case where none of those initially active slots are
in the same window, the final schema will be periodic between the active
slots from the sample, but the patterns in those intervals may vary. For
instance,Asc
k=2, s=6 000000000000010000000000000000001000000000000000000 -- stage 1 1 1 1 -- stage 2 1 1 1 1 1 11 1 11 1 11 111 111 111 -- stage 3 101010101010110010110010110010111000111000111000111 -- final
TODO sample from a disjunction of generators that explore interesting boundary conditions. i.e. different windows could use different strategies to fill each of the windows. For instance, we could arrange for some windows to start with empty slots and be dense at the end.
Testing
data HonestChainViolation hon Source #
BadCount | The schema does not contain a positive number of active slots |
BadScgWindow !(ScgViolation hon) | The schema has some window of |
BadLength !(Size hon SlotE) | The schema does not span exactly |
Instances
Read (HonestChainViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest readsPrec ∷ Int → ReadS (HonestChainViolation hon) # readList ∷ ReadS [HonestChainViolation hon] # readPrec ∷ ReadPrec (HonestChainViolation hon) # readListPrec ∷ ReadPrec [HonestChainViolation hon] # | |
Show (HonestChainViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest showsPrec ∷ Int → HonestChainViolation hon → ShowS # show ∷ HonestChainViolation hon → String # showList ∷ [HonestChainViolation hon] → ShowS # | |
Eq (HonestChainViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest (==) ∷ HonestChainViolation hon → HonestChainViolation hon → Bool # (/=) ∷ HonestChainViolation hon → HonestChainViolation hon → Bool # |
data ScgViolation hon Source #
∀ skolem. ScgViolation | |
|
Instances
Read (ScgViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest readsPrec ∷ Int → ReadS (ScgViolation hon) # readList ∷ ReadS [ScgViolation hon] # readPrec ∷ ReadPrec (ScgViolation hon) # readListPrec ∷ ReadPrec [ScgViolation hon] # | |
Show (ScgViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest showsPrec ∷ Int → ScgViolation hon → ShowS # show ∷ ScgViolation hon → String # showList ∷ [ScgViolation hon] → ShowS # | |
Eq (ScgViolation hon) Source # | |
Defined in Test.Ouroboros.Consensus.ChainGenerator.Honest (==) ∷ ScgViolation hon → ScgViolation hon → Bool # (/=) ∷ ScgViolation hon → ScgViolation hon → Bool # |
checkHonestChain ∷ ∀ base hon. HonestRecipe → ChainSchema base hon → Except (HonestChainViolation hon) () Source #
Check the Extended Praos Chain Growth assumption
Definition of window and anchored window. A window is a contiguous sequence of slots. A window anchored at a block starts with the slot immediately after that block.
Definition of Extended Praos Chain Growth Assumption. We assume the honest chain
contains at least k+1
blocks in every window that contains s
slots.
Definition of Stability Window. The s
parameter from the Praos Chain
Growth property. (At the time of writing, this is 2k
during Byron and
3k/f
after Byron on Cardano mainnet
.)
prettyChainSchema ∷ ∀ base inner. ChainSchema base inner → String → [String] Source #