Support IEEE floating point SMT theory

[Chris-Hawblitzel]

This adds support for the SMT solver's IEEE floating point theory ( https://smt-lib.org/theories-FloatingPoint.shtml ). This completes the last major item from the plan for floating point support in #1853 , building on #1859 . As with bit vectors, the IEEE operations are uninterpreted by default but are interpreted in assert-by-bit_vector, so that assert-by-bit_vector can be used for floating point reasoning. Specifications can refer to the IEEE operators by name (ieee_add, ieee_le, etc.), or by using overloaded operators (+, <=, etc.).

In general, we do not assume that Rust floating point semantics match IEEE floating point semantics (see https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md for details). However, if users are working on a platform where they are willing to make this assumption, they can use the module assume_ieee_float, which contains broadcast axioms that express this assumption. Here is a small example that uses assume_ieee_float in combination with assert-by-bit_vector to prove a simple property of a Rust f32 operation:

fn test(x: f32, y: f32) -> (z: f32)
    requires
        1.0f32 <= x <= 2.0f32,
        4.0f32 <= y <= 8.0f32,
    ensures
        5.0f32 <= z <= 10f32,
{
    broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float;

    let z = x + y;
    assert(5.0f32 <= x + y <= 10.0f32) by(bit_vector)
        requires
            1.0f32 <= x <= 2.0f32,
            4.0f32 <= y <= 8.0f32;
    z
}

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

It's unfortunate that the new axioms aren't meaningfully distinct from the other axioms in vstd. There's no indication that this is a platform specific assumption other than via the name. Is there a way we could unify this, design-wise, with our global directive for specifying platform assumptions?

[Chris-Hawblitzel]

It's unfortunate that the new axioms aren't meaningfully distinct from the other axioms in vstd. There's no indication that this is a platform specific assumption other than via the name. Is there a way we could unify this, design-wise, with our global directive for specifying platform assumptions?

Ok, I split this aspect into a separate pull request #2232 so we can discuss this separately.

[jaylorch]

This looks great! I left some individual comments about lines that I either didn't understand or thought could use improvement.