Aver 0.31.0 "Kernel"

Aver checks its own proofs: a kernel written in Aver judges every proof step, and Lean checks the same steps again.

Highlights

• A proof kernel written in Aver. aver proof closes laws with its own proof steps (induction, case splits, arithmetic), and a small kernel written in Aver checks every step, with types. Lean checks the same steps again. aver proof --backend aver runs the kernel alone in seconds on a whole project.
• Steps close many more laws, and when one stays open aver proof says which using, induction or lemma would close it. Projects can write their own proof plans in Aver (by Plans.X); the kernel checks what a plan returns.
• Refined types. An opaque record with a validating constructor (Natural with n >= 0) is a refined type in laws and proofs.
• aver proof is about twice as fast and needs half the memory. Lean 4.35.0, and --paranoid checks with every kernel Lean ships.
• Much faster compiled Rust. Far fewer copies of maps, lists, records and strings, smaller values, shared parts of trees and terms, faster Int, and aver.toml options for mimalloc and panic = "abort".
• Much faster wasm-gc. Int on machine words, fewer allocations, faster strings and maps, tail calls as loops.
• Language: lazy f(x) for deferred calls, exposes for module-level bindings, Bits.popCount, fn main() -> Int sets the exit status.
• Many fixes across the VM, Rust and wasm-gc: no more exponential == on shared values, linear string walks, NaN that behaves the same everywhere, deep recursion that no longer overflows.

Migration

Before	Now
a law over given a: Int with Natural(value = a) in it, proved for a >= 0 only	given a: Natural; a law over Int is about every Int
a validating constructor on a record not listed in exposes opaque made a refined type	add exposes opaque [T]
Natural.fromInt(5) unwrapped with match, ? or Result.Ok(...)	drop the unwrapping
aver proof exporting law samples	only with --examples; bounded_laws is gone from --check-json
a verify case with sides of different types, failing in aver verify	a type error in aver check
Shape.Rect(_) for a two-field variant, Option.Some()	list every field, or write the bare Shape.Rect
fn main() -> Int returning a value outside 0..255	exit status 1 with a message
Args.get() with no --	only the arguments after --, on every runner
a module-level binding that reads itself or a later one	refused by aver check
certifying a plain wasm-gc or wasip2 build	build with --certify and ship that build
hand-written Rust matching a generated recursive sum as an enum	match on value.view()

A 0.30 --gate baseline with bounded laws has to be recorded again.