diff --git a/Cargo.lock b/Cargo.lock index d73ba74..ea43c68 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1613,15 +1613,15 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "verus_builtin" -version = "0.0.0-2026-03-01-0109" +version = "0.0.0-2026-03-17-2326" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ee0548b407f2cbfb0228b65cd91e09be63cfd4e883b5a997b3a4e2158febe8f" +checksum = "d7ab914ab490975465ecb3286edceecb0743c3628ddeefcdf25158683e83e2fe" [[package]] name = "verus_builtin_macros" -version = "0.0.0-2026-03-08-0103" +version = "0.0.0-2026-03-17-2326" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5521119b3fd13d0b1748a0fef287a9aeeb247dd702cd7b15f96e5b9eb95f002b" +checksum = "46f1f1ee124e0bcb5cec79836ff015d138ea53bff51839a85b8364cdc8b79232" dependencies = [ "proc-macro2 1.0.106", "quote 1.0.44", @@ -1633,9 +1633,9 @@ dependencies = [ [[package]] name = "verus_prettyplease" -version = "0.0.0-2026-02-24-1505" +version = "0.0.0-2026-03-15-0111" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2930f00a7327e9837d0266a8261b35b3cf59761f50541ff471ca5e5229b7563" +checksum = "eadebc1e3b522b32c178fd2fb882e691880ff983415497232c74aa9b72bc0b65" dependencies = [ "proc-macro2 1.0.106", "verus_syn", @@ -1643,9 +1643,9 @@ dependencies = [ [[package]] name = "verus_state_machines_macros" -version = "0.0.0-2026-03-01-0109" +version = "0.0.0-2026-03-15-0111" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86996dd79d212559f03818a8973d7b9a71d26d404287e9fd2f597001f8c6cef5" +checksum = "b824c6405f8e8a063ca4a26fca1f454cb02de0c1c4da685e3e7f1974899129d5" dependencies = [ "indexmap 1.9.3", "proc-macro2 1.0.106", @@ -1655,9 +1655,9 @@ dependencies = [ [[package]] name = "verus_syn" -version = "0.0.0-2026-02-24-1505" +version = "0.0.0-2026-03-15-0111" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "baea36d7ed6cf44ce889b54740f7ae7a10622788f018b04c1addbe88109f59bb" +checksum = "1694faf01f89e1abc996da7b8d24a4e0d1ebd70147dc659e7a5dd680af696772" dependencies = [ "proc-macro2 1.0.106", "quote 1.0.44", @@ -1672,9 +1672,9 @@ checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64" [[package]] name = "vstd" -version = "0.0.0-2026-03-08-0103" +version = "0.0.0-2026-03-17-2326" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e19bb62988a03cc130a39566b58ece7677ecb26e70a05ca95bf06f7169ca6af5" +checksum = "13bbf59dfaa6a7bcb327412c778a5d2b2c226dc65473a981ae6ec53a04c75aba" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/Cargo.toml b/Cargo.toml index eafb14a..9cd8faf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -136,7 +136,7 @@ indexmap = { version = "2.12.1", default-features = false, features = ["serde"], bincode = { version = "2.0.1", default-features = false, features = ["alloc", "serde"], optional = true } # Use Verus for verification -vstd = { version = "0.0.0-2026-03-08-0103" } +vstd = { version = "0.0.0-2026-03-17-2326" } [dev-dependencies] anyhow = "1.0.45" diff --git a/src/lib.rs b/src/lib.rs index 4746692..b86fe69 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,8 @@ // Unsafe code should not be used. // Hard to reason about correctness, and maintainability. #![cfg_attr(not(verus_keep_ghost), forbid(unsafe_code))] +#![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))] +#![cfg_attr(verus_keep_ghost, feature(stmt_expr_attributes))] // Ensure that all lint names are valid. #![deny(unknown_lints)] // Fail-fast lints: correctness, safety, and API surface diff --git a/src/number.rs b/src/number.rs index 2c1c117..db9a3bd 100644 --- a/src/number.rs +++ b/src/number.rs @@ -12,9 +12,6 @@ clippy::pattern_type_mismatch )] -#![cfg_attr(verus_keep_ghost, feature(proc_macro_hygiene))] -#![cfg_attr(verus_keep_ghost, feature(stmt_expr_attributes))] - use alloc::format; use alloc::string::{String, ToString}; use core::cmp::Ordering; @@ -30,13 +27,13 @@ use num_traits::{One, Signed, ToPrimitive, Zero}; use serde::ser::Serializer; use serde::Serialize; -use vstd::prelude::*; #[cfg(verus_keep_ghost)] use vstd::float::*; -#[cfg(verus_keep_ghost)] -use vstd::std_specs::convert::*; +use vstd::prelude::*; #[cfg(verus_keep_ghost)] use vstd::std_specs::cmp::*; +#[cfg(verus_keep_ghost)] +use vstd::std_specs::convert::*; use crate::*; @@ -89,50 +86,68 @@ impl View for Number } } -impl Number { - spec fn spec_float_to_small_int(value: f64) -> Option - { - if !spec_f64_is_finite(value) || - !spec_f64_fract(value).eq_spec(&0.0f64) || - spec_f64_abs(value).partial_cmp_spec(&F64_SAFE_INTEGER) == Some(Ordering::Greater) { - None - } - else { - match value.partial_cmp_spec(&0.0) { - Some(Ordering::Greater) | Some(Ordering::Equal) => - if spec_u64_as_f64(spec_f64_as_u64(value)).eq_spec(&value) { - Some(spec_f64_as_u64(value) as int) - } - else { - None - }, - Some(Ordering::Less) | None => - if spec_i64_as_f64(spec_f64_as_i64(value)).eq_spec(&value) { - Some(spec_f64_as_i64(value) as int) - } - else { - None - }, - } - } +pub open spec fn float_to_small_int_ensures(value: f64, result: Option) -> bool +{ + 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 } - - - spec fn spec_to_f64_lossy(self: &Self) -> f64 - { - match self { - Number::UInt(v) => spec_u64_as_f64(*v), - Number::Int(v) => spec_i64_as_f64(*v), - Number::Float(v) => *v, - Number::BigInt(v) => { - if let Some(f) = ::spec_to_f64(v) { - f - } else if v@ < 0 { - spec_f64_neg_infinity() - } else { - spec_f64_infinity() + 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 + } } }, + 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 + } + } + }, + } + } +} + +impl NumberView { + pub open spec fn to_f64_lossy_ensures(self: Self, f: f64) -> bool + { + 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) + } + ||| exists|bi: BigInt| { + &&& bi@ == v + &&& match #[trigger] verusspec::bigint::ToPrimitiveSpec::spec_to_f64(&bi) { + Some(x) => f == x, + None => f == if v < 0 { spec_f64_neg_infinity() } else { spec_f64_infinity() } + } + } + }, + NumberView::Float(v) => f == v, } } } @@ -214,15 +229,13 @@ impl PartialEqSpecImpl for Number { } // end verus! - #[verus_verify] impl Number { #[verus_spec(result => ensures result@ == NumberView::Integer(value@), )] - fn from_bigint_owned(value: BigInt) -> Self - { + fn from_bigint_owned(value: BigInt) -> Self { if value.is_zero() { return Number::Int(0); } @@ -244,8 +257,7 @@ impl Number { ensures result@ == NumberView::Integer(value as int), )] - fn from_i128(value: i128) -> Self - { + fn from_i128(value: i128) -> Self { if value >= 0 { if let Ok(u) = u64::try_from(value) { return Number::UInt(u); @@ -264,14 +276,15 @@ impl Number { match self@ { NumberView::Integer(n) => result matches Some(bi) && bi@ == n, NumberView::Float(f) => - match Self::spec_float_to_small_int(f) { - Some(n) => result matches Some(bi) && bi@ == n, - None => result is None, - }, + { + match result { + None => float_to_small_int_ensures(f, None), + Some(bi) => float_to_small_int_ensures(f, Some(bi@)), + } + }, }, )] - fn to_bigint_owned(&self) -> Option - { + fn to_bigint_owned(&self) -> Option { match self { Number::UInt(v) => Some(BigInt::from(*v)), Number::Int(v) => Some(BigInt::from(*v)), @@ -282,13 +295,12 @@ impl Number { #[verus_spec(result => ensures - match Self::spec_float_to_small_int(value) { - Some(i) => result matches Some(bi) && bi@ == i, - None => result is None, + match result { + Some(bi) => float_to_small_int_ensures(value, Some(bi@)), + None => float_to_small_int_ensures(value, None), }, )] - fn float_to_small_bigint(value: f64) -> Option - { + fn float_to_small_bigint(value: f64) -> Option { proof! { axiom_f64_obeys_eq_spec(); axiom_f64_obeys_partial_cmp_spec(); @@ -303,13 +315,13 @@ impl Number { } if value >= 0.0 { - let u = f64_as_u64(value); - if u64_as_f64(u) == value { + let u = value as u64; + if u as f64 == value { return Some(BigInt::from(u)); } } else { - let i = f64_as_i64(value); - if i64_as_f64(i) == value { + let i = value as i64; + if i as f64 == value { return Some(BigInt::from(i)); } } @@ -322,14 +334,13 @@ impl Number { match self@ { NumberView::Integer(n) => result matches Some(bi) && bi@ == n, NumberView::Float(f) => - match Self::spec_float_to_small_int(f) { - Some(n) => result matches Some(bi) && bi@ == n, - None => result is None, + match result { + Some(bi) => float_to_small_int_ensures(f, Some(bi@)), + None => float_to_small_int_ensures(f, None), }, }, )] - fn to_bigint_rc(&self) -> Option> - { + fn to_bigint_rc(&self) -> Option> { match self { Number::BigInt(v) => Some(v.clone()), _ => self.to_bigint_owned().map(Rc::new), @@ -338,13 +349,12 @@ impl Number { #[verus_spec(result => ensures - result == self.spec_to_f64_lossy(), + self@.to_f64_lossy_ensures(result) )] - fn to_f64_lossy(&self) -> f64 - { + fn to_f64_lossy(&self) -> f64 { match self { - Number::UInt(v) => u64_as_f64(*v), - Number::Int(v) => i64_as_f64(*v), + Number::UInt(v) => *v as f64, + Number::Int(v) => *v as f64, Number::Float(v) => *v, Number::BigInt(v) => { if let Some(f) = v.to_f64() { @@ -365,8 +375,7 @@ impl Number { NumberView::Float(f) => result == f.eq_spec(&0.0f64), }, )] - fn is_zero(&self) -> bool - { + fn is_zero(&self) -> bool { proof! { axiom_f64_obeys_eq_spec(); } @@ -386,20 +395,18 @@ impl Number { a@ matches NumberView::Integer(m) && result.0@ == m, b@ matches NumberView::Integer(n) && result.1@ == n, )] - fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) - { + fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) { (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap()) } #[verus_spec(result => ensures - match Self::spec_float_to_small_int(value) { - Some(i) => result@ == NumberView::Integer(i), - None => result@ == NumberView::Float(value), - }, + 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, + } )] - fn normalize_float(value: f64) -> Number - { + fn normalize_float(value: f64) -> Number { if let Some(i) = Self::float_to_small_bigint(value) { return Self::from_bigint_owned(i); } @@ -413,8 +420,7 @@ impl Number { NumberView::Float(_) => result is None, }, )] - fn as_u32(&self) -> Option - { + fn as_u32(&self) -> Option { match self { Number::UInt(v) if *v <= u32::MAX as u64 => Some(*v as u32), Number::Int(v) if *v >= 0 && *v <= u32::MAX as i64 => Some(*v as u32), @@ -448,8 +454,7 @@ impl From for Number { ensures result@ == NumberView::Integer(value@), )] - fn from(value: BigInt) -> Self - { + fn from(value: BigInt) -> Self { Number::from_bigint_owned(value) } } @@ -460,20 +465,18 @@ impl From for Number { ensures result@ == NumberView::Integer(value as int), )] - fn from(value: u64) -> Self - { + fn from(value: u64) -> Self { Number::UInt(value) } } -#[verus_verify] +#[verus_verify] impl From for Number { #[verus_spec(result => ensures result@ == NumberView::Integer(value as int), )] - fn from(value: usize) -> Self - { + fn from(value: usize) -> Self { Number::UInt(value as u64) } } @@ -484,8 +487,7 @@ impl From for Number { ensures result@ == NumberView::Integer(value as int), )] - fn from(value: u128) -> Self - { + fn from(value: u128) -> Self { if let Ok(n) = u64::try_from(value) { Number::UInt(n) } else { @@ -500,8 +502,7 @@ impl From for Number { ensures result@ == NumberView::Integer(value as int), )] - fn from(value: i64) -> Self - { + fn from(value: i64) -> Self { Number::Int(value) } } @@ -512,8 +513,7 @@ impl From for Number { ensures result@ == NumberView::Integer(value as int), )] - fn from(value: i128) -> Self - { + fn from(value: i128) -> Self { Number::from_i128(value) } } @@ -524,8 +524,7 @@ impl From for Number { ensures result@ == NumberView::Float(value), )] - fn from(value: f64) -> Self - { + fn from(value: f64) -> Self { Number::Float(value) } } @@ -598,12 +597,47 @@ impl PartialEq for Number { ensures match (self@, other@) { (NumberView::Integer(n1), NumberView::Integer(n2)) => result == (n1 == n2), - _ => true, + (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) + } + ||| exists|f2: f64| #![trigger other@.to_f64_lossy_ensures(f2)] { + &&& float_to_small_int_ensures(f1, 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) + } + ||| exists|f1: f64| #![trigger self@.to_f64_lossy_ensures(f1)] { + &&& float_to_small_int_ensures(f2, 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)) + &&& result == (n1 == n2) + } + ||| { + &&& float_to_small_int_ensures(f1, None) || float_to_small_int_ensures(f2, None) + &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)) + } + } }, )] - fn eq(&self, other: &Self) -> bool - { - proof! { axiom_bigint_obeys_eq_spec(); } + fn eq(&self, other: &Self) -> bool { + proof! { + axiom_bigint_obeys_eq_spec(); + axiom_f64_obeys_eq_spec(); + } if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) { return a == b; diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs index db3a171..d2f7f73 100644 --- a/src/verusspec/float.rs +++ b/src/verusspec/float.rs @@ -12,6 +12,8 @@ clippy::pattern_type_mismatch )] +#[cfg(verus_keep_ghost)] +use vstd::float::*; use vstd::prelude::*; verus! { @@ -26,62 +28,16 @@ pub axiom fn axiom_f64_obeys_partial_cmp_spec() ::obeys_partial_cmp_spec(), ; -pub uninterp spec fn spec_f64_as_u64(f: f64) -> u64; - -#[inline] -#[verifier::external_body] -pub fn f64_as_u64(f: f64) -> (res: u64) - ensures - res == spec_f64_as_u64(f), -{ - f as u64 -} - -pub uninterp spec fn spec_u64_as_f64(u: u64) -> f64; - -#[inline] -#[verifier::external_body] -pub fn u64_as_f64(u: u64) -> (res: f64) - ensures - res == spec_u64_as_f64(u), -{ - u as f64 -} - -pub uninterp spec fn spec_f64_as_i64(f: f64) -> i64; - -#[inline] -#[verifier::external_body] -pub fn f64_as_i64(f: f64) -> (res: i64) - ensures - res == spec_f64_as_i64(f), -{ - f as i64 -} - -pub uninterp spec fn spec_i64_as_f64(u: i64) -> f64; - -#[inline] -#[verifier::external_body] -pub fn i64_as_f64(i: i64) -> (res: f64) - ensures - res == spec_i64_as_f64(i), -{ - i as f64 -} - -pub uninterp spec fn spec_f64_is_finite(f: f64) -> bool; - pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool) ensures - res == spec_f64_is_finite(f), + res == f.is_finite_spec(), ; pub uninterp spec fn spec_f64_fract(f: f64) -> f64; pub assume_specification [ f64::fract ](f: f64) -> (res: f64) requires - spec_f64_is_finite(f), + f.is_finite_spec(), ensures res == spec_f64_fract(f), ; @@ -90,16 +46,14 @@ pub uninterp spec fn spec_f64_abs(f: f64) -> f64; pub assume_specification [ f64::abs ](f: f64) -> (res: f64) requires - spec_f64_is_finite(f), + f.is_finite_spec(), ensures res == spec_f64_abs(f), ; -pub uninterp spec fn spec_f64_is_nan(f: f64) -> bool; - pub assume_specification [ f64::is_nan ](f: f64) -> (res: bool) ensures - res == spec_f64_is_nan(f), + res == f.is_nan_spec(), ; pub uninterp spec fn spec_f64_neg_infinity() -> f64;