Specs for conversion to and from float types with as

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(

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(())
+}

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

source/vir/src/ast_to_sst.rs

@@ -1754,6 +1754,42 @@ 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);

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<TypX>]) -> String {
         typs.iter().map(|t| typ_to_diagnostic_str(t)).collect::<Vec<_>>().join(", ")

source/vir/src/bitvector_to_air.rs

@@ -366,6 +366,9 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<BvExpr, Vir
             UnaryOp::Length(_) => {
                 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)

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 {

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

source/vir/src/interpreter.rs

@@ -1182,6 +1182,7 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                         | MutRefCurrent
                         | MutRefFuture(_)
                         | MutRefFinal(_)
+                        | NondeterministicCast { .. }
                         | InferSpecForLoopIter { .. } => 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<Exp, Vi
                         | MutRefCurrent
                         | MutRefFuture(_)
                         | MutRefFinal(_)
+                        | NondeterministicCast { .. }
                         | InferSpecForLoopIter { .. } => ok,
                     }
                 }

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) => {

source/vir/src/prune.rs

@@ -514,6 +514,16 @@ 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 {

source/vir/src/sst_to_air.rs

@@ -1096,6 +1096,11 @@ 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 {

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::*;

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"))
                 }

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);