proofs: expose native EVMYulLean transition target

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

@@ -3,9 +3,10 @@ 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, emitted dispatcher native/reference oracle coverage still passes, 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 +37,9 @@ 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/EvmYulLeanNativeDispatchOracleTest.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 +62,9 @@ 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/EvmYulLeanNativeDispatchOracleTest.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 +167,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/Compile.lean

@@ -126,6 +126,29 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
               compileSetStorage fields dynamicSource field value
   | Stmt.setStorageAddr field value =>
       compileSetStorage fields dynamicSource field value true
+  | Stmt.setStorageWord field wordOffset value =>
+      match findFieldWithResolvedSlot fields field with
+      | some (f, slot) => do
+          let valueExpr ← compileExpr fields dynamicSource value
+          let slotExpr (baseSlot : Nat) :=
+            if wordOffset == 0 then YulExpr.lit baseSlot
+            else YulExpr.call "add" [YulExpr.lit baseSlot, YulExpr.lit wordOffset]
+          match f.aliasSlots with
+          | [] =>
+              pure [YulStmt.expr (YulExpr.call "sstore" [slotExpr slot, valueExpr])]
+          | _ =>
+              pure [
+                YulStmt.block (
+                  [YulStmt.let_ "__compat_value" valueExpr] ++
+                  (slot :: f.aliasSlots).map (fun writeSlot =>
+                    YulStmt.expr (YulExpr.call "sstore" [
+                      slotExpr writeSlot,
+                      YulExpr.ident "__compat_value"
+                    ]))
+                )
+              ]
+      | none =>
+          throw s!"Compilation error: unknown storage field '{field}' in setStorageWord"
   | Stmt.storageArrayPush field value =>
       compileStorageArrayPush fields dynamicSource field value
   | Stmt.storageArrayPop field =>

Compiler/CompilationModel/Dispatch.lean

@@ -278,9 +278,20 @@ 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.filter (fun fn => !fn.isInternal)).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.functions.filter (·.isInternal)).map (·.name)) with
+  | some dup =>
+      throw s!"Compilation error: duplicate internal function name '{dup}' in {spec.name}; internal function Yul definitions are keyed by name"
+  | none =>
+      pure ()
+  let externalFunctionNames := (spec.functions.filter (fun fn => !fn.isInternal)).map (·.name)
+  match (spec.functions.filter (·.isInternal)).find? (fun fn => externalFunctionNames.contains fn.name) with
+  | some fn =>
+      throw s!"Compilation error: internal function name '{fn.name}' collides with an external function name in {spec.name}; internal function Yul definitions are keyed by name"
   | none =>
       pure ()
   match firstDuplicateName (spec.errors.map (·.name)) with
@@ -352,11 +363,13 @@ def validateCompileInputs (spec : CompilationModel) (selectors : List Nat) : Exc
   | none =>
       pure ()
   let mappingHelpersRequired := usesMapping fields
-  let arrayHelpersRequired := contractUsesArrayElement spec
+  let arrayHelpersRequired := contractUsesPlainArrayElement spec
+  let arrayElementWordHelpersRequired := contractUsesArrayElementWord spec
   let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
   let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
   match firstReservedExternalCollision
-      spec mappingHelpersRequired arrayHelpersRequired storageArrayHelpersRequired dynamicBytesEqHelpersRequired with
+      spec mappingHelpersRequired arrayHelpersRequired arrayElementWordHelpersRequired
+        storageArrayHelpersRequired dynamicBytesEqHelpersRequired with
   | some name =>
       if name.startsWith internalFunctionPrefix then
         throw s!"Compilation error: external declaration '{name}' uses reserved prefix '{internalFunctionPrefix}' ({issue756Ref})."
@@ -380,7 +393,8 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
   let externalFns := spec.functions.filter (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)
   let internalFns := spec.functions.filter (·.isInternal)
   let mappingHelpersRequired := usesMapping fields
-  let arrayHelpersRequired := contractUsesArrayElement spec
+  let arrayHelpersRequired := contractUsesPlainArrayElement spec
+  let arrayElementWordHelpersRequired := contractUsesArrayElementWord spec
   let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
   let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
   let fallbackSpec ← pickUniqueFunctionByName "fallback" spec.functions
@@ -389,10 +403,18 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
     compileFunctionSpec fields spec.events spec.errors spec.adtTypes sel fnSpec
   let internalFuncDefs ← internalFns.mapM (compileInternalFunction fields spec.events spec.errors spec.adtTypes)
   let arrayElementHelpers :=
