[jasisz]

Both entries move from Pestka e1b1d11 to f09ce29, and the pinned Aver release from 0.31.0 to 0.32.0 (still installed from crates.io; the build commands are unchanged). pestka-wasm now also passes --low-memory.

In the checker:

• variables and sorts carry their hash-and-metadata word, as every other node already did, instead of computing it on each read;
• each per-declaration cache gets its own limit, chosen from measured reuse distances;
• universe levels of constants are built as plain list cells;
• a closed value is substituted under binders without being lifted, and full whnf_core results are remembered within a declaration, as the reference kernel does;
• a new --low-memory flag keeps the caches bounded to about what reading the file needs.

In Aver 0.32: fields laid out by how the program reads them, scalar fields compared without branches, lent cursors over lists, a node's memory reused at a match's last use, and values built by a call and taken apart at once never built.

Measured locally (PGO on Init, one worker), mathlib on pestka takes about 14% fewer instructions than at e1b1d11 (1.89 T → 1.63 T) and about 13% less wall time; peak memory goes from 6.5 to 7.4 GB.

pestka-wasm runs with --low-memory because under V8's collector the larger default caches cost more in collection than they save; on Init and etale the flag is free in instructions and cuts peak memory by 10–17%. Locally, mathlib on the wasm entry takes 7.97 T instructions with it (573 s, peak 11.9 GB); the current entry takes 10.34 T on the Arena, which is not the same machine, so the gain there will differ somewhat.

Every verdict is unchanged: the small tests give 179 of 179 natively and under wasm-gc (Node 26).