The type of transaction modifiers. When combined using the monoid instance, individual modifications are applied in left-to-right order.

A transaction input reference togheter with the corresponding TxOut from the UTxO set.

A transaction output paired with its index in the transaction.

Type synonym for datums. The CtxTx context means that the actual datum value can be present, not just the hash.

Redeemers are plain ScriptData.

Functions common to both Inputs and Outputs.

Add a new output of any type (public key or script)

Remove an output of any type.

Add a new public key input.

Add a plutus V2 script input.

Add a simple script input.

Add a reference script input

Add a new public key reference input.

Add a plutus script reference input.

Add a simple script reference input.

Remove an input of any type.

Change the redeemer of a script input.

Change the validity range of the transaction.

Change the validity lower bound of the transaction.

Change the validity upper bound of the transaction.

The most general transaction modifier. Simply replace the original transaction and UTxO set by the given values. In most cases the modifiers above should be sufficient.

The threat model monad is how you construct threat models. It works in the context of a given transaction and the UTxO set at the point where the transaction was validated (see ThreatModelEnv) and lets you construct properties about the validatity of modifications of the original transaction.

The context in which a ThreatModel is executed: a transaction and the chain state it validated against. See getThreatModelEnv and originalTx to access this information in a threat model; the UTxO set and protocol parameters are derived from the chain state via currentUTxOs and pparams.

