Verus verification

.gitignore

@@ -54,3 +54,6 @@ bindings/ruby/bin/
 bindings/java/.classpath
 bindings/java/.project
 bindings/java/.settings/
+
+# Emacs temporary files
+*~

Cargo.lock

@@ -598,6 +598,12 @@ dependencies = [
  "zerocopy",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
 [[package]]
 name = "hashbrown"
 version = "0.14.5"
@@ -794,6 +800,16 @@ dependencies = [
  "icu_properties",
 ]
 
+[[package]]
+name = "indexmap"
+version = "1.9.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
+dependencies = [
+ "autocfg",
+ "hashbrown 0.12.3",
+]
+
 [[package]]
 name = "indexmap"
 version = "2.13.0"
@@ -1386,6 +1402,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
  "walkdir",
 ]
 
@@ -1485,7 +1502,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
  "itoa",
  "ryu",
  "serde",
@@ -1641,7 +1658,7 @@ version = "0.25.10+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a82418ca169e235e6c399a84e395ab6debeb3bc90edc959bf0f48647c6a32d1b"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
  "toml_datetime",
  "toml_parser",
  "toml_writer",
@@ -1749,12 +1766,76 @@ version = "0.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
+[[package]]
+name = "verus_builtin"
+version = "0.0.0-2026-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7ab914ab490975465ecb3286edceecb0743c3628ddeefcdf25158683e83e2fe"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "46f1f1ee124e0bcb5cec79836ff015d138ea53bff51839a85b8364cdc8b79232"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "syn 2.0.114",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eadebc1e3b522b32c178fd2fb882e691880ff983415497232c74aa9b72bc0b65"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b824c6405f8e8a063ca4a26fca1f454cb02de0c1c4da685e3e7f1974899129d5"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-03-15-0111"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1694faf01f89e1abc996da7b8d24a4e0d1ebd70147dc659e7a5dd680af696772"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "unicode-ident",
+]
+
 [[package]]
 name = "vsimd"
 version = "0.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
 
+[[package]]
+name = "vstd"
+version = "0.0.0-2026-03-17-2326"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "13bbf59dfaa6a7bcb327412c778a5d2b2c226dc65473a981ae6ec53a04c75aba"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"

Cargo.toml

@@ -14,6 +14,11 @@ license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 repository = "https://github.com/microsoft/regorus"
 keywords = ["interpreter", "no_std", "opa", "policy-as-code", "rego"]
 
+# Enable verification with Verus
+
+[package.metadata.verus]
+verify = true
+
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [lib]
@@ -134,6 +139,9 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.6",
 indexmap = { version = "2.12.1", default-features = false, features = ["serde"], optional = true }
 postcard = { version = "1.1.3", default-features = false, features = ["alloc"], optional = true }
 
+# Use Verus for verification
+vstd = { version = "0.0.0-2026-03-17-2326" }
+
 [dev-dependencies]
 anyhow = "1.0.102"
 cfg-if = "1.0.0"
@@ -214,3 +222,6 @@ doctest=false
 # RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps
 all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] }

src/builtins/numbers.rs

@@ -21,6 +21,8 @@ use anyhow::{bail, Result};
 #[cfg(feature = "std")]
 use rand::RngExt;
 
+use vstd::prelude::*;
+
 pub fn register(m: &mut builtins::BuiltinsMap<&'static str, builtins::BuiltinFcn>) {
     m.insert("abs", (abs, 1));
     m.insert("ceil", (ceil, 1));
@@ -188,3 +190,13 @@ fn intn(span: &Span, params: &[Ref<Expr>], args: &[Value], _strict: bool) -> Res
         _ => Value::Undefined,
     })
 }
+
+// Prove properties with Verus
+
+verus! {
+    proof fn lemma_test_one_plus_one_equals_two()
+        ensures
+            1 + 1 == 2,
+    {
+    }
+}

src/lib.rs

