[JasonGross]

This PR fixes a quadratic slowdown in the kernel when a term contains many Nat literals that are equal modulo 2^64, such as the powers 65536 ^ i.

The Expr hash of a Nat literal used hash n, which is n % 2^64. Thus all multiples of 2^64 had the same hash. For the 4,000 literals 65536 ^ i in #15686, there were only 5 different hashes. Each lookup in the kernel caches then compared these literals one by one.

This PR adds Literal.natHash. For n < 2^64, it returns n, so the hash of these literals does not change. For larger n, it combines all 64-bit words of n with mixHash. The result does not depend on the GMP limb size. Hashable Nat does not change.

Kernel time (type checking in the profiler) for powers% 65536 n from #15686:

n	Before	After
1,000	18.6 ms	1.1 ms
2,000	69.5 ms	2.7 ms
4,000	269 ms	3.9 ms
8,000	1.18 s	5.9 ms

The code generator also uses these hashes. For the full example in #15686, the total time goes from 3.0 s to 1.9 s.

The change alters the hashes stored in .olean files, so this PR checks the box in stage0/src/stdlib_flags.h, as in #16107.

Closes #15686

🤖 Generated with Claude Code

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 29ccdbe against b21ac79 are in. There are significant results. @nomeata

• 🟥 build//instructions: +2.3G (+0.02%)

Large changes (7🟥)

• 🟥 elab/bitvec_zero_counts//instructions: +1.8G (+9.82%)
• 🟥 elab/bitvec_zero_counts//task-clock: +159ms (+13.07%)
• 🟥 elab/bitvec_zero_counts//wall-clock: +158ms (+12.75%)
• 🟥 elab/grind_ring_5//instructions: +11.7M (+0.88%)
• 🟥 elab/trailingZeros//instructions: +5.1G (+25.17%)
• 🟥 elab/trailingZeros//task-clock: +453ms (+28.91%)
• 🟥 elab/trailingZeros//wall-clock: +451ms (+28.34%)

Medium changes (1✅)

• ✅ elab/cbv_aes//instructions: -640.2M (-3.62%)

Small changes (4✅, 4🟥)

• 🟥 compiled/async/http_server//wall-clock: +9s (+66.53%)
• ✅ elab/big_omega//instructions: -41.2M (-0.33%)
• ✅ elab/big_omega_MT//instructions: -52.7M (-0.42%)
• 🟥 elab/cbv_decide//instructions: +539.9M (+1.86%)
• 🟥 lake/inundation/precompileLibrary/clean//instructions: +410.8M (+0.13%)
• 🟥 lake/inundation/precompileModules/clean//instructions: +351.0M (+0.10%)
• and 2 hidden

[nomeata]

nice, it even shows up in our test suite:

elab/cbv_aes//instructions: -640.2M (-3.62%)

[nomeata]

@JasonGross is this intentionally a draft?

[JasonGross]

The agents were following the policy of nonmaintainers opening PRs as draft when the issue being fixed hasn't had attention from maintainers, or something like that. Otherwise I believe this is ready.

[nomeata]

The “Large changes“ regressions are tests with large literals, so it's just the feature working as expected. I don’t see much to improve here (and Claude agrees).