proofs: expose native EVMYulLean transition target

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean

@@ -1,6 +1,7 @@
 import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
 import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanStateBridge
 import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
+import Compiler.Codegen
 import EvmYul.Yul.Interpreter
 
 namespace Compiler.Proofs.YulGeneration.Backends.Native
@@ -97,6 +98,7 @@ def projectHaltReturn (state : EvmYul.Yul.State) (haltValue : EvmYul.Yul.Ast.Lit
 def projectResult
     (tx : YulTransaction)
     (initialStorage : Nat → Nat)
+    (initialEvents : List (List Nat))
     (result :
       Except EvmYul.Yul.Exception
         (EvmYul.Yul.State × List EvmYul.Yul.Ast.Literal)) :
@@ -108,20 +110,20 @@ def projectResult
         returnValue := values.head?.map uint256ToNat
         finalStorage := finalStorage
         finalMappings := Compiler.Proofs.storageAsMappings finalStorage
-        events := projectLogsFromState state }
+        events := initialEvents ++ projectLogsFromState state }
   | .error (.YulHalt state value) =>
       let finalStorage := projectStorageFromState tx state
       { success := true
         returnValue := projectHaltReturn state value
         finalStorage := finalStorage
         finalMappings := Compiler.Proofs.storageAsMappings finalStorage
-        events := projectLogsFromState state }
+        events := initialEvents ++ projectLogsFromState state }
   | .error _ =>
       { success := false
         returnValue := none
         finalStorage := initialStorage
         finalMappings := Compiler.Proofs.storageAsMappings initialStorage
-        events := [] }
+        events := initialEvents }
 
 /-- Lower and execute Verity runtime Yul through EVMYulLean's native
     dispatcher. -/
@@ -130,11 +132,29 @@ def interpretRuntimeNative
     (runtimeCode : List YulStmt)
     (tx : YulTransaction)
     (storage : Nat → Nat)
-    (observableSlots : List Nat := []) :
+    (observableSlots : List Nat := [])
+    (events : List (List Nat) := []) :
     Except AdapterError YulResult := do
   let contract ← lowerRuntimeContractNative runtimeCode
   let initial := initialState contract tx storage observableSlots
   let result := EvmYul.Yul.callDispatcher fuel (some contract) initial
-  pure (projectResult tx storage result)
+  pure (projectResult tx storage events result)
+
+/-- Native EVMYulLean execution target for emitted IR-contract runtime Yul.
+
+This is the executable target that #1737 will promote into the public theorem
+path once the state/result bridge lemmas are proved. It intentionally returns
+`Except AdapterError YulResult` today because native lowering can still fail
+closed for duplicate helper definitions or unsupported runtime shapes.
+-/
+def interpretIRRuntimeNative
+    (fuel : Nat)
+    (contract : Compiler.IRContract)
+    (tx : Compiler.Proofs.IRGeneration.IRTransaction)
+    (state : Compiler.Proofs.IRGeneration.IRState)
+    (observableSlots : List Nat := []) :
+    Except AdapterError YulResult :=
+  interpretRuntimeNative fuel (Compiler.emitYul contract).runtimeCode
+    (YulTransaction.ofIR tx) state.storage observableSlots state.events
 
 end Compiler.Proofs.YulGeneration.Backends.Native

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSmokeTest.lean

@@ -125,4 +125,11 @@ example :
     | .error _ => false) = true := by
   native_decide
 
+example :
+    (match Native.interpretRuntimeNative 128 []
+      sampleTx zeroStorage [] [[1, 2, 3]] with
+    | .ok result => result.success && result.events == [[1, 2, 3]]
+    | .error _ => false) = true := by
+  native_decide
+
 end Compiler.Proofs.YulGeneration.Backends

docs/NATIVE_EVMYULLEAN_TRANSITION.md

