~/bend-docscommunity

main.bend checks

raw source on the hub · import bend-ml-tensor-array@0.1.7.0/main.bend as Main

bend-ml-tensor-array: tensors over a flat Array<F32>, with the shape in the type.

import bend-ml-tensor-array@0.1.7.0/main.bend as TA

Mat<r, c> stores r*c numbers in an Array<F32>, row by row (index i*c + j). The dimensions are erased type parameters: the same guarantee as bend-ml-tensor (a product with wrong dimensions does not compile), but ~50x faster than lists: Array.get/set by index, and products in parallel blocks of rows.

An Array is affine (a single owner): every operation that reads an operand returns it together with the result (as Array.get does), in records MM, AR, ... Use Mat.clone when you need two copies.

What is NOT proved: the invariant "the Array has capacity >= r*c" holds because the constructors (Mat.zeros, Mat.of_list) allocate the right size; and F32 is validated by tests against PyTorch (reference/test_tensor_array.py), not by proof.

1 import
import Base

Laws

law cap_ok provedsource · line 559 · raw

@+n:Nat -> {True{} == leb(n, pow2(cap_depth(n))) : Bool}

LAW (cap_ok): an Array with 2^cap_depth(n) slots always has room for n elements.

law half_cover provedsource · line 970 · raw

@+n:Nat -> {n == Nat.add(half(n), Nat.sub(n, half(n))) : Nat}

LAW (half_cover): the two bands of a node, half(r) rows and r - half(r) rows, add up to exactly r rows: no row is lost and none is counted twice.

law leaf_len provedsource · line 1224 · raw

@-r:Nat -> @-c:Nat -> @w:Array<F32> -> @+mleft:Nat -> @+idx:U32 -> @+acc:List<&2, F32> -> @rc:Pair(Array<F32>, F32) -> {bl_len(r, c, bv_g2(r, c, w, read_l(mleft, idx, acc, rc))) == Nat.add(1n+mleft, List.length(&2, F32, acc)) : Nat}

a leaf's list: read_l reads mleft + 1 numbers onto acc and reverses them. By induction on mleft: with 0 left it reads one number (rev_len counts the reversed list); with 1 + p left it reads one and recurses, and len_step moves the 1 out of the sum.

law band_len provedsource · line 1250 · raw

@-r:Nat -> @+c:Nat -> @+rows:Nat -> @x:Array<F32> -> @w:Array<F32> -> {bl_len(r, c, bv_gemm(r, c, rows, rows, x, w)) == rows : Nat}

LAW (band_len): the product of one band with rows rows gives exactly rows numbers. 0 rows give the empty list; 1 + p rows go through the gemm, and g_len counts what is read back.

Types

type R source · line 24 · raw

Type

type G source · line 27 · raw

Type

type S3 source · line 72 · raw

Type

type P2 source · line 179 · raw

Type

type AL source · line 182 · raw

Type

type L2 source · line 321 · raw

Type

type Mat source · line 334 · raw

@-r:Nat -> @-c:Nat -> Type

type CR source · line 346 · raw

Type

type ML source · line 617 · raw

@-r:Nat -> @-c:Nat -> Type

type MM2 source · line 632 · raw

@-r:Nat -> @-c:Nat -> Type

type MMul source · line 649 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> Type

type MMulNT source · line 654 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> Type

type MMulTN source · line 659 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> Type

type MBias source · line 728 · raw

@-n:Nat -> @-m:Nat -> Type

type MPair source · line 743 · raw

@-r:Nat -> @-c:Nat -> Type

type MColSum source · line 782 · raw

@-n:Nat -> @-m:Nat -> Type

type MCE source · line 798 · raw

@-n:Nat -> @-c:Nat -> Type

type MHits source · line 813 · raw

@-n:Nat -> @-c:Nat -> Type

type MRow source · line 828 · raw

@-r:Nat -> @-c:Nat -> Type

type Bands source · line 977 · raw

@-r:Nat -> @-c:Nat -> Type

type BV source · line 1049 · raw

@-r:Nat -> @-c:Nat -> Type

B (intact) and y = B · x, typed like Mat.matmul_nt: x is 1 x c, y is 1 x r

type BL source · line 1053 · raw

@-r:Nat -> @-c:Nat -> Type

the bands and y as a list in row order (the result of Bands.matvec_l)

type BRow source · line 1118 · raw

@-r:Nat -> @-c:Nat -> Type

Definitions

def dotr source · line 35 · raw

