Retarget public correctness toward native EVMYulLean

[Th0rgal]

Summary

Retargets Verity's public EVMYulLean correctness surface away from backend-parameterized oracle spellings and toward native EVMYulLean-named entry points, and lands the first wave of leaf ExecOnlyBridgeAtFuelRevived constructors so the Revived family covers every observational-no-op fn.body shape.

Public-surface retarget

• Added interpretYulRuntimeEvmYulLean and interpretYulRuntimeEvmYulLeanFuel wrappers.
• Retargeted the public Layer 3 and SimpleStorage EndToEnd theorem names to EVMYulLean conclusions.
• Kept legacy/reference-oracle paths available under explicit ..._via_reference_oracle names; renamed the lower legacy Layer 3 theorem to yulCodegen_preserves_semantics_via_reference_oracle and guarded against restoring the bare oracle name.
• Renamed native agreement seams from ...Interpreter to ...EvmYulLean.
• Changed defaultBuiltinBackend to .evmYulLean; added legacyBuiltinBackend := .verity, legacyEvalBuiltinCallWithContext, and legacyExecYulFuel so old reference-oracle / bridge-comparison paths opt into legacy semantics explicitly.

Native EndToEnd surface

• nativeResultsMatchOn, sourceResultMatchesNativeOn, source/native composition theorem over the result surface.
• compile_preserves_native_evmYulLean_callDispatcher_of_generated_callDispatcher_match, plus helper-free and mapping-helper lowering wrappers.
• Concrete SimpleStorage native theorem; case freshness dispatcher adapters; mapping switch freshness wrappers.

Leaf Revived constructors (G1 increments S1–S4)

On NativeGeneratedSelectedUserBodyExecOnlyBridgeAtFuelRevived:

• .of_block_empty — fn.body = [.block []]
• .of_block_leave — fn.body = [.block [.leave]]
• .of_singleton_comment — fn.body = [.comment text]

Together with the pre-existing .of_empty_body and .of_leave_body, the Revived family now covers every body of shape [], [.leave], [.block []], [.block [.leave]], [.comment text] — the full observational-no-op family. Concrete contracts whose user body is a label-only stub now have a direct Revived bridge without going through the halt path.

.of_comment_cons is intentionally deferred to the success-bridge wiring layer (per-leaf _with_label_prefix adapters); see docs/NATIVE_EVMYULLEAN_TRANSITION.md for the structural rationale.

Supporting infrastructure

• New harness lemmas: exec_block_block_nil_ok_add_ten, exec_block_block_leave_ok_add_ten, exec_block_noop_block_head_eq, lowerStmtsNativeWithSwitchIds_comment_head_eq.
• Source-side helpers: nativeResultsMatchOn_execIRFunction_block_empty_body_markedPrefix, ..._block_leave_body_markedPrefix, ..._singleton_comment_body_markedPrefix.
• Updated native-transition guards/docs to enforce the new public surface and terminology.

Invariants

• Zero sorry, zero new axioms.
• lake build Compiler.Proofs.EndToEnd green.
• make check validators (axioms, capability boundary, builtin boundary, doc check) pass.

Verification

• lake build Compiler.Proofs.EndToEnd
• lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeTest
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_native_transition_doc.py
• python3 scripts/test_check_native_transition_doc.py
• python3 -m unittest scripts.test_evmyullean_capability
• make check

Deferred to a follow-up PR

The composite body shapes and the final premise drop share heavy proof infrastructure (whole-block per-slot preservation, IR execIRStmts falling-through induction) that does not fit a single landable increment in this branch's budget. See docs/NATIVE_EVMYULLEAN_TRANSITION.md — the "G1 Incremental Plan" section has full constructor signatures, harness-lemma signatures, and proof sketches.

• G1-S5 .of_nativePreservableStraightStmts_leave — bodies <straight-stmts>; leave. Companion lemma: execIRStmts_continue_of_nativePreservableStraightStmts_pre_leave (purely IR-side; recommended starting point for a follow-up worker).
• G1-S6 .of_bridgedStraightStmts_falling_through — bodies <straight-stmts> (no terminator). Deepest case; requires aligning execIRFunction's fall-through extraction with the dispatcher's outer block exit.
• G1-S7 Wire the five shipped leaves plus the two new constructors through NativeGeneratedSelectorHitSuccessBridge adapters, including per-leaf _with_label_prefix variants that strip a leading .comment "label" head via exec_block_noop_block_head_eq. Subsumes the deferred .of_comment_cons shape.
• G1-S8 Drop hUserBodyHalt from compile_preserves_native_evmYulLean_of_compile_ok_supported_generated_callDispatcher once S5–S7 land.

Long-standing items (orthogonal to this PR)

• legacyExecYulFuel remains in ReferenceOracle/Semantics.lean for legacy/reference-oracle comparisons.
• EvmYulLeanRetarget.lean still proves the EVMYulLean retarget by composing through yulCodegen_preserves_semantics_via_reference_oracle and backend comparison machinery.
• The final native execution theorem path still has explicit bridge obligations and is not fully discharged for all compiler-generated contracts — the G1-S5..S8 follow-up is the path to discharging them.

---

Note

Medium Risk
Touches the public proof surface (arithmetic correctness lemmas) and CI caching/install logic; while semantics should be equivalent, regressions could break downstream proofs or CI reliability.

Overview
Retargets the public arithmetic proof surface to state wrapping/bitwise/shift facts directly in terms of the native evalPureBuiltinViaEvmYulLean evaluator, removing reliance on legacy oracle/bridge comparison lemmas while keeping historical theorem names.

Exposes compileMappingSlotRead and compileMappingSlotChain from ExpressionCompile.lean so proof modules can reference the exact lowering shapes, and trims top-level Compiler.lean imports to drop unused proof modules.

CI updates: adds a sticky-disk pruning step for stale Lake packages, increases verify.yml job timeout, and hardens setup-solc by caching per-version in-repo with PATH injection plus install/repair retries and version verification (instead of writing to /usr/local/bin).

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

[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```