Unsound f128 -> i128 bound in float_to_int_in_range / float_to_int_unchecked UB check (F128_I128_LOWER is -2^128)

[tautschnig]

I tried this code:

#![feature(f128)]

#[kani::proof]
fn check_f128_to_i128_in_range() {
    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);
}

using the following command line invocation:

kani test.rs -Z float-lib

with Kani version: current main (also reproduces at d4df833 with CBMC 6.10; masked by CBMC's previous out-of-range conversion behavior with CBMC 6.8).

I expected to see this happen: verification succeeds — any value accepted by float_to_int_in_range::<f128, i128> is in range for to_int_unchecked, which then agrees with the saturating as cast.

Instead, this happened: the assertion fails, with counterexample f ≈ -3.402824e+38 (i.e. -1.9999… × 2^127), which is below i128::MIN and should never have been accepted by float_to_int_in_range.

Root cause: F128_I128_LOWER in kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs encodes -2^128:

const F128_I128_LOWER: [u8; 16] = [
    0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0,
];

but the documented intent ("largest floating-point value less than or equal to MIN - 1") requires -(2^127 + 2^15) — f128 has a 113-bit significand, so the f128 ulp at magnitude 2^127 is 2^15. With the exclusive > comparison, the current constant wrongly admits every f128 in (-2^128, -(2^127 + 2^15)], all of which truncate below i128::MIN. This makes both kani::float::float_to_int_in_range and the UB check for the float_to_int_unchecked intrinsic unsound for f128 -> i128.

I validated all 60 F{16,32,64,128}_{I,U}{8,...,128}_{LOWER,UPPER} constants against exact rational arithmetic; F128_I128_LOWER is the only incorrect one.

Found via the num::verify::checked_f128_to_int_unchecked_i128 harness in verify-rust-std (model-checking/verify-rust-std#613), which started failing when the Kani pin moved to CBMC 6.10.

Fix in preparation.