@k:Nat -> @+ia:U32 -> @+ib:U32 -> @+sa:U32 -> @+sb:U32 -> @a0:F32 -> @a1:F32 -> @a2:F32 -> @a3:F32 -> @ra:Pair(Array<F32>, F32) -> @rb:Pair(Array<F32>, F32) -> R

A dot product with four partial sums. Each step adds its product to a0 and rotates the sums (a1, a2, a3, a0), so each sum gets every fourth product and the processor can work on the next addition before the last one has finished; at the end the sums are added in pairs. The order of the additions is fixed, so the result is the same on every run and every thread count, but it is not the order of a single running sum (NOTES.md, exp. 17).

def dotg source · line 42 · raw

@k:Nat -> @+ia:U32 -> @+ib:U32 -> @+sa:U32 -> @+sb:U32 -> @acc:F32 -> @ra:Pair(Array<F32>, F32) -> @rb:Pair(Array<F32>, F32) -> R

def gcols source · line 47 · raw

@mleft:Nat -> @+kn:Nat -> @+ia0:U32 -> @+ib0:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @+cidx:U32 -> @c:Array<F32> -> @r:R -> G

def grows source · line 54 · raw

@nleft:Nat -> @+mm1:Nat -> @+kn:Nat -> @+i:U32 -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @+mu:U32 -> @g:G -> G

def gemm source · line 63 · raw

@+n:Nat -> @+m:Nat -> @+k:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def lcols source · line 75 · raw

@mleft:Nat -> @+kn:Nat -> @+ia0:U32 -> @+ib0:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @out:List<&2, F32> -> @r:R -> S3

def lrows source · line 82 · raw

@nleft:Nat -> @+mm1:Nat -> @+kn:Nat -> @+i:U32 -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @st:S3 -> S3

def lblock_fin source · line 89 · raw

@st:S3 -> List<&2, F32>

def lblock source · line 94 · raw

@cnt:Nat -> @+mm1:Nat -> @+kn:Nat -> @+i:U32 -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> List<&2, F32>

def lpar source · line 97 · raw

@d:Nat -> @+cnt:Nat -> @+mm1:Nat -> @+kn:Nat -> @+i:U32 -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @ra:Pair(Array<F32>, Array<F32>) -> @rb:Pair(Array<F32>, Array<F32>) -> List<&2, F32>

def write_l source · line 105 · raw

@xs:List<&2, F32> -> @+idx:U32 -> @c:Array<F32> -> Array<F32>

def gp3 source · line 114 · raw

@a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> @xs:List<&2, F32> -> G

def gp2 source · line 117 · raw

@d:Nat -> @+n:Nat -> @+mm1:Nat -> @+kn:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @c:Array<F32> -> @pa:Pair(Array<F32>, Array<F32>) -> @pb:Pair(Array<F32>, Array<F32>) -> G

def gemm_par source · line 124 · raw

@d:Nat -> @+n:Nat -> @+m:Nat -> @+k:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def cblock_fin source · line 133 · raw

@st:S3 -> List<&2, F32>

def cblock_go source · line 140 · raw

@cnt1:Nat -> @+kn:Nat -> @+ia0:U32 -> @+j0:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> List<&2, F32>

def cblock source · line 143 · raw

@cnt:Nat -> @+kn:Nat -> @+ia0:U32 -> @+j0:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> List<&2, F32>

def cpar source · line 150 · raw

@d:Nat -> @+cnt:Nat -> @+kn:Nat -> @+ia0:U32 -> @+j0:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @ra:Pair(Array<F32>, Array<F32>) -> @rb:Pair(Array<F32>, Array<F32>) -> List<&2, F32>

def cp2 source · line 158 · raw

@d:Nat -> @+m:Nat -> @+kn:Nat -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @c:Array<F32> -> @pa:Pair(Array<F32>, Array<F32>) -> @pb:Pair(Array<F32>, Array<F32>) -> G

def gemm_par_cols source · line 165 · raw

@d:Nat -> @+m:Nat -> @+k:Nat -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def read_l source · line 187 · raw

@mleft:Nat -> @+idx:U32 -> @acc:List<&2, F32> -> @rc:Pair(Array<F32>, F32) -> AL

def addl source · line 196 · raw

@xs:List<&2, F32> -> @+idx:U32 -> @rc:Pair(Array<F32>, F32) -> Array<F32>

def bias_rows source · line 205 · raw

@nleft:Nat -> @+i:U32 -> @+mu:U32 -> @+bl:List<&2, F32> -> @c:Array<F32> -> Array<F32>

