bend-ml-tensor-array Releases (20): 0.1.19.0 0x54fd18094240d26f3074e1ee00279d63 indexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.19.0 0.1.18.0 0xf4dfe0b415f12cd7b6b3e20aa7cc5aa0 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.18.0 0.1.17.0 0x7a3ad9c30a648ef09dd908b6468f25ea unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.17.0 0.1.16.0 0x0159e1f0f11cc1d285ac6a993d19ba8a unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.16.0 0.1.15.0 0x054428f37dcef26dfcdf73a81af76b07 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.15.0 0.1.14.0 0x0f6479f09ada7ae614e64e31e8f5a730 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.14.0 0.1.13.0 0xf73c9a4e5c212ca51adae9ad129e57f7 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.13.0 0.1.12.0 0xf94fab1939abde90f6dd66413a7964d8 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.12.0 0.1.11.0 0xcd90bcc8501745cf08bdce89fc915900 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.11.0 0.1.10.0 0xbb78793a12728b7aa5a6f9756c65086a unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.10.0 0.1.9.0 0x4b971e2f6428dc3f80dcd5a04dedc5f2 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.9.0 0.1.8.0 0x3283e28131a46d2d98db11347f49016c unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.8.0 0.1.7.0 0x373e5f0e1b2ccdc5e9e1fe2004c1644c unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.7.0 0.1.6.0 0x793d6e22f8bd33acb2636b33544424bc unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.6.0 0.1.5.0 0x8c5737e1fd0b5ceef704ad97770f38ee unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.5.0 0.1.4.0 0x1e52188e4a40cfe41a87f1688743dff4 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.4.0 0.1.3.0 0xa78e1f1609ed090d0092c5fff6f9bac7 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.3.0 0.1.2.0 0x83d7a8813f8d06d870224fde14ffb05a unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.2.0 0.1.1.0 0x52546eabfdaff99acd3ccd759c45cd9f unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.1.0 0.1.0.0 0x11d97125d04a371763283ef9f67fd926 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-tensor-array@0.1.0.0 Definitions (321, 1 to 100 shown): BendMlTensorArray.R (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=R) type R is Type: R{a: Array, b: Array, x: F32} BendMlTensorArray.G (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=G) type G is Type: G{a: Array, b: Array, c: Array} BendMlTensorArray.dotr (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dotr) # 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 dotr(k: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, a0: F32, a1: F32, a2: F32, a3: F32, ra: Array & F32, rb: Array & F32) -> R: BendMlTensorArray.D4 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=D4) # dotr's state between two steps: the four partial sums and the two pending reads type D4 is Type: D4{a0: F32, a1: F32, a2: F32, a3: F32, ra: Array & F32, rb: Array & F32} BendMlTensorArray.dstep (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dstep) # one step of dotr: adds the pending product to a0, rotates the sums, reads the next pair at ia, ib def dstep(+ia: U32, +ib: U32, s: D4) -> D4: BendMlTensorArray.dfin (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dfin) def dfin(k: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, s: D4) -> R: BendMlTensorArray.dot4 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dot4) # dotr with its loop unrolled by four: q rounds of four dstep, then the last rem (< 4) steps by dotr itself. # Every product goes to the same sum in the same order as in dotr (four rotations bring the names back), so the # result has dotr's bits (tests/dot4.bend). The compiled loop runs ~16% fewer instructions; one thread on a # 50,257 x 768 matrix ยท vector goes from 26.7 to 20.0 ms, smaller ones and 16 threads stay within noise (NOTES.md, # 2026-11-01). Eight steps a round were no faster. def dot4(q: Nat, +rem: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, s: D4) -> R: BendMlTensorArray.dotg (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dotg) def dotg(+k: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, acc: F32, ra: Array & F32, rb: Array & F32) -> R: BendMlTensorArray.cwr_add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cwr_add) def cwr_add(+idx: U32, +x: F32, r: Array & F32) -> Array: BendMlTensorArray.cwr (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cwr) def cwr(ac: Bool, +idx: U32, +x: F32, c: Array) -> Array: BendMlTensorArray.gcols (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gcols) def gcols(+ac: Bool, mleft: Nat, +kn: Nat, +ia0: U32, +ib0: U32, +sa: U32, +sb: U32, +bcol: U32, +cidx: U32, c: Array, r: R) -> G: BendMlTensorArray.grows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=grows) def grows(+ac: Bool, nleft: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, +mu: U32, g: G) -> G: BendMlTensorArray.gemm_ac (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gemm_ac) def gemm_ac(+ac: Bool, +n: Nat, +m: Nat, +k: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array, c: Array) -> G: BendMlTensorArray.gemm (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gemm) def gemm(+n: Nat, +m: Nat, +k: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array, c: Array) -> G: BendMlTensorArray.S3 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=S3) type S3 is Type: S3{a: Array, b: Array, out: List<&2, F32>} BendMlTensorArray.lcols (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=lcols) def lcols(mleft: Nat, +kn: Nat, +ia0: U32, +ib0: U32, +sa: U32, +sb: U32, +bcol: U32, out: List<&2, F32>, r: R) -> S3: BendMlTensorArray.lrows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=lrows) def lrows(nleft: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, st: S3) -> S3: BendMlTensorArray.lblock_fin (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=lblock_fin) def lblock_fin(st: S3) -> List<&2, F32>: BendMlTensorArray.lblock (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=lblock) def lblock(cnt: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array) -> List<&2, F32>: BendMlTensorArray.lpar (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=lpar) def lpar(d: Nat, +cnt: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, ra: Array & Array, rb: Array & Array) -> List<&2, F32>: BendMlTensorArray.write_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=write_l) def write_l(xs: List<&2, F32>, +idx: U32, c: Array) -> Array: BendMlTensorArray.write_la (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=write_la) def write_la(+ac: Bool, xs: List<&2, F32>, +idx: U32, c: Array) -> Array: BendMlTensorArray.gp3 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gp3) def gp3(+ac: Bool, a: Array, b: Array, c: Array, xs: List<&2, F32>) -> G: BendMlTensorArray.gp2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gp2) def gp2(d: Nat, +n: Nat, +mm1: Nat, +kn: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, c: Array, pa: Array & Array, pb: Array & Array) -> G: BendMlTensorArray.gemm_par (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gemm_par) def gemm_par(d: Nat, +n: Nat, +m: Nat, +k: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array, c: Array) -> G: BendMlTensorArray.cblock_fin (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cblock_fin) def cblock_fin(st: S3) -> List<&2, F32>: BendMlTensorArray.cblock_go (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cblock_go) def cblock_go(cnt1: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array) -> List<&2, F32>: BendMlTensorArray.cblock (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cblock) def cblock(cnt: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array) -> List<&2, F32>: BendMlTensorArray.cpar (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cpar) def cpar(d: Nat, +cnt: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, ra: Array & Array, rb: Array & Array) -> List<&2, F32>: BendMlTensorArray.cp2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cp2) def cp2(+ac: Bool, d: Nat, +m: Nat, +kn: Nat, +sa: U32, +sb: U32, +bcol: U32, c: Array, pa: Array & Array, pb: Array & Array) -> G: BendMlTensorArray.gemm_par_cols (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gemm_par_cols) def gemm_par_cols(+ac: Bool, d: Nat, +m: Nat, +k: Nat, +sa: U32, +sb: U32, +bcol: U32, a: Array, b: Array, c: Array) -> G: BendMlTensorArray.P2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=P2) type P2 is Type: P2{a: Array, b: Array} BendMlTensorArray.AL (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=AL) type AL is Type: AL{c: Array, l: List<&2, F32>} BendMlTensorArray.read_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=read_l) def read_l(mleft: Nat, +idx: U32, acc: List<&2, F32>, rc: Array & F32) -> AL: BendMlTensorArray.addl (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=addl) def addl(xs: List<&2, F32>, +idx: U32, rc: Array & F32) -> Array: BendMlTensorArray.bias_rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=bias_rows) def bias_rows(nleft: Nat, +i: U32, +mu: U32, +bl: List<&2, F32>, c: Array) -> Array: BendMlTensorArray.relu_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=relu_l) def relu_l(nleft: Nat, +t: U32, rc: Array & F32) -> Array: BendMlTensorArray.pos2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pos2) def pos2(b: Bool) -> F32: BendMlTensorArray.pos (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pos) def pos(+y: F32) -> F32: BendMlTensorArray.mask_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=mask_l) def mask_l(nleft: Nat, +t: U32, rd: Array & F32, rh: Array & F32) -> P2: BendMlTensorArray.maxl2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=maxl2) def maxl2(xs: List<&2, F32>, cur: F32) -> F32: BendMlTensorArray.maxl (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=maxl) def maxl(xs: List<&2, F32>) -> F32: BendMlTensorArray.expl (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=expl) def expl(xs: List<&2, F32>, +m: F32) -> List<&2, F32>: BendMlTensorArray.suml (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=suml) def suml(xs: List<&2, F32>, acc: F32) -> F32: BendMlTensorArray.divl (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=divl) def divl(xs: List<&2, F32>, +s: F32) -> List<&2, F32>: BendMlTensorArray.softmax2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=softmax2) def softmax2(+es: List<&2, F32>) -> List<&2, F32>: BendMlTensorArray.softmax (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=softmax) def softmax(+xs: List<&2, F32>) -> List<&2, F32>: BendMlTensorArray.sgd_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=sgd_l) def sgd_l(nleft: Nat, +t: U32, +lr: F32, rw: Array & F32, rd: Array & F32) -> P2: BendMlTensorArray.pick (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pick) def pick(ps: List<&2, F32>, n: Nat) -> F32: BendMlTensorArray.hit (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=hit) def hit(b: Bool) -> F32: BendMlTensorArray.grad_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=grad_l) def grad_l(ps: List<&2, F32>, +label: Nat, +j: Nat, +nf: F32) -> List<&2, F32>: BendMlTensorArray.L2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=L2) type L2 is Type: L2{loss: F32, c: Array} BendMlTensorArray.ce_row2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ce_row2) def ce_row2(+ps: List<&2, F32>, +label: Nat, +nf: F32, +idx: U32, loss: F32, c: Array) -> L2: BendMlTensorArray.ce_row (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ce_row) def ce_row(al: AL, +label: Nat, +nf: F32, +idx: U32, loss: F32) -> L2: BendMlTensorArray.Mat (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=Mat) type Mat<-r: Nat, -c: Nat> is Type: Mat{d: Array} BendMlTensorArray.ce_rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ce_rows) def ce_rows(labels: List<&2, Nat>, +mm1: Nat, +mu: U32, +nf: F32, +i: U32, r: L2) -> L2: BendMlTensorArray.AF (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=AF) type AF is Type: AF{c: Array, x: F32} BendMlTensorArray.cea_max (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_max) # the max of k + 1 cells from idx, from m (the first cell's value, already read in r) def cea_max(k: Nat, +idx: U32, +m: F32, r: Array & F32) -> AF: BendMlTensorArray.cea_exp (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_exp) # cells idx..idx + k become exp(cell - m); returns their sum from s, added left to right def cea_exp(k: Nat, +idx: U32, +m: F32, +s: F32, r: Array & F32) -> AF: BendMlTensorArray.cea_grad (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_grad) # cell idx (column j) becomes ((e / s) - onehot) / nf, for k + 1 cells def cea_grad(k: Nat, +idx: U32, +j: Nat, +label: Nat, +s: F32, +nf: F32, r: Array & F32) -> Array: BendMlTensorArray.cea_p2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_p2) def cea_p2(+s: F32, r: Array & F32) -> AF: BendMlTensorArray.cea_p (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_p) # p[label] = e[label] / s, or 0.0 for a label past the row (pick's Nil case) def cea_p(inside: Bool, +o: U32, +label: Nat, +s: F32, c: Array) -> AF: BendMlTensorArray.cea_row3 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_row3) def cea_row3(+mm1: Nat, +o: U32, +label: Nat, +s: F32, +nf: F32, +loss: F32, q: AF) -> L2: BendMlTensorArray.cea_row2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_row2) def cea_row2(+mm1: Nat, +o: U32, +label: Nat, +nf: F32, +loss: F32, q: AF) -> L2: BendMlTensorArray.cea_row1 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_row1) def cea_row1(+mm1: Nat, +o: U32, +label: Nat, +nf: F32, +loss: F32, q: AF) -> L2: BendMlTensorArray.cea_row0 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_row0) # a row's max starts from its first cell (maxl), then folds over the k + 1 cells from it def cea_row0(+mm1: Nat, +o: U32, +label: Nat, +nf: F32, +loss: F32, r: Array & F32) -> L2: BendMlTensorArray.cea_rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cea_rows) # one row per label, in order, as ce_rows def cea_rows(labels: List<&2, Nat>, +mm1: Nat, +mu: U32, +nf: F32, +i: U32, r: L2) -> L2: BendMlTensorArray.CR (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=CR) type CR is Type: CR{c: Array, n: Nat} BendMlTensorArray.gt_head (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=gt_head) def gt_head(xs: List<&2, F32>, +v: F32) -> Bool: BendMlTensorArray.argmax2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=argmax2) def argmax2(xs: List<&2, F32>, g: Bool, +i: Nat, +bi: Nat, +bv: F32) -> Nat: BendMlTensorArray.argmax (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=argmax) def argmax(xs: List<&2, F32>) -> Nat: BendMlTensorArray.one (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=one) def one(b: Bool) -> Nat: BendMlTensorArray.count_rows3 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=count_rows3) def count_rows3(+y: Nat, n: Nat, al: AL) -> CR: BendMlTensorArray.count_rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=count_rows) def count_rows(labels: List<&2, Nat>, +mm1: Nat, +mu: U32, +i: U32, r: CR) -> CR: BendMlTensorArray.BD (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=BD) # a type chosen by a Bool: rewriting through it refutes True == False def BD(b: Bool, t: Type, f: Type) -> Type: BendMlTensorArray.leb (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb) # a <= b, by direct recursion def leb(a: Nat, b: Nat) -> Bool: BendMlTensorArray.pow2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pow2) def pow2(d: Nat) -> Nat: BendMlTensorArray.cap_pick (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_pick) # smallest power of two >= n, by structural recursion on n: returns (depth, 2^depth) def cap_pick(ok: Bool, d: Nat, +p: Nat) -> Nat & Nat: BendMlTensorArray.cap_step (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_step) def cap_step(r: Nat & Nat, +n: Nat) -> Nat & Nat: BendMlTensorArray.cap_pair (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_pair) def cap_pair(n: Nat) -> Nat & Nat: BendMlTensorArray.fst_nat (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=fst_nat) def fst_nat(r: Nat & Nat) -> Nat: BendMlTensorArray.snd_nat (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=snd_nat) def snd_nat(r: Nat & Nat) -> Nat: BendMlTensorArray.le_leb (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=le_leb) # leb is Base's Nat.is_le, case for case. leb walks its arguments one step at a time in the compiled program; Base's # comparison is one native comparison there (0.1.13.0). def le_leb(a: Nat, b: Nat) -> {Nat.is_le(a, b) == leb(a, b) : Bool}: BendMlTensorArray.leb_of (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_of) def leb_of(+a: Nat, +b: Nat, e: {True{} == Nat.is_le(a, b) : Bool}) -> {True{} == leb(a, b) : Bool}: BendMlTensorArray.cap_dbl (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_dbl) # the same pair by doubling (0.1.10.0): p doubles until n <= p, log2(n) steps in a tail loop, where cap_pair takes n # steps of a recursion that is not a tail call, each with a comparison of up to n steps. Its fuel is n, which always # suffices (2^n >= n); if it ran out, the answer would be cap_pair's, so the law below needs no arithmetic about how # many doublings there are. ok is Nat.is_le(n, p), computed by the caller (match only inspects a parameter); with leb # it was n steps in all, 152 ms for n = 786,432 on one GPU lane (0.1.13.0). def cap_dbl(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat) -> Nat & Nat: BendMlTensorArray.cap_depth (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_depth) # the depth d such that an Array with 2^d slots holds n elements (the smallest such d) def cap_depth(+n: Nat) -> Nat: BendMlTensorArray.leb_succ (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_succ) # a <= b -> a <= 1 + b def leb_succ(a: Nat, b: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, 1n+b) : Bool}: BendMlTensorArray.leb_up_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_up_l) # a <= b -> a <= c + b def leb_up_l(+a: Nat, +b: Nat, c: Nat, +e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(c, b)) : Bool}: BendMlTensorArray.leb_up (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_up) # a <= b -> a <= b + c def leb_up(a: Nat, b: Nat, c: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(b, c)) : Bool}: BendMlTensorArray.leb_add (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_add) # a <= b and c <= d -> a + c <= b + d def leb_add(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}: BendMlTensorArray.pow2_pos (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pow2_pos) # 1 <= 2^d def pow2_pos(d: Nat) -> {True{} == leb(1n, pow2(d)) : Bool}: BendMlTensorArray.pos_p (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=pos_p) # 1 <= p when p = 2^d def pos_p(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {True{} == leb(1n, p) : Bool}: BendMlTensorArray.step_eq (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=step_eq) # p + p == 2^(1+d) when p == 2^d def step_eq(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {Nat.add(p, p) == pow2(1n+d) : Nat}: BendMlTensorArray.step_ok (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=step_ok) # one step: given the invariant for m, the invariant for 1+m holds whichever way the comparison goes def step_ok(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}) -> {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}: BendMlTensorArray.step_pair_ok (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=step_pair_ok) # the invariant for cap_step on a pair, opened def step_pair_ok(+m: Nat, r: Nat & Nat, i1: {snd_nat(r) == pow2(fst_nat(r)) : Nat}, i2: {True{} == leb(m, snd_nat(r)) : Bool}) -> {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}: BendMlTensorArray.cap_succ (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_succ) def cap_succ(+m: Nat, ih: {snd_nat(cap_pair(m)) == pow2(fst_nat(cap_pair(m))) : Nat} & {True{} == leb(m, snd_nat(cap_pair(m))) : Bool}) -> {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}: BendMlTensorArray.cap_inv (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_inv) # the invariant of cap_pair: the second component is 2^(first) and is >= n def cap_inv(n: Nat) -> {snd_nat(cap_pair(n)) == pow2(fst_nat(cap_pair(n))) : Nat} & {True{} == leb(n, snd_nat(cap_pair(n))) : Bool}: BendMlTensorArray.dbl_inv (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dbl_inv) # the invariant of cap_dbl: whichever way it ends (n <= p found, or the fuel out and cap_pair's answer), the second # component is 2^(first) and is >= n def dbl_inv(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat, e: {ok == Nat.is_le(n, p) : Bool}, i1: {p == pow2(d) : Nat}) -> {snd_nat(cap_dbl(f, ok, n, d, p)) == pow2(fst_nat(cap_dbl(f, ok, n, d, p))) : Nat} & {True{} == leb(n, snd_nat(cap_dbl(f, ok, n, d, p))) : Bool}: BendMlTensorArray.dbl_final (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=dbl_final) def dbl_final(n: Nat, pr: {snd_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n)) == pow2(fst_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n))) : Nat} & {True{} == leb(n, snd_nat(cap_dbl(n, Nat.is_le(n, 1n), n, 0n, 1n))) : Bool}) -> {True{} == leb(n, pow2(cap_depth(n))) : Bool}: BendMlTensorArray.cap_ok (https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=cap_ok) # LAW (cap_ok): an Array with 2^cap_depth(n) slots always has room for n elements. law cap_ok: for +n: Nat {True{} == leb(n, pow2(cap_depth(n))) : Bool} More: https://jend.leeeet.dev/packages/bend-ml-tensor-array.txt?definitions_offset=100