[alexanderlhicks]

Motivation

Bound the actual request counts and byte leaves used by the StatelessInput SSZ model. These local facts support later caller and root-domain composition without imposing a global validity invariant.

Change in behaviour or contract

Adds 15 private declarations to the existing request-size caller module. Every one of the eight actual array counts, every member transaction's byte length, extra data and the BAL is bounded by the raw request size R without a support premise. Encoded-size variants require only that actual request's Serializable proof.

Actual whole-input Serializable projects actual request support and proves the strict later witness start 16 + R < 2^32. The encoded version accepts any support proof for the same actual request. Empty transaction occurrences retain their four-byte offsets even when their payload-byte sum is zero. No final witness-end or total-input bound is claimed.

EELS sources

Pinned src/ethereum/forks/amsterdam/execution_engine/types.py:33–96, execution_engine/requests.py:99–116, stateless.py:144–165, and src/ethereum/utils/ssz.py:174–220,245–291. The additions are mathematical callers of the existing actual dictionaries and public Codec laws; they do not execute an EELS serializer or guest.

Source-to-Lean rows

EthStateless §3 describes the private size clients; §7 states their complete domains and hypotheses. The controls preserve all actual counts and member occurrences, arbitrary supported requests, the strict offset boundary, and the distinction between empty payload bytes and transaction offset overhead.

Decisions and questions

No new public API, decision, validity condition, WF, Rootable, CountRecoverable or uint256 premise. Decoder and inverse composition, source/host agreement, O2/O12, generic D5/F20, fuel, backend and guest/resource/security/readiness obligations remain open.

The integration preserves current main's accepted Q90 diagnostics, strict storage-leaf admission, parser-test cleanup and DISC-001 measurements. Those inherited changes add no new disposition in this work item.

Checks and tests

All 148 current required command lines passed. Core declaration audit: 31,509 declarations, zero findings. Kernel replay: 532 modules. The changed proof file also elaborates with fatal warnings and autoImplicit/relaxedAutoImplicit disabled; independent symbolic and negative controls cover the local support and strict-offset boundaries.

Review verdicts

Both independent adversarial reviews are CLEAN. A nonblocking source-table placement nit is deferred under CONTRIBUTING §5.5. The exact source and evidence passed final evaluation before commit.

Documentation

Updates EthStateless's private caller contracts, tests and gaps, COMPOSITION and REVIEW handoffs, generated GAPS and citation records. Corrects the global SSZ source paths and regenerates the citation ledger after integrating both accepted histories. Whole-guest readiness is unchanged.

Stack

Depends on #403 at 239e3ad95c6ec02f361532cb47e658871662c029, with current main 50dfb658b7eb578ab377fe080ae20d5bebb97bfb as an integration parent. Uses a new branch; existing maintainer-owned PR branches are unchanged.

Generated with Codex.

[alexanderlhicks]

Fresh review of d7ac9fcd4e1ca4b09dc31b61784ae8817ec62fba (tree 694026cd23d4ba6a943bceddc7ed12b51a3c3a7a): CLEAN_SCOPED_WORK_ITEM for the new work described below. This is not a whole-head clean verdict.

The fifteen new private proof clients bound all eight actual request counts and the byte lengths of each transaction, extraData and the block access list by the raw request logical size R. Actual encoded-size conclusions retain their own Serializable premises. Whole-input Serializable projects support for that same request and proves the later witness start 16 + R < 2^32; it adds no final witness-end cap. Independent source-first mathematical audits checked the formula and its boundary conditions. The new proofs do not rely on the inherited documentation claim discussed below.

All 148 literal CONTRIBUTING §6.3 commands passed in each of three fresh, isolated checkouts. Each lane reports 31,509 declarations with zero findings and kernel replay of all 532 modules. Both independent final reports, original command streams, all 22 checklist producer outputs per lane and byte-compared own-cache archives were authenticated. Auxiliary setup or inspection corrections receive no candidate-validation credit; no historical process or foreign build cache was reused as a current pass.

The material documentation finding inherited unchanged from main in #408 remains open. The oversized single-node raw-decoder probes bypass the guest SSZ admission bound and do not establish the claimed guest-level divergence. This scoped verdict neither waives that finding nor downgrades it to a nit.

The independent source audits retain their original chronology and are bound again to these unchanged source bytes. All current validation completed in fresh campaigns on this exact head.

Local validation records uv 0.8.17 while CI pins 0.13.6; literal uv/Python 3.12 commands were retained, without a claim of CI-environment equivalence. No material effect from this driver difference was identified.

This review establishes no new EELS runtime agreement, guest/EEST, resource, security, cost or readiness result. Current-main integration remains separate. This review made no tracked edits, fixes, commits, pushes or merges.

The two source-map rows before the EthStateless title and the source-span formatting are nonblocking documentation polish.