Repository navigation
feat(EthVmInstructions): supply settled child outcomes - #415
alexanderlhicks wants to merge 1 commit into
Conversation
Retain complete frame/output/error values with the existing supplied local ChildSettled proof. Add private full-payload/dependent-proof/boundary and negative elaboration controls and update owning contracts/source-test rows. No runner proof-production route or stronger raw admission is selected. All148 required checks pass in four isolated lanes; both independent reviews CLEAN. ROOT evaluation precedes commit. Actual source refinement, child execution/settlement and F11 production remain open. Co-Authored-By: Codex <noreply@openai.com>
alexanderlhicks
left a comment
There was a problem hiding this comment.
Fresh review of 75fc5d035e916addc593179f6529e32a5accb323 (tree c955bd1580a3fb16db717209f5098cce827cbab4): CLEAN_SCOPED_WORK_ITEM for the new work described below. This is not a whole-head clean verdict.
The exact four-field ChildOutcome retains the complete Frame, output Bytes and optional FrameError with the supplied dependent ChildSettled frame error.isSome proof. Eighteen private ordinary theorems and two helpers check complete payload/proof retention, reconstruction, dependent elimination, proof-aware replacements and both predicate branches. Three negative elaboration controls reject missing or mismatched proofs. Success requires only zero committed spill; failure additionally requires zero pending spill and refund, and reservoir equal to its baseline. Raw halted outcomes may retain arbitrary gas and nonempty output; actual producer behavior is a separate obligation. Independent ordinary controls establish exact local constructibility and complete output/frame retention. No runtime check, producer, settlement/rollback operation, F11 choice or stronger admission condition is introduced. The parent is checker PR #414 atop #411; sibling #412/#413 APIs are not inherited. Three citation-coordinate hints change only document locations.
All 148 literal CONTRIBUTING §6.3 commands passed in each of three fresh, isolated checkouts. Each lane reports 31,693 declarations with zero findings and kernel replay of all 542 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.
Supply the specified
ChildOutcome: the complete frame, output and optional frame error, with an already supplied proof of Core'sChildSettled frame error.isSome. It stores the existing incorporation boundary without choosing how the runner produces that proof under F11.No stronger output, execution-gas, successful-refund or unrelated-frame condition is added. Halt and revert retain their complete distinct payloads. Private facade clients check dependent construction/reconstruction, complete payload and proof retention, updates, both clause branches, boundary witnesses and missing/mismatched-proof diagnostics.
The source context is the pinned EELS incorporation assertions (
vm/__init__.py:221,226–228) and child error handling (interpreter.py:449–465). This is the Lean return carrier; actual source-Evm refinement, producer reachability, rollback, runner settlement/proof production, incorporation/adapters and resume remain open. No new F11, D14, admission or readiness disposition is made.All148 current required commands passed in author, ROOT and both independent CODE lanes on exact tree
c955bd1580a3fb16db717209f5098cce827cbab4. ROOT core audit: 31,693 declarations, zero findings; ordinary kernel replay542 modules. Complete private clients also compile warning-fatally with both implicit-variable options disabled; independent proof/boundary/negative controls pass. No guest/EEST execution is claimed.Both independent adversarial reviews are CLEAN. ROOT independently evaluated the exact source and original retained check evidence before commit.
Instructions §3/§4/§5/§7/§10 owns the exact source/test/domain rows and status; COMPOSITION, REVIEW, generated GAPS and three citation-location hints are updated together. Core providers, pin, registry, dependencies and decision statuses are unchanged.
Depends on #414. New branch
feat/vm-child-outcome, based onperf/boundary-declaration-scan, so the full checks include the reviewed checker improvement.Generated with Codex.