Tune tx trace spec #1695
Open
Tune tx trace spec #1695
+174
−226
Commits on Oct 27, 2024
-
Add coverage to prop_runActions
This will ensure we have good coverage of the actual model test later. For now, the efficiency is way to low to checkCoverage on it too (it would go up to 6400 tests like prop_traces).
-
-
-
Changing the way we generate actions will help in guiding the generators based on "what an honest node would approve" and reduce discarded values / improve coverage.
-
Only use existing genSnapshot when producing new snapshots
Otherwise we simpliy pick from the models knownSnapshots
-
Revert "Only keep knownSnapshots and derive latest version / number f…
…rom it" This reverts commit b92f051.
-
Allow for decrement with empty utxo to decommit
The decrement validator allows for this and consequently this is a possible scenario: An adversary can construct decrement transactions with any snapshot we signed.
-
Generate Nothing if realWorldModelUTxO is empty
This is more consistent with what the off-chain code does.
-
-
-
Make negative decrements fail gracefully
Also disables some preconditions to decide whether we want to test this.
-
Fix excessive discarding by generating better snapshots
This also makes the output easier to read and removes several preconditions as we now expect construction to fail if we try to decrement too much.
-
-
Model toDecommit evolution as we would expect it
This is reusing the models pendingDecommit for this purpose. However, it would be cleaner to separate the model states between Open and Closed.
-
-
It is a list of A-E elements only where shuffling of the elements represents off-chain transactions that maintain balance.
-
-
Enable coverage check on main property
Using lower Confidence values, we should not see way very long tests at the cost of occasional false positives. In such cases, the actual coverage numbers and "interesting values" test should give an indication whether it was rightfully failing or would have taken just very long.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.