Documentation

Hesper.Core.Float32Array

Float32Array - Opaque Type Implementation #

High-performance Float32 array with zero-copy GPU interop and in-place mutations.

Key Advantages #

  1. Zero Copy: Direct pointer passing to WebGPU (no conversion overhead)
  2. Memory Efficient: Native C++ std::vector<float>, not boxed Lean objects
  3. In-Place Updates: Mutable operations in IO monad (no array copying)
  4. 2x Memory Savings: vs Float64 (4 bytes/element vs 8 bytes/element)
  5. Better SIMD: AVX2 8 floats/op vs 4 doubles/op, NEON 4 vs 2

Implementation Pattern #

Usage #

-- Create array of 1000 elements (allocated in C++ heap)
let arr ← Float32Array.create 1000

-- Set values (in-place mutation, no copying!)
arr.set 0 3.14
arr.set 1 2.71

-- Get values (converts f32 → f64 only when reading)
let val ← arr.get 0  -- returns Float (f64)

-- Pass to GPU (zero-copy!)
let ptr ← arr.ptr
let size ← arr.byteSize
-- Use ptr with wgpuQueueWriteBuffer(queue, buffer, 0, ptr, size)

Type Definition #

source
opaque Hesper.Core.Float32ArrayPointed :
NonemptyType

Opaque type representing a C++ std::vector<float>. Contents are invisible to Lean - all operations go through FFI.

source
def Hesper.Core.Float32Array :
Type u_1

Float32 array type (opaque to Lean, managed by C++)

Equations
Instances For
    source
    instance Hesper.Core.instNonemptyFloat32Array :
    Nonempty Float32Array

    Creation and Destruction #

    source
    @[extern lean_f32_array_create]
    opaque Hesper.Core.Float32Array.create (size : USize) :
    IO Float32Array

    Create a new Float32Array with the specified number of elements. All elements are initialized to 0.0f.

    C++ Implementation: new std::vector<float>(size, 0.0f)

    Element Access #

    source
    @[extern lean_f32_array_set]
    opaque Hesper.Core.Float32Array.set (self : Float32Array) (index : USize) (value : Float) :
    IO Unit

    Set a value at the specified index (in-place mutation). Value is converted from Float64 to Float32.

    Safety: Out-of-bounds access will return error. Performance: O(1), in-place update (no array copy).

    source
    @[extern lean_f32_array_get]
    opaque Hesper.Core.Float32Array.get (self : Float32Array) (index : USize) :
    IO Float

    Get a value at the specified index. Value is converted from Float32 to Float64.

    Safety: Out-of-bounds access will return error. Performance: O(1).

    Array Properties #

    source
    @[extern lean_f32_array_size]
    opaque Hesper.Core.Float32Array.size (self : Float32Array) :
    USize

    Get the number of Float32 elements in the array.

    Performance: O(1) - calls vec.size().

    source
    @[extern lean_f32_array_byte_size]
    opaque Hesper.Core.Float32Array.byteSize (self : Float32Array) :
    IO USize

    Get the size in bytes (for GPU buffer allocation).

    Returns: size * sizeof(float) = size * 4 Performance: O(1).

    GPU Interop (Zero-Copy Pointer Access) #

    source
    @[extern lean_f32_array_ptr]
    opaque Hesper.Core.Float32Array.ptr (self : Float32Array) :
    IO USize

    Get the raw pointer to the underlying data for GPU operations.

    UNSAFE: This returns a raw pointer (size_t) to vec.data(). The pointer is only valid while the Float32Array object is alive.

    Use Case: Pass to wgpuQueueWriteBuffer for zero-copy uploads:

    let ptr ← arr.ptr
let size ← arr.byteSize
-- C++: wgpuQueueWriteBuffer(queue, buffer, 0, (void*)ptr, size)

    Safety: Caller must ensure:

    1. Float32Array stays alive during GPU operation
    2. No concurrent modifications while GPU reads

    Conversions #

    source
    @[extern lean_f32_array_from_float_array]
    opaque Hesper.Core.Float32Array.fromFloatArray (arr : Array Float) :
    IO Float32Array

    Create Float32Array from Lean's native Array Float.

    Performance: O(n) - each Float64 is converted to Float32. Use Case: Initial data preparation from Lean computations.

    source
    @[extern lean_f32_array_to_float_array]
    opaque Hesper.Core.Float32Array.toFloatArray (self : Float32Array) :
    IO (Array Float)

    Convert Float32Array to Lean's native Array Float.

    Performance: O(n) - each Float32 is converted to Float64. Use Case: Reading results back into Lean for verification/analysis.

    SIMD Operations #

    source
    @[extern lean_f32_array_simd_add]
    opaque Hesper.Core.Float32Array.simdAdd (a : Float32Array) (b : Float32Array) :
    IO Float32Array

    SIMD element-wise addition: result[i] = a[i] + b[i]

    Hardware Acceleration:

    • x86_64: AVX2 (8 floats/operation)
    • ARM64: NEON (4 floats/operation)

    Safety: Arrays must have same size, returns error otherwise. Performance: ~8x faster than scalar on AVX2, ~4x on NEON.

    source
    @[extern lean_f32_array_simd_mul]
    opaque Hesper.Core.Float32Array.simdMul (a : Float32Array) (b : Float32Array) :
    IO Float32Array

    SIMD element-wise multiplication: result[i] = a[i] * b[i]

    Utilities #

    source
    def Hesper.Core.Float32Array.toString (arr : Float32Array) :
    IO String

    String representation for debugging (shows first 8 elements)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Hesper.Core.instToStringFloat32Array :
      ToString Float32Array
      Equations