[alexanderlhicks]

Motivation

Add signed division and signed/unsigned remainder handlers for later opcode composition.

Change in behaviour or contract

Implement SDIV, MOD and SMOD with existing Base operations and their independently
configured prices. Eighteen ordinary laws cover ordered failures, complete success
frames and worlds, exact gas loss and conditional progress. Raw zero and huge Nat
prices remain valid; strict progress requires only that the selected price is positive.

EELS sources

src/ethereum/forks/amsterdam/vm/instructions/arithmetic.py:139–169,172–199,202–229
at 59c1473ddfba341babaeca1c97a50e996f639a0b; the three source prices are each 5.
Signed source observations are pure and total before charging. The Lean helper placement
preserves effects and results; no textual-order or host-cost equivalence is claimed.
Zero divisors and signed minimum overflow still charge and can run out of gas.

Source-to-Lean rows

EthVmInstructions §3 maps sdiv, mod and smod to the corresponding Monad-only
Handler and six local laws each. §§4,5,7 state the tests, signatures and domains.
EthBase retains ownership of the numerical models.

Decisions and questions

D14 and the existing raw configuration and provider boundaries are preserved. No
decision status or dependency changes. B11, F11, G2–G7, S2 and composed resource
and guest obligations remain open.

Checks and tests

All 165 current CONTRIBUTING commands passed in the author, ROOT and two independent
review lanes on tree bca93a86a02df32abfa214b5341c22431a0c83b4 before commit. No required check was
omitted. The core audit checked 31,849 declarations with zero findings, and kernel
replay checked all 547 library modules.

All 400 complete native/interpreted observations pass, preserving the accepted 196-case
prefix and adding 204 cases. ROOT and both reviewers each ran 323 original source calls
in normal and optimized Python; 77 raw price controls remain mathematical tests.
Source, runtime and installed RECORD identities were authenticated, including the two
raw locked numeric/RLP wheels. Strict parser regressions and 720 additional reviewer
native controls passed. This supplies no EEST guest, whole-source-world, trace or cost result.

Review verdicts

Two fresh independent adversarial CODE reviews: CLEAN, with no findings. ROOT checked
scope, source fidelity, contracts, proof boundaries, validation and documentation before
committing the exact tree. Reviewer oracle and metadata corrections are preserved;
no required check or source handler was replayed for metadata.

Documentation

EthVmInstructions source, law, domain, test, status and gap rows; the facade,
COMPOSITION, REVIEW, generated GAPS and citation locations. The prior binary worker,
four arithmetic handlers and client prefix, pin and providers remain unchanged.

Stack

Depends on #421, branch feat/vm-mul-div. One separately reviewed work-item commit.
No merge, main push or maintainer branch rewrite.

Generated with Codex.

[alexanderlhicks]

Review of a1d4b5d070984f5fabbf74e0e79cef3939de0fb5 (tree bca93a86a02df32abfa214b5341c22431a0c83b4): CLEAN_SCOPED_WORK_ITEM for SDIV, MOD and SMOD. Whole-head cleanliness remains false while the inherited documentation finding below is open.

The three handlers retain ordered pops, independently selected charging, complete residual failure frames and exact success frames/worlds. SDIV truncates toward zero and handles signed minimum divided by -1; MOD uses unsigned operands; SMOD takes the dividend's sign. Zero divisors still charge. Eighteen new ordinary laws preserve literal Monad pure, whole worlds and raw zero/large prices; strict progress requires a positive selected price. Public-facade clients use the existing Base numerical contracts.

All 165 literal CONTRIBUTING §6.3 commands passed in each of three fresh isolated checkouts. Each lane audited 31,849 declarations with zero findings and replayed all 547 kernel modules. Both independent final reports, original closed streams, all 27 producer outputs per lane and byte-compared own-cache archives were read and authenticated. All 400 complete native/interpreted records agree, including signed boundaries, zero divisors, independent prices, full stacks and partial failures. Runtime world sentinels are finite observations; arbitrary whole-world preservation rests on the ordinary laws.

Each lane also completed 323 original pinned calls in normal Python and 323 with -O: 30 ADD, 30 SUB, 46 MUL, 46 DIV, and 57 each SDIV, MOD and SMOD per mode. Root authenticated the actual waits/streams, current captures, complete 26-field source Evm observations, related Lean frame/meter fields, caught failures, pin/runtime/dependency identities and both raw locked numeric/RLP wheels. The 77 other-price records remain mathematical controls. Root's source environment used Python 3.13.5; A and B used 3.12.11. A reused its own frozen reference environment with matching before/after identities. No STOP calls or Lean producers were rerun. Installed-RECORD and trusted-startup limits remain recorded; direct-body observations establish no interpreter settlement, dispatch, whole-source-world or guest agreement.

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. This local arithmetic does not rely on that claim. The separate #423 source-cache finding concerns another loader; this verdict neither transfers nor waives it.

Independent audit chronology and auxiliary qualifications are retained, including B's metadata-only generated-dataclass location correction. Local uv 0.8.17 differs from CI's 0.13.6; literal uv/Python 3.12 checklist commands were retained without claiming environment equivalence. Main integration, composed execution/fuel, guest/EEST and resource/security/readiness remain separate. This review made no tracked edits, fixes, commits, pushes or merges.