def relu_l source · line 214 · raw

@nleft:Nat -> @+t:U32 -> @rc:Pair(Array<F32>, F32) -> Array<F32>

def pos2 source · line 221 · raw

@b:Bool -> F32

def pos source · line 228 · raw

@+y:F32 -> F32

def mask_l source · line 233 · raw

@nleft:Nat -> @+t:U32 -> @rd:Pair(Array<F32>, F32) -> @rh:Pair(Array<F32>, F32) -> P2

def maxl2 source · line 242 · raw

@xs:List<&2, F32> -> @cur:F32 -> F32

def maxl source · line 249 · raw

@xs:List<&2, F32> -> F32

def expl source · line 256 · raw

@xs:List<&2, F32> -> @+m:F32 -> List<&2, F32>

def suml source · line 263 · raw

@xs:List<&2, F32> -> @acc:F32 -> F32

def divl source · line 270 · raw

@xs:List<&2, F32> -> @+s:F32 -> List<&2, F32>

def softmax2 source · line 277 · raw

@+es:List<&2, F32> -> List<&2, F32>

def softmax source · line 280 · raw

@+xs:List<&2, F32> -> List<&2, F32>

def sgd_l source · line 285 · raw

@nleft:Nat -> @+t:U32 -> @+lr:F32 -> @rw:Pair(Array<F32>, F32) -> @rd:Pair(Array<F32>, F32) -> P2

def pick source · line 296 · raw

@ps:List<&2, F32> -> @n:Nat -> F32

def hit source · line 307 · raw

@b:Bool -> F32

def grad_l source · line 314 · raw

@ps:List<&2, F32> -> @+label:Nat -> @+j:Nat -> @+nf:F32 -> List<&2, F32>

def ce_row2 source · line 324 · raw

@+ps:List<&2, F32> -> @+label:Nat -> @+nf:F32 -> @+idx:U32 -> @loss:F32 -> @c:Array<F32> -> L2

def ce_row source · line 327 · raw

@al:AL -> @+label:Nat -> @+nf:F32 -> @+idx:U32 -> @loss:F32 -> L2

def ce_rows source · line 337 · raw

@labels:List<&2, Nat> -> @+mm1:Nat -> @+mu:U32 -> @+nf:F32 -> @+i:U32 -> @r:L2 -> L2

def gt_head source · line 349 · raw

@xs:List<&2, F32> -> @+v:F32 -> Bool

def argmax2 source · line 356 · raw

@xs:List<&2, F32> -> @g:Bool -> @+i:Nat -> @+bi:Nat -> @+bv:F32 -> Nat

def argmax source · line 365 · raw

@xs:List<&2, F32> -> Nat

def one source · line 372 · raw

@b:Bool -> Nat

def count_rows3 source · line 379 · raw

@+y:Nat -> @n:Nat -> @al:AL -> CR

def count_rows source · line 384 · raw

@labels:List<&2, Nat> -> @+mm1:Nat -> @+mu:U32 -> @+i:U32 -> @r:CR -> CR

def BD source · line 405 · raw

@b:Bool -> @t:Type -> @f:Type -> Type

a type chosen by a Bool: rewriting through it refutes True == False

def leb source · line 413 · raw

@a:Nat -> @b:Nat -> Bool

a <= b, by direct recursion

def pow2 source · line 422 · raw

@d:Nat -> Nat

def cap_pick source · line 430 · raw

@ok:Bool -> @d:Nat -> @+p:Nat -> Pair(Nat, Nat)

smallest power of two >= n, by structural recursion on n: returns (depth, 2^depth)

def cap_step source · line 437 · raw

@r:Pair(Nat, Nat) -> @+n:Nat -> Pair(Nat, Nat)

def cap_pair source · line 442 · raw

@n:Nat -> Pair(Nat, Nat)

def fst_nat source · line 449 · raw

@r:Pair(Nat, Nat) -> Nat

def snd_nat source · line 454 · raw

@r:Pair(Nat, Nat) -> Nat

def cap_depth source · line 460 · raw

@n:Nat -> Nat

the depth d such that an Array with 2^d slots holds n elements

def leb_succ source · line 466 · raw

@a:Nat -> @b:Nat -> @e:{True{} == leb(a, b) : Bool} -> {True{} == leb(a, 1n+b) : Bool}

a <= b -> a <= 1 + b

def leb_up_l source · line 477 · raw

@+a:Nat -> @+b:Nat -> @c:Nat -> @+e:{True{} == leb(a, b) : Bool} -> {True{} == leb(a, Nat.add(c, b)) : Bool}