@@ -0,0 +1,135 @@
+# Native EVMYulLean Runtime Transition
+
+This document tracks the remaining work for issue #1737: make native
+EVMYulLean execution the public Layer 3 semantic target for Verity-generated
+runtime Yul.
+
+## Current State
+
+The current public proof path still targets:
+
+```lean
+interpretYulRuntimeWithBackend .evmYulLean
+```
+
+That path executes Verity's custom fuel-based Yul statement interpreter and
+routes bridged builtins through EVMYulLean-backed builtin evaluation. This is a
+useful compatibility bridge, but it is not the final architecture requested by
+#1722.
+
+The native path now exists beside it:
+
+```lean
+Compiler.Proofs.YulGeneration.Backends.Native.interpretRuntimeNative
+Compiler.Proofs.YulGeneration.Backends.Native.interpretIRRuntimeNative
+```
+
+Those entry points lower Verity runtime Yul into an EVMYulLean `YulContract`,
+construct an EVMYulLean `SharedState .Yul`, run
+`EvmYul.Yul.callDispatcher`, and project the observable result back to
+Verity's `YulResult` shape.
+
+## What This PR Establishes
+
+- The native target has an IR-contract entry point:
+  `interpretIRRuntimeNative`.
+- Native result projection preserves pre-existing event history and appends
+  native EVMYulLean logs, matching the observable shape expected by the current
+  proof-side `YulResult`.
+- The native harness remains separate from the existing retargeting theorem, so
+  the proof tree does not claim a theorem that is not yet proved.
+
+## Clean Target Architecture
+
+The desired end state is:
+
+```text
+CompilationModel
+  -> IRContract
+  -> emitted runtime Yul
+  -> EVMYulLean YulContract
+  -> EvmYul.Yul.callDispatcher
+  -> projected observable result
+```
+
+The Verity custom Yul interpreter should then be used only as a regression
+oracle, not as the semantic target in the public theorem stack.
+
+## Remaining Work
+
+1. Prove lowering invariants for the native contract shape.
+
+   Required facts:
+   - top-level `funcDef` nodes are partitioned into `YulContract.functions`,
+   - dispatcher code contains no function definitions,
+   - known runtime builtins lower to native `.inl` primops,
+   - user/helper calls remain `.inr` function calls,
+   - duplicate helper definitions fail closed.
+
+2. Prove native state bridge lemmas.
+
+   Required fields:
+   - selector and calldata byte layout,
+   - caller/source and current address,
+   - callvalue,
+   - block timestamp, block number, chain id, and blob base fee,
+   - storage lookup and storage write projection,
+   - transient storage where generated Yul uses `tload`/`tstore`,
+   - memory and returndata for ABI return/revert/log paths.
+
+3. Prove native result projection lemmas.
+
+   Required cases:
+   - normal expression values returned by `callDispatcher`,
+   - `stop`,
+   - 32-byte `return`,
+   - `revert` with rollback,
+   - log projection with topics followed by word-aligned data,
+   - hard native errors mapping to conservative failure.
+
+4. Add wider executable coverage for the native path.
+
+   Current smoke coverage exercises primop lowering, helper function maps,
+   storage writes, callvalue, return projection, and log projection. Next
+   coverage should include:
+   - dispatcher selector selection from emitted runtime code,
+   - memory-heavy `return` and `revert`,
+   - `log0` through `log4`,
+   - returndata and external-call outcomes,
+   - static-call permission behavior,
+   - mapping helper lowering or replacement with native keccak/memory code.
+
+5. Introduce the public native preservation theorem.
+
+   The successor theorem should target `interpretIRRuntimeNative`, or a
+   total wrapper around it once the remaining closed-failure cases are ruled
+   out by syntactic invariants.
+
+   A clean intermediate theorem is:
+
+   ```lean
+   interpretYulRuntimeWithBackend .evmYulLean emittedRuntime
+     =
+   interpretRuntimeNative fuel emittedRuntime ...
+   ```
+
+   for the safe generated fragment. Once that bridge is proved, retarget the
+   Layer 3 and EndToEnd statements directly to the native execution target.
+
+6. Flip the trust boundary only after the theorem target moves.
+
+   Documentation should say EVMYulLean is the authoritative semantic target
+   only after the public theorem no longer routes through
+   `execYulFuelWithBackend`. Until then, the accurate status is:
+   EVMYulLean-backed builtin bridge proven, native runtime harness executable,
+   native public theorem pending.
+
+## Cleanup After the Flip
+
+- Move `execYulFuel` and `execYulFuelWithBackend` to reference-oracle status.
+- Remove bridge-only docs that describe the custom interpreter as the active
+  semantic target.
+- Keep cross-check tests between the old oracle and native EVMYulLean for one
+  release cycle.
+- Upstream any EVMYulLean fork changes needed for memory, returndata, logs, or
+  external-call semantics.

docs/ROADMAP.md