@@ -3,7 +3,9 @@
 
 // Unsafe code should not be used.
 // Hard to reason about correctness, and maintainability.
-#![forbid(unsafe_code)]
+#![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
@@ -125,6 +127,7 @@ mod compiler;
 mod engine;
 mod indexchecker;
 mod interpreter;
+mod verusspec;
 
 pub mod languages {
     #[cfg(feature = "azure_policy")]

src/number.rs

@@ -27,12 +27,29 @@ use num_traits::{One, Signed, ToPrimitive, Zero};
 use serde::ser::Serializer;
 use serde::Serialize;
 
+#[cfg(verus_keep_ghost)]
+use vstd::float::*;
+use vstd::prelude::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::convert::*;
+
 use crate::*;
 
+#[cfg(verus_keep_ghost)]
+use crate::verusspec::bigint::*;
+use crate::verusspec::float::*;
+
+#[verus_verify]
 pub type BigInt = NumBigInt;
 
+verus! { // TODO: Change to #[verus_verify] after PR #2243
 const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53
+}
 
+#[verus_verify]
+#[verus_verify(external_derive)]
 #[derive(Clone)]
 pub enum Number {
     UInt(u64),
@@ -41,7 +58,210 @@ pub enum Number {
     BigInt(Rc<BigInt>),
 }
 
+#[cfg(verus_keep_ghost)]
+verus! {
+
+pub assume_specification[ <Number as Clone>::clone ](n: &Number) -> (res: Number)
+    ensures
+        res == n,
+;
+
+pub enum NumberView {
+    Integer(int),
+    Float(f64),
+}
+
+impl View for Number
+{
+    type V = NumberView;
+
+    open spec fn view(&self) -> NumberView
+    {
+        match self {
+            Number::UInt(n) => NumberView::Integer(n as int),
+            Number::Int(n) => NumberView::Integer(n as int),
+            Number::Float(f) => NumberView::Float(*f),
+            Number::BigInt(b) => NumberView::Integer(b@),
+        }
+    }
+}
+
+pub open spec fn float_to_small_int(value: f64) -> Option<int>
+{
+    if !value.is_finite_spec() ||
+       !spec_f64_fract(value).eq_spec(&0.0f64) ||
+       spec_f64_abs(value) > 9_007_199_254_740_992.0 {
+        None
+    }
+    else if value >= 0.0 {
+        if ieee_float_cast::<u64, f64>(ieee_float_cast::<f64, u64>(value)).eq_spec(&value) {
+            Some(ieee_float_cast::<f64, u64>(value) as int)
+        }
+        else {
+            None
+        }
+    }
+    else {
+        if ieee_float_cast::<i64, f64>(ieee_float_cast::<f64, i64>(value)).eq_spec(&value) {
+            Some(ieee_float_cast::<f64, i64>(value) as int)
+        }
+        else {
+            None
+        }
+    }
+}
+
+impl NumberView {
+    pub open spec fn to_int(&self) -> Option<int>
+    {
+        match *self {
+            Self::Integer(n) => Some(n),
+            Self::Float(f) => float_to_small_int(f),
+        }
+    }
+
+    pub open spec fn to_f64_lossy_ensures(self: Self, f: f64) -> bool
+    {
+        match self {
+            NumberView::Integer(v) =>
+            {
+                ||| 0 <= v <= u64::MAX && f == ieee_float_cast::<u64, f64>(v as u64)
+                ||| i64::MIN <= v <= i64::MAX && f == ieee_float_cast::<i64, f64>(v as i64)
+                ||| 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,
+        }
+    }
+}
+
+impl FromSpecImpl<BigInt> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: BigInt) -> Number;
+}
+
+impl FromSpecImpl<u64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: u64) -> Number;
+}
+
+impl FromSpecImpl<usize> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: usize) -> Number;
+}
+
+impl FromSpecImpl<u128> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: u128) -> Number;
+}
+
+impl FromSpecImpl<i64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: i64) -> Number;
+}
+
+impl FromSpecImpl<i128> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: i128) -> Number;
+}
+
+impl FromSpecImpl<f64> for Number {
+    open spec fn obeys_from_spec() -> bool
+    {
+        false
+    }
+
+    uninterp spec fn from_spec(v: f64) -> Number;
+}
+
+impl PartialEqSpecImpl for Number {
+    open spec fn obeys_eq_spec() -> bool
+    {
+        false
+    }
+
+    open spec fn eq_spec(&self, other: &Self) -> bool
+    {
+        *self == *other
+    }
+}
+
 impl Number {
+    spec fn spec_to_f64_lossy(&self) -> f64
+    {
+        match *self {
+            Number::UInt(v) => ieee_float_cast::<u64, f64>(v),
+            Number::Int(v) => ieee_float_cast::<i64, f64>(v),
+            Number::Float(v) => v,
+            Number::BigInt(v) => {
+                if let Some(f) = <BigInt as ToPrimitiveSpec>::spec_to_f64(&v) {
+                    f
+                } else if v@ < 0 {
+                    spec_f64_neg_infinity()
+                } else {
+                    spec_f64_infinity()
+                }
+            },
+        }
+    }
+}
+
+impl OrdSpecImpl for Number {
+    open spec fn obeys_cmp_spec() -> bool
+    {
+        true
+    }
+
+    closed spec fn cmp_spec(&self, other: &Self) -> Ordering
+    {
+         match (self@.to_int(), other@.to_int()) {
+             (Some(n1), Some(n2)) => n1.cmp_spec(&n2),
+             _ => {
+                 let f1 = self.spec_to_f64_lossy();
+                 let f2 = self.spec_to_f64_lossy();
+                 f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal)
+            },
+        }
+    }
+}
+
+} // end verus!
+
+#[verus_verify]
+impl Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value@),
+    )]
     fn from_bigint_owned(value: BigInt) -> Self {
         if value.is_zero() {
             return Number::Int(0);
@@ -60,6 +280,10 @@ impl Number {
         Number::BigInt(Rc::new(value))
     }
 
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from_i128(value: i128) -> Self {
         if value >= 0 {
             if let Ok(u) = u64::try_from(value) {
@@ -74,6 +298,19 @@ impl Number {
         }
     }
 
+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result matches Some(bi) && bi@ == n,
+                NumberView::Float(f) =>
+                {
+                    match result {
+                        Some(bi) => float_to_small_int(f) == Some(bi@),
+                        None => float_to_small_int(f) is None,
+                    }
+                },
+            },
+    )]
     fn to_bigint_owned(&self) -> Option<BigInt> {
         match self {
             Number::UInt(v) => Some(BigInt::from(*v)),
@@ -83,7 +320,21 @@ impl Number {
         }
     }
 
+    #[verus_spec(result =>
+        ensures
+            match result {
+                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<BigInt> {
+        proof! {
+            axiom_f64_obeys_eq_spec();
+            axiom_f64_obeys_partial_cmp_spec();
+            axiom_f64_ops_deterministic();
+            axiom_f64_comparisons_match_ieee();
+        }
+
         if !value.is_finite() || value.fract() != 0.0 {
             return None;
         }
@@ -94,12 +345,12 @@ impl Number {
 
         if value >= 0.0 {
             let u = value as u64;
-            if (u as f64) == value {
+            if u as f64 == value {
                 return Some(BigInt::from(u));
             }
         } else {
             let i = value as i64;
-            if (i as f64) == value {
+            if i as f64 == value {
                 return Some(BigInt::from(i));
             }
         }
@@ -107,6 +358,17 @@ impl Number {
         None
     }
 
+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result matches Some(bi) && bi@ == n,
+                NumberView::Float(f) =>
+                    match result {
+                        Some(bi) => float_to_small_int(f) == Some(bi@),
+                        None => float_to_small_int(f) is None,
+                    },
+            },
+    )]
     fn to_bigint_rc(&self) -> Option<Rc<BigInt>> {
         match self {
             Number::BigInt(v) => Some(v.clone()),
@@ -114,7 +376,13 @@ impl Number {
         }
     }
 
+    #[verus_spec(result =>
+        ensures
+            self@.to_f64_lossy_ensures(result),
+            result == self.spec_to_f64_lossy(),
+    )]
     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,
@@ -123,15 +391,23 @@ impl Number {
                 if let Some(f) = v.to_f64() {
                     f
                 } else if v.is_negative() {
-                    f64::NEG_INFINITY
+                    f64_neg_infinity()
                 } else {
-                    f64::INFINITY
+                    f64_infinity()
                 }
             }
         }
     }
 
+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(n) => result == (n == 0),
+                NumberView::Float(f) => result == f.eq_spec(&0.0f64),
+            },
+    )]
     fn is_zero(&self) -> bool {
+        proof! { axiom_f64_obeys_eq_spec(); }
         match self {
             Number::UInt(0) | Number::Int(0) => true,
             Number::Float(f) => *f == 0.0,
@@ -140,17 +416,39 @@ impl Number {
         }
     }
 
+    #[verus_spec(result =>
+        requires
+            a@ is Integer,
+            b@ is Integer,
+        ensures
+            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) {
         (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap())
     }
 
