1	# bend-ml-tensor-array: tensors over a flat Array<F32>, with the shape in the type.
2	#
3	#   import bend-ml-tensor-array@0.1.10.0/main.bend as TA
4	#
5	# Mat<r, c> stores r*c numbers in an Array<F32>, row by row (index i*c + j). The
6	# dimensions are erased type parameters: the same guarantee as bend-ml-tensor
7	# (a product with wrong dimensions does not compile), but ~50x faster than lists:
8	# Array.get/set by index, and products in parallel blocks of rows.
9	#
10	# An Array is affine (a single owner): every operation that reads an operand returns it
11	# together with the result (as Array.get does), in records MM, AR, ... Use Mat.clone
12	# when you need two copies.
13	#
14	# What is NOT proved: the invariant "the Array has capacity >= r*c" holds because
15	# the constructors (Mat.zeros, Mat.of_list) allocate the right size; and F32 is
16	# validated by tests against PyTorch (reference/test_tensor_array.py), not by proof.
17	
18	import Base
19	
20	# ---------------------------------------------------------------------
21	# helper types
22	# ---------------------------------------------------------------------
23	
24	type R is Type:
25	  R{a: Array<F32>, b: Array<F32>, x: F32}
26	
27	type G is Type:
28	  G{a: Array<F32>, b: Array<F32>, c: Array<F32>}
29	
30	# A dot product with four partial sums. Each step adds its product to a0 and rotates the sums
31	# (a1, a2, a3, a0), so each sum gets every fourth product and the processor can work on the next
32	# addition before the last one has finished; at the end the sums are added in pairs. The order of
33	# the additions is fixed, so the result is the same on every run and every thread count, but it is
34	# not the order of a single running sum (NOTES.md, exp. 17).
35	def dotr(k: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, a0: F32, a1: F32, a2: F32, a3: F32, ra: Array<F32> & F32, rb: Array<F32> & F32) -> R:
36	  match k ra rb:
37	    case 0n Tuple{a, x} Tuple{b, y}:
38	      R{a, b, ((a0 + a1 : F32) + (a2 + a3 : F32) : F32)}
39	    case 1n+p Tuple{a, +x} Tuple{b, +y}:
40	      dotr(p, (ia + sa : U32), (ib + sb : U32), sa, sb, a1, a2, a3, (a0 + (x * y : F32) : F32), Array.get(F32, a, (ia + sa : U32)), Array.get(F32, b, (ib + sb : U32)))
41	
42	def dotg(k: Nat, +ia: U32, +ib: U32, +sa: U32, +sb: U32, acc: F32, ra: Array<F32> & F32, rb: Array<F32> & F32) -> R:
43	  dotr(k, ia, ib, sa, sb, acc, 0.0, 0.0, 0.0, ra, rb)
44	
45	# writes one cell of C: c[idx] = x, or c[idx] = c[idx] + x when ac (an accumulating product, 0.1.10.0). x is computed
46	# exactly as without ac and added once, so C + A·B has the bits of adding a separately computed A·B to C.
47	
48	def cwr_add(+idx: U32, +x: F32, r: Array<F32> & F32) -> Array<F32>:
49	  match r:
50	    case Tuple{c, +v}:
51	      Array.set(F32, c, idx, (v + x : F32))
52	
53	def cwr(ac: Bool, +idx: U32, +x: F32, c: Array<F32>) -> Array<F32>:
54	  match ac:
55	    case True{}:
56	      cwr_add(idx, x, Array.get(F32, c, idx))
57	    case False{}:
58	      Array.set(F32, c, idx, x)
59	
60	# row i of C, columns j.. ; r is the product of the current column (already computed)
61	
62	def gcols(+ac: Bool, mleft: Nat, +kn: Nat, +ia0: U32, +ib0: U32, +sa: U32, +sb: U32, +bcol: U32, +cidx: U32, c: Array<F32>, r: R) -> G:
63	  match mleft r:
64	    case 0n R{a, b, +x}:
65	      G{a, b, cwr(ac, cidx, x, c)}
66	    case 1n+p R{a, b, +x}:
67	      gcols(ac, p, kn, ia0, (ib0 + bcol : U32), sa, sb, bcol, (cidx + 1 : U32), cwr(ac, cidx, x, c), dotg(kn, ia0, (ib0 + bcol : U32), sa, sb, 0.0, Array.get(F32, a, ia0), Array.get(F32, b, (ib0 + bcol : U32))))
68	
69	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:
70	  match nleft g:
71	    case 0n G{a, b, c}:
72	      G{a, b, c}
73	    case 1n+p G{a, b, c}:
74	      grows(ac, p, mm1, kn, (i + 1 : U32), arow, sa, sb, bcol, mu, gcols(ac, mm1, kn, (i * arow : U32), 0, sa, sb, bcol, (i * mu : U32), c, dotg(kn, (i * arow : U32), 0, sa, sb, 0.0, Array.get(F32, a, (i * arow : U32)), Array.get(F32, b, 0))))
75	
76	# C (n x m) = A · B with k steps, or C + A · B when ac; c is the output array (with capacity n*m)
77	
78	def gemm_ac(+ac: Bool, +n: Nat, +m: Nat, +k: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>, c: Array<F32>) -> G:
79	  grows(ac, n, Nat.sub(m, 1n), k, 0, arow, sa, sb, bcol, U32.from_nat(m), G{a, b, c})
80	
81	def gemm(+n: Nat, +m: Nat, +k: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>, c: Array<F32>) -> G:
82	  gemm_ac(False{}, n, m, k, arow, sa, sb, bcol, a, b, c)
83	
84	
85	# ---------------------------------------------------------------------
86	# parallel gemm: 2^d blocks of rows of C, each with its own copy of A and B,
87	# returning lists that are written into C at the end
88	# ---------------------------------------------------------------------
89	
90	type S3 is Type:
91	  S3{a: Array<F32>, b: Array<F32>, out: List<&2, F32>}
92	
93	def lcols(mleft: Nat, +kn: Nat, +ia0: U32, +ib0: U32, +sa: U32, +sb: U32, +bcol: U32, out: List<&2, F32>, r: R) -> S3:
94	  match mleft r:
95	    case 0n R{a, b, +x}:
96	      S3{a, b, x <> out}
97	    case 1n+p R{a, b, +x}:
98	      lcols(p, kn, ia0, (ib0 + bcol : U32), sa, sb, bcol, x <> out, dotg(kn, ia0, (ib0 + bcol : U32), sa, sb, 0.0, Array.get(F32, a, ia0), Array.get(F32, b, (ib0 + bcol : U32))))
99	
100	def lrows(nleft: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, st: S3) -> S3:
101	  match nleft st:
102	    case 0n S3{a, b, out}:
103	      S3{a, b, out}
104	    case 1n+p S3{a, b, out}:
105	      lrows(p, mm1, kn, (i + 1 : U32), arow, sa, sb, bcol, lcols(mm1, kn, (i * arow : U32), 0, sa, sb, bcol, out, dotg(kn, (i * arow : U32), 0, sa, sb, 0.0, Array.get(F32, a, (i * arow : U32)), Array.get(F32, b, 0))))
106	
107	def lblock_fin(st: S3) -> List<&2, F32>:
108	  match st:
109	    case S3{a, b, out}:
110	      List.reverse(&2, F32, out)
111	
112	def lblock(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>:
113	  lblock_fin(lrows(cnt, mm1, kn, i, arow, sa, sb, bcol, S3{a, b, Nil{}}))
114	
115	def lpar(d: Nat, +cnt: Nat, +mm1: Nat, +kn: Nat, +i: U32, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, ra: Array<F32> & Array<F32>, rb: Array<F32> & Array<F32>) -> List<&2, F32>:
116	  match d ra rb:
117	    case 0n Tuple{a, a2} Tuple{b, b2}:
118	      lblock(cnt, mm1, kn, i, arow, sa, sb, bcol, a, b)
119	    case 1n++q Tuple{a, a2} Tuple{b, b2}:
120	      x y = lpar(q, Nat.div(cnt, 2n), mm1, kn, i, arow, sa, sb, bcol, Array.clone(F32, a), Array.clone(F32, b)) lpar(q, Nat.sub(cnt, Nat.div(cnt, 2n)), mm1, kn, (i + U32.from_nat(Nat.div(cnt, 2n)) : U32), arow, sa, sb, bcol, Array.clone(F32, a2), Array.clone(F32, b2))
121	      List.append(&2, F32, x, y)
122	
123	def write_l(xs: List<&2, F32>, +idx: U32, c: Array<F32>) -> Array<F32>:
124	  match xs:
125	    case Nil{}:
126	      c
127	    case Con{h, t}:
128	      write_l(t, (idx + 1 : U32), Array.set(F32, c, idx, h))
129	
130	# c[idx..] = list, or c[idx..] += list when ac
131	
132	def write_la(+ac: Bool, xs: List<&2, F32>, +idx: U32, c: Array<F32>) -> Array<F32>:
133	  match xs:
134	    case Nil{}:
135	      c
136	    case Con{+h, t}:
137	      write_la(ac, t, (idx + 1 : U32), cwr(ac, idx, h, c))
138	
139	def gp3(+ac: Bool, a: Array<F32>, b: Array<F32>, c: Array<F32>, xs: List<&2, F32>) -> G:
140	  G{a, b, write_la(ac, xs, 0, c)}
141	
142	def gp2(d: Nat, +n: Nat, +mm1: Nat, +kn: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, c: Array<F32>, pa: Array<F32> & Array<F32>, pb: Array<F32> & Array<F32>) -> G:
143	  match pa pb:
144	    case Tuple{a1, a2} Tuple{b1, b2}:
145	      gp3(False{}, a1, b1, c, lpar(d, n, mm1, kn, 0, arow, sa, sb, bcol, Array.clone(F32, a2), Array.clone(F32, b2)))
146	
147	# C (n x m) = A · B, with 2^d blocks of rows in parallel; returns A, B (intact) and C
148	
149	def gemm_par(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:
150	  gp2(d, n, Nat.sub(m, 1n), k, arow, sa, sb, bcol, c, Array.clone(F32, a), Array.clone(F32, b))
151	
152	
153	# ---------------------------------------------------------------------
154	# parallel gemm by COLUMNS, for n = 1 (matrix · vector): each block computes a
155	# range of columns of C, with its own copy of the operands
156	# ---------------------------------------------------------------------
157	
158	def cblock_fin(st: S3) -> List<&2, F32>:
159	  match st:
160	    case S3{a, b, out}:
161	      List.reverse(&2, F32, out)
162	
163	# cnt columns starting at j0 (cnt >= 1); row 0 of A is at ia0
164	
165	def cblock_go(cnt1: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>) -> List<&2, F32>:
166	  cblock_fin(lcols(cnt1, kn, ia0, (j0 * bcol : U32), sa, sb, bcol, Nil{}, dotg(kn, ia0, (j0 * bcol : U32), sa, sb, 0.0, Array.get(F32, a, ia0), Array.get(F32, b, (j0 * bcol : U32)))))
167	
168	def cblock(cnt: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>) -> List<&2, F32>:
169	  match cnt:
170	    case 0n:
171	      Nil{}
172	    case 1n+p:
173	      cblock_go(p, kn, ia0, j0, sa, sb, bcol, a, b)
174	
175	def cpar(d: Nat, +cnt: Nat, +kn: Nat, +ia0: U32, +j0: U32, +sa: U32, +sb: U32, +bcol: U32, ra: Array<F32> & Array<F32>, rb: Array<F32> & Array<F32>) -> List<&2, F32>:
176	  match d ra rb:
177	    case 0n Tuple{a, a2} Tuple{b, b2}:
178	      cblock(cnt, kn, ia0, j0, sa, sb, bcol, a, b)
179	    case 1n++q Tuple{a, a2} Tuple{b, b2}:
180	      x y = cpar(q, Nat.div(cnt, 2n), kn, ia0, j0, sa, sb, bcol, Array.clone(F32, a), Array.clone(F32, b)) cpar(q, Nat.sub(cnt, Nat.div(cnt, 2n)), kn, ia0, (j0 + U32.from_nat(Nat.div(cnt, 2n)) : U32), sa, sb, bcol, Array.clone(F32, a2), Array.clone(F32, b2))
181	      List.append(&2, F32, x, y)
182	
183	def cp2(+ac: Bool, d: Nat, +m: Nat, +kn: Nat, +sa: U32, +sb: U32, +bcol: U32, c: Array<F32>, pa: Array<F32> & Array<F32>, pb: Array<F32> & Array<F32>) -> G:
184	  match pa pb:
185	    case Tuple{a1, a2} Tuple{b1, b2}:
186	      gp3(ac, a1, b1, c, cpar(d, m, kn, 0, 0, sa, sb, bcol, Array.clone(F32, a2), Array.clone(F32, b2)))
187	
188	# C (1 x m) = A (1 x k) · B, with 2^d blocks of columns in parallel
189	
190	def gemm_par_cols(+ac: Bool, d: Nat, +m: Nat, +k: Nat, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>, c: Array<F32>) -> G:
191	  cp2(ac, d, m, k, sa, sb, bcol, c, Array.clone(F32, a), Array.clone(F32, b))
192	
193	# ---------------------------------------------------------------------
194	# element-wise operations (in place, by index)
195	# ---------------------------------------------------------------------
196	
197	# ---------------------------------------------------------------------
198	# gemm: C[i][j] = sum_p A[i*arow + p*sa] * B[p*sb + j*bcol]
199	# (nn: arow=K, sa=1, sb=M, bcol=1 | nt: B stored m x k: sb=1, bcol=K | tn: A stored k x n: arow=1, sa=N)
200	# ---------------------------------------------------------------------
201	
202	# acc += A[ia + t*sa] * B[ib + t*sb] for k steps; ra, rb already carry the first pair
203	
204	type P2 is Type:
205	  P2{a: Array<F32>, b: Array<F32>}
206	
207	type AL is Type:
208	  AL{c: Array<F32>, l: List<&2, F32>}
209	
210	# list of m elements starting at idx (reads with Array.get, returning the array)
211	
212	def read_l(mleft: Nat, +idx: U32, acc: List<&2, F32>, rc: Array<F32> & F32) -> AL:
213	  match mleft rc:
214	    case 0n Tuple{c, +v}:
215	      AL{c, List.reverse(&2, F32, v <> acc)}
216	    case 1n+p Tuple{c, +v}:
217	      read_l(p, (idx + 1 : U32), v <> acc, Array.get(F32, c, (idx + 1 : U32)))
218	
219	# writes the list starting at idx
220	
221	def addl(xs: List<&2, F32>, +idx: U32, rc: Array<F32> & F32) -> Array<F32>:
222	  match xs rc:
223	    case Nil{} Tuple{c, v}:
224	      c
225	    case Con{+h, t} Tuple{c, +v}:
226	      addl(t, (idx + 1 : U32), Array.get(F32, Array.set(F32, c, idx, (v + h : F32)), (idx + 1 : U32)))
227	
228	# adds a bias (a list of m) to each of the n rows of c (n x m)
229	
230	def bias_rows(nleft: Nat, +i: U32, +mu: U32, +bl: List<&2, F32>, c: Array<F32>) -> Array<F32>:
231	  match nleft:
232	    case 0n:
233	      c
234	    case 1n+p:
235	      bias_rows(p, (i + 1 : U32), mu, bl, addl(bl, (i * mu : U32), Array.get(F32, c, (i * mu : U32))))
236	
237	# in-place relu on the first n elements
238	
239	def relu_l(nleft: Nat, +t: U32, rc: Array<F32> & F32) -> Array<F32>:
240	  match nleft rc:
241	    case 0n Tuple{c, v}:
242	      c
243	    case 1n+p Tuple{c, +v}:
244	      relu_l(p, (t + 1 : U32), Array.get(F32, Array.set(F32, c, t, F32.max(v, 0.0)), (t + 1 : U32)))
245	
246	def pos2(b: Bool) -> F32:
247	  match b:
248	    case True{}:
249	      1.0
250	    case False{}:
251	      0.0
252	
253	def pos(+y: F32) -> F32:
254	  pos2(F32.is_gt(y, 0.0))
255	
256	# d[t] *= (h[t] > 0): the relu gradient; returns both arrays
257	
258	def mask_l(nleft: Nat, +t: U32, rd: Array<F32> & F32, rh: Array<F32> & F32) -> P2:
259	  match nleft rd rh:
260	    case 0n Tuple{d, x} Tuple{h, y}:
261	      P2{d, h}
262	    case 1n+p Tuple{d, +x} Tuple{h, +y}:
263	      mask_l(p, (t + 1 : U32), Array.get(F32, Array.set(F32, d, t, (x * pos(y) : F32)), (t + 1 : U32)), Array.get(F32, h, (t + 1 : U32)))
264	
265	# w[t] -= lr * dw[t]
266	
267	def maxl2(xs: List<&2, F32>, cur: F32) -> F32:
268	  match xs:
269	    case Nil{}:
270	      cur
271	    case Con{+h, t}:
272	      maxl2(t, F32.max(cur, h))
273	
274	def maxl(xs: List<&2, F32>) -> F32:
275	  match xs:
276	    case Nil{}:
277	      0.0
278	    case Con{+h, t}:
279	      maxl2(t, h)
280	
281	def expl(xs: List<&2, F32>, +m: F32) -> List<&2, F32>:
282	  match xs:
283	    case Nil{}:
284	      Nil{}
285	    case Con{+h, t}:
286	      F32.exp((h - m : F32)) <> expl(t, m)
287	
288	def suml(xs: List<&2, F32>, acc: F32) -> F32:
289	  match xs:
290	    case Nil{}:
291	      acc
292	    case Con{+h, t}:
293	      suml(t, (acc + h : F32))
294	
295	def divl(xs: List<&2, F32>, +s: F32) -> List<&2, F32>:
296	  match xs:
297	    case Nil{}:
298	      Nil{}
299	    case Con{+h, t}:
300	      (h / s : F32) <> divl(t, s)
301	
302	def softmax2(+es: List<&2, F32>) -> List<&2, F32>:
303	  divl(es, suml(es, 0.0))
304	
305	def softmax(+xs: List<&2, F32>) -> List<&2, F32>:
306	  softmax2(expl(xs, maxl(xs)))
307	
308	# p[label]
309	
310	def sgd_l(nleft: Nat, +t: U32, +lr: F32, rw: Array<F32> & F32, rd: Array<F32> & F32) -> P2:
311	  match nleft rw rd:
312	    case 0n Tuple{w, x} Tuple{d, y}:
313	      P2{w, d}
314	    case 1n+p Tuple{w, +x} Tuple{d, +y}:
315	      sgd_l(p, (t + 1 : U32), lr, Array.get(F32, Array.set(F32, w, t, (x - (lr * y : F32) : F32)), (t + 1 : U32)), Array.get(F32, d, (t + 1 : U32)))
316	
317	# ---------------------------------------------------------------------
318	# softmax + cross-entropy per row (lists of 10 elements: negligible cost)
319	# ---------------------------------------------------------------------
320	
321	def pick(ps: List<&2, F32>, n: Nat) -> F32:
322	  match ps n:
323	    case Con{+h, t} 0n:
324	      h
325	    case Con{h, t} 1n+q:
326	      pick(t, q)
327	    case Nil{} _:
328	      0.0
329	
330	# (p - onehot(label)) / n
331	
332	def hit(b: Bool) -> F32:
333	  match b:
334	    case True{}:
335	      1.0
336	    case False{}:
337	      0.0
338	
339	def grad_l(ps: List<&2, F32>, +label: Nat, +j: Nat, +nf: F32) -> List<&2, F32>:
340	  match ps:
341	    case Nil{}:
342	      Nil{}
343	    case Con{+h, t}:
344	      (((h - hit(Nat.is_eq(label, j)) : F32) / nf) : F32) <> grad_l(t, label, 1n+j, nf)
345	
346	type L2 is Type:
347	  L2{loss: F32, c: Array<F32>}
348	
349	def ce_row2(+ps: List<&2, F32>, +label: Nat, +nf: F32, +idx: U32, loss: F32, c: Array<F32>) -> L2:
350	  L2{(loss - F32.log(F32.max(pick(ps, label), 0.000000000001)) : F32), write_l(grad_l(ps, label, 0n, nf), idx, c)}
351	
352	def ce_row(al: AL, +label: Nat, +nf: F32, +idx: U32, loss: F32) -> L2:
353	  match al:
354	    case AL{c, l}:
355	      ce_row2(softmax(l), label, nf, idx, loss, c)
356	
357	# walks the rows of z2 (n x m): r carries the accumulated loss and the array; at the end the array has become the gradient
358	
359	type Mat<-r: Nat, -c: Nat> is Type:
360	  Mat{d: Array<F32>}
361	
362	def ce_rows(labels: List<&2, Nat>, +mm1: Nat, +mu: U32, +nf: F32, +i: U32, r: L2) -> L2:
363	  match labels r:
364	    case Nil{} L2{loss, c}:
365	      L2{loss, c}
366	    case Con{+y, t} L2{loss, c}:
367	      ce_rows(t, mm1, mu, nf, (i + 1 : U32), ce_row(read_l(mm1, (i * mu : U32), Nil{}, Array.get(F32, c, (i * mu : U32))), y, nf, (i * mu : U32), loss))
368	
369	# ---- helper: hits per row ----
370	
371	type CR is Type:
372	  CR{c: Array<F32>, n: Nat}
373	
374	def gt_head(xs: List<&2, F32>, +v: F32) -> Bool:
375	  match xs:
376	    case Nil{}:
377	      False{}
378	    case Con{+h, t}:
379	      F32.is_gt(h, v)
380	
381	def argmax2(xs: List<&2, F32>, g: Bool, +i: Nat, +bi: Nat, +bv: F32) -> Nat:
382	  match xs g:
383	    case Nil{} _:
384	      bi
385	    case Con{+h, +t} True{}:
386	      argmax2(t, gt_head(t, h), 1n+i, i, h)
387	    case Con{h, +t} False{}:
388	      argmax2(t, gt_head(t, bv), 1n+i, bi, bv)
389	
390	def argmax(xs: List<&2, F32>) -> Nat:
391	  match xs:
392	    case Nil{}:
393	      0n
394	    case Con{+h, +t}:
395	      argmax2(t, gt_head(t, h), 1n, 0n, h)
396	
397	def one(b: Bool) -> Nat:
398	  match b:
399	    case True{}:
400	      1n
401	    case False{}:
402	      0n
403	
404	def count_rows3(+y: Nat, n: Nat, al: AL) -> CR:
405	  match al:
406	    case AL{c, l}:
407	      CR{c, Nat.add(n, one(Nat.is_eq(argmax(l), y)))}
408	
409	def count_rows(labels: List<&2, Nat>, +mm1: Nat, +mu: U32, +i: U32, r: CR) -> CR:
410	  match labels r:
411	    case Nil{} CR{c, n}:
412	      CR{c, n}
413	    case Con{+y, t} CR{c, n}:
414	      count_rows(t, mm1, mu, (i + 1 : U32), count_rows3(y, n, read_l(mm1, (i * mu : U32), Nil{}, Array.get(F32, c, (i * mu : U32)))))
415	
416	
417	# =====================================================================
418	# Typed API: Mat<r, c> (the dimensions enter the type)
419	# =====================================================================
420	
421	# =====================================================================
422	# Array capacity: a PROVED depth for the number of slots
423	# =====================================================================
424	#
425	# cap_depth(n) is the d such that an Array with 2^d slots holds n elements. It is computed by
426	# structural recursion on n (not with U32.log2) so that the law cap_ok below can prove
427	# `n <= 2^cap_depth(n)`. What stays trusted is only that Array.new(T, d, v) allocates 2^d slots.
428	
429	# a type chosen by a Bool: rewriting through it refutes True == False
430	def BD(b: Bool, t: Type, f: Type) -> Type:
431	  match b:
432	    case True{}:
433	      t
434	    case False{}:
435	      f
436	
437	# a <= b, by direct recursion
438	def leb(a: Nat, b: Nat) -> Bool:
439	  match a b:
440	    case 0n _:
441	      True{}
442	    case 1n+p 0n:
443	      False{}
444	    case 1n+p 1n+q:
445	      leb(p, q)
446	
447	def pow2(d: Nat) -> Nat:
448	  match d:
449	    case 0n:
450	      1n
451	    case 1n++q:
452	      Nat.add(pow2(q), pow2(q))
453	
454	# smallest power of two >= n, by structural recursion on n: returns (depth, 2^depth)
455	def cap_pick(ok: Bool, d: Nat, +p: Nat) -> Nat & Nat:
456	  match ok:
457	    case True{}:
458	      (d, p)
459	    case False{}:
460	      (1n+d, Nat.add(p, p))
461	
462	def cap_step(r: Nat & Nat, +n: Nat) -> Nat & Nat:
463	  match r:
464	    case Tuple{+d, +p}:
465	      cap_pick(leb(n, p), d, p)
466	
467	def cap_pair(n: Nat) -> Nat & Nat:
468	  match n:
469	    case 0n:
470	      (0n, 1n)
471	    case 1n++m:
472	      cap_step(cap_pair(m), 1n+m)
473	
474	def fst_nat(r: Nat & Nat) -> Nat:
475	  match r:
476	    case Tuple{d, p}:
477	      d
478	
479	def snd_nat(r: Nat & Nat) -> Nat:
480	  match r:
481	    case Tuple{d, p}:
482	      p
483	
484	# 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
485	# 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
486	# suffices (2^n >= n); if it ran out, the answer would be cap_pair's, so the law below needs no arithmetic about how
487	# many doublings there are. ok is leb(n, p), computed by the caller (match only inspects a parameter).
488	def cap_dbl(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat) -> Nat & Nat:
489	  match f ok:
490	    case _ True{}:
491	      (d, p)
492	    case 0n False{}:
493	      cap_pair(n)
494	    case 1n+g False{}:
495	      cap_dbl(g, leb(n, Nat.add(p, p)), n, 1n+d, Nat.add(p, p))
496	
497	# the depth d such that an Array with 2^d slots holds n elements (the smallest such d)
498	def cap_depth(+n: Nat) -> Nat:
499	  fst_nat(cap_dbl(n, leb(n, 1n), n, 0n, 1n))
500	
501	# ---- lemmas ----
502	
503	# a <= b  ->  a <= 1 + b
504	def leb_succ(a: Nat, b: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, 1n+b) : Bool}:
505	  match a b:
506	    case 0n _:
507	      {==}
508	    case 1n+p 0n:
509	      %e : BD(_, Unit, {True{} == leb(1n+p, 1n) : Bool})
510	      Unit{}
511	    case 1n+p 1n+q:
512	      leb_succ(p, q, e)
513	
514	# a <= b  ->  a <= c + b
515	def leb_up_l(+a: Nat, +b: Nat, c: Nat, +e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(c, b)) : Bool}:
516	  match c:
517	    case 0n:
518	      e
519	    case 1n++c2:
520	      leb_succ(a, Nat.add(c2, b), leb_up_l(a, b, c2, e))
521	
522	# a <= b  ->  a <= b + c
523	def leb_up(a: Nat, b: Nat, c: Nat, e: {True{} == leb(a, b) : Bool}) -> {True{} == leb(a, Nat.add(b, c)) : Bool}:
524	  match a b:
525	    case 0n _:
526	      {==}
527	    case 1n+p 0n:
528	      %e : BD(_, Unit, {True{} == leb(1n+p, Nat.add(0n, c)) : Bool})
529	      Unit{}
530	    case 1n+p 1n+q:
531	      leb_up(p, q, c, e)
532	
533	# a <= b  and  c <= d  ->  a + c <= b + d
534	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}:
535	  match a b:
536	    case 0n _:
537	      leb_up_l(c, d, b, e2)
538	    case 1n+p 0n:
539	      %e1 : BD(_, Unit, {True{} == leb(Nat.add(1n+p, c), Nat.add(0n, d)) : Bool})
540	      Unit{}
541	    case 1n+p 1n+q:
542	      leb_add(p, q, c, d, e1, e2)
543	
544	# 1 <= 2^d
545	def pow2_pos(d: Nat) -> {True{} == leb(1n, pow2(d)) : Bool}:
546	  match d:
547	    case 0n:
548	      {==}
549	    case 1n++q:
550	      leb_up(1n, pow2(q), pow2(q), pow2_pos(q))
551	
552	# 1 <= p when p = 2^d
553	def pos_p(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {True{} == leb(1n, p) : Bool}:
554	  %Equal.sym(Nat, p, pow2(d), i1) : {True{} == leb(1n, _) : Bool}
555	  pow2_pos(d)
556	
557	# p + p == 2^(1+d) when p == 2^d
558	def step_eq(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {Nat.add(p, p) == pow2(1n+d) : Nat}:
559	  %i1 : {Nat.add(p, p) == Nat.add(_, _) : Nat}
560	  {==}
561	
562	# one step: given the invariant for m, the invariant for 1+m holds whichever way the comparison goes
563	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}:
564	  match ok:
565	    case True{}:
566	      (i1, e)
567	    case False{}:
568	      (step_eq(d, p, i1), leb_add(1n, p, m, p, pos_p(d, p, i1), i2))
569	
570	
571	# the invariant for cap_step on a pair, opened
572	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}:
573	  match r:
574	    case Tuple{+d, +p}:
575	      step_ok(leb(1n+m, p), d, p, m, {==}, i1, i2)
576	
577	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}:
578	  match ih:
579	    case Tuple{i1, i2}:
580	      step_pair_ok(m, cap_pair(m), i1, i2)
581	
582	# the invariant of cap_pair: the second component is 2^(first) and is >= n
583	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}:
584	  match n:
585	    case 0n:
586	      ({==}, {==})
587	    case 1n++m:
588	      cap_succ(m, cap_inv(m))
589	
590	# the invariant of cap_dbl: whichever way it ends (n <= p found, or the fuel out and cap_pair's answer), the second
591	# component is 2^(first) and is >= n
592	def dbl_inv(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat, e: {ok == leb(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}:
593	  match f ok:
594	    case _ True{}:
595	      (i1, e)
596	    case 0n False{}:
597	      cap_inv(n)
598	    case 1n+g False{}:
599	      dbl_inv(g, leb(n, Nat.add(p, p)), n, 1n+d, Nat.add(p, p), {==}, step_eq(d, p, i1))
600	
601	def dbl_final(n: Nat, pr: {snd_nat(cap_dbl(n, leb(n, 1n), n, 0n, 1n)) == pow2(fst_nat(cap_dbl(n, leb(n, 1n), n, 0n, 1n))) : Nat} & {True{} == leb(n, snd_nat(cap_dbl(n, leb(n, 1n), n, 0n, 1n))) : Bool}) -> {True{} == leb(n, pow2(cap_depth(n))) : Bool}:
602	  match pr:
603	    case Tuple{i1, i2}:
604	      %i1 : {True{} == leb(n, _) : Bool}
605	      i2
606	
607	# LAW (cap_ok): an Array with 2^cap_depth(n) slots always has room for n elements.
608	law cap_ok:
609	  for +n: Nat
610	  {True{} == leb(n, pow2(cap_depth(n))) : Bool}
611	
612	def cap_ok(n):
613	  dbl_final(n, dbl_inv(n, leb(n, 1n), n, 0n, 1n, {==}, {==}))
614	
615	# r x c of zeros, with the exact capacity (smallest power of 2)
616	
617	def Mat.zeros(+r: Nat, +c: Nat) -> Mat<r, c>:
618	  Mat{Array.new(F32, cap_depth(Nat.mul(r, c)), 0.0)}
619	
620	def Mat.fill(+r: Nat, +c: Nat, +v: F32) -> Mat<r, c>:
621	  Mat{Array.new(F32, cap_depth(Nat.mul(r, c)), v)}
622	
623	def fill_list(xs: List<&2, F32>, +i: U32, a: Array<F32>) -> Array<F32>:
624	  match xs:
625	    case Nil{}:
626	      a
627	    case Con{h, t}:
628	      fill_list(t, (i + 1 : U32), Array.set(F32, a, i, h))
629	
630	def len_is(xs: List<&2, F32>, n: Nat) -> Bool:
631	  match xs n:
632	    case Nil{} 0n:
633	      True{}
634	    case Con{h, t} 1n+p:
635	      len_is(t, p)
636	    case _ _:
637	      False{}
638	
639	def Mat.of_list2(-r: Nat, -c: Nat, +rr: Nat, +cc: Nat, ok: Bool, xs: List<&2, F32>) -> Maybe<&1, Mat<r, c>>:
640	  match ok:
641	    case True{}:
642	      Some{Mat{fill_list(xs, 0, Array.new(F32, cap_depth(Nat.mul(rr, cc)), 0.0))}}
643	    case False{}:
644	      None{}
645	
646	# Mat<r, c> from r*c numbers in row order; None if the size does not match
647	
648	def Mat.of_list(+r: Nat, +c: Nat, +xs: List<&2, F32>) -> Maybe<&1, Mat<r, c>>:
649	  Mat.of_list2(r, c, r, c, len_is(xs, Nat.mul(r, c)), xs)
650	
651	# reads the first n numbers, returning the matrix
652	
653	# Mat<r, c> without checking the list size (a short list leaves the rest at zero, a long one is cut
654	# by the capacity): only for when the size is known by construction. Prefer Mat.of_list.
655	
656	def Mat.from_list(+r: Nat, +c: Nat, xs: List<&2, F32>) -> Mat<r, c>:
657	  Mat{fill_list(xs, 0, Array.new(F32, cap_depth(Nat.mul(r, c)), 0.0))}
658	
659	# writes the numbers of xs into m starting at flat index i (row-major); numbers past the
660	# capacity are dropped. For loading a large matrix block by block without building one big list.
661	def Mat.fill_at(-r: Nat, -c: Nat, +i: U32, xs: List<&2, F32>, m: Mat<r, c>) -> Mat<r, c>:
662	  match m:
663	    case Mat{d}:
664	      Mat{fill_list(xs, i, d)}
665	
666	type ML<-r: Nat, -c: Nat> is Type:
667	  ML{m: Mat<r, c>, l: List<&2, F32>}
668	
669	def Mat.to_list2(-r: Nat, -c: Nat, al: AL) -> ML<r, c>:
670	  match al:
671	    case AL{d, l}:
672	      ML{Mat{d}, l}
673	
674	# two independent copies
675	
676	def Mat.to_list(+r: Nat, +c: Nat, m: Mat<r, c>) -> ML<r, c>:
677	  match m:
678	    case Mat{d}:
679	      Mat.to_list2(r, c, read_l(Nat.sub(Nat.mul(r, c), 1n), 0, Nil{}, Array.get(F32, d, 0)))
680	
681	type MM2<-r: Nat, -c: Nat> is Type:
682	  MM2{a: Mat<r, c>, b: Mat<r, c>}
683	
684	def Mat.clone2(-r: Nat, -c: Nat, p: Array<F32> & Array<F32>) -> MM2<r, c>:
685	  match p:
686	    case Tuple{x, y}:
687	      MM2{Mat{x}, Mat{y}}
688	
689	# ---- products: C (n x m) = A · B, with 2^par blocks of rows in parallel ----
690	
691	# C = A(n x k) · B(k x m)
692	
693	def Mat.clone(-r: Nat, -c: Nat, m: Mat<r, c>) -> MM2<r, c>:
694	  match m:
695	    case Mat{d}:
696	      Mat.clone2(r, c, Array.clone(F32, d))
697	
698	type MMul<-n: Nat, -k: Nat, -m: Nat> is Type:
699	  MMul{a: Mat<n, k>, b: Mat<k, m>, c: Mat<n, m>}
700	
701	# C = A(n x k) · Bᵀ, with B stored m x k
702	
703	type MMulNT<-n: Nat, -k: Nat, -m: Nat> is Type:
704	  MMulNT{a: Mat<n, k>, b: Mat<m, k>, c: Mat<n, m>}
705	
706	# C = Aᵀ · B, with A stored k x n
707	
708	type MMulTN<-n: Nat, -k: Nat, -m: Nat> is Type:
709	  MMulTN{a: Mat<k, n>, b: Mat<k, m>, c: Mat<n, m>}
710	
711	# ---------------------------------------------------------------------
712	# gemm in tiles of 8 (0.1.8.0): for products with 2 or more rows, A's rows and B's columns are packed once into cells of
713	# 8 F32 (a row of k numbers is ceil(k/8) cells, zeros after the last), so the inner loop reads 8 numbers per array
714	# access instead of one. The order of the additions is that of `dotr`: product p of a dot goes to partial sum p mod 4,
715	# in order, and the four sums are combined as dotr combines them after k steps (its rotation depends on k mod 4). The
716	# padding adds +0 to a sum that starts at +0, which changes nothing, so the results are the same bits as the scalar
717	# loop's. Products with one row (matrix · vector) keep the scalar loop: packing B would cost as much as the product.
718	# ---------------------------------------------------------------------
719	
720	type T8 is Data:
721	  T8{v0: F32, v1: F32, v2: F32, v3: F32, v4: F32, v5: F32, v6: F32, v7: F32}
722	
723	def t8_zero() -> T8:
724	  T8{0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0}
725	
726	def pick0(b: Bool, +v: F32) -> F32:
727	  match b:
728	    case True{}:
729	      v
730	    case False{}:
731	      0.0
732	
733	type PK is Type:
734	  PK{a: Array<F32>, t: Array<T8>}
735	
736	# one cell: the 8 numbers of a at idx, idx + st, ..., those at positions q0 + q >= lim (past the end of the line) as 0
737	def pk_g7(+v0: F32, +v1: F32, +v2: F32, +v3: F32, +v4: F32, +v5: F32, +v6: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
738	  match r:
739	    case Tuple{a, +v}:
740	      PK{a, Array.set(T8, t, o, T8{v0, v1, v2, v3, v4, v5, v6, pick0(U32.is_lt((q0 + 7 : U32), lim), v)})}
741	
742	def pk_g6(+v0: F32, +v1: F32, +v2: F32, +v3: F32, +v4: F32, +v5: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
743	  match r:
744	    case Tuple{a, +v}:
745	      pk_g7(v0, v1, v2, v3, v4, v5, pick0(U32.is_lt((q0 + 6 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 7 : U32) : U32)))
746	
747	def pk_g5(+v0: F32, +v1: F32, +v2: F32, +v3: F32, +v4: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
748	  match r:
749	    case Tuple{a, +v}:
750	      pk_g6(v0, v1, v2, v3, v4, pick0(U32.is_lt((q0 + 5 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 6 : U32) : U32)))
751	
752	def pk_g4(+v0: F32, +v1: F32, +v2: F32, +v3: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
753	  match r:
754	    case Tuple{a, +v}:
755	      pk_g5(v0, v1, v2, v3, pick0(U32.is_lt((q0 + 4 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 5 : U32) : U32)))
756	
757	def pk_g3(+v0: F32, +v1: F32, +v2: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
758	  match r:
759	    case Tuple{a, +v}:
760	      pk_g4(v0, v1, v2, pick0(U32.is_lt((q0 + 3 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 4 : U32) : U32)))
761	
762	def pk_g2(+v0: F32, +v1: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
763	  match r:
764	    case Tuple{a, +v}:
765	      pk_g3(v0, v1, pick0(U32.is_lt((q0 + 2 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 3 : U32) : U32)))
766	
767	def pk_g1(+v0: F32, +q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
768	  match r:
769	    case Tuple{a, +v}:
770	      pk_g2(v0, pick0(U32.is_lt((q0 + 1 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 2 : U32) : U32)))
771	
772	def pk_g0(+q0: U32, +lim: U32, +idx: U32, +st: U32, +o: U32, t: Array<T8>, r: Array<F32> & F32) -> PK:
773	  match r:
774	    case Tuple{a, +v}:
775	      pk_g1(pick0(U32.is_lt((q0 + 0 : U32), lim), v), q0, lim, idx, st, o, t, Array.get(F32, a, (idx + (st * 1 : U32) : U32)))
776	
777	# the cells of one line, cell o.. of t; q0 counts the line's numbers before the cell
778	def pk_line(tl: Nat, +q0: U32, +lim: U32, +base: U32, +st: U32, +o: U32, r: PK) -> PK:
779	  match tl r:
780	    case 0n r:
781	      r
782	    case 1n+q PK{a, t}:
783	      pk_line(q, (q0 + 8 : U32), lim, (base + (st * 8 : U32) : U32), st, (o + 1 : U32), pk_g0(q0, lim, base, st, o, t, Array.get(F32, a, base)))
784	
785	# lines count lines; source line i starts at i * lstep (in a), and goes to cell row o (cells o * tku .. in t)
786	def pk_lines(cnt: Nat, +tk: Nat, +tku: U32, +ku: U32, +i: U32, +o: U32, +lstep: U32, +st: U32, r: PK) -> PK:
787	  match cnt:
788	    case 0n:
789	      r
790	    case 1n+p:
791	      pk_lines(p, tk, tku, ku, (i + 1 : U32), (o + 1 : U32), lstep, st, pk_line(tk, 0, ku, (i * lstep : U32), st, (o * tku : U32), r))
792	
793	def pk_pack(+cnt: Nat, +tk: Nat, +k: Nat, +lstep: U32, +st: U32, a: Array<F32>) -> PK:
794	  pk_lines(cnt, tk, U32.from_nat(tk), U32.from_nat(k), 0, 0, lstep, st, PK{a, Array.new(T8, cap_depth(Nat.mul(cnt, tk)), t8_zero())})
795	
796	# the dot of two lines of cells: tk cells from ia (in a) and ib (in b); ra, rb hold the arrays and the cells at ia, ib,
797	# already read. Product q of a cell goes to sum q mod 4, the first four before the last four, as dotr adds them.
798	def t8_dot(tk: Nat, +ia: U32, +ib: U32, s0: F32, s1: F32, s2: F32, s3: F32, ra: Array<T8> & T8, rb: Array<T8> & T8) -> TD:
799	  match tk ra rb:
800	    case 0n Tuple{a, x} Tuple{b, y}:
801	      TD{a, b, s0, s1, s2, s3}
802	    case 1n+p Tuple{a, T8{x0, x1, x2, x3, x4, x5, x6, x7}} Tuple{b, T8{y0, y1, y2, y3, y4, y5, y6, y7}}:
803	      t8_dot(p, (ia + 1 : U32), (ib + 1 : U32), ((s0 + (x0 * y0 : F32) : F32) + (x4 * y4 : F32) : F32), ((s1 + (x1 * y1 : F32) : F32) + (x5 * y5 : F32) : F32), ((s2 + (x2 * y2 : F32) : F32) + (x6 * y6 : F32) : F32), ((s3 + (x3 * y3 : F32) : F32) + (x7 * y7 : F32) : F32), Array.get(T8, a, (ia + 1 : U32)), Array.get(T8, b, (ib + 1 : U32)))
804	
805	type TD is Type:
806	  TD{a: Array<T8>, b: Array<T8>, s0: F32, s1: F32, s2: F32, s3: F32}
807	
808	# dotr's final sum after k products: the sums sit rotated by k mod 4 when its loop ends
809	def t8_comb(+rot: Nat, +s0: F32, +s1: F32, +s2: F32, +s3: F32) -> F32:
810	  match rot:
811	    case 0n:
812	      ((s0 + s1 : F32) + (s2 + s3 : F32) : F32)
813	    case 1n:
814	      ((s1 + s2 : F32) + (s3 + s0 : F32) : F32)
815	    case 2n:
816	      ((s2 + s3 : F32) + (s0 + s1 : F32) : F32)
817	    case _:
818	      ((s3 + s0 : F32) + (s1 + s2 : F32) : F32)
819	
820	type TR is Type:
821	  TR{a: Array<T8>, b: Array<T8>, x: F32}
822	
823	def t8_fin(+rot: Nat, d: TD) -> TR:
824	  match d:
825	    case TD{a, b, +s0, +s1, +s2, +s3}:
826	      TR{a, b, t8_comb(rot, s0, s1, s2, s3)}
827	
828	def t8_cell(+tk: Nat, +tku: U32, +rot: Nat, +i: U32, +j: U32, a: Array<T8>, b: Array<T8>) -> TR:
829	  t8_fin(rot, t8_dot(tk, (i * tku : U32), (j * tku : U32), 0.0, 0.0, 0.0, 0.0, Array.get(T8, a, (i * tku : U32)), Array.get(T8, b, (j * tku : U32))))
830	
831	type TG is Type:
832	  TG{a: Array<T8>, b: Array<T8>, c: Array<F32>}
833	
834	def t8_set(+ac: Bool, +idx: U32, c: Array<F32>, r: TR) -> TG:
835	  match r:
836	    case TR{a, b, +x}:
837	      TG{a, b, cwr(ac, idx, x, c)}
838	
839	def t8_cols(+ac: Bool, mleft: Nat, +tk: Nat, +tku: U32, +rot: Nat, +i: U32, +j: U32, +cidx: U32, g: TG) -> TG:
840	  match mleft g:
841	    case 0n g:
842	      g
843	    case 1n+p TG{a, b, c}:
844	      t8_cols(ac, p, tk, tku, rot, i, (j + 1 : U32), (cidx + 1 : U32), t8_set(ac, cidx, c, t8_cell(tk, tku, rot, i, j, a, b)))
845	
846	def t8_rows(+ac: Bool, nleft: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, +i: U32, +mu: U32, g: TG) -> TG:
847	  match nleft:
848	    case 0n:
849	      g
850	    case 1n+p:
851	      t8_rows(ac, p, m, tk, tku, rot, (i + 1 : U32), mu, t8_cols(ac, m, tk, tku, rot, i, 0, (i * mu : U32), g))
852	
853	# rows i0 .. i0+cnt-1 of C as a list, in order (the parallel version's leaves)
854	type TL is Type:
855	  TL{a: Array<T8>, b: Array<T8>, out: List<&2, F32>}
856	
857	# cells j.. of row i, m - j of them; r is cell j, already computed
858	def t8_lcols(mleft: Nat, +tk: Nat, +tku: U32, +rot: Nat, +i: U32, +j: U32, out: List<&2, F32>, r: TR) -> TL:
859	  match mleft r:
860	    case 0n TR{a, b, +x}:
861	      TL{a, b, x <> out}
862	    case 1n+p TR{a, b, +x}:
863	      t8_lcols(p, tk, tku, rot, i, (j + 1 : U32), x <> out, t8_cell(tk, tku, rot, i, (j + 1 : U32), a, b))
864	
865	def t8_lrows(nleft: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, +i: U32, l: TL) -> TL:
866	  match nleft l:
867	    case 0n l:
868	      l
869	    case 1n+p TL{a, b, out}:
870	      t8_lrows(p, m, tk, tku, rot, (i + 1 : U32), t8_lcols(Nat.sub(m, 1n), tk, tku, rot, i, 0, out, t8_cell(tk, tku, rot, i, 0, a, b)))
871	
872	def t8_lfin(l: TL) -> List<&2, F32>:
873	  match l:
874	    case TL{a, b, out}:
875	      List.reverse(&2, F32, out)
876	
877	type PKK is Type:
878	  PKK{a: Array<F32>, b: Array<F32>, ta: Array<T8>, tb: Array<T8>}
879	
880	def t8_pk2(pa: PK, pb: PK) -> PKK:
881	  match pa pb:
882	    case PK{a, ta} PK{b, tb}:
883	      PKK{a, b, ta, tb}
884	
885	def t8_g(a: Array<F32>, b: Array<F32>, g: TG) -> G:
886	  match g:
887	    case TG{ta, tb, c}:
888	      G{a, b, c}
889	
890	def t8_out_seq(+ac: Bool, +n: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, c: Array<F32>, p: PKK) -> G:
891	  match p:
892	    case PKK{a, b, ta, tb}:
893	      t8_g(a, b, t8_rows(ac, n, m, tk, tku, rot, 0, U32.from_nat(m), TG{ta, tb, c}))
894	
895	# ---- the parallel path (0.1.9.0): the larger operand is packed into one piece per block, so a block owns its piece;
896	# the other operand is copied once per node of the fork tree (2^d - 1 copies), instead of both at every node ----
897	
898	type PT is Type:
899	  PLeaf{t: Array<T8>}
900	  PNode{l: PT, r: PT}
901	
902	type PKT is Type:
903	  PKT{a: Array<F32>, t: PT}
904	
905	def pkt_leaf(r: PK) -> PKT:
906	  match r:
907	    case PK{a, t}:
908	      PKT{a, PLeaf{t}}
909	
910	def pkt_then(r: PKT, k: Array<F32> -> PT -> PKT) -> PKT:
911	  match r:
912	    case PKT{a, t}:
913	      k(a, t)
914	
915	# lines i .. i+cnt-1 of a, packed into 2^d pieces (halves of the line count, as the fork tree splits them)
916	def pk_tree(+d: Nat, +cnt: Nat, +i: U32, +tk: Nat, +tku: U32, +ku: U32, +lstep: U32, +st: U32, a: Array<F32>) -> PKT:
917	  match d:
918	    case 0n:
919	      pkt_leaf(pk_lines(cnt, tk, tku, ku, i, 0, lstep, st, PK{a, Array.new(T8, cap_depth(Nat.mul(cnt, tk)), t8_zero())}))
920	    case 1n+q:
921	      pkt_then(pk_tree(q, Nat.div(cnt, 2n), i, tk, tku, ku, lstep, st, a), a2 => l => pkt_then(pk_tree(q, Nat.sub(cnt, Nat.div(cnt, 2n)), (i + U32.from_nat(Nat.div(cnt, 2n)) : U32), tk, tku, ku, lstep, st, a2), a3 => r => PKT{a3, PNode{l, r}}))
922	
923	def t8_with2(-R: Type, p: Array<T8> & Array<T8>, k: Array<T8> -> Array<T8> -> R) -> R:
924	  match p:
925	    case Tuple{x, y}:
926	      k(x, y)
927	
928	# split by rows of C: the pieces are A's rows, B is shared; the result is C's rows in order
929	def t8_rpar(t: PT, +cnt: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, b: Array<T8>) -> List<&2, F32>:
930	  match t:
931	    case PLeaf{a}:
932	      t8_lfin(t8_lrows(cnt, m, tk, tku, rot, 0, TL{a, b, Nil{}}))
933	    case PNode{l, r}:
934	      t8_with2(List<&2, F32>, Array.clone(T8, b), b1 => b2 => (
935	        x y = t8_rpar(l, Nat.div(cnt, 2n), m, tk, tku, rot, b1) t8_rpar(r, Nat.sub(cnt, Nat.div(cnt, 2n)), m, tk, tku, rot, b2)
936	        List.append(&2, F32, x, y)))
937	
938	# a block of C's columns j0 .. j0+w-1 for every row, row by row
939	type CB is Data:
940	  CB{j0: U32, w: Nat, xs: List<&2, F32>}
941	
942	# split by columns of C: the pieces are B's columns, A is shared
943	def t8_cpar(t: PT, +cnt: Nat, +j0: U32, +n: Nat, +tk: Nat, +tku: U32, +rot: Nat, a: Array<T8>) -> List<&2, CB>:
944	  match t:
945	    case PLeaf{b}:
946	      [CB{j0, cnt, t8_lfin(t8_lrows(n, cnt, tk, tku, rot, 0, TL{a, b, Nil{}}))}]
947	    case PNode{l, r}:
948	      t8_with2(List<&2, CB>, Array.clone(T8, a), a1 => a2 => (
949	        x y = t8_cpar(l, Nat.div(cnt, 2n), j0, n, tk, tku, rot, a1) t8_cpar(r, Nat.sub(cnt, Nat.div(cnt, 2n)), (j0 + U32.from_nat(Nat.div(cnt, 2n)) : U32), n, tk, tku, rot, a2)
950	        List.append(&2, CB, x, y)))
951	
952	type RW is Type:
953	  RW{c: Array<F32>, xs: List<&2, F32>}
954	
955	# w numbers of xs into c from idx; what is left of xs comes back
956	def cb_row(+ac: Bool, w: Nat, +idx: U32, c: Array<F32>, xs: List<&2, F32>) -> RW:
957	  match w xs:
958	    case 1n+p Con{+h, t}:
959	      cb_row(ac, p, (idx + 1 : U32), cwr(ac, idx, h, c), t)
960	    case _ _:
961	      RW{c, xs}
962	
963	def cb_rows(+ac: Bool, n: Nat, +i: U32, +j0: U32, +w: Nat, +mu: U32, r: RW) -> Array<F32>:
964	  match n r:
965	    case 0n RW{c, xs}:
966	      c
967	    case 1n+p RW{c, xs}:
968	      cb_rows(ac, p, (i + 1 : U32), j0, w, mu, cb_row(ac, w, ((i * mu : U32) + j0 : U32), c, xs))
969	
970	def cb_write(+ac: Bool, bs: List<&2, CB>, +n: Nat, +mu: U32, c: Array<F32>) -> Array<F32>:
971	  match bs:
972	    case Nil{}:
973	      c
974	    case Con{CB{+j0, +w, xs}, t}:
975	      cb_write(ac, t, n, mu, cb_rows(ac, n, 0, j0, w, mu, RW{c, xs}))
976	
977	def t8_pr2(+ac: Bool, +n: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, c: Array<F32>, ra: PKT, rb: PK) -> G:
978	  match ra rb:
979	    case PKT{a, t} PK{b, tb}:
980	      G{a, b, write_la(ac, t8_rpar(t, n, m, tk, tku, rot, tb), 0, c)}
981	
982	def t8_pc2(+ac: Bool, +n: Nat, +m: Nat, +tk: Nat, +tku: U32, +rot: Nat, c: Array<F32>, ra: PK, rb: PKT) -> G:
983	  match ra rb:
984	    case PK{a, ta} PKT{b, t}:
985	      G{a, b, cb_write(ac, t8_cpar(t, m, 0, n, tk, tku, rot, ta), n, U32.from_nat(m), c)}
986	
987	# 2^d blocks along the larger of n (rows of C, pieces of A) and m (columns of C, pieces of B)
988	def t8_par2(+ac: Bool, byrows: Bool, d: Nat, +n: Nat, +m: Nat, +k: Nat, +tk: Nat, +tku: U32, +rot: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>, c: Array<F32>) -> G:
989	  match byrows:
990	    case True{}:
991	      t8_pr2(ac, n, m, tk, tku, rot, c, pk_tree(d, n, 0, tk, tku, U32.from_nat(k), arow, sa, a), pk_pack(m, tk, k, bcol, sb, b))
992	    case False{}:
993	      t8_pc2(ac, n, m, tk, tku, rot, c, pk_pack(n, tk, k, arow, sa, a), pk_tree(d, m, 0, tk, tku, U32.from_nat(k), bcol, sb, b))
994	
995	def gemm_t8b(+ac: Bool, d: Nat, +n: Nat, +m: Nat, +k: Nat, +tk: Nat, +tku: U32, +rot: Nat, +arow: U32, +sa: U32, +sb: U32, +bcol: U32, a: Array<F32>, b: Array<F32>, c: Array<F32>) -> G:
996	  match d:
997	    case 0n:
998	      t8_out_seq(ac, n, m, tk, tku, rot, c, t8_pk2(pk_pack(n, tk, k, arow, sa, a), pk_pack(m, tk, k, bcol, sb, b)))
999	    case 1n+q:
1000	      t8_par2(ac, Nat.is_le(m, n), 1n+q, n, m, k, tk, tku, rot, arow, sa, sb, bcol, a, b, c)
1001	
1002	# C (n x m) = A · B (or C + A · B when ac) in cells of 8, sequential (d = 0) or with 2^d blocks of rows in parallel; A
1003	# and B come back intact
1004	def gemm_t8_ac(+ac: 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:
1005	  gemm_t8b(ac, d, n, m, k, Nat.div(Nat.add(k, 7n), 8n), U32.from_nat(Nat.div(Nat.add(k, 7n), 8n)), Nat.mod(k, 4n), arow, sa, sb, bcol, a, b, c)
1006	
1007	def gemm_t8(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:
1008	  gemm_t8_ac(False{}, d, n, m, k, arow, sa, sb, bcol, a, b, c)
1009	
1010	# one row (matrix · vector): the scalar loop, by columns in parallel when d > 0; two or more rows: cells of 8
1011	def gemm_any3(+ac: Bool, one: 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:
1012	  match one d:
1013	    case True{} 0n:
1014	      gemm_ac(ac, n, m, k, arow, sa, sb, bcol, a, b, c)
1015	    case True{} 1n+q:
1016	      gemm_par_cols(ac, 1n+q, m, k, sa, sb, bcol, a, b, c)
1017	    case False{} d:
1018	      gemm_t8_ac(ac, d, n, m, k, arow, sa, sb, bcol, a, b, c)
1019	
1020	def gemm_any2(+ac: 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:
1021	  gemm_any3(ac, Nat.is_le(n, 1n), d, n, m, k, arow, sa, sb, bcol, a, b, c)
1022	
1023	def gemm_any(+ac: 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:
1024	  gemm_any2(ac, d, n, m, k, arow, sa, sb, bcol, a, b, c)
1025	
1026	def mmul_fin(-n: Nat, -k: Nat, -m: Nat, g: G) -> MMul<n, k, m>:
1027	  match g:
1028	    case G{a, b, c}:
1029	      MMul{Mat{a}, Mat{b}, Mat{c}}
1030	
1031	def mmul_nt_fin(-n: Nat, -k: Nat, -m: Nat, g: G) -> MMulNT<n, k, m>:
1032	  match g:
1033	    case G{a, b, c}:
1034	      MMulNT{Mat{a}, Mat{b}, Mat{c}}
1035	
1036	def mmul_tn_fin(-n: Nat, -k: Nat, -m: Nat, g: G) -> MMulTN<n, k, m>:
1037	  match g:
1038	    case G{a, b, c}:
1039	      MMulTN{Mat{a}, Mat{b}, Mat{c}}
1040	
1041	def mm_a(+n: Nat, +k: Nat, +m: Nat, d: Nat, a: Array<F32>, b: Array<F32>) -> MMul<n, k, m>:
1042	  mmul_fin(n, k, m, gemm_any(False{}, d, n, m, k, U32.from_nat(k), 1, U32.from_nat(m), 1, a, b, Array.new(F32, cap_depth(Nat.mul(n, m)), 0.0)))
1043	
1044	# C = A · B   (n x k) · (k x m); par = log2 of the number of parallel blocks (0 = sequential)
1045	
1046	def Mat.matmul(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<n, k>, b: Mat<k, m>) -> MMul<n, k, m>:
1047	  match a b:
1048	    case Mat{x} Mat{y}:
1049	      mm_a(n, k, m, par, x, y)
1050	
1051	# C + A · B, into C (n x m); A and B come back with the result, as Mat.matmul returns them. Each cell of A · B is
1052	# computed as Mat.matmul computes it and added once to C's cell: the same bits as Mat.add(c, Mat.matmul(a, b)'s c),
1053	# without allocating the product or walking it a second time.
1054	
1055	def Mat.matmul_acc(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<n, k>, b: Mat<k, m>, c: Mat<n, m>) -> MMul<n, k, m>:
1056	  match a b c:
1057	    case Mat{x} Mat{y} Mat{z}:
1058	      mmul_fin(n, k, m, gemm_any(True{}, par, n, m, k, U32.from_nat(k), 1, U32.from_nat(m), 1, x, y, z))
1059	
1060	def mm_nt(+n: Nat, +k: Nat, +m: Nat, d: Nat, a: Array<F32>, b: Array<F32>) -> MMulNT<n, k, m>:
1061	  mmul_nt_fin(n, k, m, gemm_any(False{}, d, n, m, k, U32.from_nat(k), 1, 1, U32.from_nat(k), a, b, Array.new(F32, cap_depth(Nat.mul(n, m)), 0.0)))
1062	
1063	# C = A · Bᵀ   (n x k) · (m x k)ᵀ: for weights stored with one row per output
1064	
1065	def Mat.matmul_nt(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<n, k>, b: Mat<m, k>) -> MMulNT<n, k, m>:
1066	  match a b:
1067	    case Mat{x} Mat{y}:
1068	      mm_nt(n, k, m, par, x, y)
1069	
1070	# C + A · Bᵀ, into C (n x m)
1071	
1072	def Mat.matmul_nt_acc(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<n, k>, b: Mat<m, k>, c: Mat<n, m>) -> MMulNT<n, k, m>:
1073	  match a b c:
1074	    case Mat{x} Mat{y} Mat{z}:
1075	      mmul_nt_fin(n, k, m, gemm_any(True{}, par, n, m, k, U32.from_nat(k), 1, 1, U32.from_nat(k), x, y, z))
1076	
1077	def mm_tn(+n: Nat, +k: Nat, +m: Nat, d: Nat, a: Array<F32>, b: Array<F32>) -> MMulTN<n, k, m>:
1078	  mmul_tn_fin(n, k, m, gemm_any(False{}, d, n, m, k, 1, U32.from_nat(n), U32.from_nat(m), 1, a, b, Array.new(F32, cap_depth(Nat.mul(n, m)), 0.0)))
1079	
1080	# C = Aᵀ · B   (k x n)ᵀ · (k x m): weight gradient, X^T · dY
1081	
1082	def Mat.matmul_tn(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<k, n>, b: Mat<k, m>) -> MMulTN<n, k, m>:
1083	  match a b:
1084	    case Mat{x} Mat{y}:
1085	      mm_tn(n, k, m, par, x, y)
1086	
1087	# C + Aᵀ · B, into C (n x m): a weight gradient added into the gradient it accumulates, dW += Xᵀ · dY
1088	
1089	def Mat.matmul_tn_acc(+n: Nat, +k: Nat, +m: Nat, par: Nat, a: Mat<k, n>, b: Mat<k, m>, c: Mat<n, m>) -> MMulTN<n, k, m>:
1090	  match a b c:
1091	    case Mat{x} Mat{y} Mat{z}:
1092	      mmul_tn_fin(n, k, m, gemm_any(True{}, par, n, m, k, 1, U32.from_nat(n), U32.from_nat(m), 1, x, y, z))
1093	
1094	# ---- element-wise and training operations ----
1095	
1096	# adds the bias (one row, m numbers) to each row of C (n x m)
1097	
1098	type MBias<-n: Nat, -m: Nat> is Type:
1099	  MBias{c: Mat<n, m>, b: Mat<1n, m>}
1100	
1101	def add_row2(-n: Nat, -m: Nat, +nn: Nat, +mm: Nat, cd: Array<F32>, al: AL) -> MBias<n, m>:
1102	  match al:
1103	    case AL{bd, bl}:
1104	      MBias{Mat{bias_rows(nn, 0, U32.from_nat(mm), bl, cd)}, Mat{bd}}
1105	
1106	def Mat.add_row(+n: Nat, +m: Nat, c: Mat<n, m>, b: Mat<1n, m>) -> MBias<n, m>:
1107	  match c b:
1108	    case Mat{cd} Mat{bd}:
1109	      add_row2(n, m, n, m, cd, read_l(Nat.sub(m, 1n), 0, Nil{}, Array.get(F32, bd, 0)))
1110	
1111	# pair of matrices of the same shape (the result of an operation that reads two operands)
1112	
1113	type MPair<-r: Nat, -c: Nat> is Type:
1114	  MPair{a: Mat<r, c>, b: Mat<r, c>}
1115	
1116	def mpair_fin(-r: Nat, -c: Nat, p: P2) -> MPair<r, c>:
1117	  match p:
1118	    case P2{a, b}:
1119	      MPair{Mat{a}, Mat{b}}
1120	
1121	def relu_fin(-r: Nat, -c: Nat, d: Array<F32>) -> Mat<r, c>:
1122	  Mat{d}
1123	
1124	def Mat.relu(+r: Nat, +c: Nat, a: Mat<r, c>) -> Mat<r, c>:
1125	  match a:
1126	    case Mat{d}:
1127	      relu_fin(r, c, relu_l(Nat.mul(r, c), 0, Array.get(F32, d, 0)))
1128	
1129	# (dy * (h > 0), h): the gradient that passes through the relu
1130	
1131	def Mat.relu_bwd(+r: Nat, +c: Nat, dy: Mat<r, c>, h: Mat<r, c>) -> MPair<r, c>:
1132	  match dy h:
1133	    case Mat{d} Mat{x}:
1134	      mpair_fin(r, c, mask_l(Nat.mul(r, c), 0, Array.get(F32, d, 0), Array.get(F32, x, 0)))
1135	
1136	# (w - lr * dw, dw): one SGD step
1137	
1138	def Mat.sgd(+r: Nat, +c: Nat, +lr: F32, w: Mat<r, c>, dw: Mat<r, c>) -> MPair<r, c>:
1139	  match w dw:
1140	    case Mat{x} Mat{y}:
1141	      mpair_fin(r, c, sgd_l(Nat.mul(r, c), 0, lr, Array.get(F32, x, 0), Array.get(F32, y, 0)))
1142	
1143	# (a + b, b): element-wise sum (a - (-1)*b is exactly a + b)
1144	
1145	def Mat.add(+r: Nat, +c: Nat, a: Mat<r, c>, b: Mat<r, c>) -> MPair<r, c>:
1146	  match a b:
1147	    case Mat{x} Mat{y}:
1148	      mpair_fin(r, c, sgd_l(Nat.mul(r, c), 0, (0.0 - 1.0 : F32), Array.get(F32, x, 0), Array.get(F32, y, 0)))
1149	
1150	# sum of each column (n x m -> 1 x m), returning the matrix
1151	
1152	type MColSum<-n: Nat, -m: Nat> is Type:
1153	  MColSum{a: Mat<n, m>, s: Mat<1n, m>}
1154	
1155	def colsum_fin(-n: Nat, -m: Nat, g: G) -> MColSum<n, m>:
1156	  match g:
1157	    case G{ones, a, s}:
1158	      MColSum{Mat{a}, Mat{s}}
1159	
1160	def Mat.col_sums(+n: Nat, +m: Nat, a: Mat<n, m>) -> MColSum<n, m>:
1161	  match a:
1162	    case Mat{d}:
1163	      colsum_fin(n, m, gemm(1n, m, n, 0, 1, U32.from_nat(m), 1, Array.new(F32, cap_depth(n), 1.0), d, Array.new(F32, cap_depth(m), 0.0)))
1164	
1165	# s + the sum of each column, into s (1 x m): a bias gradient added into its accumulator, with the bits of
1166	# Mat.add(s, Mat.col_sums(a)'s s)
1167	
1168	def Mat.col_sums_acc(+n: Nat, +m: Nat, a: Mat<n, m>, s: Mat<1n, m>) -> MColSum<n, m>:
1169	  match a s:
1170	    case Mat{d} Mat{z}:
1171	      colsum_fin(n, m, gemm_ac(True{}, 1n, m, n, 0, 1, U32.from_nat(m), 1, Array.new(F32, cap_depth(n), 1.0), d, z))
1172	
1173	# mean cross-entropy and its gradient on the logits: (softmax - one-hot) / n.
1174	# labels has one entry per row (n); the gradient replaces the logits.
1175	
1176	type MCE<-n: Nat, -c: Nat> is Type:
1177	  MCE{loss: F32, grad: Mat<n, c>}
1178	
1179	def ce_fin(-n: Nat, -c: Nat, +nf: F32, r: L2) -> MCE<n, c>:
1180	  match r:
1181	    case L2{loss, d}:
1182	      MCE{(loss / nf : F32), Mat{d}}
1183	
1184	def Mat.softmax_ce(+n: Nat, +c: Nat, z: Mat<n, c>, labels: List<&2, Nat>) -> MCE<n, c>:
1185	  match z:
1186	    case Mat{d}:
1187	      ce_fin(n, c, F32.from_nat(n), ce_rows(labels, Nat.sub(c, 1n), U32.from_nat(c), F32.from_nat(n), 0, L2{0.0, d}))
1188	
1189	# argmax hits per row against labels
1190	
1191	type MHits<-n: Nat, -c: Nat> is Type:
1192	  MHits{z: Mat<n, c>, hits: Nat}
1193	
1194	def hits_fin(-n: Nat, -c: Nat, r: CR) -> MHits<n, c>:
1195	  match r:
1196	    case CR{d, k}:
1197	      MHits{Mat{d}, k}
1198	
1199	def Mat.count_correct(+n: Nat, +c: Nat, z: Mat<n, c>, labels: List<&2, Nat>) -> MHits<n, c>:
1200	  match z:
1201	    case Mat{d}:
1202	      hits_fin(n, c, count_rows(labels, Nat.sub(c, 1n), U32.from_nat(c), 0, CR{d, 0n}))
1203	
1204	# a row as a list (returning the matrix) and the other way around
1205	
1206	type MRow<-r: Nat, -c: Nat> is Type:
1207	  MRow{m: Mat<r, c>, row: List<&2, F32>}
1208	
1209	def row_fin(-r: Nat, -c: Nat, al: AL) -> MRow<r, c>:
1210	  match al:
1211	    case AL{d, l}:
1212	      MRow{Mat{d}, l}
1213	
1214	def Mat.read_row(+r: Nat, +c: Nat, m: Mat<r, c>, +i: U32) -> MRow<r, c>:
1215	  match m:
1216	    case Mat{d}:
1217	      row_fin(r, c, read_l(Nat.sub(c, 1n), (i * U32.from_nat(c) : U32), Nil{}, Array.get(F32, d, (i * U32.from_nat(c) : U32))))
1218	
1219	def Mat.write_row(-r: Nat, +c: Nat, m: Mat<r, c>, +i: U32, xs: List<&2, F32>) -> Mat<r, c>:
1220	  match m:
1221	    case Mat{d}:
1222	      Mat{write_l(xs, (i * U32.from_nat(c) : U32), d)}
1223	
1224	# ---- variants that check the number of labels ----
1225	
1226	# does the list of labels have exactly n entries (one per row)?
1227	def labels_len_is(xs: List<&2, Nat>, n: Nat) -> Bool:
1228	  match xs n:
1229	    case Nil{} 0n:
1230	      True{}
1231	    case Con{h, t} 1n+p:
1232	      labels_len_is(t, p)
1233	    case _ _:
1234	      False{}
1235	
1236	def ce_checked(ok: Bool, +n: Nat, +c: Nat, z: Mat<n, c>, labels: List<&2, Nat>) -> Maybe<&1, MCE<n, c>>:
1237	  match ok:
1238	    case True{}:
1239	      Some{Mat.softmax_ce(n, c, z, labels)}
1240	    case False{}:
1241	      None{}
1242	
1243	# like Mat.softmax_ce, but returns None unless labels has exactly n entries
1244	def Mat.softmax_ce_checked(+n: Nat, +c: Nat, z: Mat<n, c>, +labels: List<&2, Nat>) -> Maybe<&1, MCE<n, c>>:
1245	  ce_checked(labels_len_is(labels, n), n, c, z, labels)
1246	
1247	def hits_checked(ok: Bool, +n: Nat, +c: Nat, z: Mat<n, c>, labels: List<&2, Nat>) -> Maybe<&1, MHits<n, c>>:
1248	  match ok:
1249	    case True{}:
1250	      Some{Mat.count_correct(n, c, z, labels)}
1251	    case False{}:
1252	      None{}
1253	
1254	# like Mat.count_correct, but returns None unless labels has exactly n entries
1255	def Mat.count_correct_checked(+n: Nat, +c: Nat, z: Mat<n, c>, +labels: List<&2, Nat>) -> Maybe<&1, MHits<n, c>>:
1256	  hits_checked(labels_len_is(labels, n), n, c, z, labels)
1257	
1258	# ---------------------------------------------------------------------
1259	# Bands<r, c>: a matrix cut into bands of rows, for matrix · vector in parallel
1260	# without copying the weights.
1261	#
1262	# Mat.matmul_nt with n = 1 can only run in parallel by cloning the whole weight
1263	# matrix for every task, and in matrix · vector each weight is read once, so the
1264	# copies cost more than the products (NOTES.md, exp. 9). Bands keeps each band in
1265	# its own Array: a task takes its band and nothing is copied except the input vector.
1266	#
1267	# A node with r rows has children with half(r) and r - half(r) rows. The split is
1268	# part of the type, so the row count of every band follows from r, and the law
1269	# half_cover says that the two halves always cover the r rows exactly.
1270	# ---------------------------------------------------------------------
1271	
1272	# n / 2 rounded down. A tail loop with an accumulator: a non-tail recursion here would put a
1273	# continuation on every node of the band tree and keep the bands from running in parallel.
1274	def half.go(n: Nat, acc: Nat) -> Nat:
1275	  match n:
1276	    case 0n:
1277	      acc
1278	    case 1n+p:
1279	      match p:
1280	        case 0n:
1281	          acc
1282	        case 1n+q:
1283	          half.go(q, 1n+acc)
1284	
1285	def half(n: Nat) -> Nat:
1286	  half.go(n, 0n)
1287	
1288	# a <= a
1289	def leb_refl(+a: Nat) -> {True{} == leb(a, a) : Bool}:
1290	  match a:
1291	    case 0n:
1292	      {==}
1293	    case 1n+p:
1294	      leb_refl(p)
1295	
1296	# 1 + (a + b) == a + (1 + b)
1297	def add_succ_r(+a: Nat, -b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:
1298	  match a:
1299	    case 0n:
1300	      {==}
1301	    case 1n+p:
1302	      %add_succ_r(p, b) : {2n+Nat.add(p, b) == 1n+_ : Nat}
1303	      {==}
1304	
1305	# a + 0 == a
1306	def add_zero_r(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
1307	  match a:
1308	    case 0n:
1309	      {==}
1310	    case 1n+p:
1311	      %add_zero_r(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
1312	      {==}
1313	
1314	# half.go(n, acc) <= n + acc
1315	def half_go_le(+n: Nat, +acc: Nat) -> {True{} == leb(half.go(n, acc), Nat.add(n, acc)) : Bool}:
1316	  match n:
1317	    case 0n:
1318	      leb_refl(acc)
1319	    case 1n+p:
1320	      match p:
1321	        case 0n:
1322	          leb_succ(acc, acc, leb_refl(acc))
1323	        case 1n+q:
1324	          %Equal.sym(Nat, 1n+Nat.add(q, acc), Nat.add(q, 1n+acc), add_succ_r(q, acc)) : {True{} == leb(half.go(q, 1n+acc), 1n+_) : Bool}
1325	          leb_succ(half.go(q, 1n+acc), Nat.add(q, 1n+acc), half_go_le(q, 1n+acc))
1326	
1327	# half(n) <= n
1328	def half_le(+n: Nat) -> {True{} == leb(half(n), n) : Bool}:
1329	  %add_zero_r(n) : {True{} == leb(half(n), _) : Bool}
1330	  half_go_le(n, 0n)
1331	
1332	# a <= r  ->  r == a + (r - a)
1333	def add_sub(+a: Nat, +r: Nat, e: {True{} == leb(a, r) : Bool}) -> {r == Nat.add(a, Nat.sub(r, a)) : Nat}:
1334	  match a r:
1335	    case 0n 0n:
1336	      {==}
1337	    case 0n 1n+q:
1338	      {==}
1339	    case 1n+p 0n:
1340	      %e : BD(_, Unit, {0n == Nat.add(1n+p, Nat.sub(0n, 1n+p)) : Nat})
1341	      Unit{}
1342	    case 1n+p 1n+q:
1343	      %add_sub(p, q, e) : {1n+q == 1n+_ : Nat}
1344	      {==}
1345	
1346	# LAW (half_cover): the two bands of a node, half(r) rows and r - half(r) rows,
1347	# add up to exactly r rows: no row is lost and none is counted twice.
1348	law half_cover:
1349	  for +n: Nat
1350	  {n == Nat.add(half(n), Nat.sub(n, half(n))) : Nat}
1351	
1352	def half_cover(n):
1353	  add_sub(half(n), n, half_le(n))
1354	
1355	type Bands<-r: Nat, -c: Nat> is Type:
1356	  BLeaf{m: Mat<r, c>}
1357	  BNode{x: Bands<half(r), c>, y: Bands<Nat.sub(r, half(r)), c>}
1358	
1359	# r x c of zeros in 2^d bands (d = 0: a single band, the same as a Mat)
1360	def Bands.zeros(+d: Nat, +r: Nat, +c: Nat) -> Bands<r, c>:
1361	  match d:
1362	    case 0n:
1363	      BLeaf{Mat.zeros(r, c)}
1364	    case 1n+q:
1365	      BNode{Bands.zeros(q, half(r), c), Bands.zeros(q, Nat.sub(r, half(r)), c)}
1366	
1367	# the row counts of the two bands follow the row count of the node: if rr == r at run
1368	# time, the same holds for both halves (the bands carry r only in their type)
1369	def eq_half(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {half(a) == half(b) : Nat}:
1370	  %e : {half(a) == half(_) : Nat}
1371	  {==}
1372	
1373	def eq_rest(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.sub(a, half(a)) == Nat.sub(b, half(b)) : Nat}:
1374	  %e : {Nat.sub(a, half(a)) == Nat.sub(_, half(_)) : Nat}
1375	  {==}
1376	
1377	# does a block of n numbers starting at flat index i end before the second band of a
1378	# node with r rows? does it start in the second band?
1379	def bfill_l(+r: Nat, +c: Nat, +i: Nat, +n: Nat) -> Bool:
1380	  Nat.is_le(Nat.add(i, n), Nat.mul(half(r), c))
1381	
1382	def bfill_r(+r: Nat, +c: Nat, +i: Nat) -> Bool:
1383	  Nat.is_le(Nat.mul(half(r), c), i)
1384	
1385	# writes the first n numbers of xs at index i (and nothing past them)
1386	def fill_n(n: Nat, xs: List<&2, F32>, +i: U32, a: Array<F32>) -> Array<F32>:
1387	  match n xs:
1388	    case 1n+p Con{h, t}:
1389	      fill_n(p, t, (i + 1 : U32), Array.set(F32, a, i, h))
1390	    case _ _:
1391	      a
1392	
1393	def fill_band(-r: Nat, -c: Nat, n: Nat, xs: List<&2, F32>, +i: U32, m: Mat<r, c>) -> Mat<r, c>:
1394	  match m:
1395	    case Mat{d}:
1396	      Mat{fill_n(n, xs, i, d)}
1397	
1398	# writes the first n numbers of xs at flat index i; l and rt say which bands they touch
1399	# (bfill_l, bfill_r); rr is the row count r at run time. A block that crosses into the second
1400	# band is not copied: the first band writes only its part, the second gets the rest by List.drop.
1401	def bfill(+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>:
1402	  match b l rt:
1403	    case BLeaf{m} _ _:
1404	      BLeaf{fill_band(r, c, n, xs, U32.from_nat(i), m)}
1405	    case BNode{x, y} True{} _:
1406	      BNode{bfill(c, half(r), x, bfill_l(half(rr), c, i, n), bfill_r(half(rr), c, i), half(rr), eq_half(rr, r, e), i, n, xs), y}
1407	    case BNode{x, y} False{} True{}:
1408	      BNode{x, bfill(c, Nat.sub(r, half(r)), y, bfill_l(Nat.sub(rr, half(rr)), c, Nat.sub(i, Nat.mul(half(rr), c)), n), bfill_r(Nat.sub(rr, half(rr)), c, Nat.sub(i, Nat.mul(half(rr), c))), Nat.sub(rr, half(rr)), eq_rest(rr, r, e), Nat.sub(i, Nat.mul(half(rr), c)), n, xs)}
1409	    case BNode{x, y} False{} False{}:
1410	      BNode{bfill(c, half(r), x, bfill_l(half(rr), c, i, Nat.sub(Nat.mul(half(rr), c), i)), bfill_r(half(rr), c, i), half(rr), eq_half(rr, r, e), i, Nat.sub(Nat.mul(half(rr), c), i), xs), bfill(c, Nat.sub(r, half(r)), y, bfill_l(Nat.sub(rr, half(rr)), c, 0n, Nat.sub(n, Nat.sub(Nat.mul(half(rr), c), i))), bfill_r(Nat.sub(rr, half(rr)), c, 0n), Nat.sub(rr, half(rr)), eq_rest(rr, r, e), 0n, Nat.sub(n, Nat.sub(Nat.mul(half(rr), c), i)), List.drop(&2, F32, xs, Nat.sub(Nat.mul(half(rr), c), i)))}
1411	
1412	def bfill_top(ok: Bool, +r: Nat, +c: Nat, b: Bands<r, c>, +i: Nat, +n: Nat, +xs: List<&2, F32>) -> Bands<r, c>:
1413	  match ok:
1414	    case True{}:
1415	      bfill(c, r, b, bfill_l(r, c, i, n), bfill_r(r, c, i), r, {==}, i, n, xs)
1416	    case False{}:
1417	      bfill(c, r, b, bfill_l(r, c, i, Nat.sub(Nat.mul(r, c), i)), bfill_r(r, c, i), r, {==}, i, Nat.sub(Nat.mul(r, c), i), xs)
1418	
1419	# writes the n numbers of xs into b starting at flat index i (row-major, as Mat.fill_at);
1420	# numbers past r*c are dropped. For loading a large matrix block by block.
1421	def Bands.fill_at(+r: Nat, +c: Nat, +i: Nat, +n: Nat, +xs: List<&2, F32>, b: Bands<r, c>) -> Bands<r, c>:
1422	  bfill_top(Nat.is_le(Nat.add(i, n), Nat.mul(r, c)), r, c, b, i, n, xs)
1423	
1424	# ---- y = B · x for B with r rows of c numbers (a weight matrix stored out x in) ----
1425	
1426	# B (intact) and y = B · x, typed like Mat.matmul_nt: x is 1 x c, y is 1 x r
1427	type BV<-r: Nat, -c: Nat> is Type:
1428	  BV{b: Bands<r, c>, y: Mat<1n, r>}
1429	
1430	# the bands and y as a list in row order (the result of Bands.matvec_l)
1431	type BL<-r: Nat, -c: Nat> is Type:
1432	  BL{b: Bands<r, c>, y: List<&2, F32>}
1433	
1434	def bv_g2(-r: Nat, -c: Nat, w: Array<F32>, al: AL) -> BL<r, c>:
1435	  match al:
1436	    case AL{d, l}:
1437	      BL{BLeaf{Mat{w}}, l}
1438	
1439	# the band's 1 + m rows came out in an Array (one number per row); read them back as a list
1440	def bv_g(-r: Nat, -c: Nat, +m: Nat, g: G) -> BL<r, c>:
1441	  match g:
1442	    case G{a, b, y}:
1443	      bv_g2(r, c, b, read_l(m, 0, Nil{}, Array.get(F32, y, 0)))
1444	
1445	# the rows of one band, one dot product each, with the gemm of Mat.matmul_nt (n = 1), so the
1446	# results are identical. Writing the results into an Array and reading them back is faster than
1447	# building the list row by row (NOTES.md, exp. 14).
1448	def bv_gemm(-r: Nat, +c: Nat, rows: Nat, +rr: Nat, x: Array<F32>, w: Array<F32>) -> BL<r, c>:
1449	  match rows:
1450	    case 0n:
1451	      BL{BLeaf{Mat{w}}, Nil{}}
1452	    case 1n+p:
1453	      bv_g(r, c, p, gemm(1n, rr, c, U32.from_nat(c), 1, 1, U32.from_nat(c), x, w, Array.new(F32, cap_depth(rr), 0.0)))
1454	
1455	def bv_mat(-r: Nat, +c: Nat, +rr: Nat, x: Array<F32>, m: Mat<r, c>) -> BL<r, c>:
1456	  match m:
1457	    case Mat{w}:
1458	      bv_gemm(r, c, rr, rr, x, w)
1459	
1460	def bv_join(-r: Nat, -c: Nat, p: BL<half(r), c>, q: BL<Nat.sub(r, half(r)), c>) -> BL<r, c>:
1461	  match p q:
1462	    case BL{bx, yx} BL{by, yy}:
1463	      BL{BNode{bx, by}, List.append(&2, F32, yx, yy)}
1464	
1465	# the two bands of a node run in parallel, each with its own copy of x (c numbers);
1466	# xp is a pair of copies of x (a leaf uses one). xp comes after the erased e: up to Bend 2.0.36 an erased
1467	# parameter at the end of the list turned the parallel let into two sequential calls (NOTES.md, exp. 11; fixed in
1468	# 2.0.37 by bendlang/bend#1377). The order is kept, and harmless.
1469	def bmv(+c: Nat, -r: Nat, b: Bands<r, c>, +rr: Nat, -e: {rr == r : Nat}, xp: Array<F32> & Array<F32>) -> BL<r, c>:
1470	  match b xp:
1471	    case BLeaf{m} Tuple{x, x2}:
1472	      bv_mat(r, c, rr, x, m)
1473	    case BNode{bx, by} Tuple{x1, x2}:
1474	      p q = bmv(c, half(r), bx, half(rr), eq_half(rr, r, e), Array.clone(F32, x1)) bmv(c, Nat.sub(r, half(r)), by, Nat.sub(rr, half(rr)), eq_rest(rr, r, e), Array.clone(F32, x2))
1475	      bv_join(r, c, p, q)
1476	
1477	def bv_fin(+r: Nat, -c: Nat, bl: BL<r, c>) -> BV<r, c>:
1478	  match bl:
1479	    case BL{b, y}:
1480	      BV{b, Mat.from_list(1n, r, y)}
1481	
1482	# 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).
1483	# The same product as Mat.matmul_nt(1n, c, r, ..), and the same numbers, bit for bit.
1484	def Bands.matvec(+r: Nat, +c: Nat, b: Bands<r, c>, x: Mat<1n, c>) -> BV<r, c>:
1485	  match x:
1486	    case Mat{xa}:
1487	      bv_fin(r, c, bmv(c, r, b, r, {==}, Array.clone(F32, xa)))
1488	
1489	# the same product with x and y as lists (x: c numbers, y: r numbers in row order), without the
1490	# Mat conversions of Bands.matvec: for callers that already hold the vector as a list
1491	def Bands.matvec_l(+r: Nat, +c: Nat, b: Bands<r, c>, +x: List<&2, F32>) -> BL<r, c>:
1492	  bmv(c, r, b, r, {==}, Array.clone(F32, fill_list(x, 0, Array.new(F32, cap_depth(c), 0.0))))
1493	
1494	# ---- reading rows and the whole matrix ----
1495	
1496	type BRow<-r: Nat, -c: Nat> is Type:
1497	  BRow{b: Bands<r, c>, row: List<&2, F32>}
1498	
1499	def brow_fin(-r: Nat, -c: Nat, al: AL) -> BRow<r, c>:
1500	  match al:
1501	    case AL{d, l}:
1502	      BRow{BLeaf{Mat{d}}, l}
1503	
1504	# n numbers starting at flat index i of one band (a band may have no rows)
1505	def brow_leaf2(-r: Nat, -c: Nat, n: Nat, +i: U32, d: Array<F32>) -> BRow<r, c>:
1506	  match n:
1507	    case 0n:
1508	      BRow{BLeaf{Mat{d}}, Nil{}}
1509	    case 1n+p:
1510	      brow_fin(r, c, read_l(p, i, Nil{}, Array.get(F32, d, i)))
1511	
1512	def brow_leaf(-r: Nat, -c: Nat, m: Mat<r, c>, +i: U32, n: Nat) -> BRow<r, c>:
1513	  match m:
1514	    case Mat{d}:
1515	      brow_leaf2(r, c, n, i, d)
1516	
1517	def brow_l(-r: Nat, -c: Nat, p: BRow<half(r), c>, y: Bands<Nat.sub(r, half(r)), c>) -> BRow<r, c>:
1518	  match p:
1519	    case BRow{bx, row}:
1520	      BRow{BNode{bx, y}, row}
1521	
1522	def brow_r(-r: Nat, -c: Nat, x: Bands<half(r), c>, q: BRow<Nat.sub(r, half(r)), c>) -> BRow<r, c>:
1523	  match q:
1524	    case BRow{by, row}:
1525	      BRow{BNode{x, by}, row}
1526	
1527	# row i; left says whether i is in the first band of the node (i < half(rr))
1528	def brow(+c: Nat, -r: Nat, b: Bands<r, c>, left: Bool, +rr: Nat, -e: {rr == r : Nat}, +i: Nat) -> BRow<r, c>:
1529	  match b left:
1530	    case BLeaf{m} _:
1531	      brow_leaf(r, c, m, U32.from_nat(Nat.mul(i, c)), c)
1532	    case BNode{x, y} True{}:
1533	      brow_l(r, c, brow(c, half(r), x, Nat.is_lt(i, half(half(rr))), half(rr), eq_half(rr, r, e), i), y)
1534	    case BNode{x, y} False{}:
1535	      brow_r(r, c, x, brow(c, Nat.sub(r, half(r)), y, Nat.is_lt(Nat.sub(i, half(rr)), half(Nat.sub(rr, half(rr)))), Nat.sub(rr, half(rr)), eq_rest(rr, r, e), Nat.sub(i, half(rr))))
1536	
1537	# row i (c numbers), for example an embedding lookup
1538	def Bands.read_row(+r: Nat, +c: Nat, b: Bands<r, c>, +i: Nat) -> BRow<r, c>:
1539	  brow(c, r, b, Nat.is_lt(i, half(r)), r, {==}, i)
1540	
1541	def bl_join(-r: Nat, -c: Nat, p: BRow<half(r), c>, q: BRow<Nat.sub(r, half(r)), c>) -> BRow<r, c>:
1542	  match p q:
1543	    case BRow{bx, xs} BRow{by, ys}:
1544	      BRow{BNode{bx, by}, List.append(&2, F32, xs, ys)}
1545	
1546	def blist(+c: Nat, -r: Nat, b: Bands<r, c>, +rr: Nat, -e: {rr == r : Nat}) -> BRow<r, c>:
1547	  match b:
1548	    case BLeaf{m}:
1549	      brow_leaf(r, c, m, 0, Nat.mul(rr, c))
1550	    case BNode{x, y}:
1551	      bl_join(r, c, blist(c, half(r), x, half(rr), eq_half(rr, r, e)), blist(c, Nat.sub(r, half(r)), y, Nat.sub(rr, half(rr)), eq_rest(rr, r, e)))
1552	
1553	# all r*c numbers in row order (in BRow.row)
1554	def Bands.to_list(+r: Nat, +c: Nat, b: Bands<r, c>) -> BRow<r, c>:
1555	  blist(c, r, b, r, {==})
1556	
1557	# ---- the list path returns exactly r numbers ----
1558	#
1559	# The numbers do not matter here, only how many there are: each lemma below counts the list a
1560	# function builds, following the function's own recursion.
1561	
1562	def bl_len(-r: Nat, -c: Nat, bl: BL<r, c>) -> Nat:
1563	  match bl:
1564	    case BL{b, y}:
1565	      List.length(&2, F32, y)
1566	
1567	# s == a + (1 + b)  ->  s == 1 + (a + b)
1568	def succ_out(-s: Nat, +a: Nat, +b: Nat, e: {s == Nat.add(a, 1n+b) : Nat}) -> {s == 1n+Nat.add(a, b) : Nat}:
1569	  %Equal.sym(Nat, 1n+Nat.add(a, b), Nat.add(a, 1n+b), add_succ_r(a, b)) : {s == _ : Nat}
1570	  e
1571	
1572	# s == 1 + (p + (1 + l))  ->  s == 2 + (p + l)
1573	def len_step(-s: Nat, +p: Nat, +l: Nat, e: {s == 1n+Nat.add(p, 1n+l) : Nat}) -> {s == 2n+Nat.add(p, l) : Nat}:
1574	  %Equal.sym(Nat, 1n+Nat.add(p, l), Nat.add(p, 1n+l), add_succ_r(p, l)) : {s == 1n+_ : Nat}
1575	  e
1576	
1577	# s == n + 0  ->  s == n
1578	def zero_out(-s: Nat, +n: Nat, e: {s == Nat.add(n, 0n) : Nat}) -> {s == n : Nat}:
1579	  %add_zero_r(n) : {s == _ : Nat}
1580	  e
1581	
1582	# reversing onto acc adds the lengths
1583	def rev_len(+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}:
1584	  match xs:
1585	    case Nil{}:
1586	      {==}
1587	    case Con{h, t}:
1588	      succ_out(List.length(&2, F32, List.reverse.go(&2, F32, t, h <> acc)), List.length(&2, F32, t), List.length(&2, F32, acc), rev_len(t, h <> acc))
1589	
1590	# appending adds the lengths
1591	def app_len(+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}:
1592	  match xs:
1593	    case Nil{}:
1594	      {==}
1595	    case Con{h, t}:
1596	      %app_len(t, ys) : {1n+List.length(&2, F32, List.append(&2, F32, t, ys)) == 1n+_ : Nat}
1597	      {==}
1598	
1599	# a leaf's list: read_l reads mleft + 1 numbers onto acc and reverses them. By induction on
1600	# mleft: with 0 left it reads one number (rev_len counts the reversed list); with 1 + p left it
1601	# reads one and recurses, and len_step moves the 1 out of the sum.
1602	law leaf_len:
1603	  for -r: Nat
1604	  for -c: Nat
1605	  for w: Array<F32>
1606	  for +mleft: Nat
1607	  for +idx: U32
1608	  for +acc: List<&2, F32>
1609	  for rc: Array<F32> & F32
1610	  {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}
1611	
1612	def leaf_len(r, c, w, mleft, idx, acc, rc):
1613	  match mleft rc:
1614	    case 0n Tuple{d, +v}:
1615	      zero_out(List.length(&2, F32, List.reverse.go(&2, F32, v <> acc, Nil{})), 1n+List.length(&2, F32, acc), rev_len(v <> acc, Nil{}))
1616	    case 1n+p Tuple{d, +v}:
1617	      len_step(bl_len(r, c, bv_g2(r, c, w, read_l(p, (idx + 1 : U32), v <> acc, Array.get(F32, d, (idx + 1 : U32))))), p, List.length(&2, F32, acc), leaf_len(r, c, w, p, (idx + 1 : U32), v <> acc, Array.get(F32, d, (idx + 1 : U32))))
1618	
1619	# whatever the gemm wrote, reading 1 + p rows back gives 1 + p numbers (G has one constructor, so
1620	# matching g opens it, and leaf_len counts the list)
1621	def g_len(-r: Nat, -c: Nat, +p: Nat, g: G) -> {bl_len(r, c, bv_g(r, c, p, g)) == 1n+p : Nat}:
1622	  match g:
1623	    case G{a, b, y}:
1624	      zero_out(bl_len(r, c, bv_g2(r, c, b, read_l(p, 0, Nil{}, Array.get(F32, y, 0)))), 1n+p, leaf_len(r, c, b, p, 0, Nil{}, Array.get(F32, y, 0)))
1625	
1626	# LAW (band_len): the product of one band with `rows` rows gives exactly `rows` numbers.
1627	# 0 rows give the empty list; 1 + p rows go through the gemm, and g_len counts what is read back.
1628	law band_len:
1629	  for -r: Nat
1630	  for +c: Nat
1631	  for +rows: Nat
1632	  for x: Array<F32>
1633	  for w: Array<F32>
1634	  {bl_len(r, c, bv_gemm(r, c, rows, rows, x, w)) == rows : Nat}
1635	
1636	def band_len(r, c, rows, x, w):
1637	  match rows:
1638	    case 0n:
1639	      {==}
1640	    case 1n+p:
1641	      g_len(r, c, p, gemm(1n, 1n+p, c, U32.from_nat(c), 1, 1, U32.from_nat(c), x, w, Array.new(F32, cap_depth(1n+p), 0.0)))
1642	
1643	# joining two halves of h1 and h2 numbers gives h1 + h2 numbers. (The statement for the whole tree,
1644	# "Bands.matvec_l gives r numbers", would apply this to the results of the two recursive calls and
1645	# to the induction hypotheses about the same calls; that uses each band's Array twice, which Bend's
1646	# affine rules refuse. It stays open, covered by tests: NOTES.md, v3.1.)
1647	def join_len(-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}:
1648	  match p q:
1649	    case BL{bx, +yx} BL{by, +yy}:
1650	      %hp : {List.length(&2, F32, List.append(&2, F32, yx, yy)) == Nat.add(_, h2) : Nat}
1651	      %hq : {List.length(&2, F32, List.append(&2, F32, yx, yy)) == Nat.add(List.length(&2, F32, yx), _) : Nat}
1652	      app_len(yx, yy)
1653