Upgrade Lean toolchain to 4.24

[Th0rgal]

Summary

• upgrade Verity and all split package toolchains from Lean 4.22.0 to 4.24.0
• pin the Lean 4.24-compatible EVMYul migration and refresh every Lake manifest
• adapt Mathlib, String, monadic reduction, and EVMYul proof scripts to the 4.24 API
• refresh the verification status, fork-audit, and generated axiom-audit artifacts
• add regression coverage for the Lean 4.24 trusted native string-reduction boundary

Dependency

This PR is stacked on and must land after:

• Upgrade Lean toolchain to 4.24 EVMYulLean#2
• which itself is stacked on Expose checkpoint state projections EVMYulLean#1

The exact EVMYul commit pinned here is 38d53df8b4488d5322894619ea8385fcbb2e6f5d.

Lean 4.24 trust delta

Lean 4.24 makes the recursive worker used by String.startsWith private and exposes no public substrEq/startsWith correctness theorem. Two closed identifier facts therefore use native_decide, isolated in Compiler/CompilationModel/ReservedScratchNames.lean:

• Compiler.CompilationModel.compatScratch_startsWith_reserved
• Compiler.CompilationModel.compatScratch_not_internalImmutable

The generated #print axioms terms record Lean.ofReduceBool; native reduction also implicitly trusts Lean native code generation (Lean.trustCompiler), although that name is not present in the current printed proof terms. AXIOMS.md and TRUST_ASSUMPTIONS.md document this distinction. CI pins exactly two native facts in that named module, rejects relocation/duplication, and keeps native_decide out of non-test Compiler/Proofs.

This adds no project axiom, sorry, theorem weakening, or global heartbeat increase. The boundary is marked for removal once Lean or Batteries publishes the missing correctness lemmas.

Validation

• lake build — 2124 jobs
• lake build PrintAxioms — 2421 jobs
• actual generated axiom report — PASS, 3937 public theorems checked; 273 axiom-free; 3664 Lean-builtin-only; 0 documented project axioms
• make check — all checks; 612 Python tests, 1 expected skip; 0 sorry; 0 native_decide in non-test proofs
• make test-evmyullean-fork — full fork conformance probe passed
• python3 scripts/check_split_package_builds.py — all 3 split packages
• targeted axiom/trust registry tests — 16 passed
• git diff --check

This remains a draft until the EVMYul dependency lands and downstream benchmark/lean-lsp-mcp smoke validation is complete.

---

Note

Medium Risk
A full-toolchain bump plus a new documented native_decide trust boundary touches the entire proof build, though semantics and project axiom count are unchanged and CI gates the string facts.

Overview
Upgrades Verity and split packages from Lean 4.22 to 4.24, pins Mathlib and EVMYulLean at 38d53df8…, and refreshes verification status, fork-audit, and generated PrintAxioms artifacts.

Lean 4.24 string API gap: two compat scratch-name facts move from a large structural proof in Storage.lean into Compiler/CompilationModel/ReservedScratchNames.lean as isolated native_decide lemmas, with AXIOMS.md / TRUST_ASSUMPTIONS.md and CI (check_trust_surface_registry.py, check_axioms.py treating Lean.trustCompiler) documenting and pinning that boundary—still zero project axioms.

Proof maintenance for 4.24: per-op lookupRuntimePrimOp_* rfl lemmas replace heavy simp on the full matcher (heartbeat); widespread proof call sites switch to those lemmas; Yul lowering proofs gain smaller helper lemmas; IR return-path proofs factor execIRStmts_mstore_zero_return_32; Mathlib import/API fixes (abs_add_le, etc.).

Misc: internalFunctionYulName head-character lemmas consolidate builtin-name disequality proofs; minor string/simp cleanups in end-to-end and intrinsic error-message proofs.

^{Reviewed by Cursor Bugbot for commit e271e12. 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	Jul 13, 2026 9:50am

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_18f13345-858f-40f6-afdd-44fc20b58505)

[github-actions]

OpenCodeReview first-pass review

Status: no-supported · Mode: no-supported · 0 finding(s) · 0 files · 0 tokens · 0 tool calls

No changed files matched OCR include rules.

OCR pilot metrics

• Routing: no-supported (router-v8)
• Changed files: 0 supported / 0 total; Lean 0, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 0 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status no-supported; comments 0; files 0; tokens 0; tool calls 0; warnings 0; duration 0s

Pilot mode: advisory only. Codex Review remains the merge gate.