Skip to content

stdlib.simd

SIMD Module (Single Instruction Multiple Data)

Generated from v0.65.7. 5 source files, 105 documented symbols.

gather.xi

fn gather_load[T](base: Int, indices: &Vec[Int]) -> Vec[T]

Load T values from base + index for every index. Scalar fallback: generic memory loads are unavailable -- returns default T() values with one element per index (documented). Complexity: O(len(indices)).

  • Postcondition: result.len() == indices.len()
fn gather_load4[T](base: Int, i0: Int, i1: Int, i2: Int, i3: Int) -> (T, T, T, T)

Load four T values; the tuple is the four gathered values. Scalar fallback: returns default T() values (documented). Complexity: O(1).

  • Precondition: true
fn scatter_store[T](base: Int, indices: &Vec[Int], values: &Vec[T])

Store values to base + index. Scalar fallback: generic memory stores are unavailable -- no-op (documented). Complexity: O(1).

  • Precondition: true
fn gather_mask[T](base: Int, indices: &Vec[Int], m: Mask) -> Vec[T]

Gather only the lanes where the mask is set. Scalar fallback: generic memory loads are unavailable -- returns default T() values, one per set lane (documented). Complexity: O(32).

  • Postcondition: result.len() <= 32
  • Postcondition: result.len() == mask.mask_count(m)
fn gather_compress[T](values: &Vec[T], m: Mask) -> Vec[T]

Compact the set-lane values to the front. Fully implemented scalar fallback: the result holds values[i] for every set lane i, in lane order. Complexity: O(min(values, 32)).

  • Postcondition: result.len() <= values.len()
  • Postcondition: result.len() <= 32
fn gather_expand[T](values: &Vec[T], m: Mask) -> Vec[T]

Spread values back into set-lane positions. Fully implemented scalar fallback: the result has 32 lanes; lane i holds the next value from values when the mask bit is set and a default T() otherwise. Complexity: O(32).

  • Postcondition: result.len() == 32
fn gather_iota[T](base: Int, n: Int) -> Vec[T]

Materialize the values base + 0 .. base + n-1. Scalar fallback: generic construction from an Int is unavailable -- returns default T() values, one per element (documented). Complexity: O(n).

  • Postcondition: (n > 0) => (result.len() == n)
  • Postcondition: (n <= 0) => (result.len() == 0)

mask.xi

type Mask

A SIMD comparison mask holding one bit per lane (32 lanes in the scalar fallback).

Field Type
bits Int

Derives: Clone

fn mask_new(bits: Int) -> Mask

Build a mask from an integer bit pattern. Complexity: O(1).

  • Postcondition: result.bits == bits
fn mask_get(m: Mask, i: Int) -> Bool

Read lane i of a mask (0..31). Out-of-range lanes read false. Complexity: O(1).

  • Postcondition: (i < 0 || i > 31) => (result == false)
fn mask_set(m: Mask, i: Int, on: Bool) -> Mask

Set lane i of a mask (on) and return the new mask. Complexity: O(1).

  • Postcondition: (i < 0 || i > 31) => (result.bits == m.bits)
  • Postcondition: (on == true && i >= 0 && i <= 31) => (result.bits == (m.bits | (1 << i)))
  • Postcondition: (on == false && i >= 0 && i <= 31) => (result.bits == (m.bits & (0 - 1 - (1 << i))))
fn mask_count(m: Mask) -> Int

The number of set lanes. Complexity: O(32).

  • Postcondition: result >= 0 && result <= 32
fn mask_all(m: Mask) -> Bool

Whether every lane is set. Complexity: O(32).

  • Postcondition: (m.bits == 4294967295) => (result == true)
fn mask_any(m: Mask) -> Bool

Whether any lane is set. Complexity: O(1).

  • Postcondition: (m.bits == 0) => (result == false)
  • Postcondition: (result == true) => (m.bits != 0)
fn mask_and(a: Mask, b: Mask) -> Mask

Lane-wise logical AND. Complexity: O(1).

  • Postcondition: result.bits == (a.bits & b.bits)
fn mask_or(a: Mask, b: Mask) -> Mask

