Cryptol float support - Githubissues

GaloisInc / saw-script

The SAW scripting language.

BSD 3-Clause "New" or "Revised" License

438 stars 63 forks source link

Cryptol float support #1237

Open kquick opened 4 years ago

kquick commented 4 years ago

Support for Cryptol floats is currently represented by panic and error calls (see https://github.com/GaloisInc/cryptol-verifier/pull/26/commits/60611b5631fa5762108eb24b1a3d88cd2a0940db). Actual float support needs to be implemented.

brianhuffman commented 4 years ago

The float primitives should all be translated using the saw-core error function; there shouldn't be any Haskell panic that happens during Cryptol-to-saw-core translation! If any user-triggerable panic is found, it should be filed as a bug.

Removing the uses of error in for floating point operations in Cryptol.sawcore will have to wait until we add corresponding floating point primitives to saw-core.

robdockins commented 4 years ago

Well, the saw-core error function also just calls panic, so it isn't much of an improvement. https://github.com/GaloisInc/saw-core/issues/59