perf: write the constructor header with a single store

[Kha]

This PR lets lean_alloc_ctor write all four header fields at once, replacing the two partial stores a constructor allocation needed before.

lean_alloc_small_object_core initializes m_cs_sz itself, so a caller that goes on to set the remaining header fields cannot merge its stores with that one. A second entry point lean_alloc_small_object_raw leaves the header entirely to the caller, and lean_alloc_ctor then writes m_rc, m_cs_sz, m_other and m_tag with adjacent stores, which fold into one for the constant arguments of compiled code. Allocating a List.cons:

 mov    edi, 0x18
-call   lean_alloc_small_object_core   ; stores m_cs_sz itself
-mov    DWORD PTR [rax], 0x1           ; m_rc
-mov    WORD PTR [rax+0x6], 0x102      ; m_other, m_tag; cannot merge across m_cs_sz
+call   lean_alloc_small_object_raw    ; leaves the header alone
+movabs rcx, 0x102001800000001         ; m_rc | m_cs_sz | m_other | m_tag
+mov    QWORD PTR [rax], rcx           ; one store
 mov    QWORD PTR [rax+0x8], r14
 mov    QWORD PTR [rax+0x10], rbx

What this removes is stores rather than instructions. The new entry point is the same length as lean_alloc_small_object_core, the register freed by dropping the m_cs_sz store being spent elsewhere, and the call site needs two instructions either way; what changes is that the three header stores a constructor allocation performed become one.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 55ee200 against 137a88d are in. There are significant results. @Kha

• ✅ build//instructions: -1.1G (-0.01%)

Large changes (3✅)

• ✅ compiled/hashmap//instructions: -54.3M (-1.68%)
• ✅ compiled/rbmap_fbip//instructions: -118.1M (-1.67%)
• ✅ compiled/sigmaIterator//instructions: -30.0M (-1.13%)

Medium changes (5✅, 3🟥)

• 🟥 compiled/deriv//instructions: +22.5M (+0.35%)
• ✅ compiled/io_compute//instructions: -19.6M (-0.18%)
• ✅ compiled/phashmap//instructions: -20.4M (-0.23%)
• ✅ compiled/rbmap_checkpoint2//instructions: -5.8M (-0.07%)
• ✅ compiled/rbmap_library//instructions: -10.3M (-0.12%)
• 🟥 compiled/treemap//task-clock: +78ms (+7.59%)
• 🟥 compiled/treemap//wall-clock: +78ms (+7.61%)
• ✅ compiled/unionfind//instructions: -10.8M (-0.05%)

Small changes (3✅, 4🟥)

• 🟥 compiled/ilean_roundtrip//instructions: +7.4M (+0.03%)
• 🟥 compiled/nat_repr//task-clock: +95ms (+7.82%)
• 🟥 compiled/nat_repr//wall-clock: +95ms (+7.83%)
• 🟥 compiled/parser//instructions: +53.5M (+0.15%)
• ✅ compiled/rbmap//instructions: -6.4M (-0.08%)
• ✅ compiled/treemap//instructions: -8.7M (-0.05%)
• ✅ size/compile/.out//bytes: -8MiB (-0.30%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137a88d9d363d6f0c60de75d4cef02a26f38962e --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-03 16:59:00)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 137a88d9d363d6f0c60de75d4cef02a26f38962e --onto 19c79593c47bb8dd3371327c08fc80775d8488af. You can force reference manual CI using the force-manual-ci label. (2026-09-03 16:59:01)