Remove leave-aware dispatcher continuation

[Th0rgal]

Summary

• Removes LeaveAwareCallDispatcherContinuation from EndToEnd.
• Removes the leave-aware hCont premise from the E2/E4/E6 and F2/F4/F6 success bridge wrappers.
• Reuses the Proofs: model checkpoint-aware native switch-tail semantics #1890 final-matched generated dispatcher endpoint by deriving the raw matched flag from the narrow checkpoint-aware hook.

Stacked on #1906.

Verification

• Tiny Lean probe via lake env lean --stdin passed on the stacked branch.
• lake build Compiler.Proofs.EndToEnd

---

Note

Medium Risk
Touches core end-to-end correctness proofs and changes theorem premises (removing hCont and switching to the final-matched dispatcher endpoint), which may break downstream proof consumers despite being mechanically checked by Lean.

Overview
Simplifies the selector-hit end-to-end proof chain by deleting the bespoke LeaveAwareCallDispatcherContinuation hypothesis and removing the extra hCont premise from the E2/E4/E6 and F2/F4/F6 success-bridge wrappers.

Updates nativeGeneratedSelectorHit_success_of_user_body_exec_bridge_atFuel_revivedLeaveAware_and_continuation to consume the generated ..._finalMatched dispatcher endpoint directly by deriving the needed case-body execution and final matched-flag facts from the revived exec bridge, and adjusts the public nativeGeneratedCallDispatcherMatchesIR_of_compile_ok_supported / core preservation theorem to take the unified NativeGeneratedSelectedUserBodyResultBridgeAtFuel instead of the older halt-only bridge.

^{Reviewed by Cursor Bugbot for commit ec68085. 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 5:12am

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