Barrett Reduction for division and modular arithmetic

[cmcl]

Summary

This PR contributes the original Barrett reduction additions (rebased onto latest main) and unit tests for all alias families plus selected reciprocal-template configurations not exposed by those aliases.

Placement

An open review question is whether the Barrett reduction namespace belongs beside the other 256-bit arithmetic in category/core/runtime or under category/vm/runtime instead, as @andreaslyn suggested. This PR leaves it in uint256.hpp for two reasons:

1. It simplifies comparing the rebased version with Division and modular arithmetic via Barrett reduction #1628;

2. A preliminary analysis of the execution client suggests there are plausible consumers outside category/vm which make a category/vm/runtime location potentially too narrow.

A possible future middle-ground is an opt-in category/core/runtime/uint256/barrett.hpp header.

Rebasing

The procedure for rebasing the branch was conducted by Claude Fable 5. Correctly rebasing involved whitespace adjustments, macro renamings, and deleting unused directives so it was not an entirely mechanical process and agentic LLM assistance was useful. To verify the end state faithfully ported the Barrett reduction implementation, a validation stage was developed.

A validation script normalises and byte-compares each original barrett namespace snapshot with its rebased counterpart, accounting for the differences above. The script does not account for changes outside of the barrett namespace, or deviations induced by a more modular main branch; those were reviewed per commit with git range-diff.

ORIGINAL_FIRST="872c00356"
ORIGINAL_BARRETT_TIP="2a267fed6"
REBASED_FIRST="<corresponding-first-commit-on-rebased-branch>"
REBASED_BARRETT_TIP="<last-corresponding-barrett-commit>"

git range-diff --creation-factor=999 \
    ${ORIGINAL_FIRST}^..${ORIGINAL_BARRETT_TIP} \
    ${REBASED_FIRST}^..${REBASED_BARRETT_TIP} -w

Note:

• The above only compares the original series and does not include the unit-test commit;
• --creation-factor=999: the default 60% similarity threshold refuses to pair the commits (their context lines changed with main's refactor);
• -w is passed through to the inner diffs and suppresses the 4-column de-indent noise.

The output was manually inspected to verify AI-documented deviations of the rebased commits compared to the original Barrett patch series, including:

• Replacing the tie() helper with structured bindings;
• Importing force from the intrinsics namespace;
• Macro renaming, indentation, and wrapping;
• Explanatory comments above subb_zx and subb_truncating.

Correctness

Correctness is substantiated by a pure Rocq model that follows the C++ control flow and was manually reviewed for correspondence, and the unit tests in this PR. The formalisation led to clarifications of the original proof sketches. The next section describes the testing methodology.

Testing methodology

The test suite exercises all four alias intervals and the catch-all for each of udivrem, addmod, mulmod, and mulmod_const, and all four intervals through the signed wrapper. Results are compared with the independent intx implementation.

Every alias uses the same denominator construction: interval endpoints and their immediate neighbours, selected 2^k-1, 2^k, and 2^k+1 values around bit and word boundaries, and six fixed-seed bit-width-uniform samples. Duplicate values are removed.

Generated cases use a fixed seed and separate streams per operation/alias and denominator. Separate streams ensure additional draws from one denominator stream do not affect the others. Seeds are derived from structured tags and indices using David Stafford’s Mix13 finalizer, which has good avalanche properties on sequential inputs. Values are drawn from std::mt19937_64 using custom rejection samplers, avoiding the implementation-defined mapping of std::uniform_int_distribution.

Operation-specific operands combine modular or quotient/remainder boundaries with sparse and dense word-boundary patterns, exercising quotient sizing and carry propagation.

Concrete witnesses force the rare two-correction exit in every applicable udivrem, addmod, and mulmod interval.

Benchmarks & Integration

This PR does not change any execution-client call site or provide a performance analysis. #1628 reported preliminary isolated benchmarks, but in follow-up work I intend to reproduce those measurements against the current division implementation, then benchmark candidate call sites.

[cmcl]

@claude review this PR

[Copilot]

Pull request overview

Adds Barrett-reduction support for 256-bit division and modular arithmetic, with deterministic unit tests.

Changes:

• Adds reciprocal-based division and modular arithmetic operations.
• Refines uint256 arithmetic helpers and intrinsics.
• Adds comprehensive tests and registers them with VM unit tests.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 4 comments.

File	Review summary
test/vm/unit/uint256_barrett_tests.cpp	Adds Barrett boundary and randomized correctness tests.
test/vm/unit/CMakeLists.txt	Registers the new test source.
category/core/runtime/uint256/intrinsics.hpp	Updates subtraction intrinsic handling.
category/core/runtime/uint256.hpp	Contains four unresolved findings: multiplier-bearing reciprocals in division wrappers ([P1], critical, 2 votes); unsafe subb_truncating operand bounds ([P2], critical, 3 votes); unsupported non-word-aligned remainder configurations ([P2], moderate, 2 votes); and fixed-width product constraints accepting oversized inputs ([P2], moderate, 3 votes).

Suppressed comments (5)

category/core/runtime/uint256.hpp:2123

• [P2] Match the constraints to the fixed operand widths

x.as_words() always has four words, but reduce expects words_t<min_words(Params.input_bits)>; this requirement accepts input_bits >= 257, which makes the call ill-formed. It also accepts multiplier_bits > 256 even though the reciprocal constructor's static assertion rejects multipliers wider than uint256_t. Constrain both parameters to the widths this wrapper actually supports, or add a wider-input implementation.

struct std::formatter<monad::uint256_t>

category/core/runtime/uint256.hpp:2066

• [P1] Exclude multiplier-bearing reciprocals from the signed division wrapper. The current constraint accepts a reciprocal constructed with a constant multiplier, but its call to udivrem() then reduces |x| * multiplier instead of |x|, producing a valid-looking but incorrect signed quotient and remainder. Restrict this overload to multiplier_bits == 0.
  category/core/runtime/uint256.hpp:2087
• [P1] Constrain this wrapper to the no-multiplier, five-word input it actually passes to reduce(). A multiplier-bearing reciprocal is accepted and makes reduce() compute (x + y) * multiplier mod d; configurations with input_bits >= 321 also satisfy this constraint but cannot bind because sum is always words_t<5> while reduce() requires words_t<INPUT_WORDS>.

    }

