hax Support floats

Floats are kind of supported already, but all the backends reject them.

[ ] Coq
[ ] FStar

Aug 23 '23 09:08 W95Psp

Why do we need them? We don't have them in SSProve. One could potentially add them (but it would be extra work.)

Aug 23 '23 09:08 spitters

Why do we need them?

They appear in real world code. For example when doing fractions. I don't think there will be deep properties anyone wants to prove on them. But right now the tool is rejecting code because of it.

Aug 23 '23 09:08 franziskuskiefer

We also had one student here at Inria that did some work on F* verification of some post-quantum stuff that required floats, and he wanted to try Hax for that (he had to provide a model for floats in F* -- the current support of floats in F* is basically non-existent)

Aug 23 '23 09:08 W95Psp

Coq provides native IEEE 754 floats https://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIcs-ITP-2019-7.pdf

On Wed, Aug 23, 2023 at 11:30 AM Lucas Franceschino < @.***> wrote:

We also had one student here at Inria that did some work on F* verification of some post-quantum stuff that required floats, and he wanted to try Hax for that (he had to provide a model for floats in F* -- the current support of floats in F* is basically non-existent)

— Reply to this email directly, view it on GitHub https://github.com/hacspec/hacspec-v2/issues/230#issuecomment-1689614408, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTWRN75TU4JCHOXKSXTXWXEUHANCNFSM6AAAAAA33FAPWM . You are receiving this because you commented.Message ID: @.***>

Aug 23 '23 10:08 spitters

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Mar 06 '25 01:03 github-actions[bot]

There's support in F* and we add Rocq support when needed.

Mar 06 '25 12:03 franziskuskiefer