Lane-wise logical OR. Complexity: O(1).

  • Postcondition: result.bits == (a.bits | b.bits)
fn mask_xor(a: Mask, b: Mask) -> Mask

Lane-wise logical XOR. Complexity: O(1).

  • Postcondition: result.bits == (a.bits ^ b.bits)
fn mask_not(m: Mask) -> Mask

Lane-wise logical NOT (32 lanes). Complexity: O(1).

  • Postcondition: (m.bits == 0) => (result.bits == 4294967295)
  • Postcondition: result.bits >= 0
fn mask_to_bits(m: Mask) -> Int

The integer bit pattern of a mask. Complexity: O(1).

  • Postcondition: result == m.bits
fn mask_from_bits(bits: Int) -> Mask

Build a mask from an integer bit pattern. Complexity: O(1).

  • Postcondition: result.bits == bits
fn mask_from_vec(v: &Vec[Bool]) -> Mask

Build a mask from a boolean vector (lane i = v[i]). Complexity: O(len(v)).

  • Postcondition: (v.len() == 0) => (result.bits == 0)
  • Postcondition: result.bits >= 0
fn mask_to_vec(m: Mask) -> Vec[Bool]

Expand a mask to a boolean vector of 32 lanes. Complexity: O(32).

  • Postcondition: result.len() == 32

simd.xi

type Vec4f

128-bit vectors (SSE / NEON)

Field Type
data *Float32

Invariants: - data != null

type Vec2d

128-bit vector of 2 f64 lanes.

Field Type
data *Float64

type Vec4i

128-bit vector of 4 i32 lanes.

Field Type
data *Int32

type Vec8s

128-bit vector of 8 i16 lanes.

Field Type
data *Int16

type Vec16b

128-bit vector of 16 i8 lanes.

Field Type
data *Int8

type Vec8f

256-bit vectors (AVX / AVX2)

Field Type
data *Float32

Invariants: - data != null

type Vec4d

256-bit vector of 4 f64 lanes (AVX).

Field Type
data *Float64

type Vec8i

256-bit vector of 8 i32 lanes (AVX).

Field Type
data *Int32

type Vec16f

512-bit vectors (AVX-512)

Field Type
data *Float32

type Vec8d

512-bit vector of 8 f64 lanes (AVX-512).

Field Type
data *Float64

fn simd_supported() -> Bool

True when the backend reports usable SIMD support.

  • Precondition: true

fn has_sse() -> Bool

True when SSE is available on this CPU.

  • Precondition: true

fn has_avx() -> Bool

True when AVX is available on this CPU.

  • Precondition: true

fn has_avx2() -> Bool

True when AVX2 is available on this CPU.

  • Precondition: true

fn has_avx512() -> Bool

True when AVX-512 is available on this CPU.

  • Precondition: true

fn has_neon() -> Bool

True when NEON is available on this CPU (ARM64).

  • Precondition: true

fn new(x: Float32, y: Float32, z: Float32, w: Float32) -> Vec4f

Vec4f Operations (4 x f32, SSE/NEON)

  • Postcondition: result.data != null

fn splat(value: Float32) -> Vec4f

Vector with all four lanes set to value.

  • Postcondition: result.data != null

fn zero() -> Vec4f

All-zero vector.

  • Postcondition: result.data != null

fn add(self: Self, other: Vec4f) -> Vec4f

Lane-wise addition.

  • Precondition: simd_supported()

fn sub(self: Self, other: Vec4f) -> Vec4f

Lane-wise subtraction.

  • Precondition: simd_supported()

fn mul(self: Self, other: Vec4f) -> Vec4f

Lane-wise multiplication.

  • Precondition: simd_supported()

fn div(self: Self, other: Vec4f) -> Vec4f

Lane-wise division.

  • Precondition: simd_supported()

fn sqrt(self: Self) -> Vec4f

Lane-wise square root.

  • Precondition: simd_supported()

fn dot(self: Self, other: Vec4f) -> Float32

Dot product of the two vectors.

  • Precondition: simd_supported()

fn get(self: Self, index: Int) -> Float32

Lane value at index (0..3).

  • Precondition: index >= 0 && index < 4

fn set(self: Self, index: Int, value: Float32)

