Fix unsound f128 -> i128 lower bound in float-to-int range check

kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs

@@ -160,7 +160,7 @@ const F128_I64_UPPER: [u8; 16] = [
     0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0x40,
 ];
 const F128_I128_LOWER: [u8; 16] = [
-    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0,
+    0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0xC0,
 ];
 const F128_I128_UPPER: [u8; 16] = [
     0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0x40,

tests/kani/FloatToIntInRange/test.rs

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfloat-lib
+#![feature(f128)]
 
 //! This test checks that `kani::float::float_to_int_in_range` works as expected
 
@@ -24,3 +25,32 @@ fn check_float_to_int_in_range() {
     let i: u32 = unsafe { f.to_int_unchecked() };
     assert_eq!(i, 1_000_000);
 }
+
+/// The `f128` -> `i128` lower bound used to be wrong (-2^128 instead of
+/// -(2^127 + 2^15)), so `float_to_int_in_range` accepted values whose
+/// truncation is below `i128::MIN`.
+/// See https://github.com/model-checking/kani/issues/4662
+#[kani::proof]
+fn check_f128_to_i128_in_range_boundary() {
+    // i128::MIN is exactly representable in f128 and must be accepted...
+    let f: f128 = i128::MIN as f128;
+    assert!(kani::float::float_to_int_in_range::<f128, i128>(f));
+    let i: i128 = unsafe { f.to_int_unchecked() };
+    assert_eq!(i, i128::MIN);
+
+    // ...but the next f128 below it (-(2^127 + 2^15), whose truncation is
+    // out of range) must be rejected.
+    let g: f128 = -170141183460469231731687303715884138496.0;
+    assert!(!kani::float::float_to_int_in_range::<f128, i128>(g));
+}
+
+/// Symbolic variant, mirroring the harness in verify-rust-std that caught
+/// the wrong bound: for any value that `float_to_int_in_range` accepts,
+/// `to_int_unchecked` must agree with the saturating `as` cast.
+#[kani::proof]
+fn check_f128_to_i128_in_range_symbolic() {
+    let f: f128 = kani::any();
+    kani::assume(kani::float::float_to_int_in_range::<f128, i128>(f));
+    let i: i128 = unsafe { f.to_int_unchecked() };
+    assert_eq!(i, f as i128);
+}