Revive EndToEnd dispatcher cleanup

[Th0rgal]

Links #1884. Stacked after merged #1906 / #1890 foundation.

This PR closes the EndToEnd-side dispatcher revival by proving the generated runtime path with the real init-prefixed shape:

• lowers and peels [initFreeMemoryPointer, buildSwitch ...], not the old bare [buildSwitch ...] witness;
• bridges the initial mstore(0x40, 128) through the native dispatcher state before applying the switch/selector endpoint;
• keeps the bridge narrow to the generated init-prefix dispatcher path, with no broad arbitrary-tail no-op lemma;
• removes the leave-aware continuation target surface from EndToEnd.

Cleanup completed:

• no LeaveAwareCallDispatcherContinuation references remain in Compiler/Proofs/EndToEnd.lean;
• removed hCont, hExecBridge, and hUserBodyHalt hypothesis sites;
• E2/E4/E6/E7/F2/F4/F6/F7 NativeGeneratedSelectorHitSuccessBridge.of_* constructors are unconditional and compose through the final matched dispatcher endpoint;
• raw state semantics and the revived/raw lookup model are unchanged. The EVMYulLean fork-audit/package-manifest edits only synchronize checked metadata to the already-pinned dependency commit.

Proof/trust evidence:

• rg 'LeaveAwareCallDispatcherContinuation|hExecBridge|hUserBodyHalt|\(hCont\s*:|hCont :' Compiler/Proofs/EndToEnd.lean returns no matches.
• scripts/check_lean_hygiene.py reports 0 sorry, 0 native_decide in proofs.
• PrintAxioms.lean is up to date and reports Total: 5343 theorems/lemmas (3634 public, 1709 private, 0 sorry'd).
• scripts/check_axioms.py reports 0 source axioms and a synchronized registry.

Local validation:

• lake env lean Compiler/Proofs/EndToEnd.lean passed with warnings only.
• lake clean && lake build passed.
• make check passed, including Lean hygiene, fork-audit sync, PrintAxioms sync, proof-length allowlist, and 595 Python tests.

Worker/model notes from the #1890/#1884 investigation:

• Grok was best for semantic validity probing and found the revived/raw checkpoint mismatch.
• Codex was best for structured Lean scaffolding and the final focused theorem integration.
• Claude was useful for mechanical prefix edits and review, but did not solve the lowering-witness mismatch.

---

Note

Medium Risk
Touches the end-to-end correctness proof spine for the native dispatcher by changing the lowering witness/bridge structure and fuel bounds; while proof-only, regressions could break key compiler correctness guarantees or CI builds.

Overview
Revives and tightens the EndToEnd native dispatcher proof path to match the actual generated runtime shape, explicitly accounting for the initFreeMemoryPointer prefix (mstore(0x40, 128)) before the selector switch.

Removes the leave-aware continuation surface from Compiler/Proofs/EndToEnd.lean and simplifies the selector-hit success bridging so the NativeGeneratedSelectorHitSuccessBridge.of_* constructors become unconditional and compose directly through the final matched dispatcher endpoint, without a broad arbitrary-tail no-op lemma.

Includes small supporting adjustments to runtime-size/fuel bound lemmas (now witnessing [initFreeMemoryPointer, buildSwitch ...]) and syncs pinned dependency/manifest metadata for the EVMYulLean fork.

^{Reviewed by Cursor Bugbot for commit f35594f. 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 20, 2026 12:44am

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