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.

Key changes:

• 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.
• Updated native-transition guards/docs to enforce the new public surface and terminology.

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

Remaining work

• The historical fuel interpreter still exists in ReferenceOracle/Semantics.lean as legacyExecYulFuel 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.

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