-    if arrayHelpersRequired then
-      [checkedArrayElementCalldataHelper, checkedArrayElementMemoryHelper]
+    (if arrayHelpersRequired then
+      [ checkedArrayElementCalldataHelper
+      , checkedArrayElementMemoryHelper
+      ]
     else
-      []
+      []) ++
+    (if arrayElementWordHelpersRequired then
+      [ checkedArrayElementWordCalldataHelper
+      , checkedArrayElementWordMemoryHelper
+      ]
+    else
+      [])
   let storageArrayElementHelpers :=
     if storageArrayHelpersRequired then
       [checkedStorageArrayElementHelper]

Compiler/CompilationModel/DynamicData.lean

@@ -20,6 +20,12 @@ def checkedArrayElementCalldataHelperName : String :=
 def checkedArrayElementMemoryHelperName : String :=
   "__verity_array_element_memory_checked"
 
+def checkedArrayElementWordCalldataHelperName : String :=
+  "__verity_array_element_word_calldata_checked"
+
+def checkedArrayElementWordMemoryHelperName : String :=
+  "__verity_array_element_word_memory_checked"
+
 def checkedStorageArrayElementHelperName : String :=
   "__verity_storage_array_element_checked"
 
@@ -50,6 +56,33 @@ def checkedArrayElementCalldataHelper : YulStmt :=
 def checkedArrayElementMemoryHelper : YulStmt :=
   checkedArrayElementHelper checkedArrayElementMemoryHelperName "mload"
 
+private def checkedArrayElementWordHelper (helperName loadOp : String) : YulStmt :=
+  let elementWordIndex :=
+    YulExpr.call "add" [
+      YulExpr.call "mul" [YulExpr.ident "index", YulExpr.ident "element_words"],
+      YulExpr.ident "word_offset"
+    ]
+  let byteOffset := YulExpr.call "mul" [elementWordIndex, YulExpr.lit 32]
+  YulStmt.funcDef helperName ["data_offset", "length", "index", "element_words", "word_offset"] ["word"] [
+    YulStmt.if_ (YulExpr.call "iszero" [
+      YulExpr.call "lt" [YulExpr.ident "index", YulExpr.ident "length"]
+    ]) [
+      YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
+    ],
+    YulStmt.assign "word" (YulExpr.call loadOp [
+      YulExpr.call "add" [
+        YulExpr.ident "data_offset",
+        byteOffset
+      ]
+    ])
+  ]
+
+def checkedArrayElementWordCalldataHelper : YulStmt :=
+  checkedArrayElementWordHelper checkedArrayElementWordCalldataHelperName "calldataload"
+
+def checkedArrayElementWordMemoryHelper : YulStmt :=
+  checkedArrayElementWordHelper checkedArrayElementWordMemoryHelperName "mload"
+
 def checkedStorageArrayElementHelper : YulStmt :=
   YulStmt.funcDef checkedStorageArrayElementHelperName ["slot", "index"] ["word"] [
     YulStmt.let_ "__array_len" (YulExpr.call "sload" [YulExpr.ident "slot"]),

Compiler/CompilationModel/ExpressionCompile.lean

@@ -257,6 +257,23 @@ def compileExpr (fields : List Field)
         YulExpr.ident s!"{name}_length",
         indexExpr
       ])
+  | Expr.arrayElementWord name index elementWords wordOffset => do
+      if elementWords == 0 then
+        throw s!"Compilation error: Expr.arrayElementWord '{name}' requires elementWords > 0"
+      else if wordOffset >= elementWords then
+        throw s!"Compilation error: Expr.arrayElementWord '{name}' wordOffset {wordOffset} is outside element width {elementWords}"
+      else
+        let indexExpr ← compileExpr fields dynamicSource index
+        let helperName := match dynamicSource with
+          | .calldata => checkedArrayElementWordCalldataHelperName
+          | .memory => checkedArrayElementWordMemoryHelperName
+        pure (YulExpr.call helperName [
+          YulExpr.ident s!"{name}_data_offset",
+          YulExpr.ident s!"{name}_length",
+          indexExpr,
+          YulExpr.lit elementWords,
+          YulExpr.lit wordOffset
+        ])
   | Expr.storageArrayLength field =>
       match findFieldWithResolvedSlot fields field with
       | some (f, slot) =>

Compiler/CompilationModel/LogicalPurity.lean

@@ -19,7 +19,8 @@ partial def exprContainsCallLike (expr : Expr) : Bool :=
   | Expr.structMember2 _ key1 key2 _ =>
       exprContainsCallLike key1 || exprContainsCallLike key2
   | Expr.storageArrayElement _ index
