Finalize native EVMYulLean proof boundary cleanup

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

@@ -1,10 +1,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 native transition harness still
-# builds, emitted dispatcher native/reference oracle coverage still passes, the
+# satisfies Verity's bridge assumptions: the fork audit and native lowering
+# report artifacts are in sync, all universal bridge lemmas still build, the
+# native transition harness still builds, emitted dispatcher native coverage still passes, the
 # public EndToEnd EVMYulLean target still builds, and all 0 concrete
 # `native_decide` bridge-equivalence tests still pass.
 #
@@ -29,7 +28,7 @@ on:
       - 'artifacts/evmyullean_fork_audit.json'
       - 'artifacts/evmyullean_adapter_report.json'
       - 'lake-manifest.json'
-      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanAdapter.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
@@ -48,7 +47,7 @@ on:
       - 'artifacts/evmyullean_fork_audit.json'
       - 'artifacts/evmyullean_adapter_report.json'
       - 'lake-manifest.json'
-      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanAdapter.lean'
+      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
@@ -122,7 +121,7 @@ jobs:
               "make test-evmyullean-fork",
               "```",
               "",
-              "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."
+              "This guard checks the pinned EVMYulLean fork audit, checks the native lowering report, rebuilds the native transition harness, and the public EndToEnd target, and runs the concrete bridge-equivalence tests."
             ];
             const body = bodyLines.join("\n");
 

AUDIT.md

@@ -10,8 +10,8 @@ boundary checks change.
 - Lean proof placeholders: 0 `sorry` in compiler/proof modules.
 - Project-level Lean axioms: 0. See `AXIOMS.md`.
 - Authoritative safe-body Yul runtime target: pinned `lfglabs-dev/EVMYulLean`.
-- Legacy custom Yul execution files are retained as a reference oracle under
-  `Compiler/Proofs/YulGeneration/ReferenceOracle/`.
+- The previous reference-comparison modules have been removed from the live
+  proof tree; native EVMYulLean is the checked runtime boundary.
 - Yul-to-bytecode compilation remains trusted through pinned `solc` 0.8.33.
 - Gas safety is not modeled by the semantic preservation theorems.
 
@@ -20,16 +20,15 @@ boundary checks change.
 Status: full semantic integration for safe compiler-produced bodies.
 
 The EVMYulLean transition moved the safe-body EndToEnd runtime target from
