[alexanderlhicks]

Motivation

Supply the mathematical transaction-state view needed to state and prove current
account reads against the composed block and transaction effects.

Change in behaviour or contract

TxState.view applies whole revertible effects to the block view on every raw
state, without Monad or validity premises. A Lean-private conversion preserves
all four effect fields and existing order metadata; transient data is omitted.
Exactly one public derived law observes accounts: transaction entries, including
tombstones, override the block view; a miss falls back to it. Other support remains
private. The future operational account-read theorem keeps its own premises.

EELS sources

At pin 59c1473ddfba341babaeca1c97a50e996f639a0b, transaction fields are in
src/ethereum/forks/amsterdam/state_tracker.py:78–104, block extraction at
:861–881, and mathematical application in src/ethereum/state_mpt.py:133–161.
There is no standalone Python mathematical-view operation. The new numerical
checks establish finite model composition; they are not a source differential.

Source-to-Lean rows

EthState §3 maps the existing composition to TxState.view; §7.2 owns its sole
public account observer law, for the named future getAccountOptional_model
consumer. Complete conversion and raw-field/metadata support stays private.

Decisions and questions

Follows the existing mathematical-application, D23 and F20 boundaries. No new
provider interface, normalization policy, decision disposition or guest outcome.
Operational trackers, history/WF, F7, S1/S2/W1 and whole-State gates remain open.

Checks and tests

All 176 current CONTRIBUTING commands passed independently in author, ROOT and
two fresh CODE review lanes. Core audit: 31,724 declarations, zero findings;
545 library modules passed kernel replay. Complete native/interpreted raw results
match 118 independently frozen mathematical cases, including clear/write ordering,
tombstones, malformed raw storage, empty/zero maps, code and ignored contexts.
Private ordinary proofs cover exact metadata transport. Public-only clients check
arbitrary-m signatures including a constructor without Monad. Strict parser
regressions pass normally and with -O; reviewers added independent controls.
No actual-source differential, guest/EEST, resource or performance result is claimed.

Review verdicts

Two fresh independent adversarial CODE reviews: CLEAN for this exact diff.
ROOT independently evaluated scope, public/private proof boundaries, source support,
full checks, complete model observations, documentation and exact tree before commit.

The inherited material DISC-001 guest-domain claim from the #408 review
remains open and is being corrected separately; these verdicts do not waive it.

Documentation

EthState source/domain/law/test/status/gap rows, State and Conformance facades,
COMPOSITION, REVIEW, generated gaps, citation locations, lake registration and
checklist/CI commands. Whole-State readiness is unchanged.

Stack

Depends on #426, branch feat/state-prestate-account. Further State work can
continue on this basis while it awaits maintainer review.

Generated with Codex.

[alexanderlhicks]

CLEAN_SCOPED_WORK_ITEM at fe1b4c6e00845f1e5c9e76f1a7725763ab050f33 (tree 79f296870ef5bba50f8a5c223e9c43a40d93df73), against the actual #426 parent/base. No new blocking findings or recommendations in this work item. This is not a whole-head clean verdict.

Reviewed all 18 changed paths, the raw mathematical application contract, private conversion/proofs, public account law and facade clients, complete fixture observations, strict reader/regressions, documentation and citation changes. The view composes block effects before transaction effects without Monad/WF/history assumptions. Clear-before-write, zero erasure, touched-empty pruning, untouched raw storage, tombstones and complete code replacement follow the existing application contract. Order metadata is transported through the existing observers without repair; transient state is omitted. The operational account-read consumer retains its separate premises.

Root and two independent review lanes each passed all 176 literal candidate CONTRIBUTING commands on separate cold exact-head clones. Each packet retains 28 producer captures, 31,724 audited declarations with zero findings, and replay of all 545 modules. The native/interpreted results and strict mathematical reader cover all 118 complete cases. I authenticated the closed process streams, tracked sources, captures, complete cache archives and byte comparisons, and read both full independent reports.

Recovery qualification: A's receipt writer failed after all 176 child commands had passed and all 28 outputs had been captured. Its original failed outer receipt remains preserved. A separately reviewed continuation authenticated and finalized that retained evidence without rerunning the completed commands or producers, then completed archive comparison and sealing with new successful receipts. This is not an uninterrupted outer-runner success.

The new mathematical gate has no standalone EELS counterpart and executes no EELS comparator. The inherited #423 source-authentication finding remains open; this gate does not depend on that mechanism. The inherited #408 guest-domain finding also remains open. Neither is repaired or waived by this review. Parent integration, operational/source-world refinement, guest/EEST, resources, performance and whole-State readiness remain outside this verdict. Local uv was 0.8.17 rather than CI's 0.13.6; literal uv/Python 3.12 commands were retained without claiming environment equivalence.