category/core/runtime/uint256.hpp:1388

• [P2] Encode the remaining reciprocal parameter invariants in the constraint. The current requires-clause accepts configurations such as min_denominator = 2^255, input_bits = 1, for which PRE_PRODUCT_SHIFT exceeds SHIFT and POST_PRODUCT_SHIFT = SHIFT - PRE_PRODUCT_SHIFT underflows; it also accepts multiplier_bits > 256 even though the constructor later relies on a static assertion for that case. These configurations should be rejected at the class boundary rather than producing invalid array widths or a late instantiation failure.

        requires(
            uint256_t{Params.min_denominator} > 0 &&
            uint256_t{Params.min_denominator} <=
                uint256_t{Params.max_denominator} &&
            Params.input_bits > 0 &&

category/core/runtime/uint256.hpp:1752

• [P2] Fully initialize the output spans in copy. When R is smaller than four words, this loop leaves the remaining destination words unchanged; for example, a division reciprocal covering 193–256-bit denominators has a one-word maximum quotient, so reduce<true> leaves quotient words 1–3 stale when called with a non-zero buffer. The public reduce method and its span parameters do not state a zero-initialization precondition; either clear the unused words here or make that precondition explicit and enforce it through a private/internal API.

         * If PRE_PRODUCT_SHIFT != 0, then q_hat underapproximates the true
         * quotient by at most 2
         *
         * If need_quotient is false, then the quotient is only computed

---

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

[github-actions]

This PR ports the Barrett-reduction implementation from #1628 onto current main (rebased with helper cleanup commits) and adds a comprehensive unit-test suite in test/vm/unit/uint256_barrett_tests.cpp.

I reviewed the diff against the review policy in REVIEW.md — traits, FFI (n/a — pure C++), C++ correctness (lifetimes / UB / integer arithmetic / move / const / thread safety), testing, style, PR hygiene, and security. No P0/P1 blocking issues found.

Correctness spot-checks worth noting for future reviewers:

• reduce() at every if constexpr sizing path stays within array bounds for all exported aliases: MAX_R_HAT_WORDS <= INPUT_WORDS in each combination, so the subb_truncating<MAX_R_HAT_WORDS>(x, qv) call in the non-multiplier branch never OOB-reads x.
• POST_PRODUCT_BIT_SHIFT == 0 (required by reduce<false>) holds for every exported alias because PRE_PRODUCT_SHIFT is aligned to BIT_SHIFT in the PRE_PRODUCT_SHIFT lambda.
• Constructor debug-asserts guarantee the truncated high words of the reciprocal are zero, matching RECIPROCAL_BITS = bit_width(max_q) derived from MIN_DENOMINATOR.
• The >> 1 >> (63 - BIT_SHIFT) idiom in the multiplier-numerator overload avoids the >> 64 UB when BIT_SHIFT == 0, and that branch is if constexpr-gated.
• sdivrem on the INT_MIN / -1 bit pattern reproduces the EVM SDIV wrap (-2^255) via two's-complement negation, and the tests exercise it explicitly.

The removal of force(sub_borrow) from intrinsics::subb is compensated by the explicit force(diff[i]) chain now inlined in uint256_t::operator<; other callers of intrinsics::subb (in subb/subb_zx/subb_truncating) already consume the value naturally, so the sub/sbb sequence remains materialized.

Test coverage is comprehensive: every exported reciprocal alias and the catch-alls for udivrem, addmod, mulmod, and mulmod_const, plus the four interval aliases through sdivrem; two-correction witnesses pin the rare q_hat == q - 2 exit for each interval where it is reachable; and nonzero_bit_shift_multiplier_numerator exercises the previously-dormant BIT_SHIFT != 0 && MULTIPLIER_WORDS > 0 path against a 576-bit oracle. Stream isolation via splitmix64(FIXED_SEED ^ tag) keeps random cases reproducible and independent.

Verdict: CORRECT

🤖 Generated with Claude Code

[github-actions]

The discarded-return force(diff[i]) calls likely do not achieve the guard the comment describes.

force() uses asm("" : "+r"(expr)) without volatile and returns by value. Once force is inlined here, its sole output (expr) is dead, and the GCC manual states that a non-volatile asm whose outputs are unused may be eliminated. If DCE fires, the diff[i] computations become dead too, and clang is once again free to rewrite the multi-word sub/sbb chain into the cmp/setcc sequence the comment warns about.

In main, force(sub_borrow) lived inside single-word subb where its return was captured into a struct field, so the value stayed live through the aggregate return. Every other force site in this file (lines 209–213, 337–340, 354–358) similarly stores/consumes the return; this is the sole discarded-return use.

Consider either making force volatile or sinking the returned values into a computed result that flows out of the function.

[github-actions]

Dropping MONAD_NO_VECTORIZE here silently changes codegen for callers that used to inherit it via always-inline.

The wrapping helpers introduced in this PR (wide_mul, and every barrett::reduce / barrett::mulmod / mulmod free function) keep MONAD_NO_VECTORIZE, so their internal truncating_mul<> calls are still shielded. But external callers that inline the generic template are no longer shielded:

• category/core/checked_math.cpp:66 — checked_mul inlines truncating_mul<2 * uint256_t::num_words> with no wrapping no-vectorize.
• The exponentiation loop in pow at lines 1103/1105 uses truncating_mul(result, base) and truncating_mul(base, base).
• uint256_t::from_string at line 1363 uses truncating_mul(result, 10).

The compiler is now free to vectorize the multi-word MULX chain in those callers, which presumably was the reason for the attribute in the first place. Worth confirming with a codegen diff on checked_mul and pow, or wrapping those callers explicitly.

[github-actions]

The requires(0 <= R && R <= std::max(M, N)) constraint is looser than the loop body demands.

The loop accesses both lhs[i] and rhs[i] up to i == R - 1, so the real precondition is R <= std::min(M, N). Under the current clause, subb_truncating<5>(words_t<5>{}, words_t<3>{}) satisfies the constraint but reads rhs[3] / rhs[4] out of bounds — UB via std::array::operator[] in release, immediate diagnostic in constant-evaluated contexts.

No current caller trips this — every in-file use passes R equal to (or below) both M and N — but the constraint is a footgun for future callers and it's out of step with the sibling subb_zx, which handles the mixed-size case properly. Consider tightening to R <= std::min(M, N).

Suggested change

	[[gnu::always_inline]]
	inline constexpr result_with_carry<words_t<R>>
	subb_truncating(words_t<M> const &lhs, words_t<N> const &rhs) noexcept
	requires(0 <= R && R <= std::max(M, N))
	{
	words_t<R> result;
	bool borrow = false;
	#pragma GCC unroll(R)
	for (size_t i = 0; i < R; i++) {
	auto const [wi, bi] = subb(lhs[i], rhs[i], borrow);
	result[i] = wi;
	borrow = bi;
	template <size_t R, size_t M, size_t N>
	[[gnu::always_inline]]
	inline constexpr result_with_carry<words_t<R>>
	subb_truncating(words_t<M> const &lhs, words_t<N> const &rhs) noexcept
	requires(R <= std::min(M, N))
	{
	words_t<R> result;
	bool borrow = false;
	#pragma GCC unroll(R)
	for (size_t i = 0; i < R; i++) {
	auto const [wi, bi] = subb(lhs[i], rhs[i], borrow);
	result[i] = wi;
	borrow = bi;
	}
	return {.value = result, .carry = borrow};
	}

[github-actions]

The two sibling helpers introduced alongside this one — subb_zx and subb_truncating — both annotate their multi-word loops with #pragma GCC unroll(N), and the PR also adds #pragma GCC unroll(...) to the udivrem normalization loops for the same reason. The new templated addc(words_t<N>, words_t<N>) doesn't have it.

Its two callers in this file — addc(q_hat, {1}) and addc(q_hat, {2}) inside reduce() (the one- and two-correction quotient bumps) — sit on the barrett hot path, so it seems worth staying consistent:

Suggested change

	{
	words_t<N> result;
	bool carry = false;
	for (size_t i = 0; i < N; i++) {
	auto [wi, bi] = addc(lhs[i], rhs[i], carry);
	result[i] = wi;
	carry = bi;
	}
	return {.value = result, .carry = carry};
	}
	template <size_t N>
	[[gnu::always_inline]]
	inline constexpr result_with_carry<words_t<N>>
	addc(words_t<N> const &lhs, words_t<N> const &rhs) noexcept
	{
	words_t<N> result;
	bool carry = false;
	#pragma GCC unroll(N)
	for (size_t i = 0; i < N; i++) {
	auto [wi, bi] = addc(lhs[i], rhs[i], carry);
	result[i] = wi;
	carry = bi;
	}
	return {.value = result, .carry = carry};
	}

[github-actions]

This PR is a rebase of #1628's Barrett-reduction implementation onto current main, plus a substantial (~1,000 line) test suite that exercises every exported reciprocal interval and catch-all, both correction-count witnesses and full alias sweeps, against intx as the oracle. The core arithmetic ships with proof sketches in-comment and (per the PR description) an accompanying Rocq model — verification effort here is well above the norm and looks solid.

The implementation is not wired into any hot path in this PR, so runtime risk is limited to compile-time footprint and the small set of ancillary changes to existing code in uint256.hpp. I focused on those ancillary changes plus the new generic surface. Findings are:

• operator< force(diff[i]) (uint256.hpp:301) — return values are discarded and the moved codegen comment may no longer describe reality; other force sites all consume the return.
• MONAD_NO_VECTORIZE dropped from truncating_mul (uint256.hpp:639) — always-inline callers outside barrett (checked_mul, operator*/pow, from_string) inherit the compiler default rather than the previous attribute.
• subb_truncating requires (uint256.hpp:1019) — R <= std::max(M, N) should be min to prevent OOB reads on future callers.
• New addc(words_t<N>, words_t<N>) missing #pragma GCC unroll(N) (uint256.hpp:1047) — sibling subb variants and the newly-unrolled udivrem loops all set it; this one is on the barrett hot path.

None of these are correctness bugs against the current call sites. The force and MONAD_NO_VECTORIZE questions are codegen-quality; the requires and unroll items are cheap safety/consistency wins.

Verdict: CORRECT

🤖 Generated with Claude Code