[pepebndc]

Part 11 of 13 of the math library migration from midnight-apps contracts/src/math. Refs #213.

Stack: #1125 → #1126 → #1127 → #1128 → #1140 → #1141 → #1142 → #1143 → #1144 → #1145 → #1146 → #1147 → #1148. Merge in order.

Summary

The Uint<128> forms of div, rem, divRem and isMultiple check the result of one wit_divUint128(a, b) call with native arithmetic. Every valid input keeps its result and its failure message, and the circuits are about 4 times smaller.

Changes

• Native checks of the division result, in the order of the U128 form (73f3901d). Rows (v2 / v3): div 3356 / 1017 to 845 / 287, divRem 3269 / 1026 to 886 / 328. The forms no longer call wit_divU128.
• The guides and the CHANGELOG describe the change (44ba18fd), including every outcome for an incorrect witness result (28dd3eac).
• The guides and the CHANGELOG state that these forms call wit_divUint128 with the divisor b, so a consumer witness must implement a general division, as the reference does; a witness that only splits at 2^64 makes them fail (ba8b17e1).
• Outcomes for an incorrect witness result only. (1) The forms no longer split a and b, so a wrong split no longer fails them with Uint128: conversion invalid; they return the honest result. (2) They no longer call wit_divU128, so a replaced wit_divU128 result has no effect; they return the honest result. (3) The first wit_divUint128 call is now the division, so a replaced result of that call is a forged quotient and remainder, and it fails with the first failing message of the U128 form, for example Uint128: remainder error.

Validation

• 1,010 math tests pass. The full suite passes: 3,206 passed, 48 skipped.
• Only the four division circuits change (ZKIR v2 and v3).
• Soundness: the witness quotient and remainder arrive as four 64-bit limbs with range checks, so every product and sum in the checks stays below 2^193, far below the field modulus, and nothing wraps. The checks then require b > 0, r < b and a = q * b + r as integers. Only one pair (q, r) satisfies these conditions, so an accepted result is the true quotient and remainder. A machine-checked proof confirms this.
• Differential tests (98 circuits), against the source library: 26,094 equal results and 1,800 equal failures. Ten differences: the BUG-2 message fix of feat(math): add Pack, Bytes8 and Uint64 (2/13) #1126, and nine incorrect-witness scenarios. Seven replace the wit_divU128 result, which these forms no longer request, and now return the honest result. Two replace the first wit_divUint128 result, which is now the division, and now fail with Uint128: remainder error instead of Uint128: conversion invalid.
• Real proofs: covered by the live run at the refactor(math): verify Uint128.mulChecked with native arithmetic (13/13) #1148 head, where the four division circuits are identical: 12 test files and 449 tests pass with real proofs.

Types of changes

• Bugfix
• New feature
• Breaking change
• Documentation update
• Refactor (no API change)

PR Checklist

• I have read the Contributing Guide
• I have added tests that prove my fix is effective or that my feature works
• I have added documentation for new methods or changes to existing method behavior
• CI Workflows Are Passing

[coderabbitai]

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

• Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

_{Comment @coderabbitai help to get the list of available commands.}