byron-spec-ledger-1.1.0.1: Executable specification of Cardano ledger
Safe HaskellNone
LanguageHaskell2010

Byron.Spec.Ledger.STS.UTXOW

Description

UTXO transition system with witnessing

Synopsis

Documentation

data UTXOW Source #

Instances

Instances details
Data UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

gfoldl ∷ (∀ d b. Data d ⇒ c (d → b) → d → c b) → (∀ g. g → c g) → UTXOW → c UTXOW #

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

toConstr ∷ UTXOW → Constr #

dataTypeOf ∷ UTXOW → DataType #

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

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

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

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

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

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

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

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

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

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

STS UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Associated Types

type State UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type State UTXOW = UTxOState
type Signal UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Signal UTXOW = Tx
type Environment UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Environment UTXOW = UTxOEnv
type BaseM UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type BaseM UTXOW = Identity
type Event UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Event UTXOW = Void
type PredicateFailure UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type PredicateFailure UTXOW = UtxowPredicateFailure

Methods

initialRules ∷ [InitialRule UTXOW] Source #

transitionRules ∷ [TransitionRule UTXOW] Source #

assertions ∷ [Assertion UTXOW] Source #

renderAssertionViolation ∷ AssertionViolation UTXOW → String Source #

HasTrace UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Associated Types

type BaseEnv UTXOW 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type BaseEnv UTXOW = ()

Methods

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

envGen ∷ Word64 → Gen (Environment UTXOW) Source #

sigGen ∷ SignalGenerator UTXOW Source #

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

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

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

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

Embed UTXO UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

wrapFailed ∷ PredicateFailure UTXO → PredicateFailure UTXOW Source #

wrapEvent ∷ Event UTXO → Event UTXOW Source #

Embed UTXOW UTXOWS Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOWS

Methods

wrapFailed ∷ PredicateFailure UTXOW → PredicateFailure UTXOWS Source #

wrapEvent ∷ Event UTXOW → Event UTXOWS Source #

type BaseM UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type BaseM UTXOW = Identity
type Environment UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Environment UTXOW = UTxOEnv
type Event UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Event UTXOW = Void
type PredicateFailure UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type PredicateFailure UTXOW = UtxowPredicateFailure
type Signal UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Signal UTXOW = Tx
type State UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type State UTXOW = UTxOState
type BaseEnv UTXOW Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type BaseEnv UTXOW = ()

data UtxowPredicateFailure Source #

These PredicateFailures are all throwable.

Constructors

UtxoFailure (PredicateFailure UTXO) 
InsufficientWitnesses 

Instances

Instances details
Data UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

gfoldl ∷ (∀ d b. Data d ⇒ c (d → b) → d → c b) → (∀ g. g → c g) → UtxowPredicateFailure → c UtxowPredicateFailure #

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

toConstr ∷ UtxowPredicateFailure → Constr #

dataTypeOf ∷ UtxowPredicateFailure → DataType #

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

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

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

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

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

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

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

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

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

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

Generic UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Associated Types

type Rep UtxowPredicateFailure 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Rep UtxowPredicateFailure = D1 ('MetaData "UtxowPredicateFailure" "Byron.Spec.Ledger.STS.UTXOW" "byron-spec-ledger-1.1.0.1-inplace" 'False) (C1 ('MetaCons "UtxoFailure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (PredicateFailure UTXO))) :+: C1 ('MetaCons "InsufficientWitnesses" 'PrefixI 'False) (U1 ∷ Type → Type))

Methods

from ∷ UtxowPredicateFailure → Rep UtxowPredicateFailure x #

to ∷ Rep UtxowPredicateFailure x → UtxowPredicateFailure #

Show UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

showsPrec ∷ Int → UtxowPredicateFailure → ShowS #

show ∷ UtxowPredicateFailure → String #

showList ∷ [UtxowPredicateFailure] → ShowS #

Eq UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

(==) ∷ UtxowPredicateFailure → UtxowPredicateFailure → Bool #

(/=) ∷ UtxowPredicateFailure → UtxowPredicateFailure → Bool #

NoThunks UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

Methods

noThunks ∷ Context → UtxowPredicateFailure → IO (Maybe ThunkInfo) Source #

wNoThunks ∷ Context → UtxowPredicateFailure → IO (Maybe ThunkInfo) Source #

showTypeOf ∷ Proxy UtxowPredicateFailure → String Source #

type Rep UtxowPredicateFailure Source # 
Instance details

Defined in Byron.Spec.Ledger.STS.UTXOW

type Rep UtxowPredicateFailure = D1 ('MetaData "UtxowPredicateFailure" "Byron.Spec.Ledger.STS.UTXOW" "byron-spec-ledger-1.1.0.1-inplace" 'False) (C1 ('MetaCons "UtxoFailure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (PredicateFailure UTXO))) :+: C1 ('MetaCons "InsufficientWitnesses" 'PrefixI 'False) (U1 ∷ Type → Type))

authTxin ∷ VKey → TxIn → UTxO → Bool Source #

Determine if a UTxO input is authorized by a given key.

witnessed ∷ Tx → UTxO → Bool Source #

Given a ledger state, determine if the UTxO witnesses in a given transaction are sufficient. TODO - should we only check for one witness for each unique input address?

traceAddrs ∷ [Addr] Source #

Constant list of addresses intended to be used in the generators.

coverUtxoFailure Source #

Arguments

∷ (MonadTest m, HasCallStack, Data a) 
⇒ CoverPercentage

Minimum percentage that each failure must occur.

→ a

Structure containing the failures

→ m () 

Check that all the relevant predicate failures are covered.