From 2e454f2708923012510f5094603b6980e1e242a8 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Thu, 19 Mar 2026 10:49:59 -0700 Subject: [PATCH] Simplify float specs by assuming determinism --- src/number.rs | 87 ++++++++++++++++-------------------------- src/verusspec/float.rs | 29 ++++++++++++++ 2 files changed, 62 insertions(+), 54 deletions(-) diff --git a/src/number.rs b/src/number.rs index db9a3bd..46054b1 100644 --- a/src/number.rs +++ b/src/number.rs @@ -86,39 +86,31 @@ impl View for Number } } -pub open spec fn float_to_small_int_ensures(value: f64, result: Option) -> bool +pub open spec fn float_to_small_int(value: f64) -> Option { if !value.is_finite_spec() || !spec_f64_fract(value).eq_spec(&0.0f64) || spec_f64_abs(value).partial_cmp_spec(&9_007_199_254_740_992.0) == Some(Ordering::Greater) { - result is None + None } else { match value.partial_cmp_spec(&0.0) { Some(Ordering::Greater) | Some(Ordering::Equal) => { - exists|value_as_u64: u64, value_back_to_f64: f64| { - &&& float_cast_spec::(value, value_as_u64) - &&& float_cast_spec::(value_as_u64, value_back_to_f64) - &&& if value_back_to_f64.eq_spec(&value) { - result == Some(value_as_u64 as int) - } - else { - result is None - } + if ieee_float_cast::(ieee_float_cast::(value)).eq_spec(&value) { + Some(ieee_float_cast::(value) as int) + } + else { + None } }, Some(Ordering::Less) | None => { - exists|value_as_i64: i64, value_back_to_f64: f64| { - &&& float_cast_spec::(value, value_as_i64) - &&& float_cast_spec::(value_as_i64, value_back_to_f64) - &&& if value_back_to_f64.eq_spec(&value) { - result == Some(value_as_i64 as int) - } - else { - result is None - } + if ieee_float_cast::(ieee_float_cast::(value)).eq_spec(&value) { + Some(ieee_float_cast::(value) as int) + } + else { + None } }, } @@ -131,14 +123,8 @@ impl NumberView { match self { NumberView::Integer(v) => { - ||| { - &&& 0 <= v <= u64::MAX - &&& float_cast_spec::(v as u64, f) - } - ||| { - &&& i64::MIN <= v <= i64::MAX - &&& float_cast_spec::(v as i64, f) - } + ||| 0 <= v <= u64::MAX && f == ieee_float_cast::(v as u64) + ||| i64::MIN <= v <= i64::MAX && f == ieee_float_cast::(v as i64) ||| exists|bi: BigInt| { &&& bi@ == v &&& match #[trigger] verusspec::bigint::ToPrimitiveSpec::spec_to_f64(&bi) { @@ -278,8 +264,8 @@ impl Number { NumberView::Float(f) => { match result { - None => float_to_small_int_ensures(f, None), - Some(bi) => float_to_small_int_ensures(f, Some(bi@)), + None => float_to_small_int(f) is None, + Some(bi) => float_to_small_int(f) == Some(bi@), } }, }, @@ -296,14 +282,15 @@ impl Number { #[verus_spec(result => ensures match result { - Some(bi) => float_to_small_int_ensures(value, Some(bi@)), - None => float_to_small_int_ensures(value, None), + Some(bi) => float_to_small_int(value) == Some(bi@), + None => float_to_small_int(value) is None, }, )] fn float_to_small_bigint(value: f64) -> Option { proof! { axiom_f64_obeys_eq_spec(); axiom_f64_obeys_partial_cmp_spec(); + axiom_f64_ops_deterministic(); } if !value.is_finite() || value.fract() != 0.0 { @@ -335,8 +322,8 @@ impl Number { NumberView::Integer(n) => result matches Some(bi) && bi@ == n, NumberView::Float(f) => match result { - Some(bi) => float_to_small_int_ensures(f, Some(bi@)), - None => float_to_small_int_ensures(f, None), + Some(bi) => float_to_small_int(f) == Some(bi@), + None => float_to_small_int(f) is None, }, }, )] @@ -352,6 +339,7 @@ impl Number { self@.to_f64_lossy_ensures(result) )] fn to_f64_lossy(&self) -> f64 { + proof! { axiom_f64_ops_deterministic(); } match self { Number::UInt(v) => *v as f64, Number::Int(v) => *v as f64, @@ -376,9 +364,7 @@ impl Number { }, )] fn is_zero(&self) -> bool { - proof! { - axiom_f64_obeys_eq_spec(); - } + proof! { axiom_f64_obeys_eq_spec(); } match self { Number::UInt(0) | Number::Int(0) => true, Number::Float(f) => *f == 0.0, @@ -402,8 +388,8 @@ impl Number { #[verus_spec(result => ensures match result@ { - NumberView::Integer(n) => float_to_small_int_ensures(value, Some(n)), - NumberView::Float(f) => float_to_small_int_ensures(value, None) && f == value, + NumberView::Integer(n) => float_to_small_int(value) == Some(n), + NumberView::Float(f) => float_to_small_int(value) is None && f == value, } )] fn normalize_float(value: f64) -> Number { @@ -598,36 +584,29 @@ impl PartialEq for Number { match (self@, other@) { (NumberView::Integer(n1), NumberView::Integer(n2)) => result == (n1 == n2), (NumberView::Float(f1), NumberView::Integer(n2)) => { - ||| exists|n1: int| #![trigger float_to_small_int_ensures(f1, Some(n1))] { - &&& float_to_small_int_ensures(f1, Some(n1)) - &&& result == (n1 == n2) - } + ||| float_to_small_int(f1) matches Some(n1) && result == (n1 == n2) ||| exists|f2: f64| #![trigger other@.to_f64_lossy_ensures(f2)] { - &&& float_to_small_int_ensures(f1, None) + &&& float_to_small_int(f1) is None &&& other@.to_f64_lossy_ensures(f2) &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)) } }, (NumberView::Integer(n1), NumberView::Float(f2)) => { - ||| exists|n2: int| #![trigger float_to_small_int_ensures(f2, Some(n2))] { - &&& float_to_small_int_ensures(f2, Some(n2)) - &&& result == (n1 == n2) - } + ||| float_to_small_int(f2) matches Some(n2) && result == (n1 == n2) ||| exists|f1: f64| #![trigger self@.to_f64_lossy_ensures(f1)] { - &&& float_to_small_int_ensures(f2, None) + &&& float_to_small_int(f2) is None &&& self@.to_f64_lossy_ensures(f1) &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)) } }, (NumberView::Float(f1), NumberView::Float(f2)) => { - ||| exists|n1: int, n2: int| #![trigger float_to_small_int_ensures(f1, Some(n1)), - float_to_small_int_ensures(f2, Some(n2))] { - &&& float_to_small_int_ensures(f1, Some(n1)) - &&& float_to_small_int_ensures(f2, Some(n2)) + ||| { + &&& float_to_small_int(f1) matches Some(n1) + &&& float_to_small_int(f2) matches Some(n2) &&& result == (n1 == n2) } ||| { - &&& float_to_small_int_ensures(f1, None) || float_to_small_int_ensures(f2, None) + &&& float_to_small_int(f1) is None || float_to_small_int(f2) is None &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)) } } diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs index d2f7f73..cdc412b 100644 --- a/src/verusspec/float.rs +++ b/src/verusspec/float.rs @@ -28,6 +28,35 @@ pub axiom fn axiom_f64_obeys_partial_cmp_spec() ::obeys_partial_cmp_spec(), ; +pub axiom fn axiom_f64_ops_deterministic() + ensures + ::obeys_neg_spec(), + ::obeys_add_spec(), + ::obeys_sub_spec(), + ::obeys_mul_spec(), + ::obeys_div_spec(), + forall|n: i8, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u8, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i8, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u8, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i16, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u16, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i16, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u16, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i32, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u32, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i32, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u32, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i64, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u64, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i64, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u64, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: i128, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: u128, f: f64| float_cast_spec::(n, f) ==> f == ieee_float_cast::(n), + forall|n: i128, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), + forall|n: u128, f: f64| float_cast_spec::(f, n) ==> n == ieee_float_cast::(f), +; + pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool) ensures res == f.is_finite_spec(),