kata-containers/regorus
1
0
Fork 0
mirror of https://github.com/microsoft/regorus.git synced 2026-08-05 02:16:11 +00:00
Code Issues Packages Projects Releases Wiki Activity

Simplify float comparisons by assuming IEEE

Browse Source
This commit is contained in:
Jay Lorch
2026-03-19 11:52:35 -07:00
parent 9e18ded98e
commit 85e58c6f6c
2 changed files with 15 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/number.rs
View File

@@ -90,10 +90,10 @@ pub open spec fn float_to_small_int(value: f64) -> Option<int>
{
if !value.is_finite_spec() ||
!spec_f64_fract(value).eq_spec(&0.0f64) ||
spec_f64_abs(value).is_gt(&9_007_199_254_740_992.0) {
spec_f64_abs(value) > 9_007_199_254_740_992.0 {
None
}
else if value.is_ge(&0.0) {
else if value >= 0.0 {
if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
Some(ieee_float_cast::<f64, u64>(value) as int)
}
@@ -285,6 +285,7 @@ impl Number {
axiom_f64_obeys_eq_spec();
axiom_f64_obeys_partial_cmp_spec();
axiom_f64_ops_deterministic();
axiom_f64_comparisons_match_ieee();
}
if !value.is_finite() || value.fract() != 0.0 {

12
src/verusspec/float.rs
View File

@@ -14,6 +14,10 @@
#[cfg(verus_keep_ghost)]
use vstd::float::*;
#[cfg(verus_keep_ghost)]
use vstd::std_specs::cmp::PartialEqIs;
#[cfg(verus_keep_ghost)]
use vstd::std_specs::cmp::PartialOrdIs;
use vstd::prelude::*;
verus! {
@@ -28,6 +32,14 @@ pub axiom fn axiom_f64_obeys_partial_cmp_spec()
<f64 as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
;
pub axiom fn axiom_f64_comparisons_match_ieee()
ensures
forall|f1: f64, f2: f64| #[trigger] f1.ieee_lt(f2) <==> f1.is_lt(&f2),
forall|f1: f64, f2: f64| #[trigger] f1.ieee_le(f2) <==> f1.is_le(&f2),
forall|f1: f64, f2: f64| #[trigger] f1.ieee_gt(f2) <==> f1.is_gt(&f2),
forall|f1: f64, f2: f64| #[trigger] f1.ieee_ge(f2) <==> f1.is_ge(&f2),
;
pub axiom fn axiom_f64_ops_deterministic()
ensures
<f64 as vstd::std_specs::ops::NegSpec>::obeys_neg_spec(),