src/autograd/reduce_replayed_proof.bend

bendtorch-core@0.1.0.0 · 1,116 lines · 70 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/storage/array.bend as ArrayCore
9import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
10import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
11import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
12import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
13import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
14import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
15import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
16import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
17import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
18import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
19import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
20import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
21import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
22import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
23import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
24import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
25import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
26import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as Par
27import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
28import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
29import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
30import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
31import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber
32import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel
33
34# The parallel reduce over a replayed contribution. Its output is the
35# replayed storage that writes, in index order, each target cell's fiber
36# sum: the contribution's replayed words at the offsets the cell's walk
37# reads, added in order from +0.0.
38
39def PlanMap(+plan: Shape.BroadcastPlan) -> Data:
40  Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>
41
42# The replayed words at a list of offsets, added in order.
43def rfold(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, positions: List<&2, Nat>, accumulator: F32) -> F32:
44  match positions:
45    case Nil{}:
46      accumulator
47    case position <> rest:
48      rfold(shape, fill, ops, rest, F32.add(accumulator, Replayed.value(shape, fill, ops, U32.from_nat(position))))
49
50def map_word(+plan: Shape.BroadcastPlan, map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +position: Nat) -> F32:
51  match map:
52    case Shape.Unindexed{zero}:
53      0.0
54    case Shape.Indexed{+rows, exact}:
55      rfold(shape, fill, ops, ReduceParallel.visited_of(rows, Shape.extents(Shape.output_shape(plan)), position), 0.0)
56
57def cell_word(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +position: Nat) -> F32:
58  map_word(plan, map, shape, fill, ops, position)
59
60def writes(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) -> List<&2, StorageLaws.Op>:
61  match count:
62    case 0n:
63      Nil{}
64    case 1n+previous:
65      Replayed.snoc(writes(plan, map, shape, fill, ops, previous),
66        StorageLaws.Write{U32.from_nat(previous), cell_word(plan, map, shape, fill, ops, previous)})
67
68def writes_value(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
69  below: {Nat.is_lt(U32.to_nat(index), count) == True{} : Bool},
70  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
71  {Replayed.value(output, 0.0, writes(plan, map, shape, fill, ops, count), index) ==
72    cell_word(plan, map, shape, fill, ops, U32.to_nat(index)) : F32}:
73  match count:
74    case 0n:
75      Empty.absurd({Replayed.value(output, 0.0, Nil{}, index) ==
76        cell_word(plan, map, shape, fill, ops, U32.to_nat(index)) : F32},
77        Arith.lt_zero(U32.to_nat(index), below))
78    case 1n+previous:
79      PointwiseProof.write_split(output, writes(plan, map, shape, fill, ops, previous),
80        previous, cell_word(plan, map, shape, fill, ops, previous), index,
81        cell_word(plan, map, shape, fill, ops, U32.to_nat(index)),
82        below, room,
83        at => Equal.cong(Nat, F32, position => cell_word(plan, map, shape, fill, ops, position),
84          previous, U32.to_nat(index), Equal.sym(Nat, U32.to_nat(index), previous, at)),
85        earlier => writes_value(plan, map, shape, fill, ops, output, previous, index, earlier,
86          Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room)),
87        Shape.bool_case(Nat.is_eq(U32.to_nat(index), previous)))
88
89def lt_not_eq(+a: Nat, +b: Nat, below: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
90  match a b:
91    case 0n 0n:
92      Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, Arith.clash(below))
93    case 0n 1n+q:
94      {==}
95    case 1n+p 0n:
96      {==}
97    case 1n+p 1n+q:
98      lt_not_eq(p, q, below)
99
100# A write at an index below `index` leaves the word at `index`.
101def write_skip(+shape: Shape.Shape, +previous: Nat, +index: U32, +word: F32, +old: F32,
102  +room: {Nat.is_lt(previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
103  later: {Nat.is_lt(previous, U32.to_nat(index)) == True{} : Bool}) ->
104  {StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), word}, index, old) == old : F32}:
105  %Equal.sym(Nat, U32.to_nat(U32.from_nat(previous)), previous, MatrixIndex.word_exact(previous, shape, room)) :
106    {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}
107  %Equal.sym(Bool, Nat.is_lt(previous, U32.to_nat(Shape.count(shape))), True{}, PointwiseProof.lt_count(previous, shape, room)) :
108    {Bool.pick(F32, Bool.and(_, Nat.is_eq(previous, U32.to_nat(index))), word, old) == old : F32}
109  %Equal.sym(Bool, Nat.is_eq(previous, U32.to_nat(index)), False{}, lt_not_eq(previous, U32.to_nat(index), later)) :
110    {Bool.pick(F32, _, word, old) == old : F32}
111  {==}
112
113# At or above the count, the writes leave the +0.0 fill.
114def writes_zero(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
115  +above: {Nat.is_le(count, U32.to_nat(index)) == True{} : Bool},
116  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
117  {Replayed.value(output, 0.0, writes(plan, map, shape, fill, ops, count), index) == 0.0 : F32}:
118  match count:
119    case 0n:
120      {==}
121    case 1n+previous:
122      +history = writes(plan, map, shape, fill, ops, previous)
123      +word = cell_word(plan, map, shape, fill, ops, previous)
124      +op = {StorageLaws.Write{U32.from_nat(previous), word} : StorageLaws.Op}
125      Equal.trans(F32, Replayed.value(output, 0.0, Replayed.snoc(history, op), index),
126        StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)), 0.0,
127        Replayed.expected_snoc(history, op, U32.to_nat(Shape.count(output)), index, 0.0),
128        Equal.trans(F32, StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)),
129          Replayed.value(output, 0.0, history, index), 0.0,
130          write_skip(output, previous, index, word, Replayed.value(output, 0.0, history, index),
131            Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(output)), room),
132            Conversion.le_successor_lt(previous, U32.to_nat(index), above)),
133          writes_zero(plan, map, shape, fill, ops, output, previous, index,
134            Conversion.le_predecessor(previous, U32.to_nat(index), above),
135            Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room))))
136
137def lt_zero_false(+x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
138  match x:
139    case 0n:
140      {==}
141    case 1n+p:
142      {==}
143
144def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
145  match k:
146    case 0n:
147      {==}
148    case 1n+p:
149      lt_self_succ(p)
150
151def lt_succ_right(+b: Nat, +k: Nat, h: {Nat.is_lt(b, k) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == True{} : Bool}:
152  match b k:
153    case 0n _:
154      {==}
155    case 1n+p 0n:
156      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, Arith.clash(h))
157    case 1n+p 1n+q:
158      lt_succ_right(p, q, h)
159
160# k < b gives b < 1 + k false.
161def above_false(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == False{} : Bool}:
162  match k b:
163    case 0n 0n:
164      Empty.absurd({Nat.is_lt(0n, 1n) == False{} : Bool}, Arith.clash(h))
165    case 0n 1n+q:
166      lt_zero_false(q)
167    case 1n+p 0n:
168      Empty.absurd({Nat.is_lt(0n, 1n+(1n+p)) == False{} : Bool}, Arith.clash(h))
169    case 1n+p 1n+q:
170      above_false(p, q, h)
171
172def lt_asym(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, k) == False{} : Bool}:
173  match k b:
174    case 0n 0n:
175      {==}
176    case 0n 1n+q:
177      {==}
178    case 1n+p 0n:
179      Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, Arith.clash(h))
180    case 1n+p 1n+q:
181      lt_asym(p, q, h)
182
183# 1 + b <= k gives b < k.
184def below_true(+b: Nat, +k: Nat, h: {Nat.is_le(1n+b, k) == True{} : Bool}) -> {Nat.is_lt(b, k) == True{} : Bool}:
185  match b k:
186    case 0n 0n:
187      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.clash(h))
188    case 0n 1n+q:
189      {==}
190    case 1n+p 0n:
191      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, Arith.clash(h))
192    case 1n+p 1n+q:
193      below_true(p, q, h)
194
195def lt_add_right(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_lt(a, c) == True{} : Bool}) ->
196  {Nat.is_lt(Nat.add(a, b), Nat.add(c, b)) == True{} : Bool}:
197  match a c:
198    case 0n 0n:
199      Empty.absurd({Nat.is_lt(b, b) == True{} : Bool}, Arith.clash(h))
200    case 0n 1n+q:
201      Arith.lt_succ(b, Nat.add(q, b), Api.le_add_left(q, b))
202    case 1n+p 0n:
203      Empty.absurd({Nat.is_lt(1n+Nat.add(p, b), b) == True{} : Bool}, Arith.clash(h))
204    case 1n+p 1n+q:
205      lt_add_right(p, q, b, h)
206
207def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
208  {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
209  match c:
210    case 0n:
211      h
212    case 1n+r:
213      le_add_cong(r, x, y, h)
214
215def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) ->
216  {Nat.is_le(a, c) == True{} : Bool}:
217  match a b c:
218    case 0n _ _:
219      Arith.le_zero(c)
220    case 1n+p 0n _:
221      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, Arith.clash(ab))
222    case 1n+p 1n+q 0n:
223      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, Arith.clash(bc))
224    case 1n+p 1n+q 1n+r:
225      le_trans(p, q, r, ab, bc)
226
227def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
228  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
229  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
230    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))
231
232def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
233  match number:
234    case 0n:
235      {==}
236    case 1n+p:
237      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero_right(p))
238
239# A word index below the storage length is the offset of its own route.
240def output_position(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool},
241  +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
242  {Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n) == U32.to_nat(index) : Nat}:
243  +rest = Arith.and_right(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid)
244  Equal.trans(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
245    add_zero_right(Model.offset(depth, Refinement.route(depth, index))),
246    Equal.sym(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)),
247      Route.route_offset(depth, index,
248        Arith.and_left(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid),
249        Arith.lt_le_trans(U32.to_nat(index), length, Model.capacity(depth), inside,
250          Arith.and_right(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth)), rest)))))
251
252
253# The output spec: cell `base` of the tree holds the cell's word below
254# `count` and +0.0 above it.
255
256def out_leaf(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +position: Nat, inside: Bool) -> F32:
257  match inside:
258    case False{}:
259      0.0
260    case True{}:
261      cell_word(plan, map, shape, fill, ops, position)
262
263def out_spec(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Array<F32>:
264  match depth:
265    case 0n:
266      ALeaf{out_leaf(plan, map, shape, fill, ops, base, Nat.is_lt(base, count))}
267    case 1n+inner:
268      ANode{out_spec(plan, map, shape, fill, ops, count, inner, base), out_spec(plan, map, shape, fill, ops, count, inner, Nat.add(Model.capacity(inner), base))}
269
270def out_balanced(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Model.Balanced(F32, depth, out_spec(plan, map, shape, fill, ops, count, depth, base)):
271  match depth:
272    case 0n:
273      Unit{}
274    case 1n+inner:
275      (out_balanced(plan, map, shape, fill, ops, count, inner, base), out_balanced(plan, map, shape, fill, ops, count, inner, Nat.add(Model.capacity(inner), base)))
276
277def new_spec(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +depth: Nat, +base: Nat) -> {Array.new(F32, depth, 0.0) == out_spec(plan, map, shape, fill, ops, 0n, depth, base) : Array<F32>}:
278  match depth:
279    case 0n:
280      %Equal.sym(Bool, Nat.is_lt(base, 0n), False{}, lt_zero_false(base)) :
281        {ALeaf{0.0} == ALeaf{out_leaf(plan, map, shape, fill, ops, base, _)} : Array<F32>}
282      {==}
283    case 1n+inner:
284      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(plan, map, shape, fill, ops, 0n, inner, base), new_spec(plan, map, shape, fill, ops, inner, base)) :
285        {ANode{_, Array.new(F32, inner, 0.0)} == out_spec(plan, map, shape, fill, ops, 0n, 1n+inner, base) : Array<F32>}
286      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(plan, map, shape, fill, ops, 0n, inner, Nat.add(Model.capacity(inner), base)),
287        new_spec(plan, map, shape, fill, ops, inner, Nat.add(Model.capacity(inner), base))) :
288        {ANode{out_spec(plan, map, shape, fill, ops, 0n, inner, base), _} == out_spec(plan, map, shape, fill, ops, 0n, 1n+inner, base) : Array<F32>}
289      {==}
290
291# A subtree whose positions all lie above k is the same for k and 1 + k.
292def above(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_lt(k, b) == True{} : Bool}) ->
293  {out_spec(plan, map, shape, fill, ops, k, depth, b) == out_spec(plan, map, shape, fill, ops, 1n+k, depth, b) : Array<F32>}:
294  match depth:
295    case 0n:
296      %Equal.sym(Bool, Nat.is_lt(b, k), False{}, lt_asym(k, b, h)) :
297        {ALeaf{out_leaf(plan, map, shape, fill, ops, b, _)} == ALeaf{out_leaf(plan, map, shape, fill, ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
298      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), False{}, above_false(k, b, h)) :
299        {ALeaf{0.0} == ALeaf{out_leaf(plan, map, shape, fill, ops, b, _)} : Array<F32>}
300      {==}
301    case 1n+inner:
302      +high = Nat.add(Model.capacity(inner), b)
303      %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, b), out_spec(plan, map, shape, fill, ops, 1n+k, inner, b), above(plan, map, shape, fill, ops, k, inner, b, h)) :
304        {ANode{_, out_spec(plan, map, shape, fill, ops, k, inner, high)} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, b) : Array<F32>}
305      %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, high), out_spec(plan, map, shape, fill, ops, 1n+k, inner, high),
306        above(plan, map, shape, fill, ops, k, inner, high, Arith.lt_le_trans(k, b, high, h, Api.le_add_left(Model.capacity(inner), b)))) :
307        {ANode{out_spec(plan, map, shape, fill, ops, 1n+k, inner, b), _} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, b) : Array<F32>}
308      {==}
309
310# A subtree whose positions all lie below k is the same for k and 1 + k.
311def below(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(Model.capacity(depth), b), k) == True{} : Bool}) ->
312  {out_spec(plan, map, shape, fill, ops, k, depth, b) == out_spec(plan, map, shape, fill, ops, 1n+k, depth, b) : Array<F32>}:
313  match depth:
314    case 0n:
315      +lower = below_true(b, k, h)
316      %Equal.sym(Bool, Nat.is_lt(b, k), True{}, lower) :
317        {ALeaf{out_leaf(plan, map, shape, fill, ops, b, _)} == ALeaf{out_leaf(plan, map, shape, fill, ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
318      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), True{}, lt_succ_right(b, k, lower)) :
319        {ALeaf{cell_word(plan, map, shape, fill, ops, b)} == ALeaf{out_leaf(plan, map, shape, fill, ops, b, _)} : Array<F32>}
320      {==}
321    case 1n+inner:
322      +c = Model.capacity(inner)
323      +high = Nat.add(c, b)
324      +nested = Equal.trans(Bool, Nat.is_le(Nat.add(c, high), k), Nat.is_le(Nat.add(Nat.add(c, c), b), k), True{},
325        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)
326      +low_h = le_trans(high, Nat.add(c, high), k, le_add_cong(c, b, high, Api.le_add_left(c, b)), nested)
327      %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, b), out_spec(plan, map, shape, fill, ops, 1n+k, inner, b), below(plan, map, shape, fill, ops, k, inner, b, low_h)) :
328        {ANode{_, out_spec(plan, map, shape, fill, ops, k, inner, high)} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, b) : Array<F32>}
329      %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, high), out_spec(plan, map, shape, fill, ops, 1n+k, inner, high), below(plan, map, shape, fill, ops, k, inner, high, nested)) :
330        {ANode{out_spec(plan, map, shape, fill, ops, 1n+k, inner, b), _} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, b) : Array<F32>}
331      {==}
332
333# Writing cell k at the path whose position is k turns the spec for k into
334# the spec for 1 + k.
335def write_spec(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +base: Nat, +path: Model.Path(depth),
336  +h: {Nat.add(Model.offset(depth, path), base) == k : Nat}) ->
337  {ArrayCore.write_path(F32, depth, out_spec(plan, map, shape, fill, ops, k, depth, base), path, cell_word(plan, map, shape, fill, ops, k)) == out_spec(plan, map, shape, fill, ops, 1n+k, depth, base) : Array<F32>}:
338  match depth:
339    case 0n:
340      %h : {ALeaf{cell_word(plan, map, shape, fill, ops, _)} == ALeaf{out_leaf(plan, map, shape, fill, ops, base, Nat.is_lt(base, 1n+_))} : Array<F32>}
341      %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, lt_self_succ(base)) :
342        {ALeaf{cell_word(plan, map, shape, fill, ops, base)} == ALeaf{out_leaf(plan, map, shape, fill, ops, base, _)} : Array<F32>}
343      {==}
344    case 1n+inner:
345      Model.Step{+bit, +rest} = path
346      match bit:
347        case False{}:
348          +c = Model.capacity(inner)
349          +high = Nat.add(c, base)
350          +inside = Equal.trans(Bool, Nat.is_lt(k, high), Nat.is_lt(Nat.add(Model.offset(inner, rest), base), high), True{},
351            Equal.cong(Nat, Bool, x => Nat.is_lt(x, high), k, Nat.add(Model.offset(inner, rest), base),
352              Equal.sym(Nat, Nat.add(Model.offset(inner, rest), base), k, h)),
353            lt_add_right(Model.offset(inner, rest), c, base, Api.offset_lt(inner, rest)))
354          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(plan, map, shape, fill, ops, k, inner, base), rest, cell_word(plan, map, shape, fill, ops, k)),
355            out_spec(plan, map, shape, fill, ops, 1n+k, inner, base), write_spec(plan, map, shape, fill, ops, k, inner, base, rest, h)) :
356            {ANode{_, out_spec(plan, map, shape, fill, ops, k, inner, high)} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, base) : Array<F32>}
357          %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, high), out_spec(plan, map, shape, fill, ops, 1n+k, inner, high), above(plan, map, shape, fill, ops, k, inner, high, inside)) :
358            {ANode{out_spec(plan, map, shape, fill, ops, 1n+k, inner, base), _} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, base) : Array<F32>}
359          {==}
360        case True{}:
361          +c = Model.capacity(inner)
362          +high = Nat.add(c, base)
363          +off = Model.offset(inner, rest)
364          +lower = Equal.trans(Bool, Nat.is_le(high, k), Nat.is_le(high, Nat.add(c, Nat.add(off, base))), True{},
365            Equal.cong(Nat, Bool, x => Nat.is_le(high, x), k, Nat.add(c, Nat.add(off, base)),
366              Equal.trans(Nat, k, Nat.add(Nat.add(c, off), base), Nat.add(c, Nat.add(off, base)),
367                Equal.sym(Nat, Nat.add(Nat.add(c, off), base), k, h),
368                Equal.sym(Nat, Nat.add(c, Nat.add(off, base)), Nat.add(Nat.add(c, off), base), Index.add_assoc(c, off, base)))),
369            le_add_cong(c, base, Nat.add(off, base), Api.le_add_left(off, base)))
370          +shifted = Equal.trans(Nat, Nat.add(off, high), Nat.add(Nat.add(c, off), base), k, position_step(c, off, base), h)
371          %Equal.sym(Array<F32>, out_spec(plan, map, shape, fill, ops, k, inner, base), out_spec(plan, map, shape, fill, ops, 1n+k, inner, base), below(plan, map, shape, fill, ops, k, inner, base, lower)) :
372            {ANode{_, ArrayCore.write_path(F32, inner, out_spec(plan, map, shape, fill, ops, k, inner, high), rest, cell_word(plan, map, shape, fill, ops, k))} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, base) : Array<F32>}
373          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(plan, map, shape, fill, ops, k, inner, high), rest, cell_word(plan, map, shape, fill, ops, k)),
374            out_spec(plan, map, shape, fill, ops, 1n+k, inner, high), write_spec(plan, map, shape, fill, ops, k, inner, high, rest, shifted)) :
375            {ANode{out_spec(plan, map, shape, fill, ops, 1n+k, inner, base), _} == out_spec(plan, map, shape, fill, ops, 1n+k, 1n+inner, base) : Array<F32>}
376          {==}
377
378# The family history, replayed on the owned storage that `created` makes,
379# is the owned storage that holds the output spec.
380def chain(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
381  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
382  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
383  {StorageLaws.replay(writes(plan, map, shape, fill, 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(plan, map, shape, fill, ops, k, d, 0n), out_balanced(plan, map, shape, fill, ops, k, d, 0n), f} : Storage.Storage}:
384  match k:
385    case 0n:
386      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(plan, map, shape, fill, ops, 0n, d, 0n), new_spec(plan, map, shape, fill, ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
387        out_balanced(plan, map, shape, fill, ops, 0n, d, 0n))
388    case 1n+j:
389      +index = U32.from_nat(j)
390      +value = cell_word(plan, map, shape, fill, ops, j)
391      +below_n = Conversion.le_successor_lt(j, n, room)
392      +exact = Conversion.natural_word_exact(j, limit, le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
393      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
394        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
395      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
396        output_position(d, n, index, fits, inside), exact)
397      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), Refinement.route(d, index), value),
398        out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, out_balanced(plan, map, shape, fill, ops, j, d, 0n)),
399        write_spec(plan, map, shape, fill, ops, j, d, 0n, Refinement.route(d, index), offset))
400      Equal.trans(Storage.Storage, StorageLaws.replay(writes(plan, map, shape, fill, ops, 1n+j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
401        StorageLaws.step(StorageLaws.replay(writes(plan, map, shape, fill, ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
402        Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f},
403        FromValues.replay_snoc(writes(plan, map, shape, fill, ops, j), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
404        %Equal.sym(Storage.Storage, StorageLaws.replay(writes(plan, map, shape, fill, 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(plan, map, shape, fill, ops, j, d, 0n), out_balanced(plan, map, shape, fill, ops, j, d, 0n), f},
405          chain(plan, map, shape, fill, ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
406          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
407        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
408          Storage.set_checked(d, n, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n), f),
409          (Storage.Owned{d, n, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value),
410            Certificates.set_result(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n)), f}, Done{Unit{}}),
411          Api.set_checked_hit(d, n, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n), f,
412            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
413          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
414        Owned.owned_eq(d, n, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), written,
415          Certificates.set_result(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n)), f)(
416          out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n)))
417
418
419
420# The walk over the copy of a replayed contribution adds its replayed words.
421
422def below_front(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +bound: Nat,
423  +h: {ReduceParallel.all_below(List.append(&2, Nat, xs, ys), bound) == True{} : Bool}) ->
424  {ReduceParallel.all_below(xs, bound) == True{} : Bool}:
425  match xs:
426    case Nil{}:
427      {==}
428    case +x <> +rest:
429      +here = Arith.and_left(Nat.is_lt(x, bound), ReduceParallel.all_below(List.append(&2, Nat, rest, ys), bound), h)
430      +later = Arith.and_right(Nat.is_lt(x, bound), ReduceParallel.all_below(List.append(&2, Nat, rest, ys), bound), h)
431      %Equal.sym(Bool, Nat.is_lt(x, bound), True{}, here) : {Bool.and(_, ReduceParallel.all_below(rest, bound)) == True{} : Bool}
432      below_front(rest, ys, bound, later)
433
434def below_back(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +bound: Nat,
435  +h: {ReduceParallel.all_below(List.append(&2, Nat, xs, ys), bound) == True{} : Bool}) ->
436  {ReduceParallel.all_below(ys, bound) == True{} : Bool}:
437  match xs:
438    case Nil{}:
439      h
440    case +x <> +rest:
441      below_back(rest, ys, bound, Arith.and_right(Nat.is_lt(x, bound), ReduceParallel.all_below(List.append(&2, Nat, rest, ys), bound), h))
442
443def rfold_append(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +accumulator: F32) ->
444  {rfold(shape, fill, ops, List.append(&2, Nat, xs, ys), accumulator) == rfold(shape, fill, ops, ys, rfold(shape, fill, ops, xs, accumulator)) : F32}:
445  match xs:
446    case Nil{}:
447      {==}
448    case +x <> +rest:
449      rfold_append(shape, fill, ops, rest, ys, F32.add(accumulator, Replayed.value(shape, fill, ops, U32.from_nat(x))))
450
451def leaf_eq(+base: Nat, +accumulator: F32, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
452  +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +source: Par.Source<shape, fill, ops, h, d, f>,
453  +below: {Nat.is_lt(base, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
454  pair: Array<F32> & F32, +exact: {pair == Array.get(F32, Api.arr(h, d, f), U32.from_nat(base)) : Array<F32> & F32}) ->
455  {Reduce.leaf_add(accumulator, pair) == (rfold(shape, fill, ops, [base], accumulator), Api.arr(h, d, f)) : F32 & Array<F32>}:
456  (kept, word) = pair
457  Owned.pair_eq(F32, Array<F32>, F32.add(accumulator, word), F32.add(accumulator, Replayed.value(shape, fill, ops, U32.from_nat(base))),
458    kept, Api.arr(h, d, f),
459    Equal.cong(F32, F32, w => F32.add(accumulator, w), word, Replayed.value(shape, fill, ops, U32.from_nat(base)),
460      Par.source_read(shape, fill, ops, h, d, f, source, U32.from_nat(base), Par.index_inside(shape, base, below), (kept, word), exact)),
461    Build.got_kept(d, h, f, U32.from_nat(base), (kept, word), exact))
462
463def next_eq(-rec: F32 -> Array<F32> -> F32 & Array<F32>, -low: F32 & Array<F32>, -value: F32, -array: Array<F32>,
464  +first: {low == (value, array) : F32 & Array<F32>}) -> {Reduce.walk_next(rec, low) == rec(value, array) : F32 & Array<F32>}:
465  %Equal.sym(F32 & Array<F32>, low, (value, array), first) : {Reduce.walk_next(rec, _) == rec(value, array) : F32 & Array<F32>}
466  {==}
467
468def fiber_eq(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
469  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32,
470  +source: Par.Source<shape, fill, ops, h, d, f>,
471  +below: {ReduceParallel.all_below(Fiber.visited(rows, extents, fuel, target, base, digit), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
472  {Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, Api.arr(h, d, f)) ==
473    (rfold(shape, fill, ops, Fiber.visited(rows, extents, fuel, target, base, digit), accumulator), Api.arr(h, d, f)) : F32 & Array<F32>}:
474  match rows extents fuel:
475    case Nil{} _ _:
476      leaf_eq(base, accumulator, shape, fill, ops, h, d, f, source,
477        Arith.and_left(Nat.is_lt(base, Shape.logical_numel(Shape.dimensions(shape))), True{}, below),
478        Array.get(F32, Api.arr(h, d, f), U32.from_nat(base)), {==})
479    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n:
480      {==}
481    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining:
482      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
483      +extents : List<&2, Nat> = extent <> others
484      +inner = Nat.mod(target, left)
485      +offset = Nat.add(base, Nat.mul(right, digit))
486      +low = Fiber.visited(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner))
487      +high = Fiber.visited(rows, extents, remaining, target, base, 1n+digit)
488      +bound = Shape.logical_numel(Shape.dimensions(shape))
489      +value = rfold(shape, fill, ops, low, accumulator)
490      Equal.trans(F32 & Array<F32>,
491        Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
492          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f))),
493        Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, value, Api.arr(h, d, f)),
494        (rfold(shape, fill, ops, List.append(&2, Nat, low, high), accumulator), Api.arr(h, d, f)),
495        next_eq(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
496          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)),
497          value, Api.arr(h, d, f),
498          fiber_eq(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator,
499            shape, fill, ops, h, d, f, source, below_front(low, high, bound, below))),
500        %Equal.sym(F32, rfold(shape, fill, ops, List.append(&2, Nat, low, high), accumulator), rfold(shape, fill, ops, high, value),
501          rfold_append(shape, fill, ops, low, high, accumulator)) :
502          {Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, value, Api.arr(h, d, f)) == (_, Api.arr(h, d, f)) : F32 & Array<F32>}
503        fiber_eq(rows, extents, remaining, target, base, 1n+digit, value, shape, fill, ops, h, d, f, source, below_back(low, high, bound, below)))
504    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _:
505      {==}
506
507# The facts of `ReduceParallel.fast_fiber`, stated for the replayed arrays
508# `Api.arr`, which a proof can name as often as it needs: a read of
509# `Api.arr(h, d, f)` hands back that array, next to the word it read.
510def eta(pair: Array<F32> & F32) -> {pair == (Refinement.first(F32, pair), Refinement.second(F32, pair)) : Array<F32> & F32}:
511  match pair:
512    case Tuple{x, y}:
513      {==}
514
515def got(+h: List<&2, Api.Effect>, +d: Nat, +f: F32, +i: U32) ->
516  {Array.get(F32, Api.arr(h, d, f), i) == (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))) : Array<F32> & F32}:
517  Equal.trans(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), i),
518    (Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
519    (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
520    eta(Array.get(F32, Api.arr(h, d, f), i)),
521    Equal.cong(Array<F32>, Array<F32> & F32, a => (a, Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
522      Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Api.arr(h, d, f),
523      Refinement.law_get_retains(F32, d, Api.arr(h, d, f), i, Api.bal(h, d, f))))
524
525def single_arr(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +single: {Reduce.single_rows(rows, extents) == True{} : Bool},
526  +target: Nat, +base: Nat, +accumulator: F32, +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
527  {Reduce.fiber(rows, extents, Reduce.first_span(rows, extents), target, base, Reduce.first_digit(rows, target), accumulator, Api.arr(h, d, f)) ==
528    Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rows, extents, target, base)))) : F32 & Array<F32>}:
529  match rows extents:
530    case Nil{} +extents:
531      {==}
532    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others:
533      +one = ReduceParallel.span_one(left, extent, Arith.and_left(Nat.is_eq(Reduce.span(left, extent), 1n), Reduce.single_rows(rest, others), single))
534      +inner = Nat.mod(target, left)
535      +offset = Nat.add(base, Nat.mul(right, Nat.div(target, left)))
536      %Equal.sym(Nat, Reduce.span(left, extent), 1n, one) :
537        {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, _, target, base, Nat.div(target, left), accumulator, Api.arr(h, d, f)) ==
538          Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>}
539      Equal.trans(F32 & Array<F32>,
540        Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+Nat.div(target, left), v, k),
541          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f))),
542        Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+Nat.div(target, left), v, k),
543          Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
544        Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
545        Equal.cong(F32 & Array<F32>, F32 & Array<F32>,
546          p => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+Nat.div(target, left), v, k), p),
547          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)),
548          Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
549          single_arr(rest, others, Arith.and_right(Nat.is_eq(Reduce.span(left, extent), 1n), Reduce.single_rows(rest, others), single),
550            inner, offset, accumulator, h, d, f)),
551        ReduceParallel.leaf_kept(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+Nat.div(target, left), v, k),
552          value => kept => {==}, accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))))
553    case Shape.Row{+stride, +left, +right} <> +rest Nil{}:
554      Empty.absurd({Reduce.fiber(Shape.Row{stride, left, right} <> rest, Nil{}, Reduce.first_span(Shape.Row{stride, left, right} <> rest, Nil{}), target, base,
555        Reduce.first_digit(Shape.Row{stride, left, right} <> rest, target), accumulator, Api.arr(h, d, f)) ==
556        Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(Shape.Row{stride, left, right} <> rest, Nil{}, target, base)))) :
557        F32 & Array<F32>}, Arith.clash(single))
558
559# The word a strided read of `Api.arr(h, d, f)` gets.
560def word_at(+h: List<&2, Api.Effect>, +d: Nat, +f: F32, +at: Nat) -> F32:
561  Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)))
562
563def step_arr(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
564  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
565  +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
566  {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, Api.arr(h, d, f)) ==
567    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit,
568      F32.add(accumulator, word_at(h, d, f, Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))),
569      Api.arr(h, d, f)) : F32 & Array<F32>}:
570  +inner = Nat.mod(target, left)
571  +lift = Reduce.single_offset(rest, others, inner, 0n)
572  +offset = Nat.add(base, Nat.mul(right, digit))
573  +at = Reduce.strided_offset(right, base, digit, lift)
574  Equal.trans(F32 & Array<F32>,
575    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
576      Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f))),
577    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
578      Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
579    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
580      Reduce.leaf_add(accumulator, (Api.arr(h, d, f), word_at(h, d, f, at)))),
581    Equal.cong(F32 & Array<F32>, F32 & Array<F32>,
582      p => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k), p),
583      Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)),
584      Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
585      single_arr(rest, others, single, inner, offset, accumulator, h, d, f)),
586    Equal.trans(F32 & Array<F32>,
587      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
588        Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
589      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
590        Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)))),
591      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
592        Reduce.leaf_add(accumulator, (Api.arr(h, d, f), word_at(h, d, f, at)))),
593      Equal.cong(Nat, F32 & Array<F32>,
594        n => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
595          Reduce.leaf_add(accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(n)))),
596        Reduce.single_offset(rest, others, inner, offset), at, ReduceParallel.offset_shift(rest, others, inner, offset)),
597      Equal.cong(Array<F32> & F32, F32 & Array<F32>,
598        p => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
599          Reduce.leaf_add(accumulator, p)),
600        Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)),
601        got(h, d, f, U32.from_nat(at)))))
602
603def run_arr(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
604  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
605  +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
606  {Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator,
607    Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n))))) ==
608    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}:
609  match fuel:
610    case 0n:
611      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
612      +at = Reduce.strided_offset(right, base, digit, lift)
613      %Equal.sym(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) :
614        {Reduce.strided_run(0n, right, base, digit, lift, accumulator, _) ==
615          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}
616      Equal.sym(F32 & Array<F32>,
617        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)),
618        (F32.add(accumulator, word_at(h, d, f, at)), Api.arr(h, d, f)),
619        step_arr(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, h, d, f))
620    case 1n+remaining:
621      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
622      +at = Reduce.strided_offset(right, base, digit, lift)
623      +next = F32.add(accumulator, word_at(h, d, f, at))
624      %Equal.sym(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) :
625        {Reduce.strided_run(1n+remaining, right, base, digit, lift, accumulator, _) ==
626          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}
627      Equal.trans(F32 & Array<F32>,
628        Reduce.strided_run(remaining, right, base, 1n+digit, lift, next,
629          Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))),
630        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, next, Api.arr(h, d, f)),
631        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)),
632        run_arr(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, next, h, d, f),
633        Equal.sym(F32 & Array<F32>,
634          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)),
635          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, next, Api.arr(h, d, f)),
636          step_arr(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, h, d, f)))
637
638def strided_arr(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
639  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
640  +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
641  {Reduce.strided(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, Api.arr(h, d, f)) ==
642    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}:
643  match fuel:
644    case 0n:
645      {==}
646    case 1n+remaining:
647      run_arr(stride, left, right, rest, extent, others, single, remaining, target, base, digit, accumulator, h, d, f)
648
649# A fiber of `Api.arr(h, d, f)` hands that array back.
650def fiber_kept(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
651  +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
652  {Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, Api.arr(h, d, f)) ==
653    (Pair.fst(F32, Array<F32>, Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, Api.arr(h, d, f))), Api.arr(h, d, f)) : F32 & Array<F32>}:
654  match rows extents fuel:
655    case Nil{} _ _:
656      %Equal.sym(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(base)), (Api.arr(h, d, f), word_at(h, d, f, base)), got(h, d, f, U32.from_nat(base))) :
657        {Reduce.leaf_add(accumulator, _) == (Pair.fst(F32, Array<F32>, Reduce.leaf_add(accumulator, _)), Api.arr(h, d, f)) : F32 & Array<F32>}
658      {==}
659    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n:
660      {==}
661    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining:
662      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
663      +extents : List<&2, Nat> = extent <> others
664      +inner = Nat.mod(target, left)
665      +offset = Nat.add(base, Nat.mul(right, digit))
666      +value = Pair.fst(F32, Array<F32>, Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)))
667      %Equal.sym(F32 & Array<F32>, Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)), (value, Api.arr(h, d, f)),
668        fiber_kept(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, h, d, f)) :
669        {Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), _) ==
670          (Pair.fst(F32, Array<F32>, Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), _)), Api.arr(h, d, f)) :
671          F32 & Array<F32>}
672      fiber_kept(rows, extents, remaining, target, base, 1n+digit, value, h, d, f)
673    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _:
674      {==}
675
676def fast_arr(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, single: Bool, +ok: ReduceParallel.SingleOk(single, rows, extents),
677  +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32, +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
678  {Reduce.fiber_fast(rows, extents, fuel, single, target, base, digit, accumulator, Api.arr(h, d, f)) ==
679    Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}:
680  match rows extents fuel single:
681    case Nil{} _ _ single:
682      {==}
683    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others fuel True{}:
684      strided_arr(stride, left, right, rest, extent, others, ok, fuel, target, base, digit, accumulator, h, d, f)
685    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n False{}:
686      {==}
687    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining False{}:
688      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
689      +extents : List<&2, Nat> = extent <> others
690      +inner = Nat.mod(target, left)
691      +offset = Nat.add(base, Nat.mul(right, digit))
692      +value = Pair.fst(F32, Array<F32>, Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)))
693      %Equal.sym(F32 & Array<F32>,
694        Reduce.fiber_fast(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)),
695        Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)),
696        fast_arr(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others),
697          ReduceParallel.single_ok(rest, others, Reduce.single_below(rest, others), {==}), inner, offset, Reduce.first_digit(rest, inner), accumulator, h, d, f)) :
698        {Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k), _) ==
699          Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f))) : F32 & Array<F32>}
700      %Equal.sym(F32 & Array<F32>, Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)), (value, Api.arr(h, d, f)),
701        fiber_kept(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, h, d, f)) :
702        {Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k), _) ==
703          Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), _) : F32 & Array<F32>}
704      fast_arr(rows, extents, remaining, False{}, Unit{}, target, base, 1n+digit, value, h, d, f)
705    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _ single:
706      {==}
707
708# What the cells of the build need from the plan: the target is the plan's
709# left shape, with `count` cells, and the contribution is its right shape.
710type Facts<-plan: Shape.BroadcastPlan, -shape: Shape.Shape, -count: Nat> is Data:
711  Facts{count_left: {count == Shape.numel(Shape.extents(Shape.left_shape(plan))) : Nat},
712    right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}}
713
714# Every offset the walk of a cell below `count` reads lies inside the
715# contribution.
716def walk_below(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
717  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
718  +shape: Shape.Shape, +count: Nat, +facts: Facts<plan, shape, count>, +base: Nat, +inside: {Nat.is_lt(base, count) == True{} : Bool}) ->
719  {ReduceParallel.all_below(ReduceParallel.visited_of(rows, Shape.extents(Shape.output_shape(plan)), base), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
720  Facts{+count_left, +right} = facts
721  +output = Shape.extents(Shape.output_shape(plan))
722  +below_left : {Nat.is_lt(base, Shape.numel(Shape.extents(Shape.left_shape(plan)))) == True{} : Bool} =
723    %count_left : {Nat.is_lt(base, _) == True{} : Bool}
724    inside
725  %right : {ReduceParallel.all_below(ReduceParallel.visited_of(rows, output, base), Shape.logical_numel(_)) == True{} : Bool}
726  %ReduceParallel.plan_walk(plan, rows, rows_exact, base, below_left) :
727    {ReduceParallel.all_below(_, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool}
728  ReduceParallel.masked_below(plan, rows, rows_exact, base, Shape.numel(output), 0n, Conversion.le_reflexive(Shape.numel(output)))
729
730def TreeEq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
731  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
732  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +depth: Nat, +base: Nat,
733  -result: Array<F32> & (Array<F32> & Unit)) -> Type:
734  {Pair.fst(Array<F32>, Array<F32> & Unit, result) == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, depth, base) : Array<F32>} &
735    {Pair.snd(Array<F32>, Array<F32> & Unit, result) == (Api.arr(h, d, f), Unit{}) : Array<F32> & Unit}
736
737def cell_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
738  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
739  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat,
740  +source: Par.Source<shape, fill, ops, h, d, f>, +facts: Facts<plan, shape, count>, +base: Nat, inside: Bool,
741  +decided: {inside == Nat.is_lt(base, count) : Bool}) ->
742  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, base,
743    Parallel.leaf(~(Array<F32> & Unit), Reduce.keep(Reduce.cell(rows, Shape.extents(Shape.output_shape(plan)), base, Api.arr(h, d, f), inside), Unit{}))):
744  match inside:
745    case False{}:
746      (%decided : {ALeaf{0.0} == ALeaf{out_leaf(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, base, _)} : Array<F32>}
747       {==}, {==})
748    case True{}:
749      +output = Shape.extents(Shape.output_shape(plan))
750      +word = rfold(shape, fill, ops, ReduceParallel.visited_of(rows, output, base), 0.0)
751      %Equal.sym(F32 & Array<F32>, Reduce.fiber_of(rows, output, base, Api.arr(h, d, f)), (word, Api.arr(h, d, f)),
752        Equal.trans(F32 & Array<F32>, Reduce.fiber_of(rows, output, base, Api.arr(h, d, f)),
753          Reduce.fiber(rows, output, Reduce.first_span(rows, output), base, 0n, Reduce.first_digit(rows, base), 0.0, Api.arr(h, d, f)),
754          (word, Api.arr(h, d, f)),
755          fast_arr(rows, output, Reduce.first_span(rows, output), Reduce.single_below(rows, output),
756            ReduceParallel.single_ok(rows, output, Reduce.single_below(rows, output), {==}), base, 0n, Reduce.first_digit(rows, base), 0.0, h, d, f),
757          fiber_eq(rows, output, Reduce.first_span(rows, output), base, 0n, Reduce.first_digit(rows, base), 0.0, shape, fill, ops, h, d, f, source,
758            walk_below(plan, rows, rows_exact, shape, count, facts, base, Equal.sym(Bool, True{}, Nat.is_lt(base, count), decided))))) :
759        TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, base, Parallel.leaf(~(Array<F32> & Unit), Reduce.keep(_, Unit{})))
760      (%decided : {ALeaf{word} == ALeaf{out_leaf(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, base, _)} : Array<F32>}
761       {==}, {==})
762
763def tree_join_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
764  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
765  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +lower: Nat, +base: Nat,
766  -a: Array<F32>, high: Array<F32> & (Array<F32> & Unit),
767  ea: {a == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base) : Array<F32>},
768  facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, Nat.add(Model.capacity(lower), base), high)) ->
769  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n+lower, base, Parallel.join(~(Array<F32> & Unit), a, high)):
770  (b, array) = high
771  (eb, kept) = facts
772  (%Equal.sym(Array<F32>, a, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), ea) : {ANode{_, b} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, Nat.add(Model.capacity(lower), base))} : Array<F32>}
773   %Equal.sym(Array<F32>, b, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, Nat.add(Model.capacity(lower), base)), eb) : {ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), _} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, Nat.add(Model.capacity(lower), base))} : Array<F32>}
774   {==}, kept)
775
776def tree_node_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
777  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
778  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +lower: Nat, +base: Nat,
779  low: Array<F32> & (Array<F32> & Unit),
780  facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, base, low),
781  next: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, Nat.add(Model.capacity(lower), base),
782    Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), lower, count, Nat.add(Model.capacity(lower), base), (Api.arr(h, d, f), Unit{})))) ->
783  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n+lower, base,
784    Parallel.node(~Array<F32>, ~Unit, l => r => Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), lower, count, Nat.add(Model.capacity(lower), base), (l, r)), low)):
785  (a, state) = low
786  (array, none) = state
787  (ea, ek) = facts
788  %Equal.sym(Array<F32> & Unit, (array, none), (Api.arr(h, d, f), Unit{}), ek) :
789    TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n+lower, base,
790      Parallel.join(~(Array<F32> & Unit), a, Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), lower, count, Nat.add(Model.capacity(lower), base), _)))
791  tree_join_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, base, a,
792    Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), lower, count, Nat.add(Model.capacity(lower), base), (Api.arr(h, d, f), Unit{})), ea, next)
793
794# The depth-1 tree: the leaf of cell `base` and the leaf of the cell after
795# it, which reads the state the first hands back.
796def pair_join_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
797  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
798  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +base: Nat, x: F32, high: F32 & Array<F32> & Unit,
799  ex: {ALeaf{x} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base) : Array<F32>},
800  leaf_facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, Nat.add(1n, base), Parallel.leaf(~(Array<F32> & Unit), high))) ->
801  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair_join(~(Array<F32> & Unit), x, high)):
802  (y, inputs) = high
803  (ey, kept) = leaf_facts
804  (%Equal.sym(Array<F32>, ALeaf{x}, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), ex) : {ANode{_, ALeaf{y}} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base))} : Array<F32>}
805   %Equal.sym(Array<F32>, ALeaf{y}, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base)), ey) : {ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), _} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base))} : Array<F32>}
806   {==}, kept)
807
808def pair_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
809  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
810  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +source: Par.Source<shape, fill, ops, h, d, f>, +facts: Facts<plan, shape, count>, +base: Nat, low: F32 & Array<F32> & Unit,
811  leaf_facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, base, Parallel.leaf(~(Array<F32> & Unit), low))) ->
812  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), count, base, low)):
813  (x, state) = low
814  (array, none) = state
815  (ex, ek) = leaf_facts
816  %Equal.sym(Array<F32> & Unit, (array, none), (Api.arr(h, d, f), Unit{}), ek) :
817    TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair_join(~(Array<F32> & Unit), x, Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), Nat.add(1n, base), _, Nat.is_lt(Nat.add(1n, base), count))))
818  pair_join_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, base, x, Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), Nat.add(1n, base), (Api.arr(h, d, f), Unit{}), Nat.is_lt(Nat.add(1n, base), count)), ex,
819    cell_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, Nat.add(1n, base), Nat.is_lt(Nat.add(1n, base), count), {==}))
820
821def tree_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
822  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
823  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat,
824  +source: Par.Source<shape, fill, ops, h, d, f>, +facts: Facts<plan, shape, count>, +depth: Nat, +base: Nat) ->
825  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, depth, base,
826    Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), depth, count, base, (Api.arr(h, d, f), Unit{}))):
827  match depth:
828    case 0n:
829      cell_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, base, Nat.is_lt(base, count), {==})
830    case 1n+lower:
831      match lower:
832        case 0n:
833          pair_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, base, Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), base, (Api.arr(h, d, f), Unit{}), Nat.is_lt(base, count)),
834            cell_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, base, Nat.is_lt(base, count), {==}))
835        case 1n+below:
836          tree_node_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, base,
837            Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), lower, count, base, (Api.arr(h, d, f), Unit{})),
838            tree_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, lower, base),
839            tree_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, lower, Nat.add(Model.capacity(lower), base)))
840
841def tree_first(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
842  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
843  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +depth: Nat, +base: Nat,
844  -result: Array<F32> & (Array<F32> & Unit), facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, depth, base, result)) ->
845  {Pair.fst(Array<F32>, Array<F32> & Unit, result) == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, depth, base) : Array<F32>}:
846  (first, kept) = facts
847  first
848
849def fork_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
850  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
851  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat,
852  +lower: Nat, +rest: Nat, +base: Nat,
853  low: {Reduce.build(lower, rest, rows, Shape.extents(Shape.output_shape(plan)), count, base, Api.arr(h, d, f)) ==
854    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base) : Array<F32>},
855  high: {Reduce.build(lower, rest, rows, Shape.extents(Shape.output_shape(plan)), count, Nat.add(Model.capacity(lower), base), Api.arr(h, d, f)) ==
856    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, Nat.add(Model.capacity(lower), base)) : Array<F32>},
857  pair: Array<F32> & Array<F32>, +exact: {pair == Array.clone(F32, Api.arr(h, d, f)) : Array<F32> & Array<F32>}) ->
858  {Parallel.fork(~Array<F32>, ~Unit, Reduce.halves(pair),
859    l => r => Parallel.build(~Reduce.Fibers, ~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.fibers, ~Reduce.split, ~Reduce.cell_at, Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}, lower, rest, count, base, (l, r)),
860    l => r => Parallel.build(~Reduce.Fibers, ~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.fibers, ~Reduce.split, ~Reduce.cell_at, Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}, lower, rest, count, Nat.add(Model.capacity(lower), base), (l, r))) ==
861    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 1n+lower, base) : Array<F32>}:
862  (first, second) = pair
863  +output = Shape.extents(Shape.output_shape(plan))
864  +upper = Nat.add(Model.capacity(lower), base)
865  %Equal.sym(Array<F32>, first, Api.arr(h, d, f), Build.clone_first_eq(d, h, f, (first, second), exact)) :
866    {ANode{Reduce.build(lower, rest, rows, output, count, base, _), Reduce.build(lower, rest, rows, output, count, upper, second)} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 1n+lower, base) : Array<F32>}
867  %Equal.sym(Array<F32>, second, Api.arr(h, d, f), Build.clone_second_eq(d, h, f, (first, second), exact)) :
868    {ANode{Reduce.build(lower, rest, rows, output, count, base, Api.arr(h, d, f)), Reduce.build(lower, rest, rows, output, count, upper, _)} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 1n+lower, base) : Array<F32>}
869  %Equal.sym(Array<F32>, Reduce.build(lower, rest, rows, output, count, base, Api.arr(h, d, f)),
870    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), low) :
871    {ANode{_, Reduce.build(lower, rest, rows, output, count, upper, Api.arr(h, d, f))} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 1n+lower, base) : Array<F32>}
872  %Equal.sym(Array<F32>, Reduce.build(lower, rest, rows, output, count, upper, Api.arr(h, d, f)),
873    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, upper), high) :
874    {ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, lower, base), _} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 1n+lower, base) : Array<F32>}
875  {==}
876
877# Whatever the split, the parallel build over the copy returns the spec.
878def build_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
879  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
880  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat,
881  +source: Par.Source<shape, fill, ops, h, d, f>, +facts: Facts<plan, shape, count>, +depth: Nat, +splits: Nat, +base: Nat) ->
882  {Reduce.build(depth, splits, rows, Shape.extents(Shape.output_shape(plan)), count, base, Api.arr(h, d, f)) ==
883    out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, depth, base) : Array<F32>}:
884  match depth splits:
885    case 1n+lower 1n+rest:
886      fork_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, lower, rest, base,
887        build_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, lower, rest, base),
888        build_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, lower, rest, Nat.add(Model.capacity(lower), base)),
889        Array.clone(F32, Api.arr(h, d, f)), {==})
890    case 0n _:
891      tree_first(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, base,
892        Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), 0n, count, base, (Api.arr(h, d, f), Unit{})),
893        tree_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, 0n, base))
894    case 1n+lower 0n:
895      tree_first(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n+lower, base,
896        Parallel.tree(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), 1n+lower, count, base, (Api.arr(h, d, f), Unit{})),
897        tree_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, 1n+lower, base))
898
899# As in reduce_fold_PROOF.bend: below the count, the listed words are the
900# replayed words.
901def length_snoc(+values: List<&2, F32>, +word: F32) ->
902  {List.length(&2, F32, List.append(&2, F32, values, [word])) == 1n+List.length(&2, F32, values) : Nat}:
903  match values:
904    case Nil{}:
905      {==}
906    case +value <> +rest:
907      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, F32, List.append(&2, F32, rest, [word])), 1n+List.length(&2, F32, rest),
908        length_snoc(rest, word))
909
910def words_length(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
911  {List.length(&2, F32, Laws.words(shape, fill, ops, count)) == count : Nat}:
912  match count:
913    case 0n:
914      {==}
915    case 1n+previous:
916      +before = Laws.words(shape, fill, ops, previous)
917      Equal.trans(Nat, List.length(&2, F32, List.append(&2, F32, before, [Replayed.value(shape, fill, ops, U32.from_nat(previous))])),
918        1n+List.length(&2, F32, before), 1n+previous,
919        length_snoc(before, Replayed.value(shape, fill, ops, U32.from_nat(previous))),
920        Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)))
921
922def word_at_front(+values: List<&2, F32>, +word: F32, +position: Nat,
923  below: {Nat.is_lt(position, List.length(&2, F32, values)) == True{} : Bool}) ->
924  {ReduceLaws.word_at(List.append(&2, F32, values, [word]), position) == ReduceLaws.word_at(values, position) : Maybe<&2, F32>}:
925  match values position:
926    case Nil{} _:
927      Empty.absurd({ReduceLaws.word_at([word], position) == None{} : Maybe<&2, F32>}, Arith.lt_zero(position, below))
928    case +value <> +rest 0n:
929      {==}
930    case +value <> +rest 1n+next:
931      word_at_front(rest, word, next, below)
932
933def word_at_last(+values: List<&2, F32>, +word: F32) ->
934  {ReduceLaws.word_at(List.append(&2, F32, values, [word]), List.length(&2, F32, values)) == Some{word} : Maybe<&2, F32>}:
935  match values:
936    case Nil{}:
937      {==}
938    case +value <> +rest:
939      word_at_last(rest, word)
940
941def words_step(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +position: Nat,
942  below: {Nat.is_lt(position, 1n+previous) == True{} : Bool}, decision: Shape.BoolCase<Nat.is_eq(position, previous)>,
943  earlier: @inside: {Nat.is_lt(position, previous) == True{} : Bool} ->
944    {ReduceLaws.word_at(Laws.words(shape, fill, ops, previous), position) ==
945      Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}) ->
946  {ReduceLaws.word_at(Laws.words(shape, fill, ops, 1n+previous), position) ==
947    Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}:
948  match decision:
949    case Shape.BFalse{equal}:
950      +before = Laws.words(shape, fill, ops, previous)
951      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
952      +inside = PointwiseProof.lt_succ_ne(position, previous, below, equal)
953      Equal.trans(Maybe<&2, F32>, ReduceLaws.word_at(List.append(&2, F32, before, [last]), position), ReduceLaws.word_at(before, position),
954        Some{Replayed.value(shape, fill, ops, U32.from_nat(position))},
955        word_at_front(before, last, position,
956          %Equal.sym(Nat, List.length(&2, F32, before), previous, words_length(shape, fill, ops, previous)) :
957            {Nat.is_lt(position, _) == True{} : Bool}
958          inside),
959        earlier(inside))
960    case Shape.BTrue{equal}:
961      +before = Laws.words(shape, fill, ops, previous)
962      +last = Replayed.value(shape, fill, ops, U32.from_nat(previous))
963      %Equal.sym(Nat, position, previous, Arith.eq_true(position, previous, Equal.sym(Bool, True{}, Nat.is_eq(position, previous), equal))) :
964        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{Replayed.value(shape, fill, ops, U32.from_nat(_))} : Maybe<&2, F32>}
965      %words_length(shape, fill, ops, previous) :
966        {ReduceLaws.word_at(List.append(&2, F32, before, [last]), _) == Some{last} : Maybe<&2, F32>}
967      word_at_last(before, last)
968
969def words_at(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat, +position: Nat,
970  below: {Nat.is_lt(position, count) == True{} : Bool}) ->
971  {ReduceLaws.word_at(Laws.words(shape, fill, ops, count), position) ==
972    Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>}:
973  match count:
974    case 0n:
975      Empty.absurd({ReduceLaws.word_at(Nil{}, position) == Some{Replayed.value(shape, fill, ops, U32.from_nat(position))} : Maybe<&2, F32>},
976        Arith.lt_zero(position, below))
977    case 1n+previous:
978      words_step(shape, fill, ops, previous, position, below, Shape.bool_case(Nat.is_eq(position, previous)),
979        inside => words_at(shape, fill, ops, previous, position, inside))
980
981
982def parallel_splits(+plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat) -> Nat:
983  Reduce.splits(plan, depth, length)
984
985# The writes of every cell, replayed on the owned storage `created` makes for
986# the target, give the owned storage the parallel build fills.
987def output_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
988  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
989  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +dc: Nat, +fc: F32,
990  +source: Par.Source<shape, fill, ops, h, dc, fc>, +target: Shape.Shape, +facts: Facts<plan, shape, U32.to_nat(Shape.count(target))>,
991  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool},
992  -f: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool}) ->
993  {StorageLaws.replay(writes(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, U32.to_nat(Shape.count(target))),
994    Storage.Owned{d, U32.to_nat(Shape.count(target)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) ==
995    Storage.Owned{d, U32.to_nat(Shape.count(target)),
996      Reduce.build(d, parallel_splits(plan, d, U32.to_nat(Shape.count(target))), rows, Shape.extents(Shape.output_shape(plan)),
997        U32.to_nat(Shape.count(target)), 0n, Api.arr(h, dc, fc)),
998      Reduce.build_balanced(d, parallel_splits(plan, d, U32.to_nat(Shape.count(target))), rows, Shape.extents(Shape.output_shape(plan)),
999        U32.to_nat(Shape.count(target)), 0n, Api.arr(h, dc, fc)), f} : Storage.Storage}:
1000  +n = U32.to_nat(Shape.count(target))
1001  +map : PlanMap(plan) = Shape.Indexed{rows, rows_exact}
1002  +splits = parallel_splits(plan, d, n)
1003  +extents = Shape.extents(Shape.output_shape(plan))
1004  Equal.trans(Storage.Storage,
1005    StorageLaws.replay(writes(plan, map, shape, fill, ops, n), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
1006    Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, n, d, 0n), out_balanced(plan, map, shape, fill, ops, n, d, 0n), f},
1007    Storage.Owned{d, n, Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), Reduce.build_balanced(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), f},
1008    chain(plan, map, shape, fill, ops, d, n, f, fits, Shape.count(target), Conversion.le_reflexive(n), n, Conversion.le_reflexive(n)),
1009    Owned.owned_eq(d, n, out_spec(plan, map, shape, fill, ops, n, d, 0n), Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)),
1010      Equal.sym(Array<F32>, Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), out_spec(plan, map, shape, fill, ops, n, d, 0n),
1011        build_eq(plan, rows, rows_exact, shape, fill, ops, h, dc, fc, n, source, facts, d, splits, 0n)),
1012      out_balanced(plan, map, shape, fill, ops, n, d, 0n), f)(Reduce.build_balanced(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc))))
1013
1014# The parallel reduce over a replayed contribution, in transport form: P
1015# holds for the result if it holds for the contribution replayed with any
1016# history that keeps its words, next to the target replayed with any history
1017# whose cells hold the cell words.
1018def Final(+plan: Shape.BroadcastPlan, +target: Shape.Shape, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +map: PlanMap(plan),
1019  -s: Storage.Storage, -P: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic> -> Type) -> Type:
1020  @+kept: List<&2, StorageLaws.Op> ->
1021  @values: (@+other: U32 -> {Replayed.value(shape, fill, kept, other) == Replayed.value(shape, fill, ops, other) : F32}) ->
1022  @words: {Laws.words(shape, fill, kept, Shape.logical_numel(Shape.dimensions(shape))) ==
1023    Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))) : List<&2, F32>} ->
1024  @-kept_fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, kept)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
1025  @+out: List<&2, StorageLaws.Op> ->
1026  @cells: (@+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
1027    {Replayed.value(target, 0.0, out, index) == cell_word(plan, map, shape, fill, ops, U32.to_nat(index)) : F32}) ->
1028  @-out_fits: {Lifecycle.logical_length(StorageLaws.replay(out, s)) == Shape.logical_numel(Shape.dimensions(target)) : Nat} ->
1029    P((Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), kept_fits}},
1030      Done{Core.Packed{target, Core.TTensor{StorageLaws.replay(out, s), out_fits}}}))
1031
1032def room_of(+target: Shape.Shape) -> {Nat.is_le(U32.to_nat(Shape.count(target)), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}:
1033  %Equal.sym(Nat, U32.to_nat(Shape.count(target)), Shape.logical_numel(Shape.dimensions(target)), Reads.count_exact(target)) : {Nat.is_le(_, Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}
1034  Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(target)))
1035
1036def inside_count(+target: Shape.Shape, +index: U32,
1037  +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
1038  {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(target))) == True{} : Bool}:
1039  %Equal.sym(Nat, U32.to_nat(Shape.count(target)), Shape.logical_numel(Shape.dimensions(target)), Reads.count_exact(target)) :
1040    {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1041  inside
1042
1043def indexed_lift(+plan: Shape.BroadcastPlan, +target: Shape.Shape, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
1044  -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
1045  +facts: Facts<plan, shape, U32.to_nat(Shape.count(target))>,
1046  +d: Nat, +fits_d: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool},
1047  -f: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool},
1048  -fo: {Lifecycle.logical_length(Storage.Owned{d, U32.to_nat(Shape.count(target)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) ==
1049    Shape.logical_numel(Shape.dimensions(target)) : Nat},
1050  +map: PlanMap(plan), -P: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic> -> Type,
1051  final: Final(plan, target, shape, fill, ops, map,
1052    Storage.Owned{d, U32.to_nat(Shape.count(target)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}, P)) ->
1053  P(Reduce.parallel_indexed(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, target, plan,
1054    Core.TTensor{Storage.Owned{d, U32.to_nat(Shape.count(target)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}, fo},
1055    d, U32.to_nat(Shape.count(target)), f, fo, map)):
1056  match map:
1057    case Shape.Unindexed{zero}:
1058      final(ops)(other => {==})({==})(fits)(Nil{})(index => inside => {==})(fo)
1059    case Shape.Indexed{+rows, +rows_exact}:
1060      +n = U32.to_nat(Shape.count(target))
1061      +map : PlanMap(plan) = Shape.Indexed{rows, rows_exact}
1062      Par.input_take(shape, fill, ops,
1063        taken => P(Reduce.parallel_rows(plan, target, d, n, f, fo, taken, rows)),
1064        kept => values => words => h => dc => fc => source => kept_fits =>
1065          Par.storage_shift(target,
1066            StorageLaws.replay(writes(plan, map, shape, fill, ops, n), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
1067            Storage.Owned{d, n,
1068              Reduce.build(d, parallel_splits(plan, d, n), rows, Shape.extents(Shape.output_shape(plan)), n, 0n, Api.arr(h, dc, fc)),
1069              Reduce.build_balanced(d, parallel_splits(plan, d, n), rows, Shape.extents(Shape.output_shape(plan)), n, 0n, Api.arr(h, dc, fc)), f},
1070            output_eq(plan, rows, rows_exact, shape, fill, ops, h, dc, fc, source, target, facts, d, fits_d, f),
1071            st => k => P((Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), kept_fits}}, Done{Core.Packed{target, Core.TTensor{st, k}}})),
1072            final(kept)(values)(words)(kept_fits)(writes(plan, map, shape, fill, ops, n))(
1073              index => inside => writes_value(plan, map, shape, fill, ops, target, n, index, inside_count(target, index, inside), room_of(target))))(fo))(fits)
1074
1075# The cell word adds the replayed words the masked fold adds.
1076
1077def rfold_gather(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +positions: List<&2, Nat>, +accumulator: F32,
1078  +below: {ReduceParallel.all_below(positions, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1079  {Some{rfold(shape, fill, ops, positions, accumulator)} ==
1080    ReduceParallel.gather(Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), positions, Some{accumulator}) : Maybe<&2, F32>}:
1081  match positions:
1082    case Nil{}:
1083      {==}
1084    case +p <> +ps:
1085      +count = Shape.logical_numel(Shape.dimensions(shape))
1086      +here = Arith.and_left(Nat.is_lt(p, count), ReduceParallel.all_below(ps, count), below)
1087      +later = Arith.and_right(Nat.is_lt(p, count), ReduceParallel.all_below(ps, count), below)
1088      +word = Replayed.value(shape, fill, ops, U32.from_nat(p))
1089      %Equal.sym(Maybe<&2, F32>, ReduceLaws.word_at(Laws.words(shape, fill, ops, count), p), Some{word}, words_at(shape, fill, ops, count, p, here)) :
1090        {Some{rfold(shape, fill, ops, ps, F32.add(accumulator, word))} ==
1091          ReduceParallel.gather(Laws.words(shape, fill, ops, count), ps, ReduceLaws.add_word(Some{accumulator}, _)) : Maybe<&2, F32>}
1092      rfold_gather(shape, fill, ops, ps, F32.add(accumulator, word), later)
1093
1094def word_fiber(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32,
1095  +inside: {Nat.is_lt(U32.to_nat(index), Shape.numel(Shape.extents(Shape.left_shape(plan)))) == True{} : Bool},
1096  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
1097  {Some{cell_word(plan, map, shape, fill, ops, U32.to_nat(index))} ==
1098    ReduceLaws.fiber(plan, Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), index,
1099      Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}:
1100  match map:
1101    case Shape.Unindexed{zero}:
1102      %zero : {Some{0.0} == ReduceLaws.fiber(plan, Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), index, _) : Maybe<&2, F32>}
1103      {==}
1104    case Shape.Indexed{+rows, +rows_exact}:
1105      +t = U32.to_nat(index)
1106      +output = Shape.extents(Shape.output_shape(plan))
1107      +count = Shape.numel(output)
1108      +values = Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape)))
1109      +walk = ReduceParallel.plan_walk(plan, rows, rows_exact, t, inside)
1110      %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, count), ReduceParallel.gather(values, Fiber.masked(count, rows, t, 0n, 0n), Some{0.0}),
1111        ReduceParallel.fiber_masked(plan, rows, rows_exact, values, index, count, Conversion.le_reflexive(count))) :
1112        {Some{rfold(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0)} == _ : Maybe<&2, F32>}
1113      %Equal.sym(List<&2, Nat>, Fiber.masked(count, rows, t, 0n, 0n), ReduceParallel.visited_of(rows, output, t), walk) :
1114        {Some{rfold(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0)} == ReduceParallel.gather(values, _, Some{0.0}) : Maybe<&2, F32>}
1115      rfold_gather(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0,
1116        walk_below(plan, rows, rows_exact, shape, Shape.numel(Shape.extents(Shape.left_shape(plan))), Facts{{==}, right}, t, inside))