Write value to lane index (0..3).

  • Precondition: index >= 0 && index < 4

fn len(self: Self) -> Float32

Euclidean length of the vector.

  • Precondition: simd_supported()
  • Postcondition: result >= 0

fn normalize(self: Self) -> Vec4f

Unit vector in the same direction (a zero vector stays zero).

  • Precondition: simd_supported()
  • Postcondition: result.data != null

fn cross3(self: Self, other: Vec4f) -> Vec4f

Cross product using the first three lanes.

  • Postcondition: result.data != null

fn drop(self: Self)

Free the underlying lane storage.

  • Precondition: true

fn add_scalar(self: Self, other: Vec4f) -> Vec4f

Scalar fallback when SIMD unavailable Add the scalar in lane 0 to every lane.

  • Postcondition: result.data != null

fn mul_scalar(self: Self, other: Vec4f) -> Vec4f

Multiply every lane by the scalar in lane 0.

  • Postcondition: result.data != null

fn new(v0: Float32, v1: Float32, v2: Float32, v3: Float32, v4: Float32, v5: Float32, v6: Float32, v7: Float32) -> Vec8f

Vec8f Operations (8 x f32, AVX) Build an 8-lane vector from eight lane values.

  • Postcondition: result.data != null

fn add(self: Self, other: Vec8f) -> Vec8f

Lane-wise addition (AVX).

  • Precondition: has_avx()

fn mul(self: Self, other: Vec8f) -> Vec8f

Lane-wise multiplication (AVX).

  • Precondition: has_avx()

vec4.xi

type F32x4

A 4-lane single-precision SIMD vector.

Field Type
a Float32
b Float32
c Float32
d Float32

Derives: Clone

type I32x4

A 4-lane 32-bit integer SIMD vector.

Field Type
a Int
b Int
c Int
d Int

Derives: Clone

fn f32x4_new(a: Float32, b: Float32, c: Float32, d: Float32) -> F32x4

Build a vector from four lanes. Complexity: O(1).

  • Postcondition: result.a == a && result.b == b && result.c == c && result.d == d
fn f32x4_add(x: F32x4, y: F32x4) -> F32x4

Lane-wise addition. Complexity: O(1).

  • Postcondition: result.a == x.a + y.a && result.b == x.b + y.b && result.c == x.c + y.c && result.d == x.d + y.d
fn f32x4_sub(x: F32x4, y: F32x4) -> F32x4

Lane-wise subtraction. Complexity: O(1).

  • Postcondition: result.a == x.a - y.a && result.b == x.b - y.b && result.c == x.c - y.c && result.d == x.d - y.d
fn f32x4_mul(x: F32x4, y: F32x4) -> F32x4

Lane-wise multiplication. Complexity: O(1).

  • Postcondition: result.a == x.a * y.a && result.b == x.b * y.b && result.c == x.c * y.c && result.d == x.d * y.d
fn f32x4_div(x: F32x4, y: F32x4) -> F32x4

Lane-wise division. Complexity: O(1).

  • Postcondition: result.a == x.a / y.a && result.b == x.b / y.b && result.c == x.c / y.c && result.d == x.d / y.d
fn f32x4_sqrt(x: F32x4) -> F32x4

Lane-wise square root. Complexity: O(1).

  • Precondition: true
fn f32x4_min(x: F32x4, y: F32x4) -> F32x4

Lane-wise minimum. Complexity: O(1).

  • Postcondition: (result.a == x.a || result.a == y.a) && (result.b == x.b || result.b == y.b) && (result.c == x.c || result.c == y.c) && (result.d == x.d || result.d == y.d)
fn f32x4_max(x: F32x4, y: F32x4) -> F32x4

Lane-wise maximum. Complexity: O(1).

  • Postcondition: (result.a == x.a || result.a == y.a) && (result.b == x.b || result.b == y.b) && (result.c == x.c || result.c == y.c) && (result.d == x.d || result.d == y.d)
fn f32x4_dot(x: F32x4, y: F32x4) -> Float32

The dot product of two vectors. Complexity: O(1).

  • Postcondition: result == x.a * y.a + x.b * y.b + x.c * y.c + x.d * y.d
