Basic Utilities

Utility functions and helpers for the Hesper library.

@[extern lean_hesper_float64_to_bytes]

opaque Hesper.Basic.floatToBytes (f : Float) : IO ByteArray

Convert Float64 (Lean Float) to 4 bytes (little-endian f32) Uses FFI to properly convert f64→f32→bytes

def Hesper.Basic.float32BitsToFloat64 (bits : UInt32) : Float

Convert IEEE 754 float32 bit pattern to Lean Float (float64). Float.ofBits expects float64 bits, so we must manually convert.

Equations

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

def Hesper.Basic.bytesToFloat (bytes : ByteArray) (offset : Nat := 0) : Float

Convert 4 bytes (little-endian) to Float

Equations

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

def Hesper.Basic.floatArrayToBytes (arr : Array Float) : IO ByteArray

Convert an array of floats to a byte array

Equations

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

@[extern lean_hesper_bytes_to_float64]

opaque Hesper.Basic.bytesToFloat64FFI (bytes : ByteArray) (offset : UInt32) : IO Float

Convert 4 bytes (little-endian f32) to Float (f64) Uses FFI to properly interpret f32 bits and convert to f64

def Hesper.Basic.bytesToFloat32 (bytes : ByteArray) (offset : Nat := 0) : IO Float

Convert 4 bytes (little-endian f32) to Float (f64) Properly handles f32→f64 conversion via FFI

Equations

• Hesper.Basic.bytesToFloat32 bytes offset = if offset + 4 > bytes.size then pure 0.0 else Hesper.Basic.bytesToFloat64FFI bytes offset.toUInt32

def Hesper.Basic.bytesToFloatArray (bytes : ByteArray) : IO (Array Float)

Convert a byte array of f32 (GPU 32-bit floats) to Array Float (Lean 64-bit doubles) Uses FFI to properly convert each f32 to f64

Equations

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

def Hesper.Basic.bytesToFloatArrayPure (bytes : ByteArray) : Array Float

Pure version (fallback implementation using Lean) Note: This doesn't properly handle f32→f64 conversion! Use the FFI version above.

Equations

• Hesper.Basic.bytesToFloatArrayPure bytes = Array.map (fun (i : Nat) => Hesper.Basic.bytesToFloat bytes (i * 4)) (Array.range (bytes.size / 4))

def Hesper.Basic.uint32ToBytes (n : UInt32) : ByteArray

Convert UInt32 to 4 bytes (little-endian)

Equations

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

def Hesper.Basic.bytesToUInt32 (bytes : ByteArray) (offset : Nat := 0) : UInt32

Convert 4 bytes (little-endian) to UInt32

Equations

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

@[extern lean_hesper_get_time_ns]

opaque Hesper.Basic.getTimeNs : IO UInt64

Get high-precision system time in nanoseconds. Used for benchmarking GPU performance.