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
Changes the generated deploy and runtime prologue to mstore(0x40, 128), which can affect all contracts that rely on free-memory-based ABI encoding/event emission. Risk is moderate because it alters low-level EVM memory initialization but is localized and conventional.

Overview
Adds an explicit initFreeMemoryPointer Yul statement that sets the Solidity free memory pointer (mstore(0x40, 128)).

Injects this initialization into all generated outputs: before the runtime dispatcher switch, in the emit-options runtime path, and at the start of deploy code (ahead of value guards/mapping helpers/constructor code).

^{Reviewed by Cursor Bugbot for commit 7d47813. 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 1:37pm

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