[alexanderlhicks]

Depends on #418.

Implement MUL and DIV using the existing ordered binary worker. Preserve both pop
failure residuals, charge before arithmetic (including division by zero), wrap
multiplication and divide original top by next. Add twelve ordinary complete-case
and Id accounting/progress laws; existing ADD/SUB behavior and statements stay unchanged.
Prices are independent raw opcodeMul/opcodeDiv fields; source specialization is5,
and strict progress needs only local positive selected price.

Two commits: reuse the exact already reviewed PR414 checker/test blobs on this
sibling stack, then implement the separately reviewed MUL/DIV work item. No new
checker timing claim. Base: feat/vm-arithmetic (#418); no PR merge or branch rewrite.

EELS arithmetic.py79-103/106-133 at59c1473d maps to mul/div in Arithmetic.lean;
gas.py70-71/170-173 supplies source price5. Owning Instructions3/4/5/7/10 contains
exact source/domain/ordered-effect/law/test rows. Facade, COMPOSITION, REVIEW,
generated gaps and citation locations are updated. No other opcode, public helper,
provider, pin/dependency/decision/error-policy change.

All165 current required commands passed in author, ROOT and both fresh review
lanes on tree 87f2b095bfd5f9bf91c19507cb791df3aa526e40. ROOT audited31,809
declarations with zero findings and replayed547 modules. Native/interpreted196
complete rows agree, including unchanged82 prefix and114 independently checked
MUL/DIV cases. ROOT and both reviewers each reproduced152 original source calls;
44 raw-price controls are mathematical Lean tests. Both independent adversarial
reviews are CLEAN; ROOT evaluation precededcommit.

Generic laws retain literal supplied pure; runtime world fields are sentinels.
Whole source-Evm/trace/reachable/dispatch, settlement, runner/fuel/resource and
EEST/guest obligations remain open. No broader readiness claim is made.

[alexanderlhicks]

Review of 12c6763ecf11665fcc55a79535e6c9b990ec8406 (tree 87f2b095bfd5f9bf91c19507cb791df3aa526e40): CLEAN_SCOPED_WORK_ITEM for the MUL/DIV slice and its included checker prerequisite. Whole-head cleanliness remains false while the inherited documentation finding below is open.

MUL and DIV preserve the ordered worker: first pop, second pop, independently selected execution charge, word operation, push and exact Nat PC successor. Multiplication wraps modulo 2^256; unsigned division retains operand order and returns zero for a zero divisor after charging. Empty-stack, singleton and out-of-gas cases retain their complete residual frames. The twelve new ordinary laws preserve literal Monad pure and whole worlds; Id laws establish exact selected-price accounting and strict progress under the positive-price premise. Raw zero and large prices remain admitted.

The complete two-commit range from PR base #418 was reviewed, including the checker prerequisite in immediate Git parent 48133613. The checker/test bytes match #414; the fresh checklist below independently reran their regressions. No earlier #414 execution is substituted for validation of this head.

All 165 literal CONTRIBUTING §6.3 commands passed in each of three fresh isolated checkouts. Each lane audited 31,809 declarations with zero findings and replayed all 547 kernel modules. Both independent final reports, original closed streams, all 27 producer outputs per lane, exact source identities and byte-compared own-cache archives were read and authenticated. The 196 complete native/interpreted controls cover all four arithmetic handlers, full stacks, independent raw prices, zero division, wrapping and partial failures. Runtime world sentinels are finite observations; arbitrary whole-world preservation rests on the ordinary laws.

A separate current independent A phase passed preflight and 152 original pinned calls in normal isolated Python: 30 ADD, 30 SUB, 46 MUL and 46 DIV calls, at source prices 3 and 5. Root read and authenticated its original waits/streams, current 196-row native/interpreted captures, complete 26-field source Evm observations, all related Lean frame/meter fields, caught failures, pin/dependency/runtime identities and retained source-phase manifest. The other 44 raw-price records remain Lean/mathematical controls. A reused its own authenticated frozen reference environment from #416/#418 with matching before/after identities; no STOP calls or Lean producers were rerun. Root also checked all 6,281 retained reference identities against current files. Root and B ran no additional original-source phase. Installed-RECORD, locked-wheel and trusted-startup limits remain as recorded; no interpreter settlement, dispatch, source-world or guest agreement is inferred from direct-body observations.

The material #408 documentation finding remains open. Oversized single-node raw-decoder probes exceed guest SSZ admission and do not establish the promoted guest divergence. The local arithmetic does not rely on that claim, and this scoped verdict does not waive it.

Independent source-audit chronology and auxiliary qualifications remain preserved. Local uv 0.8.17 differs from CI's 0.13.6; literal uv/Python 3.12 commands were retained without claiming environment equivalence. Current-main integration, execution/settlement/fuel, guest/EEST and resource/security/readiness remain separate. This review made no tracked edits, fixes, commits, pushes or merges.