-Verity's custom Yul builtin semantics to `interpretYulRuntimeWithBackend
-.evmYulLean`. The current proof surface has:
+Verity-owned Yul builtin scaffolding to native EVMYulLean runtime execution.
+The current proof surface has:
 
 - 36 of 36 builtin bridge theorems proven.
 - 0 admitted bridge lemmas.
 - `smod` and `sar` bridge equivalences fully discharged.
 - `compileStmtList_always_bridged` proven for `BridgedSafeStmts`.
-- Public `layers2_3_ir_matches_yul_evmYulLean` wrappers that derive raw
-  `BridgedStmts` body witnesses from `SupportedSpec`, static parameter
-  witnesses, and source-level safe-body witnesses.
+- Public native EndToEnd wrappers whose runtime target is
+  `EvmYul.Yul.callDispatcher`.
 
 The external-call/function-table family
 (`internalCall`, `internalCallAssign`, `externalCallBind`, and `ecm`) now has

Compiler.lean

@@ -37,6 +37,5 @@ import Compiler.Proofs.IRGeneration.FunctionBody
 import Compiler.Proofs.IRGeneration.ParamLoading
 import Compiler.Proofs.IRGeneration.SupportedSpec
 import Compiler.Proofs.IRGeneration.SourceSemantics
-import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
 import Compiler.Proofs.YulGeneration.PatchRulesProofs
 import Compiler.Proofs.EndToEnd

Compiler/CompilationModel/TrustSurface.lean

@@ -588,6 +588,7 @@ def collectProxyUpgradeabilityMechanics (spec : CompilationModel) : List String
 private partial def collectRuntimeIntrospectionExprMechanics : Expr → List String
   | .contractAddress => ["contractAddress"]
   | .chainid => ["chainid"]
+  | .selfBalance => ["selfBalance"]
   | .blockNumber => ["blockNumber"]
   | .blobbasefee => ["blobbasefee"]
   | .externalCall _ args

Compiler/CompileDriverTest.lean

@@ -393,6 +393,22 @@ private def runtimeIntrospectionTrustSurfaceSpec : CompilationModel := {
   ]
 }
 
+private def selfBalanceTrustSurfaceSpec : CompilationModel := {
+  name := "SelfBalanceTrustSurface"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "currentBalance"
+      params := []
+      returnType := none
+      returns := [ParamType.uint256]
+      body := [
+        Stmt.returnValues [Expr.selfBalance]
+      ]
+    }
+  ]
+}
+
 private def blobbasefeeTrustSurfaceSpec : CompilationModel := {
   name := "BlobbasefeeTrustSurface"
   fields := []
@@ -1371,6 +1387,18 @@ unsafe def runTests : IO Unit := do
     throw (IO.userError "✗ verbose trust report localizes partially modeled runtime-introspection primitives")
   IO.println "✓ trust report surfaces partially modeled runtime-introspection primitives"
 
+  let selfBalanceTrustReport := emitTrustReportJson [selfBalanceTrustSurfaceSpec]
+  if !contains selfBalanceTrustReport "\"contract\":\"SelfBalanceTrustSurface\"" then
+    throw (IO.userError "✗ selfBalance trust report emits contract name")
+  if !contains selfBalanceTrustReport "\"partiallyModeledRuntimeIntrospection\":[\"selfBalance\"]" then
+    throw (IO.userError "✗ selfBalance trust report emits partially modeled runtime-introspection primitive")
+  if !contains selfBalanceTrustReport "\"usageSites\":[{\"kind\":\"function\",\"name\":\"currentBalance\",\"modeledLowLevelMechanics\":[],\"notModeledEventEmission\":[],\"notModeledProxyUpgradeability\":[],\"partiallyModeledLinearMemoryMechanics\":[],\"partiallyModeledRuntimeIntrospection\":[\"selfBalance\"]" then
+    throw (IO.userError "✗ selfBalance trust report localizes partially modeled runtime-introspection primitive")
+  let selfBalanceVerboseUsageSiteReport := String.intercalate "\n" (emitVerboseUsageSiteLines [selfBalanceTrustSurfaceSpec])
+  if !contains selfBalanceVerboseUsageSiteReport "partially modeled runtime introspection: selfBalance" then
+    throw (IO.userError "✗ verbose trust report localizes selfBalance runtime-introspection primitive")
+  IO.println "✓ trust report surfaces selfBalance runtime-introspection boundary"
+
   let axiomatizedPrimitiveUsageSiteLines := emitAxiomatizedPrimitiveUsageSiteLines [trustSurfaceSpec]
   let axiomatizedPrimitiveUsageSiteReport := String.intercalate "\n" axiomatizedPrimitiveUsageSiteLines
   if !contains axiomatizedPrimitiveUsageSiteReport "- TrustSurfaceSmoke [function:exercise]: keccak256" then
@@ -1788,6 +1816,17 @@ unsafe def runTests : IO Unit := do
     throw (IO.userError "✗ denied runtime-introspection compile still writes trust report file")
   IO.println "✓ denied runtime-introspection compile still writes trust report file"
 
+  -- Regression for issue #1836: selfBalance lowers to selfbalance(), whose
+  -- account-balance bridge is not yet proved in the native proof stack.
+  -- Strict runtime-introspection mode must reject it instead of accepting an
+  -- assumption-empty artifact.
+  let deniedSelfBalanceRuntimeReportPath := s!"{trustReportDir}/trust-report-denied-selfbalance-runtime.json"
+  expectFailureContains
+    "compileSpecsWithOptions rejects selfBalance under deny-runtime-introspection"
+    (compileSpecsWithOptions
+      [selfBalanceTrustSurfaceSpec] outDir false [] {} none (some deniedSelfBalanceRuntimeReportPath) none none false false false false false false false true false)
+    "Partially modeled runtime-introspection mechanics remain:\n- SelfBalanceTrustSurface [function:currentBalance]: selfBalance"
+
   -- Regression for issue #1829: blobbasefee must fail closed under
   -- --deny-runtime-introspection because the proof interpreters do not
   -- model the post-Dencun environment opcode.

Compiler/Proofs/EndToEnd.lean

@@ -30,7 +30,7 @@
 
 Historical EVMYulLean backend-fuel retargeting lemmas remain isolated outside
 this public theorem spine; this file no longer exposes or composes EndToEnd
-wrappers over that proof-interpreter target.
+wrappers over that older transition target.
 
   Run: lake build Compiler.Proofs.EndToEnd
 -/
@@ -79,7 +79,7 @@ the native harness' materialized-storage boundary. -/
 def sourceResultMatchesNativeOn
     (observableSlots : List Nat)
     (source : SourceSemantics.SourceContractResult)
-    (native : Except Compiler.Proofs.YulGeneration.Backends.AdapterError YulResult) :
+    (native : Except Compiler.Proofs.YulGeneration.Backends.NativeLoweringError YulResult) :
     Prop :=
   match native with
   | .ok yul =>
@@ -98,7 +98,7 @@ private theorem sourceResultMatchesNativeOn_of_sourceResultMatchesIRResult_of_na
     {observableSlots : List Nat}
     {source : SourceSemantics.SourceContractResult}
     {ir : IRResult}
-    {native : Except Compiler.Proofs.YulGeneration.Backends.AdapterError YulResult}
+    {native : Except Compiler.Proofs.YulGeneration.Backends.NativeLoweringError YulResult}
     (hSourceIR :
       Compiler.Proofs.IRGeneration.FunctionBody.sourceResultMatchesIRResult
         source ir)
@@ -403,7 +403,7 @@ noncomputable def nativeGeneratedCallDispatcherResultOf
     (state : IRState)
     (observableSlots : List Nat)
     (nativeContract : EvmYul.Yul.Ast.YulContract) :
-    Except Compiler.Proofs.YulGeneration.Backends.AdapterError YulResult :=
+    Except Compiler.Proofs.YulGeneration.Backends.NativeLoweringError YulResult :=
   let fuel := Nat.succ (sizeOf (Compiler.emitYul contract).runtimeCode)
   let initial :=
     Compiler.Proofs.YulGeneration.Backends.Native.initialState nativeContract
@@ -457,7 +457,7 @@ theorem nativeResultsMatchOn_interpretIR_of_execIRFunction_guards
     (state : IRState)
     (observableSlots : List Nat)
     (fn : IRFunction)
-    (native : Except Compiler.Proofs.YulGeneration.Backends.AdapterError
+    (native : Except Compiler.Proofs.YulGeneration.Backends.NativeLoweringError
       YulResult)
     (hFind :
       contract.functions.find? (fun fn => fn.selector == tx.functionSelector) =
@@ -484,7 +484,7 @@ theorem nativeResultsMatchOn_interpretIR_of_execIRFunction_dispatchGuards
     (state : IRState)
     (observableSlots : List Nat)
     (fn : IRFunction)
-    (native : Except Compiler.Proofs.YulGeneration.Backends.AdapterError
+    (native : Except Compiler.Proofs.YulGeneration.Backends.NativeLoweringError
       YulResult)
     (hFind :
       contract.functions.find? (fun fn => fn.selector == tx.functionSelector) =
@@ -6837,9 +6837,9 @@ private theorem nativeGeneratedCallDispatcherResultOf_eq_interpretIRRuntimeNativ
       irContract tx state observableSlots nativeContract
       (generatedRuntimeNativeFragment_of_compile_ok_supported hCompile hSupported)
       hLower hEnv
-  rw [hInterp]
   simp [nativeGeneratedCallDispatcherResultOf, Compiler.emitYul,
     Compiler.runtimeCode, Compiler.CodegenCommon.emitYul]
+  exact hInterp.symm
 
 private theorem nativeGeneratedCallDispatcherResultOf_eq_interpretIRRuntimeNative_of_lowerRuntimeContractNative_supported_except_mapping_writes_stmt_safety
     {spec : CompilationModel.CompilationModel} {selectors : List Nat}
@@ -6869,9 +6869,9 @@ private theorem nativeGeneratedCallDispatcherResultOf_eq_interpretIRRuntimeNativ
       (generatedRuntimeNativeFragment_of_compile_ok_supported_except_mapping_writes_stmt_safety
         hCompile hSupported hSafety)
       hLower hEnv
-  rw [hInterp]
   simp [nativeGeneratedCallDispatcherResultOf, Compiler.emitYul,
     Compiler.runtimeCode, Compiler.CodegenCommon.emitYul]
+  exact hInterp.symm
 
 /-- Source-level compiler correctness over the direct projected
 `EvmYul.Yul.callDispatcher` result.
@@ -33373,7 +33373,7 @@ private theorem simpleStorageNativeRuntimeDispatcherStmts_exists_init_block :
             simpa [Compiler.CodegenCommon.initFreeMemoryPointer,
               Compiler.CodegenCommon.buildSwitch, simpleStorageBuildSwitchBody,
               simpleStorageBuildSwitchSourceCases] using hInner
-          have hBad : (Except.error err : Except AdapterError
+          have hBad : (Except.error err : Except NativeLoweringError
               (List EvmYul.Yul.Ast.Stmt × Nat)) = .ok (lowered, finalNext) := by
             have hInnerMap :
                 Compiler.Proofs.YulGeneration.Backends.lowerStmtsNativeWithSwitchIds
@@ -33494,9 +33494,9 @@ private theorem simpleStorageNativeRuntimeDispatcherStmts_exists_init_block :
                          Yul.YulExpr.lit 128])),
                   EvmYul.Yul.Ast.Stmt.Block inner],
                  innerNext) :
-                Except AdapterError (List EvmYul.Yul.Ast.Stmt × Nat)) =
+                Except NativeLoweringError (List EvmYul.Yul.Ast.Stmt × Nat)) =
                 (Except.ok (lowered, finalNext) :
-                  Except AdapterError (List EvmYul.Yul.Ast.Stmt × Nat)) := by
+                  Except NativeLoweringError (List EvmYul.Yul.Ast.Stmt × Nat)) := by
             have hInnerMap :
                 Compiler.Proofs.YulGeneration.Backends.lowerStmtsNativeWithSwitchIds
                   (Compiler.Proofs.YulGeneration.Backends.yulStmtsIdentifierNames
@@ -41377,10 +41377,10 @@ theorem simpleStorage_source_endToEnd_native_evmYulLean_of_sourceIR
 /-! ## Universal Pure Arithmetic Bridge
 
 The pure arithmetic bridge proofs (`pure_add_bridge`, etc.) were removed
-after the legacy builtin dispatch grew `callvalue`/`calldatasize`
-support, making the old monolithic wrapper too large for the default
+after the older builtin-routing wrapper grew `callvalue`/`calldatasize`
+support, making the monolithic wrapper too large for the default
 heartbeat limit during type-checking. The proofs were mathematically
-correct but need the legacy builtin dispatch to be factored into smaller
+correct but need that builtin-routing surface to be factored into smaller
 pieces before they can be re-stated without timeout.
 
 See: `ArithmeticProfile.lean` and
@@ -41394,8 +41394,7 @@ The public native theorem surface in this file targets the direct projected
 `EvmYul.Yul.callDispatcher` result through `nativeGeneratedCallDispatcherResultOf`.
 The older `nativeIRRuntimeMatchesIR` and generated dispatcher-exec theorem
 families remain file-local transition evidence. EndToEnd no longer defines
-compatibility wrappers over the older backend-parameterized proof-interpreter
-surface.
+compatibility wrappers over the older backend-parameterized transition surface.
 
 The private retargeting module that previously recorded bridge-history facts
 has been removed (DoD 5 of the EVMYulLean transition).
@@ -41423,7 +41422,7 @@ expose the public surface this file needs.
   and execute equivalently under the EVMYulLean backend when the IR bodies it
   embeds satisfy `BridgedStmt`.
 - Layer 3 no longer keeps EndToEnd compatibility lemmas targeting the
-  proof-interpreter EVMYulLean backend; the public EndToEnd theorem family
+  older EVMYulLean backend-fuel surface; the public EndToEnd theorem family
   targets native dispatcher execution through the direct projected
   `nativeGeneratedCallDispatcherResultOf` result.
 - The historical Verity-backed public oracle-routed EndToEnd wrappers
@@ -41461,10 +41460,10 @@ expose the public surface this file needs.
   and needs separate simulation work before it can be admitted into the
   safe-body EndToEnd wrapper.
 
-The Phase 4 retargeting module has been removed; the equivalent
-proof-interpreter-backed retargeting theorems are no longer needed because the
-public EndToEnd surface targets EVMYulLean's native dispatcher execution
-directly via `nativeGeneratedCallDispatcherResultOf`.
+The Phase 4 retargeting module has been removed; the equivalent backend-fuel
+retargeting theorems are no longer needed because the public EndToEnd surface
+targets EVMYulLean's native dispatcher execution directly via
+`nativeGeneratedCallDispatcherResultOf`.
 -/
 
 end Compiler.Proofs.EndToEnd

Compiler/Proofs/IRGeneration/IRInterpreter.lean

@@ -1056,7 +1056,7 @@ These are the IR-side companions to `NativePreservableStraightStmt`
 We use **option (b)** of the Layer A design: inline an IR-side analog predicate
 (`IRStmtPreservesObs`) here so that this module does not
 need to import the native-harness file (which would form a cycle via
-`Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter` →
+`Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness` →
 `Compiler.Proofs.IRGeneration.IRStorageWord`). The cross-cast from
 `NativePreservableStraightStmt` to `IRStmtPreservesObs` is deferred to
 `Compiler/Proofs/EndToEnd.lean` (Layer D's responsibility per the plan). -/