verus/examples/float.rs at main · verus-lang/verus · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
use verus_builtin::*;
use verus_builtin_macros::*;
use vstd::*;

verus! {

use vstd::std_specs::ops::AddSpec;
use vstd::float::FloatBitsProperties;

/*
Verus deliberately omits axioms about floating point from vstd,
because the desired set of useful and sound axioms may vary by project and platform.
(See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md for details
about why Rust floating point semantics are complex, may be non-deterministic, and may fall short
of desired behavior on some platforms.)
Therefore, projects that want to prove properties of about floating-point numbers may want
to define their own axioms, or even define different groups of axioms for different situations.

For example, one useful axiom is that it is always safe to add any two floats
(this assumes that the platform is correctly configured not to trap on a NaN result,
which should usually be true):
*/

pub broadcast axiom fn f64_can_add_anything(a: f64, b: f64)
    ensures
        #[trigger] a.add_req(b);

/*
The axiom above doesn't guarantee non-NaN results -- it's possible to add large positive numbers to
construct positive infinity, to add large negative numbers to construct negative infinity,
and then add negative infinity to positive infinity to construct a NaN.
As an example of verifying something slightly nontrivial,
the axioms below only permit addition of positive numbers,
and guarantee non-NaN results.
*/

pub broadcast axiom fn f64_add_positive_spec(a: f64, b: f64)
    requires
        !a.is_nan_spec(),
        !b.is_nan_spec(),
        !a.is_sign_negative_spec(),
        !b.is_sign_negative_spec(),
    ensures
        #![trigger a.add_spec(b)]
        !a.add_spec(b).is_nan_spec(),
        !a.add_spec(b).is_sign_negative_spec();

pub broadcast axiom fn f64_add_positive_exec(a: f64, b: f64)
    requires
        !a.is_nan_spec(),
        !b.is_nan_spec(),
        !a.is_sign_negative_spec(),
        !b.is_sign_negative_spec(),
    ensures
        #[trigger] a.add_req(b);

use vstd::std_specs::ops::add_ensures;

pub broadcast axiom fn f64_add_positive_ensures(a: f64, b: f64, o: f64)
    requires
        !a.is_nan_spec(),
        !b.is_nan_spec(),
        !a.is_sign_negative_spec(),
        !b.is_sign_negative_spec(),
    ensures
        #[trigger] add_ensures::<f64>(a, b, o) ==> o == a.add_spec(b);

pub broadcast group f64_add_positive {
    f64_add_positive_spec,
    f64_add_positive_exec,
    f64_add_positive_ensures,
}

fn main() {
    broadcast use f64_add_positive;
    let a: f64 = 3.1;
    let b: f64 = 2.8;
    let c = a + b;
    let d = b + c;
    let e = c + d;

    // This would fail the !b.is_sign_negative_spec() precondition:
    // let f = e + (-0.7);

    // But if we use the more permissive axiom, then we can add a negative number
    // (albeit with no guarantee about the result):
    broadcast use f64_can_add_anything;
    let f = e + (-0.7);
}

} // verus!