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 infinity)
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
95pub assume_specification[ <f32 as Clone>::clone ](f: &f32) -> (res: f32)
96    ensures
97        res == f,
98;
99
100pub assume_specification[ <f64 as Clone>::clone ](f: &f64) -> (res: f64)
101    ensures
102        res == f,
103;
104
105#[verifier::external_trait_specification]
106pub trait ExIeeeFloatCast<To> {
107    type ExternalTraitSpecificationFor: IeeeFloatCast<To>;
108}
109
110// deterministic IEEE cast
111#[verifier::inline]
112pub open spec fn ieee_float_cast<From: IeeeFloatCast<To>, To>(from: From) -> To {
113    from.ieee_cast()
114}
115
116// (possibly) non-deterministic Rust cast
117pub uninterp spec fn float_cast_spec<From, To>(from: From, to: To) -> bool;
118
119// Used only for internal Verus translation of "as" operator;
120// this is not meant to be called directly by user code,
121// and it is not actually compiled to executable code
122#[cfg(verus_keep_ghost)]
123#[doc(hidden)]
124#[verifier::external_body]
125#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")]
126#[verifier::when_used_as_spec(ieee_float_cast)]
127pub fn float_cast<From: Copy + IeeeFloatCast<To>, To>(from: From) -> (to: To)
128    ensures
129        float_cast_spec(from, to),
130    opens_invariants none
131    no_unwind
132{
133    unimplemented!{}
134}
135
136} // verus!
vstd/float.rs

vstd/
float.rs
