Add division scalability example to debugging-slow-proofs guide

[CYJ904]

Description of changes:

Adds concrete verification-time data and a worked example to the
"Debugging Slow Proofs" guide, specifically around integer division.

1. In the "Large Value Operations" section, replaces the generic
   statement that division/multiplication can be expensive with real
   cargo kani timing data (i8: ~0.15s, i16: ~25s, u16: ~55s for
   full-range harnesses), showing that verification cost grows sharply
   with bit-width rather than linearly.

2. Adds a new "Division: Bound Both Operands" subsection under
   "Partition the Input Space", showing that for division/modulo,
   bounding only the divisor is often not enough — the dividend
   typically needs to be bounded as well to make verification converge
   in reasonable time.

Context

While writing Kani proof harnesses for unchecked_div_exact in
verify-rust-std, I found that unconstrained division harnesses became impractically slow for i32 and larger integer types due to state-space explosion in the underlying SAT solver. The existing guide already documents the
general "partition the input space" pattern (linking to #3006 for
future automatic support), but did not include any concrete timing
data, nor call out that division specifically often requires bounding
both operands rather than just one. This PR adds that missing detail
based on real measurements from that work.

Issues resolved

None — this is a documentation improvement rather than a bug fix, and
was not tied to a pre-filed issue.

Manual testing

• Ran mdbook build locally to confirm the book builds successfully
  with the new content.
• Ran mdbook serve to visually verify formatting, heading levels,
  and Rust code block syntax highlighting for the new section.
• Verification-time figures cited (i8/i16/u16) come from actual local
  cargo kani runs against unchecked_div_exact, not estimates.

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

[Copilot]

🟡 Changes recommended

The new division example can fail due to signed-division overflow and the added performance claims read as overly strong guarantees without caveats.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

This PR updates the Kani documentation guide on debugging slow proofs by adding concrete verification-time data for integer division and a worked example showing how bounding operands can reduce solver workload.

Changes:

• Replaces a generic warning about expensive arithmetic with measured cargo kani timings across small integer bit-widths.
• Adds a new “Division: Bound Both Operands” subsection under “Partition the Input Space” with illustrative harnesses and guidance.

File summaries

File	Description
docs/src/debugging-slow-proofs.md	Adds division scalability timing data and a new subsection demonstrating operand bounding to improve proof performance

Review details

Suppressed comments (1)

docs/src/debugging-slow-proofs.md:121

• This sentence makes a fairly strong performance guarantee ("typically brings ... well under a second") that may not hold across machines/solvers/Kani versions. Consider phrasing it as an empirical guideline ("can often") and mentioning that results vary with solver and timeout settings.

In practice, bounding both operands to a small representative range typically brings verification for `i32` and larger integer types down to well under a second, compared to unconstrained runs that may take significantly longer or fail to converge within a reasonable timeout.

• Files reviewed: 1/1 changed files
• Comments generated: 2
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[CYJ904]

@Tianshu-Huang @wodex1nhaoIeng @srivatsansamraj @acearyanarun