+    #[verus_spec(result =>
+        ensures
+            match result@ {
+                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 {
-        if let Some(int) = Self::float_to_small_bigint(value) {
+        if let Some(i) = Self::float_to_small_bigint(value) {
-            return Self::from_bigint_owned(int);
+            return Self::from_bigint_owned(i);
         }
         Number::Float(value)
     }
 
+    #[verus_spec(result =>
+        ensures
+            match self@ {
+                NumberView::Integer(v) => if 0 <= v <= u32::MAX { result == Some(v as u32) } else { result is None },
+                NumberView::Float(_) => result is None,
+            },
+    )]
     fn as_u32(&self) -> Option<u32> {
         match self {
             Number::UInt(v) if *v <= u32::MAX as u64 => Some(*v as u32),
@@ -179,25 +477,45 @@ impl Serialize for Number {
     }
 }
 
+#[verus_verify]
 impl From<BigInt> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value@),
+    )]
     fn from(value: BigInt) -> Self {
         Number::from_bigint_owned(value)
     }
 }
 
+#[verus_verify]
 impl From<u64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from(value: u64) -> Self {
         Number::UInt(value)
     }
 }
 
+#[verus_verify]
 impl From<usize> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from(value: usize) -> Self {
         Number::UInt(value as u64)
     }
 }
 