a <= b -> a <= c + b

def leb_up source · line 485 · raw

@a:Nat -> @b:Nat -> @c:Nat -> @e:{True{} == leb(a, b) : Bool} -> {True{} == leb(a, Nat.add(b, c)) : Bool}

a <= b -> a <= b + c

def leb_add source · line 496 · raw

@a:Nat -> @b:Nat -> @c:Nat -> @d:Nat -> @e1:{True{} == leb(a, b) : Bool} -> @e2:{True{} == leb(c, d) : Bool} -> {True{} == leb(Nat.add(a, c), Nat.add(b, d)) : Bool}

a <= b and c <= d -> a + c <= b + d

def pow2_pos source · line 507 · raw

@d:Nat -> {True{} == leb(1n, pow2(d)) : Bool}

1 <= 2^d

def pos_p source · line 515 · raw

@d:Nat -> @p:Nat -> @i1:{p == pow2(d) : Nat} -> {True{} == leb(1n, p) : Bool}

1 <= p when p = 2^d

def step_eq source · line 520 · raw

@d:Nat -> @p:Nat -> @i1:{p == pow2(d) : Nat} -> {Nat.add(p, p) == pow2(1n+d) : Nat}

p + p == 2^(1+d) when p == 2^d

def step_ok source · line 525 · raw

@ok:Bool -> @+d:Nat -> @+p:Nat -> @+m:Nat -> @+e:{ok == leb(1n+m, p) : Bool} -> @+i1:{p == pow2(d) : Nat} -> @+i2:{True{} == leb(m, p) : Bool} -> Pair({snd_nat(cap_pick(ok, d, p)) == pow2(fst_nat(cap_pick(ok, d, p))) : Nat}, {True{} == leb(1n+m, snd_nat(cap_pick(ok, d, p))) : Bool})

one step: given the invariant for m, the invariant for 1+m holds whichever way the comparison goes

def step_pair_ok source · line 534 · raw

@+m:Nat -> @r:Pair(Nat, Nat) -> @i1:{snd_nat(r) == pow2(fst_nat(r)) : Nat} -> @i2:{True{} == leb(m, snd_nat(r)) : Bool} -> Pair({snd_nat(cap_step(r, 1n+m)) == pow2(fst_nat(cap_step(r, 1n+m))) : Nat}, {True{} == leb(1n+m, snd_nat(cap_step(r, 1n+m))) : Bool})

the invariant for cap_step on a pair, opened

def cap_succ source · line 539 · raw

@+m:Nat -> @ih:Pair({snd_nat(cap_pair(m)) == pow2(fst_nat(cap_pair(m))) : Nat}, {True{} == leb(m, snd_nat(cap_pair(m))) : Bool}) -> Pair({snd_nat(cap_pair(1n+m)) == pow2(fst_nat(cap_pair(1n+m))) : Nat}, {True{} == leb(1n+m, snd_nat(cap_pair(1n+m))) : Bool})

def cap_inv source · line 545 · raw

@n:Nat -> Pair({snd_nat(cap_pair(n)) == pow2(fst_nat(cap_pair(n))) : Nat}, {True{} == leb(n, snd_nat(cap_pair(n))) : Bool})

the invariant of cap_pair: the second component is 2^(first) and is >= n

def cap_final source · line 552 · raw

@n:Nat -> @pr:Pair({snd_nat(cap_pair(n)) == pow2(fst_nat(cap_pair(n))) : Nat}, {True{} == leb(n, snd_nat(cap_pair(n))) : Bool}) -> {True{} == leb(n, pow2(cap_depth(n))) : Bool}

def Mat.zeros source · line 568 · raw

@+r:Nat -> @+c:Nat -> Mat<r, c>

def Mat.fill source · line 571 · raw

@+r:Nat -> @+c:Nat -> @+v:F32 -> Mat<r, c>

def fill_list source · line 574 · raw

@xs:List<&2, F32> -> @+i:U32 -> @a:Array<F32> -> Array<F32>

def len_is source · line 581 · raw

@xs:List<&2, F32> -> @n:Nat -> Bool

def Mat.of_list2 source · line 590 · raw

@-r:Nat -> @-c:Nat -> @+rr:Nat -> @+cc:Nat -> @ok:Bool -> @xs:List<&2, F32> -> Maybe<&1, Mat<r, c>>

def Mat.of_list source · line 599 · raw

@+r:Nat -> @+c:Nat -> @+xs:List<&2, F32> -> Maybe<&1, Mat<r, c>>

