feat: fast fixed-width integer load/store on ByteArray (native UInt16/UInt32/UInt64 accessors) #14050

Lean can do a single native scalar load/store out of a contiguous unboxed buffer for exactly two element types today:

• ByteArray (lean_sarray of UInt8): uget/uset compile to one bounds-free byte load/store (lean_sarray_cptr(a)[i]).
• FloatArray (lean_sarray of Float/64-bit): same.

Code that wants a dense array of a fixed-width integer (UInt16/UInt32/UInt64) has no equivalent. The two encodings available are both bad:

1. Array UInt32 — a pointer-slot array of Lean objects, not a contiguous uint32_t buffer. On 64-bit the elements are tagged immediates rather than heap boxes, but each still occupies a pointer-width slot and a read is lean_array_fget + unbox.
2. A ByteArray with manual little-endian packing — contiguous and unboxed, but every element access is written in pure Lean as several fgets + shifts/ors + Nat offset arithmetic, where a native array would do one load.

This proposal is not a new type. The contiguous unboxed buffer already exists — it is ByteArray. What is missing is a small set of @[extern] wide load/store accessors on ByteArray that read/write a UInt16/UInt32/UInt64 in (typically) a single native load, plus their verification lemmas. Dedicated UIntNArray types are noted at the end as a much larger ask for the same generated code.

What core already has (v4.30.0-rc2, nightly 2026-06-10)

• ByteArray.toUInt64LE! / toUInt64BE! exist (Init/Data/ByteArray/Extra.lean), but are pure-Lean byte assembly (8× get! + shift + or), operate on a whole size-8 array (no offset), have no UInt16/UInt32 siblings, and are not @[extern].
• The only single-load scalar extern is lean_byte_array_uget (UInt8).

ByteArray is the contiguous representation; the reason toUInt64LE! reads as byte assembly is that it is written in Lean as shifts and ors, not that the storage cannot do a wide load (lean_sarray_cptr is right there). The missing piece is intrinsics, not a type.

Proposal: wide load/store accessors on ByteArray

For each width w ∈ {16, 32, 64}, byte-offset addressed, explicit little- and big-endian, modelled on uget/uset. UInt32 as the worked example:

@[extern "lean_byte_array_uget_uint32le"]
def ByteArray.ugetUInt32LE (a : @& ByteArray) (i : USize)
    (h : i.toNat + 4 ≤ a.size) : UInt32

def ByteArray.ugetUInt32BE (a : @& ByteArray) (i : USize)
    (h : i.toNat + 4 ≤ a.size) : UInt32

-- in-place when the array is exclusive, otherwise copied
def ByteArray.usetUInt32LE (a : ByteArray) (i : USize) (v : UInt32)
    (h : i.toNat + 4 ≤ a.size) : ByteArray

plus the ! and bounds-returning siblings the existing API has, with the same out-of-bounds contract: getUInt32LE! returns 0 (as get! does), setUInt32LE! returns the array unchanged (as set! does). i is a byte offset, the most general primitive: an "array of UInt32" view is i = k*4, and the common codec case "read a UInt32 at an arbitrary position" is the same call with arbitrary i. A native-endian (reinterpret) variant is plausible but secondary; LE/BE cover the real use cases and optimize just as well, so I'd leave NE out of the first cut.

Codegen

uint32_t lean_byte_array_uget_uint32le(b_lean_obj_arg a, size_t i) {
    uint32_t x;
    memcpy(&x, lean_sarray_cptr(a) + i, sizeof(x)); // fixed-size load, no aliasing/alignment UB
    return /* identity on LE, byte-swap on BE — via a portable bswap helper/compiler builtin */ x;
}

A fixed-size memcpy lowers to a single load (plus a bswap/movbe for the endian conversion) on optimizing native backends, and avoids the strict-aliasing/alignment UB of a raw pointer cast. So even the portable LE/BE accessors are a load plus an optional byte-swap, versus several byte loads + shifts + ors for the pure-Lean version. (Endianness should use a portable swap helper or compiler builtin, not the BSD le32toh.)

Verification lemmas

ByteArray is usable in proofs because of its lemma set; ship the analogues:

• size_usetUInt32LE (= a.size), size_* for every setter
• read-after-write, same window (ugetUInt32LE (usetUInt32LE a i v) i = v) and disjoint window (needs a 4-byte interval-overlap hypothesis — the one genuinely new lemma shape versus ByteArray's single-byte cells)
• agreement with a pure-Lean reference. This means introducing offset-taking reference specs at each width (toUInt16LE/BE, toUInt32LE/BE, toUInt64LE/BE with an offset, generalizing the existing whole-array toUInt64LE!) and proving the externs agree with them — so the slow definition is the proof-level semantics and the extern is translation-validated against it.
• uget/get/! agreement, as for ByteArray.

Alignment

On the current 64-bit runtime sizeof(lean_sarray_object) == 24 (lean_object header + two size_t) and lean_alloc_object rounds to LEAN_OBJECT_SIZE_DELTA = 8, so m_data is 8-byte aligned; element-aligned offsets (i = k*w) are then naturally aligned up to 64 bits. This is not load-bearing: because the implementation uses memcpy, correctness does not depend on alignment, and arbitrary byte offsets (a UInt32 at an odd position) are handled with one unaligned load on x86/modern ARM or a compiler fixup elsewhere. So there is no alignment reason to withhold this from plain ByteArray.

Length need not be a multiple of the width

Byte-offset addressing sidesteps it: the bound is i.toNat + 4 ≤ a.size regardless of a.size % 4, and leftover trailing bytes are simply not reachable as a full UInt32. An element-indexed view on top (sizeUInt32 := a.size / 4, bound k < sizeUInt32) is equivalent to 4*k + 4 ≤ a.size since 4 divides 4*k, keeping the clean k < size lemma shape.

Secondary: typed arrays

If typed ergonomics are wanted, they can be a thin library wrapper over the primitives above — structure UInt32Array where bytes : ByteArray; mult : bytes.size % 4 = 0, with size := bytes.size / 4 and accessors delegating to the externs — zero runtime cost and no core change. First-class UInt32Array/UInt64Array types are a much larger undertaking (frontend/compiler/library plumbing, deriving/serialization decisions, conversions, a parallel lemma set) for codegen identical to the wrapper, and are not required for the scalar-load win. The one thing only a first-class type could add is over-aligned storage for SIMD, but lean_sarray does not over-align today, so that is a separate runtime change either way. (USize, being platform-width, and Float32 are natural later additions but out of scope for the fixed-width ask here.)

User experience / beneficiaries / maintainability

• User experience: a single native UInt16/UInt32/UInt64 load/store out of the buffer type users already have, with the lemmas needed to use it in verified code.
• Beneficiaries: binary parsers and codecs (the existing toUInt64LE!, every ByteArray-based decoder), and dense numeric workloads (graph/CSR, hash tables keyed by small ints, DSP). Concrete motivation: a pure-Lean DEFLATE implementation (lean-zip) — converting the LZ77 match loop's indices to USize + ByteArray.uget gave a 1.23×–1.8× end-to-end compress win, but the prev/hashTable position arrays have no single-load home: Array Nat is a tagged load, Array UInt32 adds an unbox, and ByteArray + manual packing is byte assembly.
• Maintainability: additive @[extern] functions + lemmas on an existing type — no new runtime type, GC case, or serialization handling. The typed-array question, if pursued, is a library wrapper rather than a compiler feature.

🤖 Prepared with Claude Code