Finalize native EVMYulLean proof boundary cleanup

[Th0rgal]

Summary

• remove the old structural EVMYulLean adapter module from the build root
• collapse the one-constructor builtin backend abstraction into direct native EVMYulLean context evaluation
• retarget EVMYulLean capability/native-lowering reports, workflow probes, docs, and tests to EvmYulLeanNativeLowering.lean / EvmYulLeanNativeHarness.lean
• remove dead backend-wrapper builtin lemmas from the proof inventory
• surface selfBalance as a partially modeled runtime-introspection boundary and reject it under --deny-runtime-introspection until the native account-balance bridge is proved
• refresh EVMYulLean transition docs to describe the current native-only proof boundary and remove stale adapter/reference-oracle/proof-interpreter wording
• fix native lowering capability gap detection so throw s!"..." branches, including inline funcDef, are reported instead of silently treated as complete

Validation

• lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBuiltinSemantics.lean
• lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean
• lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean
• lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean
• lake env lean Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean
• lake env lean Compiler/Proofs/EndToEnd.lean
• lake env lean PrintAxioms.lean
• lake build Compiler.CompileDriverTest
• lake build Compiler
• python3 -m unittest scripts/test_generate_evmyullean_adapter_report.py scripts/test_evmyullean_fork_conformance_workflow.py scripts/test_check_yul.py scripts/test_evmyullean_capability.py -v
• python3 scripts/generate_evmyullean_capability_report.py --check
• make check

Audit Notes

• stale-reference scan is clean for EvmYulLeanAdapter, evalBuiltinCallWithBackend, ReferenceOracle, reference oracle, proof-interpreter, and custom-Yul wording across live source, docs, scripts, workflows, and artifacts
• PrintAxioms.lean now reports 5162 theorems/lemmas and 0 sorry'd
• native capability reporting now marks inline funcDef statement lowering as a partial native lowering boundary; top-level runtime funcDef partitioning remains supported by lowerRuntimeContractNative

---

Note

Medium Risk
Medium risk because it removes/renames core proof-boundary components (adapter/backend wrapper) and retargets CI/artifacts to the native lowering path; mistakes could silently weaken conformance checks or break proof builds.

Overview
Finalizes the native EVMYulLean-only proof boundary by deleting the legacy structural adapter (EvmYulLeanAdapter.lean), collapsing the one-constructor BuiltinBackend/evalBuiltinCallWithBackend* indirection into direct evalBuiltinCallWithEvmYulLeanContext, and renaming error plumbing from AdapterError to NativeLoweringError across the native harness and EndToEnd theorem surface.

Updates trust-surface reporting to treat Expr.selfBalance as partially modeled runtime introspection (with new compile-driver tests that ensure --deny-runtime-introspection fails closed), and trims now-dead bridge lemmas/references from proof inventories.

Retargets CI/workflows, scripts, tests, and generated artifacts/documentation from “adapter” coverage to native lowering coverage (EvmYulLeanNativeLowering.lean/EvmYulLeanNativeHarness.lean), including improved gap detection that recognizes throw s!"..." branches and reporting funcDef as a native lowering gap in the capability/unsupported-node reports.

^{Reviewed by Cursor Bugbot for commit 5fbf9b5. Bugbot is set up for automated code reviews on this repo. Configure here.}

Fixes #1836.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	May 20, 2026 12:47pm

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit bf4d0d5. Configure here.}