Clarify native EVMYulLean boundary wording

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

@@ -22,11 +22,11 @@ on:
       - '.github/workflows/evmyullean-fork-conformance.yml'
       - 'Makefile'
       - 'Compiler/Proofs/EndToEnd.lean'
-      - 'scripts/generate_evmyullean_adapter_report.py'
+      - 'scripts/generate_evmyullean_native_lowering_report.py'
       - 'scripts/generate_evmyullean_fork_audit.py'
       - 'scripts/test_evmyullean_fork_conformance_workflow.py'
       - 'artifacts/evmyullean_fork_audit.json'
-      - 'artifacts/evmyullean_adapter_report.json'
+      - 'artifacts/evmyullean_native_lowering_report.json'
       - 'lake-manifest.json'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
@@ -41,11 +41,11 @@ on:
       - '.github/workflows/evmyullean-fork-conformance.yml'
       - 'Makefile'
       - 'Compiler/Proofs/EndToEnd.lean'
-      - 'scripts/generate_evmyullean_adapter_report.py'
+      - 'scripts/generate_evmyullean_native_lowering_report.py'
       - 'scripts/generate_evmyullean_fork_audit.py'
       - 'scripts/test_evmyullean_fork_conformance_workflow.py'
       - 'artifacts/evmyullean_fork_audit.json'
-      - 'artifacts/evmyullean_adapter_report.json'
+      - 'artifacts/evmyullean_native_lowering_report.json'
       - 'lake-manifest.json'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
       - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'

.github/workflows/verify.yml

@@ -254,7 +254,7 @@ jobs:
           python3 scripts/generate_layer2_boundary_catalog.py
           python3 scripts/generate_verify_sync_spec.py
           python3 scripts/generate_evmyullean_capability_report.py
-          python3 scripts/generate_evmyullean_adapter_report.py
+          python3 scripts/generate_evmyullean_native_lowering_report.py
           python3 scripts/generate_print_axioms.py
           python3 scripts/sync_verification_status_doc.py
 

Compiler/Proofs/EndToEnd.lean

@@ -28,9 +28,8 @@
   `EvmYul.Yul.callDispatcher` execution through
   `Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness`.
 
-Historical EVMYulLean backend-fuel retargeting lemmas remain isolated outside
-this public theorem spine; this file no longer exposes or composes EndToEnd
-wrappers over that older transition target.
+The removed backend-fuel transition target is not part of this public theorem
+spine; this file composes only the native dispatcher result surface.
 
   Run: lake build Compiler.Proofs.EndToEnd
 -/
@@ -93,7 +92,7 @@ def sourceResultMatchesNativeOn
   | .error _ => False
 
 /-- Compose Layer 2 source-to-IR correctness with native EVMYulLean runtime
-correctness, without mentioning the legacy Yul interpreter. -/
+correctness. -/
 private theorem sourceResultMatchesNativeOn_of_sourceResultMatchesIRResult_of_nativeResultsMatchOn
     {observableSlots : List Nat}
     {source : SourceSemantics.SourceContractResult}
@@ -121,7 +120,7 @@ private theorem sourceResultMatchesNativeOn_of_sourceResultMatchesIRResult_of_na
       · exact hSourceEvents.trans hNativeEvents
 
 /-- File-local supported-compiler correctness theorem over native EVMYulLean
-runtime adapter execution.
+runtime execution.
 
 The theorem target is the native runtime harness backed by
 `EvmYul.Yul.callDispatcher`; the only Layer 3 premise is a direct native-vs-IR
@@ -20506,10 +20505,10 @@ private theorem NativeGeneratedSelectedUserBodyExecOnlyBridgeAtFuelRevived.of_br
 /-- Selected user bodies containing only `leave` execute as a native checkpoint
 and project to the same observable result as `execIRFunction`.
 
-The native interpreter records `leave` as a revivable checkpoint, while the
-legacy IR function interpreter treats it as a normal fall-through. After
-`reviveJump`, both paths have the same observable storage, return value, and
-events at the transaction-entry state. -/
+The native runtime records `leave` as a revivable checkpoint, while source-side
+IR execution observes the same fall-through result after `reviveJump`. Both
+paths have the same observable storage, return value, and events at the
+transaction-entry state. -/
 private theorem nativeResultsMatchOn_execIRFunction_leave_body_markedPrefix
     (irContract : IRContract)
     (tx : IRTransaction)