+#[verus_verify]
 impl From<u128> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from(value: u128) -> Self {
         if let Ok(n) = u64::try_from(value) {
             Number::UInt(n)
@@ -207,19 +525,34 @@ impl From<u128> for Number {
     }
 }
 
+#[verus_verify]
 impl From<i64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from(value: i64) -> Self {
         Number::Int(value)
     }
 }
 
+#[verus_verify]
 impl From<i128> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Integer(value as int),
+    )]
     fn from(value: i128) -> Self {
         Number::from_i128(value)
     }
 }
 
+#[verus_verify]
 impl From<f64> for Number {
+    #[verus_spec(result =>
+        ensures
+            result@ == NumberView::Float(value),
+    )]
     fn from(value: f64) -> Self {
         Number::Float(value)
     }
@@ -287,8 +620,25 @@ impl FromStr for Number {
     }
 }
 
+#[verus_verify]
 impl PartialEq for Number {
+    #[verus_spec(result =>
+        ensures
+            match (self@.to_int(), other@.to_int()) {
+                (Some(n1), Some(n2)) => result == (n1 == n2),
+                _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] {
+                    &&& self@.to_f64_lossy_ensures(f1)
+                    &&& other@.to_f64_lossy_ensures(f2)
+                    &&& 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();
+            axiom_f64_obeys_eq_spec();
+        }
+
         if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) {
             return a == b;
         }
