[nomeata]

This PR adds InLean, a Lean port of the con-leche kernel checker, to the stdlib without using it. It is an experiment: the companion PR #16353 replaces the C++ kernel by InLean, and its benchmark results mix two costs, compiling InLean's code and switching the kernel. This PR only adds the code, so that its compile cost can be measured on its own; #16353 is based on it, and its diff is the switch. The C++ kernel stays active here.

It contains:

• a cherry-pick of perf: hash all bits of large Nat literals in Expr #16146 (by Jason Gross), which hashes all bits of large Nat literals in Expr (Literal.natHash), with its stage0 checkbox commit; feat: replace the C++ kernel with InLean, a verified Lean port (experiment) #16353 carries it, so this PR does too, and the two benchmark against each other on the same footing;
• Lean bodies for Expr.mkData, Expr.mkAppData and Level.mkData that state what their C implementations compute, so that the cached expression and level fields can be reasoned about. They keep their @[extern] attributes, so the compiled code still runs C. tests/elab/expr_mkData_bodies.lean compares the C-backed calls with a transcription of the C on sample and boundary inputs, and proves the fields of an application's data from the bodies;
• InLean itself, in src/Lean/Kernel/InLean/, generated from con-leche's InLean/ by con-leche's scripts/inlean-sync.py (it only adds the copyright header and prelude, renames the namespace and drops InLean's copy of Init.Util's withIsExclusive), with the Nat-operation pins under pins/. Lean imports its top module Lean.Kernel.InLean.AddDecl, so the stdlib build compiles it. The module that exports the kernel entry points (Lean.Kernel.InLean.Core) is not part of this PR;
• tests/elab/csimpCore.lean lists InLean's @[csimp] lemmas.

All tests pass locally (stage1) except elab/async_systems_info, which fails in our sandbox on an unmodified build too.

🤖 Generated with Claude Code

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 1c92992 against da4295a are in. There are significant results. @nomeata

• 🟥 build//instructions: +705.9G (+7.44%)

Large changes (52🟥)

• 🟥 build//task-clock: +1m 41s (+5.84%)
• 🟥 build/lakeprof/longest rebuild path//instructions: +349.7G (+67.15%)
• 🟥 build/lakeprof/longest rebuild path//wall-clock: +25s (+36.57%)
• 🟥 build/profile/process pre-definitions//wall-clock: +6s (+17.93%)
• 🟥 build/profile/simp//wall-clock: +23s (+20.09%)
• 🟥 build/profile/type checking//wall-clock: +19s (+21.10%)
• 🟥 build/stat/imported bytes//bytes: +2GiB (+1.59%)
• 🟥 build/stat/imported consts//amount: +1.6M (+1.72%)
• 🟥 build/stat/imported modules//amount: +32.5k (+1.80%)
• 🟥 compiled/ilean_roundtrip//instructions: +1.4M (+0.01%)
• 🟥 compiled/incr_header_load//instructions: +3.1M (+0.86%)
• 🟥 compiled/incr_header_save//maxrss: +40MiB (+2.16%)
• 🟥 compiled/liasolver//instructions: +1.4M (+0.04%)
• 🟥 compiled/phashmap//instructions: +1.4M (+0.02%)
• 🟥 compiled/rbmap_library//instructions: +1.4M (+0.02%)
• 🟥 compiled/watchdogRss//instructions: +305.8M (+1.53%)
• 🟥 compiled/workspaceSymbolsNewRanges//instructions: +1.4M (+0.22%)
• 🟥 elab/big_beq//maxrss: +33MiB (+1.91%)
• 🟥 elab/big_beq_rec//maxrss: +31MiB (+1.80%)
• 🟥 elab/big_deceq//maxrss: +33MiB (+1.91%)
• and 31 more
• and 1 hidden

Medium changes (1✅, 20🟥)

• 🟥 build/profile/.olean serialization//wall-clock: +6s (+8.60%)
• 🟥 compiled/parser//instructions: +1.5M (+0.00%)
• 🟥 elab/big_match_partial//maxrss: +34MiB (+1.91%)
• 🟥 elab/bv_normalize_cast//instructions: +1.4M (+0.19%)
• ✅ elab/cbv_aes//instructions: -639.4M (-3.62%)
• 🟥 elab/delayed_assign//maxrss: +52MiB (+3.06%)
• 🟥 elab/lift_lets_binders//maxrss: +50MiB (+2.90%)
• 🟥 elab/matcherInferTypeCache//maxrss: +20MiB (+2.12%)
• 🟥 elab/mut_rec_wf//maxrss: +54MiB (+3.07%)
• 🟥 elab/partial_fixpoint_mutual_eqns//maxrss: +54MiB (+3.00%)
• 🟥 elab/string_simp_ne//maxrss: +50MiB (+2.86%)
• 🟥 elab/sym_lift_lets_parallel//maxrss: +47MiB (+2.59%)
• 🟥 elab/sym_lift_lets_spine//maxrss: +47MiB (+2.58%)
• 🟥 lake/inundation/build/clean//instructions: +574.4M (+0.27%)
• 🟥 misc/import Lean cold//instructions: +10.9M (+1.21%)
• 🟥 misc/import Lean//instructions: +10.9M (+1.20%)
• 🟥 size/all/.c//lines: +353.4k (+2.74%)
• 🟥 size/all/.ir//bytes: +11MiB (+2.58%)
• 🟥 size/all/.olean.private//bytes: +38MiB (+2.73%)
• 🟥 size/install//bytes: +88MiB (+2.59%)
• and 1 more

Small changes (3✅, 874🟥)

• 🟥 build/profile/blocked (unaccounted)//wall-clock: +6s (+6.99%)
• 🟥 build/profile/compilation (IR)//wall-clock: +285ms (+4.88%)
• 🟥 build/profile/compilation (LCNF base)//wall-clock: +6s (+4.10%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+4.46%)
• 🟥 build/profile/compilation (LCNF mono)//wall-clock: +2s (+5.40%)
• 🟥 build/profile/import//wall-clock: +5s (+5.26%)
• 🟥 build/profile/interpretation//wall-clock: +3s (+3.66%)
• 🟥 build/profile/parsing//wall-clock: +996ms (+3.88%)
• 🟥 build/profile/tactic execution//wall-clock: +5s (+4.24%)
• 🟥 build/profile/typeclass inference//wall-clock: +4s (+4.79%)
• 🟥 compiled/server_startup//instructions: +2.6M (+0.73%)
• 🟥 elab/big_deceq//instructions: +15.3M (+0.53%)
• 🟥 elab/big_deceq_rec//instructions: +14.9M (+0.39%)
• 🟥 elab/big_match//instructions: +15.7M (+0.20%)
• 🟥 elab/big_match_nat//instructions: +14.5M (+0.43%)
• ✅ elab/big_omega//instructions: -49.7M (-0.40%)
• ✅ elab/big_omega_MT//instructions: -55.3M (-0.44%)
• 🟥 elab/bitvec_zero_counts//maxrss: +16MiB (+1.81%)
• 🟥 elab/bv_decide_incremental//maxrss: +32MiB (+1.62%)
• 🟥 elab/cbv_decide//maxrss: +51MiB (+2.85%)
• and 37 more
• and 820 hidden