Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tune tx trace spec #1695

Open
wants to merge 21 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
ad0715a
Add coverage to prop_runActions
ch1bo Oct 9, 2024
523e2a1
Increase likelihood of closed state with deltaUTxO
ch1bo Oct 9, 2024
85405f3
Increase likelihood of multiple commits
ch1bo Oct 9, 2024
495ae2e
WIP: Draft a plan
ch1bo Oct 9, 2024
a3f63da
Switch to individual snapshot production while in Open state
ch1bo Oct 10, 2024
7e7003b
Only use existing genSnapshot when producing new snapshots
ch1bo Oct 10, 2024
20913ca
Only keep knownSnapshots and derive latest version / number from it
ch1bo Oct 10, 2024
bd42c46
Revert "Only keep knownSnapshots and derive latest version / number f…
ch1bo Oct 10, 2024
31b614f
Generate plausible sequences of snapshots (version and number)
ch1bo Oct 10, 2024
8b03153
Allow for decrement with empty utxo to decommit
ch1bo Oct 10, 2024
9c6da41
Generate Nothing if realWorldModelUTxO is empty
ch1bo Oct 10, 2024
1280f85
Not shrink relevant NewSnapshots away
ch1bo Oct 10, 2024
272268b
Only update pendingDecommitUTxO in contest if not outdated
ch1bo Oct 10, 2024
3d6ae8f
Make negative decrements fail gracefully
ch1bo Oct 10, 2024
f8312ae
Fix excessive discarding by generating better snapshots
ch1bo Oct 10, 2024
cdebb64
Small tuning on generators
ch1bo Oct 10, 2024
d105327
Model toDecommit evolution as we would expect it
ch1bo Oct 10, 2024
3a150cd
Fix nextState of Close/Contest
ch1bo Oct 27, 2024
d96d55c
Futher simplify ModelUTxO
ch1bo Oct 27, 2024
ea603b9
Drop old, commented code
ch1bo Oct 27, 2024
461282e
Enable coverage check on main property
ch1bo Oct 27, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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