GGUF Reader - High-Level API

High-level interface for loading and accessing GGUF files.

Usage Example

def main : IO Unit := do
  -- Load GGUF file
  let gguf ← loadGGUF "model.gguf"

  -- Query model info
  IO.println s!"Architecture: {gguf.getMetadataString "general.architecture"}"
  IO.println s!"Tensors: {gguf.header.tensorCount}"

  -- Get tensor by name
  match gguf.findTensor "blk.0.attn_q.weight" with
  | some ti =>
    IO.println s!"Found tensor: {ti.name}, shape: {ti.dimensions}"
    let data ← gguf.getTensorFloat32 ti
    IO.println s!"First 10 values: {data.extract 0 10}"
  | none => IO.println "Tensor not found"

File Loading

def Hesper.GGUF.loadGGUF (path : String) : IO GGUFFile

Load GGUF file from disk

Equations

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

def Hesper.GGUF.loadGGUFMmap (path : String) : IO GGUFFile

Load GGUF with mmap: only the metadata prefix is copied into a Lean ByteArray (for parser); tensor data is referenced directly via the mmap handle attached to the returned GGUFFile.

The returned GGUFFile keeps the mmap alive via .mmap; tensor body uploads should use Hesper.CUDA.cuMemcpyHtoDFromMmap with gguf.dataSectionOffset + tensor.offset instead of reading dataBlob (which is empty in this mode). getTensorData still works against the prefix copy, but is now a no-op for tensor bodies — callers must handle mmap explicitly.

Equations

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

def Hesper.GGUF.loadGGUFHeader (path : String) (maxPrefixBytes : Nat := 256 * 1024 * 1024) : IO GGUFFile

Load only the GGUF header (metadata + tensor infos) by reading a bounded prefix of the file — without copying the tensor body. loadGGUF/loadGGUFMmap both slurp the entire file into a ByteArray, which is unsafe for very large models (a 16 GB file allocates 16 GB).

Tensor bodies live after the aligned data section, so a prefix that covers metadata + tensor-infos is sufficient: parseGGUF sets dataBlob := ByteArray.empty when the prefix ends before the data section, and metadata + tensor infos still parse correctly.

Pure Lean IO (no CUDA/mmap), so it works on every backend. Use for introspection / validation (config, tensor presence, shapes); tensor body uploads are NOT possible from the returned file. maxPrefixBytes must exceed the metadata+tensor-info size (a few MB even for huge models).

Equations

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

Extended GGUFFile API

def Hesper.GGUF.GGUFFile.getMetadataString (gf : GGUFFile) (key : String) : Option String

Get metadata value as String (if it exists and is a string)

Equations

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

def Hesper.GGUF.GGUFFile.getMetadataUInt32 (gf : GGUFFile) (key : String) : Option UInt32

Get metadata value as UInt32

Equations

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

def Hesper.GGUF.GGUFFile.getMetadataUInt64 (gf : GGUFFile) (key : String) : Option UInt64

Get metadata value as UInt64

Equations

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

def Hesper.GGUF.GGUFFile.getArchitecture (gf : GGUFFile) : Option String

Get model architecture string

Equations

• gf.getArchitecture = gf.getMetadataString "general.architecture"

def Hesper.GGUF.GGUFFile.getModelName (gf : GGUFFile) : Option String

Get model name

Equations

• gf.getModelName = gf.getMetadataString "general.name"

def Hesper.GGUF.GGUFFile.getLayerCount (gf : GGUFFile) : Option UInt32

Get number of layers

Equations

• gf.getLayerCount = match gf.getArchitecture with | some arch => gf.getMetadataUInt32 (toString arch ++ toString ".block_count") | none => none

def Hesper.GGUF.GGUFFile.getHiddenSize (gf : GGUFFile) : Option UInt32

Get hidden dimension size

Equations

• gf.getHiddenSize = match gf.getArchitecture with | some arch => gf.getMetadataUInt32 (toString arch ++ toString ".embedding_length") | none => none

def Hesper.GGUF.GGUFFile.getAttentionHeadCount (gf : GGUFFile) : Option UInt32

Get attention head count

Equations

• gf.getAttentionHeadCount = match gf.getArchitecture with | some arch => gf.getMetadataUInt32 (toString arch ++ toString ".attention.head_count") | none => none

def Hesper.GGUF.GGUFFile.getTensorFloat32 (gf : GGUFFile) (ti : TensorInfo) : IO (Array Float)

Get tensor data as Float32 array (automatically dequantizes)

Equations

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

def Hesper.GGUF.GGUFFile.getTensorRaw (gf : GGUFFile) (ti : TensorInfo) : ByteArray

Get tensor data as raw ByteArray (no dequantization)

⚠️ Use this for GPU inference! This preserves the quantized format (TQ2_0, Q4_0, etc.) for direct GPU upload. Decode on-the-fly in WGSL compute shaders for optimal performance.

Equations

• gf.getTensorRaw ti = gf.getTensorData ti

GPU Upload API

def Hesper.GGUF.GGUFFile.uploadTensorQuantized {α : Sort u_1} {β : Type} (gf : GGUFFile) (device : α) (ti : TensorInfo) : IO β

Upload quantized tensor directly to GPU buffer

This is the recommended approach for inference with quantized models.

Performance benefits:

• ✅ 16x less PCIe bandwidth (for TQ2_0: 2-bit vs 32-bit)
• ✅ Decode on-the-fly in GPU shaders (kernel fusion)
• ✅ No intermediate CPU memory allocation

Example usage:

let gguf ← loadGGUF "model.gguf"
let weightTensor := gguf.findTensor "blk.0.attn_q.weight" |>.get!
let gpuBuf ← gguf.uploadTensorQuantized device weightTensor
-- Now use gpuBuf in BitLinear layer

@param device WebGPU device @param ti Tensor info @return GPU buffer containing quantized data

Equations

• gf.uploadTensorQuantized device ti = throw (IO.userError "uploadTensorQuantized: WebGPU integration not yet available in this module")

def Hesper.GGUF.GGUFFile.findTensorsByPattern (gf : GGUFFile) (pattern : String) : Array TensorInfo

Find tensor by pattern (substring match)

Equations

• gf.findTensorsByPattern pattern = Array.filter (fun (ti : Hesper.GGUF.TensorInfo) => ti.name.startsWith pattern || decide (pattern.toList ⊆ ti.name.toList)) gf.tensors

def Hesper.GGUF.GGUFFile.getLayerTensors (gf : GGUFFile) (layerIdx : Nat) : Array TensorInfo

Get all tensors of a specific layer

Equations

• gf.getLayerTensors layerIdx = Array.filter (fun (ti : Hesper.GGUF.TensorInfo) => ti.name.startsWith (toString "blk." ++ toString layerIdx ++ toString ".")) gf.tensors

def Hesper.GGUF.GGUFFile.printSummary (gf : GGUFFile) : IO Unit

Print file summary

Equations

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

Tensor Name Mapping Utilities

def Hesper.GGUF.hfToGGUFTensorName (hfName : String) : Option String

Convert HuggingFace tensor name to GGUF tensor name Example: "model.layers.0.self_attn.q_proj.weight" → "blk.0.attn_q.weight"

Equations

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

def Hesper.GGUF.GGUFFile.findTensorByHFName (gf : GGUFFile) (hfName : String) : Option TensorInfo

Find tensor by HuggingFace name

Equations

• gf.findTensorByHFName hfName = match Hesper.GGUF.hfToGGUFTensorName hfName with | some ggufName => gf.findTensor ggufName | none => none