proofs: expose native EVMYulLean transition target

.github/workflows/evmyullean-fork-conformance.yml

@@ -3,9 +3,9 @@ name: EVMYulLean fork conformance
 # Weekly probe that the pinned lfglabs-dev/EVMYulLean fork still
 # satisfies Verity's bridge assumptions: the fork audit and adapter
 # report artifacts are in sync, adapter correctness still builds,
-# all universal bridge lemmas still build, the public EndToEnd
-# EVMYulLean target still builds, and all 123 concrete `native_decide`
-# bridge-equivalence tests still pass.
+# all universal bridge lemmas still build, the native transition harness still
+# builds, the public EndToEnd EVMYulLean target still builds, and all 123
+# concrete `native_decide` bridge-equivalence tests still pass.
 #
 # Burn-in: the probe step is captured with `continue-on-error: true`
 # during the two-week window starting 2026-04-20 (see issue #1722 plan
@@ -36,6 +36,8 @@ on:
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSmokeTest.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanRetarget.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSignedArithSpec.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean'
@@ -58,6 +60,8 @@ on:
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSmokeTest.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanRetarget.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSignedArithSpec.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean'
@@ -160,7 +164,7 @@ jobs:
               "make test-evmyullean-fork",
               "```",
               "",
-              "This guard checks the pinned EVMYulLean fork audit, checks the adapter report, rebuilds adapter correctness and the public EndToEnd target, and runs the concrete bridge-equivalence tests."
+              "This guard checks the pinned EVMYulLean fork audit, checks the adapter report, rebuilds adapter correctness, the native transition harness, and the public EndToEnd target, and runs the concrete bridge-equivalence tests."
             ];
             const body = bodyLines.join("\n");
 

AXIOMS.md

@@ -117,8 +117,9 @@ the EVM.
 **Soundness controls**:
 - `make check` validates the fork-audit artifact against `lake-manifest.json`.
 - `make test-evmyullean-fork` rechecks the fork audit, checks the adapter
-  report, rebuilds adapter correctness and the public EndToEnd EVMYulLean
-  target, and runs the concrete `native_decide` bridge-equivalence tests.
+  report, rebuilds adapter correctness, the native transition harness, the
+  public EndToEnd EVMYulLean target, and the concrete `native_decide`
+  bridge-equivalence tests.
 - `.github/workflows/evmyullean-fork-conformance.yml` runs the conformance probe
   weekly; after the burn-in ending 2026-05-04, scheduled/manual failures fail
   the workflow and open or update a GitHub issue for drift triage.

Compiler/CompilationModel/AbiHelpers.lean

@@ -73,6 +73,10 @@ def eventSignature (eventDef : EventDef) : String :=
 def errorSignature (errorDef : ErrorDef) : String :=
   s!"{errorDef.name}(" ++ String.intercalate "," (errorDef.params.map paramTypeToSolidityString) ++ ")"
 
+def functionSignature (fn : FunctionSpec) : String :=
+  let params := fn.params.map (fun p => paramTypeToSolidityString p.ty)
+  s!"{fn.name}(" ++ String.intercalate "," params ++ ")"
+
 def storageArrayElemTypeToParamType : StorageArrayElemType → ParamType
   | .uint256 => .uint256
   | .address => .address

Compiler/CompilationModel/Dispatch.lean

@@ -278,9 +278,9 @@ private def validateCompileInputsBeforeFieldWriteConflict
   for ext in spec.externals do
     let _ ← externalFunctionReturns ext
     validateInteropExternalSpec ext
-  match firstDuplicateName (spec.functions.map (·.name)) with
+  match firstDuplicateName (spec.functions.map functionSignature) with
   | some dup =>
-      throw s!"Compilation error: duplicate function name '{dup}' in {spec.name}"
+      throw s!"Compilation error: duplicate function signature '{dup}' in {spec.name}"
   | none =>
       pure ()
   match firstDuplicateName (spec.errors.map (·.name)) with

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanAdapter.lean

@@ -180,6 +180,23 @@ def lowerExprNative : YulExpr → EvmYul.Yul.Ast.Expr
       | some prim => .Call (.inl prim) loweredArgs
       | none => .Call (.inr func) loweredArgs
 
+@[simp] theorem lowerExprNative_call_runtimePrimOp
+    (func : String)
+    (args : List YulExpr)
+    (op : EvmYul.Operation .Yul)
+    (hOp : lookupRuntimePrimOp func = some op) :
+    lowerExprNative (.call func args) =
+      .Call (.inl op) (args.map lowerExprNative) := by
+  simp [lowerExprNative, hOp]
+
+@[simp] theorem lowerExprNative_call_userFunction
+    (func : String)
+    (args : List YulExpr)
+    (hOp : lookupRuntimePrimOp func = none) :
+    lowerExprNative (.call func args) =
+      .Call (.inr func) (args.map lowerExprNative) := by
+  simp [lowerExprNative, hOp]
+
 mutual
 partial def lowerStmtsNative :
     List YulStmt → Except AdapterError (List EvmYul.Yul.Ast.Stmt)