-
Notifications
You must be signed in to change notification settings - Fork 157
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
Added first Necessary And Sufficient EraRule tests #4423
base: master
Are you sure you want to change the base?
Conversation
0d26507
to
df13324
Compare
I haven't had time yet to look in deep detail. However, what I'm a little bit concerned about here is that
This way it would be possible to control the behaviour of different assertions in a neat way given we write some convenient syntax for constructing |
I completely agree with this. One thing missing is communicating, back to the test, what extra information is being used. That will be necessary to make good error messages if one of them fails. |
397bbb3
to
c3d134e
Compare
c3d134e
to
57a2943
Compare
|
||
module Test.Cardano.Ledger.Constrained.Conway.NecessaryAndSufficient where | ||
|
||
-- hiding (Pred,match,reify) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
-- hiding (Pred,match,reify) |
-- , ("voteDelegated", ppMap pcCredential pcDRep (dRepMap um)) | ||
-- , ("ptrs", ppMap ppPtr pcCredential (ptrMap um)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
-- , ("voteDelegated", ppMap pcCredential pcDRep (dRepMap um)) | |
-- , ("ptrs", ppMap ppPtr pcCredential (ptrMap um)) |
prop "GOVCERT Invert 1" $ govProp (Invert 1) | ||
prop "GOVCERT Invert 2" $ govProp (Invert 2) | ||
prop "GOVCERT Invert 3" $ govProp (Invert 3) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think having to number each predicate that we want to flip and having to make a separate test for each number is a bit too much. Could this numbering be done behind the scenes somehow so that whoever is writing these constraints doesn't need to keep track of that?
assertExplain | ||
["Status Nonmatching Invert (" ++ show n ++ " /= " ++ show m ++ " (" ++ show x ++ ")"] | ||
x | ||
assertWith n Remove x = assertExplain ["Status Remove " ++ show n ++ " (" ++ show x ++ ")"] TruePred |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wouldn't it make sense to also remove the constraints one-by-one like we do with Invert
?
Adds a new style of tests.
One writes a specification for a triple (Environment, State, Signal).
This specifucation specifies the minimal constraints to make the tests pass.
Tests can be run in 3 Modes 1) Apply, Invert, Remove
In Apply Mode, we test that the given tests are Sufficient to pass the STS rules.
in Invert Mode, we test that the given tests are Neccssary, as we invert them, and then Expect the test to Fail.
if the test doesn't fail, the test is Not necessary.
in Remove Mode, we remove the constraint. It may or may not pass, as one can get lucky. We use classify
to record which constraints can get lucky.
Checklist
.cabal
andCHANGELOG.md
files according to theversioning process.
.cabal
files for all affected packages are updated. If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)CHANGELOG.md
for the affected packages. New section is never added with the code changes. (See RELEASING.md)fourmolu
(usescripts/fourmolize.sh
)scripts/cabal-format.sh
)hie.yaml
has been updated (usescripts/gen-hie.sh
)