[DicksonWu654]

Description

Concrete ADDMOD and MULMOD (Expr.addmod / Expr.mulmod on literals) widen their operands to Word512 and do the addition or multiplication and the mod in software 512-bit arithmetic. This PR uses Integer instead; the change is into @Word512 → into @Integer on two lines. For 256-bit operands the sum is below 2^257 and the product below 2^512, so the exact value is the same as before, and the remainder is below the modulus, so it still fits in a W256. A zero modulus still gives 0, and symbolic operands go through op3 as before.

It matters for code that calls mulmod in a loop, such as Uniswap's FullMath.mulDiv (two mulmods per call).

New tests: conc-modular-arithmetic-full-width (all-ones operands with moduli 2^256-1 and 2^256-2, and a zero modulus), and a QuickCheck property comparing both operations with the previous Word512 computation.

Numbers

Linux x86-64, GHC 9.8.4, -O2, both builds made the same way from this branch and from its base (8007137), runs pinned to two cores on a shared machine. Ratios are base/PR, so above 1 is faster.

• hevm exec of a contract that calls the unmodified FullMath.mulDiv (from Echidna's tests/solidity/assert/fullmath.sol) 100,000 times with large operands: median 16.64 s → 3.16 s, median paired ratio 5.09x (3 inputs, AB and BA order, 6 pairs between 4.86x and 5.83x). The return value and both output streams are identical, and for 3-call runs the --json-trace files are byte-identical.

• Echidna master built against this branch and against 8007137, six campaigns from Echidna's tests/solidity (50,000 calls, 1 worker, 5 seeds × ABBA, 10 pairs per campaign; wall time includes compilation and shrinking):

  Campaign	base (median s)	PR (median s)	median paired ratio	pairs faster	heap allocated
  assert/fullmath.sol	8.40	5.50	1.52	10/10	92.8 GB → 27.4 GB
  basic/flags.sol	6.07	6.00	0.99	4/10	unchanged
  basic/assert.sol	5.02	4.90	1.03	7/10	unchanged
  optimize/linear.sol	3.70	3.72	0.99	3/10	unchanged
  research/vera_dschief.sol	9.36	9.63	0.99	2/10	unchanged
  research/ilf_crowdsale.sol	2.64	2.54	1.04	6/10	unchanged

  The five campaigns that do not use mulmod allocate the same to within 0.01%, and in other blocks of the same benchmark they moved by a few percent in either direction, so I read them as noise. With a fixed seed, all four runs of every campaign/seed produced byte-identical corpora, reports and coverage on both builds.

Echidna pins hevm 8007137, so it would get this with its next hevm bump.

Checklist

• tested locally: test 1100/1100 (1098 existing + 2 new, -j1 --quickcheck-replay 43), ethereum-tests 14881 passed / 2108 ignored (execution-spec-tests v5.4.0 as pinned in flake.nix), cli-test 30/30, built with -f ci (-Werror). Echidna's test suite against this branch passes with solc 0.8.10 and 0.8.25. Not run locally: rpc-tests (needs an RPC key) and forge-symbolic-tests.
• added automated tests
• updated the docs
• updated the changelog

🤖 Generated with Claude Code