def Mat.from_list source · line 607 · raw

@+r:Nat -> @+c:Nat -> @xs:List<&2, F32> -> Mat<r, c>

def Mat.fill_at source · line 612 · raw

@-r:Nat -> @-c:Nat -> @+i:U32 -> @xs:List<&2, F32> -> @m:Mat<r, c> -> Mat<r, c>

writes the numbers of xs into m starting at flat index i (row-major); numbers past the capacity are dropped. For loading a large matrix block by block without building one big list.

def Mat.to_list2 source · line 620 · raw

@-r:Nat -> @-c:Nat -> @al:AL -> ML<r, c>

def Mat.to_list source · line 627 · raw

@+r:Nat -> @+c:Nat -> @m:Mat<r, c> -> ML<r, c>

def Mat.clone2 source · line 635 · raw

@-r:Nat -> @-c:Nat -> @p:Pair(Array<F32>, Array<F32>) -> MM2<r, c>

def Mat.clone source · line 644 · raw

@-r:Nat -> @-c:Nat -> @m:Mat<r, c> -> MM2<r, c>

def gemm_any3 source · line 662 · raw

@cols:Bool -> @d:Nat -> @+n:Nat -> @+m:Nat -> @+k:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def gemm_any2 source · line 669 · raw

@d:Nat -> @+n:Nat -> @+m:Nat -> @+k:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def gemm_any source · line 676 · raw

@d:Nat -> @+n:Nat -> @+m:Nat -> @+k:Nat -> @+arow:U32 -> @+sa:U32 -> @+sb:U32 -> @+bcol:U32 -> @a:Array<F32> -> @b:Array<F32> -> @c:Array<F32> -> G

def mmul_fin source · line 679 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> @g:G -> MMul<n, k, m>

def mmul_nt_fin source · line 684 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> @g:G -> MMulNT<n, k, m>

def mmul_tn_fin source · line 689 · raw

@-n:Nat -> @-k:Nat -> @-m:Nat -> @g:G -> MMulTN<n, k, m>

def mm_a source · line 694 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @d:Nat -> @a:Array<F32> -> @b:Array<F32> -> MMul<n, k, m>

def Mat.matmul source · line 699 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @par:Nat -> @a:Mat<n, k> -> @b:Mat<k, m> -> MMul<n, k, m>

def mm_nt source · line 704 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @d:Nat -> @a:Array<F32> -> @b:Array<F32> -> MMulNT<n, k, m>

def Mat.matmul_nt source · line 709 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @par:Nat -> @a:Mat<n, k> -> @b:Mat<m, k> -> MMulNT<n, k, m>

def mm_tn source · line 714 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @d:Nat -> @a:Array<F32> -> @b:Array<F32> -> MMulTN<n, k, m>

def Mat.matmul_tn source · line 719 · raw

@+n:Nat -> @+k:Nat -> @+m:Nat -> @par:Nat -> @a:Mat<k, n> -> @b:Mat<k, m> -> MMulTN<n, k, m>

def add_row2 source · line 731 · raw

@-n:Nat -> @-m:Nat -> @+nn:Nat -> @+mm:Nat -> @cd:Array<F32> -> @al:AL -> MBias<n, m>

def Mat.add_row source · line 736 · raw

@+n:Nat -> @+m:Nat -> @c:Mat<n, m> -> @b:Mat<1n, m> -> MBias<n, m>

def mpair_fin source · line 746 · raw

@-r:Nat -> @-c:Nat -> @p:P2 -> MPair<r, c>

def relu_fin source · line 751 · raw

@-r:Nat -> @-c:Nat -> @d:Array<F32> -> Mat<r, c>

def Mat.relu source · line 754 · raw

@+r:Nat -> @+c:Nat -> @a:Mat<r, c> -> Mat<r, c>

def Mat.relu_bwd source · line 761 · raw

@+r:Nat -> @+c:Nat -> @dy:Mat<r, c> -> @h:Mat<r, c> -> MPair<r, c>

def Mat.sgd source · line 768 · raw

@+r:Nat -> @+c:Nat -> @+lr:F32 -> @w:Mat<r, c> -> @dw:Mat<r, c> -> MPair<r, c>

def Mat.add source · line 775 · raw

@+r:Nat -> @+c:Nat -> @a:Mat<r, c> -> @b:Mat<r, c> -> MPair<r, c>

def colsum_fin source · line 785 · raw

@-n:Nat -> @-m:Nat -> @g:G -> MColSum<n, m>

