[alexanderlhicks]

Motivation

VM handlers use VmM, while state operations use StateM. The guided lift gives them a shared complete state/error boundary.

Change in behaviour or contract

Supply liftState [Monad m] : StateM m α → VmM m α and exactly one ordinary public liftState_run equation for its literal underlying bind/pure expression. It runs the supplied action on world.tx, retains the complete success value and updated transaction, and wraps every complete StateError in VmFault.state. Failure returns no world; underlying effects and failures stay in m.

The operation and equation require Monad alone. Private clients keep LawfulMonad premises local to lawful simplification. Whole Id results, read/replace/read, skipped continuations, ordered effects and outer Option failure are checked through the public equation.

EELS sources

None. This implements the Lean-only transformer seam already specified in EthVmCore §5. State providers retain their existing source contracts.

Source-to-Lean rows

EthVmCore §3 records the action domain, complete routing, sole public equation and private clients. No EELS tracker or opcode operation is implemented here.

Decisions and questions

Follow D14's state-fault channel and the existing monad-parametric architecture. No decision or disposition changes. State X16(b), D5/S1/S2/W1, F6/F7/F11, actual trackers/lifetimes, execution/source and fuel/resource/guest obligations remain open.

Checks and tests

All148 current required commands passed in author, ROOT and both independent CODE lanes on exact tree e2552c88134c6f512612eacbd28758c65ec59d28. ROOT core audit: 31,632 declarations, zero findings; kernel replay540 modules. The exact private clients also elaborate warning-fatally with both implicit-variable options disabled. Complete ordinary Id/effect/error/base-failure clients and independent probes passed. No guest/EEST execution or native benchmark is claimed. Author and ROOT used CI-pinned uv0.13.6; both reviewers disclosed uv0.8.17 with the same managed Python3.12.11. Every literal command completed; this driver difference is recorded as a validation limitation, with no identified material effect.

Review verdicts

Both independent adversarial reviews are CLEAN with no unresolved material finding. ROOT independently checked and evaluated the exact source and original retained evidence before commit.

Documentation

Update EthVmCore §3/§4/§5/§7/§10, World's module summary, COMPOSITION, REVIEW, generated GAPS and canonical citation locations. World declarations and all other providers are unchanged. Registry, pins and layer readiness remain unchanged.

Stack

Depends on #410. New branch feat/vm-state-lift, based on feat/vm-world-carrier. This slice is independent of the CALL request carrier.

Generated with Codex.

[alexanderlhicks]

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

The Monad-only state lift and its sole ordinary public literal run equation apply the supplied StateM action to world.tx, retain every complete success value and returned transaction, and wrap every complete StateError in VmFault.state without returning a world on failure. Lawful simplification uses local LawfulMonad assumptions. Complete Id, ordered-effect and outer Option-failure clients preserve the stated scope. Independent source analysis distinguishes literal Monad behavior from unjustified lawful simplification; underlying effects are not claimed to roll back. All 116 citation-record changes relocate document line numbers only.

All 148 literal CONTRIBUTING §6.3 commands passed in each of three fresh, isolated checkouts. Each lane reports 31,632 declarations with zero findings and kernel replay of all 540 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.