Add Kani proof harnesses and contracts for unchecked_div_exact

[CYJ904]

Summary

⚠️ Coverage note: for i32 and larger types, verification uses representative interval sampling, not exhaustive proof. Values outside the tested intervals are not covered. See "Verification strategy note" below for details.

This is a deliberate coverage trade-off: representative sampling, not an exhaustive proof, for large bit-widths. Values in the unconstrained middle range are not covered by these harnesses.

This PR adds Kani function contracts and proof harnesses for unchecked_div_exact
on both signed and unsigned integer types (i8–i128, isize, u8–u128, usize).

unchecked_div_exact is an unstable intrinsic wrapper (tracking issue: rust-lang#139911)
that computes self / rhs without checking for division-by-zero, non-exact division,
or overflow. It currently has no verification coverage in this repository.

Changes

• Added #[requires(...)] contracts to unchecked_div_exact in:
  • library/core/src/num/int_macros.rs (signed integers)
  • library/core/src/num/uint_macros.rs (unsigned integers)
• Added proof harnesses in library/core/src/num/mod.rs:
  • Full-range harnesses for small bit-widths (i8, i16, u8, u16)
  • Interval-bounded harnesses (following the existing generate_unchecked_mul_intervals
    pattern) for larger bit-widths (i32, i64, i128, isize, u32, u64, u128, usize),
    each covering three representative divisor ranges: small values, values near MAX,
    and values near MAX / 2

Precondition rationale

• Signed types: rhs > 0 && self % rhs == 0 && (self != Self::MIN || rhs != -1)
• Unsigned types: rhs > 0 && self % rhs == 0

These match the runtime assert_unsafe_precondition! checks already present in the
function body. The extra MIN / -1 exclusion for signed types prevents the one
overflow case possible in exact division.

Verification strategy note

For i32 and larger types, exploratory unconstrained verification (kani::any() on both operands) was observed to take substantially longer than for smaller types, consistent with the exponential growth already visible at smaller bit-widths — the full-range i16 and u16 harnesses for this function verify in ~25s and ~55s respectively despite only a doubling in bit-width. Unconstrained runs on i32 and larger types were abandoned in favor of interval bounding before a precise wall-clock time was recorded. Following the precedent set by generate_unchecked_mul_intervals for unchecked_mul, both operands are constrained to representative sub-ranges rather than the full domain. This is a deliberate coverage trade-off (representative sampling rather than exhaustive proof for large bit-widths), consistent with the existing pattern in this file. Values in the unconstrained middle range are not covered by these harnesses.

Verification results

All 28 harnesses pass locally with 0 failures:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.