Elide full reciprocal correction verification

perfloop/uint256 · INEFFICIENT ALGORITHM

https://perfloop.ai/t/oss/case_gv3jgpm74s

Verdict

VERIFIED · settled 2026-08-04 · pull request opened as holiman/uint256#220

Hypothesis

For the normal four-word path, lines 231-290 materialize a full five-limb by four-limb product (20 bits.Mul64 calls plus carry/subtract chains) solely to produce b for the possible one-unit decrement at line 288. I traced its consumer: reduce4 handles an overestimated quotient with r += m at lines 440-446 and an underestimated quotient with the subtraction loop at lines 450-465, so the case session should establish the Newton candidate's exactness or bounded error before treating this check as removable. The indexed incoming-call check showed Int.MulMod calls Reciprocal at uint256.go:811 for each uncached nonzero four-word modulus; callers using MulModWithReciprocal can amortize construction separately. In disposable local checks, a temporary deletion changed a direct dense-256 reciprocal benchmark from roughly 69-72 ns/op to 53-56 ns/op with zero allocations, and the existing uncached BenchmarkMulMod/mod256/uint256 moved from roughly 139-142 ns/op to 120-131 ns/op. The temporary deletion passed go test ./... including a one-million-case BigInt modular-product differential; a separate 200,000-input output comparison was byte-identical, and a 10-million-modulus search did not hit the final correction branch. Those are falsification signals, not a proof of the exported reciprocal contract or all edge cases. The proof target is an integer-bound proof or exhaustive boundary corpus showing the uncorrected candidate remains the documented floor reciprocal, followed by differential tests of both mu and MulModWithReciprocal against big.Int over adversarial limb patterns; the reproducible benchmark and CPU profile should then show the removed final-product frame accounts for the predicted direct-path reduction.

Change to test: Prove the fourth Newton candidate is already the required floor reciprocal for every supported modulus, or retain only a demonstrably rare exactness fallback, then remove the final 5-by-4 product and decrement check before alignment.

Where it lives

perfloop/uint256 · mod.go

Evidence

Reciprocal over dense four-word moduli · 10 sample pairs

metric baseline candidate paired median change confidence range required result
ns/op 69.49 52.34 −24.8% (−17.27) −17.45 to −16.59 < 0 PASSED
B/op 0 0 0 0 to 0 ≤ 0 PASSED
allocs/op 0 0 0 0 to 0 ≤ 0 PASSED

Uncached MulMod over dense four-word moduli · 10 sample pairs

metric baseline candidate paired median change confidence range required result
ns/op 114.3 98.32 −13.2% (−15.05) −17.62 to −14.73 < 0 PASSED
B/op 0 0 0 0 to 0 ≤ 0 PASSED
allocs/op 0 0 0 0 to 0 ≤ 0 PASSED

Checks: 5 of 5 passed. Verification: no defect found.

Timeline