NDArray

Owned, contiguous arrays with a static rank and runtime shape. Rank markers are erased; every rank uses the same data/shape/stride descriptor.
Imports
import Array;
Table of Contents

Types

Rank1

(type)
type Rank1

Rank2

(type)
type Rank2

Rank3

(type)
type Rank3

NDArray

(type) linear
linear type NDArray a rank

Functions

full1

def full1 (n : Int | n ≥ 0 && n ≤ 2147483647) (value : a) : {r : NDArray a Rank1 | r.ndim = 1 && (r.elements = n && r.dimension_size 0 = n)}

full2

def full2 (rows : Int | rows ≥ 0 && rows ≤ 2147483647) (cols : Int | cols ≥ 0 && (cols ≤ 2147483647 && rows * cols ≤ 2147483647)) (value : a) : { r : NDArray a Rank2 | r.ndim = 2 && (r.elements = rows * cols && (r.dimension_size 0 = rows && r.dimension_size 1 = cols)) }

full3

def full3 (depth : Int | depth ≥ 0 && depth ≤ 2147483647) (rows : Int | rows ≥ 0 && rows ≤ 2147483647) (cols : Int | cols ≥ 0 && (cols ≤ 2147483647 && depth * rows * cols ≤ 2147483647)) (value : a) : { r : NDArray a Rank3 | r.ndim = 3 && ( r.elements = depth * rows * cols && (r.dimension_size 0 = depth && (r.dimension_size 1 = rows && r.dimension_size 2 = cols)) ) }

from_array

Bridge to the existing linear Array library without copying element storage.
def from_array (1 arr : Array a) : {r : NDArray a Rank1 | r.ndim = 1 && (r.elements = arr.size && r.dimension_size 0 = arr.size)}

to_array

def to_array (1 arr : NDArray a Rank1) : {r : Array a | r.size = arr.elements}

to_1d

Reshape transfers ownership. The element order and count are preserved.
def to_1d (1 arr : NDArray a rank) : {r : NDArray a Rank1 | r.ndim = 1 && (r.elements = arr.elements && r.dimension_size 0 = arr.elements)}

from_1d2

def from_1d2 (1 arr : NDArray a Rank1) (rows : Int | rows ≥ 0 && rows ≤ 2147483647) (cols : Int | cols ≥ 0 && (cols ≤ 2147483647 && rows * cols = arr.elements)) : { r : NDArray a Rank2 | r.ndim = 2 && (r.elements = arr.elements && (r.dimension_size 0 = rows && r.dimension_size 1 = cols)) }

from_1d3

def from_1d3 (1 arr : NDArray a Rank1) (depth : Int | depth ≥ 0 && depth ≤ 2147483647) (rows : Int | rows ≥ 0 && rows ≤ 2147483647) (cols : Int | cols ≥ 0 && (cols ≤ 2147483647 && depth * rows * cols = arr.elements)) : { r : NDArray a Rank3 | r.ndim = 3 && (r.elements = arr.elements && (r.dimension_size 0 = depth && (r.dimension_size 1 = rows && r.dimension_size 2 = cols))) }

dimension

def dimension (1 arr : NDArray a rank) (axis : Int | axis ≥ 0 && axis < arr.ndim) : {n : Int | n = arr.dimension_size axis && n ≥ 0}

count

def count (1 arr : NDArray a rank) : {n : Int | n = arr.elements && n ≥ 0}

get1

def get1 (1 arr : NDArray a Rank1) (i : Int | i ≥ 0 && i < arr.dimension_size 0) : a

get2

def get2 (1 arr : NDArray a Rank2) (row : Int | row ≥ 0 && row < arr.dimension_size 0) (col : Int | col ≥ 0 && col < arr.dimension_size 1) : a

get3

def get3 (1 arr : NDArray a Rank3) (depth : Int | depth ≥ 0 && depth < arr.dimension_size 0) (row : Int | row ≥ 0 && row < arr.dimension_size 1) (col : Int | col ≥ 0 && col < arr.dimension_size 2) : a

set1

def set1 (1 arr : NDArray a Rank1) (i : Int | i ≥ 0 && i < arr.dimension_size 0) (value : a) : {r : NDArray a Rank1 | r.ndim = arr.ndim && (r.elements = arr.elements && r.dimension_size 0 = arr.dimension_size 0)}

set2

def set2 (1 arr : NDArray a Rank2) (row : Int | row ≥ 0 && row < arr.dimension_size 0) (col : Int | col ≥ 0 && col < arr.dimension_size 1) (value : a) : { r : NDArray a Rank2 | r.ndim = arr.ndim && (r.elements = arr.elements && (r.dimension_size 0 = arr.dimension_size 0 && r.dimension_size 1 = arr.dimension_size 1)) }

set3

def set3 (1 arr : NDArray a Rank3) (depth : Int | depth ≥ 0 && depth < arr.dimension_size 0) (row : Int | row ≥ 0 && row < arr.dimension_size 1) (col : Int | col ≥ 0 && col < arr.dimension_size 2) (value : a) : { r : NDArray a Rank3 | r.ndim = arr.ndim && ( r.elements = arr.elements && ( r.dimension_size 0 = arr.dimension_size 0 && (r.dimension_size 1 = arr.dimension_size 1 && r.dimension_size 2 = arr.dimension_size 2) ) ) }

fill

def fill (1 arr : NDArray a rank) (value : a) : { r : NDArray a rank | r.ndim = arr.ndim && ( r.elements = arr.elements && ( r.dimension_size 0 = arr.dimension_size 0 && (r.dimension_size 1 = arr.dimension_size 1 && r.dimension_size 2 = arr.dimension_size 2) ) ) }

map_rows

Each callback owns one disjoint row. A direct @gpu entry launches one thread per row.
def map_rows (1 arr : NDArray a Rank2) ( f : (i : Int | i ≥ 0 && i < arr.dimension_size 0) → ( 1 row : NDArray a Rank1 | r.ndim = 1 && (r.elements = arr.dimension_size 1 && r.dimension_size 0 = arr.dimension_size 1) ) → {r : NDArray a Rank1 | r.dimension_size 0 = arr.dimension_size 1} ) : { r : NDArray a Rank2 | r.ndim = arr.ndim && (r.elements = arr.elements && (r.dimension_size 0 = arr.dimension_size 0 && r.dimension_size 1 = arr.dimension_size 1)) }

discard

def discard (1 arr : NDArray a rank) : Unit

reduce

An associative scalar combiner, compiled through the shared vector reduction. CUDA uses a parallel tree; z is applied once. Empty arrays return z.
def reduce (1 arr : NDArray a rank) (f : (acc : a) → (x : a) → a) (z : a) : a

filter

Stable row-major selection; the result is a packed one-dimensional array.
def filter (1 arr : NDArray a rank) (f : (x : a) → Bool) : {r : NDArray a Rank1 | r.elements ≤ arr.elements && r.dimension_size 0 = r.elements}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

ndim

uninterpreted
def ndim : (arr : NDArray a rank) → Int

elements

uninterpreted
def elements : (arr : NDArray a rank) → Int

dimension_size

uninterpreted
def dimension_size : (arr : NDArray a rank) → (axis : Int) → Int