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; import ReadOnly;
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 (borrow arr : (NDArray a rank)) (axis : Int | axis ≥ 0 && axis < arr.ndim) : {n : Int | n = arr.dimension_size axis && n ≥ 0}

count

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

get1

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

take1

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

get2

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

take2

def take2 (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 (_inst4203 : (Copy a)) (borrow 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

take3

def take3 (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 (_inst4204 : (Copy a)) (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 (_inst4205 : (Copy a)) (borrow 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 (_inst4206 : (Copy a)) (1 arr : (NDArray a rank)) (f : (x : a) → Bool) : {r : (NDArray a Rank1) | r.elements ≤ arr.elements && r.dimension_size 0 = r.elements}

map

Elementwise operations consume their inputs and preserve their shape. Equal element types allow the runtime to reuse the first input's allocation.
def map (_inst4207 : (Copy a)) (1 arr : (NDArray a rank)) (f : (x : a) → b) : { r : (NDArray b 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 }

zipWith

def zipWith (_inst4208 : (Copy a)) (_inst4209 : (Copy b)) (1 arr : (NDArray a rank)) ( 1 other : (NDArray b rank) | r.dimension_size 0 = arr.dimension_size 0 && (arr.ndim < 2 || r.dimension_size 1 = arr.dimension_size 1) && (arr.ndim < 3 || r.dimension_size 2 = arr.dimension_size 2) ) (f : (x : a) → (y : b) → c) : { r : (NDArray c 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 }

reduce_axis

Keep the reduced dimension with size one, so the static rank is preserved.
def reduce_axis (_inst4210 : (Copy a)) (1 arr : (NDArray a rank)) (axis : Int | axis ≥ 0 && axis < arr.ndim) (f : (acc : a) → (x : a) → a) (z : a) : {r : (NDArray a rank) | r.ndim = arr.ndim && r.dimension_size axis = 1}

scan

Row-major prefix folds. The combiner must be pure and associative, as for reduce. z is applied exactly once per prefix; it need not be an identity.
def scan (_inst4211 : (Copy a)) (1 arr : (NDArray a rank)) (f : (acc : a) → (x : a) → a) (z : 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 }

scan_exclusive

def scan_exclusive (_inst4212 : (Copy a)) (1 arr : (NDArray a rank)) (f : (acc : a) → (x : a) → a) (z : 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 }

iterate

Host scheduling over two reusable buffers. Each destination starts filled with value. The callback must return that destination and preserve its shape.
def iterate (_inst4213 : (Copy a)) (1 arr : (NDArray a rank)) (steps : Int | steps ≥ 0 && steps ≤ 2147483647) (value : a) ( f : (step : Int | step ≥ 0 && step < steps) → (xs : (ReadOnly a) | ReadOnly.size xs = arr.elements) → ( 1 output : (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 ) → (NDArray a rank) ) : { 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 }

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