Function lean_alloc_sarray 

pub unsafe fn lean_alloc_sarray(
    elem_size: u32,
    size: usize,
    capacity: usize,
) -> lean_obj_res

Allocate a freshly initialised scalar-array (lean.h:1004–1010).

Returns a LeanScalarArray-tagged object with m_size = size, m_capacity = capacity, and elem_size bytes per element. The payload bytes are uninitialised; the caller must write to lean_sarray_cptr before the array escapes.

Safety

• elem_size must fit a u8 (Lean stores it in m_other) and must be one of {1, 2, 4, 8} for the existing scalar-array consumers (ByteArray uses 1).
• size <= capacity.
• size_of::<LeanSArrayObjectRepr>() + elem_size * capacity must not overflow usize; the helper checks this with strict_* arithmetic and panics on overflow (mirroring lean_alloc_sarray_would_overflow).