Upgrade Verity and EVMYulLean to Lean 4.30 after the current roadmap drain

[Th0rgal]

Goal

Upgrade the Verity toolchain and its EVMYulLean dependency from Lean 4.24.0 to Lean 4.30.0, while preserving kernel/trust guarantees and using the upgrade to improve maintainability, proof automation, dependency hygiene, and executable performance.

Priority: deliberately last in the current roadmap. Do not start this while the authorized existing Verity PR drain or roadmap lanes A–H are blocked by unfinished integration work.

Current baseline

• Verity pins leanprover/lean4:v4.24.0, Mathlib v4.24.0, Batteries v4.24.0, and lfglabs-dev/EVMYulLean at 38d53df8b4488d5322894619ea8385fcbb2e6f5d.
• Static inventory on current main: 386 Lean files / about 279k lines. The largest proof files are about 33k, 30k, 11k, and 8k lines, so migration failures may have wide compile fan-out.
• NethermindEth/EVMYulLean main still pins Lean/Mathlib 4.22.0. The LFG fork is already on 4.24.0 and contains downstream verification hooks; its current main is two commits ahead of Verity's pin.
• EVMYulLean is comparatively small: 66 Lean files / about 11.4k lines.

Relevant Lean 4.25–4.30 changes

Primary release notes:

• https://lean-lang.org/doc/reference/latest/releases/v4.25.0/
• https://lean-lang.org/doc/reference/latest/releases/v4.26.0/
• https://lean-lang.org/doc/reference/latest/releases/v4.27.0/
• https://lean-lang.org/doc/reference/latest/releases/v4.28.0/
• https://lean-lang.org/doc/reference/latest/releases/v4.29.0/
• https://lean-lang.org/doc/reference/latest/releases/v4.30.0/

Migration-sensitive changes

1. Lean 4.29 transparency / instance behavior

   • isDefEq no longer raises transparency while comparing implicit arguments.
   • simp/dsimp no longer simplify typeclass instances by default.
   • @[implicit_reducible] and the improved inferInstanceAs are the intended fixes for legitimate alias transport; the project-wide backward.isDefEq.respectTransparency=false option should only be a temporary diagnostic, never the final migration state.
   • Audit semireducible type aliases and hand-written transported instances.

2. inferInstanceAs behavior

   • EVMYulLean has 10 uses across EvmYul/Wheels.lean, EvmYul/UInt256.lean, EvmYul/Data/Stack.lean, and EvmYul/Yul/Ast.lean.
   • Decide explicitly whether Identifier, Blob, Stack, and similar wrappers are representational aliases (abbrev) or abstraction boundaries (real wrapper structures). Avoid relying on accidental definitional unfolding.

3. Stricter noncomputable semantics and universe inference

   • Lean 4.29 may require additional noncomputable annotations.
   • Recursive predicates and universe levels that appeared only in constructor fields may need explicit annotations.

4. Native computation trust reporting changed

   • From Lean 4.29, native_decide/bv_decide produce one generated axiom per computation instead of reporting the single Lean.trustCompiler axiom.
   • Verity has hundreds of textual native_decide occurrences in tests/witnesses and a fixed builtin allowlist in scripts/check_axioms.py that currently names Lean.trustCompiler.
   • Update the axiom parser/classifier, trust reports, tests, AXIOMS.md, AUDIT.md, and TRUST_ASSUMPTIONS.md together. Fail closed: recognize generated native-computation axioms structurally and report their exact users; do not add an unrestricted wildcard allowlist.

5. Metaprogramming/module changes

   • Lean 4.30 makes theorems opaque in essentially all contexts and re-enables axiom dependency data under the module system.
   • Verity's generated PrintAxioms.lean contains a custom recursive environment walker over env.checked.get.find?. Revalidate it against 4.30 and prefer a small wrapper around supported Lean axiom APIs if possible.
   • No direct uses of the renamed isStructureLike/compileDecl APIs were found in the initial static scan, but custom command elaborators still need compilation testing.

6. Lake and FFI changes

   • EVMYulLean has custom Lake targets for C FFI libraries and four @[extern] ByteArray functions. Rebuild and execute those paths; compilation success alone is not enough to establish ABI/runtime correctness.
   • Lean 4.30's Lake cache overhaul changes artifact materialization/download behavior and adds staged transfers, fixedToolchain, parallel transfers, and on-demand restoration.

Opportunities after the minimal port

These should be follow-up PRs, not mixed into the version-bump PR.

Verity

