Safe Haskell	Safe-Inferred
Language	Haskell2010

Byron.Spec.Ledger.STS.UTXOW

Description

UTXO transition system with witnessing

Synopsis

data UTXOW
data UtxowPredicateFailure
- = UtxoFailure (PredicateFailure UTXO)
- | InsufficientWitnesses
authTxin ∷ VKey → TxIn → UTxO → Bool
witnessed ∷ Tx → UTxO → Bool
traceAddrs ∷ [Addr]
coverUtxoFailure ∷ ∀ m a. (MonadTest m, HasCallStack, Data a) ⇒ CoverPercentage → a → m ()

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 Source # type Signal UTXOW Source # type Environment UTXOW Source # type BaseM UTXOW ∷ Type → Type Source # type Event UTXOW Source # type PredicateFailure UTXOW Source # 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 Source # 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 ∷ 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

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