Documentation

Hesper.GGUF.Types

GGUF Format Type Definitions #

GGUF (Generic Graph Universal Format) is a binary format for storing large language models. This module defines the core data structures for the GGUF v3 format.

Format Structure #

[Header]        - Magic number, version, counts
[Metadata]      - Key-value pairs (architecture, hyperparameters)
[Tensor Info]   - Tensor descriptors (name, shape, type, offset)
[Alignment]     - Padding to align tensor data
[Tensor Data]   - Raw binary blobs

Reference #

Specification: https://github.com/ggerganov/ggml/blob/master/docs/gguf.md
Implementation: llama.cpp/gguf-py/gguf/gguf_reader.py

def Hesper.GGUF.GGUF_MAGIC :

GGUF file magic number: 0x46554747 ("GGUF" in ASCII)

Equations

Hesper.GGUF.GGUF_MAGIC = 1179993927

Instances For

def Hesper.GGUF.GGUF_VERSION :

Supported GGUF version

Equations

Hesper.GGUF.GGUF_VERSION = 3

Instances For

def Hesper.GGUF.GGUF_DEFAULT_ALIGNMENT :

Default alignment for tensor data (32 bytes)

Equations

Hesper.GGUF.GGUF_DEFAULT_ALIGNMENT = 32

Instances For

inductive Hesper.GGUF.GGMLType :

GGML tensor types (quantization formats)

Instances For

instance Hesper.GGUF.instReprGGMLType :

Equations

Hesper.GGUF.instReprGGMLType = { reprPrec := Hesper.GGUF.instReprGGMLType.repr }

def Hesper.GGUF.instReprGGMLType.repr :

GGMLType → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.F32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.F32")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.F16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.F16")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q4_0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q4_0")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q4_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q4_1")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q5_0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q5_0")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q5_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q5_1")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q8_0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q8_0")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q8_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q8_1")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q2_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q2_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q3_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q3_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q4_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q4_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q5_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q5_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q6_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q6_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.Q8_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.Q8_K")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.I8 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.I8")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.I16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.I16")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.I32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.I32")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.I64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.I64")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.F64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.F64")).group prec✝
Hesper.GGUF.instReprGGMLType.repr Hesper.GGUF.GGMLType.BF16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.GGUF.GGMLType.BF16")).group prec✝

Instances For

def Hesper.GGUF.instBEqGGMLType.beq :

GGMLType → GGMLType → Bool

Equations

Hesper.GGUF.instBEqGGMLType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Hesper.GGUF.instBEqGGMLType :

Equations

Hesper.GGUF.instBEqGGMLType = { beq := Hesper.GGUF.instBEqGGMLType.beq }

def Hesper.GGUF.instInhabitedGGMLType.default :

Equations

Hesper.GGUF.instInhabitedGGMLType.default = Hesper.GGUF.GGMLType.F32

Instances For

instance Hesper.GGUF.instInhabitedGGMLType :

Inhabited GGMLType

Equations

Hesper.GGUF.instInhabitedGGMLType = { default := Hesper.GGUF.instInhabitedGGMLType.default }

def Hesper.GGUF.GGMLType.toUInt32 :

GGMLType → UInt32

Convert GGMLType to its numeric ID used in GGUF files

Equations

Instances For

def Hesper.GGUF.GGMLType.fromUInt32 (id : UInt32) :

Except String GGMLType

Parse GGMLType from numeric ID

Equations

Instances For

def Hesper.GGUF.GGMLType.isTernary :

GGMLType → Bool

Check if type is a ternary (BitNet) quantization format

Equations

Instances For

def Hesper.GGUF.GGMLType.bytesPerElement :

GGMLType → Nat

Get the bytes per element for unquantized types

Equations

Instances For

instance Hesper.GGUF.instToStringGGMLType :

ToString GGMLType

Equations

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

inductive Hesper.GGUF.MetadataValueType :

Metadata value types in GGUF

Instances For

def Hesper.GGUF.instReprMetadataValueType.repr :

MetadataValueType → Nat → Std.Format

Equations

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

Instances For

instance Hesper.GGUF.instReprMetadataValueType :

Repr MetadataValueType

Equations

Hesper.GGUF.instReprMetadataValueType = { reprPrec := Hesper.GGUF.instReprMetadataValueType.repr }

def Hesper.GGUF.instBEqMetadataValueType.beq :

MetadataValueType → MetadataValueType → Bool

Equations

Hesper.GGUF.instBEqMetadataValueType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Hesper.GGUF.instBEqMetadataValueType :

BEq MetadataValueType

Equations

Hesper.GGUF.instBEqMetadataValueType = { beq := Hesper.GGUF.instBEqMetadataValueType.beq }

def Hesper.GGUF.instInhabitedMetadataValueType.default :

MetadataValueType

Equations

Hesper.GGUF.instInhabitedMetadataValueType.default = Hesper.GGUF.MetadataValueType.MUInt8

Instances For

instance Hesper.GGUF.instInhabitedMetadataValueType :

Inhabited MetadataValueType

Equations

Hesper.GGUF.instInhabitedMetadataValueType = { default := Hesper.GGUF.instInhabitedMetadataValueType.default }

instance Hesper.GGUF.instToStringMetadataValueType :

ToString MetadataValueType

Equations

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

def Hesper.GGUF.MetadataValueType.fromNat (id : Nat) :

Except String MetadataValueType

Parse MetadataValueType from numeric ID

Equations

Instances For

structure Hesper.GGUF.MetadataValue :

Metadata value (simplified - stores raw bytes for now)

