search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Make `coreLint` sanity-check numeric constraint guards #1647

Closed RyanGlScott closed 7 months ago

RyanGlScott commented 7 months ago

Currently, the coreLint code for sanity-checking numeric constraint guards doesn't actually check any interesting properties:

https://github.com/GaloisInc/cryptol/blob/1e06a4b03d596c3c5f2f6908e8f4a08feacf31d2/src/Cryptol/TypeCheck/Sanity.hs#L367-L368

In particular, it would be nice if coreLint could check that the guards are well formed. Not doing so would have made it easier to detect issues such as https://github.com/GaloisInc/saw-script/issues/2043.