Add Kani proof harnesses and contracts for unchecked_div_exact

[CYJ904]

Summary

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, full unconstrained verification (kani::any() on both
operands) was found to take upwards of 19 minutes per harness due to state-space
explosion in the bit-precise model checker — well above a reasonable per-harness
budget. 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.