src/autograd/reduce_parallel_proof.bend

bendtorch-core@0.1.0.0 · 804 lines · 50 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
4import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
5import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
6import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
7import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
8import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
9import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ShapeProjection
10import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
11import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
12import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
13import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
14import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
15import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as BroadcastMap
16import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend as BroadcastProof
17import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
18import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
19import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
20import bendtorch-core@0.1.0.0/src/autograd/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
28def 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
36def 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
43def 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.
52def 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.
68def 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.
81def 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.
113def 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
120def 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
128def 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
136def 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.
142def 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.
191def 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
198def 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
208def 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
229def 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
236def 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.
245def 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
256type 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
259def 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.
277type 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
282def 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
296def 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
318def 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
348def 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.
357def 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.
379def 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
386def 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`.
391def 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.
432def 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.
477def 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.
518def 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.
532def 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
539def 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.
548def 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.
556def 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.
609def 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.
614type 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
618def 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
626def 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
630def 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.
636def 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
639def 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
644def 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.
660def 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.
680def 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.
701def 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.
716def 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.
749def 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
753def 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.
780def 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))}