byron-spec-chain-1.0.1.0: Executable specification of the Cardano blockchain
Safe HaskellSafe-Inferred
LanguageHaskell2010

Byron.Spec.Chain.STS.Rule.Chain

Synopsis

Documentation

data CHAIN Source #

Instances

Instances details
Data CHAIN 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) → CHAIN → c CHAIN #

gunfold ∷ (∀ b r. Data b ⇒ c (b → r) → c r) → (∀ r. r → c r) → Constr → c CHAIN #

toConstr ∷ CHAIN → Constr #

dataTypeOf ∷ CHAIN → DataType #

dataCast1 ∷ Typeable t ⇒ (∀ d. Data d ⇒ c (t d)) → Maybe (c CHAIN) #

dataCast2 ∷ Typeable t ⇒ (∀ d e. (Data d, Data e) ⇒ c (t d e)) → Maybe (c CHAIN) #

gmapT ∷ (∀ b. Data b ⇒ b → b) → CHAIN → CHAIN #

gmapQl ∷ (r → r' → r) → r → (∀ d. Data d ⇒ d → r') → CHAIN → r #

gmapQr ∷ ∀ r r'. (r' → r → r) → r → (∀ d. Data d ⇒ d → r') → CHAIN → r #

gmapQ ∷ (∀ d. Data d ⇒ d → u) → CHAIN → [u] #

gmapQi ∷ Int → (∀ d. Data d ⇒ d → u) → CHAIN → u #

gmapM ∷ Monad m ⇒ (∀ d. Data d ⇒ d → m d) → CHAIN → m CHAIN #

gmapMp ∷ MonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → CHAIN → m CHAIN #

gmapMo ∷ MonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → CHAIN → m CHAIN #

STS CHAIN Source # 
Instance details

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

Associated Types

type State CHAIN Source #

type Signal CHAIN Source #

type Environment CHAIN Source #

type BaseM CHAIN ∷ Type → Type Source #

type Event CHAIN Source #

type PredicateFailure CHAIN Source #

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 Source #

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 #

Constructors

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

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

∷ ∀ m a. (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 #