Specs for conversion to and from float types with as

source/rust_verify/src/rust_to_vir_expr.rs

@@ -2264,6 +2264,142 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                         expr_vattrs.truncate,
                     )))
                 }
+                (TypX::Int(src_range), TypX::Float(dst_bits)) => {
+                    match src_range {
+                        IntRange::Int
+                        | IntRange::Nat
+                        | IntRange::Char
+                        | IntRange::USize
+                        | IntRange::ISize => {
+                            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),
+                        );
+                    }
+                    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) {
+                        TypX::Int(r) => *r,
+                        _ => unreachable!(),
+                    };
+                    match dst_range {
+                        IntRange::Int
+                        | IntRange::Nat
+                        | IntRange::Char
+                        | IntRange::USize
+                        | IntRange::ISize => {
+                            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),
+                        );
+                    }
+                    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)
+                    {
+                        return err_span(
+                            expr.span,
+                            format!(
+                                "Verus does not support `as` cast from `f{}` to `f{}`",
+                                src_bits, dst_bits,
+                            ),
+                        );
+                    }
+                    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
+                    Ok(ExprOrPlace::Expr(source_vir_expr))
+                }
                 _ => {
                     let to_ty = bctx.types.expr_ty(expr);
                     return err_span(

source/rust_verify/src/verus_items.rs

@@ -357,6 +357,7 @@ pub(crate) enum VstdItem {
     CastSlicePtrToStrPtr,
     CastStrPtrToSlicePtr,
     CastPtrToUsize,
+    FloatCast,
     RefMutArrayUnsizingCoercion,
     VecIndex,
     VecIndexMut,
@@ -666,6 +667,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)),

source/rust_verify_test/tests/float.rs

@@ -50,6 +50,143 @@ 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::float_cast_spec;
+            let x: f64 = n as f64;
+            // The ensures predicate should hold for the cast result
+            assert(float_cast_spec(n, x));
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] int_to_f32_cast verus_code! {
+        fn test_u32_as_f32(n: u32) {
+            use vstd::float::float_cast_spec;
+            let x: f32 = n as f32;
+            assert(float_cast_spec(n, x));
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] f64_to_int_cast verus_code! {
+        fn test_f64_as_u32(f: f64) {
+            use vstd::float::float_cast_spec;
+            let n: u32 = f as u32;
+            assert(float_cast_spec(f, n));
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] f32_to_int_cast verus_code! {
+        fn test_f32_as_i64(f: f32) {
+            use vstd::float::float_cast_spec;
+            let n: i64 = f as i64;
+            assert(float_cast_spec(f, n));
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] float_to_float_cast verus_code! {
+        fn test_f32_as_f64(f: f32) {
+            use vstd::float::float_cast_spec;
+            let d: f64 = f as f64;
+            assert(float_cast_spec(f, d));
+        }
+
+        fn test_f64_as_f32(d: f64) {
+            use vstd::float::float_cast_spec;
+            let f: f32 = d as f32;
+            assert(float_cast_spec(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_to_f64_unsupported verus_code! {
+        fn test_usize_as_f64(n: usize) {
+            let x: f64 = n as f64;
+        }
+    } => 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) {
+            let n: isize = f as isize;
+        }
+    } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f64` to `isize`")
+}
+
+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`")
+}
+
 test_verify_one_file! {
     #[test] f32_ieee verus_code! {
         // TODO: replace explicit calls to ieee_cast with "as" when support for "as" is added

source/vstd/float.rs

@@ -102,4 +102,31 @@ 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>;
+}
+
+// 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>(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]
+#[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<From: Copy + IeeeFloatCast<To>, To>(from: From) -> (to: To)
+    ensures
+        float_cast_spec(from, to),
+    opens_invariants none
+    no_unwind
+{
+    unimplemented!{}
+}
+
 } // verus!