Add assume_ieee_float

[Chris-Hawblitzel]

I split off assume_ieee_float from the main pull request #2229 :

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.

[jaylorch]

This refers to things in a different PR (#2229), so we should make sure not to merge it until that other PR is merged.

[Chris-Hawblitzel]

I'm copying this comment over from #2229 so we don't forget to address it:

@tjhance said:

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?