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 Number::eq spec

Browse Source
This commit is contained in:
Jay Lorch
2026-03-19 13:58:10 -07:00
parent 85e58c6f6c
commit 41c2d502fa
1 changed files with 21 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

48
src/number.rs
View File

@@ -578,33 +578,27 @@ impl PartialEq for Number {
ensures
match (self@, other@) {
(NumberView::Integer(n1), NumberView::Integer(n2)) => result == (n1 == n2),
(NumberView::Float(f1), NumberView::Integer(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(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)) => {
||| 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(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)) => {
||| {
&&& float_to_small_int(f1) matches Some(n1)
&&& float_to_small_int(f2) matches Some(n2)
&&& result == (n1 == n2)
}
||| {
&&& 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))
}
}
(NumberView::Float(f1), NumberView::Integer(n2)) =>
match float_to_small_int(f1) {
Some(n1) => result == (n1 == n2),
None => exists|f2: f64| #![trigger other@.to_f64_lossy_ensures(f2)] {
&&& 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)) =>
match float_to_small_int(f2) {
Some(n2) => result == (n1 == n2),
None => exists|f1: f64| #![trigger self@.to_f64_lossy_ensures(f1)] {
&&& 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)) =>
match (float_to_small_int(f1), float_to_small_int(f2)) {
(Some(n1), Some(n2)) => result == (n1 == n2),
_ => result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)),
},
},
)]
fn eq(&self, other: &Self) -> bool {