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

[feliperodri]

🟡 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

File summaries

Review details

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

@CYJ904 did you address all observations from Copilot?

[CYJ904]

@feliperodri Yes — I've addressed both issues Copilot identified:

1. Signed-division overflow: Added kani::assume(!(dividend == i64::MIN && divisor == -1)) to test_division_divisor_only to exclude the only input combination that would trigger a division overflow (commit 9030e01).
2. Overly strong performance claims: Softened the absolute wording in two places：

• the "Large Value Operations" paragraph (commit 3c8a81d)
• "Division: Bound Both Operands" closing sentence (commit f47fdff), which was the second occurrence Copilot flagged on line 121 that I'd initially missed.

Happy to request another Copilot review if that's the right next step.

[Copilot]

🟡 Changes recommended

The divisor-only example is not actually bounded, and the guidance may imply incomplete input coverage is sufficient.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (2)

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

• The divisor is not actually bounded here: != 0 excludes only one value and leaves almost the entire i64 domain. As written, this compares an effectively unconstrained pair with a pair whose operands are both range-bounded, so it does not demonstrate the stated “only the divisor is bounded” case. Give the divisor the same small nonzero range while leaving the dividend unrestricted.

    let divisor: i64 = kani::any_where(|d| *d != 0);

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

• Restricting both operands to one representative range is not a partition and establishes nothing about excluded inputs. Because this example appears under “Partition the Input Space,” explicitly note that full-domain verification requires complementary harnesses whose ranges collectively cover every input; otherwise readers may mistake this fast harness for a complete proof.

In practice, bounding both operands to a small representative range can bring verification for `i32` and larger integer types down significantly — often to well under a second on a given machine — compared to unconstrained runs that may take much longer or fail to converge within a reasonable timeout. Actual timing will vary with the solver, machine, and timeout settings used.

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

[feliperodri]

🟡 Changes recommended

The divisor-only example is not actually bounded, and the guidance may imply incomplete input coverage is sufficient.

Get a fresh assessment by requesting another Copilot review.
Review details

Suppressed comments (2)

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

* The divisor is not actually bounded here: `!= 0` excludes only one value and leaves almost the entire `i64` domain. As written, this compares an effectively unconstrained pair with a pair whose operands are both range-bounded, so it does not demonstrate the stated “only the divisor is bounded” case. Give the divisor the same small nonzero range while leaving the dividend unrestricted.

    let divisor: i64 = kani::any_where(|d| *d != 0);

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

* Restricting both operands to one representative range is not a partition and establishes nothing about excluded inputs. Because this example appears under “Partition the Input Space,” explicitly note that full-domain verification requires complementary harnesses whose ranges collectively cover every input; otherwise readers may mistake this fast harness for a complete proof.

In practice, bounding both operands to a small representative range can bring verification for `i32` and larger integer types down significantly — often to well under a second on a given machine — compared to unconstrained runs that may take much longer or fail to converge within a reasonable timeout. Actual timing will vary with the solver, machine, and timeout settings used.

* **Files reviewed:** 1/1 changed files

* **Comments generated:** 1

* **Review effort level:** Balanced

@CYJ904 these are right, could you address them?

[CYJ904]

@feliperodri Thanks for confirming — that helped me know where to focus.

I've made both changes locally, but something came up while verifying them and I'd rather check with you before pushing.

What I changed: the divisor is now bounded to an actual range (-100..=100) instead of just excluding zero, and I added a note that a single bounded range isn't a partition — full coverage would need complementary harnesses.

What I found: once the divisor is properly bounded, the performance contrast this section was built around goes away. Measured on my machine (i64, CBMC 6.8.0, CaDiCaL 2.0.0):

divisor bounded, dividend unbounded — 0.069s
both operands bounded — 0.027s
with an exact-division precondition (dividend % divisor == 0) — 0.041s
same, as proof_for_contract — 0.079s

It makes sense in hindsight — assume narrows the input space, so it tends to make solving easier rather than harder. That means the "May not converge in reasonable time" comment no longer matches reality, so I've also reworded the comments and the intro sentence to describe what each example constrains instead of promising a timing difference.

For context, the slow case I originally ran into is the real i32::unchecked_div_exact in verify-rust-std under proof_for_contract — one run went past 10 hours without converging before I stopped it, and I still have the log if it's useful. But that setup doesn't reduce to a short snippet that fits this guide.

So I'm a bit unsure what serves the docs best here, and I'd value your take:

keep the section with the neutral, coverage-focused wording I have now
drop the division subsection and fold the partition note into the general guidance above
keep a performance-focused example, which would need something closer to the real verify-rust-std setup

Happy to go whichever way you think is right — just didn't want to push wording I knew was inaccurate.