Safe Buffer Operations

Type-safe buffer read/write utilities with runtime bounds checking. Backend-agnostic via [GPUBackend β].

def Hesper.Training.SafeBuffer.readU32 (bytes : ByteArray) (offset : Nat) : UInt32

Safely read a UInt32 (4 bytes LE) from a ByteArray. Returns 0 if out of bounds.

Equations

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

def Hesper.Training.SafeBuffer.readF32 (bytes : ByteArray) (offset : Nat) : Float

Safely read a Float32 from a ByteArray at the given byte offset.

Equations

• Hesper.Training.SafeBuffer.readF32 bytes offset = Hesper.Basic.float32BitsToFloat64 (Hesper.Training.SafeBuffer.readU32 bytes offset)

def Hesper.Training.SafeBuffer.readF32Array (bytes : ByteArray) (n : Nat) : Array Float

Safely read N Float32 values starting at byte offset 0.

Equations

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

@[inline]

def Hesper.Training.SafeBuffer.safeMapBufferReadF32 {β : Type} [GPUBackend β] (ctx : β) (buf : GPUBackend.Buf β) (numElements : Nat) : IO (Array Float)

Safely read a GPU buffer and return Float32 values.

Equations

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

@[inline]

def Hesper.Training.SafeBuffer.safeReadF32 {β : Type} [GPUBackend β] (ctx : β) (buf : GPUBackend.Buf β) (elementIdx : Nat := 0) : IO Float

Safely read a single Float32 from a GPU buffer at element index.

Equations

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

def Hesper.Training.SafeBuffer.isNaN (f : Float) : Bool

Equations

• Hesper.Training.SafeBuffer.isNaN f = (f != f)

@[inline]

def Hesper.Training.SafeBuffer.hasNaN {β : Type} [GPUBackend β] (ctx : β) (buf : GPUBackend.Buf β) (numElements : Nat) : IO Bool

Check if any value in a GPU buffer is NaN.

Equations

• Hesper.Training.SafeBuffer.hasNaN ctx buf numElements = do let vals ← Hesper.Training.SafeBuffer.safeMapBufferReadF32 ctx buf numElements pure (vals.any Hesper.Training.SafeBuffer.isNaN)