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.

Sign up for GitHub

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

Jump to bottom

Cryptol float support #1237

Open
kquick opened this issue Jul 3, 2020 · 2 comments
Open

Cryptol float support #1237

kquick opened this issue Jul 3, 2020 · 2 comments
Labels
missing cryptol features Issues about features in Cryptol that don't work in SAW subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem tech debt Issues that document or involve technical debt type: feature request Issues requesting a new feature or capability
Milestone
Someday

Comments

@kquick
Copy link
Member

kquick commented Jul 3, 2020

Support for Cryptol floats is currently represented by panic and error calls (see GaloisInc/cryptol-verifier@60611b5). Actual float support needs to be implemented.
@brianhuffman
Copy link
Contributor

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
Copy link
Contributor

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

@brianhuffman brianhuffman transferred this issue from GaloisInc/cryptol-verifier Aug 7, 2020
@brianhuffman brianhuffman transferred this issue from GaloisInc/saw-core Apr 27, 2021
@brianhuffman brianhuffman added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Apr 27, 2021
@qsctr qsctr mentioned this issue Oct 2, 2023
Merged
10 tasks
@mccleeary-galois mccleeary-galois added the missing cryptol features Issues about features in Cryptol that don't work in SAW label Oct 25, 2024
@sauclovian-g sauclovian-g added tech debt Issues that document or involve technical debt type: feature request Issues requesting a new feature or capability subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core labels Oct 25, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Oct 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
missing cryptol features Issues about features in Cryptol that don't work in SAW subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem tech debt Issues that document or involve technical debt type: feature request Issues requesting a new feature or capability
Projects
None yet
Milestone
Someday
Development

No branches or pull requests
5 participants
@brianhuffman @kquick @robdockins @sauclovian-g @mccleeary-galois