Tensor

Dimension-indexed linear algebra: the numeric foundation for ``NN``. Design goals: * Tensor *shape* lives in the types. ``Vector`` and ``Matrix`` are opaque, numpy-backed handles whose dimensions are described by the uninterpreted measures ``dim`` / ``rows`` / ``cols``. The SMT solver reasons about these symbolically, so the classic shape bugs are rejected at compile time rather than blowing up at runtime: - ``vadd`` / ``vsub`` / ``hadamard`` require both operands to have the *same* length; ``dot`` likewise. - ``matmul`` requires the inner dimensions to agree (``rows b == cols a``) and stamps the product's shape (``rows a`` by ``cols b``). - ``matvec`` requires the vector's length to match the matrix's column count and yields a vector of length ``rows m``. - ``transpose`` swaps ``rows`` and ``cols`` at the type level. * "Other requirements on values" beyond shape are refinements too: constructors take non-negative / positive sizes, ``get`` indices are bounds-checked (``0 <= i < dim v``), and ``normalize`` demands a non-zero-length vector. * Runtime *witnesses* (``vdim``, ``mrows``, ``mcols``) refine their ``Int`` result back to the measure, so a length read at runtime can discharge a static dimension precondition. ─── Opaque, numpy-backed tensor handles ─────────────────────────────── A 1-D tensor (numpy 1-D float array).
Imports
open Math; open List;
Table of Contents

Types

Vector

(type)
A 1-D tensor (numpy 1-D float array).
type Vector

Matrix

(type)
A 2-D tensor (numpy 2-D float array).
type Matrix

Functions

np

Side-effecting import; ``np`` is then in scope for every native body.
def np : Unit

vzeros

All-zeros vector of the requested length; every element is exactly 0.
def vzeros (n : Int | n ≥ 0) : {v : Vector | dim v = n && (lower v = 0.0 && upper v = 0.0)}

vones

All-ones vector of the requested length; every element is exactly 1.
def vones (n : Int | n ≥ 0) : {v : Vector | dim v = n && (lower v = 1.0 && upper v = 1.0)}

vfull

Constant vector: ``n`` copies of ``x`` — so the element interval is exactly ``[x, x]``.
def vfull (n : Int | n ≥ 0) (x : Float) : {v : Vector | dim v = n && (lower v = x && upper v = x)}

from_list

Build a vector from an Aeon ``List`` of floats. The vector's length is tied to the list's ``size`` measure, so a statically-known list length carries through to ``dim``.
def from_list (xs : List Float) : {v : Vector | dim v = size xs}

vdim

Length of a vector, refined back to the ``dim`` measure so it can discharge a static dimension obligation.
def vdim (v : Vector) : {n : Int | n = dim v && n ≥ 0}

vget

Bounds-checked indexed read. The element is known to lie in the vector's value interval ``[lower v, upper v]`` — so reading a ``relu`` output gives a ``{x | x >= 0.0}`` directly.
def vget (v : Vector) (i : Int | i ≥ 0 && i < dim v) : {x : Float | lower v ≤ x && x ≤ upper v}

vlower

Runtime witnesses for the value bounds (require a non-empty vector).
def vlower (v : Vector | dim v > 0) : {f : Float | f = lower v}

vupper

def vupper (v : Vector | dim v > 0) : {f : Float | f = upper v}

vadd

Element-wise sum. Interval: ``[la + lb, ua + ub]``.
def vadd (a : Vector) (b : Vector | dim b = dim a) : {r : Vector | dim r = dim a && (lower r ≥ lower a + lower b && upper r ≤ upper a + upper b)}

vsub

Element-wise difference. Interval: ``[la - ub, ua - lb]``.
def vsub (a : Vector) (b : Vector | dim b = dim a) : {r : Vector | dim r = dim a && (lower r ≥ lower a - upper b && upper r ≤ upper a - lower b)}

hadamard

Element-wise (Hadamard) product. General signs make the product interval sign-dependent (not simply expressible), so the unrestricted version propagates only the shape; use ``hadamard_nonneg`` when both operands are known non-negative.
def hadamard (a : Vector) (b : Vector | dim b = dim a) : {r : Vector | dim r = dim a}

hadamard_nonneg

Hadamard product of two non-negative vectors. With ``la, lb >= 0`` the product is monotone in both factors, so the interval is ``[la*lb, ua*ub]`` and the result stays non-negative.
def hadamard_nonneg (a : Vector | lower a ≥ 0.0) (b : Vector | dim b = dim a && lower b ≥ 0.0) : {r : Vector | dim r = dim a && (lower r ≥ lower a * lower b && upper r ≤ upper a * upper b)}

