very few specs include properties

[kiniry]

We have tons of non-trivial properties specified for various algorithms. Sharing specs with properties permits us to easily demonstrate the power and utility of stating and having assurance about theorems in order to ensure that a specification is validated, as well as to help drive an assurance case of an implementation of the algorithm. We should endeavor to include these properties in our public specs.

[weaversa]

At the very least, each spec should come with test vectors. Also, remember that the `:safe` command adds assurance to any Cryptol function by showing it is total (defined for all inputs).

…

On Fri, Nov 13, 2020 at 4:07 PM Joseph Kiniry ***@***.***> wrote: We have tons of non-trivial properties specified for various algorithms. Sharing specs with properties permits us to easily demonstrate the power and utility of stating and having assurance about theorems in order to ensure that a specification is validated, as well as to help drive an assurance case of an implementation of the algorithm. We should endeavor to include these properties in our public specs. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#32>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABYQSOWDH3IL5OMBMF7LVNLSPWNXJANCNFSM4TVBRAAQ> .

[robdockins]

Indeed; test vectors should be an absolute minimum. For AES, SHA-2 and ECDSA, I spent a fair amount of time munging some of the public NIST test vectors into Cryptol syntax to validate the new primitive implementations. They could pretty easily be reused here, I think.

https://github.com/GaloisInc/cryptol/tree/master/tests/suiteb