def Mat.col_sums source · line 790 · raw

@+n:Nat -> @+m:Nat -> @a:Mat<n, m> -> MColSum<n, m>

def ce_fin source · line 801 · raw

@-n:Nat -> @-c:Nat -> @+nf:F32 -> @r:L2 -> MCE<n, c>

def Mat.softmax_ce source · line 806 · raw

@+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @labels:List<&2, Nat> -> MCE<n, c>

def hits_fin source · line 816 · raw

@-n:Nat -> @-c:Nat -> @r:CR -> MHits<n, c>

def Mat.count_correct source · line 821 · raw

@+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @labels:List<&2, Nat> -> MHits<n, c>

def row_fin source · line 831 · raw

@-r:Nat -> @-c:Nat -> @al:AL -> MRow<r, c>

def Mat.read_row source · line 836 · raw

@+r:Nat -> @+c:Nat -> @m:Mat<r, c> -> @+i:U32 -> MRow<r, c>

def Mat.write_row source · line 841 · raw

@-r:Nat -> @+c:Nat -> @m:Mat<r, c> -> @+i:U32 -> @xs:List<&2, F32> -> Mat<r, c>

def labels_len_is source · line 849 · raw

@xs:List<&2, Nat> -> @n:Nat -> Bool

does the list of labels have exactly n entries (one per row)?

def ce_checked source · line 858 · raw

@ok:Bool -> @+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @labels:List<&2, Nat> -> Maybe<&1, MCE<n, c>>

def Mat.softmax_ce_checked source · line 866 · raw

@+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @+labels:List<&2, Nat> -> Maybe<&1, MCE<n, c>>

like Mat.softmax_ce, but returns None unless labels has exactly n entries

def hits_checked source · line 869 · raw

@ok:Bool -> @+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @labels:List<&2, Nat> -> Maybe<&1, MHits<n, c>>

def Mat.count_correct_checked source · line 877 · raw

@+n:Nat -> @+c:Nat -> @z:Mat<n, c> -> @+labels:List<&2, Nat> -> Maybe<&1, MHits<n, c>>

like Mat.count_correct, but returns None unless labels has exactly n entries

def half.go source · line 896 · raw

@n:Nat -> @acc:Nat -> Nat

n / 2 rounded down. A tail loop with an accumulator: a non-tail recursion here would put a continuation on every node of the band tree and keep the bands from running in parallel.

def half source · line 907 · raw

@n:Nat -> Nat

def leb_refl source · line 911 · raw

@+a:Nat -> {True{} == leb(a, a) : Bool}

a <= a

def add_succ_r source · line 919 · raw

@+a:Nat -> @-b:Nat -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}

1 + (a + b) == a + (1 + b)

def add_zero_r source · line 928 · raw

@+a:Nat -> {Nat.add(a, 0n) == a : Nat}

a + 0 == a

def half_go_le source · line 937 · raw

@+n:Nat -> @+acc:Nat -> {True{} == leb(half.go(n, acc), Nat.add(n, acc)) : Bool}

half.go(n, acc) <= n + acc

def half_le source · line 950 · raw

@+n:Nat -> {True{} == leb(half(n), n) : Bool}

half(n) <= n

def add_sub source · line 955 · raw

@+a:Nat -> @+r:Nat -> @e:{True{} == leb(a, r) : Bool} -> {r == Nat.add(a, Nat.sub(r, a)) : Nat}

a <= r -> r == a + (r - a)

def Bands.zeros source · line 982 · raw

@+d:Nat -> @+r:Nat -> @+c:Nat -> Bands<r, c>

r x c of zeros in 2^d bands (d = 0: a single band, the same as a Mat)

def eq_half source · line 991 · raw

@-a:Nat -> @-b:Nat -> @e:{a == b : Nat} -> {half(a) == half(b) : Nat}

the row counts of the two bands follow the row count of the node: if rr == r at run time, the same holds for both halves (the bands carry r only in their type)

def eq_rest source · line 995 · raw

@-a:Nat -> @-b:Nat -> @e:{a == b : Nat} -> {Nat.sub(a, half(a)) == Nat.sub(b, half(b)) : Nat}

def bfill_l source · line 1001 · raw

@+r:Nat -> @+c:Nat -> @+i:Nat -> @+n:Nat -> Bool

does a block of n numbers starting at flat index i end before the second band of a node with r rows? does it start in the second band?

def bfill_r source · line 1004 · raw

@+r:Nat -> @+c:Nat -> @+i:Nat -> Bool