@@ -304,12 +654,31 @@ impl PartialEq for Number {
 
 impl Eq for Number {}
 
+#[verus_verify]
 impl Ord for Number {
+    #[verus_spec(result =>
+         ensures
+             match (self@.to_int(), other@.to_int()) {
+                 (Some(n1), Some(n2)) => result == n1.cmp_spec(&n2),
+                 _ => exists|f1: f64, f2: f64| #![trigger self@.to_f64_lossy_ensures(f1), other@.to_f64_lossy_ensures(f2)] {
+                     &&& self@.to_f64_lossy_ensures(f1)
+                     &&& other@.to_f64_lossy_ensures(f2)
+                     &&& result == f1.partial_cmp_spec(&f2).unwrap_or(Ordering::Equal)
+                },
+            },
+    )]
     fn cmp(&self, other: &Self) -> Ordering {
+        proof! {
+            axiom_f64_obeys_partial_cmp_spec();
+            axiom_bigint_obeys_cmp_spec();
+        }
         if let (Some(a), Some(b)) = (self.to_bigint_owned(), other.to_bigint_owned()) {
             return a.cmp(&b);
         }
 
+        proof! {
+            assume(false);
+        }
         self.to_f64_lossy()
             .partial_cmp(&other.to_f64_lossy())
             .unwrap_or(Ordering::Equal)

src/verusspec/bigint.rs

@@ -0,0 +1,712 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+#[cfg(verus_keep_ghost)]
+use core::cmp::Ordering;
+#[cfg(verus_keep_ghost)]
+use num_bigint::BigInt;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::OrdSpec;
+use vstd::prelude::*;
+
+verus! {
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExNumBigInt(num_bigint::BigInt);
+
+pub assume_specification[ <BigInt as Clone>::clone ](n: &BigInt) -> (res: BigInt)
+    ensures
+        res == n,
+;
+
+#[cfg(verus_keep_ghost)]
+pub trait BigIntAdditionalSpecFns {
+    spec fn view(&self) -> int;
+}
+
+#[cfg(verus_keep_ghost)]
+impl BigIntAdditionalSpecFns for BigInt {
+    uninterp spec fn view(&self) -> int;
+}
+
+// Conditions
+
+pub assume_specification[ <BigInt as num_traits::Zero>::is_zero ](x: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ == 0),
+;
+
+pub assume_specification[ <BigInt as num_traits::Signed>::is_negative ](x: &BigInt) -> (res: bool)
+    ensures
+        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@),
+;
+
+// Ord
+
+pub axiom fn axiom_bigint_obeys_cmp_spec()
+    ensures
+        <BigInt as vstd::std_specs::cmp::OrdSpec>::obeys_cmp_spec(),
+        forall|b1: &BigInt, b2: &BigInt| b1.cmp_spec(b2) == b1@.cmp_spec(&b2@),
+;
+
+pub assume_specification[ <BigInt as core::cmp::Ord>::cmp ](x: &BigInt, y: &BigInt) -> (res: Ordering)
+    ensures
+        res == x@.cmp_spec(&y@),
+;
+
+// From
+
+pub assume_specification[ <BigInt as core::convert::From<i64>>::from ](i: i64) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<i128>>::from ](i: i128) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u64>>::from ](u: u64) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u128>>::from ](u: u128) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+// Negation
+
+pub assume_specification[ <BigInt as core::ops::Neg>::neg ](x: BigInt) -> (y: BigInt)
+    ensures
+        y@ == -x@,
+;
+
+// Addition
+
+pub assume_specification[ <BigInt as core::ops::Add>::add ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&BigInt>>::add ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Add<&BigInt>>::add ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ + (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u8>>::add ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u16>>::add ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u32>>::add ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u64>>::add ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u128>>::add ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i8>>::add ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i16>>::add ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i32>>::add ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i64>>::add ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i128>>::add ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u8>>::add ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u16>>::add ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u32>>::add ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u64>>::add ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u128>>::add ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i8>>::add ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i16>>::add ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i32>>::add ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i64>>::add ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i128>>::add ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+// Subtraction
+
+pub assume_specification[ <BigInt as core::ops::Sub>::sub ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&BigInt>>::sub ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Sub<&BigInt>>::sub ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ - (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u8>>::sub ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u16>>::sub ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u32>>::sub ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u64>>::sub ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u128>>::sub ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i8>>::sub ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i16>>::sub ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i32>>::sub ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i64>>::sub ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i128>>::sub ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u8>>::sub ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u16>>::sub ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u32>>::sub ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u64>>::sub ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u128>>::sub ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i8>>::sub ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i16>>::sub ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i32>>::sub ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i64>>::sub ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i128>>::sub ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+// Multiplication
+
+pub assume_specification[ <BigInt as core::ops::Mul>::mul ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&BigInt>>::mul ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Mul<&BigInt>>::mul ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ * (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u8>>::mul ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u16>>::mul ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u32>>::mul ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u64>>::mul ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u128>>::mul ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i8>>::mul ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i16>>::mul ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i32>>::mul ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i64>>::mul ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i128>>::mul ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&u8>>::mul ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * *y,
+;
+
+// Division
+
+pub assume_specification[ <BigInt as core::ops::Div>::div ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&BigInt>>::div ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Div<&BigInt>>::div ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ / (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u8>>::div ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u16>>::div ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u32>>::div ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u64>>::div ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u128>>::div ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i8>>::div ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i16>>::div ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i32>>::div ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i64>>::div ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i128>>::div ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&u8>>::div ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y as int),
+;
+
+} // end verus!
+
+// Verus's encoding of ToPrimitive relies on an unstable feature
+// `sized_hierarchy`, so we can only talk about it when verifying.
+// So, we wrap it all in `#[cfg(verus_keep_ghost)]`.
+
+#[cfg(verus_keep_ghost)]
+verus! {
+
+// ToPrimitive
+
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(ToPrimitiveSpec via ToPrimitiveSpecImpl)]
+pub trait ExToPrimitive {
+    type ExternalTraitSpecificationFor: num_traits::ToPrimitive;
+
+    spec fn obeys_to_primitive_spec() -> bool;
+
+    spec fn spec_to_int(&self) -> Option<int>;
+
+    fn to_isize(&self) -> (res: Option<isize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(isize::MIN <= n <= isize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i8(&self) -> (res: Option<i8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i8::MIN <= n <= i8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i16(&self) -> (res: Option<i16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i16::MIN <= n <= i16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i32(&self) -> (res: Option<i32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i32::MIN <= n <= i32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i64(&self) -> (res: Option<i64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i64::MIN <= n <= i64::MAX),
+                },
+    ;
+
+    fn to_i128(&self) -> (res: Option<i128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i128::MIN <= n <= i128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_usize(&self) -> (res: Option<usize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(usize::MIN <= n <= usize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u8(&self) -> (res: Option<u8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u8::MIN <= n <= u8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u16(&self) -> (res: Option<u16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u16::MIN <= n <= u16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u32(&self) -> (res: Option<u32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u32::MIN <= n <= u32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u64(&self) -> (res: Option<u64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u64::MIN <= n <= u64::MAX),
+                },
+    ;
+
+    fn to_u128(&self) -> (res: Option<u128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u128::MIN <= n <= u128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f32(&self) -> Option<f32>;
+
+    fn to_f32(&self) -> (res: Option<f32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f32(),
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f64(&self) -> Option<f64>;
+
+    fn to_f64(&self) -> (res: Option<f64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f64(),
+        default_ensures
+            true,
+    ;
+}
+
+impl ToPrimitiveSpecImpl for num_bigint::BigInt
+{
+    open spec fn obeys_to_primitive_spec() -> bool
+    {
+        true
+    }
+
+    open spec fn spec_to_int(&self) -> Option<int>
+    {
+        Some(self@)
+    }
+
+    uninterp spec fn spec_to_f32(&self) -> Option<f32>;
+
+    uninterp spec fn spec_to_f64(&self) -> Option<f64>;
+}
+
+// These are the methods of ToPrimitive that BigInt implements because there is no default in ToPrimitive
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i64 ](x: &BigInt) -> (res: Option<i64>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u64 ](x: &BigInt) -> (res: Option<u64>);
+
+// These are the methods of ToPrimitive that BigInt overrides the defaults for because they'd otherwise be wrong
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i128 ](x: &BigInt) -> (res: Option<i128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u128 ](x: &BigInt) -> (res: Option<u128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f32 ](x: &BigInt) -> (res: Option<f32>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f64 ](x: &BigInt) -> (res: Option<f64>);
+
+} // end verus! hidden by cfg(verus_keep_ghost)

src/verusspec/float.rs

@@ -0,0 +1,122 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+#[cfg(verus_keep_ghost)]
+use vstd::float::*;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialEqIs;
+#[cfg(verus_keep_ghost)]
+use vstd::std_specs::cmp::PartialOrdIs;
+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 axiom fn axiom_f64_comparisons_match_ieee()
+    ensures
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_lt(f2) <==> f1.is_lt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_le(f2) <==> f1.is_le(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_gt(f2) <==> f1.is_gt(&f2),
+        forall|f1: f64, f2: f64| #[trigger] f1.ieee_ge(f2) <==> f1.is_ge(&f2),
+;
+
+pub axiom fn axiom_f64_ops_deterministic()
+    ensures
+        <f64 as vstd::std_specs::ops::NegSpec>::obeys_neg_spec(),
+        <f64 as vstd::std_specs::ops::AddSpec>::obeys_add_spec(),
+        <f64 as vstd::std_specs::ops::SubSpec>::obeys_sub_spec(),
+        <f64 as vstd::std_specs::ops::MulSpec>::obeys_mul_spec(),
+        <f64 as vstd::std_specs::ops::DivSpec>::obeys_div_spec(),
+        forall|n: i8, f: f64| float_cast_spec::<i8, f64>(n, f) ==> f == ieee_float_cast::<i8, f64>(n),
+        forall|n: u8, f: f64| float_cast_spec::<u8, f64>(n, f) ==> f == ieee_float_cast::<u8, f64>(n),
+        forall|n: i8, f: f64| float_cast_spec::<f64, i8>(f, n) ==> n == ieee_float_cast::<f64, i8>(f),
+        forall|n: u8, f: f64| float_cast_spec::<f64, u8>(f, n) ==> n == ieee_float_cast::<f64, u8>(f),
+        forall|n: i16, f: f64| float_cast_spec::<i16, f64>(n, f) ==> f == ieee_float_cast::<i16, f64>(n),
+        forall|n: u16, f: f64| float_cast_spec::<u16, f64>(n, f) ==> f == ieee_float_cast::<u16, f64>(n),
+        forall|n: i16, f: f64| float_cast_spec::<f64, i16>(f, n) ==> n == ieee_float_cast::<f64, i16>(f),
+        forall|n: u16, f: f64| float_cast_spec::<f64, u16>(f, n) ==> n == ieee_float_cast::<f64, u16>(f),
+        forall|n: i32, f: f64| float_cast_spec::<i32, f64>(n, f) ==> f == ieee_float_cast::<i32, f64>(n),
+        forall|n: u32, f: f64| float_cast_spec::<u32, f64>(n, f) ==> f == ieee_float_cast::<u32, f64>(n),
+        forall|n: i32, f: f64| float_cast_spec::<f64, i32>(f, n) ==> n == ieee_float_cast::<f64, i32>(f),
+        forall|n: u32, f: f64| float_cast_spec::<f64, u32>(f, n) ==> n == ieee_float_cast::<f64, u32>(f),
+        forall|n: i64, f: f64| float_cast_spec::<i64, f64>(n, f) ==> f == ieee_float_cast::<i64, f64>(n),
+        forall|n: u64, f: f64| float_cast_spec::<u64, f64>(n, f) ==> f == ieee_float_cast::<u64, f64>(n),
+        forall|n: i64, f: f64| float_cast_spec::<f64, i64>(f, n) ==> n == ieee_float_cast::<f64, i64>(f),
+        forall|n: u64, f: f64| float_cast_spec::<f64, u64>(f, n) ==> n == ieee_float_cast::<f64, u64>(f),
+        forall|n: i128, f: f64| float_cast_spec::<i128, f64>(n, f) ==> f == ieee_float_cast::<i128, f64>(n),
+        forall|n: u128, f: f64| float_cast_spec::<u128, f64>(n, f) ==> f == ieee_float_cast::<u128, f64>(n),
+        forall|n: i128, f: f64| float_cast_spec::<f64, i128>(f, n) ==> n == ieee_float_cast::<f64, i128>(f),
+        forall|n: u128, f: f64| float_cast_spec::<f64, u128>(f, n) ==> n == ieee_float_cast::<f64, u128>(f),
+;
+
+pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool)
+    ensures
+        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
+        f.is_finite_spec(),
+    ensures
+        res == spec_f64_fract(f),
+;
+
+pub uninterp spec fn spec_f64_abs(f: f64) -> f64;
+
+pub assume_specification [ f64::abs ](f: f64) -> (res: f64)
+    requires
+        f.is_finite_spec(),
+    ensures
+        res == spec_f64_abs(f),
+;
+
+pub assume_specification [ f64::is_nan ](f: f64) -> (res: bool)
+    ensures
+        res == f.is_nan_spec(),
+;
+
+pub uninterp spec fn spec_f64_neg_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_neg_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_neg_infinity(),
+{
+    f64::NEG_INFINITY
+}
+
+pub uninterp spec fn spec_f64_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_infinity(),
+{
+    f64::INFINITY
+}
+
+} // end verus!

src/verusspec/mod.rs

@@ -0,0 +1,3 @@
+pub(crate) mod bigint;
+pub(crate) mod float;
+pub(crate) mod utils;

src/verusspec/utils.rs

@@ -0,0 +1,65 @@
+use anyhow::{bail, Result};
+use std::format;
+use std::string::String;
+
+use vstd::prelude::*;
+
+verus! {
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_body]
+pub fn verus_format_helper() -> String
+{
+    format!("who cares")
+}
+
+macro_rules! verus_format {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { format!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { verus_format_helper() }
+        }
+    }
+}
+
+#[allow(dead_code)]
+fn my_test_verus_format(fcn: &'static str, x: u32) -> String
+{
+    verus_format!("The parameters are `{fcn}` and `{x}`")
+}
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExAnyhowError(anyhow::Error);
+
+#[cfg(verus_keep_ghost)]
+#[verifier::external_body]
+pub fn verus_bail_helper<T>() -> Result<T>
+{
+    bail!("who cares")
+}
+
+macro_rules! verus_bail {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { bail!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { return verus_bail_helper(); }
+        }
+    }
+}
+
+#[allow(dead_code)]
+fn my_test_verus_bail(fcn: &'static str, x: u32) -> Result<()>
+{
+    if x > 0 {
+        verus_bail!("Invalid parameters `{}` and `{}`", fcn, x)
+    }
+    Ok(())
+}
+
+} // end verus!