Repository navigation
Conversation
Contributor
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: true
Comment |
This was referenced Oct 14, 2026
Port the Uint128 module from midnight-apps contracts/src/math (7de45ab, identical to the audited commit 7e09763). The circuit code is unchanged. Only the header, the pragma (>= 0.26.0) and the module imports (relative paths) change. Add the test material in the compact-contracts layout: the MockUint128 mock with the 42 source circuits, an async simulator, the test-only Uint128Witnesses (wit_divU128, wit_divUint128, wit_sqrtU128 and the toU128 and toBigint helpers), and the 169 source tests, converted to await every circuit call and to assert failures with expectRejection. Tests that replace a witness run on the dry backend only. The test helper u128 moves to test/utils/oracles.ts as toU128.
The tests "should fail when remainder >= divisor" for the Uint<128> forms of div and rem replaced wit_divUint128, the toU128 splitter. They tested the conversion check and expected "Uint128: conversion invalid", so the remainder check of these two forms had no test. Replace wit_divU128 in these tests and expect "Uint128: remainder error". Keep the conversion checks as separate tests with a correct name.
sub(U128) computed the low limb in an if/else, with a downcast to Uint<64> in the borrow branch. A circuit contains both branches. Compilers 0.28.0 to 0.30.0 range-check that downcast also when the branch is not taken, so every input with a.low >= b.low (for example sub(5, 3) and div(10, 5)) could not be proven. Compiler 0.31.1 and later guard the check, so 0.34.0 proves these inputs, but the module must not depend on that compiler behavior. Compute the low limb without a branch, as midnight-apps #309 does: lowDiff = a.low + borrow * 2^64 - b.low. The value is below 2^64 for both borrow values, so the downcast is an unguarded 64-bit range check that always holds. Uint128.zkir-shape.test.ts reads the ZKIR v2 of subU128 and fails if a less_than takes a cond_select result (the compiler form of a guarded downcast). The value tests in the same file also run on the live backend, where they are real proofs.
Apply the Uint128.compact part of midnight-apps #313 (audit finding L-06, which the May 2026 audit lists as resolved). _mul now adds each 64-bit result word in one step: 4 partial products and 3 word sums, so 7 limb splits (toU128 calls) instead of 9. Every caller of _mul (mul, mulChecked, the divisions and sqrt) gets fewer rows. The new assert "Uint128: unexpected multiplication overflow" checks that the top carry is 0. It cannot fail: the product of two values below 2^128 is below 2^256. It is a defensive check. The comment alignment of the partial products follows compact format. Test: a counting wrapper around the honest wit_divUint128 shows 7 calls for mulU128(2^128 - 1, 2^128 - 1), and the product is correct.
In Uint128._div, a bad wit_divU128 result with quotient * b > a passed the remainder and product checks and then failed inside sub(U128) with "Uint128: subtraction underflow". Check a >= quotient * b in _div first, so the failure has the division message "Uint128: division invalid". The doc of _div listed "Uint128: division sum overflow", which no code emits. Remove that line. Test: divRem(10, 5) with a witness that returns quotient 3 and remainder 0 fails with "Uint128: division invalid".
Fix the Uint128 typos of audit finding N-01 (midnight-apps #312): "equal than" in the eq doc, the step numbers in _div (Step 1 was followed by Step 3), and the witness name wit_sqrtU128Locally in the sqrt doc (the witness is wit_sqrtU128).
The failure lists of div, rem and divRem (both forms) did not name "Uint128: division product overflow", and the lists of isMultiple (both forms) and _isMultiple named only "Uint128: division by zero". A bad division witness reaches each of these messages. Name all of them. The _div entry for "Uint128: division invalid" now also covers a quotient that is too large. The wit_divUint128 comment said that Uint256 shares the witness. Uint256 does not use it. Describe the use in Uint128.toU128 instead.
Convert the Uint128 doc comments to the repository style: @module and @description instead of @title, @dev for implementation notes, a Requirements list for every assert (with its failure message) instead of @throws, and @Constraints for the circuit size. The @Constraints values are the rows of the matching MockUint128 circuit (the U128 overloads use the <name>U128 mock circuit, the internal circuits use the mock circuit of their U128 entry point), measured with compiler 0.34.0 for ZKIR v2 and v3 at this commit. Doc comments only. The code is unchanged, and every mock circuit compiles to the same ZKIR as before this commit.
MockUint128 has 42 circuits. On the local live stack, its deploy transaction with all 42 verifier keys fails before submission: "exceeded block limit in transaction fee computation" (wallet fee computation in ledger v9). The deployer halves a deploy only on a node rejection, so it does not recover from this error. Every Uint128 live test failed in its beforeAll. Set circuits_per_tx = 14 for MockUint128 in compact.toml. The deployer then sends the deploy as 3 transactions (one deploy and two circuit inserts). The other math mocks have at most 18 circuits and deploy in one transaction.
The _div step list did not name the check a >= quotient * b that fails with "Uint128: division invalid". Add it as step 4c. Replace the MODULUS comment that said pow() is not supported yet with the reason for the literal: Compact has no exponentiation operator. Doc comments only.
The rows of _add, _mul, _mulChecked, _div, _sqrt and _isMultiple were the rows of their exported U128 wrappers, which document them.
This was referenced Oct 15, 2026
pepebndc
force-pushed
the
feat/math-03-uint128
branch
from
October 15, 2026 06:21
239976f to
de2305f
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part 3 of 13 of the math library migration from midnight-apps
contracts/src/math. Closes #215.Stack: #1125 → #1126 → #1127 → #1128 → #1140 → #1141 → #1142 → #1143 → #1144 → #1145 → #1146 → #1147 → #1148. Merge in order.
Summary
Adds the
Uint128module, with three bug fixes and the open audit fixes. Names, signatures and failure messages do not change, except for the one listed message fix.Changes
Uint128with its mock, simulator, witnesses and tests (4a530191).sub(U128)branchless (13bbb278). With compilers 0.28.0 to 0.30.0, a range check in the branch that does not run made common inputs unprovable, for examplediv(10, 5). See LFDT-Minokawa/compact#250. Compiler 0.31.1 and later hide the bug, but the code fix removes the dependency on the compiler. It is the same fix as midnight-apps#309._mulcarry handling (fad854b0). This is the open midnight-apps#313. It also makesmul,divandsqrtabout 13% to 16% smaller.Uint128: division invalid, which is the documented message (63926a02)._divsteps (0f6a94e9), and the removal of the wrapper rows from the doc comments of the internal circuits (de2305f7).MockUint128in parts of 14 circuits (ebe9085b). Its 42 circuits in one deploy transaction exceed the block limit.Validation
Uint128live tests pass, includingsubU128(5, 3)anddiv(10, 5).Types of changes
PR Checklist