def fill_n source · line 1008 · raw

@n:Nat -> @xs:List<&2, F32> -> @+i:U32 -> @a:Array<F32> -> Array<F32>

writes the first n numbers of xs at index i (and nothing past them)

def fill_band source · line 1015 · raw

@-r:Nat -> @-c:Nat -> @n:Nat -> @xs:List<&2, F32> -> @+i:U32 -> @m:Mat<r, c> -> Mat<r, c>

def bfill source · line 1023 · raw

@+c:Nat -> @-r:Nat -> @b:Bands<r, c> -> @l:Bool -> @rt:Bool -> @+rr:Nat -> @-e:{rr == r : Nat} -> @+i:Nat -> @+n:Nat -> @+xs:List<&2, F32> -> Bands<r, c>

writes the first n numbers of xs at flat index i; l and rt say which bands they touch (bfill_l, bfill_r); rr is the row count r at run time. A block that crosses into the second band is not copied: the first band writes only its part, the second gets the rest by List.drop.

def bfill_top source · line 1034 · raw

@ok:Bool -> @+r:Nat -> @+c:Nat -> @b:Bands<r, c> -> @+i:Nat -> @+n:Nat -> @+xs:List<&2, F32> -> Bands<r, c>

def Bands.fill_at source · line 1043 · raw

@+r:Nat -> @+c:Nat -> @+i:Nat -> @+n:Nat -> @+xs:List<&2, F32> -> @b:Bands<r, c> -> Bands<r, c>

writes the n numbers of xs into b starting at flat index i (row-major, as Mat.fill_at); numbers past r*c are dropped. For loading a large matrix block by block.

def bv_g2 source · line 1056 · raw

@-r:Nat -> @-c:Nat -> @w:Array<F32> -> @al:AL -> BL<r, c>

def bv_g source · line 1062 · raw

@-r:Nat -> @-c:Nat -> @+m:Nat -> @g:G -> BL<r, c>

the band's 1 + m rows came out in an Array (one number per row); read them back as a list

def bv_gemm source · line 1070 · raw

@-r:Nat -> @+c:Nat -> @rows:Nat -> @+rr:Nat -> @x:Array<F32> -> @w:Array<F32> -> BL<r, c>

the rows of one band, one dot product each, with the gemm of Mat.matmul_nt (n = 1), so the results are identical. Writing the results into an Array and reading them back is faster than building the list row by row (NOTES.md, exp. 14).

def bv_mat source · line 1077 · raw

@-r:Nat -> @+c:Nat -> @+rr:Nat -> @x:Array<F32> -> @m:Mat<r, c> -> BL<r, c>

def bv_join source · line 1082 · raw

@-r:Nat -> @-c:Nat -> @p:BL<half(r), c> -> @q:BL<Nat.sub(r, half(r)), c> -> BL<r, c>

def bmv source · line 1091 · raw

@+c:Nat -> @-r:Nat -> @b:Bands<r, c> -> @+rr:Nat -> @-e:{rr == r : Nat} -> @xp:Pair(Array<F32>, Array<F32>) -> BL<r, c>

the two bands of a node run in parallel, each with its own copy of x (c numbers); xp is a pair of copies of x (a leaf uses one). xp comes after the erased e on purpose: in Bend 2.0.35 an erased parameter at the end of the list turns the parallel let into two sequential calls (NOTES.md, exp. 11).

def bv_fin source · line 1099 · raw

@+r:Nat -> @-c:Nat -> @bl:BL<r, c> -> BV<r, c>

def Bands.matvec source · line 1106 · raw

@+r:Nat -> @+c:Nat -> @b:Bands<r, c> -> @x:Mat<1n, c> -> BV<r, c>

y = B · x for B (r x c, one row per output) and x (1 x c); returns B intact and y (1 x r). The same product as Mat.matmul_nt(1n, c, r, ..), and the same numbers, bit for bit.

def Bands.matvec_l source · line 1113 · raw

@+r:Nat -> @+c:Nat -> @b:Bands<r, c> -> @+x:List<&2, F32> -> BL<r, c>

the same product with x and y as lists (x: c numbers, y: r numbers in row order), without the Mat conversions of Bands.matvec: for callers that already hold the vector as a list

def brow_fin source · line 1121 · raw

@-r:Nat -> @-c:Nat -> @al:AL -> BRow<r, c>

def brow_leaf2 source · line 1127 · raw

@-r:Nat -> @-c:Nat -> @n:Nat -> @+i:U32 -> @d:Array<F32> -> BRow<r, c>