@@ -41396,8 +41395,8 @@ 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 transition surface.
 
-The private retargeting module that previously recorded bridge-history facts
-has been removed (DoD 5 of the EVMYulLean transition).
+The private backend-fuel transition module that previously recorded
+bridge-history facts has been removed (DoD 5 of the EVMYulLean transition).
 The file-local `runtimeCode_bridged_local` lemma in this module retains the
 emitted-runtime closure witness, and the SupportedSpec-discharged variants
 `emitYul_runtimeCode_bridged_of_compile_ok_supported` and
@@ -41460,9 +41459,9 @@ 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 backend-fuel
-retargeting theorems are no longer needed because the public EndToEnd surface
-targets EVMYulLean's native dispatcher execution directly via
+The Phase 4 backend-fuel module has been removed; the equivalent transition
+theorems are no longer needed because the public EndToEnd surface targets
+EVMYulLean's native dispatcher execution directly via
 `nativeGeneratedCallDispatcherResultOf`.
 -/
 

Compiler/Proofs/README.md

@@ -9,7 +9,7 @@ See [TRUST_ASSUMPTIONS.md](../../TRUST_ASSUMPTIONS.md) for the full trust bounda
 
 - **Layer 1: EDSL = CompilationModel** -- Frontend semantic bridge. Generic typed-IR core in [`TypedIRCompilerCorrectness.lean`](../../Compiler/TypedIRCompilerCorrectness.lean); contract-level bridges are per-contract.
 - **Layer 2: CompilationModel -> IR** -- Generic whole-contract theorem in [`Contract.lean`](IRGeneration/Contract.lean). 0 sorry, 0 axioms.
-- **Native Layer 3: IR -> native EVMYulLean** -- Runtime lowering and dispatcher execution through [`YulGeneration/Backends/EvmYulLeanNativeHarness.lean`](YulGeneration/Backends/EvmYulLeanNativeHarness.lean), composed in [`EndToEnd.lean`](EndToEnd.lean). The public Layer 3 theorem target is native EVMYulLean; retained reference-oracle code is builtin comparison scaffolding below that trust boundary.
+- **Native Layer 3: IR -> native EVMYulLean** -- Runtime lowering and dispatcher execution through [`YulGeneration/Backends/EvmYulLeanNativeHarness.lean`](YulGeneration/Backends/EvmYulLeanNativeHarness.lean), composed in [`EndToEnd.lean`](EndToEnd.lean). The public Layer 3 theorem target is native EVMYulLean; the old builtin comparison path has been removed.
 
 All three layers carry zero project-specific axioms.
 

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean

@@ -16489,9 +16489,9 @@ theorem compileStmtList_mappingPackedWordMultiSlotNonzero_noFuncDefs
 /-!
 ## Universal safe-body closure
 
-`BridgedSafeStmts` is the source-level whitelist used by the EVMYulLean
-retargeting report: it collects the statement-list fragments that this module
-has proved to compile into `BridgedStmts`. The external-call family
+`BridgedSafeStmts` is the source-level whitelist used by the EVMYulLean native
+lowering report: it collects the statement-list fragments that this module has
+proved to compile into `BridgedStmts`. The external-call family
 (`internalCall`, `internalCallAssign`, `externalCallBind`, and `ecm`) is
 intentionally absent; those statements still need function-table simulation
 before they can be discharged without explicit hypotheses.

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean

@@ -11,7 +11,7 @@ open Compiler.Proofs.IRGeneration (IRStorageWord IRStorageSlot)
 /-!
 Native EVMYulLean builtin routing facts.
 
-The historical reference-oracle comparison layer has been removed. These lemmas
+The historical builtin-comparison layer has been removed. These lemmas
 record only the native `.evmYulLean` dispatch surface used by the public
 EndToEnd target and by reporting scripts that audit available builtin coverage.
 -/

Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean

