Target native EVMYulLean runtime for generated Yul

[Th0rgal]

Goal

Make EVMYulLean's native Yul runtime/interpreter the authoritative Layer 3 execution target for Verity-generated runtime Yul, instead of executing Verity's custom Yul statement interpreter with an EVMYulLean-backed builtin backend.

This follows up #1722, which was auto-closed by #1725. #1725 substantially improved the EVMYulLean builtin bridge, but it did not switch Verity to EvmYul.Yul.exec / EvmYul.Yul.callDispatcher as the runtime target.

Current status after #1725

• Verity has EVMYulLean-backed builtin coverage for the current safe fragment.
• The public Layer 3 retargeting path still runs Verity-shaped YulStmt, YulState, and YulResult through interpretYulRuntimeWithBackend .evmYulLean.
• The EVMYulLean-native interpreter exists and builds:
  • EvmYul.Yul.eval
  • EvmYul.Yul.exec
  • EvmYul.Yul.execTopLevel
  • EvmYul.Yul.callDispatcher
• The existing adapter is structural, not a complete native-runtime bridge.

Required migration plan

Phase 1: Native runtime harness

Add a separate native execution path without disturbing the proven #1725 path yet.

• Implement primop-aware lowering from Verity Yul expressions to EVMYulLean expressions.
  • Known builtins must lower to .Call (.inl primOp) ... using lookupPrimOp or an explicit verified mapping.
  • Unknown names should remain .Call (.inr functionName) ... for user/helper Yul functions.
• Lower generated runtime code into an EVMYulLean YulContract.
  • Partition top-level function definitions into YulContract.functions.
  • Put non-function top-level runtime statements into the dispatcher.
• Build a native initial-state bridge from Verity transaction/state inputs into EvmYul.Yul.State.Ok.
  • Install the current contract code in the native account/code map.
  • Populate calldata, callvalue, caller/source, address, storage, memory, returndata, block/env fields, and static-call permissions.
• Define native result projection back to Verity's observable YulResult shape.
  • Return/stop/revert status
  • Return data/value projection
  • Storage changes and revert rollback
  • Logs/events
• Add executable smoke tests around EvmYul.Yul.exec / EvmYul.Yul.callDispatcher for return, storage, dispatcher selection, mapping helpers, and event logs.

Backup option: keep this as a CI smoke-test runner first, while #1725's theorem remains the public target.

Phase 2: Bridge native execution to current observable semantics

• Prove syntactic lowering invariants:
  • no top-level funcDef remains in the dispatcher,
  • helper functions are present in YulContract.functions,
  • builtin calls lower to native primops.
• Prove state bridge lemmas for calldata, selector, sender/source, callvalue, address, block fields, storage lookup, memory, and returndata.
• Prove result projection lemmas for return, stop, revert, storage, and logs.

Backup option: start with a read-only/no-storage fragment, then widen to storage and events.

Phase 3: Add a public native target theorem

Introduce a native target function, conceptually:

interpretYulRuntimeNativeEvmYulLean :
  List Compiler.Yul.YulStmt →
  YulTransaction →
  (Nat → Nat) →
  List (List Nat) →
  YulResult

Internally this should lower to an EVMYulLean YulContract, build native state, run EvmYul.Yul.callDispatcher or EvmYul.Yul.exec, and project the result.

Then prove the Layer 3 preservation theorem against this native target for the same safe fragment covered by #1725.

Backup option: first prove equivalence between interpretYulRuntimeWithBackend .evmYulLean and the native target, then retarget Layer 3 directly later.

Phase 4: Flip the trusted path

• Make the native EVMYulLean theorem the canonical end-to-end target.
• Move Verity's custom Yul interpreter to reference-oracle/regression-test status.
• Update TRUST_ASSUMPTIONS.md to document EVMYulLean as the semantic trust boundary.
• Keep the old interpreter for one release cycle as a cross-check.

Phase 5: Cleanup and upstream/fork work

• Delete or archive the old interpreter only after the proof imports no longer depend on it.
• Push any required EVMYulLean fork fixes upstream where appropriate.
• Add conformance/cross-check CI coverage for the native path.