fn f32x4_load(ptr: Int) -> F32x4

Load a vector from aligned memory (16 bytes, four Float32 values). Complexity: O(1).

  • Precondition: ptr != 0
fn f32x4_store(ptr: Int, x: F32x4)

Store a vector to aligned memory (16 bytes). Complexity: O(1).

  • Precondition: ptr != 0
fn f32x4_splat(v: Float32) -> F32x4

Fill every lane with v. Complexity: O(1).

  • Postcondition: result.a == v && result.b == v && result.c == v && result.d == v
fn f32x4_extract(x: F32x4, i: Int) -> Float32

Read lane i (0..3). Complexity: O(1).

  • Postcondition: (i <= 0) => (result == x.a)
  • Postcondition: (i == 1) => (result == x.b)
  • Postcondition: (i == 2) => (result == x.c)
  • Postcondition: (i >= 3) => (result == x.d)
fn f32x4_insert(x: F32x4, i: Int, v: Float32) -> F32x4

Write lane i and return the vector. Complexity: O(1).

  • Postcondition: (i <= 0) => (result.a == v)
  • Postcondition: (i == 1) => (result.b == v)
  • Postcondition: (i == 2) => (result.c == v)
  • Postcondition: (i >= 3) => (result.d == v)
fn f32x4_sum(x: F32x4) -> Float32

The sum of all lanes. Complexity: O(1).

  • Postcondition: result == x.a + x.b + x.c + x.d
fn i32x4_new(a: Int, b: Int, c: Int, d: Int) -> I32x4

Build a vector from four integer lanes. Complexity: O(1).

  • Postcondition: result.a == a && result.b == b && result.c == c && result.d == d
fn i32x4_add(x: I32x4, y: I32x4) -> I32x4

Lane-wise addition. Complexity: O(1).

  • Postcondition: result.a == x.a + y.a && result.b == x.b + y.b && result.c == x.c + y.c && result.d == x.d + y.d
fn i32x4_sub(x: I32x4, y: I32x4) -> I32x4

Lane-wise subtraction. Complexity: O(1).

  • Postcondition: result.a == x.a - y.a && result.b == x.b - y.b && result.c == x.c - y.c && result.d == x.d - y.d
fn i32x4_mul(x: I32x4, y: I32x4) -> I32x4

Lane-wise multiplication. Complexity: O(1).

  • Postcondition: result.a == x.a * y.a && result.b == x.b * y.b && result.c == x.c * y.c && result.d == x.d * y.d
fn i32x4_min(x: I32x4, y: I32x4) -> I32x4

Lane-wise minimum. Complexity: O(1).

  • Postcondition: (result.a == x.a || result.a == y.a) && (result.b == x.b || result.b == y.b) && (result.c == x.c || result.c == y.c) && (result.d == x.d || result.d == y.d)
fn i32x4_max(x: I32x4, y: I32x4) -> I32x4

Lane-wise maximum. Complexity: O(1).

  • Postcondition: (result.a == x.a || result.a == y.a) && (result.b == x.b || result.b == y.b) && (result.c == x.c || result.c == y.c) && (result.d == x.d || result.d == y.d)
fn i32x4_splat(v: Int) -> I32x4

Fill every lane with v. Complexity: O(1).

  • Postcondition: result.a == v && result.b == v && result.c == v && result.d == v
fn i32x4_extract(x: I32x4, i: Int) -> Int

Read lane i (0..3). Complexity: O(1).

  • Postcondition: (i <= 0) => (result == x.a)
  • Postcondition: (i == 1) => (result == x.b)
  • Postcondition: (i == 2) => (result == x.c)
  • Postcondition: (i >= 3) => (result == x.d)

vec8.xi

type F32x8

An 8-lane single-precision SIMD vector.

Field Type
a0 Float32
a1 Float32
a2 Float32
a3 Float32
a4 Float32
a5 Float32
a6 Float32
a7 Float32

Derives: Clone

type I32x8

An 8-lane 32-bit integer SIMD vector.

Field Type
a0 Int
a1 Int
a2 Int
a3 Int
a4 Int
a5 Int
a6 Int
a7 Int

Derives: Clone

