1	import Base
2	import ../storage/model.bend as Model
3	import ../storage/refinement.bend as Refinement
4	import ../tensor/elementwise_parallel_proof.bend as Parallel
5	import ../tensor/parallel_proofs.bend as Generic
6	import ../shape/core.bend as Shape
7	import ../shape/flat.bend as Flat
8	import ../shape/broadcast_proofs.bend as Broadcast
9	import ../shape/projection_proofs.bend as ShapeProjection
10	import ../storage/arith.bend as Arith
11	import ../shape/index_proofs.bend as Index
12	import ../tensor/word_conversion.bend as Conversion
13	import ../tensor/projection_LAWS.bend as Projection
14	import ../shape/LAWS.bend as ShapeLaws
15	import ../tensor/contracts/broadcast.bend as BroadcastMap
16	import ../tensor/contracts/broadcast_proof.bend as BroadcastProof
17	import ../tensor/contracts/pointwise_proof.bend as PointwiseProof
18	import ./reduce.bend as Reduce
19	import ./reduce_LAWS.bend as ReduceLaws
20	import ./reduce_fiber_proof.bend as Fiber
21	
22	# The fiber walk of a reduce plan. For the index rows of a plan whose output
23	# broadcasts the target, the walk of a target cell below the target's count
24	# reads the masked positions (`Fiber.fiber_walk`), every one of them lies
25	# inside the contribution, and adding the contribution's words there, in that
26	# order from +0.0, is `ReduceLaws.fiber`.
27	
28	def numel_pad(+count: Nat, +dims: List<&2, Nat>) -> {Shape.numel(Shape.pad(count, dims)) == Shape.numel(dims) : Nat}:
29	  match count:
30	    case 0n:
31	      {==}
32	    case 1n+rest:
33	      Equal.trans(Nat, Nat.add(Shape.numel(Shape.pad(rest, dims)), 0n), Shape.numel(Shape.pad(rest, dims)), Shape.numel(dims),
34	        Broadcast.add_zero(Shape.numel(Shape.pad(rest, dims))), numel_pad(rest, dims))
35	
36	def padding_left(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +lp: Nat, +rp: Nat,
37	  +aligned: Shape.Aligned(Shape.pad(lp, left), Shape.pad(rp, right), output)) ->
38	  {lp == Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left)) : Nat}:
39	  ShapeProjection.padding_of(List.length(&2, Nat, output), lp, List.length(&2, Nat, left),
40	    Equal.trans(Nat, Nat.add(lp, List.length(&2, Nat, left)), List.length(&2, Nat, Shape.pad(lp, left)), List.length(&2, Nat, output),
41	      Broadcast.pad_length(lp, left), Broadcast.aligned_length_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned)))
42	
43	def padding_right(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +lp: Nat, +rp: Nat,
44	  +aligned: Shape.Aligned(Shape.pad(lp, left), Shape.pad(rp, right), output)) ->
45	  {rp == Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right)) : Nat}:
46	  ShapeProjection.padding_of(List.length(&2, Nat, output), rp, List.length(&2, Nat, right),
47	    Equal.trans(Nat, Nat.add(rp, List.length(&2, Nat, right)), List.length(&2, Nat, Shape.pad(rp, right)), List.length(&2, Nat, output),
48	      Broadcast.pad_length(rp, right), Broadcast.aligned_length_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned)))
49	
50	# The index table of an aligned broadcast is walked as `Fiber.fiber_walk`
51	# says.
52	def table_walk(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>,
53	  +target: Nat, +below: {Nat.is_lt(target, Shape.numel(left)) == True{} : Bool}) ->
54	  Fiber.RestWalk(Shape.index_table(left, right, output), output, target, Shape.numel(output)):
55	  match alignment:
56	    case Shape.BAlign{+lp, +rp, minimal, +aligned}:
57	      +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left))
58	      +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right))
59	      Fiber.fiber_walk(Shape.pad(nl, left), Shape.pad(nr, right), output,
60	        %padding_left(left, right, output, lp, rp, aligned) : Shape.Aligned(Shape.pad(_, left), Shape.pad(nr, right), output)
61	        %padding_right(left, right, output, lp, rp, aligned) : Shape.Aligned(Shape.pad(lp, left), Shape.pad(_, right), output)
62	        aligned,
63	        target,
64	        %Equal.sym(Nat, Shape.numel(Shape.pad(nl, left)), Shape.numel(left), numel_pad(nl, left)) : {Nat.is_lt(target, _) == True{} : Bool}
65	        below)
66	
67	# The same for the rows of a plan's index map.
68	def plan_walk(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
69	  +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>},
70	  +target: Nat, +below: {Nat.is_lt(target, Shape.numel(Shape.extents(Shape.left_shape(plan)))) == True{} : Bool}) ->
71	  Fiber.RestWalk(rows, Shape.extents(Shape.output_shape(plan)), target, Shape.numel(Shape.extents(Shape.output_shape(plan)))):
72	  +left = Shape.extents(Shape.left_shape(plan))
73	  +right = Shape.extents(Shape.right_shape(plan))
74	  +output = Shape.extents(Shape.output_shape(plan))
75	  %Equal.sym(List<&2, Shape.Row>, rows, Shape.index_table(left, right, output), exact) :
76	    Fiber.RestWalk(_, output, target, Shape.numel(output))
77	  table_walk(left, right, output, Shape.alignment(plan), target, below)
78	
79	# As in reduce_fold_PROOF.bend: below the output count, the specified
80	# offsets are the index walks.
81	def offsets_walk(+plan: Shape.BroadcastPlan,
82	  +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
83	  +position: Nat, +bound: {True{} == Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
84	  {Projection.offset_spec(plan, position) ==
85	    Some{(U32.from_nat(BroadcastMap.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
86	        Shape.extents(Shape.output_shape(plan)), map, position)),
87	      U32.from_nat(BroadcastMap.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
88	        Shape.extents(Shape.output_shape(plan)), map, position)))} : Maybe<&1, U32 & U32>}:
89	  match map:
90	    case Shape.Indexed{+rows, +exact}:
91	      +left = Shape.extents(Shape.left_shape(plan))
92	      +right = Shape.extents(Shape.right_shape(plan))
93	      +output = Shape.extents(Shape.output_shape(plan))
94	      +index = {Shape.FIndex{position, bound} : Shape.FlatIndex<Shape.output_shape(plan)>}
95	      +slot = ShapeLaws.fin_of(Shape.numel(output), position)
96	      +x = U32.from_nat(Shape.walk_left(rows, position))
97	      +y = U32.from_nat(Shape.walk_right(rows, position))
98	      %ShapeLaws.project_left_index_refines(plan, Shape.Indexed{rows, exact}, index) :
99	        {Projection.pair_offsets(_, ShapeLaws.flatten_spec(right, ShapeLaws.project_right_coordinate(left, right, output, Shape.alignment(plan), slot))) ==
100	          Some{(x, y)} : Maybe<&1, U32 & U32>}
101	      %ShapeLaws.project_right_index_refines(plan, Shape.Indexed{rows, exact}, index) :
102	        {Projection.pair_offsets(Some{x}, _) == Some{(x, y)} : Maybe<&1, U32 & U32>}
103	      {==}
104	    case Shape.Unindexed{zero}:
105	      +output = Shape.output_shape(plan)
106	      Empty.absurd({Projection.offset_spec(plan, position) == Some{(U32.from_nat(0n), U32.from_nat(0n))} : Maybe<&1, U32 & U32>},
107	        Arith.lt_zero(position,
108	          %Equal.trans(Nat, Shape.elements(output), Shape.numel(Shape.extents(output)), 0n, Shape.elements_exact(output),
109	            Equal.sym(Nat, 0n, Shape.numel(Shape.extents(output)), zero)) : {Nat.is_lt(position, _) == True{} : Bool}
110	          Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(output)), bound)))
111	
112	# Adding the words at a list of positions, in order.
113	def gather(+values: List<&2, F32>, positions: List<&2, Nat>, total: Maybe<&2, F32>) -> Maybe<&2, F32>:
114	  match positions:
115	    case Nil{}:
116	      total
117	    case position <> rest:
118	      gather(values, rest, ReduceLaws.add_word(total, ReduceLaws.word_at(values, position)))
119	
120	def gather_append(+values: List<&2, F32>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +total: Maybe<&2, F32>) ->
121	  {gather(values, List.append(&2, Nat, xs, ys), total) == gather(values, ys, gather(values, xs, total)) : Maybe<&2, F32>}:
122	  match xs:
123	    case Nil{}:
124	      {==}
125	    case +x <> +rest:
126	      gather_append(values, rest, ys, ReduceLaws.add_word(total, ReduceLaws.word_at(values, x)))
127	
128	def gather_kept(+values: List<&2, F32>, +keep: Bool, +position: Nat, +total: Maybe<&2, F32>) ->
129	  {gather(values, Fiber.kept(keep, position, Nil{}), total) == ReduceLaws.matched(total, ReduceLaws.word_at(values, position), keep) : Maybe<&2, F32>}:
130	  match keep:
131	    case True{}:
132	      {==}
133	    case False{}:
134	      {==}
135	
136	def succ_add(+k: Nat) -> {Nat.add(k, 1n) == 1n+k : Nat}:
137	  Equal.trans(Nat, Nat.add(k, 1n), 1n+Nat.add(k, 0n), 1n+k, Arith.add_succ(k, 0n),
138	    Equal.cong(Nat, Nat, n => 1n+n, Nat.add(k, 0n), k, Broadcast.add_zero(k)))
139	
140	# The masked fold of `ReduceLaws.fiber` adds, in order, the words at the
141	# masked positions.
142	def fiber_masked(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
143	  +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>},
144	  +values: List<&2, F32>, +index: U32, +count: Nat,
145	  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
146	  {ReduceLaws.fiber(plan, values, index, count) == gather(values, Fiber.masked(count, rows, U32.to_nat(index), 0n, 0n), Some{0.0}) : Maybe<&2, F32>}:
147	  match count:
148	    case 0n:
149	      {==}
150	    case 1n+k:
151	      +t = U32.to_nat(index)
152	      +map : Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))> =
153	        Shape.Indexed{rows, exact}
154	      +limit = Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))
155	      +below = Conversion.le_successor_lt(k, limit, room)
156	      +lm = Shape.walk_left(rows, k)
157	      +rm = Shape.walk_right(rows, k)
158	      +before = Fiber.masked(k, rows, t, 0n, 0n)
159	      +last = Fiber.kept(Nat.is_eq(lm, t), rm, Nil{})
160	      +lm_below = BroadcastProof.left_walk_bound(plan, map, k, below)
161	      +rm_below = BroadcastProof.right_walk_bound(plan, map, k, below)
162	      %Equal.sym(Maybe<&1, U32 & U32>, Projection.offset_spec(plan, k), Some{(U32.from_nat(lm), U32.from_nat(rm))},
163	        offsets_walk(plan, map, k, BroadcastProof.output_inside(plan, k, below))) :
164	        {ReduceLaws.contribute(values, index, ReduceLaws.fiber(plan, values, index, k), _) ==
165	          gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>}
166	      %Equal.sym(Nat, U32.to_nat(U32.from_nat(rm)), rm, PointwiseProof.word_exact(rm, Shape.right_shape(plan), rm_below)) :
167	        {ReduceLaws.matched(ReduceLaws.fiber(plan, values, index, k), ReduceLaws.word_at(values, _), Nat.is_eq(U32.to_nat(U32.from_nat(lm)), t)) ==
168	          gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>}
169	      %Equal.sym(Nat, U32.to_nat(U32.from_nat(lm)), lm, PointwiseProof.word_exact(lm, Shape.left_shape(plan), lm_below)) :
170	        {ReduceLaws.matched(ReduceLaws.fiber(plan, values, index, k), ReduceLaws.word_at(values, rm), Nat.is_eq(_, t)) ==
171	          gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>}
172	      %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, k), gather(values, before, Some{0.0}),
173	        fiber_masked(plan, rows, exact, values, index, k, Conversion.le_predecessor(k, limit, room))) :
174	        {ReduceLaws.matched(_, ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) ==
175	          gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>}
176	      %succ_add(k) :
177	        {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) ==
178	          gather(values, Fiber.masked(_, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>}
179	      %Equal.sym(List<&2, Nat>, Fiber.masked(Nat.add(k, 1n), rows, t, 0n, 0n), List.append(&2, Nat, before, Fiber.masked(1n, rows, t, 0n, Nat.add(0n, k))),
180	        Fiber.masked_split(k, 1n, rows, t, 0n, 0n)) :
181	        {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) ==
182	          gather(values, _, Some{0.0}) : Maybe<&2, F32>}
183	      %Equal.sym(Maybe<&2, F32>, gather(values, List.append(&2, Nat, before, last), Some{0.0}), gather(values, last, gather(values, before, Some{0.0})),
184	        gather_append(values, before, last, Some{0.0})) :
185	        {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) == _ : Maybe<&2, F32>}
186	      Equal.sym(Maybe<&2, F32>, gather(values, last, gather(values, before, Some{0.0})),
187	        ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)),
188	        gather_kept(values, Nat.is_eq(lm, t), rm, gather(values, before, Some{0.0})))
189	
190	# Every masked position lies inside the contribution.
191	def all_below(positions: List<&2, Nat>, +bound: Nat) -> Bool:
192	  match positions:
193	    case Nil{}:
194	      True{}
195	    case position <> rest:
196	      Bool.and(Nat.is_lt(position, bound), all_below(rest, bound))
197	
198	def kept_below(+keep: Bool, +position: Nat, +rest: List<&2, Nat>, +bound: Nat,
199	  +inside: {Nat.is_lt(position, bound) == True{} : Bool}, +others: {all_below(rest, bound) == True{} : Bool}) ->
200	  {all_below(Fiber.kept(keep, position, rest), bound) == True{} : Bool}:
201	  match keep:
202	    case True{}:
203	      %Equal.sym(Bool, Nat.is_lt(position, bound), True{}, inside) : {Bool.and(_, all_below(rest, bound)) == True{} : Bool}
204	      others
205	    case False{}:
206	      others
207	
208	def masked_below(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
209	  +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>},
210	  +target: Nat, +n: Nat, +cursor: Nat,
211	  +room: {Nat.is_le(Nat.add(cursor, n), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
212	  {all_below(Fiber.masked(n, rows, target, 0n, cursor), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool}:
213	  match n:
214	    case 0n:
215	      {==}
216	    case 1n+m:
217	      +map : Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))> =
218	        Shape.Indexed{rows, exact}
219	      kept_below(Nat.is_eq(Shape.walk_left(rows, cursor), target), Shape.walk_right(rows, cursor), Fiber.masked(m, rows, target, 0n, 1n+cursor),
220	        Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))),
221	        BroadcastProof.right_walk_bound(plan, map, cursor, Fiber.lt_of_room(cursor, m, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), room)),
222	        masked_below(plan, rows, exact, target, m, 1n+cursor, Fiber.le_step(cursor, m, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), room)))
223	
224	# The parallel build over an observed array. For a balanced array A, the
225	# fiber walk of a cell reads A at the offsets `Fiber.visited` lists and adds
226	# the words it sees there in order, and every cell of the build holds its
227	# walk's total below `count` and +0.0 above it.
228	
229	def fsum(words: List<&2, F32>, accumulator: F32) -> F32:
230	  match words:
231	    case Nil{}:
232	      accumulator
233	    case word <> rest:
234	      fsum(rest, F32.add(accumulator, word))
235	
236	def fsum_append(+xs: List<&2, F32>, +ys: List<&2, F32>, +accumulator: F32) ->
237	  {fsum(List.append(&2, F32, xs, ys), accumulator) == fsum(ys, fsum(xs, accumulator)) : F32}:
238	  match xs:
239	    case Nil{}:
240	      {==}
241	    case +x <> +rest:
242	      fsum_append(rest, ys, F32.add(accumulator, x))
243	
244	# Each word is what A holds at its position.
245	def Obs(+d: Nat, -A: Array<F32>, positions: List<&2, Nat>, words: List<&2, F32>) -> Data:
246	  match positions words:
247	    case Nil{} Nil{}:
248	      Unit
249	    case p <> ps w <> ws:
250	      ObsStep<d, A, p, w, ps, ws>
251	    case Nil{} w <> ws:
252	      Empty
253	    case p <> ps Nil{}:
254	      Empty
255	
256	type ObsStep<-d: Nat, -A: Array<F32>, -p: Nat, -w: F32, -ps: List<&2, Nat>, -ws: List<&2, F32>> is Data:
257	  ObsStep{-seen: {Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(p))) == Some{w} : Maybe<&2, F32>}, -more: Obs(d, A, ps, ws)}
258	
259	def obs_append(+d: Nat, -A: Array<F32>, +xs: List<&2, Nat>, +vs: List<&2, F32>, -ys: List<&2, Nat>, -ws: List<&2, F32>,
260	  -first: Obs(d, A, xs, vs), -second: Obs(d, A, ys, ws)) ->
261	  Parallel.Fact<Obs(d, A, List.append(&2, Nat, xs, ys), List.append(&2, F32, vs, ws))>:
262	  match xs vs:
263	    case Nil{} Nil{}:
264	      Parallel.Fact{second}
265	    case +p <> +ps +v <> +rest:
266	      Parallel.Fact{{\{ObsStep: seen => more =>
267	        ObsStep{seen, {\{Parallel.Fact: p => p} : Parallel.Fact<Obs(d, A, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws))> ->
268	          Obs(d, A, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws))}(obs_append(d, A, ps, rest, ys, ws, more, second))}} :
269	        ObsStep<d, A, p, v, ps, rest> -> ObsStep<d, A, p, v, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws)>}(first)}
270	    case Nil{} +v <> +rest:
271	      Parallel.Fact{Empty.absurd(Obs(d, A, ys, List.append(&2, F32, v <> rest, ws)), first)}
272	    case +p <> +ps Nil{}:
273	      Parallel.Fact{Empty.absurd(Obs(d, A, List.append(&2, Nat, p <> ps, ys), ws), first)}
274	
275	# A run of `Reduce.fiber`: its total adds the words it saw, in order, and
276	# the array comes back unchanged.
277	type FiberRun<-d: Nat, -A: Array<F32>, -positions: List<&2, Nat>, -accumulator: F32, -result: F32 & Array<F32>> is Data:
278	  FiberRun{-words: List<&2, F32>, -seen: Obs(d, A, positions, words),
279	    -total: {Pair.fst(F32, Array<F32>, result) == fsum(words, accumulator) : F32},
280	    -kept: {Pair.snd(F32, Array<F32>, result) == A : Array<F32>}}
281	
282	def leaf_run(+d: Nat, -A: Array<F32>, +base: Nat, -accumulator: F32, -array: Array<F32>, pair: Array<F32> & F32,
283	  -exact: {pair == Array.get(F32, array, U32.from_nat(base)) : Array<F32> & F32}, -same: {array == A : Array<F32>},
284	  -valid: Model.Balanced(F32, d, A)) ->
285	  Parallel.Fact<FiberRun<d, A, [base], accumulator, Reduce.leaf_add(accumulator, pair)>>:
286	  (kept, word) = pair
287	  Parallel.Fact{FiberRun{[word],
288	    ObsStep{Equal.sym(Maybe<&2, F32>, Some{word}, Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))),
289	      {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}> ->
290	        {Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}}(
291	        Parallel.read_value(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))), Unit{}},
292	    {==},
293	    {\{Parallel.Fact: p => p} : Parallel.Fact<{Refinement.first(F32, (kept, word)) == A : Array<F32>}> -> {Refinement.first(F32, (kept, word)) == A : Array<F32>}}(
294	      Parallel.read_keeps(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))}}
295	
296	def next_run(+d: Nat, -A: Array<F32>, -low: List<&2, Nat>, -high: List<&2, Nat>, -accumulator: F32,
297	  -rec: F32 -> Array<F32> -> F32 & Array<F32>, pair: F32 & Array<F32>,
298	  -first: Parallel.Fact<FiberRun<d, A, low, accumulator, pair>>,
299	  -next: @value: F32 -> @array: Array<F32> -> @-same: {array == A : Array<F32>} -> Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>>) ->
300	  Parallel.Fact<FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, Reduce.walk_next(rec, pair)>>:
301	  (value, array) = pair
302	  Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
303	    {\{FiberRun: rest => more => after => back =>
304	      FiberRun{List.append(&2, F32, words, rest),
305	        {\{Parallel.Fact: p => p} : Parallel.Fact<Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))> ->
306	          Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))}(obs_append(d, A, low, words, high, rest, seen, more)),
307	        %Equal.sym(F32, fsum(List.append(&2, F32, words, rest), accumulator), fsum(rest, fsum(words, accumulator)),
308	          fsum_append(words, rest, accumulator)) : {Pair.fst(F32, Array<F32>, rec(value, array)) == _ : F32}
309	        %total : {Pair.fst(F32, Array<F32>, rec(value, array)) == fsum(rest, _) : F32}
310	        after,
311	        back}} :
312	      FiberRun<d, A, high, value, rec(value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
313	      {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>> -> FiberRun<d, A, high, value, rec(value, array)>}(
314	        next(value)(array)(kept)))} :
315	    FiberRun<d, A, low, accumulator, (value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
316	    {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, low, accumulator, (value, array)>> -> FiberRun<d, A, low, accumulator, (value, array)>}(first))}
317	
318	def fiber_run(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +d: Nat,
319	  -A: Array<F32>, +accumulator: F32, array: Array<F32>, -same: {array == A : Array<F32>}, -valid: Model.Balanced(F32, d, A)) ->
320	  Parallel.Fact<FiberRun<d, A, Fiber.visited(rows, extents, fuel, target, base, digit), accumulator,
321	    Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, array)>>:
322	  match rows extents fuel:
323	    case Nil{} _ _:
324	      leaf_run(d, A, base, accumulator, array, Array.get(F32, array, U32.from_nat(base)), {==}, same, valid)
325	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n:
326	      Parallel.Fact{FiberRun{Nil{}, Unit{}, {==}, same}}
327	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining:
328	      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
329	      +extents : List<&2, Nat> = extent <> others
330	      +inner = Nat.mod(target, left)
331	      next_run(d, A,
332	        Fiber.visited(rest, others, Reduce.first_span(rest, others), inner, Nat.add(base, Nat.mul(right, digit)), Reduce.first_digit(rest, inner)),
333	        Fiber.visited(rows, extents, remaining, target, base, 1n+digit), accumulator,
334	        value => kept => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, value, kept),
335	        Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, Nat.add(base, Nat.mul(right, digit)), Reduce.first_digit(rest, inner),
336	          accumulator, array),
337	        fiber_run(rest, others, Reduce.first_span(rest, others), inner, Nat.add(base, Nat.mul(right, digit)), Reduce.first_digit(rest, inner),
338	          d, A, accumulator, array, same, valid),
339	        value => kept => same => fiber_run(rows, extents, remaining, target, base, 1n+digit, d, A, value, kept, same, valid))
340	    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _:
341	      Parallel.Fact{FiberRun{Nil{}, Unit{}, {==}, same}}
342	
343	# `Reduce.fiber_of` runs `Reduce.fiber_fast`, which walks the digits of a
344	# row whose rows below all take one digit in one strided loop. The proofs
345	# below show it returns what `Reduce.fiber` returns: the same words, added in
346	# the same order, and the array they were read from.
347	
348	def add_zero(+number: Nat) -> {number == Nat.add(number, 0n) : Nat}:
349	  match number:
350	    case 0n:
351	      {==}
352	    case 1n+p:
353	      Equal.cong(Nat, Nat, value => 1n+value, p, Nat.add(p, 0n), add_zero(p))
354	
355	# The one word that rows of span 1 reach from `base` sits `base` past the
356	# one they reach from 0.
357	def offset_shift(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +target: Nat, +base: Nat) ->
358	  {Reduce.single_offset(rows, extents, target, base) == Nat.add(base, Reduce.single_offset(rows, extents, target, 0n)) : Nat}:
359	  match rows extents:
360	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others:
361	      +inner = Nat.mod(target, left)
362	      +step = Nat.mul(right, Nat.div(target, left))
363	      +below = Reduce.single_offset(rest, others, inner, 0n)
364	      Equal.trans(Nat, Reduce.single_offset(rest, others, inner, Nat.add(base, step)), Nat.add(Nat.add(base, step), below),
365	        Nat.add(base, Reduce.single_offset(rest, others, inner, step)),
366	        offset_shift(rest, others, inner, Nat.add(base, step)),
367	        Equal.trans(Nat, Nat.add(Nat.add(base, step), below), Nat.add(base, Nat.add(step, below)),
368	          Nat.add(base, Reduce.single_offset(rest, others, inner, step)),
369	          Equal.sym(Nat, Nat.add(base, Nat.add(step, below)), Nat.add(Nat.add(base, step), below), Index.add_assoc(base, step, below)),
370	          Equal.cong(Nat, Nat, x => Nat.add(base, x), Nat.add(step, below), Reduce.single_offset(rest, others, inner, step),
371	            Equal.sym(Nat, Reduce.single_offset(rest, others, inner, step), Nat.add(step, below), offset_shift(rest, others, inner, step)))))
372	    case Nil{} +extents:
373	      add_zero(base)
374	    case Shape.Row{+stride, +left, +right} <> +rest Nil{}:
375	      add_zero(base)
376	
377	# A closure that hands its two arguments back as they are leaves a leaf add
378	# as it is.
379	def leaf_kept(-rec: F32 -> Array<F32> -> F32 & Array<F32>, same: @value: F32 -> @array: Array<F32> -> {rec(value, array) == (value, array) : F32 & Array<F32>},
380	  +accumulator: F32, pair: Array<F32> & F32) ->
381	  {Reduce.walk_next(rec, Reduce.leaf_add(accumulator, pair)) == Reduce.leaf_add(accumulator, pair) : F32 & Array<F32>}:
382	  match pair:
383	    case Tuple{array, word}:
384	      same(F32.add(accumulator, word), array)
385	
386	def span_one(+left: Nat, +extent: Nat, +single: {Nat.is_eq(Reduce.span(left, extent), 1n) == True{} : Bool}) ->
387	  {Reduce.span(left, extent) == 1n : Nat}:
388	  Arith.eq_true(Reduce.span(left, extent), 1n, single)
389	
390	# Rows of span 1 read one word: the one at `single_offset`.
391	def single_fiber(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +single: {Reduce.single_rows(rows, extents) == True{} : Bool},
392	  +target: Nat, +base: Nat, +accumulator: F32, -array: Array<F32>) ->
393	  Generic.Fact<{Reduce.fiber(rows, extents, Reduce.first_span(rows, extents), target, base, Reduce.first_digit(rows, target), accumulator, array) ==
394	    Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rows, extents, target, base)))) : F32 & Array<F32>}>:
395	  match rows extents:
396	    case Nil{} +extents:
397	      Generic.Fact{{==}}
398	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others:
399	      +one = span_one(left, extent, Arith.and_left(Nat.is_eq(Reduce.span(left, extent), 1n), Reduce.single_rows(rest, others), single))
400	      +inner = Nat.mod(target, left)
401	      +offset = Nat.add(base, Nat.mul(right, Nat.div(target, left)))
402	      Generic.Fact{
403	        %Equal.sym(Nat, Reduce.span(left, extent), 1n, one) :
404	          {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, _, target, base, Nat.div(target, left), accumulator, array) ==
405	            Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>}
406	        Equal.trans(F32 & Array<F32>,
407	          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),
408	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)),
409	          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),
410	            Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
411	          Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
412	          Equal.cong(F32 & Array<F32>, F32 & Array<F32>,
413	            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),
414	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array),
415	            Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
416	            {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
417	              Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>})> ->
418	              {Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
419	                Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>}}(
420	              single_fiber(rest, others, Arith.and_right(Nat.is_eq(Reduce.span(left, extent), 1n), Reduce.single_rows(rest, others), single),
421	                inner, offset, accumulator, array))),
422	          leaf_kept(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+Nat.div(target, left), v, k),
423	            value => kept => {==}, accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))))}
424	    case Shape.Row{+stride, +left, +right} <> +rest Nil{}:
425	      Empty.absurd(Generic.Fact<{Reduce.fiber(Shape.Row{stride, left, right} <> rest, Nil{}, Reduce.first_span(Shape.Row{stride, left, right} <> rest, Nil{}), target, base,
426	        Reduce.first_digit(Shape.Row{stride, left, right} <> rest, target), accumulator, array) ==
427	        Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(Shape.Row{stride, left, right} <> rest, Nil{}, target, base)))) :
428	        F32 & Array<F32>}>, Arith.clash(single))
429	
430	# One digit of a row whose rows below take one digit adds the word at its
431	# strided offset.
432	def fiber_step(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
433	  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
434	  -array: Array<F32>, -kept: Array<F32>, -word: F32,
435	  -read: {(kept, word) == Array.get(F32, array, U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))) : Array<F32> & F32}) ->
436	  Generic.Fact<{Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, array) ==
437	    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>}>:
438	  +inner = Nat.mod(target, left)
439	  +lift = Reduce.single_offset(rest, others, inner, 0n)
440	  +offset = Nat.add(base, Nat.mul(right, digit))
441	  +at = Reduce.strided_offset(right, base, digit, lift)
442	  Generic.Fact{Equal.trans(F32 & Array<F32>,
443	    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
444	      Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)),
445	    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
446	      Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
447	    Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
448	      Reduce.leaf_add(accumulator, (kept, word))),
449	    Equal.cong(F32 & Array<F32>, F32 & Array<F32>,
450	      p => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k), p),
451	      Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array),
452	      Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))),
453	      {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
454	        Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>})> ->
455	        {Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
456	          Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset)))) : F32 & Array<F32>}}(
457	        single_fiber(rest, others, single, inner, offset, accumulator, array))),
458	    Equal.trans(F32 & Array<F32>,
459	      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
460	        Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(Reduce.single_offset(rest, others, inner, offset))))),
461	      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
462	        Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(at)))),
463	      Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
464	        Reduce.leaf_add(accumulator, (kept, word))),
465	      Equal.cong(Nat, F32 & Array<F32>,
466	        n => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
467	          Reduce.leaf_add(accumulator, Array.get(F32, array, U32.from_nat(n)))),
468	        Reduce.single_offset(rest, others, inner, offset), at, offset_shift(rest, others, inner, offset)),
469	      Equal.cong(Array<F32> & F32, F32 & Array<F32>,
470	        p => Reduce.walk_next(v => k => Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, 1n+digit, v, k),
471	          Reduce.leaf_add(accumulator, p)),
472	        Array.get(F32, array, U32.from_nat(at)), (kept, word),
473	        Equal.sym(Array<F32> & F32, (kept, word), Array.get(F32, array, U32.from_nat(at)), read))))}
474	
475	# The strided run of a row whose rows below take one digit is the fiber of
476	# that row from the same digit, one more word than the run's fuel.
477	def run_fiber(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
478	  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
479	  -array: Array<F32>, pair: Array<F32> & F32,
480	  -read: {pair == Array.get(F32, array, U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))) : Array<F32> & F32}) ->
481	  Generic.Fact<{Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, pair) ==
482	    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}>:
483	  match fuel pair:
484	    case 0n Tuple{kept, word}:
485	      Generic.Fact{Equal.sym(F32 & Array<F32>,
486	        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array),
487	        (F32.add(accumulator, word), kept),
488	        {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) ==
489	          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
490	          {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) ==
491	            (F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
492	          fiber_step(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, array, kept, word, read)))}
493	    case 1n+remaining Tuple{kept, word}:
494	      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
495	      Generic.Fact{Equal.trans(F32 & Array<F32>,
496	        Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
497	          Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))),
498	        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept),
499	        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array),
500	        {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
501	          Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) ==
502	          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
503	          {Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
504	            Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) ==
505	            Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
506	          run_fiber(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, F32.add(accumulator, word), kept,
507	            Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift))), {==})),
508	        Equal.sym(F32 & Array<F32>,
509	          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array),
510	          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept),
511	          {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) ==
512	            Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
513	            {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) ==
514	              Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
515	            fiber_step(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, array, kept, word, read))))}
516	
517	# The strided loop of such a row is its fiber.
518	def strided_fiber(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
519	  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
520	  array: Array<F32>) ->
521	  Generic.Fact<{Reduce.strided(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, array) ==
522	    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}>:
523	  match fuel:
524	    case 0n:
525	      Generic.Fact{{==}}
526	    case 1n+remaining:
527	      run_fiber(stride, left, right, rest, extent, others, single, remaining, target, base, digit, accumulator, array,
528	        Array.get(F32, array, U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))), {==})
529	
530	# What a fast fiber's flag promises: True only where the rows below the
531	# first take one digit each.
532	def SingleOk(single: Bool, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>) -> Data:
533	  match single:
534	    case True{}:
535	      {Reduce.single_below(rows, extents) == True{} : Bool}
536	    case False{}:
537	      Unit
538	
539	def single_ok(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, single: Bool,
540	  +exact: {single == Reduce.single_below(rows, extents) : Bool}) -> SingleOk(single, rows, extents):
541	  match single:
542	    case True{}:
543	      Equal.sym(Bool, True{}, Reduce.single_below(rows, extents), exact)
544	    case False{}:
545	      Unit{}
546	
547	# Two closures equal on every argument continue a pair alike.
548	def next_same(-fast: F32 -> Array<F32> -> F32 & Array<F32>, -slow: F32 -> Array<F32> -> F32 & Array<F32>,
549	  same: @value: F32 -> @array: Array<F32> -> Generic.Fact<{fast(value, array) == slow(value, array) : F32 & Array<F32>}>,
550	  pair: F32 & Array<F32>) -> Generic.Fact<{Reduce.walk_next(fast, pair) == Reduce.walk_next(slow, pair) : F32 & Array<F32>}>:
551	  match pair:
552	    case Tuple{value, array}:
553	      same(value, array)
554	
555	# The fast fiber returns what the fiber returns.
556	def fast_fiber(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, fuel: Nat, single: Bool, -ok: SingleOk(single, rows, extents),
557	  +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32, -array: Array<F32>) ->
558	  Generic.Fact<{Reduce.fiber_fast(rows, extents, fuel, single, target, base, digit, accumulator, array) ==
559	    Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}>:
560	  match rows extents fuel single:
561	    case Nil{} _ _ single:
562	      Generic.Fact{{==}}
563	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others fuel True{}:
564	      Generic.Fact{{\{Generic.Fact: p => p} : Generic.Fact<({Reduce.strided(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, array) ==
565	        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, digit, accumulator, array) : F32 & Array<F32>})> ->
566	        {Reduce.strided(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, array) ==
567	          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}}(
568	        strided_fiber(stride, left, right, rest, extent, others, ok, fuel, target, base, digit, accumulator, array))}
569	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n False{}:
570	      Generic.Fact{{==}}
571	    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining False{}:
572	      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
573	      +extents : List<&2, Nat> = extent <> others
574	      +inner = Nat.mod(target, left)
575	      +offset = Nat.add(base, Nat.mul(right, digit))
576	      Generic.Fact{Equal.trans(F32 & Array<F32>,
577	        Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k),
578	          Reduce.fiber_fast(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)),
579	        Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k),
580	          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)),
581	        Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
582	          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)),
583	        Equal.cong(F32 & Array<F32>, F32 & Array<F32>,
584	          p => Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k), p),
585	          Reduce.fiber_fast(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array),
586	          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array),
587	          {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber_fast(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
588	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) : F32 & Array<F32>})> ->
589	            {Reduce.fiber_fast(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) ==
590	              Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array) : F32 & Array<F32>}}(
591	            fast_fiber(rest, others, Reduce.first_span(rest, others), Reduce.single_below(rest, others),
592	              single_ok(rest, others, Reduce.single_below(rest, others), {==}), inner, offset, Reduce.first_digit(rest, inner), accumulator, array))),
593	        {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k),
594	          Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)) ==
595	          Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
596	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)) : F32 & Array<F32>})> ->
597	          {Reduce.walk_next(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k),
598	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)) ==
599	            Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
600	              Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array)) : F32 & Array<F32>}}(
601	          next_same(v => k => Reduce.fiber_fast(rows, extents, remaining, False{}, target, base, 1n+digit, v, k),
602	            v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k),
603	            value => kept => fast_fiber(rows, extents, remaining, False{}, Unit{}, target, base, 1n+digit, value, kept),
604	            Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, array))))}
605	    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _ single:
606	      Generic.Fact{{==}}
607	
608	# The offsets the walk of cell `position` reads.
609	def visited_of(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat) -> List<&2, Nat>:
610	  Fiber.visited(rows, extents, Reduce.first_span(rows, extents), position, 0n, Reduce.first_digit(rows, position))
611	
612	# What target cell `position` holds: below `count`, the total of the words
613	# its walk saw, from +0.0; at or above it, +0.0.
614	type CellAt<-d: Nat, -A: Array<F32>, -rows: List<&2, Shape.Row>, -extents: List<&2, Nat>, -position: Nat, -value: Maybe<&2, F32>> is Data:
615	  CellAt{-word: F32, -observed: {value == Some{word} : Maybe<&2, F32>}, -words: List<&2, F32>,
616	    -seen: Obs(d, A, visited_of(rows, extents, position), words), -total: {word == fsum(words, 0.0) : F32}}
617	
618	def CellSpec(+d: Nat, -A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, inside: Bool,
619	  -value: Maybe<&2, F32>) -> Type:
620	  match inside:
621	    case False{}:
622	      {value == Some{0.0} : Maybe<&2, F32>}
623	    case True{}:
624	      CellAt<d, A, rows, extents, position, value>
625	
626	def CellIs(+d: Nat, -A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +count: Nat, +position: Nat,
627	  -value: Maybe<&2, F32>) -> Type:
628	  CellSpec(d, A, rows, extents, position, Nat.is_lt(position, count), value)
629	
630	def Cells(+depth: Nat, +d: Nat, -A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +count: Nat, +base: Nat,
631	  -out: Array<F32>) -> Type:
632	  @+path: Model.Path(depth) ->
633	    CellIs(d, A, rows, extents, count, Nat.add(Model.offset(depth, path), base), Model.observe(F32, depth, out, path))
634	
635	# The reduce cell function of `Parallel.build`, from the contribution array.
636	def cell_of(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, A: Array<F32>, inside: Bool) -> F32 & (Array<F32> & Unit):
637	  Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, extents}), position, (A, Unit{}), inside)
638	
639	def keep_equal(pair: F32 & Array<F32>, -none: Unit) ->
640	  {Reduce.keep(pair, none) == (Pair.fst(F32, Array<F32>, pair), (Pair.snd(F32, Array<F32>, pair), none)) : F32 & (Array<F32> & Unit)}:
641	  (value, array) = pair
642	  {==}
643	
644	def run_of(+d: Nat, A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, -valid: Model.Balanced(F32, d, A)) ->
645	  Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>>:
646	  +fuel = Reduce.first_span(rows, extents)
647	  +digit = Reduce.first_digit(rows, position)
648	  Parallel.Fact{
649	    %Equal.sym(F32 & Array<F32>, Reduce.fiber_of(rows, extents, position, A), Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A),
650	      {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber_of(rows, extents, position, A) == Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A) : F32 & Array<F32>})> ->
651	        {Reduce.fiber_of(rows, extents, position, A) == Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A) : F32 & Array<F32>}}(
652	        fast_fiber(rows, extents, fuel, Reduce.single_below(rows, extents), single_ok(rows, extents, Reduce.single_below(rows, extents), {==}),
653	          position, 0n, digit, 0.0, A))) :
654	      FiberRun<d, A, visited_of(rows, extents, position), 0.0, _>
655	    {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A)>> ->
656	      FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A)>}(
657	      fiber_run(rows, extents, fuel, position, 0n, digit, d, A, 0.0, A, {==}, valid))}
658	
659	# Every cell hands the contribution array back.
660	def cell_keeps(+d: Nat, A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, inside: Bool,
661	  -valid: Model.Balanced(F32, d, A)) ->
662	  Parallel.Fact<{Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, position, A, inside)) == (A, Unit{}) : Array<F32> & Unit}>:
663	  match inside:
664	    case False{}:
665	      Parallel.Fact{{==}}
666	    case True{}:
667	      Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
668	        %Equal.sym(F32 & (Array<F32> & Unit), Reduce.keep(Reduce.fiber_of(rows, extents, position, A), Unit{}),
669	          (Pair.fst(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), (Pair.snd(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), Unit{})),
670	          keep_equal(Reduce.fiber_of(rows, extents, position, A), Unit{})) :
671	          {Pair.snd(F32, Array<F32> & Unit, _) == (A, Unit{}) : Array<F32> & Unit}
672	        Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), Pair.snd(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), A, kept)} :
673	        FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)> ->
674	        {Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, position, A, True{})) == (A, Unit{}) : Array<F32> & Unit}}(
675	        {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>> ->
676	          FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>}(
677	          run_of(d, A, rows, extents, position, valid)))}
678	
679	# What the cell function computes is what CellSpec names.
680	def cell_spec(+d: Nat, A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, inside: Bool,
681	  -observed: Maybe<&2, F32>, -computed: {observed == Some{Pair.fst(F32, Array<F32> & Unit, cell_of(rows, extents, position, A, inside))} : Maybe<&2, F32>},
682	  -valid: Model.Balanced(F32, d, A)) ->
683	  Parallel.Fact<CellSpec(d, A, rows, extents, position, inside, observed)>:
684	  match inside:
685	    case False{}:
686	      Parallel.Fact{computed}
687	    case True{}:
688	      Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
689	        CellAt{Pair.fst(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)),
690	          %keep_equal(Reduce.fiber_of(rows, extents, position, A), Unit{}) :
691	            {observed == Some{Pair.fst(F32, Array<F32> & Unit, _)} : Maybe<&2, F32>}
692	          computed,
693	          words, seen, total}} :
694	        FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)> ->
695	        CellAt<d, A, rows, extents, position, observed>}(
696	        {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>> ->
697	          FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>}(
698	          run_of(d, A, rows, extents, position, valid)))}
699	
700	# A split hands each half the contribution array.
701	def halves_equal(+d: Nat, -A: Array<F32>, pair: Array<F32> & Array<F32>, -exact: {pair == Array.clone(F32, A) : Array<F32> & Array<F32>},
702	  -valid: Model.Balanced(F32, d, A)) ->
703	  Parallel.Fact<({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(pair)) == (A, Unit{}) : Array<F32> & Unit} &
704	    {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(pair)) == (A, Unit{}) : Array<F32> & Unit})>:
705	  (first, second) = pair
706	  Parallel.Fact{(
707	    Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), first, A,
708	      {\{Parallel.Fact: p => p} : Parallel.Fact<({Pair.fst(Array<F32>, Array<F32>, (first, second)) == A : Array<F32>})> ->
709	        {Pair.fst(Array<F32>, Array<F32>, (first, second)) == A : Array<F32>}}(Parallel.clone_first(d, A, A, (first, second), exact, {==}, valid))),
710	    Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), second, A,
711	      {\{Parallel.Fact: p => p} : Parallel.Fact<({Pair.snd(Array<F32>, Array<F32>, (first, second)) == A : Array<F32>})> ->
712	        {Pair.snd(Array<F32>, Array<F32>, (first, second)) == A : Array<F32>}}(Parallel.clone_second(d, A, A, (first, second), exact, {==}, valid))))}
713	
714	# Whatever the split, every cell of the parallel build holds what CellIs
715	# names: the generic law of `Parallel.build`, with the reduce cell.
716	def build_cells(+depth: Nat, +splits: Nat, +d: Nat, -A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +count: Nat,
717	  +base: Nat, array: Array<F32>, -same: {array == A : Array<F32>}, -valid: Model.Balanced(F32, d, A)) ->
718	  Parallel.Fact<Cells(depth, d, A, rows, extents, count, base, Reduce.build(depth, splits, rows, extents, count, base, array))>:
719	  -split = {\{Parallel.Fact: q => q} : Parallel.Fact<({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit} &
720	    {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit})> ->
721	    {Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit} &
722	    {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}}(
723	    halves_equal(d, A, Array.clone(F32, A), {==}, valid))
724	  -cells = {\{Generic.Fact: q => q} :
725	    Generic.Fact<Generic.Cells(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base,
726	      Reduce.build(depth, splits, rows, extents, count, base, array))> ->
727	    Generic.Cells(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base,
728	      Reduce.build(depth, splits, rows, extents, count, base, array))}(
729	    Generic.build_cells(~Reduce.Fibers, ~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.fibers, ~Reduce.split, ~Reduce.cell_at,
730	      Reduce.Fibers{rows, extents}, (A, Unit{}), depth, splits, count, base, (array, Unit{}),
731	      Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), array, A, same),
732	      at => inside => {\{Parallel.Fact: q => q} :
733	        Parallel.Fact<({Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array<F32> & Unit})> ->
734	        {Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array<F32> & Unit}}(
735	        cell_keeps(d, A, rows, extents, at, inside, valid)),
736	      Pair.fst({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit},
737	        {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}, split),
738	      Pair.snd({Pair.fst(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit},
739	        {Pair.snd(Array<F32> & Unit, Array<F32> & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array<F32> & Unit}, split)))
740	  Parallel.Fact{path => {\{Parallel.Fact: q => q} :
741	    Parallel.Fact<CellSpec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
742	      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path))> ->
743	    CellSpec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
744	      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path))}(
745	    cell_spec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count),
746	      Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path), cells(path), valid))}
747	
748	# The words a walk saw are the contribution's words at the offsets it read.
749	def Reads(+d: Nat, -A: Array<F32>, +values: List<&2, F32>, +bound: Nat) -> Type:
750	  @+position: Nat -> @inside: {Nat.is_lt(position, bound) == True{} : Bool} ->
751	    {Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(position))) == ReduceLaws.word_at(values, position) : Maybe<&2, F32>}
752	
753	def obs_gather(+d: Nat, -A: Array<F32>, +values: List<&2, F32>, +bound: Nat, +positions: List<&2, Nat>, +words: List<&2, F32>,
754	  +accumulator: F32, -seen: Obs(d, A, positions, words), +below: {all_below(positions, bound) == True{} : Bool},
755	  -reads: Reads(d, A, values, bound)) ->
756	  Parallel.Fact<{Some{fsum(words, accumulator)} == gather(values, positions, Some{accumulator}) : Maybe<&2, F32>}>:
757	  match positions words:
758	    case Nil{} Nil{}:
759	      Parallel.Fact{{==}}
760	    case +p <> +ps +w <> +ws:
761	      +inside = Arith.and_left(Nat.is_lt(p, bound), all_below(ps, bound), below)
762	      +others = Arith.and_right(Nat.is_lt(p, bound), all_below(ps, bound), below)
763	      Parallel.Fact{{\{ObsStep: observed => more =>
764	        %Equal.sym(Maybe<&2, F32>, ReduceLaws.word_at(values, p), Some{w},
765	          Equal.trans(Maybe<&2, F32>, ReduceLaws.word_at(values, p), Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(p))), Some{w},
766	            Equal.sym(Maybe<&2, F32>, Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(p))), ReduceLaws.word_at(values, p), reads(p, inside)),
767	            observed)) :
768	          {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, ReduceLaws.add_word(Some{accumulator}, _)) : Maybe<&2, F32>}
769	        {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, Some{F32.add(accumulator, w)}) : Maybe<&2, F32>}> ->
770	          {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, Some{F32.add(accumulator, w)}) : Maybe<&2, F32>}}(
771	          obs_gather(d, A, values, bound, ps, ws, F32.add(accumulator, w), more, others, reads))} :
772	        ObsStep<d, A, p, w, ps, ws> -> {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, p <> ps, Some{accumulator}) : Maybe<&2, F32>}}(seen)}
773	    case Nil{} +w <> +ws:
774	      Parallel.Fact{Empty.absurd({Some{fsum(w <> ws, accumulator)} == gather(values, Nil{}, Some{accumulator}) : Maybe<&2, F32>}, seen)}
775	    case +p <> +ps Nil{}:
776	      Parallel.Fact{Empty.absurd({Some{accumulator} == gather(values, p <> ps, Some{accumulator}) : Maybe<&2, F32>}, seen)}
777	
778	# A cell of the parallel build holds `ReduceLaws.fiber`: the words its walk
779	# saw add up, from +0.0, to the masked fold over the contribution.
780	def cell_value(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
781	  +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>},
782	  +values: List<&2, F32>, +index: U32, +d: Nat, -A: Array<F32>, +words: List<&2, F32>,
783	  -seen: Obs(d, A, visited_of(rows, Shape.extents(Shape.output_shape(plan)), U32.to_nat(index)), words),
784	  +inside: {Nat.is_lt(U32.to_nat(index), Shape.numel(Shape.extents(Shape.left_shape(plan)))) == True{} : Bool},
785	  -reads: Reads(d, A, values, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))))) ->
786	  Parallel.Fact<{Some{fsum(words, 0.0)} == ReduceLaws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}>:
787	  +t = U32.to_nat(index)
788	  +output = Shape.extents(Shape.output_shape(plan))
789	  +count = Shape.numel(output)
790	  +walk = plan_walk(plan, rows, exact, t, inside)
791	  +spot = masked_below(plan, rows, exact, t, count, 0n, Conversion.le_reflexive(count))
792	  Parallel.Fact{
793	    %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, count), gather(values, Fiber.masked(count, rows, t, 0n, 0n), Some{0.0}),
794	      fiber_masked(plan, rows, exact, values, index, count, Conversion.le_reflexive(count))) :
795	      {Some{fsum(words, 0.0)} == _ : Maybe<&2, F32>}
796	    %Equal.sym(List<&2, Nat>, Fiber.masked(count, rows, t, 0n, 0n), visited_of(rows, output, t), walk) :
797	      {Some{fsum(words, 0.0)} == gather(values, _, Some{0.0}) : Maybe<&2, F32>}
798	    {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{fsum(words, 0.0)} == gather(values, visited_of(rows, output, t), Some{0.0}) : Maybe<&2, F32>}> ->
799	      {Some{fsum(words, 0.0)} == gather(values, visited_of(rows, output, t), Some{0.0}) : Maybe<&2, F32>}}(
800	      obs_gather(d, A, values, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), visited_of(rows, output, t), words, 0.0, seen,
801	        %walk :
802	          {all_below(_, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool}
803	        spot,
804	        reads))}