From 5819992d1795aa066b1d96c3df4a47b467e9dea2 Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 3 Mar 2026 16:44:31 -0800
Subject: [PATCH] More progress toward cargo build

---
 src/verusspec/utils.rs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/verusspec/utils.rs b/src/verusspec/utils.rs
index 534318a..a6d0f9c 100644
--- a/src/verusspec/utils.rs
+++ b/src/verusspec/utils.rs
@@ -6,6 +6,7 @@ use vstd::prelude::*;
 
 verus! {
 
+#[cfg(verus_keep_ghost)]
 #[verifier::external_body]
 pub fn verus_format_helper() -> String
 {
@@ -23,15 +24,18 @@ macro_rules! verus_format {
     }
 }
 
+#[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>
 {
@@ -49,10 +53,11 @@ macro_rules! verus_bail {
     }
 }
 
+#[allow(dead_code)]
 fn my_test_verus_bail(fcn: &'static str, x: u32) -> Result<()>
 {
     if x > 0 {
-        verus_bail!(format!("Invalid parameters `{fcn}` and `{x}`").as_str())
+        verus_bail!("Invalid parameters `{}` and `{}`", fcn, x)
     }
     Ok(())
 }