vstd/
float.rs

1//! Properties of floating point values.
2use super::prelude::*;
3
4verus! {
5
6pub trait FloatBitsProperties {
7    type Bits;
8
9    spec fn to_bits_spec(&self) -> Self::Bits;
10
11    // All bits except sign bit
12    spec fn to_bits_abs_spec(&self) -> Self::Bits;
13
14    // Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN)
15    spec fn is_sign_negative_spec(&self) -> bool;
16
17    // Zero, subnormal, or normal (not infinite, not NaN)
18    spec fn is_finite_spec(&self) -> bool;
19
20    // Positive or negative infinity (not zero, not subnormal, not normal, not NaN)
21    spec fn is_infinite_spec(&self) -> bool;
22
23    // A NaN value (not zero, not subnormal, not normal, not NaN)
24    spec fn is_nan_spec(&self) -> bool;
25}
26
27impl FloatBitsProperties for f32 {
28    type Bits = u32;
29
30    open spec fn to_bits_spec(&self) -> u32 {
31        f32_to_bits(*self)
32    }
33
34    open spec fn to_bits_abs_spec(&self) -> u32 {
35        let bits = self.to_bits_spec();
36        if bits >= 0x8000_0000 {
37            (bits - 0x8000_0000) as u32
38        } else {
39            bits
40        }
41    }
42
43    // Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN)
44    open spec fn is_sign_negative_spec(&self) -> bool {
45        self.to_bits_spec() >= 0x8000_0000
46    }
47
48    open spec fn is_finite_spec(&self) -> bool {
49        self.to_bits_abs_spec() < 0x7f80_0000
50    }
51
52    open spec fn is_infinite_spec(&self) -> bool {
53        self.to_bits_abs_spec() == 0x7f80_0000
54    }
55
56    open spec fn is_nan_spec(&self) -> bool {
57        self.to_bits_abs_spec() > 0x7f80_0000
58    }
59}
60
61impl FloatBitsProperties for f64 {
62    type Bits = u64;
63
64    open spec fn to_bits_spec(&self) -> u64 {
65        f64_to_bits(*self)
66    }
67
68    open spec fn to_bits_abs_spec(&self) -> u64 {
69        let bits = self.to_bits_spec();
70        if bits >= 0x8000_0000_0000_0000 {
71            (bits - 0x8000_0000_0000_0000) as u64
72        } else {
73            bits
74        }
75    }
76
77    // Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN)
78    open spec fn is_sign_negative_spec(&self) -> bool {
79        self.to_bits_spec() >= 0x8000_0000_0000_0000
80    }
81
82    open spec fn is_finite_spec(&self) -> bool {
83        self.to_bits_abs_spec() < 0x7ff0_0000_0000_0000
84    }
85
86    open spec fn is_infinite_spec(&self) -> bool {
87        self.to_bits_abs_spec() == 0x7ff0_0000_0000_0000
88    }
89
90    open spec fn is_nan_spec(&self) -> bool {
91        self.to_bits_abs_spec() > 0x7ff0_0000_0000_0000
92    }
93}
94
95} // verus!
vstd/float.rs

vstd/
float.rs
