src/tensor/contracts/matmul_parallel_proof.bend

bendtorch-core@0.1.0.0 · 861 lines · 59 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
4import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
5import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
6import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
7import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
8import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
9import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
10import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
11import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
12import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
13import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
14import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
15import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
16import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
17import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
18import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
19import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
20import bendtorch-core@0.1.0.0/src/tensor/contracts/dot_proof.bend as DotProof
21import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
22import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
23import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
24import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
25import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
26import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
27import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
28import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
29import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
30
31# The parallel matmul over replayed inputs. Its output is the replayed
32# storage that writes, in index order, the word `matmul_ordered` names at each
33# cell.
34
35def cell_word(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
36  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +position: Nat) -> F32:
37  DotFold.dot_fold(Laws.factors(Matrix.row_of(columns, position), Matrix.column_of(columns, position), inner, columns,
38    left, left_fill, left_ops, right, right_fill, right_ops, inner), 0.0)
39
40def writes(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
41  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat) -> List<&2, StorageLaws.Op>:
42  match count:
43    case 0n:
44      Nil{}
45    case 1n+previous:
46      Replayed.snoc(writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous),
47        StorageLaws.Write{U32.from_nat(previous), cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)})
48
49def writes_value(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
50  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
51  below: {Nat.is_lt(U32.to_nat(index), count) == True{} : Bool},
52  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
53  {Replayed.value(output, 0.0, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, count), index) ==
54    cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32}:
55  match count:
56    case 0n:
57      Empty.absurd({Replayed.value(output, 0.0, Nil{}, index) ==
58        cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32},
59        Arith.lt_zero(U32.to_nat(index), below))
60    case 1n+previous:
61      PointwiseProof.write_split(output, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous),
62        previous, cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous), index,
63        cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
64        below, room,
65        at => Equal.cong(Nat, F32, position => cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, position),
66          previous, U32.to_nat(index), Equal.sym(Nat, U32.to_nat(index), previous, at)),
67        earlier => writes_value(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, output, previous, index, earlier,
68          Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room)),
69        Shape.bool_case(Nat.is_eq(U32.to_nat(index), previous)))
70
71def lt_not_eq(+a: Nat, +b: Nat, below: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
72  match a b:
73    case 0n 0n:
74      Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, Arith.clash(below))
75    case 0n 1n+q:
76      {==}
77    case 1n+p 0n:
78      {==}
79    case 1n+p 1n+q:
80      lt_not_eq(p, q, below)
81
82# A write at an index below `index` leaves the word at `index`.
83def write_skip(+shape: Shape.Shape, +previous: Nat, +index: U32, +word: F32, +old: F32,
84  +room: {Nat.is_lt(previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
85  later: {Nat.is_lt(previous, U32.to_nat(index)) == True{} : Bool}) ->
86  {StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), word}, index, old) == old : F32}:
87  %Equal.sym(Nat, U32.to_nat(U32.from_nat(previous)), previous, MatrixIndex.word_exact(previous, shape, room)) :
88    {Bool.pick(F32, Bool.and(Nat.is_lt(_, U32.to_nat(Shape.count(shape))), Nat.is_eq(_, U32.to_nat(index))), word, old) == old : F32}
89  %Equal.sym(Bool, Nat.is_lt(previous, U32.to_nat(Shape.count(shape))), True{}, PointwiseProof.lt_count(previous, shape, room)) :
90    {Bool.pick(F32, Bool.and(_, Nat.is_eq(previous, U32.to_nat(index))), word, old) == old : F32}
91  %Equal.sym(Bool, Nat.is_eq(previous, U32.to_nat(index)), False{}, lt_not_eq(previous, U32.to_nat(index), later)) :
92    {Bool.pick(F32, _, word, old) == old : F32}
93  {==}
94
95# At or above the count, the writes leave the +0.0 fill.
96def writes_zero(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
97  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
98  +above: {Nat.is_le(count, U32.to_nat(index)) == True{} : Bool},
99  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
100  {Replayed.value(output, 0.0, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, count), index) == 0.0 : F32}:
101  match count:
102    case 0n:
103      {==}
104    case 1n+previous:
105      +history = writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)
106      +word = cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)
107      +op = {StorageLaws.Write{U32.from_nat(previous), word} : StorageLaws.Op}
108      Equal.trans(F32, Replayed.value(output, 0.0, Replayed.snoc(history, op), index),
109        StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)), 0.0,
110        Replayed.expected_snoc(history, op, U32.to_nat(Shape.count(output)), index, 0.0),
111        Equal.trans(F32, StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)),
112          Replayed.value(output, 0.0, history, index), 0.0,
113          write_skip(output, previous, index, word, Replayed.value(output, 0.0, history, index),
114            Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(output)), room),
115            Conversion.le_successor_lt(previous, U32.to_nat(index), above)),
116          writes_zero(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, output, previous, index,
117            Conversion.le_predecessor(previous, U32.to_nat(index), above),
118            Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room))))
119
120def lt_zero_false(+x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
121  match x:
122    case 0n:
123      {==}
124    case 1n+p:
125      {==}
126
127def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
128  match k:
129    case 0n:
130      {==}
131    case 1n+p:
132      lt_self_succ(p)
133
134def lt_succ_right(+b: Nat, +k: Nat, h: {Nat.is_lt(b, k) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == True{} : Bool}:
135  match b k:
136    case 0n _:
137      {==}
138    case 1n+p 0n:
139      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, Arith.clash(h))
140    case 1n+p 1n+q:
141      lt_succ_right(p, q, h)
142
143# k < b gives b < 1 + k false.
144def above_false(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == False{} : Bool}:
145  match k b:
146    case 0n 0n:
147      Empty.absurd({Nat.is_lt(0n, 1n) == False{} : Bool}, Arith.clash(h))
148    case 0n 1n+q:
149      lt_zero_false(q)
150    case 1n+p 0n:
151      Empty.absurd({Nat.is_lt(0n, 1n+(1n+p)) == False{} : Bool}, Arith.clash(h))
152    case 1n+p 1n+q:
153      above_false(p, q, h)
154
155def lt_asym(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, k) == False{} : Bool}:
156  match k b:
157    case 0n 0n:
158      {==}
159    case 0n 1n+q:
160      {==}
161    case 1n+p 0n:
162      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, Arith.clash(h))
163    case 1n+p 1n+q:
164      lt_asym(p, q, h)
165
166# 1 + b <= k gives b < k.
167def below_true(+b: Nat, +k: Nat, h: {Nat.is_le(1n+b, k) == True{} : Bool}) -> {Nat.is_lt(b, k) == True{} : Bool}:
168  match b k:
169    case 0n 0n:
170      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.clash(h))
171    case 0n 1n+q:
172      {==}
173    case 1n+p 0n:
174      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, Arith.clash(h))
175    case 1n+p 1n+q:
176      below_true(p, q, h)
177
178def lt_add_right(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_lt(a, c) == True{} : Bool}) ->
179  {Nat.is_lt(Nat.add(a, b), Nat.add(c, b)) == True{} : Bool}:
180  match a c:
181    case 0n 0n:
182      Empty.absurd({Nat.is_lt(b, b) == True{} : Bool}, Arith.clash(h))
183    case 0n 1n+q:
184      Arith.lt_succ(b, Nat.add(q, b), Api.le_add_left(q, b))
185    case 1n+p 0n:
186      Empty.absurd({Nat.is_lt(1n+Nat.add(p, b), b) == True{} : Bool}, Arith.clash(h))
187    case 1n+p 1n+q:
188      lt_add_right(p, q, b, h)
189
190def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
191  {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
192  match c:
193    case 0n:
194      h
195    case 1n+r:
196      le_add_cong(r, x, y, h)
197
198def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) ->
199  {Nat.is_le(a, c) == True{} : Bool}:
200  match a b c:
201    case 0n _ _:
202      Arith.le_zero(c)
203    case 1n+p 0n _:
204      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, Arith.clash(ab))
205    case 1n+p 1n+q 0n:
206      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, Arith.clash(bc))
207    case 1n+p 1n+q 1n+r:
208      le_trans(p, q, r, ab, bc)
209
210def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
211  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
212  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
213    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))
214
215def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
216  match number:
217    case 0n:
218      {==}
219    case 1n+p:
220      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero_right(p))
221
222# A word index below the storage length is the offset of its own route.
223def output_position(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool},
224  +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
225  {Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n) == U32.to_nat(index) : Nat}:
226  +rest = Arith.and_right(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid)
227  Equal.trans(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
228    add_zero_right(Model.offset(depth, Refinement.route(depth, index))),
229    Equal.sym(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)),
230      Route.route_offset(depth, index,
231        Arith.and_left(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid),
232        Arith.lt_le_trans(U32.to_nat(index), length, Model.capacity(depth), inside,
233          Arith.and_right(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth)), rest)))))
234
235
236# The output spec: cell `base` of the tree holds the cell's word below
237# `count` and +0.0 above it.
238
239def out_leaf(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +position: Nat, inside: Bool) -> F32:
240  match inside:
241    case False{}:
242      0.0
243    case True{}:
244      cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, position)
245
246def out_spec(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Array<F32>:
247  match depth:
248    case 0n:
249      ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, count))}
250    case 1n+inner:
251      ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base))}
252
253def out_balanced(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Model.Balanced(F32, depth, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base)):
254  match depth:
255    case 0n:
256      Unit{}
257    case 1n+inner:
258      (out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base)))
259
260def new_spec(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +depth: Nat, +base: Nat) -> {Array.new(F32, depth, 0.0) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, depth, base) : Array<F32>}:
261  match depth:
262    case 0n:
263      %Equal.sym(Bool, Nat.is_lt(base, 0n), False{}, lt_zero_false(base)) :
264        {ALeaf{0.0} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
265      {==}
266    case 1n+inner:
267      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), new_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, inner, base)) :
268        {ANode{_, Array.new(F32, inner, 0.0)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array<F32>}
269      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, Nat.add(Model.capacity(inner), base)),
270        new_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, inner, Nat.add(Model.capacity(inner), base))) :
271        {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array<F32>}
272      {==}
273
274# A subtree whose positions all lie above k is the same for k and 1 + k.
275def above(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_lt(k, b) == True{} : Bool}) ->
276  {out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array<F32>}:
277  match depth:
278    case 0n:
279      %Equal.sym(Bool, Nat.is_lt(b, k), False{}, lt_asym(k, b, h)) :
280        {ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
281      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), False{}, above_false(k, b, h)) :
282        {ALeaf{0.0} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array<F32>}
283      {==}
284    case 1n+inner:
285      +high = Nat.add(Model.capacity(inner), b)
286      %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), above(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, h)) :
287        {ANode{_, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
288      %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high),
289        above(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, Arith.lt_le_trans(k, b, high, h, Api.le_add_left(Model.capacity(inner), b)))) :
290        {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
291      {==}
292
293# A subtree whose positions all lie below k is the same for k and 1 + k.
294def below(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(Model.capacity(depth), b), k) == True{} : Bool}) ->
295  {out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array<F32>}:
296  match depth:
297    case 0n:
298      +lower = below_true(b, k, h)
299      %Equal.sym(Bool, Nat.is_lt(b, k), True{}, lower) :
300        {ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
301      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), True{}, lt_succ_right(b, k, lower)) :
302        {ALeaf{cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b)} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array<F32>}
303      {==}
304    case 1n+inner:
305      +c = Model.capacity(inner)
306      +high = Nat.add(c, b)
307      +nested = Equal.trans(Bool, Nat.is_le(Nat.add(c, high), k), Nat.is_le(Nat.add(Nat.add(c, c), b), k), True{},
308        Equal.cong(Nat, Bool, x => Nat.is_le(x, k), Nat.add(c, high), Nat.add(Nat.add(c, c), b), Index.add_assoc(c, c, b)), h)
309      +low_h = le_trans(high, Nat.add(c, high), k, le_add_cong(c, b, high, Api.le_add_left(c, b)), nested)
310      %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), below(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, low_h)) :
311        {ANode{_, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
312      %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), below(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, nested)) :
313        {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
314      {==}
315
316# Writing cell k at the path whose position is k turns the spec for k into
317# the spec for 1 + k.
318def write_spec(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +base: Nat, +path: Model.Path(depth),
319  +h: {Nat.add(Model.offset(depth, path), base) == k : Nat}) ->
320  {ArrayCore.write_path(F32, depth, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, base), path, cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k)) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, base) : Array<F32>}:
321  match depth:
322    case 0n:
323      %h : {ALeaf{cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, _)} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, 1n+_))} : Array<F32>}
324      %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, lt_self_succ(base)) :
325        {ALeaf{cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base)} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
326      {==}
327    case 1n+inner:
328      Model.Step{+bit, +rest} = path
329      match bit:
330        case False{}:
331          +c = Model.capacity(inner)
332          +high = Nat.add(c, base)
333          +inside = Equal.trans(Bool, Nat.is_lt(k, high), Nat.is_lt(Nat.add(Model.offset(inner, rest), base), high), True{},
334            Equal.cong(Nat, Bool, x => Nat.is_lt(x, high), k, Nat.add(Model.offset(inner, rest), base),
335              Equal.sym(Nat, Nat.add(Model.offset(inner, rest), base), k, h)),
336            lt_add_right(Model.offset(inner, rest), c, base, Api.offset_lt(inner, rest)))
337          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), rest, cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k)),
338            out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), write_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, rest, h)) :
339            {ANode{_, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
340          %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), above(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, inside)) :
341            {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
342          {==}
343        case True{}:
344          +c = Model.capacity(inner)
345          +high = Nat.add(c, base)
346          +off = Model.offset(inner, rest)
347          +lower = Equal.trans(Bool, Nat.is_le(high, k), Nat.is_le(high, Nat.add(c, Nat.add(off, base))), True{},
348            Equal.cong(Nat, Bool, x => Nat.is_le(high, x), k, Nat.add(c, Nat.add(off, base)),
349              Equal.trans(Nat, k, Nat.add(Nat.add(c, off), base), Nat.add(c, Nat.add(off, base)),
350                Equal.sym(Nat, Nat.add(Nat.add(c, off), base), k, h),
351                Equal.sym(Nat, Nat.add(c, Nat.add(off, base)), Nat.add(Nat.add(c, off), base), Index.add_assoc(c, off, base)))),
352            le_add_cong(c, base, Nat.add(off, base), Api.le_add_left(off, base)))
353          +shifted = Equal.trans(Nat, Nat.add(off, high), Nat.add(Nat.add(c, off), base), k, position_step(c, off, base), h)
354          %Equal.sym(Array<F32>, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), below(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, lower)) :
355            {ANode{_, ArrayCore.write_path(F32, inner, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k))} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
356          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k)),
357            out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), write_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, rest, shifted)) :
358            {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
359          {==}
360
361# The family history, replayed on the owned storage that `created` makes,
362# is the owned storage that holds the output spec.
363def chain(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
364  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
365  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
366  {StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), f} : Storage.Storage}:
367  match k:
368    case 0n:
369      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n), new_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
370        out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n))
371    case 1n+j:
372      +index = U32.from_nat(j)
373      +value = cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j)
374      +below_n = Conversion.le_successor_lt(j, n, room)
375      +exact = Conversion.natural_word_exact(j, limit, le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
376      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
377        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
378      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
379        output_position(d, n, index, fits, inside), exact)
380      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), Refinement.route(d, index), value),
381        out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)),
382        write_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n, Refinement.route(d, index), offset))
383      Equal.trans(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
384        StorageLaws.step(StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
385        Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f},
386        FromValues.replay_snoc(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
387        %Equal.sym(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f},
388          chain(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
389          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
390        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
391          Storage.set_checked(d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f),
392          (Storage.Owned{d, n, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value),
393            Certificates.set_result(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f}, Done{Unit{}}),
394          Api.set_checked_hit(d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f,
395            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
396          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
397        Owned.owned_eq(d, n, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), written,
398          Certificates.set_result(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f)(
399          out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n)))
400
401
402# The copy the build reads of a replayed input in normal form: the Second
403# half of the clone of the array its normalized history makes.
404def history(+shape: Shape.Shape, +ops: List<&2, StorageLaws.Op>) -> List<&2, Api.Effect>:
405  Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{})
406
407def copy(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +depth: Nat) -> Array<F32>:
408  Api.arr(history(shape, ops), depth, fill)
409
410def copy_valid(+shape: Shape.Shape, +ops: List<&2, StorageLaws.Op>) -> {Build.written(U32.to_nat(Shape.count(shape)), history(shape, ops)) == True{} : Bool}:
411  Owned.norm_written(U32.to_nat(Shape.count(shape)), ops, Nil{}, Api.hit_of(U32.to_nat(Shape.count(shape)), ops), {==}, {==})
412
413# A read of the copy below the input's count holds the replayed word.
414def copy_word(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32) ->
415  {Api.current(history(shape, ops), index, fill) == Replayed.value(shape, fill, ops, index) : F32}:
416  Owned.norm_current(U32.to_nat(Shape.count(shape)), ops, Nil{}, index, fill, Api.hit_of(U32.to_nat(Shape.count(shape)), ops), {==})
417
418def index_inside(+shape: Shape.Shape, +number: Nat, +below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
419  {Nat.is_lt(U32.to_nat(U32.from_nat(number)), U32.to_nat(Shape.count(shape))) == True{} : Bool}:
420  PointwiseProof.lt_count(U32.to_nat(U32.from_nat(number)), shape, MatrixIndex.word_inside(number, shape, below))
421
422# The terms `cursor .. cursor + fuel` of cell (row, column) over the replayed
423# words, added to `accumulator` in increasing k.
424def fold_from(fuel: Nat, +span: Nat, +columns: Nat, +row: Nat, +column: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
425  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat, accumulator: F32) -> F32:
426  match fuel:
427    case 0n:
428      accumulator
429    case 1n+rest:
430      fold_from(rest, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor,
431        F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, span), cursor))),
432          Replayed.value(right, right_fill, right_ops, U32.from_nat(Nat.add(Nat.mul(cursor, columns), column))))))
433
434def fold_factors(+fuel: Nat, +span: Nat, +columns: Nat, +row: Nat, +column: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
435  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat,
436  +steps: {Nat.add(cursor, fuel) == span : Nat}) ->
437  {fold_from(fuel, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, cursor,
438    DotFold.dot_fold(Laws.factors(row, column, span, columns, left, left_fill, left_ops, right, right_fill, right_ops, cursor), 0.0)) ==
439    DotFold.dot_fold(Laws.factors(row, column, span, columns, left, left_fill, left_ops, right, right_fill, right_ops, span), 0.0) : F32}:
440  match fuel:
441    case 0n:
442      Equal.cong(Nat, F32,
443        k => DotFold.dot_fold(Laws.factors(row, column, span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k), 0.0),
444        cursor, span, PointwiseProof.steps_done(cursor, span, steps))
445    case 1n+rest:
446      +x = Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, span), cursor)))
447      +y = Replayed.value(right, right_fill, right_ops, U32.from_nat(Nat.add(Nat.mul(cursor, columns), column)))
448      +before = Laws.factors(row, column, span, columns, left, left_fill, left_ops, right, right_fill, right_ops, cursor)
449      %DotProof.dot_snoc(before, x, y, 0.0) :
450        {fold_from(rest, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor, _) ==
451          DotFold.dot_fold(Laws.factors(row, column, span, columns, left, left_fill, left_ops, right, right_fill, right_ops, span), 0.0) : F32}
452      fold_factors(rest, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor,
453        MatrixIndex.steps_next(cursor, rest, span, steps))
454
455
456# How a build copy answers the reads of its input: an empty input has no
457# cell to read, and a normal one holds the input's normalized history.
458type Source<-shape: Shape.Shape, -fill: F32, -ops: List<&2, StorageLaws.Op>, -h: List<&2, Api.Effect>, -d: Nat, -f: F32> is Data:
459  NoCells{zero: {U32.to_nat(Shape.count(shape)) == 0n : Nat}}
460  Normal{fits: {Storage.bounds(d, U32.to_nat(Shape.count(shape))) == True{} : Bool},
461    same: {h == history(shape, ops) : List<&2, Api.Effect>}, filled: {f == fill : F32}}
462
463def source_read(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32,
464  +source: Source<shape, fill, ops, h, d, f>, +index: U32,
465  +inside: {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}, -pair: Array<F32> & F32,
466  +exact: {pair == Array.get(F32, Api.arr(h, d, f), index) : Array<F32> & F32}) ->
467  {Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32}:
468  match source:
469    case NoCells{zero}:
470      Empty.absurd({Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32},
471        Arith.lt_zero(U32.to_nat(index),
472          %zero : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
473          inside))
474    case Normal{fits, same, filled}:
475      Equal.trans(F32, Refinement.second(F32, pair), Api.current(h, index, f), Replayed.value(shape, fill, ops, index),
476        Build.got_value(d, h, f, U32.to_nat(Shape.count(shape)), index, pair, exact, fits, inside,
477          %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Build.written(U32.to_nat(Shape.count(shape)), _) == True{} : Bool}
478          copy_valid(shape, ops)),
479        %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Api.current(_, index, f) == Replayed.value(shape, fill, ops, index) : F32}
480        %Equal.sym(F32, f, fill, filled) : {Api.current(history(shape, ops), index, _) == Replayed.value(shape, fill, ops, index) : F32}
481        copy_word(shape, fill, ops, index))
482
483def DotIs(+fuel: Nat, +span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
484  -result: F32 & (Array<F32> & Array<F32>)) -> Type:
485  {result == (fold_from(fuel, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, cursor, accumulator), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))) : F32 & (Array<F32> & Array<F32>)}
486
487# The last term of a run: both reads hold the replayed words, and both
488# copies come back.
489def run_last(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>, +rows: Nat, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
490  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
491  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
492  +below: {Nat.is_lt(cursor, span) == True{} : Bool},
493  pl: Array<F32> & F32, +exact_l: {pl == Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)) : Array<F32> & F32},
494  pr: Array<F32> & F32, +exact_r: {pr == Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)) : Array<F32> & F32}) ->
495  DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(0n, 1n, columns, Nat.add(Nat.mul(row, span), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)):
496  (la, x) = pl
497  (ra, y) = pr
498  +ex = source_read(left, left_fill, left_ops, ha, dl, fa, lsrc, Matrix.left_index(span, row, cursor),
499    index_inside(left, Nat.add(Nat.mul(row, span), cursor), MatrixIndex.left_below(rows, span, row, row_below, left, left_extents, cursor, below)),
500    (la, x), exact_l)
501  +ey = source_read(right, right_fill, right_ops, hb, dr, fb, rsrc, Matrix.right_index(columns, column, cursor),
502    index_inside(right, Nat.add(Nat.mul(cursor, columns), column), MatrixIndex.right_below(span, columns, column, column_below, right, right_extents, cursor, below)),
503    (ra, y), exact_r)
504  +el = Build.got_kept(dl, ha, fa, Matrix.left_index(span, row, cursor), (la, x), exact_l)
505  +er = Build.got_kept(dr, hb, fb, Matrix.right_index(columns, column, cursor), (ra, y), exact_r)
506  %Equal.sym(F32, x, Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), ex) :
507    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(_, y)), (la, ra)))
508  %Equal.sym(F32, y, Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)), ey) :
509    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), _)), (la, ra)))
510  %Equal.sym(Array<F32>, la, Api.arr(ha, dl, fa), el) :
511    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), (_, ra)))
512  %Equal.sym(Array<F32>, ra, Api.arr(hb, dr, fb), er) :
513    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), (Api.arr(ha, dl, fa), _)))
514  {==}
515
516# A term with more after it: the reads hold the replayed words, the offsets
517# step to the next term's, and the run goes on from its reads of the same
518# copies.
519def run_next(+rest: Nat, +span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>, +rows: Nat, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
520  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
521  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
522  +below: {Nat.is_lt(cursor, span) == True{} : Bool},
523  pl: Array<F32> & F32, +exact_l: {pl == Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)) : Array<F32> & F32},
524  pr: Array<F32> & F32, +exact_r: {pr == Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)) : Array<F32> & F32},
525  next: DotIs(1n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Matrix.product_run(rest, 1n, columns, Nat.add(Nat.mul(row, span), 1n+cursor), Nat.add(Nat.mul(1n+cursor, columns), column), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, 1n+cursor)), Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, 1n+cursor))))) ->
526  DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(1n+rest, 1n, columns, Nat.add(Nat.mul(row, span), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)):
527  (la, x) = pl
528  (ra, y) = pr
529  +ex = source_read(left, left_fill, left_ops, ha, dl, fa, lsrc, Matrix.left_index(span, row, cursor),
530    index_inside(left, Nat.add(Nat.mul(row, span), cursor), MatrixIndex.left_below(rows, span, row, row_below, left, left_extents, cursor, below)),
531    (la, x), exact_l)
532  +ey = source_read(right, right_fill, right_ops, hb, dr, fb, rsrc, Matrix.right_index(columns, column, cursor),
533    index_inside(right, Nat.add(Nat.mul(cursor, columns), column), MatrixIndex.right_below(span, columns, column, column_below, right, right_extents, cursor, below)),
534    (ra, y), exact_r)
535  +el = Build.got_kept(dl, ha, fa, Matrix.left_index(span, row, cursor), (la, x), exact_l)
536  +er = Build.got_kept(dr, hb, fb, Matrix.right_index(columns, column, cursor), (ra, y), exact_r)
537  %Equal.sym(F32, x, Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), ex) :
538    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(_, y)), Array.get(F32, la, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))))
539  %Equal.sym(F32, y, Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)), ey) :
540    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), _)), Array.get(F32, la, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))))
541  %Equal.sym(Array<F32>, la, Api.arr(ha, dl, fa), el) :
542    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, _, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))))
543  %Equal.sym(Array<F32>, ra, Api.arr(hb, dr, fb), er) :
544    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, _, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))))
545  %Equal.sym(Nat, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(Nat.mul(row, span), 1n+cursor), MatrixIndex.stepped_left(span, row, cursor)) :
546    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, _, Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(_)), Array.get(F32, Api.arr(hb, dr, fb), U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))))
547  %Equal.sym(Nat, Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), Nat.add(Nat.mul(1n+cursor, columns), column), MatrixIndex.stepped_right(columns, column, cursor)) :
548    DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(Nat.mul(row, span), 1n+cursor), _, F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(Nat.add(Nat.mul(row, span), 1n+cursor))), Array.get(F32, Api.arr(hb, dr, fb), U32.from_nat(_))))
549  next
550
551# A run of fuel + 1 terms from cursor folds the replayed words in increasing
552# k and hands both copies back.
553def run_eq(+fuel: Nat, +span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>, +rows: Nat, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
554  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
555  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
556  +steps: {Nat.add(cursor, 1n+fuel) == span : Nat},
557  pl: Array<F32> & F32, +exact_l: {pl == Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)) : Array<F32> & F32},
558  pr: Array<F32> & F32, +exact_r: {pr == Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)) : Array<F32> & F32}) ->
559  DotIs(1n+fuel, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(fuel, 1n, columns, Nat.add(Nat.mul(row, span), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)):
560  match fuel:
561    case 0n:
562      run_last(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, cursor, accumulator, row_below, left_extents, column_below, right_extents, MatrixIndex.cursor_below(cursor, 0n, span, steps), pl, exact_l, pr, exact_r)
563    case 1n+rest:
564      run_next(rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, cursor, accumulator, row_below, left_extents, column_below, right_extents, MatrixIndex.cursor_below(cursor, 1n+rest, span, steps), pl, exact_l, pr, exact_r,
565        run_eq(rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, 1n+cursor, F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), row_below, left_extents, column_below, right_extents, MatrixIndex.steps_next(cursor, 1n+rest, span, steps),
566          Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, 1n+cursor)), {==}, Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, 1n+cursor)), {==}))
567
568# Cell (row, column) of the build over the two copies folds the replayed
569# words in increasing k and hands both copies back.
570def dot_eq(+fuel: Nat, +span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>, +rows: Nat, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
571  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
572  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>}, +steps: {Nat.add(cursor, fuel) == span : Nat}) ->
573  DotIs(fuel, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.cell_dot(fuel, span, columns, row, column, cursor, accumulator, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))):
574  match fuel:
575    case 0n:
576      {==}
577    case 1n+rest:
578      run_eq(rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, cursor, accumulator, row_below, left_extents, column_below, right_extents, steps, Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)), {==}, Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)), {==})
579
580def TreeEq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +depth: Nat, +base: Nat, -result: Array<F32> & (Array<F32> & Array<F32>)) -> Type:
581  {Pair.fst(Array<F32>, Array<F32> & Array<F32>, result) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base) : Array<F32>} &
582    ({Pair.fst(Array<F32>, Array<F32>, Pair.snd(Array<F32>, Array<F32> & Array<F32>, result)) == Api.arr(ha, dl, fa) : Array<F32>} &
583      {Pair.snd(Array<F32>, Array<F32>, Pair.snd(Array<F32>, Array<F32> & Array<F32>, result)) == Api.arr(hb, dr, fb) : Array<F32>})
584
585def cell_inside_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
586  +output: Shape.Shape, +rows: Nat,
587  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
588  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
589  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
590  +count_exact: {count == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +base: Nat,
591  +decided: {True{} == Nat.is_lt(base, count) : Bool}) ->
592  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, base, Parallel.leaf(~(Array<F32> & Array<F32>), Matrix.cell(span, columns, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb), True{}))):
593  +row = Matrix.row_of(columns, base)
594  +column = Matrix.column_of(columns, base)
595  +below = MatrixIndex.lt_bound(base, count, Shape.logical_numel(Shape.dimensions(output)), count_exact,
596    Equal.sym(Bool, True{}, Nat.is_lt(base, count), decided))
597  +fit = MatrixIndex.position_fits(output, rows, columns, output_extents, base, below)
598  +row_below = Arith.and_left(Nat.is_lt(row, rows), Bool.and(Nat.is_lt(column, columns), True{}), fit)
599  +column_below = Arith.and_left(Nat.is_lt(column, columns), True{},
600    Arith.and_right(Nat.is_lt(row, rows), Bool.and(Nat.is_lt(column, columns), True{}), fit))
601  %Equal.sym(F32 & (Array<F32> & Array<F32>),
602    Matrix.dot_of(span, columns, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)),
603    (fold_from(span, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 0.0), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))),
604    dot_eq(span, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, 0n, 0.0, row_below, left_extents, column_below, right_extents, {==})) :
605    TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, base, Parallel.leaf(~(Array<F32> & Array<F32>), _))
606  (%decided : {ALeaf{fold_from(span, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 0.0)} ==
607      ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
608    Equal.cong(F32, Array<F32>, w => ALeaf{w},
609      fold_from(span, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 0.0),
610      cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base),
611      fold_factors(span, span, columns, row, column, left, left_fill, left_ops, right, right_fill, right_ops, 0n, {==})),
612   ({==}, {==}))
613
614def cell_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
615  +output: Shape.Shape, +rows: Nat,
616  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
617  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
618  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
619  +count_exact: {count == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +base: Nat, inside: Bool,
620  +decided: {inside == Nat.is_lt(base, count) : Bool}) ->
621  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, base, Parallel.leaf(~(Array<F32> & Array<F32>), Matrix.cell(span, columns, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb), inside))):
622  match inside:
623    case False{}:
624      (%decided : {ALeaf{0.0} == ALeaf{out_leaf(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
625       {==}, ({==}, {==}))
626    case True{}:
627      cell_inside_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, base, decided)
628
629def tree_join_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lower: Nat, +base: Nat, -a: Array<F32>, high: Array<F32> & (Array<F32> & Array<F32>),
630  ea: {a == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base) : Array<F32>},
631  facts: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, Nat.add(Model.capacity(lower), base), high)) ->
632  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n+lower, base, Parallel.join(~(Array<F32> & Array<F32>), a, high)):
633  (b, inputs) = high
634  (eb, kept) = facts
635  (%Equal.sym(Array<F32>, a, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), ea) :
636     {ANode{_, b} == ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, Nat.add(Model.capacity(lower), base))} : Array<F32>}
637   %Equal.sym(Array<F32>, b, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, Nat.add(Model.capacity(lower), base)), eb) :
638     {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), _} == ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, Nat.add(Model.capacity(lower), base))} : Array<F32>}
639   {==}, kept)
640
641def tree_node_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lower: Nat, +base: Nat, low: Array<F32> & (Array<F32> & Array<F32>),
642  facts: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, base, low),
643  next: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, Nat.add(Model.capacity(lower), base), Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, Nat.add(Model.capacity(lower), base), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))))) ->
644  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n+lower, base, Parallel.node(~Array<F32>, ~Array<F32>, l => r => Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, Nat.add(Model.capacity(lower), base), (l, r)), low)):
645  (a, inputs) = low
646  (la, ra) = inputs
647  (ea, kept) = facts
648  (el, er) = kept
649  %Equal.sym(Array<F32>, la, Api.arr(ha, dl, fa), el) :
650    TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n+lower, base, Parallel.join(~(Array<F32> & Array<F32>), a, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, Nat.add(Model.capacity(lower), base), (_, ra))))
651  %Equal.sym(Array<F32>, ra, Api.arr(hb, dr, fb), er) :
652    TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n+lower, base, Parallel.join(~(Array<F32> & Array<F32>), a, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, Nat.add(Model.capacity(lower), base), (Api.arr(ha, dl, fa), _))))
653  tree_join_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, base, a, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, Nat.add(Model.capacity(lower), base), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))), ea, next)
654
655# The depth-1 tree: the leaf of cell `base` and the leaf of the cell after
656# it, which reads the state the first hands back.
657def pair_join_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +base: Nat, x: F32, high: F32 & Array<F32> & Array<F32>,
658  ex: {ALeaf{x} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, base) : Array<F32>},
659  leaf_facts: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, Nat.add(1n, base), Parallel.leaf(~(Array<F32> & Array<F32>), high))) ->
660  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n, base, Parallel.pair_join(~(Array<F32> & Array<F32>), x, high)):
661  (y, inputs) = high
662  (ey, kept) = leaf_facts
663  (%Equal.sym(Array<F32>, ALeaf{x}, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, base), ex) : {ANode{_, ALeaf{y}} == ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, Nat.add(1n, base))} : Array<F32>}
664   %Equal.sym(Array<F32>, ALeaf{y}, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, Nat.add(1n, base)), ey) : {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, base), _} == ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, base), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 0n, Nat.add(1n, base))} : Array<F32>}
665   {==}, kept)
666
667def pair_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
668  +output: Shape.Shape, +rows: Nat,
669  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
670  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
671  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
672  +count_exact: {count == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +base: Nat, low: F32 & Array<F32> & Array<F32>,
673  leaf_facts: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, base, Parallel.leaf(~(Array<F32> & Array<F32>), low))) ->
674  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n, base, Parallel.pair(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), count, base, low)):
675  (x, inputs) = low
676  (la, ra) = inputs
677  (ex, kept) = leaf_facts
678  (el, er) = kept
679  %Equal.sym(Array<F32>, la, Api.arr(ha, dl, fa), el) :
680    TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n, base, Parallel.pair_join(~(Array<F32> & Array<F32>), x, Matrix.cell_at(Matrix.dims(Matrix.Dims{span, columns}), Nat.add(1n, base), (_, ra), Nat.is_lt(Nat.add(1n, base), count))))
681  %Equal.sym(Array<F32>, ra, Api.arr(hb, dr, fb), er) :
682    TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n, base, Parallel.pair_join(~(Array<F32> & Array<F32>), x, Matrix.cell_at(Matrix.dims(Matrix.Dims{span, columns}), Nat.add(1n, base), (Api.arr(ha, dl, fa), _), Nat.is_lt(Nat.add(1n, base), count))))
683  pair_join_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, base, x, Matrix.cell_at(Matrix.dims(Matrix.Dims{span, columns}), Nat.add(1n, base), (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Nat.is_lt(Nat.add(1n, base), count)), ex,
684    cell_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, Nat.add(1n, base), Nat.is_lt(Nat.add(1n, base), count), {==}))
685
686def tree_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
687  +output: Shape.Shape, +rows: Nat,
688  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
689  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
690  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
691  +count_exact: {count == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +depth: Nat, +base: Nat) ->
692  TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, depth, base, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), depth, count, base, (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)))):
693  match depth:
694    case 0n:
695      cell_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, base, Nat.is_lt(base, count), {==})
696    case 1n+lower:
697      match lower:
698        case 0n:
699          pair_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, base, Matrix.cell_at(Matrix.dims(Matrix.Dims{span, columns}), base, (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Nat.is_lt(base, count)),
700            cell_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, base, Nat.is_lt(base, count), {==}))
701        case 1n+below:
702          tree_node_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, base, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), lower, count, base, (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))),
703            tree_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, lower, base),
704            tree_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, lower, Nat.add(Model.capacity(lower), base)))
705
706def tree_first(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +depth: Nat, +base: Nat, -result: Array<F32> & (Array<F32> & Array<F32>), facts: TreeEq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, depth, base, result)) ->
707  {Pair.fst(Array<F32>, Array<F32> & Array<F32>, result) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base) : Array<F32>}:
708  (first, kept) = facts
709  first
710
711def fork_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lower: Nat, +rest: Nat, +base: Nat,
712  low: {Matrix.build(lower, rest, span, columns, count, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base) : Array<F32>},
713  high: {Matrix.build(lower, rest, span, columns, count, Nat.add(Model.capacity(lower), base), Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, Nat.add(Model.capacity(lower), base)) : Array<F32>},
714  lp: Array<F32> & Array<F32>, +le: {lp == Array.clone(F32, Api.arr(ha, dl, fa)) : Array<F32> & Array<F32>},
715  rp: Array<F32> & Array<F32>, +re: {rp == Array.clone(F32, Api.arr(hb, dr, fb)) : Array<F32> & Array<F32>}) ->
716  {Parallel.fork(~Array<F32>, ~Array<F32>, Elementwise.halves(lp, rp), l => r => Parallel.build(~Matrix.Dims, ~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.dims, ~Elementwise.split, ~Matrix.cell_at, Matrix.Dims{span, columns}, lower, rest, count, base, (l, r)), l => r => Parallel.build(~Matrix.Dims, ~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.dims, ~Elementwise.split, ~Matrix.cell_at, Matrix.Dims{span, columns}, lower, rest, count, Nat.add(Model.capacity(lower), base), (l, r))) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}:
717  (l1, l2) = lp
718  (r1, r2) = rp
719  +upper = Nat.add(Model.capacity(lower), base)
720  %Equal.sym(Array<F32>, l1, Api.arr(ha, dl, fa), Build.clone_first_eq(dl, ha, fa, (l1, l2), le)) :
721    {ANode{Matrix.build(lower, rest, span, columns, count, base, _, r1), Matrix.build(lower, rest, span, columns, count, upper, l2, r2)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
722  %Equal.sym(Array<F32>, r1, Api.arr(hb, dr, fb), Build.clone_first_eq(dr, hb, fb, (r1, r2), re)) :
723    {ANode{Matrix.build(lower, rest, span, columns, count, base, Api.arr(ha, dl, fa), _), Matrix.build(lower, rest, span, columns, count, upper, l2, r2)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
724  %Equal.sym(Array<F32>, l2, Api.arr(ha, dl, fa), Build.clone_second_eq(dl, ha, fa, (l1, l2), le)) :
725    {ANode{Matrix.build(lower, rest, span, columns, count, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build(lower, rest, span, columns, count, upper, _, r2)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
726  %Equal.sym(Array<F32>, r2, Api.arr(hb, dr, fb), Build.clone_second_eq(dr, hb, fb, (r1, r2), re)) :
727    {ANode{Matrix.build(lower, rest, span, columns, count, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build(lower, rest, span, columns, count, upper, Api.arr(ha, dl, fa), _)} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
728  %Equal.sym(Array<F32>, Matrix.build(lower, rest, span, columns, count, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), low) :
729    {ANode{_, Matrix.build(lower, rest, span, columns, count, upper, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
730  %Equal.sym(Array<F32>, Matrix.build(lower, rest, span, columns, count, upper, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, upper), high) :
731    {ANode{out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, lower, base), _} == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, 1n+lower, base) : Array<F32>}
732  {==}
733
734# Whatever the split, the parallel build over the copies returns the spec.
735def build_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +count: Nat, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
736  +output: Shape.Shape, +rows: Nat,
737  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
738  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
739  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
740  +count_exact: {count == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +depth: Nat, +splits: Nat, +base: Nat) ->
741  {Matrix.build(depth, splits, span, columns, count, base, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)) == out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base) : Array<F32>}:
742  match depth splits:
743    case 1n+lower 1n+rest:
744      fork_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lower, rest, base, build_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, lower, rest, base),
745        build_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, lower, rest, Nat.add(Model.capacity(lower), base)),
746        Array.clone(F32, Api.arr(ha, dl, fa)), {==}, Array.clone(F32, Api.arr(hb, dr, fb)), {==})
747    case 0n _:
748      tree_first(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 0n, base, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), 0n, count, base, (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))), tree_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, 0n, base))
749    case 1n+lower 0n:
750      tree_first(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, 1n+lower, base, Parallel.tree(~Matrix.Dims, ~Array<F32>, ~Array<F32>, ~Matrix.cell_at, Matrix.dims(Matrix.Dims{span, columns}), 1n+lower, count, base, (Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))), tree_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, count, lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, count_exact, 1n+lower, base))
751
752# The writes of every cell, replayed on the owned storage `created` makes for
753# the output, give the owned storage the parallel build fills.
754def output_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
755  +output: Shape.Shape, +rows: Nat,
756  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
757  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
758  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
759  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(output))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(output))) == True{} : Bool}) ->
760  {StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output))), Storage.Owned{d, U32.to_nat(Shape.count(output)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(output)), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), f} : Storage.Storage}:
761  Equal.trans(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output))), Storage.Owned{d, U32.to_nat(Shape.count(output)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
762    Storage.Owned{d, U32.to_nat(Shape.count(output)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), f},
763    Storage.Owned{d, U32.to_nat(Shape.count(output)), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), f},
764    chain(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, U32.to_nat(Shape.count(output)), f, fits, Shape.count(output), Conversion.le_reflexive(U32.to_nat(Shape.count(output))), U32.to_nat(Shape.count(output)), Conversion.le_reflexive(U32.to_nat(Shape.count(output)))),
765    Owned.owned_eq(d, U32.to_nat(Shape.count(output)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)),
766      Equal.sym(Array<F32>, Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n),
767        build_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, U32.to_nat(Shape.count(output)), lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, Reads.count_exact(output), d, Matrix.product_splits(d, span), 0n)),
768      out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), f)(Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))))
769
770# The inputs of the parallel product, as the elementwise export takes them.
771def half_keeps(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32) ->
772  {Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), index) == Replayed.value(shape, fill, ops, index) : F32}:
773  Replayed.expected_snoc(ops, StorageLaws.First{}, U32.to_nat(Shape.count(shape)), index, fill)
774
775def words_snoc(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +word: F32, +other: F32,
776  +before: List<&2, F32>, rest: {Laws.words(shape, fill, ops, previous) == before : List<&2, F32>}, last: {word == other : F32}) ->
777  {List.append(&2, F32, Laws.words(shape, fill, ops, previous), [word]) == List.append(&2, F32, before, [other]) : List<&2, F32>}:
778  Equal.trans(List<&2, F32>, List.append(&2, F32, Laws.words(shape, fill, ops, previous), [word]),
779    List.append(&2, F32, before, [word]), List.append(&2, F32, before, [other]),
780    Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), Laws.words(shape, fill, ops, previous), before, rest),
781    Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, before, [value]), word, other, last))
782
783# The First half of a clone lists the same words.
784
785def words_first(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
786  {Laws.words(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), count) == Laws.words(shape, fill, ops, count) : List<&2, F32>}:
787  match count:
788    case 0n:
789      {==}
790    case 1n+previous:
791      +position = U32.from_nat(previous)
792      words_snoc(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), previous,
793        Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), position), Replayed.value(shape, fill, ops, position),
794        Laws.words(shape, fill, ops, previous), words_first(shape, fill, ops, previous), half_keeps(shape, fill, ops, position))
795
796# `take` of an owned tensor hands back the First half of its clone and the
797# Second half's array.
798
799def take_owned_lift(+shape: Shape.Shape, +d: Nat, +n: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
800  -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -b: Model.Balanced(F32, d, array),
801  -f: {Storage.bounds(d, n) == True{} : Bool}, -fits: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
802  -Q: (Core.Dynamic & Array<F32>) -> Type,
803  h: @-kept: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f))) ==
804    Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
805    Q((Core.Packed{shape, Core.TTensor{StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f)), kept}},
806      Pair.snd(Array<F32>, Array<F32>, pair)))) ->
807  Q(Elementwise.take_owned(shape, d, n, array, pair, same, b, f, fits)):
808  (kept, copy) = pair
809  h(fits)
810
811def storage_shift(-shape: Shape.Shape, -s: Storage.Storage, -t: Storage.Storage, e: {s == t : Storage.Storage},
812  -R: @st: Storage.Storage -> @-k: {Lifecycle.logical_length(st) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> Type,
813  h: @-k: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(s, k)) ->
814  @-k: {Lifecycle.logical_length(t) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(t, k):
815  %e : (@-k: {Lifecycle.logical_length(_) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(_, k))
816  h
817
818
819# What the rest of the product asks of one input's `take`: the kept tensor,
820# replayed with a history that keeps its words, and the copy the build reads,
821# with its source.
822def InputAt(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, -s: Storage.Storage,
823  -Q: Core.Dynamic & Array<F32> -> Type) -> Type:
824  @+kept: List<&2, StorageLaws.Op> ->
825  @values: (@+other: U32 -> {Replayed.value(shape, fill, kept, other) == Replayed.value(shape, fill, ops, other) : F32}) ->
826  @words: {Laws.words(shape, fill, kept, Shape.logical_numel(Shape.dimensions(shape))) == Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))) : List<&2, F32>} ->
827  @+h: List<&2, Api.Effect> -> @+d: Nat -> @+f: F32 -> @+source: Source<shape, fill, ops, h, d, f> ->
828  @-kept_fits: {Lifecycle.logical_length(StorageLaws.replay(kept, s)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
829    Q((Core.Packed{shape, Core.TTensor{StorageLaws.replay(kept, s), kept_fits}}, Api.arr(h, d, f)))
830
831def input_take(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, -Q: Core.Dynamic & Array<F32> -> Type,
832  h: InputAt(shape, fill, ops, StorageLaws.created(Shape.count(shape), fill), Q)) ->
833  @-fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
834  Q(Elementwise.take(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})):
835  Owned.created_lift(Shape.count(shape), fill, Conversion.shape_count_within(shape),
836    s => (InputAt(shape, fill, ops, s, Q) -> @-fits: {Lifecycle.logical_length(StorageLaws.replay(ops, s)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
837      Q(Elementwise.take(Core.Packed{shape, Core.TTensor{StorageLaws.replay(ops, s), fits}}))),
838    zero => k => fits =>
839      storage_shift(shape, Storage.Empty{}, StorageLaws.replay(ops, Storage.Empty{}),
840        Equal.sym(Storage.Storage, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops)),
841        st => kk => Q(Elementwise.take(Core.Packed{shape, Core.TTensor{st, kk}})),
842        kk => storage_shift(shape, StorageLaws.replay(ops, Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(ops),
843          st => k2 => Q((Core.Packed{shape, Core.TTensor{st, k2}}, Array.new(F32, 0n, 0.0))),
844          k2 => k(ops)(other => {==})({==})(Nil{})(0n)(0.0)(NoCells{zero})(k2))(kk))(fits),
845    d => fits_d => f => k => fits =>
846      Owned.replay_lift(ops, d, U32.to_nat(Shape.count(shape)), fill, Nil{}, Api.hit_of(U32.to_nat(Shape.count(shape)), ops), {==},
847        ArrayCore.new_balanced(F32, d, fill), f, fits_d,
848        st => (@-fits: {Lifecycle.logical_length(st) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
849          (@-kk: {Lifecycle.logical_length(StorageLaws.step(st, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
850            Q((Core.Packed{shape, Core.TTensor{StorageLaws.step(st, StorageLaws.First{}), kk}}, Api.arr(history(shape, ops), d, fill)))) ->
851          Q(Elementwise.take(Core.Packed{shape, Core.TTensor{st, fits}}))),
852        c => fits2 => kc =>
853          take_owned_lift(shape, d, U32.to_nat(Shape.count(shape)), Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill),
854            Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill)), {==}, c, f, fits2, Q, kc))(fits)(
855        storage_shift(shape,
856          StorageLaws.replay(Replayed.snoc(ops, StorageLaws.First{}), Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}),
857          StorageLaws.step(StorageLaws.replay(ops, Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}), StorageLaws.First{}),
858          FromValues.replay_snoc(ops, StorageLaws.First{}, Storage.Owned{d, U32.to_nat(Shape.count(shape)), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f}),
859          st => kk => Q((Core.Packed{shape, Core.TTensor{st, kk}}, Api.arr(history(shape, ops), d, fill))),
860          k(Replayed.snoc(ops, StorageLaws.First{}))(other => half_keeps(shape, fill, ops, other))(words_first(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))))(
861            history(shape, ops))(d)(fill)(Normal{fits_d, {==}, {==}}))))(h)