scale

Scalar multiple; preserves length. Sign of ``s`` makes the scaled interval sign-dependent, so the unrestricted version keeps only the shape; use ``scale_nonneg`` for a non-negative factor.
def scale (s : Float) (v : Vector) : {r : Vector | dim r = dim v}

scale_nonneg

Scale by a non-negative factor: the interval is just ``[s*lv, s*uv]``.
def scale_nonneg (s : Float | s ≥ 0.0) (v : Vector) : {r : Vector | dim r = dim v && (lower r ≥ s * lower v && upper r ≤ s * upper v)}

dot

Inner product; both operands must share a length.
def dot (a : Vector) (b : Vector | dim b = dim a) : Float

dot_nonneg

Inner product of two non-negative vectors is non-negative.
def dot_nonneg (a : Vector | lower a ≥ 0.0) (b : Vector | dim b = dim a && lower b ≥ 0.0) : {f : Float | f ≥ 0.0}

norm

Euclidean (L2) norm; always non-negative.
def norm (v : Vector) : {f : Float | f ≥ 0.0}

normalize

Unit vector in the direction of ``v``; requires a non-empty vector so the norm is non-zero. Length is preserved.
def normalize (v : Vector | dim v > 0) : {r : Vector | dim r = dim v}

vsum

Sum of all entries.
def vsum (v : Vector) : Float

mzeros

Zero matrix of the requested shape; every entry is exactly 0.
def mzeros (r : Int | r ≥ 0) (c : Int | c ≥ 0) : {m : Matrix | rows m = r && (cols m = c && (mlower m = 0.0 && mupper m = 0.0))}

eye

``n`` by ``n`` identity matrix; every entry lies in ``[0, 1]``.
def eye (n : Int | n ≥ 0) : {m : Matrix | rows m = n && (cols m = n && (mlower m ≥ 0.0 && mupper m ≤ 1.0))}

mrows

def mrows (m : Matrix) : {n : Int | n = rows m && n ≥ 0}

mcols

def mcols (m : Matrix) : {n : Int | n = cols m && n ≥ 0}

mget

Bounds-checked element read; the entry lies in ``[mlower m, mupper m]``.
def mget (m : Matrix) (i : Int | i ≥ 0 && i < rows m) (j : Int | j ≥ 0 && j < cols m) : {x : Float | mlower m ≤ x && x ≤ mupper m}

mlower_of

Runtime witnesses for the matrix value bounds (require a non-empty matrix).
def mlower_of (m : Matrix | rows m > 0 && cols m > 0) : {f : Float | f = mlower m}

mupper_of

def mupper_of (m : Matrix | rows m > 0 && cols m > 0) : {f : Float | f = mupper m}

madd

Element-wise sum; both operands must share a shape, which the result inherits. Value interval: ``[la + lb, ua + ub]``.
def madd (a : Matrix) (b : Matrix | rows b = rows a && cols b = cols a) : { r : Matrix | rows r = rows a && (cols r = cols a && (mlower r ≥ mlower a + mlower b && mupper r ≤ mupper a + mupper b)) }

matmul

Matrix product. The inner dimensions must agree (``rows b == cols a``) and the product's shape is ``rows a`` by ``cols b``.
def matmul (a : Matrix) (b : Matrix | rows b = cols a) : {r : Matrix | rows r = rows a && cols r = cols b}

matvec

Matrix-vector product. The vector length must match the column count; the result has length ``rows m``.
def matvec (m : Matrix) (v : Vector | dim v = cols m) : {r : Vector | dim r = rows m}

transpose

Transpose swaps the two dimensions; the entries are unchanged, so the value interval is preserved exactly.
def transpose (m : Matrix) : {r : Matrix | rows r = cols m && (cols r = rows m && (mlower r = mlower m && mupper r = mupper m))}

Uninterpreted

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

dim

uninterpreted
Length of a vector.
def dim : (v : Vector) → Int

rows

uninterpreted
Row / column counts of a matrix.
def rows : (m : Matrix) → Int

cols

uninterpreted
def cols : (m : Matrix) → Int

lower

uninterpreted
def lower : (v : Vector) → Float

upper

uninterpreted
def upper : (v : Vector) → Float

mlower

uninterpreted
def mlower : (m : Matrix) → Float

mupper

uninterpreted
def mupper : (m : Matrix) → Float