1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/model.bend as Model
4	import ../storage/main.bend as Storage
5	import ../storage/LAWS.bend as StorageLaws
6	import ../storage/refinement.bend as Refinement
7	import ../storage/arith.bend as Arith
8	import ../storage/array.bend as ArrayCore
9	import ../storage/api.bend as Api
10	import ../storage/certificates.bend as Certificates
11	import ../storage/route.bend as Route
12	import ../shape/index_proofs.bend as Index
13	import ../shape/nat_proofs.bend as Nats
14	import ../tensor/core.bend as Core
15	import ../tensor/lifecycle.bend as Lifecycle
16	import ../tensor/elementwise.bend as Elementwise
17	import ../tensor/word_conversion.bend as Conversion
18	import ../tensor/read_contract.bend as Reads
19	import ../tensor/from_values_contract.bend as FromValues
20	import ../tensor/matrix_index_proof.bend as MatrixIndex
21	import ../tensor/contracts/replayed.bend as Replayed
22	import ../tensor/contracts/pointwise_proof.bend as PointwiseProof
23	import ../tensor/contracts/LAWS.bend as Laws
24	import ../tensor/contracts/binary_storage_proof.bend as Owned
25	import ../tensor/contracts/binary_build_proof.bend as Build
26	import ../tensor/contracts/matmul_parallel_proof.bend as Par
27	import ../tensor/matmul.bend as Matrix
28	import ../tensor/parallel.bend as Parallel
29	import ./reduce.bend as Reduce
30	import ./reduce_LAWS.bend as ReduceLaws
31	import ./reduce_fiber_proof.bend as Fiber
32	import ./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	
39	def 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.
43	def 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	
50	def 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	
57	def 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	
60	def 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	
68	def 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	
89	def 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`.
101	def 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.
114	def 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	
137	def 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	
144	def 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	
151	def 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.
161	def 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	
172	def 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.
184	def 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	
195	def 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	
207	def 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	
215	def 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	
227	def 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	
232	def 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.
240	def 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	
256	def 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	
263	def 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	
270	def 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	
277	def 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.
292	def 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.
311	def 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.
335	def 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.
380	def 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	
422	def 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	
434	def 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	
443	def 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	
451	def 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	
463	def 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	
468	def 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.
510	def 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	
515	def 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	
525	def 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.
560	def 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	
563	def 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	
603	def 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	
638	def 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.
650	def 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	
676	def 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.
710	type 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.
716	def 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	
730	def 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	
737	def 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	
763	def 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	
776	def 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.
796	def 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	
808	def 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	
821	def 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	
841	def 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	
849	def 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.
878	def 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.
901	def 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	
910	def 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	
922	def 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	
933	def 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	
941	def 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	
969	def 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	
982	def 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.
987	def 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.
1018	def 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	
1032	def 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	
1036	def 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	
1043	def 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	
1077	def 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	
1094	def 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))