• Trust audit cleanup: replace brittle custom axiom traversal where supported 4.30 APIs suffice; add leanchecker as an independent CI validation layer.
• Import/API boundaries: both repositories currently use only plain imports (initial scan: ~1,262 in Verity and ~364 in the LFG EVMYulLean fork), with no real module-system visibility boundaries. Introduce module, public/private/meta imports, public section, assert_not_imported, and assert_not_exists incrementally around stable leaf APIs.
• Dependency minimization: run lake shake module-by-module, starting with proof API leaves and generated audit modules. Do not perform a whole-tree import rewrite in one PR.
• Proof automation: pilot user-defined grind attributes, [grind norm], [grind unfold], +locals, higher-order Miller-pattern matching, and sym => on one repetitive semantics family. Verity currently has about 10k textual simp and 1k omega occurrences, but broad replacement without benchmarks would be risky.
• Symbolic simulation: evaluate Lean 4.28's symbolic simulation framework as a reusable VC/symbolic-execution layer for the IR/Yul semantics. Start with one isolated straight-line fragment and compare proof term size, elaboration time, and maintainability against the current bespoke bridge lemmas.
• Concrete evaluation: pilot the expanded kernel-oriented cbv tactic for concrete compiler/interpreter smoke goals where it can replace fragile unfolding scripts or trusted native computation.
• File decomposition: split the 30k+ line proof modules along stable semantic interfaces only after the port is green. Use module visibility and dependency assertions to prevent the split from creating a larger accidental public API.
• Executable performance: benchmark the completed LCNF backend and user borrow annotations on the compiler/CLI and metaprogramming paths. ReaderT already benefits globally; add explicit @& only after profiling shows reference-count pressure. These changes may improve executable runtime/binary size, not necessarily proof elaboration.
• Build performance: adopt the 4.30 cache features in the dedicated Verity workspace, with exact-toolchain isolation and before/after clean/incremental build measurements.

EVMYulLean

• Port the maintained LFG fork first, then decide whether to upstream the clean 4.30 port to NethermindEth/EVMYulLean (which currently jumps from 4.22 rather than 4.24).
• Resolve the 10 transported-instance sites explicitly instead of using the global backward-compatibility option.
• Keep the existing borrowed @& ByteArray FFI arguments and benchmark the 4.30 backend; verify SHA-256, Keccak, Blake2, and zero-byte-array runtime behavior against known vectors.
• Add import visibility and lake shake incrementally; the small codebase is a good pilot before attempting the same discipline in Verity.
• Consider grind/cbv only where they remove repetitive proofs in UInt256, stack, and Yul size lemmas; do not add automation merely because it is new.

Proposed implementation sequence

1. Capture reproducible 4.24 baselines for both repos: clean build, tests, axiom report, build time, peak RSS, artifact/binary size.
2. Upgrade lfglabs-dev/EVMYulLean to Lean/Mathlib 4.30.0 in a dedicated branch.
3. Inventory compile failures. A localized backward transparency option may be used temporarily to classify failures, but the final diff must remove it.
4. Fix Lake/FFI and instance/alias issues; run lake build, conform/Yul tests, and known-vector FFI tests.
5. Update Verity to Lean/Mathlib/Batteries 4.30.0 and pin the green EVMYulLean commit.
6. Repair source and proofs without semantic refactors. Regenerate and validate PrintAxioms.lean; update all trust-boundary documents in the same PR.
7. Run make check, Python and Foundry tests, full lake build, generated trust reports, and an independent leanchecker pass.
8. Compare 4.24 vs 4.30 clean/incremental build time, peak RSS, audit runtime, CLI runtime, and binary size. Do not claim a performance gain without measurements.
9. Land follow-up refactor PRs separately: trust audit API, imports/modules, one automation pilot, one symbolic-simulation pilot, then large-file decomposition.

Acceptance criteria

• EVMYulLean 4.30 build and runtime/FFI tests are green.
• Verity make check, tests, and full Lean build are green on 4.30.
• No project-wide backward.* compatibility option remains.
• No new sorry, admit, project axiom, or silently widened native-computation allowlist.
• AXIOMS.md, AUDIT.md, and TRUST_ASSUMPTIONS.md match the 4.30 native-computation and checker semantics.
• Verity pins the exact reviewed EVMYulLean 4.30 commit.
• Before/after performance results are attached.
• Follow-up refactors are split into reviewable PRs and preserve theorem/API behavior.

Explicit non-goals for the version-bump PR

• No broad proof rewrite to grind.
• No whole-repository module/import conversion.
• No simultaneous redesign of Verity semantics.
• No upstream publication claim until the fork port, Verity integration, trust audit, and runtime checks are all complete.