fn f32x8_new(v: [N]Float32) -> F32x8

Build a vector from a fixed 8-element array. Complexity: O(1).

  • Postcondition: result.a0 == v[0] && result.a1 == v[1] && result.a2 == v[2] && result.a3 == v[3] && result.a4 == v[4] && result.a5 == v[5] && result.a6 == v[6] && result.a7 == v[7]
fn f32x8_add(x: F32x8, y: F32x8) -> F32x8

Lane-wise addition. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 + y.a0 && result.a1 == x.a1 + y.a1 && result.a2 == x.a2 + y.a2 && result.a3 == x.a3 + y.a3 && result.a4 == x.a4 + y.a4 && result.a5 == x.a5 + y.a5 && result.a6 == x.a6 + y.a6 && result.a7 == x.a7 + y.a7
fn f32x8_sub(x: F32x8, y: F32x8) -> F32x8

Lane-wise subtraction. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 - y.a0 && result.a1 == x.a1 - y.a1 && result.a2 == x.a2 - y.a2 && result.a3 == x.a3 - y.a3 && result.a4 == x.a4 - y.a4 && result.a5 == x.a5 - y.a5 && result.a6 == x.a6 - y.a6 && result.a7 == x.a7 - y.a7
fn f32x8_mul(x: F32x8, y: F32x8) -> F32x8

Lane-wise multiplication. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 * y.a0 && result.a1 == x.a1 * y.a1 && result.a2 == x.a2 * y.a2 && result.a3 == x.a3 * y.a3 && result.a4 == x.a4 * y.a4 && result.a5 == x.a5 * y.a5 && result.a6 == x.a6 * y.a6 && result.a7 == x.a7 * y.a7
fn f32x8_div(x: F32x8, y: F32x8) -> F32x8

Lane-wise division. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 / y.a0 && result.a1 == x.a1 / y.a1 && result.a2 == x.a2 / y.a2 && result.a3 == x.a3 / y.a3 && result.a4 == x.a4 / y.a4 && result.a5 == x.a5 / y.a5 && result.a6 == x.a6 / y.a6 && result.a7 == x.a7 / y.a7
fn f32x8_sqrt(x: F32x8) -> F32x8

Lane-wise square root. Complexity: O(1).

  • Precondition: true
fn f32x8_min(x: F32x8, y: F32x8) -> F32x8

Lane-wise minimum. Complexity: O(1).

  • Postcondition: (result.a0 == x.a0 || result.a0 == y.a0) && (result.a1 == x.a1 || result.a1 == y.a1) && (result.a2 == x.a2 || result.a2 == y.a2) && (result.a3 == x.a3 || result.a3 == y.a3) && (result.a4 == x.a4 || result.a4 == y.a4) && (result.a5 == x.a5 || result.a5 == y.a5) && (result.a6 == x.a6 || result.a6 == y.a6) && (result.a7 == x.a7 || result.a7 == y.a7)
fn f32x8_max(x: F32x8, y: F32x8) -> F32x8

Lane-wise maximum. Complexity: O(1).

  • Postcondition: (result.a0 == x.a0 || result.a0 == y.a0) && (result.a1 == x.a1 || result.a1 == y.a1) && (result.a2 == x.a2 || result.a2 == y.a2) && (result.a3 == x.a3 || result.a3 == y.a3) && (result.a4 == x.a4 || result.a4 == y.a4) && (result.a5 == x.a5 || result.a5 == y.a5) && (result.a6 == x.a6 || result.a6 == y.a6) && (result.a7 == x.a7 || result.a7 == y.a7)
fn f32x8_splat(v: Float32) -> F32x8

Fill every lane with v. Complexity: O(1).

  • Postcondition: result.a0 == v && result.a1 == v && result.a2 == v && result.a3 == v && result.a4 == v && result.a5 == v && result.a6 == v && result.a7 == v
fn f32x8_extract(x: F32x8, i: Int) -> Float32

Read lane i (0..7). Complexity: O(1).

  • Postcondition: (i <= 0) => (result == x.a0)
  • Postcondition: (i == 1) => (result == x.a1)
  • Postcondition: (i == 2) => (result == x.a2)
  • Postcondition: (i == 3) => (result == x.a3)
  • Postcondition: (i == 4) => (result == x.a4)
  • Postcondition: (i == 5) => (result == x.a5)
  • Postcondition: (i == 6) => (result == x.a6)
  • Postcondition: (i >= 7) => (result == x.a7)
