SIMD CPU Backend for Hesper

High-performance CPU vector operations using SIMD intrinsics (AVX2/NEON).

This module provides FFI bindings to optimized C++ implementations that leverage:

• AVX2 on x86_64 (8 floats per operation)
• NEON on ARM64 (4 floats per operation)
• Scalar fallback on other architectures

Example

let a := FloatArray.mk #[1.0, 2.0, 3.0, 4.0]
let b := FloatArray.mk #[5.0, 6.0, 7.0, 8.0]
let c := simdAdd a b  -- [6.0, 8.0, 10.0, 12.0]

@[extern lean_simd_backend_info]

opaque Hesper.Simd.backendInfo : IO String

Get information about the SIMD backend being used

def Hesper.Simd.simdAdd (a b : FloatArray) : FloatArray

SIMD-optimized Float64 vector addition: c = a + b

Adds two float arrays element-wise using SIMD instructions when available.

Safety: Returns empty array if input sizes don't match.

Performance:

• AVX2 (x86_64): 4 doubles/operation
• NEON (ARM64): 2 doubles/operation
• OpenMP multithreading for arrays ≥10K elements

Equations

• Hesper.Simd.simdAdd a b = if (a.size != b.size) = true then { data := #[] } else Hesper.Simd.simdAddF64Unsafe✝ a b

def Hesper.Simd.naiveAdd (a b : FloatArray) : FloatArray

Naive (non-SIMD) vector addition for benchmarking comparison.

Implemented in pure Lean using Array.mapIdx.

Equations

• Hesper.Simd.naiveAdd a b = if (a.size != b.size) = true then { data := #[] } else have result := Array.mapIdx (fun (i : Nat) (x : Float) => x + b.data[i]!) a.data; { data := result }

def Hesper.Simd.verifyEqual (a b : FloatArray) (epsilon : Float := 1e-6) : Bool

Verify two float arrays are equal within epsilon tolerance.

Used for correctness verification of SIMD operations.

Equations

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