Known blockers / design questions

• The current adapter lowers all calls as user functions, which fails native execution for builtins such as add.
• Top-level function definitions are currently not preserved as EVMYulLean contract functions.
• Full native state construction and result projection are incomplete.
• Runtime Yul is the right first target. Deploy/object-code intrinsics such as dataoffset, datasize, and datacopy should stay out of the initial migration.
• Review the EVMYulLean fork for missing primops/notations such as log0, external-call failure semantics, nested static-call behavior, and whether execTopLevel erases too much information for proof use.

Success criteria

• Native EVMYulLean runtime smoke tests execute generated Verity runtime Yul through EvmYul.Yul.exec / callDispatcher.
• Runtime lowering builds an EVMYulLean YulContract with dispatcher and functions.
• State bridge and result projection are defined and tested.
• A public theorem targets native EVMYulLean execution, not Verity's custom Yul interpreter.
• TRUST_ASSUMPTIONS.md reflects the reduced trusted surface.
• The old Verity Yul interpreter is removed from the trusted proof path or explicitly documented as a reference oracle only.

Related

• Follow-up to Replace custom Yul semantics with EVMYulLean fork as compilation target #1722 and proofs: expand EVMYulLean builtin bridge to cover signed operations #1725
• Supports Extend proven fragment to cover the full CompilationModel language surface #1723 by making the semantic target cleaner and more auditable
• Related to Strengthen macro bridge to semantic preservation (not only structural equality) #998 and [Compiler Enhancement] P0: Canonical Yul equivalence engine (solc Yul ↔ Verity Yul) #581

[Th0rgal]

After #1725, this issue is the right follow-up for the remaining native-runtime migration. I revalidated while rebasing #1731 onto main:

• proofs: expand EVMYulLean builtin bridge to cover signed operations #1725 moved the trusted builtin bridge forward, but the public Layer 3 path still runs Verity-shaped YulStmt/YulState/YulResult through interpretYulRuntimeWithBackend .evmYulLean.
• The native EVMYulLean APIs to target are still EvmYul.Yul.exec / execTopLevel / callDispatcher.
• The first implementation should stay separate from Language design axes: full implementation (25 steps across 6 axes) #1731 and add a native runtime harness: primop-aware lowering, YulContract construction, native state bridge, result projection, and smoke tests.

This should be treated as the successor scope for the native part of #1722. #1722 being closed by #1725 means “builtin bridge covered”, not “native EVMYulLean runtime adopted”.

[Th0rgal]

Progress from PR #1731 / commit 7ffa44dc:

• Added a separate native EVMYulLean lowering path beside the existing proof/report adapter so the proofs: expand EVMYulLean builtin bridge to cover signed operations #1725 bridge path stays stable.
• Added lookupRuntimePrimOp for runtime/effectful builtins (mstore, sstore, return, revert, logs, calls, transient storage, etc.) so known Yul calls lower to native .inl primops instead of user functions.
• Added lowerExprNative, lowerStmtsNative, and lowerRuntimeContractNative.
  • Top-level funcDefs are partitioned into YulContract.functions.
  • Non-function runtime statements become the dispatcher block.
  • Duplicate helper function names fail closed.
• Added EvmYulLeanNativeSmokeTest covering primop lowering, user-helper call preservation, simple execution through EvmYul.Yul.exec, and YulContract function-map construction.

This does not yet complete native state construction or result projection. The next concrete step is to build a real native initial-state bridge that installs the lowered YulContract into the account map so callDispatcher and helper-function execution can be tested without a synthetic shortcut.

[Th0rgal]

Progress from PR #1731 / commit b7e90f87:

• Native result projection now carries observable logs from EVMYulLean substate.logSeries into Verity's YulResult.events shape: topics followed by word-aligned log data.
• Native return projection now reads the returned 32-byte word from H_return instead of using EVMYulLean's internal YulHalt sentinel value. stop remains returnValue = none; non-32-byte returns project to the existing proof-oracle fallback value 0.
• Added pure projection helpers for byte-array word decoding and log-entry projection that avoid the EVMYulLean ffi.ByteArray.zeroes native-evaluator limitation.
• Added smoke coverage for return projection, log projection, and callvalue flowing through the native dispatcher/state bridge into storage.

