More specs for Number

src/number.rs

@@ -539,8 +539,31 @@ impl FromStr for Number {
     }
 }
 
+verus! {
+
+#[cfg(verus_keep_ghost)]
+impl PartialEqSpecImpl for Number {
+    open spec fn obeys_eq_spec() -> bool
+    {
+        false
+    }
+
+    open spec fn eq_spec(&self, other: &Self) -> bool
+    {
+        *self == *other
+    }
+}
+
 impl PartialEq for Number {
-    fn eq(&self, other: &Self) -> bool {
+    fn eq(&self, other: &Self) -> (result: bool)
+        ensures
+            match (self@, other@) {
+                (NumberView::Integer(n1), NumberView::Integer(n2)) => result == (n1 == n2),
+                _ => true,
+            },
+    {
+        proof { axiom_bigint_obeys_eq_spec(); }
+
         if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) {
             return a == b;
         }
@@ -554,6 +577,8 @@ impl PartialEq for Number {
     }
 }
 
+}
+
 impl Eq for Number {}
 
 impl Ord for Number {

src/verusspec/bigint.rs

@@ -50,6 +50,23 @@ pub assume_specification[ <BigInt as num_traits::Signed>::is_negative ](x: &BigI
         res == (x@ < 0),
 ;
 
+// PartialEq
+
+pub axiom fn axiom_bigint_obeys_eq_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::PartialEqSpec>::obeys_eq_spec(),
+;
+
+pub axiom fn axiom_bigint_obeys_partial_cmp_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
+;
+
+pub assume_specification[ <BigInt as core::cmp::PartialEq>::eq ](x: &BigInt, y: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ == y@),
+;
+
 // From
 
 pub assume_specification[ <BigInt as core::convert::From<i64>>::from ](i: i64) -> (res: BigInt)

src/verusspec/float.rs

@@ -95,6 +95,13 @@ pub assume_specification [ f64::abs ](f: f64) -> (res: f64)
         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),
+;
+
 pub uninterp spec fn spec_f64_neg_infinity() -> f64;
 
 #[inline]