@@ -2,7 +2,7 @@
   EvmYulLeanBridgeTest: compile-time smoke checks for the native EVMYulLean
   builtin surface.
 
-  The old Verity reference-oracle comparison target has been removed. These
+  The old Verity builtin-comparison target has been removed. These
   tests now exercise direct native dispatch and selected boundary values.
 
   Run: lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest

Compiler/Proofs/YulGeneration/IRFuel.lean

@@ -8,9 +8,9 @@ open Compiler.Yul
 
 /-! ## Fuel-Parametric IR Aliases
 
-These names are shared by the source-to-IR proof stack and the legacy IR/Yul
-equivalence stack. They are intentionally kept free of the reference-oracle Yul
-interpreter so IR-generation compiler-correctness modules do not need to import
+These names are shared by the source-to-IR proof stack and Yul-facing proof
+modules. They are intentionally kept free of Yul execution dependencies so
+IR-generation compiler-correctness modules do not need to import
 `Compiler.Proofs.YulGeneration.Equivalence` just to talk about fuel-indexed IR
 execution.
 -/

Makefile

@@ -109,7 +109,7 @@ test-evmyullean-fork: ## Probe EVMYulLean fork conformance (audit + native lower
 	@echo "Checking EVMYulLean fork pin + drift audit..."
 	python3 scripts/generate_evmyullean_fork_audit.py --check
 	@echo "Checking EVMYulLean native lowering report..."
-	python3 scripts/generate_evmyullean_adapter_report.py --check
+	python3 scripts/generate_evmyullean_native_lowering_report.py --check
 	@echo "Building EVMYulLean bridge lemmas, native harness, and 0 concrete bridge tests..."
 	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
 	lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest
@@ -154,7 +154,7 @@ check: ## Run local CI-equivalent checks job (no Lean build, no solc)
 	python3 scripts/check_yul.py --builtin-boundary-only
 	python3 scripts/check_rewrite_proof_metadata.py
 	python3 scripts/generate_evmyullean_capability_report.py --check
-	python3 scripts/generate_evmyullean_adapter_report.py --check
+	python3 scripts/generate_evmyullean_native_lowering_report.py --check
 	python3 scripts/generate_evmyullean_fork_audit.py --check
 	python3 scripts/generate_print_axioms.py --check
 	python3 scripts/check_proof_length.py

artifacts/COMPILER_ARTIFACTS.md

@@ -11,7 +11,7 @@ This folder collects compiler artifacts and fixtures used by tests, CI, and docu
 - `lean_warning_baseline.json`: Lean warning regression baseline. Consumed by `scripts/check_lean_warning_regression.py`.
 - `interpreter_feature_matrix.json`: Machine-readable interpreter feature support matrix.
 - `evmyullean_capability_report.json`: EVMYulLean builtin coverage report. Generated by `scripts/generate_evmyullean_capability_report.py`.
-- `evmyullean_adapter_report.json`: EVMYulLean native lowering and bridge report.
+- `evmyullean_native_lowering_report.json`: EVMYulLean native lowering and bridge report.
 - `evmyullean_unsupported_nodes.json`: EVMYulLean unsupported AST node report.
 - `issue_1060_progress.json`: Issue #1060 migration tracking ledger (complete).
 

artifacts/evmyullean_adapter_report.json → artifacts/evmyullean_native_lowering_report.json

@@ -182,7 +182,7 @@
     "runtime_lowering": "present"
   },
   "native_lowering_file": "Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean",
