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/Compile.lean

@@ -126,6 +126,16 @@ 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 :=
+            if wordOffset == 0 then YulExpr.lit slot
+            else YulExpr.call "add" [YulExpr.lit slot, YulExpr.lit wordOffset]
+          pure [YulStmt.expr (YulExpr.call "sstore" [slotExpr, valueExpr])]
+      | 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,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
@@ -390,7 +390,11 @@ def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Exce
   let internalFuncDefs ← internalFns.mapM (compileInternalFunction fields spec.events spec.errors spec.adtTypes)
   let arrayElementHelpers :=
     if arrayHelpersRequired then
-      [checkedArrayElementCalldataHelper, checkedArrayElementMemoryHelper]
+      [ checkedArrayElementCalldataHelper
+      , checkedArrayElementMemoryHelper
+      , checkedArrayElementWordCalldataHelper
+      , checkedArrayElementWordMemoryHelper
+      ]
     else
       []
   let storageArrayElementHelpers :=

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 :=
+  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",
+        YulExpr.call "mul" [
+          YulExpr.call "add" [
+            YulExpr.call "mul" [YulExpr.ident "index", YulExpr.ident "element_words"],
+            YulExpr.ident "word_offset"
+          ],
+          YulExpr.lit 32
+        ]
+      ]
+    ])
+  ]
+
+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

@@ -56,10 +56,12 @@ private def genDynamicParamLoads
           ]) [
             YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
           ]]
-    | ParamType.array _ =>
+    | ParamType.array elemTy =>
+        let elemWords :=
+          if isDynamicParamType elemTy then 1 else paramHeadSize elemTy / 32
         [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,18 @@ 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 (ParamType.array _) => pure ()
+      | 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 +275,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

Compiler/CompilationModel/TrustSurface.lean

@@ -147,6 +147,7 @@ private partial def collectLowLevelStmtMechanics : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>
@@ -211,6 +212,7 @@ private partial def collectAxiomatizedStmtPrimitives : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>
@@ -296,6 +298,7 @@ private partial def collectUnguardedLowLevelStmtMechanics : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>
@@ -470,6 +473,7 @@ private partial def collectEventEmissionStmtMechanics : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>
@@ -629,6 +633,7 @@ private partial def collectRuntimeIntrospectionStmtMechanics : Stmt → List Str
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>
@@ -776,6 +781,7 @@ private partial def collectExternalStmtNames : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value
   | .require value _ =>

Compiler/CompilationModel/Types.lean

@@ -338,6 +338,10 @@ inductive Expr
   | internalCall (functionName : String) (args : List Expr)  -- Internal function call (#181)
   | arrayLength (name : String)  -- Length of a dynamic array parameter (#180)
   | arrayElement (name : String) (index : Expr)  -- Checked element access of a dynamic array parameter (revert on out-of-range) (#180)
+  /-- Checked word access inside a dynamic array element.  `elementWords` is the
+      static ABI word width of one element and `wordOffset` is the word inside
+      that element.  This supports arrays of static tuple/struct-like values. -/
+  | arrayElementWord (name : String) (index : Expr) (elementWords wordOffset : Nat)
   | storageArrayLength (field : String)  -- Read the length word of a storage dynamic array (#1571)
   | storageArrayElement (field : String) (index : Expr)  -- Checked element access of a storage dynamic array (#1571)
   /-- Equality on direct `bytes` / `string` parameters loaded from calldata or memory.
@@ -413,6 +417,10 @@ inductive Stmt
   | assignVar (name : String) (value : Expr)  -- Reassign existing variable
   | setStorage (field : String) (value : Expr)
   | setStorageAddr (field : String) (value : Expr)
+  /-- Write a full storage word at `field.slot + wordOffset`.  Intended for
+      migration-faithful manual packed-word writes where the source constructs
+      the packed word explicitly. -/
+  | setStorageWord (field : String) (wordOffset : Nat) (value : Expr)
   | storageArrayPush (field : String) (value : Expr)  -- Append to a storage dynamic array (#1571)
   | storageArrayPop (field : String)  -- Pop from a storage dynamic array (#1571)
   | setStorageArrayElement (field : String) (index : Expr) (value : Expr)  -- Indexed write (#1571)