@@ -180,7 +180,7 @@ Execution priorities:
 | # | Component | Approach | Effort | Status |
 |---|-----------|----------|--------|--------|
 | 1 | ~~Function Selectors~~ | keccak256 axiom + CI | — | ✅ **DONE** (PR #43, #46) |
-| 2 | Yul/EVM Semantics Bridge | EVMYulLean integration | 1-3m | 🟢 **PHASE 4 COMPLETE** |
+| 2 | Yul/EVM Semantics Bridge | EVMYulLean integration | 1-3m | 🟡 **BRIDGE COMPLETE, NATIVE TARGET PENDING** |
 | 3 | EVM Semantics | Strong testing + documented assumption | Ongoing | ⚪ TODO |
 
 **Yul/EVM Semantics Bridge** (Issue [#1722](https://github.com/lfglabs-dev/verity/issues/1722)): EVMYulLean (NethermindEth) provides formally-defined Yul AST types and UInt256 operations. Current integration status:
@@ -191,6 +191,7 @@ Execution priorities:
 - Unbridged: none; `mappingSlot` is bridged via the shared keccak-faithful `abstractMappingSlot` derivation
 - Phase 2 state bridge scaffolding: type conversions, storage round-trip, env field bridges (0 sorry)
 - **Phase 4 (safe-body EndToEnd retarget)**: `EvmYulLeanRetarget.lean` proves `backends_agree_on_bridged_builtins` and `evalYulExpr_evmYulLean_eq_on_bridged`, establishing that `.verity` and `.evmYulLean` agree for `BridgedExpr` expressions built from bridged builtin calls plus backend-independent `tload`/`mload`. It also defines `execYulFuelWithBackend`, proves `execYulFuelWithBackend_verity_eq`, proves straight-line/block/if/switch/for statement-fragment helpers, proves `execYulFuelWithBackend_eq_on_bridged_target` for recursive `BridgedTarget` values, proves `emitYul_runtimeCode_bridged`, proves `emitYul_runtimeCode_evmYulLean_eq_on_bridged_bodies`, and proves `yulCodegen_preserves_semantics_evmYulLean`: the existing Layer-3 IR→Yul preservation theorem retargeted to `interpretYulRuntimeWithBackend .evmYulLean` under bridged-body hypotheses. `EndToEnd.lean` now exposes `layers2_3_ir_matches_yul_evmYulLean` over that EVMYulLean-backed target without raw external function-body `BridgedStmts` hypotheses, deriving them from `SupportedSpec`, static-parameter witnesses, and `BridgedSafeStmts` source-body witnesses. `EvmYulLeanBodyClosure.lean` proves universal `compileStmtList_always_bridged` coverage for `BridgedSafeStmts`; the external-call family remains carved out behind explicit function-table simulation work. `EvmYulLeanSourceExprClosure.lean` proves scalar leaf closure (`compileExpr_bridgedSource_leaf`) and pure arithmetic/comparison/bit-operation expression closure (`compileExpr_bridgedSource`) for the `BridgedSourceExpr` fragment. Trust boundary shifts for bridged expressions, recursive bridged statement targets, Layer-3 contract executions, and the safe-body EndToEnd wrapper with fully proven builtin dependencies.
+- **Native runtime follow-up (#1737)**: the public theorem target still routes through the backend-parameterized Verity Yul interpreter. `EvmYulLeanNativeHarness.lean` provides the executable native path through `EvmYul.Yul.callDispatcher`, and `docs/NATIVE_EVMYULLEAN_TRANSITION.md` tracks the remaining state/result bridge lemmas and theorem flip needed to remove the custom interpreter from the public semantic target.
 - **Remaining to make retargeting whole-program**: extend `BridgedSafeStmts` or add a separate function-table simulation for the external-call family (`internalCall`, `internalCallAssign`, `externalCallBind`, and `ecm`)
 
 **EVM Semantics**: Mitigated by differential testing against actual EVM execution (Foundry). Likely remains a documented fundamental assumption.

docs/VERIFICATION_STATUS.md

@@ -145,10 +145,13 @@ The retargeting module [`EvmYulLeanRetarget.lean`](../Compiler/Proofs/YulGenerat
 
 The backend-parameterized executor now has a proved `.verity = .evmYulLean` theorem for recursive statement targets constrained by `BridgedTarget`, the generated runtime wrapper is proved to preserve that predicate and to execute equivalently under explicit body-closure hypotheses, Layer 3 now has a contract-level theorem whose Yul side is `interpretYulRuntimeWithBackend .evmYulLean`, and the public EndToEnd module exposes a safe-body wrapper over that target. Body closure now has a universal safe-body aggregation theorem for `BridgedSafeStmts`, and the public EndToEnd theorem uses that closure to discharge raw `BridgedStmts` body hypotheses for supported compiler-produced contracts while keeping the external-call/function-table family carved out where needed.
 
-Trust boundary (safe-body EndToEnd target): `BridgedExpr` expressions, `BridgedStraightStmts` statement lists, recursively nested `BridgedTarget` executions, source statement lists admitted by `BridgedSafeStmts`, emitted runtime wrappers whose embedded bodies are bridged, and public EndToEnd wrappers deriving those body bridges from source-level safe-body/static-param witnesses now inherit EVMYulLean semantics with fully proven builtin bridge dependencies — "EVMYulLean's execution model matches the EVM" (backed by upstream Ethereum conformance tests) — rather than "Verity's custom builtin implementations are correct."
+Native-runtime transition status: the current theorem target is still the backend-parameterized Verity statement interpreter. The executable native EVMYulLean path lives in [`EvmYulLeanNativeHarness.lean`](../Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean), and the remaining theorem-transition plan is tracked in [`NATIVE_EVMYULLEAN_TRANSITION.md`](NATIVE_EVMYULLEAN_TRANSITION.md).
+
+Trust boundary (safe-body EndToEnd target): `BridgedExpr` expressions, `BridgedStraightStmts` statement lists, recursively nested `BridgedTarget` executions, source statement lists admitted by `BridgedSafeStmts`, emitted runtime wrappers whose embedded bodies are bridged, and public EndToEnd wrappers deriving those body bridges from source-level safe-body/static-param witnesses now inherit EVMYulLean builtin semantics with fully proven bridge dependencies. The stronger claim that native `EvmYul.Yul.callDispatcher` is the public semantic target remains pending until the native theorem path replaces `execYulFuelWithBackend`.
 
 Not yet proven in this module:
 - external-call/function-table body closure beyond the current `BridgedSafeStmts` whitelist
+- native `EvmYul.Yul.callDispatcher` preservation for emitted runtime Yul
 
 Remaining gaps for whole-program retargeting:
 - 0 sorry-backed core equivalences