Plan to supporting floating points

[LGFae]

Hello!

I would like to know if there are any plans to add support for floating points in Verus.

I know it is quite difficult, I'd just like to know if there are any plans for it, or if it is considered out-of-scope for the project, because I couldn't find anything either in the issue tracker or in the discussions tab.

[Chris-Hawblitzel]

I think support can be implemented in stages:

1. Support floating point types and floating point constants, but leave the arithmetic operations uninterpreted. Users could use floating point and write their own axioms about arithmetic, but there wouldn't be any automated reasoning about arithmetic supplied by Verus.
2. Connect the arithmetic operations to the SMT solver's exact floating point theory in an assert by(...) context.
3. Also support real numbers, which can approximate floating point arithmetic and may be faster for the SMT solver.

The first of these steps should be easy and I have a partial implementation from a couple months ago that I haven't finished yet. The other two steps would take some more work.

[Chris-Hawblitzel]

Stage 1 is now merged ( #1859 ).

[ahuoguo]

Step 3 is merged #2025