Fix Layout::repeat contract and f128->i128 harness failures

Two harness failures surfaced in CI once compilation was fixed:

* alloc::layout::verify::check_repeat: rust-lang#148769 changed
  Layout::repeat to not include padding after the trailing element, so
  on success the resulting size is (n - 1) * stride + self.size()
  rather than n * stride. Our postcondition size >= stride is thus
  violated for n == 1 whenever self needs padding (e.g. size 6, align
  4: size 6 < stride 8). Update the exact (non-kani) postconditions to
  the new semantics and weaken the Kani-checkable variant to n <= 1 ||
  size >= stride.

* num::verify::checked_f128_to_int_unchecked_i128: Kani's f128 -> i128
  lower bound in float_to_int_in_range is unsound (-2^128 instead of
  -(2^127 + 2^15)), so the contract instrumentation admits values that
  truncate below i128::MIN; the CBMC 6.10 upgrade in the new Kani pin
  exposed this (previously such conversions happened to saturate the
  same way as the 'as' oracle). Reported as
  model-checking/kani#4662, fix proposed in
  model-checking/kani#4663. Until that fix is
  in the pinned Kani version, hand-write this harness with an explicit
  sound input range.

Verified locally with the pinned Kani commit: both harnesses pass, and
'cargo check -p core' stays clean.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

library/core/src/alloc/layout.rs

@@ -461,19 +461,21 @@ impl Layout {
     #[stable(feature = "alloc_layout_extra", since = "CURRENT_RUSTC_VERSION")]
     #[rustc_const_stable(feature = "alloc_layout_extra", since = "CURRENT_RUSTC_VERSION")]
     #[inline]
-    // for Kani (v0.54.0), the below modulo operation is too costly to prove (running into the
-    // 6-hours timeout on GitHub); we use a weaker postcondition instead
+    // Since rust-lang/rust#148769, the result does not include padding after the trailing
+    // element, i.e., on success the resulting size is (n - 1) * stride + self.size() for n > 0
+    // (and 0 for n == 0), where stride is the returned offset.
+    // for Kani (v0.54.0), multiplication by a symbolic n is too costly to prove (running into
+    // the 6-hours timeout on GitHub); we use weaker postconditions instead
     #[cfg_attr(not(kani),
-        ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))]
+        ensures(|result| result.is_err() || n == 0 ||
+            result.as_ref().unwrap().0.size() ==
+                (n - 1) * result.as_ref().unwrap().1 + self.size()))]
     #[cfg_attr(kani,
         ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))]
-    // for Kani (v0.54.0), the below multiplication is too costly to prove (running into the
-    // 6-hours timeout on GitHub); we use a weaker postcondition instead
     #[cfg_attr(not(kani),
-        ensures(|result| result.is_err() ||
-            result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1))]
+        ensures(|result| result.is_err() || n != 0 || result.as_ref().unwrap().0.size() == 0))]
     #[cfg_attr(kani,
-        ensures(|result| result.is_err() || n == 0 ||
+        ensures(|result| result.is_err() || n <= 1 ||
             result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1))]
     pub const fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
         // FIXME(const-hack): the following could be way shorter with `?`

library/core/src/num/mod.rs

@@ -2175,8 +2175,6 @@ mod verify {
         checked_f128_to_int_unchecked_i32,
         i64,
         checked_f128_to_int_unchecked_i64,
-        i128,
-        checked_f128_to_int_unchecked_i128,
         isize,
         checked_f128_to_int_unchecked_isize,
         u8,
@@ -2192,4 +2190,25 @@ mod verify {
         usize,
         checked_f128_to_int_unchecked_usize
     );
+
+    // FIXME(kani): this harness is hand-written (instead of being generated via
+    // generate_to_int_unchecked_harness! above) because Kani's f128 -> i128 lower bound in
+    // float_to_int_in_range is unsound (-2^128 instead of -(2^127 + 2^15)), so the contract
+    // instrumentation admits out-of-range values; see
+    // https://github.com/model-checking/kani/issues/4662. Until the fix
+    // (https://github.com/model-checking/kani/pull/4663) is part of the Kani version pinned
+    // here, constrain the input to the sound range explicitly.
+    #[kani::proof_for_contract(f128::to_int_unchecked)]
+    pub fn checked_f128_to_int_unchecked_i128() {
+        let num1: f128 = kani::any_where(|f: &f128| {
+            // -(2^127 + 2^15) is the largest f128 whose truncation is below i128::MIN;
+            // require the value to be strictly above it (and below i128::MAX + 1 = 2^127).
+            f.is_finite()
+                && *f > -170141183460469231731687303715884138496.0
+                && *f < 170141183460469231731687303715884105728.0
+        });
+        let result = unsafe { num1.to_int_unchecked::<i128>() };
+
+        assert_eq!(result, num1 as i128);
+    }
 }