src/tensor/gather_PROOF.bend
bendtorch-core@0.1.0.0 · 658 lines · 41 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
6import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
7import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
8import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
9import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
10import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws
11import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
12import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as Plans
13import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
14import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedProof
15
16
17
18def 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
25def 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
33def 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
45def 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
58def 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
63def 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
72def 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
87def 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
92def 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
98def 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
107def 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
120def 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
129def 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
134def 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
140def 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
149def 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
161def 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
176def 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
194def 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
218def 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
224def 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
231
232def 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
238def 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
243def 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
248def 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
255def 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
265def 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
279def 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
297def 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
306def 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
309def 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
331def 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
337
338def 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
356
357def 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
365def 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
380def 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
394def 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
407def 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
444
445
446type 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
454def 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
459def 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
463def 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
481def 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
491def 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
502
503def 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
508def 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
513def 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
523def 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
561def 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
580
581def 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
593def 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
611def 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
628def 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
649def 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
657def Laws.gather_index_shaped(dimensions, entries):
658 index_same(entries, dimensions, Shape.construct(dimensions))