n numbers starting at flat index i of one band (a band may have no rows)

def brow_leaf source · line 1134 · raw

@-r:Nat -> @-c:Nat -> @m:Mat<r, c> -> @+i:U32 -> @n:Nat -> BRow<r, c>

def brow_l source · line 1139 · raw

@-r:Nat -> @-c:Nat -> @p:BRow<half(r), c> -> @y:Bands<Nat.sub(r, half(r)), c> -> BRow<r, c>

def brow_r source · line 1144 · raw

@-r:Nat -> @-c:Nat -> @x:Bands<half(r), c> -> @q:BRow<Nat.sub(r, half(r)), c> -> BRow<r, c>

def brow source · line 1150 · raw

@+c:Nat -> @-r:Nat -> @b:Bands<r, c> -> @left:Bool -> @+rr:Nat -> @-e:{rr == r : Nat} -> @+i:Nat -> BRow<r, c>

row i; left says whether i is in the first band of the node (i < half(rr))

def Bands.read_row source · line 1160 · raw

@+r:Nat -> @+c:Nat -> @b:Bands<r, c> -> @+i:Nat -> BRow<r, c>

row i (c numbers), for example an embedding lookup

def bl_join source · line 1163 · raw

@-r:Nat -> @-c:Nat -> @p:BRow<half(r), c> -> @q:BRow<Nat.sub(r, half(r)), c> -> BRow<r, c>

def blist source · line 1168 · raw

@+c:Nat -> @-r:Nat -> @b:Bands<r, c> -> @+rr:Nat -> @-e:{rr == r : Nat} -> BRow<r, c>

def Bands.to_list source · line 1176 · raw

@+r:Nat -> @+c:Nat -> @b:Bands<r, c> -> BRow<r, c>

all r*c numbers in row order (in BRow.row)

def bl_len source · line 1184 · raw

@-r:Nat -> @-c:Nat -> @bl:BL<r, c> -> Nat

def succ_out source · line 1190 · raw

@-s:Nat -> @+a:Nat -> @+b:Nat -> @e:{s == Nat.add(a, 1n+b) : Nat} -> {s == 1n+Nat.add(a, b) : Nat}

s == a + (1 + b) -> s == 1 + (a + b)

def len_step source · line 1195 · raw

@-s:Nat -> @+p:Nat -> @+l:Nat -> @e:{s == 1n+Nat.add(p, 1n+l) : Nat} -> {s == 2n+Nat.add(p, l) : Nat}

s == 1 + (p + (1 + l)) -> s == 2 + (p + l)

def zero_out source · line 1200 · raw

@-s:Nat -> @+n:Nat -> @e:{s == Nat.add(n, 0n) : Nat} -> {s == n : Nat}

s == n + 0 -> s == n

def rev_len source · line 1205 · raw

@+xs:List<&2, F32> -> @+acc:List<&2, F32> -> {List.length(&2, F32, List.reverse.go(&2, F32, xs, acc)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, acc)) : Nat}

reversing onto acc adds the lengths

def app_len source · line 1213 · raw

@+xs:List<&2, F32> -> @+ys:List<&2, F32> -> {List.length(&2, F32, List.append(&2, F32, xs, ys)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, ys)) : Nat}

appending adds the lengths

def g_len source · line 1243 · raw

@-r:Nat -> @-c:Nat -> @+p:Nat -> @g:G -> {bl_len(r, c, bv_g(r, c, p, g)) == 1n+p : Nat}

whatever the gemm wrote, reading 1 + p rows back gives 1 + p numbers (G has one constructor, so matching g opens it, and leaf_len counts the list)

def join_len source · line 1269 · raw

@-r:Nat -> @-c:Nat -> @-h1:Nat -> @-h2:Nat -> @p:BL<half(r), c> -> @q:BL<Nat.sub(r, half(r)), c> -> @hp:{bl_len(half(r), c, p) == h1 : Nat} -> @hq:{bl_len(Nat.sub(r, half(r)), c, q) == h2 : Nat} -> {bl_len(r, c, bv_join(r, c, p, q)) == Nat.add(h1, h2) : Nat}

joining two halves of h1 and h2 numbers gives h1 + h2 numbers. (The statement for the whole tree, "Bands.matvec_l gives r numbers", would apply this to the results of the two recursive calls and to the induction hypotheses about the same calls; that uses each band's Array twice, which Bend's affine rules refuse. It stays open, covered by tests: NOTES.md, v3.1.)