fn f32x8_insert(x: F32x8, i: Int, v: Float32) -> F32x8

Write lane i and return the vector. Complexity: O(1).

  • Postcondition: (i <= 0) => (result.a0 == v)
  • Postcondition: (i == 1) => (result.a1 == v)
  • Postcondition: (i == 2) => (result.a2 == v)
  • Postcondition: (i == 3) => (result.a3 == v)
  • Postcondition: (i == 4) => (result.a4 == v)
  • Postcondition: (i == 5) => (result.a5 == v)
  • Postcondition: (i == 6) => (result.a6 == v)
  • Postcondition: (i >= 7) => (result.a7 == v)
fn f32x8_sum(x: F32x8) -> Float32

The sum of all lanes. Complexity: O(1).

  • Postcondition: result == x.a0 + x.a1 + x.a2 + x.a3 + x.a4 + x.a5 + x.a6 + x.a7
fn f32x8_load(ptr: Int) -> F32x8

Load a vector from aligned memory (32 bytes, eight Float32 values). Complexity: O(1).

  • Precondition: ptr != 0
fn f32x8_store(ptr: Int, x: F32x8)

Store a vector to aligned memory (32 bytes). Complexity: O(1).

  • Precondition: ptr != 0
fn i32x8_new(v: [N]Int) -> I32x8

Build a vector from a fixed 8-element integer array. Complexity: O(1).

  • Postcondition: result.a0 == v[0] && result.a1 == v[1] && result.a2 == v[2] && result.a3 == v[3] && result.a4 == v[4] && result.a5 == v[5] && result.a6 == v[6] && result.a7 == v[7]
fn i32x8_add(x: I32x8, y: I32x8) -> I32x8

Lane-wise addition. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 + y.a0 && result.a1 == x.a1 + y.a1 && result.a2 == x.a2 + y.a2 && result.a3 == x.a3 + y.a3 && result.a4 == x.a4 + y.a4 && result.a5 == x.a5 + y.a5 && result.a6 == x.a6 + y.a6 && result.a7 == x.a7 + y.a7
fn i32x8_sub(x: I32x8, y: I32x8) -> I32x8

Lane-wise subtraction. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 - y.a0 && result.a1 == x.a1 - y.a1 && result.a2 == x.a2 - y.a2 && result.a3 == x.a3 - y.a3 && result.a4 == x.a4 - y.a4 && result.a5 == x.a5 - y.a5 && result.a6 == x.a6 - y.a6 && result.a7 == x.a7 - y.a7
fn i32x8_mul(x: I32x8, y: I32x8) -> I32x8

Lane-wise multiplication. Complexity: O(1).

  • Postcondition: result.a0 == x.a0 * y.a0 && result.a1 == x.a1 * y.a1 && result.a2 == x.a2 * y.a2 && result.a3 == x.a3 * y.a3 && result.a4 == x.a4 * y.a4 && result.a5 == x.a5 * y.a5 && result.a6 == x.a6 * y.a6 && result.a7 == x.a7 * y.a7
fn i32x8_splat(v: Int) -> I32x8

Fill every lane with v. Complexity: O(1).

  • Postcondition: result.a0 == v && result.a1 == v && result.a2 == v && result.a3 == v && result.a4 == v && result.a5 == v && result.a6 == v && result.a7 == v
fn i32x8_extract(x: I32x8, i: Int) -> Int

Read lane i (0..7). Complexity: O(1).

  • Postcondition: (i <= 0) => (result == x.a0)
  • Postcondition: (i == 1) => (result == x.a1)
  • Postcondition: (i == 2) => (result == x.a2)
  • Postcondition: (i == 3) => (result == x.a3)
  • Postcondition: (i == 4) => (result == x.a4)
  • Postcondition: (i == 5) => (result == x.a5)
  • Postcondition: (i == 6) => (result == x.a6)
  • Postcondition: (i >= 7) => (result == x.a7)