1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/model.bend as Model
4	import ../storage/refinement.bend as Refinement
5	import ./core.bend as Core
6	import ./layout.bend as Layout
7	import ./slice.bend as Slice
8	import ./signed.bend as Signed
9	import ./gather.bend as Gather
10	import ./gather_LAWS.bend as Laws
11	import ../storage/clone.bend as Clone
12	import ../shape/plan_proofs.bend as Plans
13	import ./parallel_proofs.bend as Generic
14	import ./batched_matmul_PROOF.bend as BatchedProof
15	
16	# The checks and the plans.
17	
18	def count_length(entries: List<&2, U32>) -> {Gather.count(entries) == Laws.length(entries) : Nat}:
19	  match entries:
20	    case Nil{}:
21	      {==}
22	    case head <> rest:
23	      Equal.cong(Nat, Nat, x => 1n+x, Gather.count(rest), Laws.length(rest), count_length(rest))
24	
25	def below_inside(entries: List<&2, U32>, +bound: Nat) -> {Gather.below(entries, bound) == Laws.inside(entries, bound) : Bool}:
26	  match entries:
27	    case Nil{}:
28	      {==}
29	    case +head <> rest:
30	      Equal.cong(Bool, Bool, x => Bool.and(Nat.is_lt(U32.to_nat(head), bound), x), Gather.below(rest, bound), Laws.inside(rest, bound),
31	        below_inside(rest, bound))
32	
33	def equal_same(left: List<&2, U32>, right: List<&2, U32>) -> {Gather.equal(left, right) == Laws.equal(left, right) : Bool}:
34	  match left right:
35	    case Nil{} Nil{}:
36	      {==}
37	    case +x <> xs +y <> ys:
38	      Equal.cong(Bool, Bool, b => Bool.and(Nat.is_eq(U32.to_nat(x), U32.to_nat(y)), b), Gather.equal(xs, ys), Laws.equal(xs, ys),
39	        equal_same(xs, ys))
40	    case Nil{} y <> ys:
41	      {==}
42	    case x <> xs Nil{}:
43	      {==}
44	
45	def matches_others(dimensions: List<&2, U32>, index: List<&2, U32>, +at: Nat) ->
46	  {Gather.matches(dimensions, index, at) == Laws.others(dimensions, index, at) : Bool}:
47	  match dimensions index at:
48	    case x <> xs y <> ys 0n:
49	      equal_same(xs, ys)
50	    case +x <> xs +y <> ys 1n+next:
51	      Equal.cong(Bool, Bool, b => Bool.and(Nat.is_eq(U32.to_nat(x), U32.to_nat(y)), b), Gather.matches(xs, ys, next), Laws.others(xs, ys, next),
52	        matches_others(xs, ys, next))
53	    case Nil{} index at:
54	      {==}
55	    case x <> xs Nil{} at:
56	      {==}
57	
58	def viewed_same(+kind: Gather.Lookup, +given: Slice.View, +count: Nat) ->
59	  {Gather.viewed(kind, given, count) == Laws.viewed(kind, given, count) : Gather.Plan}:
60	  Slice.View{+outer, +rows, +inner} = given
61	  {==}
62	
63	def shaped_same(+plan: Gather.Plan, -dimensions: List<&2, U32>, built: Shape.ConstructResult<dimensions>) ->
64	  {Gather.shaped(plan, dimensions, built) == Laws.output(dimensions, plan, built) : Result<&2, &2, Gather.Error, Gather.Planned>}:
65	  match built:
66	    case Shape.SError{error}:
67	      {==}
68	    case Shape.SBuilt{+shape, preserved}:
69	      {==}
70	
71	# An accepted request's plan and output are what the laws name.
72	def accepted_taken(+kind: Gather.Lookup, +dimensions: List<&2, U32>, +at: Nat, +count: Nat) ->
73	  {Gather.accepted(kind, dimensions, at, count) == Laws.taken(kind, dimensions, at, count) : Result<&2, &2, Gather.Error, Gather.Planned>}:
74	  Equal.trans(Result<&2, &2, Gather.Error, Gather.Planned>, Gather.accepted(kind, dimensions, at, count),
75	    Gather.shaped(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
76	      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
77	    Laws.taken(kind, dimensions, at, count),
78	    Equal.cong(Gather.Plan, Result<&2, &2, Gather.Error, Gather.Planned>,
79	      p => Gather.shaped(p, Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
80	      Gather.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
81	      Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
82	      viewed_same(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count)),
83	    shaped_same(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
84	      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))))
85	
86	# below(entries, bound) is the laws' inside, so it rewrites to its value.
87	def below_is(+entries: List<&2, U32>, +bound: Nat, +value: Bool, given: {Laws.inside(entries, bound) == value : Bool}) ->
88	  {value == Gather.below(entries, bound) : Bool}:
89	  Equal.sym(Bool, Gather.below(entries, bound), value,
90	    Equal.trans(Bool, Gather.below(entries, bound), Laws.inside(entries, bound), value, below_inside(entries, bound), given))
91	
92	def Laws.index_select_axis_refused(input, dim, entries, outside):
93	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), False{}, outside) :
94	    {Gather.selecting(Shape.dimensions(input), Laws.axis(input, dim), entries, _) == Fail{Gather.LayoutError{Layout.AxisOutOfBounds{}}} :
95	      Result<&2, &2, Gather.Error, Gather.Planned>}
96	  {==}
97	
98	def Laws.index_select_out_of_range(input, dim, entries, in_rank, past):
99	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
100	    {Gather.selecting(Shape.dimensions(input), Laws.axis(input, dim), entries, _) == Fail{Gather.OutOfRange{}} :
101	      Result<&2, &2, Gather.Error, Gather.Planned>}
102	  %below_is(entries, Laws.extent(input, Laws.axis(input, dim)), False{}, past) :
103	    {Gather.ranged(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), entries, Gather.count(entries), _) == Fail{Gather.OutOfRange{}} :
104	      Result<&2, &2, Gather.Error, Gather.Planned>}
105	  {==}
106	
107	def Laws.index_select_planned(input, dim, entries, in_rank, within):
108	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
109	    {Gather.selecting(Shape.dimensions(input), Laws.axis(input, dim), entries, _) ==
110	      Laws.taken(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), Laws.length(entries)) : Result<&2, &2, Gather.Error, Gather.Planned>}
111	  %below_is(entries, Laws.extent(input, Laws.axis(input, dim)), True{}, within) :
112	    {Gather.ranged(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), entries, Gather.count(entries), _) ==
113	      Laws.taken(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), Laws.length(entries)) : Result<&2, &2, Gather.Error, Gather.Planned>}
114	  %Equal.sym(Nat, Gather.count(entries), Laws.length(entries), count_length(entries)) :
115	    {Gather.accepted(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), _) ==
116	      Laws.taken(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), Laws.length(entries)) : Result<&2, &2, Gather.Error, Gather.Planned>}
117	  accepted_taken(Gather.Selected{}, Shape.dimensions(input), Laws.axis(input, dim), Laws.length(entries))
118	
119	# The entry count rewrites to its value.
120	def counted_is(+entries: List<&2, U32>, +index: Shape.Shape, +value: Bool,
121	  given: {Nat.is_eq(Laws.length(entries), Shape.elements(index)) == value : Bool}) ->
122	  {value == Nat.is_eq(Gather.count(entries), Shape.elements(index)) : Bool}:
123	  Equal.sym(Bool, Nat.is_eq(Gather.count(entries), Shape.elements(index)), value,
124	    Equal.trans(Bool, Nat.is_eq(Gather.count(entries), Shape.elements(index)), Nat.is_eq(Laws.length(entries), Shape.elements(index)),
125	      value,
126	      Equal.cong(Nat, Bool, n => Nat.is_eq(n, Shape.elements(index)), Gather.count(entries), Laws.length(entries), count_length(entries)),
127	      given))
128	
129	def matched_is(+dimensions: List<&2, U32>, +index: List<&2, U32>, +at: Nat, +value: Bool,
130	  given: {Laws.others(dimensions, index, at) == value : Bool}) -> {value == Gather.matches(dimensions, index, at) : Bool}:
131	  Equal.sym(Bool, Gather.matches(dimensions, index, at), value,
132	    Equal.trans(Bool, Gather.matches(dimensions, index, at), Laws.others(dimensions, index, at), value, matches_others(dimensions, index, at), given))
133	
134	def Laws.gather_count_refused(input, dim, index, entries, miscounted):
135	  %counted_is(entries, index, False{}, miscounted) :
136	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
137	      Fail{Gather.TensorError{Core.ValueCountMismatch{}}} : Result<&2, &2, Gather.Error, Gather.Planned>}
138	  {==}
139	
140	def Laws.gather_axis_refused(input, dim, index, entries, counted, outside):
141	  %counted_is(entries, index, True{}, counted) :
142	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
143	      Fail{Gather.LayoutError{Layout.AxisOutOfBounds{}}} : Result<&2, &2, Gather.Error, Gather.Planned>}
144	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), False{}, outside) :
145	    {Gather.gather_axis(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
146	      Fail{Gather.LayoutError{Layout.AxisOutOfBounds{}}} : Result<&2, &2, Gather.Error, Gather.Planned>}
147	  {==}
148	
149	def Laws.gather_rank_refused(input, dim, index, entries, counted, in_rank, ranked):
150	  %counted_is(entries, index, True{}, counted) :
151	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
152	      Fail{Gather.IndexRankMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
153	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
154	    {Gather.gather_axis(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
155	      Fail{Gather.IndexRankMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
156	  %Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(index)), Laws.rank(input)), False{}, ranked) :
157	    {Gather.gather_ranked(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
158	      Fail{Gather.IndexRankMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
159	  {==}
160	
161	def Laws.gather_shape_refused(input, dim, index, entries, counted, in_rank, ranked, unmatched):
162	  %counted_is(entries, index, True{}, counted) :
163	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
164	      Fail{Gather.IndexShapeMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
165	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
166	    {Gather.gather_axis(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
167	      Fail{Gather.IndexShapeMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
168	  %Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(index)), Laws.rank(input)), True{}, ranked) :
169	    {Gather.gather_ranked(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
170	      Fail{Gather.IndexShapeMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
171	  %matched_is(Shape.dimensions(input), Shape.dimensions(index), Laws.axis(input, dim), False{}, unmatched) :
172	    {Gather.gather_shaped(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
173	      Fail{Gather.IndexShapeMismatch{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
174	  {==}
175	
176	def Laws.gather_out_of_range(input, dim, index, entries, counted, in_rank, ranked, matched, past):
177	  %counted_is(entries, index, True{}, counted) :
178	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
179	      Fail{Gather.OutOfRange{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
180	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
181	    {Gather.gather_axis(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
182	      Fail{Gather.OutOfRange{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
183	  %Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(index)), Laws.rank(input)), True{}, ranked) :
184	    {Gather.gather_ranked(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
185	      Fail{Gather.OutOfRange{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
186	  %matched_is(Shape.dimensions(input), Shape.dimensions(index), Laws.axis(input, dim), True{}, matched) :
187	    {Gather.gather_shaped(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
188	      Fail{Gather.OutOfRange{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
189	  %below_is(entries, Laws.extent(input, Laws.axis(input, dim)), False{}, past) :
190	    {Gather.ranged(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), entries,
191	      Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim)), _) == Fail{Gather.OutOfRange{}} : Result<&2, &2, Gather.Error, Gather.Planned>}
192	  {==}
193	
194	def Laws.gather_planned(input, dim, index, entries, counted, in_rank, ranked, matched, within):
195	  %counted_is(entries, index, True{}, counted) :
196	    {Gather.gather_counted(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
197	      Laws.taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim))) :
198	      Result<&2, &2, Gather.Error, Gather.Planned>}
199	  %Equal.sym(Bool, Nat.is_lt(Laws.axis(input, dim), Laws.rank(input)), True{}, in_rank) :
200	    {Gather.gather_axis(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
201	      Laws.taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim))) :
202	      Result<&2, &2, Gather.Error, Gather.Planned>}
203	  %Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(index)), Laws.rank(input)), True{}, ranked) :
204	    {Gather.gather_ranked(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
205	      Laws.taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim))) :
206	      Result<&2, &2, Gather.Error, Gather.Planned>}
207	  %matched_is(Shape.dimensions(input), Shape.dimensions(index), Laws.axis(input, dim), True{}, matched) :
208	    {Gather.gather_shaped(Shape.dimensions(input), Laws.axis(input, dim), Shape.dimensions(index), entries, _) ==
209	      Laws.taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim))) :
210	      Result<&2, &2, Gather.Error, Gather.Planned>}
211	  %below_is(entries, Laws.extent(input, Laws.axis(input, dim)), True{}, within) :
212	    {Gather.ranged(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), entries,
213	      Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim)), _) ==
214	      Laws.taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim))) :
215	      Result<&2, &2, Gather.Error, Gather.Planned>}
216	  accepted_taken(Gather.Gathered{}, Shape.dimensions(input), Laws.axis(input, dim), Slice.axis_extent(Shape.dimensions(index), Laws.axis(input, dim)))
217	
218	def Laws.index_select_refused(input, dim, entries, error, refused):
219	  Core.Packed{+shape, tensor} = input
220	  %Equal.sym(Result<&2, &2, Gather.Error, Gather.Planned>, Gather.select_plan(shape, dim, entries), Fail{error}, refused) :
221	    {Gather.copied(shape, tensor, entries, _) == (Core.Packed{shape, tensor}, Fail{error}) : Core.Dynamic & Result<&2, &1, Gather.Error, Core.Dynamic>}
222	  {==}
223	
224	def Laws.gather_refused(input, dim, index, entries, error, refused):
225	  Core.Packed{+shape, tensor} = input
226	  %Equal.sym(Result<&2, &2, Gather.Error, Gather.Planned>, Gather.gather_plan(shape, dim, Gather.Index{index, entries}), Fail{error}, refused) :
227	    {Gather.copied(shape, tensor, entries, _) == (Core.Packed{shape, tensor}, Fail{error}) : Core.Dynamic & Result<&2, &1, Gather.Error, Core.Dynamic>}
228	  {==}
229	
230	# The cells of the forward build.
231	
232	def balanced_as(-T: Data, -d: Nat, -a: Array<T>, -b: Array<T>, -same: {a == b : Array<T>}, -valid: Model.Balanced(T, d, b)) ->
233	  Generic.Fact<Model.Balanced(T, d, a)>:
234	  Generic.Fact{
235	    %Equal.sym(Array<T>, a, b, same) : Model.Balanced(T, d, _)
236	    valid}
237	
238	def take_snd(index: Array<U32>, pair: Array<F32> & F32) ->
239	  {Pair.snd(F32, Array<F32> & Array<U32>, Gather.take(index, pair)) == (Refinement.first(F32, pair), index) : Array<F32> & Array<U32>}:
240	  (a, x) = pair
241	  {==}
242	
243	def take_fst(index: Array<U32>, pair: Array<F32> & F32) ->
244	  {Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, pair)) == Refinement.second(F32, pair) : F32}:
245	  (a, x) = pair
246	  {==}
247	
248	def both(-a: Array<F32>, -b: Array<U32>, -A: Array<F32>, -B: Array<U32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<U32>}) ->
249	  {(a, b) == (A, B) : Array<F32> & Array<U32>}:
250	  Equal.trans(Array<F32> & Array<U32>, (a, b), (A, b), (A, B),
251	    Equal.cong(Array<F32>, Array<F32> & Array<U32>, x => (x, b), a, A, ea),
252	    Equal.cong(Array<U32>, Array<F32> & Array<U32>, y => (A, y), b, B, eb))
253	
254	# A forward read hands both arrays back ...
255	def looked_keeps(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, -I: Array<U32>, pair: Array<U32> & U32,
256	  -kept: {Refinement.first(U32, pair) == I : Array<U32>}, -valid: Model.Balanced(F32, da, A)) ->
257	  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair)) == (A, I) : Array<F32> & Array<U32>}>:
258	  (index, +j) = pair
259	  Generic.Fact{Equal.trans(Array<F32> & Array<U32>, Pair.snd(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j)))))),
260	    (Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index), (A, I),
261	    take_snd(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))),
262	    both(Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index, A, I,
263	      Refinement.law_get_retains(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))), valid), kept))}
264	
265	def cell_keeps(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, inside: Bool,
266	  -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
267	  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.cell(plan, at, (A, I), inside)) == (A, I) : Array<F32> & Array<U32>}>:
268	  match inside:
269	    case False{}:
270	      Generic.Fact{{==}}
271	    case True{}:
272	      Generic.Fact{{\{Generic.Fact: q => q} :
273	        Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, Array.get(U32, I, U32.from_nat(Gather.entry(plan, at))))) == (A, I) : Array<F32> & Array<U32>}> ->
274	        {Pair.snd(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, Array.get(U32, I, U32.from_nat(Gather.entry(plan, at))))) == (A, I) : Array<F32> & Array<U32>}}(
275	        looked_keeps(plan, at, da, A, I, Array.get(U32, I, U32.from_nat(Gather.entry(plan, at))),
276	          Refinement.law_get_retains(U32, di, I, U32.from_nat(Gather.entry(plan, at)), index_valid), valid))}
277	
278	# ... and gives the input word at the entry it read.
279	def looked_value(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, pair: Array<U32> & U32, +j: U32,
280	  -seen: {Refinement.second(U32, pair) == j : U32}, -valid: Model.Balanced(F32, da, A)) ->
281	  Generic.Fact<{Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair))} ==
282	    Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))) : Maybe<&2, F32>}>:
283	  (index, +found) = pair
284	  Generic.Fact{
285	    %seen : {Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))} ==
286	      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(_))))) : Maybe<&2, F32>}
287	    Equal.trans(Maybe<&2, F32>, Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))},
288	      Some{Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))},
289	      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
290	      Equal.cong(F32, Maybe<&2, F32>, x => Some{x},
291	        Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
292	        Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
293	        take_fst(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
294	      Refinement.law_get_refines(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))), valid))}
295	
296	# The entry read is the one the index array holds there.
297	def read_entry(+di: Nat, -I: Array<U32>, +e: Nat, +j: U32,
298	  -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(e))) == Some{j} : Maybe<&2, U32>},
299	  -index_valid: Model.Balanced(U32, di, I)) ->
300	  Generic.Fact<{Refinement.second(U32, Array.get(U32, I, U32.from_nat(e))) == j : U32}>:
301	  Generic.Fact{Plans.some_injective(U32, Refinement.second(U32, Array.get(U32, I, U32.from_nat(e))), j,
302	    Equal.trans(Maybe<&2, U32>, Some{Refinement.second(U32, Array.get(U32, I, U32.from_nat(e)))},
303	      Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(e))), Some{j},
304	      Refinement.law_get_refines(U32, di, I, U32.from_nat(e), index_valid), read))}
305	
306	def SplitFacts(-A: Array<F32>, -I: Array<U32>) -> Type:
307	  {Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>} & {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>}
308	
309	def halves_facts(+da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, lp: Array<F32> & Array<F32>, rp: Array<U32> & Array<U32>,
310	  -le: {lp == Array.clone(F32, A) : Array<F32> & Array<F32>}, -re: {rp == Array.clone(U32, I) : Array<U32> & Array<U32>},
311	  -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
312	  Generic.Fact<({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.halves(lp, rp)) == (A, I) : Array<F32> & Array<U32>} & {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.halves(lp, rp)) == (A, I) : Array<F32> & Array<U32>})>:
313	  (l1, l2) = lp
314	  (r1, r2) = rp
315	  Generic.Fact{(
316	    both(l1, r1, A, I,
317	      Equal.trans(Array<F32>, l1, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
318	        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.fst(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
319	        Clone.first_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
320	      Equal.trans(Array<U32>, r1, Pair.fst(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
321	        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.fst(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
322	        Clone.first_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))),
323	    both(l2, r2, A, I,
324	      Equal.trans(Array<F32>, l2, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
325	        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.snd(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
326	        Clone.second_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
327	      Equal.trans(Array<U32>, r2, Pair.snd(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
328	        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.snd(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
329	        Clone.second_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))))}
330	
331	def split_facts(+da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
332	  Generic.Fact<SplitFacts(A, I)>:
333	  Generic.Fact{{\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(A, I)> -> SplitFacts(A, I)}(
334	    halves_facts(da, A, di, I, Array.clone(F32, A), Array.clone(U32, I), {==}, {==}, valid, index_valid))}
335	
336	# Every slot of the forward build holds what its cell computes from (A, I).
337	# The Fact holds the cells eta-expanded, as slice_PROOF.bend's build_cells.
338	def build_cells(+depth: Nat, +splits: Nat, +plan: Gather.Plan, +cells: Nat, +base: Nat, +da: Nat, -A: Array<F32>, a: Array<F32>,
339	  -same: {a == A : Array<F32>}, -valid: Model.Balanced(F32, da, A), +di: Nat, -I: Array<U32>, index: Array<U32>,
340	  -same_index: {index == I : Array<U32>}, -index_valid: Model.Balanced(U32, di, I)) ->
341	  Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.cell, plan, (A, I), depth, cells, base, Gather.build(depth, splits, plan, cells, base, a, index))>:
342	  Generic.Fact{path =>
343	    {\{Generic.Fact: q => q} : Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.cell, plan, (A, I), depth, cells, base, Gather.build(depth, splits, plan, cells, base, a, index))> -> Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.cell, plan, (A, I), depth, cells, base, Gather.build(depth, splits, plan, cells, base, a, index))}(
344	      Generic.build_cells(~Gather.Plan, ~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.same, ~Gather.split, ~Gather.cell,
345	        plan, (A, I), depth, splits, cells, base, (a, index), both(a, index, A, I, same, same_index),
346	        at => inside => {\{Generic.Fact: q => q} :
347	          Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.cell(plan, at, (A, I), inside)) == (A, I) : Array<F32> & Array<U32>}> ->
348	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.cell(plan, at, (A, I), inside)) == (A, I) : Array<F32> & Array<U32>}}(
349	          cell_keeps(plan, at, da, A, di, I, inside, valid, index_valid)),
350	        Pair.fst({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>},
351	          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(A, I)> -> SplitFacts(A, I)}(split_facts(da, A, di, I, valid, index_valid))),
352	        Pair.snd({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((A, I))) == (A, I) : Array<F32> & Array<U32>},
353	          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(A, I)> -> SplitFacts(A, I)}(split_facts(da, A, di, I, valid, index_valid)))))(path)}
354	
355	# The arithmetic of the positions: output cell (o, k, r) reads the entry
356	# the laws name and the input cell (o, j, r).
357	def entry_same(+kind: Gather.Lookup, +count: Nat, +inner: Nat, +o: Nat, +k: Nat, +r: Nat) ->
358	  {Gather.entry_of(kind, count, inner, o, k, r) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}:
359	  match kind:
360	    case Gather.Selected{}:
361	      {==}
362	    case Gather.Gathered{}:
363	      {==}
364	
365	def entry_at(+kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +o: Nat, +k: Nat, +r: Nat,
366	  +k_below: {Nat.is_lt(k, count) == True{} : Bool}, +r_below: {Nat.is_lt(r, inner) == True{} : Bool}) ->
367	  {Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(count, inner, o, k, r)) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}:
368	  +row = Nat.add(Nat.mul(o, count), k)
369	  +pos = Laws.position(count, inner, o, k, r)
370	  %Equal.sym(Nat, Nat.div(pos, inner), row, BatchedProof.div_exact(row, inner, r, r_below)) :
371	    {Gather.entry_of(kind, count, inner, Nat.div(_, count), Nat.mod(_, count), Nat.mod(pos, inner)) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}
372	  %Equal.sym(Nat, Nat.mod(pos, inner), r, BatchedProof.mod_exact(row, inner, r, r_below)) :
373	    {Gather.entry_of(kind, count, inner, Nat.div(row, count), Nat.mod(row, count), _) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}
374	  %Equal.sym(Nat, Nat.div(row, count), o, BatchedProof.div_exact(o, count, k, k_below)) :
375	    {Gather.entry_of(kind, count, inner, _, Nat.mod(row, count), r) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}
376	  %Equal.sym(Nat, Nat.mod(row, count), k, BatchedProof.mod_exact(o, count, k, k_below)) :
377	    {Gather.entry_of(kind, count, inner, o, _, r) == Laws.entry_at(kind, count, inner, o, k, r) : Nat}
378	  entry_same(kind, count, inner, o, k, r)
379	
380	def source_at(+kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +o: Nat, +k: Nat, +r: Nat, +j: Nat,
381	  +k_below: {Nat.is_lt(k, count) == True{} : Bool}, +r_below: {Nat.is_lt(r, inner) == True{} : Bool}) ->
382	  {Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(count, inner, o, k, r), j) == Laws.position(rows, inner, o, j, r) : Nat}:
383	  +row = Nat.add(Nat.mul(o, count), k)
384	  +pos = Laws.position(count, inner, o, k, r)
385	  %Equal.sym(Nat, Nat.div(pos, inner), row, BatchedProof.div_exact(row, inner, r, r_below)) :
386	    {Gather.position(rows, inner, Nat.div(_, count), j, Nat.mod(pos, inner)) == Laws.position(rows, inner, o, j, r) : Nat}
387	  %Equal.sym(Nat, Nat.mod(pos, inner), r, BatchedProof.mod_exact(row, inner, r, r_below)) :
388	    {Gather.position(rows, inner, Nat.div(row, count), j, _) == Laws.position(rows, inner, o, j, r) : Nat}
389	  %Equal.sym(Nat, Nat.div(row, count), o, BatchedProof.div_exact(o, count, k, k_below)) :
390	    {Gather.position(rows, inner, _, j, r) == Laws.position(rows, inner, o, j, r) : Nat}
391	  {==}
392	
393	# The entry the cell reads, as the laws name it, rewritten to the code's.
394	def entry_read(+depth: Nat, +path: Model.Path(depth), +base: Nat, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
395	  +o: Nat, +k: Nat, +r: Nat, +k_below: {Nat.is_lt(k, count) == True{} : Bool}, +r_below: {Nat.is_lt(r, inner) == True{} : Bool},
396	  +at: {Nat.add(Model.offset(depth, path), base) == Laws.position(count, inner, o, k, r) : Nat}, +di: Nat, -I: Array<U32>, +j: U32,
397	  -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>}) ->
398	  Generic.Fact<{Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))) == Some{j} : Maybe<&2, U32>}>:
399	  Generic.Fact{Equal.trans(Maybe<&2, U32>, Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))),
400	    Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))), Some{j},
401	    Equal.cong(Nat, Maybe<&2, U32>, e => Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(e))), Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base)), Laws.entry_at(kind, count, inner, o, k, r),
402	      Equal.trans(Nat, Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base)), Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(count, inner, o, k, r)), Laws.entry_at(kind, count, inner, o, k, r),
403	        Equal.cong(Nat, Nat, x => Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, x), Nat.add(Model.offset(depth, path), base), Laws.position(count, inner, o, k, r), at),
404	        entry_at(kind, outer, rows, inner, count, o, k, r, k_below, r_below))),
405	    read)}
406	
407	def Laws.gather_build_cells(depth, splits, kind, outer, rows, inner, count, cells, base, da, A, a, same, valid, di, I, index, same_index,
408	  index_valid, path, o, k, r, k_below, r_below, at, in_count, j, read):
409	  Laws.Holds{
410	    Equal.trans(Maybe<&2, F32>,
411	      Model.observe(F32, depth, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index), path),
412	      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j))))),
413	      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Laws.position(rows, inner, o, U32.to_nat(j), r)))),
414	      Equal.trans(Maybe<&2, F32>,
415	        Model.observe(F32, depth, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index), path),
416	        Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), A, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))))},
417	        Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j))))),
418	        %in_count :
419	          {Model.observe(F32, depth, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index), path) ==
420	            Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.cell(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), (A, I), _))} : Maybe<&2, F32>}
421	        {\{Generic.Fact: q => q} : Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.cell, Gather.Plan{kind, outer, rows, inner, count}, (A, I), depth, cells, base, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index))> -> Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.cell, Gather.Plan{kind, outer, rows, inner, count}, (A, I), depth, cells, base, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index))}(
422	          build_cells(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, da, A, a, same, valid, di, I, index, same_index, index_valid))(path),
423	        {\{Generic.Fact: q => q} :
424	          Generic.Fact<{Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), A, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))))} ==
425	            Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j))))) : Maybe<&2, F32>}> ->
426	          {Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), A, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))))} ==
427	            Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j))))) : Maybe<&2, F32>}}(
428	          looked_value(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), da, A, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base)))), j,
429	            {\{Generic.Fact: q => q} : Generic.Fact<{Refinement.second(U32, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))) == j : U32}> -> {Refinement.second(U32, Array.get(U32, I, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))) == j : U32}}(
430	              read_entry(di, I, Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base)), j,
431	                {\{Generic.Fact: q => q} :
432	                  Generic.Fact<{Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))) == Some{j} : Maybe<&2, U32>}> ->
433	                  {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base))))) == Some{j} : Maybe<&2, U32>}}(
434	                  entry_read(depth, path, base, kind, outer, rows, inner, count, o, k, r, k_below, r_below, at, di, I, j, read)),
435	                index_valid)),
436	            valid))),
437	      Equal.cong(Nat, Maybe<&2, F32>, x => Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(x))),
438	        Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j)), Laws.position(rows, inner, o, U32.to_nat(j), r),
439	        Equal.trans(Nat, Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), U32.to_nat(j)), Gather.source(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(count, inner, o, k, r), U32.to_nat(j)), Laws.position(rows, inner, o, U32.to_nat(j), r),
440	          Equal.cong(Nat, Nat, x => Gather.source(Gather.Plan{kind, outer, rows, inner, count}, x, U32.to_nat(j)), Nat.add(Model.offset(depth, path), base), Laws.position(count, inner, o, k, r), at),
441	          source_at(kind, outer, rows, inner, count, o, k, r, U32.to_nat(j), k_below, r_below))))}
442	
443	# The cells of the backward build.
444	
445	# One gradient cell of the backward: it skips, or adds its word.
446	type Stepped<-dg: Nat, -G: Array<F32>, -di: Nat, -I: Array<U32>, -i: Nat, -at: Nat, -slot: Nat, -acc: F32, -result: F32 & (Array<F32> & Array<U32>)> is Data:
447	  Skipped{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
448	    -other: {Nat.is_eq(U32.to_nat(j), i) == False{} : Bool}, -kept: {result == (acc, (G, I)) : F32 & (Array<F32> & Array<U32>)}}
449	  Taken{-j: U32, -read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
450	    -same: {Nat.is_eq(U32.to_nat(j), i) == True{} : Bool}, -x: F32,
451	    -word: {Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(at))) == Some{x} : Maybe<&2, F32>},
452	    -kept: {result == (F32.add(acc, x), (G, I)) : F32 & (Array<F32> & Array<U32>)}}
453	
454	def accumulated(acc: F32, index: Array<U32>, pair: Array<F32> & F32) ->
455	  {Gather.accumulate(acc, index, pair) == (F32.add(acc, Refinement.second(F32, pair)), (Refinement.first(F32, pair), index)) : F32 & (Array<F32> & Array<U32>)}:
456	  (g, x) = pair
457	  {==}
458	
459	def triple(-acc: F32, -x: F32, -a: Array<F32>, -b: Array<U32>, -A: Array<F32>, -B: Array<U32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<U32>}) ->
460	  {(F32.add(acc, x), (a, b)) == (F32.add(acc, x), (A, B)) : F32 & (Array<F32> & Array<U32>)}:
461	  Equal.cong(Array<F32> & Array<U32>, F32 & (Array<F32> & Array<U32>), p => (F32.add(acc, x), p), (a, b), (A, B), both(a, b, A, B, ea, eb))
462	
463	def summed_is(+i: Nat, +at: Nat, +slot: Nat, +acc: F32, +dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, index: Array<U32>, +j: U32,
464	  -kept: {index == I : Array<U32>}, -seen: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) == Some{j} : Maybe<&2, U32>},
465	  hit: Bool, -told: {Nat.is_eq(U32.to_nat(j), i) == hit : Bool}, -valid: Model.Balanced(F32, dg, G)) ->
466	  Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.summed(hit, at, acc, G, index)>>:
467	  match hit:
468	    case False{}:
469	      Generic.Fact{Skipped{j, seen, told, Equal.cong(Array<U32>, F32 & (Array<F32> & Array<U32>), b => (acc, (G, b)), index, I, kept)}}
470	    case True{}:
471	      Generic.Fact{Taken{j, seen, told, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at))),
472	        Equal.sym(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))},
473	          Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(at))), Refinement.law_get_refines(F32, dg, G, U32.from_nat(at), valid)),
474	        Equal.trans(F32 & (Array<F32> & Array<U32>), Gather.accumulate(acc, index, Array.get(F32, G, U32.from_nat(at))),
475	          (F32.add(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))), (Refinement.first(F32, Array.get(F32, G, U32.from_nat(at))), index)),
476	          (F32.add(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at)))), (G, I)),
477	          accumulated(acc, index, Array.get(F32, G, U32.from_nat(at))),
478	          triple(acc, Refinement.second(F32, Array.get(F32, G, U32.from_nat(at))), Refinement.first(F32, Array.get(F32, G, U32.from_nat(at))), index, G, I,
479	            Refinement.law_get_retains(F32, dg, G, U32.from_nat(at), valid), kept))}}
480	
481	def compared_is(+i: Nat, +at: Nat, +slot: Nat, +acc: F32, +dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, pair: Array<U32> & U32,
482	  -kept: {Refinement.first(U32, pair) == I : Array<U32>},
483	  -seen: {Some{Refinement.second(U32, pair)} == Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))) : Maybe<&2, U32>},
484	  -valid: Model.Balanced(F32, dg, G)) ->
485	  Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.compared(i, at, acc, G, pair)>>:
486	  (index, +j) = pair
487	  summed_is(i, at, slot, acc, dg, G, di, I, index, j, kept,
488	    Equal.sym(Maybe<&2, U32>, Some{j}, Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(slot))), seen),
489	    Nat.is_eq(U32.to_nat(j), i), {==}, valid)
490	
491	def stepped_is(+i: Nat, +at: Nat, +slot: Nat, +acc: F32, +dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>,
492	  -valid: Model.Balanced(F32, dg, G), -index_valid: Model.Balanced(U32, di, I)) ->
493	  Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.stepped(i, at, slot, acc, (G, I))>>:
494	  Generic.Fact{{\{Generic.Fact: q => q} :
495	    Generic.Fact<Stepped<dg, G, di, I, i, at, slot, acc, Gather.compared(i, at, acc, G, Array.get(U32, I, U32.from_nat(slot)))>> ->
496	    Stepped<dg, G, di, I, i, at, slot, acc, Gather.compared(i, at, acc, G, Array.get(U32, I, U32.from_nat(slot)))>}(
497	    compared_is(i, at, slot, acc, dg, G, di, I, Array.get(U32, I, U32.from_nat(slot)),
498	      Refinement.law_get_retains(U32, di, I, U32.from_nat(slot), index_valid),
499	      Refinement.law_get_refines(U32, di, I, U32.from_nat(slot), index_valid), valid))}
500	
501	# The run of the backward from gradient cell k, for `left` more k: both
502	# arrays come back, and the sum is the one Added names.
503	def AddedIs(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
504	  +o: Nat, +i: Nat, +r: Nat, +left: Nat, +k: Nat, +acc: F32, -result: F32 & (Array<F32> & Array<U32>)) -> Type:
505	  {Pair.snd(F32, Array<F32> & Array<U32>, result) == (G, I) : Array<F32> & Array<U32>} &
506	    Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, left, k, acc, Pair.fst(F32, Array<F32> & Array<U32>, result))
507	
508	def StepIs(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
509	  +o: Nat, +i: Nat, +r: Nat, +rest: Nat, +k: Nat, +acc: F32, -result: F32 & (Array<F32> & Array<U32>)) -> Type:
510	  {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, result)) == (G, I) : Array<F32> & Array<U32>} &
511	    Laws.AddStep<dg, G, di, I, kind, count, inner, o, i, r, rest, k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, result))>
512	
513	def read_slot(+kind: Gather.Lookup, +count: Nat, +inner: Nat, +o: Nat, +k: Nat, +r: Nat, +di: Nat, -I: Array<U32>, +j: U32,
514	  read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry_of(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>}) ->
515	  {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>}:
516	  Equal.trans(Maybe<&2, U32>, Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))),
517	    Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry_of(kind, count, inner, o, k, r)))), Some{j},
518	    Equal.cong(Nat, Maybe<&2, U32>, e => Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(e))),
519	      Laws.entry_at(kind, count, inner, o, k, r), Gather.entry_of(kind, count, inner, o, k, r),
520	      Equal.sym(Nat, Gather.entry_of(kind, count, inner, o, k, r), Laws.entry_at(kind, count, inner, o, k, r), entry_same(kind, count, inner, o, k, r))),
521	    read)
522	
523	def step_added(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
524	  +o: Nat, +i: Nat, +r: Nat, +rest: Nat, +k: Nat, +acc: F32,
525	  ih: @+next: F32 -> Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, next,
526	    Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (next, (G, I))))>,
527	  -result: F32 & (Array<F32> & Array<U32>),
528	  st: Stepped<dg, G, di, I, i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, result>) ->
529	  Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, result)>:
530	  match st:
531	    case Skipped{j, read, other, kept}:
532	      Generic.Fact{
533	        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (acc, (G, I)), kept) :
534	          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
535	        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))}(
536	      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
537	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
538	          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q),
539	        Laws.Skips{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), other, Pair.snd(
540	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
541	          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, acc, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))), q)})}} :
542	        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (acc, (G, I))))> ->
543	        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (acc, (G, I)))>}(ih(acc)))}
544	    case Taken{j, read, same, x, word, kept}:
545	      Generic.Fact{
546	        %Equal.sym(F32 & (Array<F32> & Array<U32>), result, (F32.add(acc, x), (G, I)), kept) :
547	          StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, _)
548	        {\{Generic.Fact: q => q} : Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))> -> StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))}(
549	      {\{Generic.Fact: q => Generic.Fact{(Pair.fst(
550	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
551	          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
552	            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q),
553	        Laws.Adds{j, read_slot(kind, count, inner, o, k, r, di, I, j, read), same, x, word, Pair.snd(
554	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I)))) == (G, I) : Array<F32> & Array<U32>},
555	          Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, rest, 1n+k, F32.add(acc, x),
556	            Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))), q)})}} :
557	        Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, F32.add(acc, x),
558	          Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, rest, 1n+k, (F32.add(acc, x), (G, I))))> ->
559	        Generic.Fact<StepIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc, (F32.add(acc, x), (G, I)))>}(ih(F32.add(acc, x))))}
560	
561	def added_is(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat,
562	  +o: Nat, +i: Nat, +r: Nat, left: Nat, +k: Nat, +acc: F32, -valid: Model.Balanced(F32, dg, G), -index_valid: Model.Balanced(U32, di, I)) ->
563	  Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, left, k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, left, k, (acc, (G, I))))>:
564	  match left:
565	    case 0n:
566	      Generic.Fact{({==}, {==})}
567	    case 1n+rest:
568	      Generic.Fact{{\{Generic.Fact: q => q} : Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, 1n+rest, k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, 1n+rest, k, (acc, (G, I))))> -> AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, 1n+rest, k, acc, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, 1n+rest, k, (acc, (G, I))))}(
569	      step_added(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, k, acc,
570	        next => added_is(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, rest, 1n+k, next, valid, index_valid),
571	        Gather.stepped(i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, (G, I)),
572	        {\{Generic.Fact: q => q} :
573	          Generic.Fact<Stepped<dg, G, di, I, i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc,
574	            Gather.stepped(i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, (G, I))>> ->
575	          Stepped<dg, G, di, I, i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc,
576	            Gather.stepped(i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, (G, I))>}(
577	          stepped_is(i, Gather.cell_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), Gather.slot_at(Gather.Plan{kind, outer, rows, inner, count}, o, k, r), acc, dg, G, di, I, valid, index_valid))))}
578	
579	# A backward cell runs the sum from +0.0 over every k and hands both arrays
580	# back.
581	def scatter_keeps(+kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +at: Nat, +dg: Nat, -G: Array<F32>, +di: Nat,
582	  -I: Array<U32>, inside: Bool, -valid: Model.Balanced(F32, dg, G), -index_valid: Model.Balanced(U32, di, I)) ->
583	  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}>:
584	  match inside:
585	    case False{}:
586	      Generic.Fact{{==}}
587	    case True{}:
588	      Generic.Fact{Pair.fst({Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
589	        Laws.Added(dg, G, di, I, kind, count, inner, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))),
590	        {\{Generic.Fact: q => q} : Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))> -> AddedIs(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))}(
591	          added_is(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, valid, index_valid)))}
592	
593	def scatter_cells(+depth: Nat, +splits: Nat, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +cells: Nat, +base: Nat,
594	  +dg: Nat, -G: Array<F32>, g: Array<F32>, -same: {g == G : Array<F32>}, -valid: Model.Balanced(F32, dg, G), +di: Nat, -I: Array<U32>,
595	  index: Array<U32>, -same_index: {index == I : Array<U32>}, -index_valid: Model.Balanced(U32, di, I)) ->
596	  Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))>:
597	  Generic.Fact{path =>
598	    {\{Generic.Fact: q => q} : Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))> -> Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))}(
599	      Generic.build_cells(~Gather.Plan, ~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.same, ~Gather.split, ~Gather.scatter_cell,
600	        Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, splits, cells, base, (g, index), both(g, index, G, I, same, same_index),
601	        at => inside => {\{Generic.Fact: q => q} :
602	          Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}> ->
603	          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}}(
604	          scatter_keeps(kind, outer, rows, inner, count, at, dg, G, di, I, inside, valid, index_valid)),
605	        Pair.fst({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>},
606	          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(G, I)> -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid))),
607	        Pair.snd({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>},
608	          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(G, I)> -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid)))))(path)}
609	
610	# Input cell (o, i, r) runs the sum of (o, i, r).
611	def scattered_at(+kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +o: Nat, +i: Nat, +r: Nat,
612	  +i_below: {Nat.is_lt(i, rows) == True{} : Bool}, +r_below: {Nat.is_lt(r, inner) == True{} : Bool}, -state: Array<F32> & Array<U32>) ->
613	  {Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(rows, inner, o, i, r), state) == Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, state)) : F32 & (Array<F32> & Array<U32>)}:
614	  +row = Nat.add(Nat.mul(o, rows), i)
615	  +pos = Laws.position(rows, inner, o, i, r)
616	  %Equal.sym(Nat, Nat.div(pos, inner), row, BatchedProof.div_exact(row, inner, r, r_below)) :
617	    {Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(_, rows), Nat.mod(_, rows), Nat.mod(pos, inner), count, 0n, (0.0, state)) ==
618	      Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, state)) : F32 & (Array<F32> & Array<U32>)}
619	  %Equal.sym(Nat, Nat.mod(pos, inner), r, BatchedProof.mod_exact(row, inner, r, r_below)) :
620	    {Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(row, rows), Nat.mod(row, rows), _, count, 0n, (0.0, state)) ==
621	      Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, state)) : F32 & (Array<F32> & Array<U32>)}
622	  %Equal.sym(Nat, Nat.div(row, rows), o, BatchedProof.div_exact(o, rows, i, i_below)) :
623	    {Gather.added(Gather.Plan{kind, outer, rows, inner, count}, _, Nat.mod(row, rows), r, count, 0n, (0.0, state)) == Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, state)) : F32 & (Array<F32> & Array<U32>)}
624	  %Equal.sym(Nat, Nat.mod(row, rows), i, BatchedProof.mod_exact(o, rows, i, i_below)) :
625	    {Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, _, r, count, 0n, (0.0, state)) == Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, state)) : F32 & (Array<F32> & Array<U32>)}
626	  {==}
627	
628	def Laws.gather_scatter_cells(depth, splits, kind, outer, rows, inner, count, cells, base, dg, G, g, same, valid, di, I, index, same_index,
629	  index_valid, path, o, i, r, i_below, r_below, at, in_count):
630	  Laws.Summed{Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I)))),
631	    Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index), path),
632	      Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), (G, I)))},
633	      Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))))},
634	      %in_count :
635	        {Model.observe(F32, depth, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index), path) ==
636	          Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), (G, I), _))} : Maybe<&2, F32>}
637	      {\{Generic.Fact: q => q} : Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))> -> Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))}(
638	        scatter_cells(depth, splits, kind, outer, rows, inner, count, cells, base, dg, G, g, same, valid, di, I, index, same_index, index_valid))(path),
639	      Equal.cong(F32 & (Array<F32> & Array<U32>), Maybe<&2, F32>, p => Some{Pair.fst(F32, Array<F32> & Array<U32>, p)},
640	        Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), (G, I)), Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))),
641	        Equal.trans(F32 & (Array<F32> & Array<U32>), Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, Nat.add(Model.offset(depth, path), base), (G, I)), Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, Laws.position(rows, inner, o, i, r), (G, I)), Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))),
642	          Equal.cong(Nat, F32 & (Array<F32> & Array<U32>), x => Gather.scattered(Gather.Plan{kind, outer, rows, inner, count}, x, (G, I)), Nat.add(Model.offset(depth, path), base), Laws.position(rows, inner, o, i, r), at),
643	          scattered_at(kind, outer, rows, inner, count, o, i, r, i_below, r_below, (G, I))))),
644	    Pair.snd({Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
645	      Laws.Added(dg, G, di, I, kind, count, inner, o, i, r, count, 0n, 0.0, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))))),
646	      {\{Generic.Fact: q => q} : Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))))> -> AddedIs(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, o, i, r, count, 0n, (0.0, (G, I))))}(
647	        added_is(dg, G, di, I, kind, outer, rows, inner, count, o, i, r, count, 0n, 0.0, valid, index_valid)))}
648	
649	def index_same(+entries: List<&2, U32>, -dimensions: List<&2, U32>, built: Shape.ConstructResult<dimensions>) ->
650	  {Gather.built_index(entries, dimensions, built) == Laws.index_of(entries, dimensions, built) : Result<&2, &2, Gather.Error, Gather.Index>}:
651	  match built:
652	    case Shape.SError{error}:
653	      {==}
654	    case Shape.SBuilt{+shape, preserved}:
655	      {==}
656	
657	def Laws.gather_index_shaped(dimensions, entries):
658	  index_same(entries, dimensions, Shape.construct(dimensions))