Kernel, runtime, and safety hardening
Stronger kernel checks and soundness fixes — Lean tightened several kernel invariants: unknown package names are rejected by lake update, malformed propositions and non-uniform inductives are checked more strictly, generated recursors are kernel-verified, is_def_eq caching is made order-independent, and Nat numerals now have a configurable size cap. Runtime safety also improved with refcount overflow freezing, a lean_apply_m crash fix, a String.extract UAF fix, and a hardened paranoid checker target.
VCGen and intrinsic verification become a first-class workflow
Loop contracts, frames, and specs got much richer — The month’s biggest language-facing work was on vcgen/Std.WP: loop invariants and termination measures were added to do/while/for/repeat, cond now splits into per-branch VCs, requires/ensures gained better binders plus given and match-style clauses, and frames/exception postconditions were reworked for a cleaner protocol. vcgen itself was renamed, documented, moved into a public namespace, and made more explicit about experimental status, while the old mvcgen path was deprecated.
Verification infrastructure was refactored underneath — The weakest-precondition and order/frame-closure machinery was split out of Std.Internal.Do, PredTrans moved into its own namespace, and vcgen gained better goal naming, faster simplification, registered WP instance support, and more robust candidate selection/backtracking.
Tactics and automation got faster and broader
grind and bv_decide saw major upgrades — bv_decide picked up a faster SymM pipeline, explicit type filters, incremental push caching, better SAT/CNF lowering, more symbolic Nat shift reasoning, and min/max support for bitvector families. grind gained loop-measure reasoning, homomorphism-based simplification, better case-splitting performance, more literal canonicalization, lift_lets, improved sym handling, and new diagnostics for e-matching blowups. Sym.simp also became more robust around metavariables, metadata, and definitional unfolding.
Elaboration and simplification were polished — rwa now targets the right goal predictably, constructor warns on ambiguity, casesOn/recOn and simp/dsimp were fixed for several edge cases, and Decidable was redefined to be Bool-backed for stronger definitional equalities.
Lake/build tooling became more reliable
Cache, clone, lint, and build flows were hardened — Lake gained fail-fast builds, partial-clone dependency fetching, package-aware cache commands, safer cache transfers, better JSON/code-quality lint output, and CI-safe cache tests. It also fixed library-root reporting, import all/meta import interaction, static linking for Lake consumers, and several release/tooling rough edges.
Other misc changes
- New
recall/recall?commands for checked restatements. ST.Refwas tightened to a true take/put protocol.Vectorrepr now prints as#v[...]; recursor printing is richer.- Several small theorem/lemma fixes and cleanup in
Init, iterators, lists, strings, bitvectors, and deprecations.