[gmh5225]

symbolic-simplify leaves some identically zero high-order products intact and spends its work budget trying to expand them. For example, 2^29*x*(x+1)*(x+2)*(x+3) vanishes modulo 2^32 for every input, even though a parity-only argument is insufficient.

Add an exact residue proof in the shared symbolic core. It groups factors by their complete additive base, partitions literal offsets by successive low bits, and bounds the product's trailing zeros over every possible base value. Bounds from different groups remain valid when their bases are correlated. Once the bound covers the word width, the product can be removed without polynomial expansion. CLI simplification and the GUI worker's symbolic source action both use this path automatically.

The proof retains multiplicities, wrapped offsets and opaque nonlinear bases. Its comparisons, traversal, wide constants and storage use the existing request budgets; incomplete proofs retain the original product. No public flag, optimizer default budget, dependency or ABI changes. The expanded worker integration suite took 207 seconds locally; its CTest timeout is adjusted from 180 to 360 seconds to cover the additional compile-and-run fixtures.

Validation on macOS ARM64 Release with the pinned LLVM 23 r6 package and Z3 enabled:

• 831 symbolic, 80 quadratic, 59 HighC simplification, 123 guard/predicate and 76 MBA source tests passed. New coverage includes degree 256, 257-bit arithmetic, exhaustive small-word inputs and factor multisets, independent full-width Z3 checks, nonzero near misses, distinct/correlated bases and exact/one-short resource budgets.
• Real worker and CLI tests passed for 23 source families: 138 generated C outputs, each compiled and executed at O0/O2 against 1,331 boundary triples and 4,096 random triples. New original x64 quartic/octic fixtures verify product removal, ordinary-source retention, both source representations and toggle/cache isolation.
• Seven focused GUI behavior tests passed, plus initialization/cleanup (9 total).
• All 2,296 corpus cases at 8/16/32/64 bits passed with a fixed 65,536-work benchmark allowance: zero budget caps and zero output-cost regressions. The 1,976 existing cases preserve output, work and proof status. Of 320 new cases, prior caps fall from 128 to zero, 242 outputs become smaller, and all 264 zero-product cases fully remove the product; the remaining 56 are nonzero controls.
• Eleven paired timing rounds alternate the two frozen SDKs per expression in one process, after a discarded warmup pair. Every timed output/cost/work result must match the independently checked CLI corpus. CPU P95 across per-case medians: new family 7.165 ms -> 0.603 ms (-91.6%); all cases 3.072 ms -> 2.671 ms (-13.1%); previous corpus 2.774 ms -> 2.757 ms (essentially unchanged). Individual previous-family P95 changes range from -2.2% to +3.2%; this is not a claim that every case gets faster.

Commands used for the affected build and suites:

python3 scripts/build.py build-mba-residual --parallel 8 --target \
  neverd NeverDSymbolicTests NeverDSymMBAQuadraticTests \
  NeverDHighSymSimplifyTests NeverDSymSimplifyGuardTests NeverDMBASourceTests
build-mba-residual/bin/NeverDSymbolicTests
build-mba-residual/bin/NeverDSymMBAQuadraticTests
build-mba-residual/bin/NeverDHighSymSimplifyTests
build-mba-residual/bin/NeverDSymSimplifyGuardTests
build-mba-residual/bin/NeverDMBASourceTests
DYLD_LIBRARY_PATH="$PWD/build-mba-residual/bin" \
  python3 tools/neverd-worker/tests/source_synthesis_test.py \
  build-gui-mba-residual/bin/neverd-worker \
  --cli build-mba-residual/bin/neverd --compiler /usr/bin/clang
QT_QPA_PLATFORM=offscreen DYLD_LIBRARY_PATH="$PWD/build-mba-residual/bin" \
  build-gui-mba-residual/bin/neverd-gui-tests \
  sourceTransformationCancelsWithoutBlockingBrowsingOrLosingSource \
  sourceTransformationFailureKeepsThePrecedingSource \
  sourceTransformationProfilesAreIndependentAndResetOnNavigation \
  symbolicSimplificationOfEveryFunctionIsTheDefaultUntilTurnedOff \
  symbolicSimplificationOfEveryFunctionGivesWayToOrdinarySource \
  cancellingSymbolicSimplificationOfANewFunctionShowsOrdinarySource \
  cancelledPrefetchDoesNotHoldItsLane
python3 scripts/check_clang_format.py --base origin/dev \
  --clang-format /opt/homebrew/bin/clang-format
python3 scripts/check_docs_i18n.py
python3 -m py_compile tools/neverd-bench/benchmark_symbolic_masks.py \
  tools/neverd-worker/tests/source_synthesis_test.py
git diff origin/dev --check

The reusable benchmark adds --family residue-product --count 80; local raw reports and timing harnesses remain in ignored diagnostic directories. Core qualification uses the system allocator with optional acceleration libraries, CPU/driver emulation, Python plugins, web analysis and binary-corpus/Unicorn semantic suites disabled. Those configurations and other native hosts are outside this local qualification. Full hosted platform CI is reported separately by GitHub checks.