Like propDL for scripted scenarios where only the keys are random. Shrinking is off: it cannot simplify a fixed script, it only reruns it hundreds of times with varied values (a failing run takes ~0.3s, a shrunk one took minutes).

Open a head of n parties, each owning one UTxO that can be deposited, and return the head id variable together with each party's deposit fuel.

Funds only enter the head through deposits (it opens empty), so every scenario starts from here. The Wait leaves room for deep forks that must stay clear of the head-opening transactions.

The fuel of a two-party head, see openHeadWithDepositFuel.

The fuel of a three-party head, see openHeadWithDepositFuel.

Payment decommitting a party's deposited fuel back to itself.

The head must still settle after the fork: confirm an L2 transaction, close and fan out the whole confirmed UTxO (checked by the Fanout postcondition). A head wedged on an erased settlement fails here, either because the close cannot land (its snapshot is ahead of the on-chain version) or because the fanout does not match.

Scenario 1: two deposits settle back to back, then a fork erases both increments for good (no mempool re-inclusion). Both must be re-posted.

Scenario 2: deposit B's transaction is on chain before A's increment lands. Right after A settles, B's snapshot is approved and its increment is in flight; a shallow fork then erases A's increment but keeps B's deposit. Timing dependent by nature; the random walk covers the rest of this space.

Scenario 3: two decommits settle back to back (a second decommit is only accepted once the first is finalized), then a fork erases both decrements.

Scenario 4: an increment and then a decrement settle in consecutive versions; a fork erases both. The decrement can only re-land after the increment did.

While erased settlements are being re-posted, L2 keeps going: a new decommit and a new deposit are requested right after the fork. Their snapshots are signed at the local version, ahead of the chain, so their settlements must queue behind the replayed ones and land in version order.

Scenario 5: a deep fork erases the deposit transaction itself along with its increment; the mempool re-includes the deposit, so the increment must be re-posted once the deposit is observed again.

Open a single-party head holding n outputs of 1 ADA, each owned by a different key, and close it. More than fanoutOutputThreshold outputs do not fit one fanout transaction, so the fanout takes several steps; how many outputs each step carries is decided by the node from the script budget.

The automatic fanout is in progress and a fork erases its latest step. The node must re-post it (the step is expected to be reported a second time) and the head must still be fully fanned out.

Like autoFanoutStepErased but with two partial steps landed, of which the fork erases the second: the node has to post that step again while its bookkeeping is already at the final one.

Manual mode: the client hands the node two selections in turn. The second one drains the head, so it ends in the final fanout.

Manual mode with a fork erasing the first selection's step before the client hands over the next selection. The node must post the erased step again (the step is expected to be reported a second time) before the head can be drained.

Scenario 6: a fork erases a finalized increment, the re-post lands, and a second fork erases the re-posted increment as well.

Same balance consistency assertion as propCheckModelBalances, but over longer random action sequences: heavier L2 traffic with deposits, decommits, benign rollbacks and divergent-fork rollbacks interleaved. This is the property meant to shake out races between settlement, re-posting and rollbacks: a wedged head surfaces as a waitUntilMatch timeout inside the failing action, together with the shrunk action sequence and an io-sim trace to diagnose from.

A random walk with WorldState: deposits and decommits may overlap each other, L2 traffic and forks of every RequeueMode.

The node's head UTxO must contain everything the model has as confirmed, and nothing else except commits still pending in the model: those were submitted but not observed as finalized (SubmitDeposit), so the node may or may not have absorbed them yet.

Expect to see contestations when trying to close with an old snapshot

XXX: Since heads open empty (funds only enter via version-bumping increments), a head with funds always has $sel:onChainVersion:Start > 0 and closing with the initial snapshot (open version 0) is invalid on-chain — so this scenario is effectively vacuous under random actions. To stay meaningful it needs the mock to close with an old confirmed snapshot at the current version instead of CloseWithInitialSnapshot.

Given any random walk of the model, if the Head is open a NewTx getting confirmed must be part of the UTxO after finalization.

Observe every settlement the random walk left pending, so that the steps after it (NewTx, Close, ...) are not blocked by their preconditions.

Specialised runner similar to https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:monadicST.

Similar to https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:runSTGen

It returns Property rather than `Gen a`, what allows to enhance the logging in case of failures.