From 90894aa8e19505fc90f6bd3399fe279ce48c8e69 Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 3 Mar 2026 16:35:05 -0800
Subject: [PATCH] Progress to cargo build success

---
 src/number.rs        | 8 ++++++++
 src/verusspec/mod.rs | 1 +
 2 files changed, 9 insertions(+)

diff --git a/src/number.rs b/src/number.rs
index 9a40aaa..703729a 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -37,6 +37,7 @@ use vstd::std_specs::cmp::*;
 
 use crate::*;
 
+#[cfg(verus_keep_ghost)]
 use crate::verusspec::bigint::*;
 use crate::verusspec::float::*;
 
@@ -335,6 +336,7 @@ impl Serialize for Number {
 
 verus! {
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<BigInt> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -353,6 +355,7 @@ impl From<BigInt> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<u64> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -371,6 +374,7 @@ impl From<u64> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<usize> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -389,6 +393,7 @@ impl From<usize> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<u128> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -411,6 +416,7 @@ impl From<u128> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<i64> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -429,6 +435,7 @@ impl From<i64> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<i128> for Number {
     open spec fn obeys_from_spec() -> bool
     {
@@ -447,6 +454,7 @@ impl From<i128> for Number {
     }
 }
 
+#[cfg(verus_keep_ghost)]
 impl FromSpecImpl<f64> for Number {
     open spec fn obeys_from_spec() -> bool
     {
diff --git a/src/verusspec/mod.rs b/src/verusspec/mod.rs
index 6319b84..3062cb4 100644
--- a/src/verusspec/mod.rs
+++ b/src/verusspec/mod.rs
@@ -1,3 +1,4 @@
+#[cfg(verus_keep_ghost)]
 pub(crate) mod bigint;
 pub(crate) mod float;
 pub(crate) mod utils;