Changelog

leanprover/lean4 · · 17 commits

Arithmetic normalizer lands; async bugs fixed

Lean4 adds a reflected polynomial normalizer, fixes async cancellation/races, and tightens float and bitvector semantics.

leodemoura hargoniX TwoFX algebraic-dev Kha Rob23oba thorimur gasparattila Chessing234 kim-em

Polynomial normalization for ring and semiring terms (leodemourabb25f8f)

Lean now has Sym.Arith.normalize?, a reflected normalizer that rewrites CommRing and CommSemiring terms into polynomial normal form and produces a proof by reflection. This is a major new arithmetic foundation for Sym.simp/grind-style automation, with new support code for denotation and safe polynomial handling.

Async cancellation and wakeup handling fixed (algebraic-dev81da73b)

ContextAsync, Notify, Channel, and Broadcast now cancel more reliably and avoid wasting wakeups on stale waiters. The race helpers were also tightened so losing computations are cancelled more aggressively, reducing hangs and leaked background work.

TCP/UDP socket races, leaks, and selector behavior fixed (algebraic-dev8648bf7)

The TCP/UDP stack got a broad correctness pass: accept/wait paths were reworked, cancellation-related leaks and races were fixed, and keep-alive delay handling now validates size limits before passing values down to C. The changes also remove some blocking assumptions and make socket operations safer under concurrent use.

Float min/max now use IEEE-754 minimum/maximum (TwoFX5371d44, TwoFXfbb1eef)

Min Float/Max Float were replaced with explicit IEEE-754 minimum/maximum operations, and Float.minimumNumber/maximumNumber plus the Float32 variants were added. The follow-up commit gives these operations logical models, which matters because they now reduce in the kernel and can be reasoned about in proofs.

Lean exposes more arithmetic and character internals (kim-em362101e, leodemoura095a077, gasparattila0888335, thorimur3def45e)

Char.ordinal/succ?/succMany? were made reducible across module boundaries, inferInstanceAs learned to reuse instances for non-exposed definitions, and Lean.toolchain now uses the release-style v prefix. The semiring polynomial normalizer also fixed its x ^ 0 case to normalize to 1, improving arithmetic simplification fidelity.

LCNF simplification and bv_decide get smarter (hargoniX55c3cb0, hargoniX35e1c9a)

LCNF simplification now uses a faster heuristic for choosing default alternatives, cutting down unnecessary alpha-equivalence checks. bv_decide also gained extra reduction power for matches and projections, fixing regressions around structured terms.

Other misc changes

  • Removed a large amount of unreachable C++ code across src/ (Khaf03441b)
  • Added missing BitVec order instances and updated Grove metadata (TwoFXa14a87f)
  • Fixed cbv on trivial ite/dite conditions (Rob23oba1d056ee)
  • Rejected invalid ← modifiers for simprocs/simp extensions (Chessing2347dee48a)
  • Moved order-instance classification into Sym.Arith for reuse (leodemoura99ef90d)