Bytes — fast unaligned reads, writes, and bulk ops on ByteArray

The functions in this module are declared @[extern] and route to small C functions in c/bytes_ffi.c at runtime. The Lean bodies remain the spec for kernel reduction and proofs: any in-bounds offset must produce the same result either way.

Out-of-bounds semantics

The whole module avoids panics; OOB is handled as a documented default:

• Loads are partial: each byte beyond data.size reads as 0, inheriting the ByteArray.get! runtime behaviour. So a loadU64LE whose last few bytes lie past the end returns the in-bounds prefix with the missing high bytes zeroed.
• Stores are atomic: if any byte of the requested write would fall outside data.size, the call is a no-op and data is returned unchanged. No partial writes.
• Bulk ops (copy, fill) are atomic in the same sense; equal returns false when ranges don't fit, compare returns .eq (a safe but information-losing default — callers that care must bounds-check).

Reads

Each loadU{N}{LE,BE} returns a UInt{N} of the natural width. To zero-extend to a wider type, use .toUInt64 etc. at the call site.

@[extern lean_bytes_load_u8]

def Bytes.loadU8 (data : ByteArray) (off : Nat) : UInt8

Read one byte from data at byte off. Returns 0 if OOB.

Equations

• Bytes.loadU8 data off = data.get! off

@[extern lean_bytes_load_u16_le]

def Bytes.loadU16LE (data : ByteArray) (off : Nat) : UInt16

Read a little-endian 16-bit word at byte off.

Equations

• Bytes.loadU16LE data off = (data.get! off).toUInt16 ||| (data.get! (off + 1)).toUInt16 <<< 8

@[extern lean_bytes_load_u16_be]

def Bytes.loadU16BE (data : ByteArray) (off : Nat) : UInt16

Read a big-endian 16-bit word at byte off.

Equations

• Bytes.loadU16BE data off = (data.get! off).toUInt16 <<< 8 ||| (data.get! (off + 1)).toUInt16

@[extern lean_bytes_load_u32_le]

def Bytes.loadU32LE (data : ByteArray) (off : Nat) : UInt32

Read a little-endian 32-bit word at byte off.

Equations

• Bytes.loadU32LE data off = (data.get! off).toUInt32 ||| (data.get! (off + 1)).toUInt32 <<< 8 ||| (data.get! (off + 2)).toUInt32 <<< 16 ||| (data.get! (off + 3)).toUInt32 <<< 24

@[extern lean_bytes_load_u32_be]

def Bytes.loadU32BE (data : ByteArray) (off : Nat) : UInt32

Read a big-endian 32-bit word at byte off.

Equations

• Bytes.loadU32BE data off = (data.get! off).toUInt32 <<< 24 ||| (data.get! (off + 1)).toUInt32 <<< 16 ||| (data.get! (off + 2)).toUInt32 <<< 8 ||| (data.get! (off + 3)).toUInt32

@[extern lean_bytes_load_u64_le]

def Bytes.loadU64LE (data : ByteArray) (off : Nat) : UInt64

Read a little-endian 64-bit word at byte off.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_load_u64_be]

def Bytes.loadU64BE (data : ByteArray) (off : Nat) : UInt64

Read a big-endian 64-bit word at byte off.

Equations

• One or more equations did not get rendered due to their size.

Writes

Stores take data by value, return the modified ByteArray, and preserve linearity at runtime: when the C function is given an exclusive reference it mutates in place; otherwise it copies once and mutates the copy. Atomic OOB semantics — any out-of-bounds byte makes the whole call a no-op.

@[extern lean_bytes_store_u8]

def Bytes.storeU8 (data : ByteArray) (off : Nat) (val : UInt8) : ByteArray

Write one byte at off. No-op if OOB.

Equations

• Bytes.storeU8 data off val = if off < data.size then data.set! off val else data

@[extern lean_bytes_store_u16_le]

def Bytes.storeU16LE (data : ByteArray) (off : Nat) (val : UInt16) : ByteArray

Write a little-endian 16-bit word at off. No-op if off+2 > data.size.

Equations

• Bytes.storeU16LE data off val = if off + 2 ≤ data.size then have b0 := val.toUInt8; have b1 := (val >>> 8).toUInt8; (data.set! off b0).set! (off + 1) b1 else data

@[extern lean_bytes_store_u16_be]

def Bytes.storeU16BE (data : ByteArray) (off : Nat) (val : UInt16) : ByteArray

Write a big-endian 16-bit word at off. No-op if off+2 > data.size.

Equations

• Bytes.storeU16BE data off val = if off + 2 ≤ data.size then have b0 := (val >>> 8).toUInt8; have b1 := val.toUInt8; (data.set! off b0).set! (off + 1) b1 else data

@[extern lean_bytes_store_u32_le]

def Bytes.storeU32LE (data : ByteArray) (off : Nat) (val : UInt32) : ByteArray

Write a little-endian 32-bit word at off. No-op if off+4 > data.size.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_store_u32_be]

def Bytes.storeU32BE (data : ByteArray) (off : Nat) (val : UInt32) : ByteArray

Write a big-endian 32-bit word at off. No-op if off+4 > data.size.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_store_u64_le]

def Bytes.storeU64LE (data : ByteArray) (off : Nat) (val : UInt64) : ByteArray

Write a little-endian 64-bit word at off. No-op if off+8 > data.size.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_store_u64_be]

def Bytes.storeU64BE (data : ByteArray) (off : Nat) (val : UInt64) : ByteArray

Write a big-endian 64-bit word at off. No-op if off+8 > data.size.

Equations

• One or more equations did not get rendered due to their size.

Bulk operations

Backed by memmove, memset, memcmp on the C side. All four are atomic w.r.t. OOB: if the requested range exceeds either array's size, copy/fill no-op, equal returns false, compare returns .eq.

@[extern lean_bytes_copy]

def Bytes.copy (src : ByteArray) (srcOff : Nat) (dst : ByteArray) (dstOff len : Nat) : ByteArray

Copy len bytes from src starting at srcOff into dst starting at dstOff. Aliasing is handled (uses memmove semantics on the C side). No-op if either range is OOB.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_fill]

def Bytes.fill (data : ByteArray) (off len : Nat) (val : UInt8) : ByteArray

Fill len bytes of data starting at off with val. No-op if off+len > data.size.

Equations

• Bytes.fill data off len val = if off + len > data.size then data else len.fold (fun (i : Nat) (x : i < len) (d : ByteArray) => d.set! (off + i) val) data

@[extern lean_bytes_equal]

def Bytes.equal (a : ByteArray) (aOff : Nat) (b : ByteArray) (bOff len : Nat) : Bool

Byte-equal: true iff a[aOff..aOff+len] = b[bOff..bOff+len]. Returns false if either range is OOB. The Lean spec walks the full range with an && accumulator (no early exit); the C runtime uses memcmp. Same observable result.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_bytes_compare]

def Bytes.compare (a : ByteArray) (aOff : Nat) (b : ByteArray) (bOff len : Nat) : Ordering

Lexicographic byte compare of two ranges. Returns .eq as the safe default if either range is OOB — callers that care must bounds-check. The spec walks the full range, keeping the first non-.eq decision; C side uses memcmp and exits early. Same observable result.

Equations

• One or more equations did not get rendered due to their size.