type State CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type State CHAIN = (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
type Signal CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type Signal CHAIN = Block
type Environment CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type Environment CHAIN = (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
type BaseM CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type BaseM CHAIN = Identity
type Event CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type Event CHAIN = Void
type PredicateFailure CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type PredicateFailure CHAIN = ChainPredicateFailure

Methods

initialRules ∷ [InitialRule CHAIN] Source #

transitionRules ∷ [TransitionRule CHAIN] Source #

assertions ∷ [Assertion CHAIN] Source #

renderAssertionViolation ∷ AssertionViolation CHAIN → String Source #

HasTrace CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Associated Types

type BaseEnv CHAIN
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain type BaseEnv CHAIN = ()

Methods

interpretSTS ∷ BaseEnv CHAIN → BaseM CHAIN a → a Source #

envGen ∷ Word64 → Gen (Environment CHAIN) Source #

sigGen ∷ SignalGenerator CHAIN Source #

trace ∷ BaseEnv CHAIN → Word64 → Gen (Trace CHAIN) Source #

traceWithProfile ∷ BaseEnv CHAIN → Word64 → TraceProfile CHAIN → Gen (Trace CHAIN) Source #

traceOfLength ∷ BaseEnv CHAIN → Word64 → Gen (Trace CHAIN) Source #

traceOfLengthWithInitState ∷ BaseEnv CHAIN → Word64 → (Environment CHAIN → Gen (State CHAIN)) → Gen (Trace CHAIN) Source #

Embed BBODY CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Methods

wrapFailed ∷ PredicateFailure BBODY → PredicateFailure CHAIN Source #

wrapEvent ∷ Event BBODY → Event CHAIN Source #

Embed EPOCH CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Methods

wrapFailed ∷ PredicateFailure EPOCH → PredicateFailure CHAIN Source #

wrapEvent ∷ Event EPOCH → Event CHAIN Source #

Embed PBFT CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Methods

wrapFailed ∷ PredicateFailure PBFT → PredicateFailure CHAIN Source #

wrapEvent ∷ Event PBFT → Event CHAIN Source #

Embed DELEG CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Methods

wrapFailed ∷ PredicateFailure DELEG → PredicateFailure CHAIN Source #

wrapEvent ∷ Event DELEG → Event CHAIN Source #

Embed UTXOWS CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

Methods

wrapFailed ∷ PredicateFailure UTXOWS → PredicateFailure CHAIN Source #

wrapEvent ∷ Event UTXOWS → Event CHAIN Source #

type BaseM CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type BaseM CHAIN = Identity

type Environment CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type Environment CHAIN = (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)

type Event CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type Event CHAIN = Void

type PredicateFailure CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type PredicateFailure CHAIN = ChainPredicateFailure

type Signal CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type Signal CHAIN = Block

type State CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type State CHAIN = (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)

type BaseEnv CHAIN Source #

Instance details

Defined in Byron.Spec.Chain.STS.Rule.Chain

type BaseEnv CHAIN = ()

data ChainPredicateFailure Source #

Instances

Instances details

Data ChainPredicateFailure Source #
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain Methods gfoldl ∷ (∀ d b. Data d ⇒ c (d → b) → d → c b) → (∀ g. g → c g) → ChainPredicateFailure → c ChainPredicateFailure # gunfold ∷ (∀ b r. Data b ⇒ c (b → r) → c r) → (∀ r. r → c r) → Constr → c ChainPredicateFailure # toConstr ∷ ChainPredicateFailure → Constr # dataTypeOf ∷ ChainPredicateFailure → DataType # dataCast1 ∷ Typeable t ⇒ (∀ d. Data d ⇒ c (t d)) → Maybe (c ChainPredicateFailure) # dataCast2 ∷ Typeable t ⇒ (∀ d e. (Data d, Data e) ⇒ c (t d e)) → Maybe (c ChainPredicateFailure) # gmapT ∷ (∀ b. Data b ⇒ b → b) → ChainPredicateFailure → ChainPredicateFailure # gmapQl ∷ (r → r' → r) → r → (∀ d. Data d ⇒ d → r') → ChainPredicateFailure → r # gmapQr ∷ ∀ r r'. (r' → r → r) → r → (∀ d. Data d ⇒ d → r') → ChainPredicateFailure → r # gmapQ ∷ (∀ d. Data d ⇒ d → u) → ChainPredicateFailure → [u] # gmapQi ∷ Int → (∀ d. Data d ⇒ d → u) → ChainPredicateFailure → u # gmapM ∷ Monad m ⇒ (∀ d. Data d ⇒ d → m d) → ChainPredicateFailure → m ChainPredicateFailure # gmapMp ∷ MonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → ChainPredicateFailure → m ChainPredicateFailure # gmapMo ∷ MonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → ChainPredicateFailure → m ChainPredicateFailure #
Show ChainPredicateFailure Source #
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain Methods showsPrec ∷ Int → ChainPredicateFailure → ShowS # show ∷ ChainPredicateFailure → String # showList ∷ [ChainPredicateFailure] → ShowS #
Eq ChainPredicateFailure Source #
Instance details Defined in Byron.Spec.Chain.STS.Rule.Chain Methods (==) ∷ ChainPredicateFailure → ChainPredicateFailure → Bool # (/=) ∷ ChainPredicateFailure → ChainPredicateFailure → Bool #

isHeaderSizeTooBigFailure ∷ PredicateFailure CHAIN → Bool Source #

headerIsValid ∷ UPIState → BlockHeader → Rule CHAIN 'Transition () Source #

disL ∷ Lens' (State CHAIN) DIState Source #

Lens for the delegation interface state contained in the chain state.

data ShouldGenDelegation Source #

Constructors

GenDelegation
NoGenDelegation

data ShouldGenUTxO Source #

Constructors

GenUTxO
NoGenUTxO

data ShouldGenUpdate Source #

Constructors

GenUpdate
NoGenUpdate

sigGenChain ∷ ShouldGenDelegation → ShouldGenUTxO → ShouldGenUpdate → Environment CHAIN → State CHAIN → Gen (Signal CHAIN) Source #

coverInvalidBlockProofs Source #

Arguments

∷ (MonadTest m, HasCallStack, Data a)
⇒ CoverPercentage	Minimum percentage that each failure must occur.
→ a	Structure containing the failures
→ m ()

Orphan instances

Field1 (a, b, c, d, e, f) (a', b, c, d, e, f) a a' Source #
Instance details Methods _1 ∷ Lens (a, b, c, d, e, f) (a', b, c, d, e, f) a a' Source #
Field5 (a, b, c, d, e, f) (a, b, c, d, e', f) e e' Source #
Instance details Methods _5 ∷ Lens (a, b, c, d, e, f) (a, b, c, d, e', f) e e' Source #

EpochFailure (PredicateFailure EPOCH)
HeaderSizeTooBig BlockHeader Natural (Threshold Natural)
BBodyFailure (PredicateFailure BBODY)
PBFTFailure (PredicateFailure PBFT)
MaximumBlockSize Natural Natural
LedgerDelegationFailure (PredicateFailure DELEG)
LedgerUTxOFailure (PredicateFailure UTXOWS)