Specs for conversion to and from float types with as

[jaylorch]

Written by Github Copilot + Claude Opus 4.6

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[Copilot]

Pull request overview

Adds a conservative (nondeterministic) verification model for Rust as casts involving floating-point types by desugaring casts into fresh nondeterministic values constrained by uninterpreted _ensures predicates in vstd::float.

Changes:

• Introduces vstd::float::{src}_as_{dst}_ensures uninterpreted spec predicates for int/float casts.
• Lowers Rust as casts between ints/floats (and f32<->f64) into UnaryOp::NondeterministicCast, then desugars in ast_to_sst into nondet temps + assume of the relevant _ensures predicate.
• Updates VIR plumbing (pruning, triggers, printing, AIR conversion guards) and adds verification tests covering the new behavior.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
source/vstd/float.rs	Adds _as_..._ensures uninterpreted predicates for cast specs (currently f32/f64 targets and Rust primitive integer sources).
source/vir/src/ast.rs	Introduces CastType and UnaryOp::NondeterministicCast.
source/vir/src/ast_util.rs	Adds cast_type_to_type_string used to build _ensures function names.
source/vir/src/def.rs	Adds fn_cast_ensures to construct the vstd::float::{src}_as_{dst}_ensures Fun path.
source/vir/src/ast_to_sst.rs	Desugars NondeterministicCast into nondet temp + assume has_type + assume _ensures(...).
source/rust_verify/src/rust_to_vir_expr.rs	Lowers Rust as casts between ints/floats (and float width changes) into NondeterministicCast.
source/vir/src/prune.rs	Ensures the referenced _ensures functions are marked reachable.
source/vir/src/triggers_auto.rs	Updates auto-trigger term gathering for the new unary op.
source/vir/src/triggers.rs	Allows the new unary op in trigger validation logic.
source/vir/src/sst_util.rs	Adds string rendering for NondeterministicCast.
source/vir/src/sst_to_air.rs	Adds a defensive panic if NondeterministicCast reaches AIR lowering (should be desugared earlier).
source/vir/src/poly.rs	Adds a defensive panic if NondeterministicCast reaches poly phase.
source/vir/src/bitvector_to_air.rs	Adds a defensive panic if NondeterministicCast reaches bitvector lowering.
source/vir/src/interpreter.rs	Marks the new unary op as acceptable in interpreter’s unary-op whitelist.
source/vir/src/heuristics.rs	Treats the new unary op as a no-op for heuristic rewriting.
source/rust_verify_test/tests/float.rs	Adds tests asserting _ensures holds for casts and that repeated casts are nondeterministic.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

You can also share your feedback on Copilot code review. Take the survey.

[Copilot]

Pull request overview

Copilot reviewed 16 out of 16 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

You can also share your feedback on Copilot code review. Take the survey.

[tjhance]

Right now, most nontrivial as-casts are implemented by writing an exec function in vstd and then emitting a call to that function in rust_to_vir. For example, casting an array pointer to a slice is implemented by a function cast_array_ptr_to_slice_ptr which is emitted here.

I'd prefer floating point casts be implemented this way, too. (Unless there's a compelling automation-related reason that requires special VIR logic). This doesn't require any VIR changes, and the specifications are easy to maintain and document.

[Chris-Hawblitzel]

Right now, most nontrivial as-casts are implemented by writing an exec function in vstd and then emitting a call to that function in rust_to_vir. For example, casting an array pointer to a slice is implemented by a function cast_array_ptr_to_slice_ptr which is emitted here.

I'd prefer floating point casts be implemented this way, too. (Unless there's a compelling automation-related reason that requires special VIR logic). This doesn't require any VIR changes, and the specifications are easy to maintain and document.

I agree with this. Since we already have ways to represent nondeterminism in VIR, we don't have to add a new mechanism for nondeterminism to implement floating point casts. We can just do it with function calls, the same way that @tjhance mentioned for pointer casts.

In addition, I would rather not declare a separate function for each cast (u8_as_f32_ensures, u16_as_f32_ensures, etc.), which would become even more unwieldy when support for f16 and f128 is added. Instead, we can use generic functions, and we can build on the trait that is already declared in #2229 to make the type bounds of those generic functions precise.

