Skip to content

Commit

Permalink
Tune tx trace spec (#1695)
Browse files Browse the repository at this point in the history
Rewrite of the model part and tuning of the TxTrace stateful
property-based test suite comprised of:

* Allow for empty decrements, but identify `DecrementValueNegative`
errors when constructing transactions.

* Added coverage to model test `TxTrace/all valid transactions`

* Changed how snapshots are generated and modeled: Instead of generating
snapshots ad-hoc, we create them in a dedicated `NewSnapshot` action and
only pick from a list of `knownSnapshots` when generating `Close` and
other actions. This resembles better what is actually happening in the
real world, where the adversary could only pick from a list of plausible
snapshots. It also makes the `arbitraryAction` simpler and requires less
`precondition`s. Lastly, this also results in less discarded values as
was the original motivation in #1524

---

<!-- Consider each and tick it off one way or the other -->
* [x] CHANGELOG update not needed
* [x] Documentation update not needed
* [x] Haddocks updated
* [x] No new TODOs introduced or explained herafter
- Three very minor `XXX` comments how further refactoring could be done
in `TxTrace`
  • Loading branch information
v0d1ch authored Oct 28, 2024
2 parents f0d2fa0 + 461282e commit ca9c1a7
Show file tree
Hide file tree
Showing 2 changed files with 174 additions and 226 deletions.
21 changes: 10 additions & 11 deletions hydra-node/src/Hydra/Chain/Direct/State.hs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ import Hydra.Cardano.Api (
getTxId,
isScriptTxOut,
modifyTxOutValue,
negateValue,
networkIdToNetwork,
selectAsset,
selectLovelace,
Expand Down Expand Up @@ -535,7 +536,7 @@ increment ctx spendableUTxO headId headParameters incrementingSnapshot depositTx
data DecrementTxError
= InvalidHeadIdInDecrement {headId :: HeadId}
| CannotFindHeadOutputInDecrement
| SnapshotMissingDecrementUTxO
| DecrementValueNegative
| SnapshotDecrementUTxOIsNull
deriving stock (Show)

Expand All @@ -553,19 +554,17 @@ decrement ::
decrement ctx spendableUTxO headId headParameters decrementingSnapshot = do
pid <- headIdToPolicyId headId ?> InvalidHeadIdInDecrement{headId}
let utxoOfThisHead' = utxoOfThisHead pid spendableUTxO
headUTxO <- UTxO.find (isScriptTxOut headScript) utxoOfThisHead' ?> CannotFindHeadOutputInDecrement
case utxoToDecommit of
Nothing ->
Left SnapshotMissingDecrementUTxO
Just decrementUTxO
| null decrementUTxO ->
Left SnapshotDecrementUTxOIsNull
_ ->
Right $ decrementTx scriptRegistry ownVerificationKey headId headParameters headUTxO sn sigs
headUTxO@(_, headOut) <- UTxO.find (isScriptTxOut headScript) utxoOfThisHead' ?> CannotFindHeadOutputInDecrement
let balance = txOutValue headOut <> negateValue decommitValue
when (isNegative balance) $
Left DecrementValueNegative
Right $ decrementTx scriptRegistry ownVerificationKey headId headParameters headUTxO sn sigs
where
headScript = fromPlutusScript @PlutusScriptV2 Head.validatorScript

Snapshot{utxoToDecommit} = sn
decommitValue = foldMap txOutValue $ fromMaybe mempty $ utxoToDecommit sn

isNegative = any ((< 0) . snd) . IsList.toList

(sn, sigs) =
case decrementingSnapshot of
Expand Down
Loading

0 comments on commit ca9c1a7

Please sign in to comment.