valueType : MetadataValueType
data : ByteArray

Instances For

instance Hesper.GGUF.instInhabitedMetadataValue :

Inhabited MetadataValue

Equations

Hesper.GGUF.instInhabitedMetadataValue = { default := Hesper.GGUF.instInhabitedMetadataValue.default }

def Hesper.GGUF.instInhabitedMetadataValue.default :

Equations

Hesper.GGUF.instInhabitedMetadataValue.default = { valueType := default, data := default }

Instances For

instance Hesper.GGUF.instReprMetadataValue :

Repr MetadataValue

Equations

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

structure Hesper.GGUF.GGUFHeader :

GGUF file header

magic : UInt32
version : UInt32
tensorCount : UInt64
metadataKVCount : UInt64

Instances For

def Hesper.GGUF.instReprGGUFHeader.repr :

GGUFHeader → Nat → Std.Format

Equations

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

Instances For

instance Hesper.GGUF.instReprGGUFHeader :

Repr GGUFHeader

Equations

Hesper.GGUF.instReprGGUFHeader = { reprPrec := Hesper.GGUF.instReprGGUFHeader.repr }

instance Hesper.GGUF.instInhabitedGGUFHeader :

Inhabited GGUFHeader

Equations

Hesper.GGUF.instInhabitedGGUFHeader = { default := Hesper.GGUF.instInhabitedGGUFHeader.default }

def Hesper.GGUF.instInhabitedGGUFHeader.default :

Equations

Hesper.GGUF.instInhabitedGGUFHeader.default = { magic := default, version := default, tensorCount := default, metadataKVCount := default }

Instances For

structure Hesper.GGUF.TensorInfo :

Tensor information (metadata about a single tensor)

name : String
nDims : UInt32
dimensions : Array UInt64
ggmlType : GGMLType
offset : UInt64

Instances For

instance Hesper.GGUF.instReprTensorInfo :

Repr TensorInfo

Equations

Hesper.GGUF.instReprTensorInfo = { reprPrec := Hesper.GGUF.instReprTensorInfo.repr }

def Hesper.GGUF.instReprTensorInfo.repr :

TensorInfo → Nat → Std.Format

Equations

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

Instances For

def Hesper.GGUF.instInhabitedTensorInfo.default :

Equations

Hesper.GGUF.instInhabitedTensorInfo.default = { name := default, nDims := default, dimensions := default, ggmlType := default, offset := default }

Instances For

instance Hesper.GGUF.instInhabitedTensorInfo :

Inhabited TensorInfo

Equations

Hesper.GGUF.instInhabitedTensorInfo = { default := Hesper.GGUF.instInhabitedTensorInfo.default }

def Hesper.GGUF.TensorInfo.numElements (ti : TensorInfo) :

Calculate total number of elements in tensor

Equations

ti.numElements = Array.foldl (fun (x1 x2 : UInt64) => x1 * x2) 1 ti.dimensions

Instances For

def Hesper.GGUF.TensorInfo.sizeBytes (ti : TensorInfo) :

Calculate size in bytes (for quantized types, this is approximate)

Equations

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

Instances For

structure Hesper.GGUF.GGUFFile :

Complete GGUF file structure

header : GGUFHeader
metadata : Array (String × MetadataValue)
tensors : Array TensorInfo
dataBlob : ByteArray
alignment : UInt32
mmap : Option CUDA.MMappedFile
Optional mmap handle. When set, dataBlob is empty (or holds only a prefix for metadata parsing) and tensor bodies are read from the mmap at dataSectionOffset + tensor.offset. The mmap's lifetime is tied to this Lean object via GC, so any GPU weight upload issued async while the GGUFFile reference is live is safe to complete.
dataSectionOffset : USize
Absolute file offset where the aligned tensor-data section starts. Only meaningful when mmap.isSome. Tensor body at mmap offset = dataSectionOffset + tensorInfo.offset.

Instances For

def Hesper.GGUF.instInhabitedGGUFFile.default :

Equations

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

Instances For

instance Hesper.GGUF.instInhabitedGGUFFile :

Inhabited GGUFFile

Equations

Hesper.GGUF.instInhabitedGGUFFile = { default := Hesper.GGUF.instInhabitedGGUFFile.default }

instance Hesper.GGUF.instReprGGUFFile :

Equations

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

def Hesper.GGUF.GGUFFile.findTensor (gf : GGUFFile) (name : String) :

Option TensorInfo

Find tensor by name

Equations

gf.findTensor name = Array.find? (fun (x : Hesper.GGUF.TensorInfo) => x.name == name) gf.tensors

Instances For

def Hesper.GGUF.GGUFFile.tensorNames (gf : GGUFFile) :

Get tensor names

Equations

gf.tensorNames = Array.map (fun (x : Hesper.GGUF.TensorInfo) => x.name) gf.tensors

Instances For

def Hesper.GGUF.GGUFFile.findMetadata (gf : GGUFFile) (key : String) :

Option MetadataValue

Find metadata value by key

Equations

gf.findMetadata key = Option.map (fun (x : String × Hesper.GGUF.MetadataValue) => x.snd) (Array.find? (fun (x : String × Hesper.GGUF.MetadataValue) => x.fst == key) gf.metadata)

Instances For

def Hesper.GGUF.GGUFFile.getTensorData (gf : GGUFFile) (ti : TensorInfo) :

Extract tensor data as ByteArray

Equations

gf.getTensorData ti = gf.dataBlob.extract ti.offset.toNat (ti.offset.toNat + ti.sizeBytes.toNat)

Instances For