| 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.
Given an initial UTxO, the model generates a plausible sequence of snapshots that an honest node would approve. That is, the total balance of UTxO remains constant and utxoToDecommit is only allowed to clear if the version is incremented. Consequently, also all snapshots are correctly signed (we don't test handling of adverarial signatures). UTxOs are simplified such that they are A-E items, where each maps to an arbitrary real UTxO.
From this sequence of valid snapshots, possible Decrement and Close actions are generated, along with occasional Contest and consequential Fanout.
Synopsis
- spec :: Spec
- coversInterestingActions :: Testable p => Actions Model -> p -> Property
- prop_runActions :: Actions Model -> Property
- data SingleUTxO
- type ModelUTxO = [SingleUTxO]
- data Model = Model {
- headState :: State
- knownSnapshots :: [ModelSnapshot]
- currentVersion :: SnapshotVersion
- closedSnapshotNumber :: SnapshotNumber
- alreadyContested :: [Actor]
- utxoInHead :: ModelUTxO
- pendingDecommit :: ModelUTxO
- latestSnapshotNumber :: [ModelSnapshot] -> SnapshotNumber
- latestSnapshot :: [ModelSnapshot] -> Maybe ModelSnapshot
- data ModelSnapshot = ModelSnapshot {}
- data State
- data Actor
- data TxResult = TxResult {
- constructedTx :: Either String Tx
- spendableUTxO :: UTxO
- validationError :: Maybe String
- observation :: HeadObservation
- newtype AppM a = AppM {}
- performTx :: Show err => Either err Tx -> AppM TxResult
- getValidationError :: Tx -> UTxO -> Maybe String
- allActors :: [Actor]
- 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
coversInterestingActions :: Testable p => Actions Model -> p -> Property Source #
prop_runActions :: Actions Model -> Property Source #
============================== MODEL WORLD ==========================
data SingleUTxO Source #
Instances
type ModelUTxO = [SingleUTxO] Source #
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 | |
latestSnapshotNumber :: [ModelSnapshot] -> SnapshotNumber Source #
latestSnapshot :: [ModelSnapshot] -> Maybe ModelSnapshot Source #
data ModelSnapshot Source #
Model of a real snapshot which contains a SnapshotNumber but also our
simplified form of UTxO.
Constructors
| ModelSnapshot | |
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
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 or construction failed.
orSometimes :: a -> Gen a -> Gen a Source #
Generate sometimes a value with given generator, but more often just use the given value.