| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Hydra.Chain.Direct.TxTraceSpec
Description
Stateful model-based testing of the transactions created by the Direct chain modules.
The model is focusing on transitions between Open and Closed states of the head right now. It generates plausible sequences of Decrement and Close actions, along with Contest and Fanout, each using a snapshot of some version and number. UTxOs are simplified such that their identity is A-E and value is just a number.
Actions and snapshots are generated "just-in-time" and result in valid, but also deliberately invalid combinations of versions/numbers. Generated snapshots are correctly signed and consistent in what they decommit from the head.
Synopsis
- spec :: Spec
- prop_traces :: Property
- prop_runActions :: Actions Model -> Property
- data SingleUTxO
- type ModelUTxO = Map SingleUTxO Natural
- data Model = Model {
- headState :: State
- currentVersion :: SnapshotVersion
- latestSnapshot :: SnapshotNumber
- alreadyContested :: [Actor]
- utxoInHead :: ModelUTxO
- pendingDecommitUTxO :: ModelUTxO
- data ModelSnapshot = ModelSnapshot {
- version :: SnapshotVersion
- number :: SnapshotNumber
- snapshotUTxO :: ModelUTxO
- decommitUTxO :: ModelUTxO
- data State
- data Actor
- data TxResult = TxResult {
- constructedTx :: Either String Tx
- spendableUTxO :: UTxO
- validationError :: Maybe String
- observation :: HeadObservation
- initialAmount :: Natural
- initialModelUTxO :: ModelUTxO
- balanceUTxOInHead :: Ord k => Map k Natural -> Map k Natural -> Map k Natural
- newtype AppM a = AppM {}
- performTx :: Show err => Either err Tx -> AppM TxResult
- getValidationError :: Tx -> UTxO -> Maybe String
- allActors :: [Actor]
- generateUTxOFromModelSnapshot :: ModelSnapshot -> (UTxO, UTxO)
- realWorldModelUTxO :: ModelUTxO -> UTxO
- signedSnapshot :: ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx))
- confirmedSnapshot :: ModelSnapshot -> ConfirmedSnapshot Tx
- openHeadUTxO :: UTxO
- newDecrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx)
- newCloseTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either CloseTxError Tx)
- newContestTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either ContestTxError Tx)
- newFanoutTx :: Actor -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx)
- alicePVk :: VerificationKey PaymentKey
- bobPVk :: VerificationKey PaymentKey
- carolPVk :: VerificationKey PaymentKey
- actorChainContext :: Actor -> ChainContext
- testScriptRegistry :: ScriptRegistry
- runPostconditionM' :: Monad m => PostconditionM' m () -> PostconditionM m Bool
- newtype PostconditionM' m a = PostconditionM' (ExceptT (Maybe String) (PostconditionM m) a)
- fulfilled :: Monad m => PostconditionM' m ()
- counterexample' :: Monad m => String -> PostconditionM' m ()
- expectValid :: Monad m => TxResult -> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a
- expectInvalid :: Monad m => TxResult -> PostconditionM' m ()
- orSometimes :: a -> Gen a -> Gen a
Documentation
prop_traces :: Property Source #
prop_runActions :: Actions Model -> Property Source #
============================== MODEL WORLD ==========================
data SingleUTxO Source #
Instances
Constructors
| Model | |
Fields
| |
Instances
| Show Model Source # | |
| StateModel Model Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec Methods actionName :: Action Model a -> String arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model)) shrinkAction :: Typeable a => VarContext -> Model -> Action Model a -> [Any (Action Model)] nextState :: Typeable a => Model -> Action Model a -> Var a -> Model failureNextState :: Typeable a => Model -> Action Model a -> Model precondition :: Model -> Action Model a -> Bool validFailingAction :: Model -> Action Model a -> Bool | |
| HasVariables Model Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec Methods getAllVariables :: Model -> Set (Any Var) | |
| RunModel Model AppM Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec Methods perform :: Typeable a => Model -> Action Model a -> LookUp AppM -> AppM (PerformResult (Error Model) (Realized AppM a)) postcondition :: (Model, Model) -> Action Model a -> LookUp AppM -> Realized AppM a -> PostconditionM AppM Bool postconditionOnFailure :: (Model, Model) -> Action Model a -> LookUp AppM -> Either (Error Model) (Realized AppM a) -> PostconditionM AppM Bool monitoring :: (Model, Model) -> Action Model a -> LookUp AppM -> Either (Error Model) (Realized AppM a) -> Property -> Property monitoringFailure :: Model -> Action Model a -> LookUp AppM -> Error Model -> Property -> Property | |
| Show (Action Model a) Source # | |
| Eq (Action Model a) Source # | |
| HasVariables (Action Model a) Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec Methods getAllVariables :: Action Model a -> Set (Any Var) | |
| data Action Model a Source # | |
| type Error Model Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec | |
data ModelSnapshot Source #
Model of a real snapshot which contains a SnapshotNumber but also our
simplified form of UTxO.
Constructors
| ModelSnapshot | |
Fields
| |
Instances
Result of constructing and performing a transaction. Notably there are three stages to this which can fail: construction, validation, and observation. Results from all stages are needed to express post-conditions.
Constructors
| TxResult | |
Fields
| |
============================== REAL WORLD ==========================
Application monad to perform model actions. Currently it only keeps a
UTxO which is updated whenever transactions are valid in performTx.
Instances
| MonadFail AppM Source # | |
| MonadIO AppM Source # | |
| Applicative AppM Source # | |
| Functor AppM Source # | |
| Monad AppM Source # | |
| MonadThrow AppM Source # | |
| MonadReader UTxO AppM Source # | |
| MonadState UTxO AppM Source # | |
| RunModel Model AppM Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec Methods perform :: Typeable a => Model -> Action Model a -> LookUp AppM -> AppM (PerformResult (Error Model) (Realized AppM a)) postcondition :: (Model, Model) -> Action Model a -> LookUp AppM -> Realized AppM a -> PostconditionM AppM Bool postconditionOnFailure :: (Model, Model) -> Action Model a -> LookUp AppM -> Either (Error Model) (Realized AppM a) -> PostconditionM AppM Bool monitoring :: (Model, Model) -> Action Model a -> LookUp AppM -> Either (Error Model) (Realized AppM a) -> Property -> Property monitoringFailure :: Model -> Action Model a -> LookUp AppM -> Error Model -> Property -> Property | |
| type Realized AppM a Source # | |
Defined in Hydra.Chain.Direct.TxTraceSpec type Realized AppM a = a | |
getValidationError :: Tx -> UTxO -> Maybe String Source #
Fixtures and glue code
generateUTxOFromModelSnapshot :: ModelSnapshot -> (UTxO, UTxO) Source #
A "random" UTxO distribution for a given ModelSnapshot.
realWorldModelUTxO :: ModelUTxO -> UTxO Source #
Map a ModelUTxO to a real-world UTxO.
signedSnapshot :: ModelSnapshot -> (Snapshot Tx, MultiSignature (Snapshot Tx)) Source #
A correctly signed snapshot. Given a snapshot number a snapshot signed by all participants (alice, bob and carol) with some UTxO contained is produced.
confirmedSnapshot :: ModelSnapshot -> ConfirmedSnapshot Tx Source #
A confirmed snapshot (either initial or later confirmed), based onTxTra
signedSnapshot.
openHeadUTxO :: UTxO Source #
UTxO of the open head on-chain. NOTE: This uses fixtures for headId, parties, and cperiod.
newDecrementTx :: Actor -> ConfirmedSnapshot Tx -> AppM (Either DecrementTxError Tx) Source #
Creates a decrement transaction using given utxo and given snapshot.
newCloseTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either CloseTxError Tx) Source #
Creates a transaction that closes openHeadUTxO with given the snapshot.
NOTE: This uses fixtures for headId, parties (alice, bob, carol),
contestation period and also claims to close at time 0 resulting in a
contestation deadline of 0 + cperiod.
newContestTx :: Actor -> SnapshotVersion -> ConfirmedSnapshot Tx -> AppM (Either ContestTxError Tx) Source #
Creates a contest transaction using given utxo and contesting with given snapshot. NOTE: This uses fixtures for headId, contestation period and also claims to contest at time 0.
newFanoutTx :: Actor -> ModelUTxO -> ModelUTxO -> AppM (Either FanoutTxError Tx) Source #
Creates a fanout transaction using given utxo. NOTE: This uses fixtures for seedTxIn and contestation period. Consequently, the lower bound used is precisely at the maximum deadline slot as if everyone contested.
actorChainContext :: Actor -> ChainContext Source #
Fixture for the chain context of a model Actor on testNetworkId. Uses a generated ScriptRegistry.
testScriptRegistry :: ScriptRegistry Source #
Helpers
runPostconditionM' :: Monad m => PostconditionM' m () -> PostconditionM m Bool Source #
newtype PostconditionM' m a Source #
Constructors
| PostconditionM' (ExceptT (Maybe String) (PostconditionM m) a) |
Instances
fulfilled :: Monad m => PostconditionM' m () Source #
Short-cut a postcondition monad like fail, but in a successful way. This
is useful to not have unrelated counterexample' outputs.
counterexample' :: Monad m => String -> PostconditionM' m () Source #
Add given message in case the postcondition fails.
expectValid :: Monad m => TxResult -> (HeadObservation -> PostconditionM' m a) -> PostconditionM' m a Source #
Assertion helper to check whether a TxResult was valid and the expected
HeadObservation could be made. To be used in postcondition.
expectInvalid :: Monad m => TxResult -> PostconditionM' m () Source #
Assertion helper to check whether a TxResult was invalid.
orSometimes :: a -> Gen a -> Gen a Source #
Generate sometimes a value with given generator, bur more often just use the given value.