-  | Expr.arrayElement _ index =>
+  | Expr.arrayElement _ index
+  | Expr.arrayElementWord _ index _ _ =>
       exprContainsCallLike index
   | Expr.dynamicBytesEq _ _ =>
       false
@@ -110,7 +111,8 @@ def exprContainsUnsafeLogicalCallLike (expr : Expr) : Bool :=
   | Expr.mapping2 _ key1 key2 | Expr.mapping2Word _ key1 key2 _
   | Expr.structMember2 _ key1 key2 _ =>
       exprContainsUnsafeLogicalCallLike key1 || exprContainsUnsafeLogicalCallLike key2
-  | Expr.storageArrayElement _ index | Expr.arrayElement _ index | Expr.returndataOptionalBoolAt index =>
+  | Expr.storageArrayElement _ index | Expr.arrayElement _ index
+  | Expr.arrayElementWord _ index _ _ | Expr.returndataOptionalBoolAt index =>
       exprContainsUnsafeLogicalCallLike index
   | Expr.dynamicBytesEq _ _ =>
       false
@@ -152,7 +154,8 @@ termination_by es => sizeOf es
 decreasing_by all_goals simp_wf; all_goals omega
 
 def stmtContainsUnsafeLogicalCallLike : Stmt → Bool
-  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value |
+  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
+  | Stmt.setStorageWord _ _ value |
     Stmt.storageArrayPush _ value |
     Stmt.return value | Stmt.require value _ =>
       exprContainsUnsafeLogicalCallLike value

Compiler/CompilationModel/ParamLoading.lean

@@ -15,6 +15,12 @@ def isScalarParamType : ParamType → Bool
   | ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 => true
   | _ => false
 
+private def dynamicArrayElementStrideWords (elemTy : ParamType) : Nat :=
+  if isDynamicParamType elemTy then
+    1
+  else
+    max 1 (paramHeadSize elemTy / 32)
+
 private def genDynamicParamLoads
     (loadWord : YulExpr → YulExpr) (sizeExpr : YulExpr) (headSize : Nat)
     (baseOffset : Nat) (name : String) (ty : ParamType) (headOffset : Nat) :
@@ -56,10 +62,11 @@ private def genDynamicParamLoads
           ]) [
             YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
           ]]
-    | ParamType.array _ =>
+    | ParamType.array elemTy =>
+        let elemWords := dynamicArrayElementStrideWords elemTy
         [YulStmt.if_ (YulExpr.call "gt" [
             YulExpr.ident s!"{name}_length",
-            YulExpr.call "div" [YulExpr.ident tailRemainingName, YulExpr.lit 32]
+            YulExpr.call "div" [YulExpr.ident tailRemainingName, YulExpr.lit (32 * elemWords)]
           ]) [
             YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
           ]]

Compiler/CompilationModel/ScopeValidation.lean

@@ -131,6 +131,26 @@ def validateScopedExprIdentifiers
       | none =>
           throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElement"
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index
+  | Expr.arrayElementWord name index elementWords wordOffset => do
+      if elementWords == 0 then
+        throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' requires elementWords > 0"
+      else if wordOffset >= elementWords then
+        throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' wordOffset {wordOffset} is outside element width {elementWords}"
+      match findParamType params name with
+      | some ty@(ParamType.array elemTy) =>
+          if isDynamicParamType elemTy then
+            throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' requires an array parameter with static ABI-word elements, got {repr ty}"
+          else
+            let expectedWords := paramHeadSize elemTy / 32
+            if elementWords == expectedWords then
+              pure ()
+            else
+              throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' element width {elementWords} does not match ABI width {expectedWords} for {repr ty}"
+      | some ty =>
+          throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' requires array parameter, got {repr ty}"
+      | none =>
+          throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementWord"
+      validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index
   | Expr.mapping _ key | Expr.mappingWord _ key _ | Expr.mappingPackedWord _ key _ _ | Expr.mappingUint _ key
   | Expr.structMember _ key _ =>
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key
@@ -263,7 +283,8 @@ def validateScopedStmtIdentifiers
         throw s!"Compilation error: {context} assigns to undeclared local variable '{name}'"
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value
       pure localScope
-  | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.return value | Stmt.require value _ => do
+  | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value
+  | Stmt.return value | Stmt.require value _ => do
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value
       pure localScope
   | Stmt.storageArrayPush _ value => do