feat: wide fixed-width integer load/store accessors on ByteArray

[kim-em]

This PR adds little- and big-endian UInt16/UInt32/UInt64 load and store accessors to ByteArray, reading or writing a fixed-width integer at a byte offset in a single native load/store rather than through a boxed Array UInt32 (a tagged load plus an unbox) or hand-written byte assembly.

For each width and endianness there are three readers and three writers, mirroring the existing byte accessors get!/get/uget and set!/set/uset:

• getUInt32LE! / setUInt32LE! — Nat offset, no proof. All-or-nothing on bounds: a read whose W/8-byte window does not fit returns 0, and such a write leaves the array unchanged, matching the defaulting behaviour of ByteArray.get!/set!.
• getUInt32LE / setUInt32LE — Nat offset with an in-bounds proof.
• ugetUInt32LE / usetUInt32LE — USize offset with an in-bounds proof (the fast path).

The offset is a byte position, so the same primitive serves both an array-of-UInt32 view (i = 4*k) and the read-a-UInt32-at-an-arbitrary-position case common in codecs. The @[extern] implementations are static inline C in lean.h built from the portable byte-shift idiom, which optimizing compilers typically fold to an efficient (possibly unaligned) load or store; the Lean definitions are the proof-level model and the externs are validated against them by tests.

In a hot loop the USize-indexed ugetUInt* / usetUInt* forms are the ones to reach for: the Nat-indexed variants (including the ! forms) take a boxed Nat, so the loop's index arithmetic runs boxed and measures noticeably slower. The module docstring says so.

Lemmas accompany the API in Init.Data.ByteArray.Lemmas: the proof-carrying variants are definitionally the ! model, writes preserve size, and reads round-trip writes (get* (set* a off v) off = v under bounds), for every width and endianness. The round-trip proofs reduce the read of the freshly-written bytes to a fixed-width bit-recombination identity discharged by getLsbD extensionality (no bv_decide, so everything stays in Init). Disjointness is stated at the byte level — getElem!_setUIntWE!_of_outside says a wide write changes only the bytes in its own window, so a read of any byte (hence any width or endianness) outside that window is unaffected; same-width/endianness _of_disjoint corollaries are provided for convenience. tests/elab/bytearray_pack.lean additionally checks that the @[extern] C implementations match the Lean model on concrete values, endianness, and the all-or-nothing out-of-bounds behaviour.

This is motivated by performance work on pure-Lean codecs (see #14050 "feat: fast fixed-width integer load/store on ByteArray"): a data structure that is conceptually a dense array of fixed-width integers previously had no representation with a single-instruction element load.

ByteSlice forwarding accessors are a natural follow-up left out of this PR.

🤖 Prepared with Claude Code

[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 9f1e8022b71e919870342562a89a6cb71e3e38c7 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-15 09:35:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9f1e8022b71e919870342562a89a6cb71e3e38c7 --onto 4620e4d946957ae7c582764c79eb93cc779f77e2. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-26 04:57:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9c9eb9a3acefaa242c1da2a31e3723e94fde3a5 --onto 4620e4d946957ae7c582764c79eb93cc779f77e2. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-26 06:59:46)

[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 9f1e8022b71e919870342562a89a6cb71e3e38c7 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-15 09:35:26)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9f1e8022b71e919870342562a89a6cb71e3e38c7 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-26 04:57:39)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b9c9eb9a3acefaa242c1da2a31e3723e94fde3a5 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-26 06:59:47)

[Rob23oba]

I actually added these already in #8165; I'll update that to fix the merge conflicts (to be clear, I don't particularly like the approach of making a ton of independent functions, my PR instead adds a general simp normal form of setBitVecLE / setBitVecBE).

[mitschabaude]

@kim-em Landing this would be really valuable, but I think it could be made faster.

I tested these storage externs on a fast implementation of NTT (number theoretic transform), where without them it was impossible to match existing Rust benchmarks. With this PR's C implementation it was still too slow, but slight changes (without affecting the API) made it fast enough, so I want to propose this as a change.

I worked on this with Claude Opus 5.5 and not an expert in the technical details myself so the proposal that follows is written by Claude 🤖

---

1. Load and store with a fixed-size memcpy instead of byte-shift loops.

T r; memcpy(&r, lean_sarray_cptr(a) + i, sizeof r);   /* + byte swap when host order differs */

• The byte-shift form relies on the compiler recognising it as a wide load or store. That works for an isolated access but fails in exactly the code these functions are for: runs of adjacent word accesses in hashing, parsing, codecs, crypto and numeric kernels.
• There, clang's SLP vectorizer turns the byte operations into shuffle and insert sequences before they get combined.
• A fixed-size memcpy is the standard C idiom for unaligned, alias-safe word access. Every compiler lowers it to a single load or store at any optimisation level, with no idiom recognition required.
• Endianness costs one __builtin_bswap* behind a byte-order check (or the portable shift form only on hosts without the builtin).

2. After a store, tell the compiler the array is still exclusive.

lean_obj_res r = lean_sarray_ensure_exclusive(a);
memcpy(lean_sarray_cptr(r) + i, &v, sizeof v);
LEAN_ASSUME(r->m_rc == 1);   /* __builtin_assume / __assume / no-op */

• A byte store may alias anything, including the array's own m_rc. So the compiler must reload the reference count after every store and repeat the exclusivity check and copy path.
• A loop of usets therefore keeps a check-and-maybe-copy branch per store, which blocks unrolling and vectorization.
• The assumption is true by construction, since the array was exclusive or just copied. It costs nothing at runtime, and it lets the compiler keep a single check for a whole run of stores.
• Note that __builtin_assume(lean_is_exclusive(r)) is silently ignored, because clang treats the call as a possible side effect. The assumption has to name the field.
• A LEAN_ASSUME macro in lean.h would help the other scalar-array setters too.

Evidence.

• With both changes, our verified NTT matches Plonky3's parallel AVX2 NTT, a highly optimised Rust implementation. At a million points it is within 9–18% on one core and 19–23% faster on eight; results table.
• With the C as currently written in this PR and everything else identical, the same transform is 4.7× slower on one core (47 ms vs 10 ms) and 2.9× slower on eight.
• memcpy alone gives back 2.5×, and the exclusivity assumption the remaining 1.9×.