Specifically, I would recommend starting with the following diff (some of which is taken verbatim from #2229 and some of which is a declaration of a new float_cast function that represents floating point as ) and then update rust_to_vir_expr.rs to translate floating point as into a call to float_cast (following @tjhance 's example of cast_array_ptr_to_slice_ptr):

diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs
index 9d977f09f..0cabcc24e 100644
--- a/source/builtin/src/lib.rs
+++ b/source/builtin/src/lib.rs
@@ -1503,6 +1503,49 @@ impl_binary_op!(SpecShr, spec_shr, Self, [
     isize i8 i16 i32 i64 i128
 ]);
 
+#[cfg_attr(verus_keep_ghost, verifier::sealed)]
+pub trait IeeeFloatCast<To> {
+    // rounding modes:
+    // - to integer: RTZ
+    // - to float: RNE
+    // - to real: no rounding
+    #[cfg(verus_keep_ghost)]
+    #[verifier::spec]
+    fn ieee_cast(self) -> To;
+}
+
+macro_rules! impl_ieee_float_cast {
+    ($from:ty, [$($to:ty)*]) => {
+        $(
+            impl IeeeFloatCast<$to> for $from {
+                #[cfg(verus_keep_ghost)]
+                #[verifier::spec]
+                fn ieee_cast(self) -> $to {
+                    unimplemented!()
+                }
+            }
+        )*
+    }
+}
+
+impl_ieee_float_cast!(f32, [real f64]);
+impl_ieee_float_cast!(f64, [real f32]);
+impl_ieee_float_cast!(real, [f32 f64]);
+impl_ieee_float_cast!(u8, [f32 f64]);
+impl_ieee_float_cast!(u16, [f32 f64]);
+impl_ieee_float_cast!(u32, [f32 f64]);
+impl_ieee_float_cast!(u64, [f32 f64]);
+impl_ieee_float_cast!(u128, [f32 f64]);
+impl_ieee_float_cast!(i8, [f32 f64]);
+impl_ieee_float_cast!(i16, [f32 f64]);
+impl_ieee_float_cast!(i32, [f32 f64]);
+impl_ieee_float_cast!(i64, [f32 f64]);
+impl_ieee_float_cast!(i128, [f32 f64]);
+impl_ieee_float_cast!(f32, [u8 u16 u32 u64 u128]);
+impl_ieee_float_cast!(f32, [i8 i16 i32 i64 i128]);
+impl_ieee_float_cast!(f64, [u8 u16 u32 u64 u128]);
+impl_ieee_float_cast!(f64, [i8 i16 i32 i64 i128]);
+
 #[cfg(verus_keep_ghost)]
 #[verifier::spec]
 #[rustc_diagnostic_item = "verus::verus_builtin::f32_to_bits"]
diff --git a/source/vstd/float.rs b/source/vstd/float.rs
index af9d6d124..78dab1e5c 100644
--- a/source/vstd/float.rs
+++ b/source/vstd/float.rs
@@ -102,4 +102,36 @@ pub assume_specification[ <f64 as Clone>::clone ](f: &f64) -> (res: f64)
         res == f,
 ;
 
+#[verifier::external_trait_specification]
+pub trait ExIeeeFloatCast<To> {
+    type ExternalTraitSpecificationFor: IeeeFloatCast<To>;
+}
+
+#[verifier::external_trait_specification]
+pub trait ExDecimal: Copy {
+    type ExternalTraitSpecificationFor: Decimal;
+}
+
+// TODO: when IEEE float support is merged, this should point to IeeeFloatCast::ieee_cast
+pub uninterp spec fn ieee_float_cast<From: IeeeFloatCast<To>, To: Decimal>(from: From) -> To;
+
+pub uninterp spec fn float_cast_spec<From, To>(from: From, to: To) -> bool;
+
+// Used only for internal Verus translation of "as" operator;
+// this is not meant to be called directly by user code,
+// and it is not actually compiled to executable code
+#[cfg(verus_keep_ghost)]
+#[doc(hidden)]
+#[verifier::external_body]
+#[verifier::when_used_as_spec(ieee_float_cast)]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")]
+pub const fn float_cast<From: Copy + IeeeFloatCast<To>, To: Decimal>(from: From) -> (to: To)
+    ensures
+        float_cast_spec(from, to),
+    opens_invariants none
+    no_unwind
+{
+    To::CONST_DEFAULT
+}
+
 } // verus!

[jaylorch]

Thanks, @tjhance and @Chris-Hawblitzel! How does it look now?

[Chris-Hawblitzel]

There's a lot of repeated code in rust_to_vir_expr.rs across the three cases (int->float, float->int, and float->float) that could be refactored so that the code is shared, but it may be easier for me to just do this myself after the merge rather than going through additional rounds of review. Everything else looks fine.

[jaylorch]

Right now, most nontrivial as-casts are implemented by writing an exec function in vstd and then emitting a call to that function in rust_to_vir. For example, casting an array pointer to a slice is implemented by a function cast_array_ptr_to_slice_ptr which is emitted here.

I'd prefer floating point casts be implemented this way, too. (Unless there's a compelling automation-related reason that requires special VIR logic). This doesn't require any VIR changes, and the specifications are easy to maintain and document.

OK, done.