Validation:

lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeSmokeTest Compiler.Proofs.YulGeneration.Backends.EvmYulLeanStateBridge Compiler.Proofs.YulGeneration.Backends.EvmYulLeanRetarget
python3 scripts/check_lean_hygiene.py

Remaining #1737 work after this slice:

• Extend executable native smoke tests for memory-heavy return/revert/log* paths once the EVMYulLean FFI byte-array padding path can be evaluated in CI, or route those tests through an executable with the required native support.
• Add public state/result bridge lemmas for the new projections.
• Widen native state construction for external-call semantics and returndata.
• Introduce the public native target theorem and then flip the trusted path once equivalence/preservation is proved.

[Th0rgal]

Native EVMYulLean migration progress on PR #1743, head 728b8226915896bb7f42e88ac95281001c0bb1b5:

• Added bridge reductions from the public native obligation down through nativeCallDispatcherAgreesWithInterpreter, nativeDispatcherBlockAgreesWithInterpreter, and now nativeDispatcherExecAgreesWithInterpreter.
• Added native harness names for the execution layers:
  • callDispatcherBlockResult
  • contractDispatcherBlockResult
  • contractDispatcherExecResult
• Proved wrapper reductions:
  • callDispatcher_succ_eq_callDispatcherBlockResult
  • callDispatcherBlockResult_initialState_eq_contractDispatcherBlockResult
  • contractDispatcherBlockResult_eq_execResult

Exact remaining semantic blocker:

Prove raw native dispatcher execution preservation for the supported generated fragment: EvmYul.Yul.exec fuel' (.Block nativeContract.dispatcher.body) (some nativeContract) callState, where nativeContract is produced by lowerRuntimeContractNative, must project through the current restoration/projection layer to the same observable YulResult as interpretYulRuntimeWithBackendFuel .evmYulLean fuel (Compiler.emitYul contract).runtimeCode on the same transaction, storage, events, and observable slots.

The next missing proof artifact is a cross-semantics simulation/state-alignment relation between EVMYulLean State after raw native exec and the Verity YulState used by the interpreter oracle. Existing bridge facts cover initial state construction/projection and backend retargeting within the Verity interpreter, but I did not find a reusable theorem that relates native EvmYul.Yul.exec steps to execYulFuelWithBackend .evmYulLean steps.

[Th0rgal]

Progress on PR #1743:

• Added native selector-evaluation bridge lemmas in EvmYulLeanNativeHarness: lowered generated selectorExpr now reduces through native SHR(CALLDATALOAD(0), 224), with primitive step/primCall lemmas and first-four-calldata-byte read lemmas over initialState.
• Fixed the active typed-IR review blocker by compiling Stmt.setStorageWord field wordOffset value to typed TStmt.setStorage (slot + wordOffset), with a reduction theorem covering the setPackedStorage path.

Remaining native theorem blocker: prove the UInt256 arithmetic lemma that shiftRight (calldataload initialState 0) 224 = tx.functionSelector % selectorModulus, then connect that selector result to the lazy selected-case native dispatcher proof and statement-level native/interpreter preservation.

[Th0rgal]

PR #1743 now has two more proof-facing artifacts:

• lowerNativeSwitchBlock_eq exposes the actual lazy guarded block shape generated for native switch lowering.
• selectorBytesAsNat proves the four ABI selector bytes recompose to functionSelector % selectorModulus.

The remaining native selector obligation is no longer arithmetic. It is the EVMYulLean byte-array/list decoding bridge from State.calldataload (ByteArray.readBytes ... |> uInt256OfByteArray) plus UInt256.shiftRight 224 to those four high selector bytes. Once that lands, the next bridge is selected guarded-case execution for lowerNativeSwitchBlock against the interpreter oracle.