Construct a ThreatModelEnv from a transaction and the chain state it validated against (captured *before* the transaction was submitted - a state captured afterwards no longer resolves the transaction's inputs).

The protocol parameters, derived from currentChainState.

Structured outcome of running a threat model against a transaction.

Create ThreatModelEnvs by reapplying the given transactions in order, starting with the given chain state.

Run threat model inside MockchainT with full Phase 1 + Phase 2 validation.

Unlike runThreatModel which only validates Phase 2 (script execution), this version uses re-balancing and re-signing for modified transactions, then performs full Phase 1 + Phase 2 validation via applyTransaction.

This catches vulnerabilities that would be masked by signature/fee failures in the simpler Phase 2-only validation.

The wallet parameter controls signing: - SignWith wallet - use the specified wallet for signing - AutoSign - detect the signing wallet from the transaction's witnesses

Usage: result <- runMockchain0IOWith utxos params $ do -- ... run your actions to get a transaction ... runThreatModelM (SignWith Wallet.w1) unprotectedScriptOutput [env] -- or auto-detect: runThreatModelM AutoSign unprotectedScriptOutput [env]

Like runThreatModelM but suppresses verbose counterexample annotations.

This is useful for expectFailure tests where you want the test to fail (proving vulnerability exists) but don't want the lengthy counterexample output cluttering test results.

The property still succeedsfails correctly based on shouldValidateshouldNotValidate checks, but Monitor/MonitorLocal annotations (counterexampleTM, etc.) are ignored.

The wallet parameter controls signing (see runThreatModelM for details).

Run a threat model and return a structured outcome instead of a Property. Coverage is still accumulated in MockChainState as a side effect.

Rebalancing failures (e.g., "No change output found") are treated as skipped because they indicate the transaction modification cannot be applied to this particular transaction, similar to a precondition failure.

The wallet parameter controls signing: - SignWith wallet - use the specified wallet for signing - AutoSign - detect the signing wallet from the transaction's witnesses

Like runThreatModelCheck but additionally accumulates trace data. Each Validate call in the threat model produces a ThreatModelCheckEntry. Coverage is still accumulated in MockChainState as a side effect.

A single trace entry from a threat model check against one ThreatModelEnv.

The outcome of a whole model run, most informative first: a pass beats everything else, an environmental skip at least proves the precondition held, and an error only speaks when nothing else happened. Mirrors zeroCoverageKind, which ranks the same three when deciding whether zero coverage should fail a test case - so TMError there can be trusted to mean "no attack was ever carried out".

Evaluate a ThreatModel on a list of transactions, each paired with the chain state it validated against.

Extract the name from a threat model, if it was defined with Named.

Check a precondition. If the argument threat model fails, the evaluation of the current transaction is skipped. If all transactions in an evaluation of runThreatModel are skipped it is considered a discarded test for QuickCheck.

Having the argument to threatPrecondition be a threat model computation instead of a plain boolean allows you do express preconditions talking about the validation of modified transactions (using shouldValidate and shouldNotValidate). See ensure for the boolean version.

Returns True if evaluated under a threatPrecondition and False otherwise.

Same as threatPrecondition but takes a boolean and skips the test if the argument is False.

Precondition that check that the original transaction has an input at a given address. Useful, for example, to ensure that you only consider transactions that trie to spend a script output from the script under test.

Precondition that requires the original transaction to run at least one Plutus script, of any purpose: a spending validator, a minting policy, a withdraw-zero staking validator, ... Attacks that mutate a script output and then check whether the transaction still validates need this: on a transaction that runs no script at all (e.g. a setup transaction that just pays a key input into a script for the first time), no validator ever gets a chance to reject the mutation, so "the mutated transaction still validates" is vacuous and proves nothing about the contract under test.

The check is based on the transaction's redeemer set, not on its input addresses, because the script that guards a contract's outputs is not always a spending validator - the withdraw-zero pattern, for instance, validates the whole transaction from a Rewarding script while every input is key-owned. Conversely, an input at a native-script address runs no Plutus code and does not count.

Not every attack needs this - one that tests a minting policy in isolation (e.g. Convex.ThreatModel.TokenForgery) is still meaningful on a transaction that spends no script - so this is opt-in per attack rather than applied globally to every ThreatModelEnv.

The transaction's outputs whose payment credential is the hash of a Plutus script that runs in this transaction.

Stronger than requireScriptExecution, and what the output-mutation attacks actually want: degrading an output is only evidence against a contract if a script plausibly responsible for it was executing and failed to object. Under the transaction-wide check, a transaction whose only script is an unrelated minting policy, paying into a validator for the first time, let those attacks degrade the new output and report a finding.

Hash identity is a proxy, not proof, and it cuts both ways. A script running under any purpose counts, so the withdraw-zero pattern's Rewarding script guards outputs at its own payment address - which is the point, and restricting this to Spending purposes would break that pattern, as there are no script inputs there at all. By the same token a multi-validator whose minting policy id equals its spending hash counts as guarding its own outputs. Conversely an output policed by some other running script is not matched and those attacks skip it, which is a known and accepted gap.

Empty when no Plutus script runs at all, which is what lets anyGuardedOutputSuchThat subsume requireScriptExecution.

Pick any output that guardedScriptOutputs admits.

Pick any output that guardedScriptOutputs admits and that satisfies the predicate, recording a precondition miss when there is none.

The output-mutation attacks all want exactly this, so the emptiness convention lives here rather than being restated at each call site. Since guardedScriptOutputs is empty whenever no Plutus script runs, this subsumes requireScriptExecution and no separate call is needed. Attacks that corrupt a redeemer of any running script (e.g. Convex.ThreatModel.InvalidScriptPurpose, which targets a key output) still want the weaker, transaction-wide check.

Pick any output that guardedScriptOutputs admits and that carries an inline datum, returning the output together with that datum.

Every datum-mutating attack starts here, so the predicate and the extraction are one operation: splitting them left each call site with a Nothing branch the predicate had already ruled out.

Does this output carry an inline datum?

The output's inline datum, if it has one.

Wrap a ScriptData as an inline datum, for use with changeDatumOf.

Check that a given modification of the original transaction validates. The modified transaction is printed in counterexample when this fails, or if it succeeds in a precondition and the test fails later.

Check that a given modification of the original transaction does not validate. The modified transaction is printed in counterexample when it does validate, or if it doesn't in a satisfied precondition and the test fails later.

The result of validating a transaction. In case of failure, it includes a list of reasons.

The outcome of validating a transaction, mirroring the ledger's two-phase validation: Phase 2 (script execution) only runs when Phase 1 (structural ledger rules) passes, so no other combinations exist.

The most low-level way to validate a modified transaction. In most cases shouldValidate and shouldNotValidate are preferred.

Get the current context.

Get the original transaction from the context.

Get the inputs from the original transaction.

Get the reference inputs from the original transaction.

Get the outputs from the original transaction.

Get the redeemer (if any) for an input of the original transaction.

Get the required signers from the original transaction body.

Generate a random value. Takes a QuickCheck generator and a shrink function.

Shrink towards 1, never below it: the counts these attacks generate are sizes, and a size of zero is not a smaller failing case but a different (no-op) one.

Pick a random value from a list. Skips the test if the list is empty.

Pick a random signer of the original transaction.

Pick a random input

Pick a random reference input

Pick a random output

Pick a random input satisfying the given predicate.

Pick a random reference input satisfying the given predicate.

Pick a random output satisfying the given predicate.

Print the given string in case this threat model fails. Threat model counterpart of the QuickCheck counterexample function.

Threat model counterpart of QuickCheck's tabulate function.

Threat model counterpart of QuickCheck's collect function.

Threat model counterpart of QuickCheck's classify function.

Monitoring that's shared between all transactions evaluated. Avoid this in favour of tabulateTM, collectTM and classifyTM when possible.

Monitoring that's local to the current transaction. Use counterexampleTM when possible.

How to determine the wallet for re-balancing and re-signing modified transactions.

Keep only the Ada part of a value.

Check if a value is less or equal than another value.

Construct a public key address.

Construct a script address.

Check if an address is a public key address — i.e. has no script payment credential. Byron addresses count as key addresses, as they have no script credentials at all.

Convert ScriptData to a Datum.

Convert a Haskell value to ScriptData for use as a Redeemer or convert to a Datum with txOutDatum.

Get the datum from a transaction output.

Format a list of strings as a paragraph. The structure of the list is not considered other than inserting whitespace between consecutive elements. Use with counterexampleTM when printing longer texts.