Model checkpoint-aware native switch tails

[Th0rgal]

Summary

• Pins EVMYulLean to 7785a9bba344db917e42b7f1033ee8346197bb40 from Expose checkpoint state projections EVMYulLean#1.
• Adds nativeSwitchMatchedFlag_of_revived_body_final, a narrow generated-switch proof hook from _revived body preservation plus final.reviveJump = Ok ... to the raw matched flag expected by the generated switch tail.
• Keeps EndToEnd cleanup out of this PR; the removal of the old continuation is stacked separately.

Closes #1890.

Verification

• Tiny Lean probe via lake env lean --stdin proving checkpoint raw lookup agrees with revived lookup after final.reviveJump = Ok ....
• lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness
• lake build Compiler.Proofs.EndToEnd

---

Note

Medium Risk
Moderate risk: introduces a new proof lemma that relies on reviveJump/checkpoint state projections and updates the pinned evmyul dependency, which could affect downstream proof compilation.

Overview
Adds nativeSwitchMatchedFlag_of_revived_body_final, a new proof bridge that converts _revived block preservation (via reviveJump) plus a final.reviveJump = Ok … assumption into the raw final-state lookup needed by generated native switch tails.

Updates the evmyul dependency pin to 7785a9b… and registers the new lemma in PrintAxioms for axiom-audit builds.

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

[vercel]

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

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	May 19, 2026 2:29pm

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