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

Add verification of CoinSelection output errors. #2992

Merged
merged 6 commits into from
Oct 27, 2021

Conversation

jonathanknowles
Copy link
Contributor

@jonathanknowles jonathanknowles commented Oct 26, 2021

Issue Number

ADP-1037

Summary

This PR:

  • verifies errors of type SelectionOutputSizeExceedsLimitError.
  • verifies errors of type SelectionOutputTokenQuantityExceedsLimitError.
  • unifies the different post-condition verification types and functions.
  • removes outer algebraic types for verification failures, as these were not used, and are therefore boilerplate.

Instead of only offering views on the output (which are difficult to
test, because information has been lost), include the output itself.

This will allow us to more easily verify that errors are correct.
For some reason, the names of the constructors have diverged.

This commit makes them consistent again.
We don't need to pattern match on different types of failures: we only
need to be able to pretty-print any failures that occur.

Therefore, we can remove the outer algebraic types, which are just
boilerplate, and generalize the way in which we represent verification
failures.
Use of the `RecordWildCards` extension can lead to less readable code,
since it becomes harder for a reader to determine which fields have been
"absorbed" into a record value at the point of construction.

However, in the case of the post-condition verification functions
affected by this commit, it's relatively easy to tell which fields are
picked up, as the definition of each failure is always next to the
function that fails.

Therefore, we can safely use `RecordWildCards` to remove a bit of
verbosity.
@jonathanknowles jonathanknowles self-assigned this Oct 26, 2021
@jonathanknowles jonathanknowles changed the title Untitled Add verification of output errors produced by module CoinSelection. Oct 26, 2021
@jonathanknowles jonathanknowles changed the title Add verification of output errors produced by module CoinSelection. Add verification of output errors produced within CoinSelection. Oct 26, 2021
@jonathanknowles jonathanknowles changed the title Add verification of output errors produced within CoinSelection. Add verification of CoinSelection output errors. Oct 26, 2021
@jonathanknowles
Copy link
Contributor Author

bors r+

@iohk-bors
Copy link
Contributor

iohk-bors bot commented Oct 27, 2021

Build succeeded:

@iohk-bors iohk-bors bot merged commit bc0d709 into master Oct 27, 2021
@iohk-bors iohk-bors bot deleted the jonathanknowles/adp-1037/test-coin-selection-10 branch October 27, 2021 03:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants