From 00d7dedf83116e79e0c8d72b48cc4d65af53b580 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Wed, 4 Mar 2026 17:25:19 -0800 Subject: [PATCH 1/6] Specs for conversion to and from float types with as --- source/rust_verify/src/rust_to_vir_expr.rs | 26 ++++++ source/rust_verify_test/tests/float.rs | 92 ++++++++++++++++++++++ source/vir/src/ast.rs | 17 ++++ source/vir/src/ast_to_sst.rs | 41 ++++++++++ source/vir/src/ast_util.rs | 7 ++ source/vir/src/bitvector_to_air.rs | 3 + source/vir/src/def.rs | 12 +++ source/vir/src/heuristics.rs | 1 + source/vir/src/interpreter.rs | 2 + source/vir/src/poly.rs | 3 + source/vir/src/prune.rs | 13 +++ source/vir/src/sst_to_air.rs | 3 + source/vir/src/sst_util.rs | 9 +++ source/vir/src/triggers.rs | 4 +- source/vir/src/triggers_auto.rs | 1 + source/vstd/float.rs | 75 ++++++++++++++++++ 16 files changed, 308 insertions(+), 1 deletion(-) diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index dc5153d27d..ae721c5275 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -2217,6 +2217,32 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( expr_vattrs.truncate, ))) } + (TypX::Int(src_range), TypX::Float(dst_bits)) => { + let src = vir::ast::CastType::Int(*src_range); + let dst = vir::ast::CastType::Float(*dst_bits); + let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; + mk_expr(ExprX::Unary(op, source_vir_expr)) + } + (TypX::Float(src_bits), TypX::Int(_dst_range)) => { + let src = vir::ast::CastType::Float(*src_bits); + let dst_range = match &*undecorate_typ(&to_vir_ty) { + TypX::Int(r) => *r, + _ => unreachable!(), + }; + let dst = vir::ast::CastType::Int(dst_range); + let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; + mk_expr(ExprX::Unary(op, source_vir_expr)) + } + (TypX::Float(src_bits), TypX::Float(dst_bits)) if src_bits != dst_bits => { + let src = vir::ast::CastType::Float(*src_bits); + let dst = vir::ast::CastType::Float(*dst_bits); + let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; + mk_expr(ExprX::Unary(op, source_vir_expr)) + } + (TypX::Float(_), TypX::Float(_)) => { + // Same float type, identity cast + Ok(ExprOrPlace::Expr(source_vir_expr)) + } _ => { let to_ty = bctx.types.expr_ty(expr); return err_span( diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 27ce779d50..c25e998d6b 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -49,3 +49,95 @@ test_verify_one_file! { } } => Err(err) => assert_one_fails(err) } + +test_verify_one_file! { + #[test] int_to_f64_cast verus_code! { + fn test_i32_as_f64(n: i32) { + use vstd::float::i32_as_f64_ensures; + let x: f64 = n as f64; + // The ensures predicate should hold for the cast result + assert(i32_as_f64_ensures(n, x)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] int_to_f32_cast verus_code! { + fn test_u32_as_f32(n: u32) { + use vstd::float::u32_as_f32_ensures; + let x: f32 = n as f32; + assert(u32_as_f32_ensures(n, x)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] f64_to_int_cast verus_code! { + fn test_f64_as_u32(f: f64) { + use vstd::float::f64_as_u32_ensures; + let n: u32 = f as u32; + assert(f64_as_u32_ensures(f, n)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] f32_to_int_cast verus_code! { + fn test_f32_as_i64(f: f32) { + use vstd::float::f32_as_i64_ensures; + let n: i64 = f as i64; + assert(f32_as_i64_ensures(f, n)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] float_to_float_cast verus_code! { + fn test_f32_as_f64(f: f32) { + use vstd::float::f32_as_f64_ensures; + let d: f64 = f as f64; + assert(f32_as_f64_ensures(f, d)); + } + + fn test_f64_as_f32(d: f64) { + use vstd::float::f64_as_f32_ensures; + let f: f32 = d as f32; + assert(f64_as_f32_ensures(d, f)); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] cast_nondeterministic_fail ["vstd"] => verus_code! { + fn test_nondeterministic(n: i32) { + let x: f64 = n as f64; + let y: f64 = n as f64; + assert(x == y); // FAILS: each cast is nondeterministic + } + } => Err(err) => assert_one_fails(err) +} + +test_verify_one_file! { + #[test] cast_same_float_identity verus_code! { + fn test_f64_identity(f: f64) { + let g: f64 = f as f64; + assert(f == g); // Same-type cast is identity + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] cast_usize_and_isize verus_code! { + fn test_usize_as_f64(n: usize) { + use vstd::float::usize_as_f64_ensures; + let x: f64 = n as f64; + assert(usize_as_f64_ensures(n, x)); + } + + fn test_f64_as_isize(f: f64) { + use vstd::float::f64_as_isize_ensures; + let n: isize = f as isize; + assert(f64_as_isize_ensures(f, n)); + } + } => Ok(()) +} diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index b9be4c0982..1f3fdea722 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -152,6 +152,16 @@ pub enum IntRange { Char, } +/// Represents a type involved in a nondeterministic cast (int or float). +/// Used by `UnaryOp::NondeterministicCast` to identify the source and destination types. +#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] +pub enum CastType { + /// An integer type, identified by its IntRange + Int(IntRange), + /// A floating-point type, identified by its bit width (32 or 64) + Float(u32), +} + /// Type information relevant to Rust but generally not relevant to the SMT encoding. /// This information is relevant for resolving traits. /// @@ -448,6 +458,13 @@ pub enum UnaryOp { /// Length of an array or slice Length(ArrayKind), + /// Nondeterministic cast (e.g. int to float, float to int, float to float). + /// The result is constrained by an uninterpreted `_ensures` predicate in vstd::float. + /// `src` and `dst` identify the source and destination types. + NondeterministicCast { + src: CastType, + dst: CastType, + }, } /// Which builtin source name does this come from diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs index 3b8cb42d76..e1d81c1160 100644 --- a/source/vir/src/ast_to_sst.rs +++ b/source/vir/src/ast_to_sst.rs @@ -1754,6 +1754,47 @@ pub(crate) fn expr_to_stm_opt( let infer_exp = mk_exp(ExpX::Unary(*op, spec_exp)); Ok((vec![], Maybe::Some(Value::Exp(infer_exp)))) } + ExprX::Unary(UnaryOp::NondeterministicCast { src, dst }, exprr) => { + // Desugar into: + // 1. Evaluate the source expression + // 2. Declare a fresh nondeterministic variable of target type + // 3. Assume has_type for the target + // 4. Assume {src}_as_{dst}_ensures(source_val, result_val) + // 5. Return result_val + let (mut stms, exp) = expr_to_stm_opt(ctx, state, exprr)?; + let exp = to_exp_or_return_never!(exp, stms); + + // Declare fresh nondeterministic temp variable of the target type + let kind = PreLocalDeclKind::Immutable(Immutable(LocalDeclKind::Nondeterministic)); + let (var_ident, result_exp) = + state.declare_temp_var_stm(&expr.span, &expr.typ, kind); + + // Assume the result has the target type + let has_typ_stm = assume_has_typ(&var_ident, &expr.typ, &expr.span); + stms.push(has_typ_stm); + + // Construct the call to the _ensures function + let src_name = crate::ast_util::cast_type_to_type_string(src); + let dst_name = crate::ast_util::cast_type_to_type_string(dst); + let ensures_fun = crate::def::fn_cast_ensures( + &ctx.global.vstd_crate_name, + &src_name, + &dst_name, + ); + let call = ExpX::Call( + CallFun::Fun(ensures_fun, None), + Arc::new(vec![]), + Arc::new(vec![exp, result_exp.clone()]), + ); + let call_exp = + SpannedTyped::new(&expr.span, &Arc::new(TypX::Bool), call); + + // Assume the ensures predicate + let assume_stm = Spanned::new(expr.span.clone(), StmX::Assume(call_exp)); + stms.push(assume_stm); + + Ok((stms, Maybe::Some(Value::Exp(result_exp)))) + } ExprX::Unary(op, exprr) => { let (mut stms, exp) = expr_to_stm_opt(ctx, state, exprr)?; let exp = to_exp_or_return_never!(exp, stms); diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs index 6b362a0103..11c39088e6 100644 --- a/source/vir/src/ast_util.rs +++ b/source/vir/src/ast_util.rs @@ -923,6 +923,13 @@ pub fn int_range_to_type_string(range: &IntRange) -> String { } } +pub fn cast_type_to_type_string(ct: &CastType) -> String { + match ct { + CastType::Int(range) => int_range_to_type_string(range), + CastType::Float(bits) => format!("f{}", bits), + } +} + pub fn typ_to_diagnostic_str(typ: &Typ) -> String { fn typs_to_comma_separated_str(typs: &[Arc]) -> String { typs.iter().map(|t| typ_to_diagnostic_str(t)).collect::>().join(", ") diff --git a/source/vir/src/bitvector_to_air.rs b/source/vir/src/bitvector_to_air.rs index f535fa954a..2b4c639890 100644 --- a/source/vir/src/bitvector_to_air.rs +++ b/source/vir/src/bitvector_to_air.rs @@ -366,6 +366,9 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result { panic!("ArrayLength operation not allowed in bitvector query") } + UnaryOp::NondeterministicCast { .. } => { + panic!("internal error: NondeterministicCast should have been desugared") + } }, ExpX::UnaryOpr(UnaryOpr::Box(_) | UnaryOpr::Unbox(_), exp) => { bv_exp_to_expr(ctx, state, exp) diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index 6f966d849d..09e43d9e2e 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -431,6 +431,18 @@ pub fn strslice_type() -> Path { Arc::new(PathX { krate: None, segments: Arc::new(vec![ident]) }) } +pub fn fn_cast_ensures(vstd_crate_name: &Ident, src_name: &str, dst_name: &str) -> Fun { + Arc::new(FunX { + path: Arc::new(PathX { + krate: Some(vstd_crate_name.clone()), + segments: Arc::new(vec![ + Arc::new("float".to_string()), + Arc::new(format!("{}_as_{}_ensures", src_name, dst_name)), + ]), + }), + }) +} + pub fn fn_slice_len(vstd_crate_name: &Ident) -> Fun { Arc::new(FunX { path: Arc::new(PathX { diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs index a264cff7aa..a6ff53138e 100644 --- a/source/vir/src/heuristics.rs +++ b/source/vir/src/heuristics.rs @@ -58,6 +58,7 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp { UnaryOp::RealToInt => exp.clone(), UnaryOp::StrLen | UnaryOp::StrIsAscii | UnaryOp::Length(_) => exp.clone(), UnaryOp::InferSpecForLoopIter { .. } => exp.clone(), + UnaryOp::NondeterministicCast { .. } => exp.clone(), UnaryOp::Trigger(_) | UnaryOp::CoerceMode { .. } | UnaryOp::MustBeFinalized diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs index 42500b2ff0..720981cbf5 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -1182,6 +1182,7 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result ok, MustBeFinalized | UnaryOp::MustBeElaborated => { panic!("Found MustBeFinalized op {:?} after calling finalize_exp", exp) @@ -1302,6 +1303,7 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result ok, } } diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs index ad8a40e0c6..92c1cab33e 100644 --- a/source/vir/src/poly.rs +++ b/source/vir/src/poly.rs @@ -595,6 +595,9 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { UnaryOp::MutRefFinal(_) => { panic!("internal error: MustBeFinalized in SST") } + UnaryOp::NondeterministicCast { .. } => { + panic!("internal error: NondeterministicCast should have been desugared") + } } } ExpX::UnaryOpr(op, e1) => { diff --git a/source/vir/src/prune.rs b/source/vir/src/prune.rs index 232282ddf0..89146caf98 100644 --- a/source/vir/src/prune.rs +++ b/source/vir/src/prune.rs @@ -514,6 +514,19 @@ fn traverse_reachable(ctxt: &Ctxt, state: &mut State) { ExprX::Unary(UnaryOp::Length(ArrayKind::Slice), _) => { reach_function(ctxt, state, &fn_slice_len(&ctxt.vstd_crate_name)); } + ExprX::Unary( + UnaryOp::NondeterministicCast { src, dst }, + _, + ) => { + let src_name = crate::ast_util::cast_type_to_type_string(src); + let dst_name = crate::ast_util::cast_type_to_type_string(dst); + let fun = crate::def::fn_cast_ensures( + &ctxt.vstd_crate_name, + &src_name, + &dst_name, + ); + reach_function(ctxt, state, &fun); + } ExprX::Binary(BinaryOp::Index(ArrayKind::Slice, bounds_check), _, _) => { reach_function(ctxt, state, &fn_slice_index(&ctxt.vstd_crate_name)); if *bounds_check != BoundsCheck::Allow { diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 13874375ee..004e3bcdc6 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1096,6 +1096,9 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< UnaryOp::MutRefFinal(_) => { panic!("internal error: MutRefFinal should have been removed before here") } + UnaryOp::NondeterministicCast { .. } => { + panic!("internal error: NondeterministicCast should have been desugared in ast_to_sst") + } UnaryOp::Length(kind) => { let typ = undecorate_typ(&e.typ); let typ = match &*typ { diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs index ff7edad5b2..7b8fdea8ff 100644 --- a/source/vir/src/sst_util.rs +++ b/source/vir/src/sst_util.rs @@ -486,6 +486,15 @@ impl ExpX { UnaryOp::Length(_kind) => { (format!("length({})", exp.x.to_string_prec(global, 99)), 0) } + UnaryOp::NondeterministicCast { src, dst } => ( + format!( + "nondeterministic_cast::<{}, {}>({})", + crate::ast_util::cast_type_to_type_string(src), + crate::ast_util::cast_type_to_type_string(dst), + exp.x.to_user_string(global) + ), + 99, + ), }, UnaryOpr(op, exp) => { use crate::ast::UnaryOpr::*; diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs index 27455a99de..a7954cdc26 100644 --- a/source/vir/src/triggers.rs +++ b/source/vir/src/triggers.rs @@ -132,6 +132,7 @@ fn check_trigger_expr_arg(state: &mut State, arg: &Exp) { | UnaryOp::MutRefFuture(_) | UnaryOp::MutRefFinal(_) | UnaryOp::Length(_) + | UnaryOp::NondeterministicCast { .. } | UnaryOp::InferSpecForLoopIter { .. } => {} }, ExpX::UnaryOpr(op, arg) => match op { @@ -280,7 +281,8 @@ fn check_trigger_expr( | UnaryOp::CoerceMode { .. } | UnaryOp::MustBeFinalized | UnaryOp::MustBeElaborated - | UnaryOp::CastToInteger => Ok(()), + | UnaryOp::CastToInteger + | UnaryOp::NondeterministicCast { .. } => Ok(()), UnaryOp::InferSpecForLoopIter { .. } => { Err(error(&exp.span, "triggers cannot contain loop spec inference")) } diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs index d2794723d0..1765475bf5 100644 --- a/source/vir/src/triggers_auto.rs +++ b/source/vir/src/triggers_auto.rs @@ -417,6 +417,7 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter UnaryOp::InferSpecForLoopIter { .. } => 1, UnaryOp::StrIsAscii | UnaryOp::StrLen => fail_on_strop(), UnaryOp::MutRefFinal(_) => 1, + UnaryOp::NondeterministicCast { .. } => 0, UnaryOp::MutRefCurrent | UnaryOp::MutRefFuture(_) => unreachable!(), }; let (is_pure1, term1) = gather_terms(ctxt, ctx, e1, depth); diff --git a/source/vstd/float.rs b/source/vstd/float.rs index af9d6d1243..03fd3e83c7 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -102,4 +102,79 @@ pub assume_specification[ ::clone ](f: &f64) -> (res: f64) res == f, ; +// Nondeterministic cast specification functions. +// Each `{src}_as_{dst}_ensures(input, output)` predicate constrains the result +// of the Rust `as` cast `input as {dst}`. Because float casts involve rounding +// and platform-dependent behavior, each cast produces a nondeterministic result +// constrained only by this uninterpreted predicate. Users can supply axioms +// about these predicates to reason about specific rounding modes or exactness. +// +// This follows the same pattern as `add_ensures`, `sub_ensures`, etc. for +// float arithmetic. + +// --- Integer to f32 --- + +pub uninterp spec fn u8_as_f32_ensures(i: u8, o: f32) -> bool; +pub uninterp spec fn u16_as_f32_ensures(i: u16, o: f32) -> bool; +pub uninterp spec fn u32_as_f32_ensures(i: u32, o: f32) -> bool; +pub uninterp spec fn u64_as_f32_ensures(i: u64, o: f32) -> bool; +pub uninterp spec fn u128_as_f32_ensures(i: u128, o: f32) -> bool; +pub uninterp spec fn usize_as_f32_ensures(i: usize, o: f32) -> bool; +pub uninterp spec fn i8_as_f32_ensures(i: i8, o: f32) -> bool; +pub uninterp spec fn i16_as_f32_ensures(i: i16, o: f32) -> bool; +pub uninterp spec fn i32_as_f32_ensures(i: i32, o: f32) -> bool; +pub uninterp spec fn i64_as_f32_ensures(i: i64, o: f32) -> bool; +pub uninterp spec fn i128_as_f32_ensures(i: i128, o: f32) -> bool; +pub uninterp spec fn isize_as_f32_ensures(i: isize, o: f32) -> bool; + +// --- Integer to f64 --- + +pub uninterp spec fn u8_as_f64_ensures(i: u8, o: f64) -> bool; +pub uninterp spec fn u16_as_f64_ensures(i: u16, o: f64) -> bool; +pub uninterp spec fn u32_as_f64_ensures(i: u32, o: f64) -> bool; +pub uninterp spec fn u64_as_f64_ensures(i: u64, o: f64) -> bool; +pub uninterp spec fn u128_as_f64_ensures(i: u128, o: f64) -> bool; +pub uninterp spec fn usize_as_f64_ensures(i: usize, o: f64) -> bool; +pub uninterp spec fn i8_as_f64_ensures(i: i8, o: f64) -> bool; +pub uninterp spec fn i16_as_f64_ensures(i: i16, o: f64) -> bool; +pub uninterp spec fn i32_as_f64_ensures(i: i32, o: f64) -> bool; +pub uninterp spec fn i64_as_f64_ensures(i: i64, o: f64) -> bool; +pub uninterp spec fn i128_as_f64_ensures(i: i128, o: f64) -> bool; +pub uninterp spec fn isize_as_f64_ensures(i: isize, o: f64) -> bool; + +// --- f32 to integer --- + +pub uninterp spec fn f32_as_u8_ensures(f: f32, o: u8) -> bool; +pub uninterp spec fn f32_as_u16_ensures(f: f32, o: u16) -> bool; +pub uninterp spec fn f32_as_u32_ensures(f: f32, o: u32) -> bool; +pub uninterp spec fn f32_as_u64_ensures(f: f32, o: u64) -> bool; +pub uninterp spec fn f32_as_u128_ensures(f: f32, o: u128) -> bool; +pub uninterp spec fn f32_as_usize_ensures(f: f32, o: usize) -> bool; +pub uninterp spec fn f32_as_i8_ensures(f: f32, o: i8) -> bool; +pub uninterp spec fn f32_as_i16_ensures(f: f32, o: i16) -> bool; +pub uninterp spec fn f32_as_i32_ensures(f: f32, o: i32) -> bool; +pub uninterp spec fn f32_as_i64_ensures(f: f32, o: i64) -> bool; +pub uninterp spec fn f32_as_i128_ensures(f: f32, o: i128) -> bool; +pub uninterp spec fn f32_as_isize_ensures(f: f32, o: isize) -> bool; + +// --- f64 to integer --- + +pub uninterp spec fn f64_as_u8_ensures(f: f64, o: u8) -> bool; +pub uninterp spec fn f64_as_u16_ensures(f: f64, o: u16) -> bool; +pub uninterp spec fn f64_as_u32_ensures(f: f64, o: u32) -> bool; +pub uninterp spec fn f64_as_u64_ensures(f: f64, o: u64) -> bool; +pub uninterp spec fn f64_as_u128_ensures(f: f64, o: u128) -> bool; +pub uninterp spec fn f64_as_usize_ensures(f: f64, o: usize) -> bool; +pub uninterp spec fn f64_as_i8_ensures(f: f64, o: i8) -> bool; +pub uninterp spec fn f64_as_i16_ensures(f: f64, o: i16) -> bool; +pub uninterp spec fn f64_as_i32_ensures(f: f64, o: i32) -> bool; +pub uninterp spec fn f64_as_i64_ensures(f: f64, o: i64) -> bool; +pub uninterp spec fn f64_as_i128_ensures(f: f64, o: i128) -> bool; +pub uninterp spec fn f64_as_isize_ensures(f: f64, o: isize) -> bool; + +// --- Float to float --- + +pub uninterp spec fn f32_as_f64_ensures(f: f32, o: f64) -> bool; +pub uninterp spec fn f64_as_f32_ensures(f: f64, o: f32) -> bool; + } // verus! From 66b3e9d42dffaffee8f7771213d04b8222f12283 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Wed, 4 Mar 2026 17:26:55 -0800 Subject: [PATCH 2/6] Apply verusfmt formatting --- source/vir/src/ast_to_sst.rs | 13 +++------ source/vir/src/prune.rs | 5 +--- source/vir/src/sst_to_air.rs | 4 ++- source/vstd/float.rs | 51 +++++++++++++++++++++++++++++++----- 4 files changed, 53 insertions(+), 20 deletions(-) diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs index e1d81c1160..916513050a 100644 --- a/source/vir/src/ast_to_sst.rs +++ b/source/vir/src/ast_to_sst.rs @@ -1766,8 +1766,7 @@ pub(crate) fn expr_to_stm_opt( // Declare fresh nondeterministic temp variable of the target type let kind = PreLocalDeclKind::Immutable(Immutable(LocalDeclKind::Nondeterministic)); - let (var_ident, result_exp) = - state.declare_temp_var_stm(&expr.span, &expr.typ, kind); + let (var_ident, result_exp) = state.declare_temp_var_stm(&expr.span, &expr.typ, kind); // Assume the result has the target type let has_typ_stm = assume_has_typ(&var_ident, &expr.typ, &expr.span); @@ -1776,18 +1775,14 @@ pub(crate) fn expr_to_stm_opt( // Construct the call to the _ensures function let src_name = crate::ast_util::cast_type_to_type_string(src); let dst_name = crate::ast_util::cast_type_to_type_string(dst); - let ensures_fun = crate::def::fn_cast_ensures( - &ctx.global.vstd_crate_name, - &src_name, - &dst_name, - ); + let ensures_fun = + crate::def::fn_cast_ensures(&ctx.global.vstd_crate_name, &src_name, &dst_name); let call = ExpX::Call( CallFun::Fun(ensures_fun, None), Arc::new(vec![]), Arc::new(vec![exp, result_exp.clone()]), ); - let call_exp = - SpannedTyped::new(&expr.span, &Arc::new(TypX::Bool), call); + let call_exp = SpannedTyped::new(&expr.span, &Arc::new(TypX::Bool), call); // Assume the ensures predicate let assume_stm = Spanned::new(expr.span.clone(), StmX::Assume(call_exp)); diff --git a/source/vir/src/prune.rs b/source/vir/src/prune.rs index 89146caf98..c0cbb92215 100644 --- a/source/vir/src/prune.rs +++ b/source/vir/src/prune.rs @@ -514,10 +514,7 @@ fn traverse_reachable(ctxt: &Ctxt, state: &mut State) { ExprX::Unary(UnaryOp::Length(ArrayKind::Slice), _) => { reach_function(ctxt, state, &fn_slice_len(&ctxt.vstd_crate_name)); } - ExprX::Unary( - UnaryOp::NondeterministicCast { src, dst }, - _, - ) => { + ExprX::Unary(UnaryOp::NondeterministicCast { src, dst }, _) => { let src_name = crate::ast_util::cast_type_to_type_string(src); let dst_name = crate::ast_util::cast_type_to_type_string(dst); let fun = crate::def::fn_cast_ensures( diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 004e3bcdc6..73301344e7 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1097,7 +1097,9 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< panic!("internal error: MutRefFinal should have been removed before here") } UnaryOp::NondeterministicCast { .. } => { - panic!("internal error: NondeterministicCast should have been desugared in ast_to_sst") + panic!( + "internal error: NondeterministicCast should have been desugared in ast_to_sst" + ) } UnaryOp::Length(kind) => { let typ = undecorate_typ(&e.typ); diff --git a/source/vstd/float.rs b/source/vstd/float.rs index 03fd3e83c7..b76667f3d9 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -111,70 +111,109 @@ pub assume_specification[ ::clone ](f: &f64) -> (res: f64) // // This follows the same pattern as `add_ensures`, `sub_ensures`, etc. for // float arithmetic. - // --- Integer to f32 --- - pub uninterp spec fn u8_as_f32_ensures(i: u8, o: f32) -> bool; + pub uninterp spec fn u16_as_f32_ensures(i: u16, o: f32) -> bool; + pub uninterp spec fn u32_as_f32_ensures(i: u32, o: f32) -> bool; + pub uninterp spec fn u64_as_f32_ensures(i: u64, o: f32) -> bool; + pub uninterp spec fn u128_as_f32_ensures(i: u128, o: f32) -> bool; + pub uninterp spec fn usize_as_f32_ensures(i: usize, o: f32) -> bool; + pub uninterp spec fn i8_as_f32_ensures(i: i8, o: f32) -> bool; + pub uninterp spec fn i16_as_f32_ensures(i: i16, o: f32) -> bool; + pub uninterp spec fn i32_as_f32_ensures(i: i32, o: f32) -> bool; + pub uninterp spec fn i64_as_f32_ensures(i: i64, o: f32) -> bool; + pub uninterp spec fn i128_as_f32_ensures(i: i128, o: f32) -> bool; + pub uninterp spec fn isize_as_f32_ensures(i: isize, o: f32) -> bool; // --- Integer to f64 --- - pub uninterp spec fn u8_as_f64_ensures(i: u8, o: f64) -> bool; + pub uninterp spec fn u16_as_f64_ensures(i: u16, o: f64) -> bool; + pub uninterp spec fn u32_as_f64_ensures(i: u32, o: f64) -> bool; + pub uninterp spec fn u64_as_f64_ensures(i: u64, o: f64) -> bool; + pub uninterp spec fn u128_as_f64_ensures(i: u128, o: f64) -> bool; + pub uninterp spec fn usize_as_f64_ensures(i: usize, o: f64) -> bool; + pub uninterp spec fn i8_as_f64_ensures(i: i8, o: f64) -> bool; + pub uninterp spec fn i16_as_f64_ensures(i: i16, o: f64) -> bool; + pub uninterp spec fn i32_as_f64_ensures(i: i32, o: f64) -> bool; + pub uninterp spec fn i64_as_f64_ensures(i: i64, o: f64) -> bool; + pub uninterp spec fn i128_as_f64_ensures(i: i128, o: f64) -> bool; + pub uninterp spec fn isize_as_f64_ensures(i: isize, o: f64) -> bool; // --- f32 to integer --- - pub uninterp spec fn f32_as_u8_ensures(f: f32, o: u8) -> bool; + pub uninterp spec fn f32_as_u16_ensures(f: f32, o: u16) -> bool; + pub uninterp spec fn f32_as_u32_ensures(f: f32, o: u32) -> bool; + pub uninterp spec fn f32_as_u64_ensures(f: f32, o: u64) -> bool; + pub uninterp spec fn f32_as_u128_ensures(f: f32, o: u128) -> bool; + pub uninterp spec fn f32_as_usize_ensures(f: f32, o: usize) -> bool; + pub uninterp spec fn f32_as_i8_ensures(f: f32, o: i8) -> bool; + pub uninterp spec fn f32_as_i16_ensures(f: f32, o: i16) -> bool; + pub uninterp spec fn f32_as_i32_ensures(f: f32, o: i32) -> bool; + pub uninterp spec fn f32_as_i64_ensures(f: f32, o: i64) -> bool; + pub uninterp spec fn f32_as_i128_ensures(f: f32, o: i128) -> bool; + pub uninterp spec fn f32_as_isize_ensures(f: f32, o: isize) -> bool; // --- f64 to integer --- - pub uninterp spec fn f64_as_u8_ensures(f: f64, o: u8) -> bool; + pub uninterp spec fn f64_as_u16_ensures(f: f64, o: u16) -> bool; + pub uninterp spec fn f64_as_u32_ensures(f: f64, o: u32) -> bool; + pub uninterp spec fn f64_as_u64_ensures(f: f64, o: u64) -> bool; + pub uninterp spec fn f64_as_u128_ensures(f: f64, o: u128) -> bool; + pub uninterp spec fn f64_as_usize_ensures(f: f64, o: usize) -> bool; + pub uninterp spec fn f64_as_i8_ensures(f: f64, o: i8) -> bool; + pub uninterp spec fn f64_as_i16_ensures(f: f64, o: i16) -> bool; + pub uninterp spec fn f64_as_i32_ensures(f: f64, o: i32) -> bool; + pub uninterp spec fn f64_as_i64_ensures(f: f64, o: i64) -> bool; + pub uninterp spec fn f64_as_i128_ensures(f: f64, o: i128) -> bool; + pub uninterp spec fn f64_as_isize_ensures(f: f64, o: isize) -> bool; // --- Float to float --- - pub uninterp spec fn f32_as_f64_ensures(f: f32, o: f64) -> bool; + pub uninterp spec fn f64_as_f32_ensures(f: f64, o: f32) -> bool; } // verus! From ef5607eb0ee1e96e909f2af9ffc1e7eb5ad51f59 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Wed, 4 Mar 2026 18:13:37 -0800 Subject: [PATCH 3/6] Useful error messages for unsupported casts --- source/rust_verify/src/rust_to_vir_expr.rs | 50 +++++++++++++++++++++- source/rust_verify_test/tests/float.rs | 45 +++++++++++++++++++ source/vir/src/ast.rs | 2 +- source/vir/src/ast_to_sst.rs | 9 ++++ 4 files changed, 104 insertions(+), 2 deletions(-) diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index ae721c5275..128f99ec00 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -2218,22 +2218,70 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( ))) } (TypX::Int(src_range), TypX::Float(dst_bits)) => { + match src_range { + IntRange::Int | IntRange::Nat | IntRange::Char => { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `{}` to `f{}`", + vir::ast_util::int_range_to_type_string(src_range), + dst_bits, + ), + ); + } + _ => {} + } + if *dst_bits != 32 && *dst_bits != 64 { + return err_span( + expr.span, + format!("Verus does not support `as` cast to `f{}`", dst_bits,), + ); + } let src = vir::ast::CastType::Int(*src_range); let dst = vir::ast::CastType::Float(*dst_bits); let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; mk_expr(ExprX::Unary(op, source_vir_expr)) } (TypX::Float(src_bits), TypX::Int(_dst_range)) => { - let src = vir::ast::CastType::Float(*src_bits); let dst_range = match &*undecorate_typ(&to_vir_ty) { TypX::Int(r) => *r, _ => unreachable!(), }; + match dst_range { + IntRange::Int | IntRange::Nat | IntRange::Char => { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `f{}` to `{}`", + src_bits, + vir::ast_util::int_range_to_type_string(&dst_range), + ), + ); + } + _ => {} + } + if *src_bits != 32 && *src_bits != 64 { + return err_span( + expr.span, + format!("Verus does not support `as` cast from `f{}`", src_bits,), + ); + } + let src = vir::ast::CastType::Float(*src_bits); let dst = vir::ast::CastType::Int(dst_range); let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; mk_expr(ExprX::Unary(op, source_vir_expr)) } (TypX::Float(src_bits), TypX::Float(dst_bits)) if src_bits != dst_bits => { + if (*src_bits != 32 && *src_bits != 64) || (*dst_bits != 32 && *dst_bits != 64) + { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `f{}` to `f{}`", + src_bits, dst_bits, + ), + ); + } let src = vir::ast::CastType::Float(*src_bits); let dst = vir::ast::CastType::Float(*dst_bits); let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index c25e998d6b..2e18fadbfc 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -141,3 +141,48 @@ test_verify_one_file! { } } => Ok(()) } + +test_verify_one_file_with_options! { + #[test] cast_int_to_f16_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_i32_as_f16(n: i32) { + let y: f16 = n as f16; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast to `f16`") +} + +test_verify_one_file_with_options! { + #[test] cast_f16_to_int_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_f16_as_i32(f: f16) { + let n: i32 = f as i32; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f16`") +} + +test_verify_one_file_with_options! { + #[test] cast_f16_to_f64_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_f16_as_f64(f: f16) { + let d: f64 = f as f64; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f16` to `f64`") +} diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index 1f3fdea722..0318e93f08 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -158,7 +158,7 @@ pub enum IntRange { pub enum CastType { /// An integer type, identified by its IntRange Int(IntRange), - /// A floating-point type, identified by its bit width (32 or 64) + /// A floating-point type, identified by its bit width (e.g., 32 or 64) Float(u32), } diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs index 916513050a..92ae7a9e9d 100644 --- a/source/vir/src/ast_to_sst.rs +++ b/source/vir/src/ast_to_sst.rs @@ -1777,6 +1777,15 @@ pub(crate) fn expr_to_stm_opt( let dst_name = crate::ast_util::cast_type_to_type_string(dst); let ensures_fun = crate::def::fn_cast_ensures(&ctx.global.vstd_crate_name, &src_name, &dst_name); + if !ctx.func_map.contains_key(&ensures_fun) { + return Err(crate::messages::error( + &expr.span, + format!( + "Verus does not support `as` cast from `{}` to `{}` (no specification function `{}_as_{}_ensures` found in vstd::float)", + src_name, dst_name, src_name, dst_name, + ), + )); + } let call = ExpX::Call( CallFun::Fun(ensures_fun, None), Arc::new(vec![]), From 0888bf084d2743566c1273519dbf3feb3fb2d2de Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 9 Mar 2026 14:37:41 -0700 Subject: [PATCH 4/6] Use Chris's approach, modulo const in float_cast --- source/builtin/src/lib.rs | 43 +++++++ source/rust_verify/src/rust_to_vir_expr.rs | 94 +++++++++++--- source/rust_verify/src/verus_items.rs | 2 + source/rust_verify_test/tests/float.rs | 36 +++--- source/vir/src/ast.rs | 17 --- source/vir/src/ast_to_sst.rs | 45 ------- source/vir/src/ast_util.rs | 7 -- source/vir/src/bitvector_to_air.rs | 3 - source/vir/src/def.rs | 12 -- source/vir/src/heuristics.rs | 1 - source/vir/src/interpreter.rs | 2 - source/vir/src/poly.rs | 3 - source/vir/src/prune.rs | 10 -- source/vir/src/sst_to_air.rs | 5 - source/vir/src/sst_util.rs | 9 -- source/vir/src/triggers.rs | 4 +- source/vir/src/triggers_auto.rs | 1 - source/vstd/float.rs | 136 ++++----------------- 18 files changed, 169 insertions(+), 261 deletions(-) diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs index 9d977f09fa..0cabcc24e3 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 { + // 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/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 128f99ec00..5f40aa55a4 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -2219,7 +2219,11 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( } (TypX::Int(src_range), TypX::Float(dst_bits)) => { match src_range { - IntRange::Int | IntRange::Nat | IntRange::Char => { + IntRange::Int + | IntRange::Nat + | IntRange::Char + | IntRange::USize + | IntRange::ISize => { return err_span( expr.span, format!( @@ -2234,13 +2238,31 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( if *dst_bits != 32 && *dst_bits != 64 { return err_span( expr.span, - format!("Verus does not support `as` cast to `f{}`", dst_bits,), + format!("Verus does not support `as` cast to `f{}`", dst_bits), ); } - let src = vir::ast::CastType::Int(*src_range); - let dst = vir::ast::CastType::Float(*dst_bits); - let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; - mk_expr(ExprX::Unary(op, source_vir_expr)) + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) } (TypX::Float(src_bits), TypX::Int(_dst_range)) => { let dst_range = match &*undecorate_typ(&to_vir_ty) { @@ -2248,7 +2270,11 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( _ => unreachable!(), }; match dst_range { - IntRange::Int | IntRange::Nat | IntRange::Char => { + IntRange::Int + | IntRange::Nat + | IntRange::Char + | IntRange::USize + | IntRange::ISize => { return err_span( expr.span, format!( @@ -2263,13 +2289,31 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( if *src_bits != 32 && *src_bits != 64 { return err_span( expr.span, - format!("Verus does not support `as` cast from `f{}`", src_bits,), + format!("Verus does not support `as` cast from `f{}`", src_bits), ); } - let src = vir::ast::CastType::Float(*src_bits); - let dst = vir::ast::CastType::Int(dst_range); - let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; - mk_expr(ExprX::Unary(op, source_vir_expr)) + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) } (TypX::Float(src_bits), TypX::Float(dst_bits)) if src_bits != dst_bits => { if (*src_bits != 32 && *src_bits != 64) || (*dst_bits != 32 && *dst_bits != 64) @@ -2282,10 +2326,28 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( ), ); } - let src = vir::ast::CastType::Float(*src_bits); - let dst = vir::ast::CastType::Float(*dst_bits); - let op = vir::ast::UnaryOp::NondeterministicCast { src, dst }; - mk_expr(ExprX::Unary(op, source_vir_expr)) + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) } (TypX::Float(_), TypX::Float(_)) => { // Same float type, identity cast diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index fd28abcf17..acdb23ef1f 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -324,6 +324,7 @@ pub(crate) enum VstdItem { CastSlicePtrToStrPtr, CastStrPtrToSlicePtr, CastPtrToUsize, + FloatCast, RefMutArrayUnsizingCoercion, VecIndex, VecIndexMut, @@ -607,6 +608,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { ("verus::vstd::raw_ptr::cast_str_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastStrPtrToSlicePtr, Some(Arc::new("raw_ptr::cast_str_ptr_to_slice_ptr".to_owned())))), ("verus::vstd::raw_ptr::cast_ptr_to_usize", VerusItem::Vstd(VstdItem::CastPtrToUsize, Some(Arc::new("raw_ptr::cast_ptr_to_usize".to_owned())))), ("verus::vstd::raw_ptr::SharedReference", VerusItem::Vstd(VstdItem::SharedReference, Some(Arc::new("raw_ptr::SharedReference".to_owned())))), + ("verus::vstd::float::float_cast", VerusItem::Vstd(VstdItem::FloatCast, Some(Arc::new("float::float_cast".to_owned())))), // SeqFn(vir::interpreter::SeqFn::Last ))), ("verus::verus_builtin::Structural", VerusItem::Marker(MarkerItem::Structural)), diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 2e18fadbfc..e3497e466c 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -53,10 +53,10 @@ test_verify_one_file! { test_verify_one_file! { #[test] int_to_f64_cast verus_code! { fn test_i32_as_f64(n: i32) { - use vstd::float::i32_as_f64_ensures; + use vstd::float::float_cast_spec; let x: f64 = n as f64; // The ensures predicate should hold for the cast result - assert(i32_as_f64_ensures(n, x)); + assert(float_cast_spec(n, x)); } } => Ok(()) } @@ -64,9 +64,9 @@ test_verify_one_file! { test_verify_one_file! { #[test] int_to_f32_cast verus_code! { fn test_u32_as_f32(n: u32) { - use vstd::float::u32_as_f32_ensures; + use vstd::float::float_cast_spec; let x: f32 = n as f32; - assert(u32_as_f32_ensures(n, x)); + assert(float_cast_spec(n, x)); } } => Ok(()) } @@ -74,9 +74,9 @@ test_verify_one_file! { test_verify_one_file! { #[test] f64_to_int_cast verus_code! { fn test_f64_as_u32(f: f64) { - use vstd::float::f64_as_u32_ensures; + use vstd::float::float_cast_spec; let n: u32 = f as u32; - assert(f64_as_u32_ensures(f, n)); + assert(float_cast_spec(f, n)); } } => Ok(()) } @@ -84,9 +84,9 @@ test_verify_one_file! { test_verify_one_file! { #[test] f32_to_int_cast verus_code! { fn test_f32_as_i64(f: f32) { - use vstd::float::f32_as_i64_ensures; + use vstd::float::float_cast_spec; let n: i64 = f as i64; - assert(f32_as_i64_ensures(f, n)); + assert(float_cast_spec(f, n)); } } => Ok(()) } @@ -94,15 +94,15 @@ test_verify_one_file! { test_verify_one_file! { #[test] float_to_float_cast verus_code! { fn test_f32_as_f64(f: f32) { - use vstd::float::f32_as_f64_ensures; + use vstd::float::float_cast_spec; let d: f64 = f as f64; - assert(f32_as_f64_ensures(f, d)); + assert(float_cast_spec(f, d)); } fn test_f64_as_f32(d: f64) { - use vstd::float::f64_as_f32_ensures; + use vstd::float::float_cast_spec; let f: f32 = d as f32; - assert(f64_as_f32_ensures(d, f)); + assert(float_cast_spec(d, f)); } } => Ok(()) } @@ -127,19 +127,19 @@ test_verify_one_file! { } test_verify_one_file! { - #[test] cast_usize_and_isize verus_code! { + #[test] cast_usize_to_f64_unsupported verus_code! { fn test_usize_as_f64(n: usize) { - use vstd::float::usize_as_f64_ensures; let x: f64 = n as f64; - assert(usize_as_f64_ensures(n, x)); } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `usize` to `f64`") +} +test_verify_one_file! { + #[test] cast_f64_to_isize_unsupported verus_code! { fn test_f64_as_isize(f: f64) { - use vstd::float::f64_as_isize_ensures; let n: isize = f as isize; - assert(f64_as_isize_ensures(f, n)); } - } => Ok(()) + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f64` to `isize`") } test_verify_one_file_with_options! { diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index 0318e93f08..b9be4c0982 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -152,16 +152,6 @@ pub enum IntRange { Char, } -/// Represents a type involved in a nondeterministic cast (int or float). -/// Used by `UnaryOp::NondeterministicCast` to identify the source and destination types. -#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] -pub enum CastType { - /// An integer type, identified by its IntRange - Int(IntRange), - /// A floating-point type, identified by its bit width (e.g., 32 or 64) - Float(u32), -} - /// Type information relevant to Rust but generally not relevant to the SMT encoding. /// This information is relevant for resolving traits. /// @@ -458,13 +448,6 @@ pub enum UnaryOp { /// Length of an array or slice Length(ArrayKind), - /// Nondeterministic cast (e.g. int to float, float to int, float to float). - /// The result is constrained by an uninterpreted `_ensures` predicate in vstd::float. - /// `src` and `dst` identify the source and destination types. - NondeterministicCast { - src: CastType, - dst: CastType, - }, } /// Which builtin source name does this come from diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs index 92ae7a9e9d..3b8cb42d76 100644 --- a/source/vir/src/ast_to_sst.rs +++ b/source/vir/src/ast_to_sst.rs @@ -1754,51 +1754,6 @@ pub(crate) fn expr_to_stm_opt( let infer_exp = mk_exp(ExpX::Unary(*op, spec_exp)); Ok((vec![], Maybe::Some(Value::Exp(infer_exp)))) } - ExprX::Unary(UnaryOp::NondeterministicCast { src, dst }, exprr) => { - // Desugar into: - // 1. Evaluate the source expression - // 2. Declare a fresh nondeterministic variable of target type - // 3. Assume has_type for the target - // 4. Assume {src}_as_{dst}_ensures(source_val, result_val) - // 5. Return result_val - let (mut stms, exp) = expr_to_stm_opt(ctx, state, exprr)?; - let exp = to_exp_or_return_never!(exp, stms); - - // Declare fresh nondeterministic temp variable of the target type - let kind = PreLocalDeclKind::Immutable(Immutable(LocalDeclKind::Nondeterministic)); - let (var_ident, result_exp) = state.declare_temp_var_stm(&expr.span, &expr.typ, kind); - - // Assume the result has the target type - let has_typ_stm = assume_has_typ(&var_ident, &expr.typ, &expr.span); - stms.push(has_typ_stm); - - // Construct the call to the _ensures function - let src_name = crate::ast_util::cast_type_to_type_string(src); - let dst_name = crate::ast_util::cast_type_to_type_string(dst); - let ensures_fun = - crate::def::fn_cast_ensures(&ctx.global.vstd_crate_name, &src_name, &dst_name); - if !ctx.func_map.contains_key(&ensures_fun) { - return Err(crate::messages::error( - &expr.span, - format!( - "Verus does not support `as` cast from `{}` to `{}` (no specification function `{}_as_{}_ensures` found in vstd::float)", - src_name, dst_name, src_name, dst_name, - ), - )); - } - let call = ExpX::Call( - CallFun::Fun(ensures_fun, None), - Arc::new(vec![]), - Arc::new(vec![exp, result_exp.clone()]), - ); - let call_exp = SpannedTyped::new(&expr.span, &Arc::new(TypX::Bool), call); - - // Assume the ensures predicate - let assume_stm = Spanned::new(expr.span.clone(), StmX::Assume(call_exp)); - stms.push(assume_stm); - - Ok((stms, Maybe::Some(Value::Exp(result_exp)))) - } ExprX::Unary(op, exprr) => { let (mut stms, exp) = expr_to_stm_opt(ctx, state, exprr)?; let exp = to_exp_or_return_never!(exp, stms); diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs index 11c39088e6..6b362a0103 100644 --- a/source/vir/src/ast_util.rs +++ b/source/vir/src/ast_util.rs @@ -923,13 +923,6 @@ pub fn int_range_to_type_string(range: &IntRange) -> String { } } -pub fn cast_type_to_type_string(ct: &CastType) -> String { - match ct { - CastType::Int(range) => int_range_to_type_string(range), - CastType::Float(bits) => format!("f{}", bits), - } -} - pub fn typ_to_diagnostic_str(typ: &Typ) -> String { fn typs_to_comma_separated_str(typs: &[Arc]) -> String { typs.iter().map(|t| typ_to_diagnostic_str(t)).collect::>().join(", ") diff --git a/source/vir/src/bitvector_to_air.rs b/source/vir/src/bitvector_to_air.rs index 2b4c639890..f535fa954a 100644 --- a/source/vir/src/bitvector_to_air.rs +++ b/source/vir/src/bitvector_to_air.rs @@ -366,9 +366,6 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result { panic!("ArrayLength operation not allowed in bitvector query") } - UnaryOp::NondeterministicCast { .. } => { - panic!("internal error: NondeterministicCast should have been desugared") - } }, ExpX::UnaryOpr(UnaryOpr::Box(_) | UnaryOpr::Unbox(_), exp) => { bv_exp_to_expr(ctx, state, exp) diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index 09e43d9e2e..6f966d849d 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -431,18 +431,6 @@ pub fn strslice_type() -> Path { Arc::new(PathX { krate: None, segments: Arc::new(vec![ident]) }) } -pub fn fn_cast_ensures(vstd_crate_name: &Ident, src_name: &str, dst_name: &str) -> Fun { - Arc::new(FunX { - path: Arc::new(PathX { - krate: Some(vstd_crate_name.clone()), - segments: Arc::new(vec![ - Arc::new("float".to_string()), - Arc::new(format!("{}_as_{}_ensures", src_name, dst_name)), - ]), - }), - }) -} - pub fn fn_slice_len(vstd_crate_name: &Ident) -> Fun { Arc::new(FunX { path: Arc::new(PathX { diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs index a6ff53138e..a264cff7aa 100644 --- a/source/vir/src/heuristics.rs +++ b/source/vir/src/heuristics.rs @@ -58,7 +58,6 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp { UnaryOp::RealToInt => exp.clone(), UnaryOp::StrLen | UnaryOp::StrIsAscii | UnaryOp::Length(_) => exp.clone(), UnaryOp::InferSpecForLoopIter { .. } => exp.clone(), - UnaryOp::NondeterministicCast { .. } => exp.clone(), UnaryOp::Trigger(_) | UnaryOp::CoerceMode { .. } | UnaryOp::MustBeFinalized diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs index 720981cbf5..42500b2ff0 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -1182,7 +1182,6 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result ok, MustBeFinalized | UnaryOp::MustBeElaborated => { panic!("Found MustBeFinalized op {:?} after calling finalize_exp", exp) @@ -1303,7 +1302,6 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result ok, } } diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs index 92c1cab33e..ad8a40e0c6 100644 --- a/source/vir/src/poly.rs +++ b/source/vir/src/poly.rs @@ -595,9 +595,6 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { UnaryOp::MutRefFinal(_) => { panic!("internal error: MustBeFinalized in SST") } - UnaryOp::NondeterministicCast { .. } => { - panic!("internal error: NondeterministicCast should have been desugared") - } } } ExpX::UnaryOpr(op, e1) => { diff --git a/source/vir/src/prune.rs b/source/vir/src/prune.rs index c0cbb92215..232282ddf0 100644 --- a/source/vir/src/prune.rs +++ b/source/vir/src/prune.rs @@ -514,16 +514,6 @@ fn traverse_reachable(ctxt: &Ctxt, state: &mut State) { ExprX::Unary(UnaryOp::Length(ArrayKind::Slice), _) => { reach_function(ctxt, state, &fn_slice_len(&ctxt.vstd_crate_name)); } - ExprX::Unary(UnaryOp::NondeterministicCast { src, dst }, _) => { - let src_name = crate::ast_util::cast_type_to_type_string(src); - let dst_name = crate::ast_util::cast_type_to_type_string(dst); - let fun = crate::def::fn_cast_ensures( - &ctxt.vstd_crate_name, - &src_name, - &dst_name, - ); - reach_function(ctxt, state, &fun); - } ExprX::Binary(BinaryOp::Index(ArrayKind::Slice, bounds_check), _, _) => { reach_function(ctxt, state, &fn_slice_index(&ctxt.vstd_crate_name)); if *bounds_check != BoundsCheck::Allow { diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 73301344e7..13874375ee 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1096,11 +1096,6 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< UnaryOp::MutRefFinal(_) => { panic!("internal error: MutRefFinal should have been removed before here") } - UnaryOp::NondeterministicCast { .. } => { - panic!( - "internal error: NondeterministicCast should have been desugared in ast_to_sst" - ) - } UnaryOp::Length(kind) => { let typ = undecorate_typ(&e.typ); let typ = match &*typ { diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs index 7b8fdea8ff..ff7edad5b2 100644 --- a/source/vir/src/sst_util.rs +++ b/source/vir/src/sst_util.rs @@ -486,15 +486,6 @@ impl ExpX { UnaryOp::Length(_kind) => { (format!("length({})", exp.x.to_string_prec(global, 99)), 0) } - UnaryOp::NondeterministicCast { src, dst } => ( - format!( - "nondeterministic_cast::<{}, {}>({})", - crate::ast_util::cast_type_to_type_string(src), - crate::ast_util::cast_type_to_type_string(dst), - exp.x.to_user_string(global) - ), - 99, - ), }, UnaryOpr(op, exp) => { use crate::ast::UnaryOpr::*; diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs index a7954cdc26..27455a99de 100644 --- a/source/vir/src/triggers.rs +++ b/source/vir/src/triggers.rs @@ -132,7 +132,6 @@ fn check_trigger_expr_arg(state: &mut State, arg: &Exp) { | UnaryOp::MutRefFuture(_) | UnaryOp::MutRefFinal(_) | UnaryOp::Length(_) - | UnaryOp::NondeterministicCast { .. } | UnaryOp::InferSpecForLoopIter { .. } => {} }, ExpX::UnaryOpr(op, arg) => match op { @@ -281,8 +280,7 @@ fn check_trigger_expr( | UnaryOp::CoerceMode { .. } | UnaryOp::MustBeFinalized | UnaryOp::MustBeElaborated - | UnaryOp::CastToInteger - | UnaryOp::NondeterministicCast { .. } => Ok(()), + | UnaryOp::CastToInteger => Ok(()), UnaryOp::InferSpecForLoopIter { .. } => { Err(error(&exp.span, "triggers cannot contain loop spec inference")) } diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs index 1765475bf5..d2794723d0 100644 --- a/source/vir/src/triggers_auto.rs +++ b/source/vir/src/triggers_auto.rs @@ -417,7 +417,6 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter UnaryOp::InferSpecForLoopIter { .. } => 1, UnaryOp::StrIsAscii | UnaryOp::StrLen => fail_on_strop(), UnaryOp::MutRefFinal(_) => 1, - UnaryOp::NondeterministicCast { .. } => 0, UnaryOp::MutRefCurrent | UnaryOp::MutRefFuture(_) => unreachable!(), }; let (is_pure1, term1) = gather_terms(ctxt, ctx, e1, depth); diff --git a/source/vstd/float.rs b/source/vstd/float.rs index b76667f3d9..fe0325077a 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -102,118 +102,36 @@ pub assume_specification[ ::clone ](f: &f64) -> (res: f64) res == f, ; -// Nondeterministic cast specification functions. -// Each `{src}_as_{dst}_ensures(input, output)` predicate constrains the result -// of the Rust `as` cast `input as {dst}`. Because float casts involve rounding -// and platform-dependent behavior, each cast produces a nondeterministic result -// constrained only by this uninterpreted predicate. Users can supply axioms -// about these predicates to reason about specific rounding modes or exactness. -// -// This follows the same pattern as `add_ensures`, `sub_ensures`, etc. for -// float arithmetic. -// --- Integer to f32 --- -pub uninterp spec fn u8_as_f32_ensures(i: u8, o: f32) -> bool; - -pub uninterp spec fn u16_as_f32_ensures(i: u16, o: f32) -> bool; - -pub uninterp spec fn u32_as_f32_ensures(i: u32, o: f32) -> bool; - -pub uninterp spec fn u64_as_f32_ensures(i: u64, o: f32) -> bool; - -pub uninterp spec fn u128_as_f32_ensures(i: u128, o: f32) -> bool; - -pub uninterp spec fn usize_as_f32_ensures(i: usize, o: f32) -> bool; - -pub uninterp spec fn i8_as_f32_ensures(i: i8, o: f32) -> bool; - -pub uninterp spec fn i16_as_f32_ensures(i: i16, o: f32) -> bool; - -pub uninterp spec fn i32_as_f32_ensures(i: i32, o: f32) -> bool; - -pub uninterp spec fn i64_as_f32_ensures(i: i64, o: f32) -> bool; - -pub uninterp spec fn i128_as_f32_ensures(i: i128, o: f32) -> bool; - -pub uninterp spec fn isize_as_f32_ensures(i: isize, o: f32) -> bool; - -// --- Integer to f64 --- -pub uninterp spec fn u8_as_f64_ensures(i: u8, o: f64) -> bool; - -pub uninterp spec fn u16_as_f64_ensures(i: u16, o: f64) -> bool; - -pub uninterp spec fn u32_as_f64_ensures(i: u32, o: f64) -> bool; - -pub uninterp spec fn u64_as_f64_ensures(i: u64, o: f64) -> bool; - -pub uninterp spec fn u128_as_f64_ensures(i: u128, o: f64) -> bool; - -pub uninterp spec fn usize_as_f64_ensures(i: usize, o: f64) -> bool; - -pub uninterp spec fn i8_as_f64_ensures(i: i8, o: f64) -> bool; - -pub uninterp spec fn i16_as_f64_ensures(i: i16, o: f64) -> bool; - -pub uninterp spec fn i32_as_f64_ensures(i: i32, o: f64) -> bool; - -pub uninterp spec fn i64_as_f64_ensures(i: i64, o: f64) -> bool; - -pub uninterp spec fn i128_as_f64_ensures(i: i128, o: f64) -> bool; - -pub uninterp spec fn isize_as_f64_ensures(i: isize, o: f64) -> bool; - -// --- f32 to integer --- -pub uninterp spec fn f32_as_u8_ensures(f: f32, o: u8) -> bool; - -pub uninterp spec fn f32_as_u16_ensures(f: f32, o: u16) -> bool; - -pub uninterp spec fn f32_as_u32_ensures(f: f32, o: u32) -> bool; - -pub uninterp spec fn f32_as_u64_ensures(f: f32, o: u64) -> bool; - -pub uninterp spec fn f32_as_u128_ensures(f: f32, o: u128) -> bool; - -pub uninterp spec fn f32_as_usize_ensures(f: f32, o: usize) -> bool; - -pub uninterp spec fn f32_as_i8_ensures(f: f32, o: i8) -> bool; - -pub uninterp spec fn f32_as_i16_ensures(f: f32, o: i16) -> bool; - -pub uninterp spec fn f32_as_i32_ensures(f: f32, o: i32) -> bool; - -pub uninterp spec fn f32_as_i64_ensures(f: f32, o: i64) -> bool; - -pub uninterp spec fn f32_as_i128_ensures(f: f32, o: i128) -> bool; - -pub uninterp spec fn f32_as_isize_ensures(f: f32, o: isize) -> bool; - -// --- f64 to integer --- -pub uninterp spec fn f64_as_u8_ensures(f: f64, o: u8) -> bool; - -pub uninterp spec fn f64_as_u16_ensures(f: f64, o: u16) -> bool; - -pub uninterp spec fn f64_as_u32_ensures(f: f64, o: u32) -> bool; - -pub uninterp spec fn f64_as_u64_ensures(f: f64, o: u64) -> bool; - -pub uninterp spec fn f64_as_u128_ensures(f: f64, o: u128) -> bool; - -pub uninterp spec fn f64_as_usize_ensures(f: f64, o: usize) -> bool; - -pub uninterp spec fn f64_as_i8_ensures(f: f64, o: i8) -> bool; - -pub uninterp spec fn f64_as_i16_ensures(f: f64, o: i16) -> bool; - -pub uninterp spec fn f64_as_i32_ensures(f: f64, o: i32) -> bool; - -pub uninterp spec fn f64_as_i64_ensures(f: f64, o: i64) -> bool; +#[verifier::external_trait_specification] +pub trait ExIeeeFloatCast { + type ExternalTraitSpecificationFor: IeeeFloatCast; +} -pub uninterp spec fn f64_as_i128_ensures(f: f64, o: i128) -> bool; +#[verifier::external_trait_specification] +pub trait ExDecimal: Copy { + type ExternalTraitSpecificationFor: Decimal; +} -pub uninterp spec fn f64_as_isize_ensures(f: f64, o: isize) -> bool; +// TODO: when IEEE float support is merged, this should point to IeeeFloatCast::ieee_cast +pub uninterp spec fn ieee_float_cast, To: Decimal>(from: From) -> To; -// --- Float to float --- -pub uninterp spec fn f32_as_f64_ensures(f: f32, o: f64) -> bool; +pub uninterp spec fn float_cast_spec(from: From, to: To) -> bool; -pub uninterp spec fn f64_as_f32_ensures(f: f64, o: f32) -> 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] +#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")] +#[verifier::when_used_as_spec(ieee_float_cast)] +pub fn float_cast, To: Decimal>(from: From) -> (to: To) + ensures + float_cast_spec(from, to), + opens_invariants none + no_unwind +{ + To::CONST_DEFAULT +} } // verus! From f85d29eda45f8f90f833c41eb5c2844e7f55498f Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Mon, 9 Mar 2026 14:48:48 -0700 Subject: [PATCH 5/6] Remove code that's unneeded now that float_cast isn't const --- source/vstd/float.rs | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/source/vstd/float.rs b/source/vstd/float.rs index fe0325077a..b10870ffb2 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -107,13 +107,8 @@ pub trait ExIeeeFloatCast { type ExternalTraitSpecificationFor: IeeeFloatCast; } -#[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, To: Decimal>(from: From) -> To; +pub uninterp spec fn ieee_float_cast, To>(from: From) -> To; pub uninterp spec fn float_cast_spec(from: From, to: To) -> bool; @@ -125,13 +120,13 @@ pub uninterp spec fn float_cast_spec(from: From, to: To) -> bool; #[verifier::external_body] #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")] #[verifier::when_used_as_spec(ieee_float_cast)] -pub fn float_cast, To: Decimal>(from: From) -> (to: To) +pub fn float_cast, To>(from: From) -> (to: To) ensures float_cast_spec(from, to), opens_invariants none no_unwind { - To::CONST_DEFAULT + unimplemented!{} } } // verus! From 6bc9b31bfb4b08e843aed41ff476e2947095c311 Mon Sep 17 00:00:00 2001 From: "Chris Hawblitzel (Microsoft)" Date: Mon, 16 Mar 2026 10:30:05 -0700 Subject: [PATCH 6/6] Post-merge fixes Add a test case for f32 to f64 casting error handling. --- source/rust_verify_test/tests/float.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 4bbb8a9170..5e297efa69 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -185,6 +185,9 @@ test_verify_one_file_with_options! { } } } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f16` to `f64`") +} + +test_verify_one_file! { #[test] f32_ieee verus_code! { // TODO: replace explicit calls to ieee_cast with "as" when support for "as" is added // (and use this to replace === with ==)