Clarify native EVMYulLean boundary wording

[Th0rgal]

Summary

• rename the EVMYulLean coverage artifact/generator from adapter report to native lowering report
• remove the stale removed-retarget compatibility payload from the report schema
• tighten docs/comments so the public proof boundary is described as native EVMYulLean only, without custom-interpreter/reference-oracle wording
• keep the native report focused on native lowering, builtin routing, bridge lemmas, and native harness markers

Validation

• lake env lean Compiler/Proofs/YulGeneration/IRFuel.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/EvmYulLeanBodyClosure.lean
• lake env lean Compiler/Proofs/EndToEnd.lean
• python3 scripts/generate_evmyullean_native_lowering_report.py --check
• python3 -m unittest scripts/test_generate_evmyullean_native_lowering_report.py scripts/test_evmyullean_fork_conformance_workflow.py scripts/test_check_builtin_bridge_matrix_sync.py scripts/test_check_verify_sync.py -v
• python3 scripts/check_proof_length.py && python3 scripts/check_verify_sync.py && python3 scripts/check_builtin_bridge_matrix_sync.py
• make check

Boundary Notes

• EvmYulLeanAdapter.lean and the backend abstraction are already gone on main via Finalize native EVMYulLean proof boundary cleanup #1924.
• selfBalance now reports as partially modeled runtime introspection and fails under --deny-runtime-introspection via Finalize native EVMYulLean proof boundary cleanup #1924.
• This follow-up removes the last native-report/tooling names that implied an adapter or removed transition payload still existed.

[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 2:03pm