GGUF Binary Parser

Binary parser for GGUF v3 format files. Uses single ByteArray with offset tracking (following gemma.hs pattern for efficiency).

Design Principles

1. Single Buffer Allocation: Pin ByteArray once, pass offsets
2. Zero-Copy: Extract sub-arrays without copying when possible
3. Bounds Checking: Return Except for all parsing operations
4. Little-Endian: All integers are stored in little-endian format

References

• gemma.hs/src/Gemma/GGUF.hs - Memory pinning strategy
• llama.cpp/gguf-py/gguf/gguf_reader.py - Format specification

Low-level Binary Reading Utilities

def Hesper.GGUF.Parser.readUInt8 (data : ByteArray) (offset : Nat) : Except String (UInt8 × Nat)

Read UInt8 from ByteArray at offset

Equations

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

def Hesper.GGUF.Parser.readUInt16LE (data : ByteArray) (offset : Nat) : Except String (UInt16 × Nat)

Read UInt16 (little-endian) from ByteArray

Equations

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

def Hesper.GGUF.Parser.readUInt32LE (data : ByteArray) (offset : Nat) : Except String (UInt32 × Nat)

Read UInt32 (little-endian) from ByteArray

Equations

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

def Hesper.GGUF.Parser.readUInt64LE (data : ByteArray) (offset : Nat) : Except String (UInt64 × Nat)

Read UInt64 (little-endian) from ByteArray

Equations

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

def Hesper.GGUF.Parser.readInt32LE (data : ByteArray) (offset : Nat) : Except String (Int32 × Nat)

Read Int32 (little-endian) from ByteArray

Equations

• Hesper.GGUF.Parser.readInt32LE data offset = do let __discr ← Hesper.GGUF.Parser.readUInt32LE data offset match __discr with | (uval, newOffset) => Except.ok (uval.toInt32, newOffset)

def Hesper.GGUF.Parser.readInt64LE (data : ByteArray) (offset : Nat) : Except String (Int64 × Nat)

Read Int64 (little-endian) from ByteArray

Equations

• Hesper.GGUF.Parser.readInt64LE data offset = do let __discr ← Hesper.GGUF.Parser.readUInt64LE data offset match __discr with | (uval, newOffset) => Except.ok (uval.toInt64, newOffset)

def Hesper.GGUF.Parser.readFloat32LE (data : ByteArray) (offset : Nat) : Except String (Float × Nat)

Read Float32 (IEEE 754, little-endian) from ByteArray

Equations

• Hesper.GGUF.Parser.readFloat32LE data offset = do let __discr ← Hesper.GGUF.Parser.readUInt32LE data offset match __discr with | (bits, newOffset) => Except.ok (bits.toNat.toFloat, newOffset)

def Hesper.GGUF.Parser.readString (data : ByteArray) (offset : Nat) : Except String (String × Nat)

Read string (length-prefixed) from ByteArray

Equations

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

GGUF Header Parsing

def Hesper.GGUF.Parser.parseHeader (data : ByteArray) : Except String (GGUFHeader × Nat)

Parse GGUF header (24 bytes)

Equations

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

Metadata Parsing

def Hesper.GGUF.Parser.parseMetadataValue (data : ByteArray) (offset : Nat) : Except String (MetadataValue × Nat)

Parse a single metadata value (simplified - stores raw bytes)

Equations

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

def Hesper.GGUF.Parser.parseMetadataKV (data : ByteArray) (offset : Nat) : Except String ((String × MetadataValue) × Nat)

Parse single metadata key-value pair

Equations

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

def Hesper.GGUF.Parser.parseAllMetadata (data : ByteArray) (offset : Nat) (count : UInt64) : Except String (Array (String × MetadataValue) × Nat)

Parse all metadata key-value pairs

Equations

• Hesper.GGUF.Parser.parseAllMetadata data offset count = Hesper.GGUF.Parser.parseAllMetadata.loop data offset count.toNat #[]

partial def Hesper.GGUF.Parser.parseAllMetadata.loop (data : ByteArray) (offset remaining : Nat) (acc : Array (String × MetadataValue)) : Except String (Array (String × MetadataValue) × Nat)

Tensor Info Parsing

def Hesper.GGUF.Parser.parseDimensions (data : ByteArray) (offset : Nat) (nDims : UInt32) : Except String (Array UInt64 × Nat)

Parse dimensions array

Equations

• Hesper.GGUF.Parser.parseDimensions data offset nDims = Hesper.GGUF.Parser.parseDimensions.loop data offset nDims.toNat #[]

@[irreducible]

def Hesper.GGUF.Parser.parseDimensions.loop (data : ByteArray) (offset remaining : Nat) (acc : Array UInt64) : Except String (Array UInt64 × Nat)

Equations

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

def Hesper.GGUF.Parser.parseTensorInfo (data : ByteArray) (offset : Nat) : Except String (TensorInfo × Nat)

Parse single tensor info

Equations

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

def Hesper.GGUF.Parser.parseAllTensorInfos (data : ByteArray) (offset : Nat) (count : UInt64) : Except String (Array TensorInfo × Nat)

Parse all tensor infos

Equations

• Hesper.GGUF.Parser.parseAllTensorInfos data offset count = Hesper.GGUF.Parser.parseAllTensorInfos.loop data offset count.toNat #[]

partial def Hesper.GGUF.Parser.parseAllTensorInfos.loop (data : ByteArray) (offset remaining : Nat) (acc : Array TensorInfo) : Except String (Array TensorInfo × Nat)

Complete GGUF File Parsing

def Hesper.GGUF.Parser.alignmentPadding (offset : Nat) (alignment : UInt32) : Nat

Calculate alignment padding

Equations

• Hesper.GGUF.Parser.alignmentPadding offset alignment = if offset % alignment.toNat = 0 then 0 else alignment.toNat - offset % alignment.toNat

def Hesper.GGUF.Parser.parseGGUF (data : ByteArray) : Except String GGUFFile

Parse complete GGUF file

Equations

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