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.

[CYJ904]

@Tianshu-Huang @wodex1nhaoIeng @srivatsansamraj @acearyanarun

[acearyanarun]

The signed contract requires rhs > 0, which excludes valid exact divisions such as 64 / -2. I see this matches the existing runtime unsafe precondition, but is that restriction intentional? If not, it may be worth allowing nonzero negative divisors while still explicitly excluding the MIN / -1 overflow case.

[CYJ904]

The signed contract requires rhs > 0, which excludes valid exact divisions such as 64 / -2. I see this matches the existing runtime unsafe precondition, but is that restriction intentional? If not, it may be worth allowing nonzero negative divisors while still explicitly excluding the MIN / -1 overflow case.

Good catch — I dug into this with Kani.

The underlying intrinsics::exact_div's actual UB conditions are rhs == 0 || self % rhs != 0 || (self == MIN && rhs == -1) — there's no sign restriction on rhs. I verified with Kani that relaxing the precondition to rhs != 0 && (self != MIN || rhs != -1) && self % rhs == 0 (in that order, to avoid an overflow in self % rhs itself when self == MIN && rhs == -1) verifies successfully with zero failures across the full i8 domain. Kani's own semantic model of the intrinsic finds no UB for negative divisors once those two cases are excluded — this matches your 64 / -2 example.

Separately, I confirmed the function's existing assert_unsafe_precondition!(rhs > 0 && ...) isn't actually exercised by Kani for this proof. Checks using the check_language_ub kind are documented as always skipped under const-eval/Miri, since those tools have their own independent UB semantics and the manual assert would be redundant (and Kani follows the same model). So this result is direct evidence about the intrinsic's true safety envelope, not a claim about the current implementation's runtime behavior in a normal debug build.

Given that, rhs > 0 does look like a stricter precondition than the intrinsic actually needs — my best guess is it was carried over conservatively rather than derived from the true UB conditions. I'd rather not widen it inside this PR though, since that would be a change to unchecked_div_exact's actual safety contract, not just adding verification for the existing one. Happy to open a follow-up issue to track relaxing the runtime precondition if that's worth pursuing