-  "schema_version": 7,
+  "schema_version": 8,
   "status": "partial",
   "stmt_gap_messages": {
     "funcDef": [

docs/ARITHMETIC_PROFILE.md

@@ -157,7 +157,7 @@ The arithmetic model is invariant across profiles. See [`docs/SOLIDITY_PARITY_PR
 - **Gas semantics**: proofs establish result correctness, not gas cost or bounded liveness.
 - **Compiler-layer overflow detection**: the compiler does not insert overflow or division-by-zero checks. Use EDSL `safeAdd`/`safeSub`/`safeMul`/`safeDiv` for checked behavior.
 - **Cryptographic primitives**: keccak256 is axiomatized (see [`AXIOMS.md`](../AXIOMS.md)).
-- **Universal bridge equivalence**: 25/25 pure EVMYulLean-backed builtins have universal bridge lemmas. All 25 also have context-lifted backend bridge theorems for Phase 4 retargeting. All 8 higher-level expression operators also have proven compilation correctness.
+- **Universal bridge equivalence**: 25/25 pure EVMYulLean-backed builtins have universal bridge lemmas. All 25 also have context-lifted native bridge theorems. All 8 higher-level expression operators also have proven compilation correctness.
 
 ## Auditor Checklist
 

docs/IR_STORAGE_UINT256_REFACTOR.md

@@ -132,8 +132,8 @@ Deliverables:
 - `simpleStorage_endToEnd_native_evmYulLean` consumes the direct per-case
   splitter without a retrieve-hit premise.
 
-Status: complete for the public native theorem. The compatibility proof remains
-only for the generic fuel-wrapper/reference-oracle cleanup.
+Status: complete for the public native theorem. Any remaining compatibility
+proof references are historical notes, not public proof authority.
 
 ### Phase 3 — discharge store hit
 
@@ -150,16 +150,16 @@ Deliverables:
 - `simpleStorage_endToEnd_native_evmYulLean` consumes the direct per-case
   splitter without a store-hit premise.
 
-Status: complete for the public native theorem. The compatibility proof remains
-only for the generic fuel-wrapper/reference-oracle cleanup.
+Status: complete for the public native theorem. Any remaining compatibility
+proof references are historical notes, not public proof authority.
 
 ### Phase 4 — generalize and retire the per-case bridge surface
 
 Replace the per-contract SimpleStorage direct-match family with a generic,
 dispatcher-shape-driven bridge so future contracts inherit discharge
 automatically. The older non-`Match` SimpleStorage bridge family is
 compatibility-only and should disappear with the generic
-fuel-wrapper/reference-oracle cleanup.
+native-proof modularization cleanup.
 
 Deliverables:
 - Generic `nativeCallDispatcherBridge_of_typed_storage` lemma over the
@@ -174,8 +174,7 @@ Deliverables:
   `hStoreHit` premise and consumes
   `simpleStorageNativeCallDispatcherMatchBridge_of_per_case`.
 - `PrintAxioms` includes the direct match proofs for the public native theorem;
-  compatibility bridge proofs may remain only while the generic
-  fuel-wrapper/reference-oracle family remains.
+  compatibility bridge proofs are not part of the public native theorem.
 - `Contracts/SimpleStorage/Proofs/` spec theorems are unchanged.
 - A second contract (e.g. Counter) lifts to the native theorem under the
   generic Phase-4 surface without contract-specific bridge code.

docs/NATIVE_EVMYULLEAN_DONE_GRAPH.md

@@ -19,8 +19,9 @@ source DSL
 -> public end-to-end theorem
 ```
 
-The custom Verity Yul interpreter may remain as a regression oracle, but it
-must not carry the public theorem claim.
+The native EVMYulLean runtime is the sole theorem-facing Yul semantics for the
+public end-to-end claim; historical interpreter scaffolding is not a regression
+oracle for this boundary.
 
 ## Critical Path
 

docs/NATIVE_EVMYULLEAN_FULL_TRANSITION_DONE.md

@@ -10,11 +10,10 @@ EVMYulLean dispatcher execution. Removed transition evidence used to record a
 Verity-side Yul statement-interpreter path through the EVMYulLean-backed builtin
 backend.
 
-The removed transition theorem name
-`yulCodegen_preserves_semantics_evmYulLeanBackend_via_reference_oracle` marks
-the old shape that has now been deleted. The public compiler-correctness
-theorem targets native EVMYulLean execution directly through
-`EvmYul.Yul.callDispatcher`; that condition is satisfied on `main`.
+The removed backend-fuel theorem family marks the old shape that has now been
+deleted. The public compiler-correctness theorem targets native EVMYulLean
+execution directly through `EvmYul.Yul.callDispatcher`; that condition is
+satisfied on `main`.
 
 ## Current Baseline
 
@@ -27,8 +26,8 @@ The current baseline is:
   which executes through native EVMYulLean. Helper-free and mapping-helper
   generated-dispatcher wrappers consume concrete dispatcher lowering and build
   full emitted-runtime native lowering internally.
-- Lower Layer 3 transition modules no longer contain the reference-oracle
-  builtin comparison or the backend-parameterized builtin wrapper.
+- Lower Layer 3 transition modules no longer contain the old builtin
+  comparison path or the backend-parameterized builtin wrapper.
 - `simpleStorage_endToEnd_native_evmYulLean` is a concrete native theorem over
   the direct projected `EvmYul.Yul.callDispatcher` result, with no public
   retrieve-hit, store-hit, or selector-miss bridge premises.
@@ -49,8 +48,9 @@ CompilationModel
   -> public end-to-end theorem
 ```
 
-Historical differential tests may still compare against older execution paths,
-but the public semantic-preservation proof path must not depend on them.
+Differential tests may still compare generated code against external execution
+engines, but the public semantic-preservation proof path must not depend on an
+alternate Verity Yul interpreter.
 
 ## Non-Negotiable Completion Criteria
 
@@ -65,12 +65,12 @@ The transition is done only when all criteria in this section are true on
 - The theorem-facing native target is either `Native.interpretIRRuntimeNative`
   or a narrower wrapper that internally lowers to EVMYulLean and executes via
   `EvmYul.Yul.callDispatcher`.
-- No public theorem keeps a native-vs-custom-interpreter agreement premise such
+- No public theorem keeps a native-vs-alternate-interpreter agreement premise such
   as `nativeIRRuntimeAgreesWithEvmYulLeanFuelWrapper`,
   `nativeCallDispatcherAgreesWithEvmYulLeanFuelWrapper`, or an equivalent bridge
   assumption.
-- Any remaining comparison with older execution paths is explicitly marked as
-  differential testing, not as the authoritative proof target.
+- Any remaining comparison with non-proof execution engines is explicitly
+  marked as differential testing, not as the authoritative proof target.
 
 ### 2. Generated Fragment Characterization
 
@@ -160,18 +160,18 @@ The transition is done only when all criteria in this section are true on
 
 - `README.md`, `AUDIT.md`, `TRUST_ASSUMPTIONS.md`, and
   `docs/VERIFICATION_STATUS.md` describe native EVMYulLean as the
-  authoritative semantic target only after the theorem target has flipped.
-- Legacy custom-interpreter files are documented as reference-oracle or
-  regression infrastructure.
+  authoritative semantic target.
+- Removed alternate-interpreter paths do not appear in the checked-in proof tree
+  or theorem-facing reports.
 - EVMYulLean fork audit artifacts and capability reports are regenerated and
   checked.
 - The transition docs name all remaining excluded features and link them to
   issue-tracked scope decisions.
 
 ### 9. CI Enforcement
 
-- CI fails if the public compiler theorem drifts back to the custom
-  interpreter path.
+- CI fails if the public compiler theorem drifts away from the native
+  EVMYulLean dispatcher path.
 - CI checks the generated-fragment boundary, native transition docs, bridge
   coverage reports, fork audit artifacts, axiom report, proof-length metadata,
   and native smoke/regression tests.
@@ -212,14 +212,13 @@ Each PR should move exactly one durable boundary:
 4. Native statement/expression equivalence for one generated construct family.
 5. Dispatcher/native-switch preservation.
 6. Fuel sufficiency or fuel-parametric theorem layer.
-7. Generic native-vs-interpreter agreement for generated Yul.
-8. Public theorem target flip.
-9. CI/doc/trust-boundary cleanup after the flip.
-10. Legacy interpreter demotion or removal.
-
-Do not mix proof work with unrelated cleanup. Do not remove the custom
-interpreter until the public theorem target has flipped and at least one PR has
-kept it only as regression infrastructure.
+7. Fuel adequacy and native execution modularity for generated Yul.
+8. Public theorem target maintenance.
+9. CI/doc/trust-boundary cleanup after proof-boundary changes.
+10. Keep removed interpreter/adapter surfaces out of the public proof path.
+
+Do not mix proof work with unrelated cleanup. Do not reintroduce alternate
+interpreter paths as proof authority.
 
 ## Reusable Agent Prompt