From 6ab452989fed1f06ab1edc4d6adf3fda4b36bd9e Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 3 Mar 2026 14:43:45 -0800
Subject: [PATCH] Proofs about some float operations

---
 Cargo.lock             |  8 +++---
 src/number.rs          | 63 ++++++++++++++++++++++++++++++++++++++----
 src/verusspec/float.rs | 10 +++++++
 3 files changed, 72 insertions(+), 9 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index a6aa618..dbd6854 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1613,11 +1613,11 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
 [[package]]
 name = "verus_builtin"
-version = "0.0.0-2026-02-24-1505"
+version = "0.0.0-2026-03-01-0109"
 
 [[package]]
 name = "verus_builtin_macros"
-version = "0.0.0-2026-02-24-1505"
+version = "0.0.0-2026-03-01-0109"
 dependencies = [
  "proc-macro2 1.0.106",
  "quote 1.0.44",
@@ -1637,7 +1637,7 @@ dependencies = [
 
 [[package]]
 name = "verus_state_machines_macros"
-version = "0.0.0-2026-02-24-1505"
+version = "0.0.0-2026-03-01-0109"
 dependencies = [
  "indexmap 1.9.3",
  "proc-macro2 1.0.106",
@@ -1662,7 +1662,7 @@ checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
 
 [[package]]
 name = "vstd"
-version = "0.0.0-2026-02-24-1505"
+version = "0.0.0-2026-03-01-0109"
 dependencies = [
  "verus_builtin",
  "verus_builtin_macros",
diff --git a/src/number.rs b/src/number.rs
index 15846bb..d5ae5b7 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -28,7 +28,9 @@ use serde::ser::Serializer;
 use serde::Serialize;
 
 use vstd::prelude::*;
+use vstd::float::*;
 use vstd::std_specs::convert::*;
+use vstd::std_specs::cmp::*;
 
 use crate::*;
 use crate::verusspec::bigint::*;
@@ -76,7 +78,10 @@ impl View for Number
 }
 
 impl Number {
-    fn from_bigint_owned(value: BigInt) -> Self {
+    fn from_bigint_owned(value: BigInt) -> (result: Self)
+        ensures
+            result@ == NumberView::Integer(value@),
+    {
         if value.is_zero() {
             return Number::Int(0);
         }
@@ -94,7 +99,10 @@ impl Number {
         Number::BigInt(Rc::new(value))
     }
 
-    fn from_i128(value: i128) -> Self {
+    fn from_i128(value: i128) -> (result: Self)
+        ensures
+            result@ == NumberView::Integer(value as int),
+    {
         if value >= 0 {
             if let Ok(u) = u64::try_from(value) {
                 return Number::UInt(u);
@@ -108,9 +116,43 @@ impl Number {
         }
     }
 
+    spec fn spec_float_to_small_int(value: f64) -> Option<int>
+    {
+        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
+                    },
+            }
+        }
+    }
+
     fn to_bigint_owned(&self) -> (res: Option<BigInt>)
         ensures
-            self@ matches NumberView::Integer(n) ==> res matches Some(b) && b@ == n,
+            match self@ {
+                NumberView::Integer(n) => res matches Some(bi) && bi@ == n,
+                NumberView::Float(f) =>
+                    match Self::spec_float_to_small_int(f) {
+                        Some(n) => res matches Some(bi) && bi@ == n,
+                        None => res is None,
+                    },
+            },
     {
         match self {
             Number::UInt(v) => Some(BigInt::from(*v)),
@@ -120,7 +162,18 @@ impl Number {
         }
     }
 
-    fn float_to_small_bigint(value: f64) -> Option<BigInt> {
+    fn float_to_small_bigint(value: f64) -> (res: Option<BigInt>)
+        ensures
+            match Self::spec_float_to_small_int(value) {
+                Some(i) => res matches Some(bi) && bi@ == i,
+                None => res is None,
+            },
+    {
+        proof {
+            axiom_f64_obeys_eq_spec();
+            axiom_f64_obeys_partial_cmp_spec();
+        }
+
         if !value.is_finite() || value.fract() != 0.0 {
             return None;
         }
@@ -144,7 +197,7 @@ impl Number {
         None
     }
 
-    fn to_bigint_rc(&self) -> Option<Rc<BigInt>> {
+    fn to_bigint_rc(&self) -> (res: Option<Rc<BigInt>>) {
         match self {
             Number::BigInt(v) => Some(v.clone()),
             _ => self.to_bigint_owned().map(Rc::new),
diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs
index 51f8bcb..79919a4 100644
--- a/src/verusspec/float.rs
+++ b/src/verusspec/float.rs
@@ -16,6 +16,16 @@ use vstd::prelude::*;
 
 verus! {
 
+pub axiom fn axiom_f64_obeys_eq_spec()
+    ensures
+        <f64 as vstd::std_specs::cmp::PartialEqSpec>::obeys_eq_spec(),
+;
+
+pub axiom fn axiom_f64_obeys_partial_cmp_spec()
+    ensures
+        <f64 as vstd::std_specs::cmp::PartialOrdSpec>::obeys_partial_cmp_spec(),
+;
+
 pub uninterp spec fn spec_f64_as_u64(f: f64) -> u64;
 
 #[inline]