src/autograd/reduce_PROOF.bend
bendtorch-core@0.1.0.0 · 680 lines · 46 definitions
1import Base
2
3import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
4
5import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
6
7import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
8
9import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
10
11import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
12
13import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
14
15import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
16
17import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
18
19import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
20
21import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
22
23import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
24
25import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
26
27import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
28
29import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
30
31import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
32
33import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
34
35import bendtorch-core@0.1.0.0/src/tensor/projection_PROOF.bend as ProjectionProof
36
37import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
38
39import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
40
41import bendtorch-core@0.1.0.0/src/tensor/construction_contract_PROOF.bend as ConstructionProof
42
43import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
44
45import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
46
47import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
48
49import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws
50
51import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
52
53import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
54
55import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
56
57import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
58
59import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
60
61import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
62
63import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel
64
65import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulProof
66
67type Holds<-P: Type> is Data:
68 Holds{-proof: P}
69
70def inspection_value(value: Totality.Inspection) -> Maybe<&2, F32>:
71 match value:
72 case Totality.Dims{dimensions}:
73 None{}
74 case Totality.Value{value}:
75 value
76
77def same_checked(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained), +index: U32) ->
78 Holds<{Core.checked_observe_dynamic(retained, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}>:
79 Holds{Equal.cong(Totality.Inspection, Maybe<&2, F32>, inspection_value,
80 Totality.inspect(Totality.Checked{index}, retained), Totality.inspect(Totality.Checked{index}, original), same(Totality.Checked{index}))}
81
82def same_dimensions(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained)) ->
83 Holds<{Totality.dimensions(retained) == Totality.dimensions(original) : List<&2, U32>}>:
84 Holds{Equal.cong(Totality.Inspection, List<&2, U32>, ElementwiseProof.inspection_dimensions,
85 Totality.inspect(Totality.Dimensions{}, retained), Totality.inspect(Totality.Dimensions{}, original), same(Totality.Dimensions{}))}
86
87def same_trans(-a: Core.Dynamic, -b: Core.Dynamic, -c: Core.Dynamic,
88 -ab: Totality.SameSource(a, b), -bc: Totality.SameSource(b, c)) -> Holds<Totality.SameSource(a, c)>:
89 Holds{property => Equal.trans(Totality.Inspection, Totality.inspect(property, c), Totality.inspect(property, b), Totality.inspect(property, a),
90 bc(property), ab(property))}
91
92def Inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, +cursor: Nat, output: Core.Tensor<target>) -> Type:
93 @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
94 {Core.checked_observe(target, output, index) == Laws.fiber(plan, values, index, cursor) : Maybe<&2, F32>}
95
96def update_written(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
97 meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
98 {Core.checked_observe(shape, output, index) == Some{value} : Maybe<&2, F32>}:
99 (checked, rest) = meaning
100 (observed, frame) = rest
101 observed
102
103def update_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
104 meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
105 @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
106 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
107 Core.ObservationChecked(Core.Packed{shape, output}, other) &
108 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}:
109 (checked, rest) = meaning
110 (observed, frame) = rest
111 frame
112
113def frame_equal(-shape: Shape.Shape, -output: Core.Tensor<shape>, -original: Core.Tensor<shape>, -other: U32,
114 pair: Core.ObservationChecked(Core.Packed{shape, output}, other) &
115 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
116 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}:
117 (checked, equal) = pair
118 equal
119
120def listed_kept(-original: Core.Dynamic, -retained: Core.Dynamic, +values: List<&2, F32>,
121 -same: Totality.SameSource(original, retained), -listed: Laws.Listed(original, values)) -> Holds<Laws.Listed(retained, values)>:
122 Holds{source => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(retained, source), Core.checked_observe_dynamic(original, source),
123 Laws.word_at(values, U32.to_nat(source)),
124 {\{Holds: proof => proof} : Holds<{Core.checked_observe_dynamic(retained, source) == Core.checked_observe_dynamic(original, source) : Maybe<&2, F32>}> ->
125 {Core.checked_observe_dynamic(retained, source) == Core.checked_observe_dynamic(original, source) : Maybe<&2, F32>}}(
126 same_checked(original, retained, same, source)),
127 listed(source))}
128
129def zero_inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, output: Core.Tensor<target>,
130 -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>}) ->
131 Holds<Inv(plan, values, target, 0n, output)>:
132 Holds{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(target, output, index),
133 Core.read_value(target, Core.read_flat(target, output, index)), Some{0.0},
134 Equal.sym(Maybe<&2, F32>, Core.read_value(target, Core.read_flat(target, output, index)), Core.checked_observe(target, output, index),
135 {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<target, output, index> ->
136 {Core.read_value(target, Core.read_flat(target, output, index)) == Core.checked_observe(target, output, index) : Maybe<&2, F32>}}(
137 Core.source_read_model(target, output, index))),
138 %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{output}, Core.new(target, 0.0), same) :
139 {Observation.point(target, index, _) == Some{0.0} : Maybe<&2, F32>}
140 ConstructionProof.point_value(target, 0.0, index, inside))}
141
142def mapping_values(-input: Core.Dynamic, -target: Shape.Shape, -plan: Shape.BroadcastPlan, -output: Core.Dynamic,
143 model: {Totality.dimensions(output) == Shape.dimensions(target) : List<&2, U32>} &
144 (@+values: List<&2, F32> -> @-listed: Laws.Listed(input, values) ->
145 @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
146 {Core.checked_observe_dynamic(output, index) == Laws.planned_fiber(values, index, Shape.logical_numel(Totality.dimensions(input)), Done{plan}) : Maybe<&2, F32>})) ->
147 @+values: List<&2, F32> -> @-listed: Laws.Listed(input, values) ->
148 @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
149 {Core.checked_observe_dynamic(output, index) == Laws.planned_fiber(values, index, Shape.logical_numel(Totality.dimensions(input)), Done{plan}) : Maybe<&2, F32>}:
150 (dimensions, mapped) = model
151 mapped
152
153def output_count(+shape: Shape.Shape, +plan: Shape.BroadcastPlan,
154 -equal: {True{} == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool}) ->
155 Holds<{Shape.elements(Shape.output_shape(plan)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
156 Holds{Equal.trans(Nat, Shape.elements(Shape.output_shape(plan)), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))),
157 Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(Shape.output_shape(plan)),
158 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape),
159 TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape), equal)))}
160
161def rank_of(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n):
162 match shape:
163 case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
164 rank_bound
165
166def capacity_of(+shape: Shape.Shape) -> Shape.LE(Shape.logical_numel(Shape.dimensions(shape)), 1048576n):
167 match shape:
168 case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
169 capacity_bound
170
171
172
173
174def indexed_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
175 +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
176 -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
177 map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
178 Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
179 match map:
180 case Shape.Unindexed{zero}:
181 Laws.Retained{property => {==}}
182 case Shape.Indexed{rows, same}:
183 MatmulProof.take_lift(shape, tensor,
184 pair => Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
185 kept => copy => taken => Laws.Retained{{\{Parallel.Taken: depth => balanced => reads => retained => retained} :
186 Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, copy)> -> Totality.SameSource(Core.Packed{shape, tensor}, Core.Packed{shape, kept})}(taken)})
187
188def parallel_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
189 result: Result<&2, &1, Core.Error, Core.Tensor<target>>) ->
190 Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result)>:
191 match result:
192 case Fail{error}:
193 Laws.Retained{property => {==}}
194 case Done{Core.TTensor{storage, exact}}:
195 match storage:
196 case Storage.Empty{}:
197 Laws.Retained{property => {==}}
198 case Storage.Owned{+depth, +length, array, balanced, valid}:
199 indexed_retains(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
200 valid, exact, Shape.index_map(plan))
201
202def fitted_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool) ->
203 Laws.Retained<Core.Packed{shape, tensor}, Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same)>:
204 match same:
205 case False{}:
206 Laws.Retained{property => {==}}
207 case True{}:
208 parallel_retains(shape, tensor, target, plan, Core.new(target, 0.0))
209
210def planned_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
211 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>) ->
212 Laws.Retained<Core.Packed{shape, tensor}, Reduce.planned(shape, tensor, target, result)>:
213 match result:
214 case Fail{error}:
215 Laws.Retained{property => {==}}
216 case Done{+plan}:
217 fitted_retains(shape, tensor, target, plan,
218 Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)))
219
220def Laws.reduce_retains_input(input, target):
221 Core.Packed{+shape, tensor} = input
222 planned_retains(shape, tensor, target, Shape.broadcast_checked(target, shape))
223
224
225
226
227def parallel_build(+plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat, +rows: List<&2, Shape.Row>, array: Array<F32>) -> Array<F32>:
228 Reduce.build(depth, Reduce.splits(plan, depth, length), rows, Shape.extents(Shape.output_shape(plan)), length, 0n, array)
229
230def rows_cell(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
231 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
232 +rows: List<&2, Shape.Row>,
233 +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
234 -array: Array<F32>, +d: Nat, -balanced: Model.Balanced(F32, d, array), -reads: Parallel.SourceReads(Core.Packed{shape, tensor}, d, array),
235 +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
236 +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
237 +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
238 +values: List<&2, F32>, -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +index: U32,
239 +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
240 Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
241 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}>:
242 +t = U32.to_nat(index)
243 +extents = Shape.extents(Shape.output_shape(plan))
244 +splits = Reduce.splits(plan, depth, length)
245 -built = parallel_build(plan, depth, length, rows, array)
246 -inside_length : {Nat.is_lt(t, length) == True{} : Bool} =
247 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(target)), exact) : {Nat.is_lt(t, _) == True{} : Bool}
248 inside
249 +path = Refinement.route(depth, index)
250 Holds{{\{ReduceParallel.CellAt: word => observed => words => seen => total =>
251 Equal.trans(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)),
252 Model.observe(F32, depth, built, path), Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))),
253 Parallel.observe_allowed_equal(depth, length, built, index, Nat.is_lt(t, length), inside_length,
254 Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), Route.index_complete(depth, length, index, valid, inside_length))),
255 %Equal.sym(Maybe<&2, F32>, Model.observe(F32, depth, built, path), Some{word}, observed) :
256 {_ == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
257 %Equal.sym(F32, word, ReduceParallel.fsum(words, 0.0), total) :
258 {Some{_} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
259 %count : {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, _) : Maybe<&2, F32>}
260 {\{Parallel.Fact: p => p} :
261 Parallel.Fact<{Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}> ->
262 {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}}(
263 ReduceParallel.cell_value(plan, rows, rows_exact, values, index, d, array, words, seen,
264 %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(target), left) :
265 {Nat.is_lt(t, Shape.logical_numel(_)) == True{} : Bool}
266 inside,
267 position => below =>
268 +shaped : {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool} =
269 %right : {Nat.is_lt(position, Shape.logical_numel(_)) == True{} : Bool}
270 below
271 +exact_word = MatrixIndex.word_exact(position, shape, shaped)
272 Equal.trans(Maybe<&2, F32>, Model.observe(F32, d, array, Refinement.route(d, U32.from_nat(position))),
273 Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)), Laws.word_at(values, position),
274 reads(U32.from_nat(position))(
275 %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, exact_word) :
276 {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
277 shaped),
278 %exact_word :
279 {Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)) == Laws.word_at(values, _) : Maybe<&2, F32>}
280 listed(U32.from_nat(position))))))} :
281 ReduceParallel.CellAt<d, array, rows, extents, t, Model.observe(F32, depth, built, path)> ->
282 {Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)) ==
283 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
284 %inside_length : ReduceParallel.CellSpec(d, array, rows, extents, t, _, Model.observe(F32, depth, built, path))
285 %Parallel.output_position(depth, length, index, valid, inside_length) :
286 ReduceParallel.CellIs(d, array, rows, extents, length, _, Model.observe(F32, depth, built, path))
287 {\{Parallel.Fact: p => p} :
288 Parallel.Fact<ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)> -> ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)}(
289 ReduceParallel.build_cells(depth, splits, d, array, rows, extents, length, 0n, array, {==}, balanced))(path))}
290
291def rows_mapping(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
292 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
293 -kept: Core.Tensor<shape>, -array: Array<F32>, -taken: Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)>,
294 +rows: List<&2, Shape.Row>,
295 +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
296 +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
297 +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
298 +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
299 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
300 Reduce.parallel_rows(plan, target, depth, length, valid, exact, (Core.Packed{shape, kept}, array), rows))>:
301 Holds{({==}, values => listed => index => inside =>
302 {\{Parallel.Taken: d => balanced => reads => retained =>
303 {\{Holds: proof => proof} :
304 Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
305 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}> ->
306 {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
307 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
308 rows_cell(shape, tensor, target, plan, depth, length, valid, exact, rows, rows_exact, array, d, balanced, reads, left, right, count,
309 values, listed, index, inside))} :
310 Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)> ->
311 {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
312 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(taken))}
313
314def indexed_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
315 +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
316 -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
317 map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
318 -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>},
319 +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
320 +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
321 +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
322 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
323 Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map))>:
324 match map:
325 case Shape.Unindexed{zero}:
326 Holds{({==}, values => listed => index => inside =>
327 %Equal.trans(Nat, 0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(shape)), zero, count) :
328 {Core.checked_observe(target, output, index) == Laws.fiber(plan, values, index, _) : Maybe<&2, F32>}
329 {\{Holds: proof => proof} : Holds<Inv(plan, values, target, 0n, output)> -> Inv(plan, values, target, 0n, output)}(
330 zero_inv(plan, values, target, output, same))(index)(inside))}
331 case Shape.Indexed{rows, same_rows}:
332 MatmulProof.take_lift(shape, tensor,
333 pair => Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows))>,
334 kept => copy => taken => rows_mapping(shape, tensor, target, plan, depth, length, valid, exact, kept, copy,
335 taken, rows, same_rows, left, right, count))
336
337def parallel_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
338 result: Result<&2, &1, Core.Error, Core.Tensor<target>>,
339 -same: {result == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>},
340 +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
341 +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
342 +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
343 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result))>:
344 match result:
345 case Fail{error}:
346 Holds{Unit{}}
347 case Done{Core.TTensor{storage, exact}}:
348 match storage:
349 case Storage.Empty{}:
350 Holds{({==}, values => listed => index => inside =>
351 Empty.absurd({Core.checked_observe(target, Core.TTensor{Storage.Empty{}, exact}, index) ==
352 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>},
353 Arith.lt_zero(U32.to_nat(index),
354 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(target)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
355 inside)))}
356 case Storage.Owned{+depth, +length, array, balanced, valid}:
357 indexed_mapping(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
358 valid, exact, Shape.index_map(plan), same, left, right, count)
359
360def output_numel(+shape: Shape.Shape, +plan: Shape.BroadcastPlan,
361 -equal: {True{} == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool}) ->
362 Holds<{Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
363 Holds{Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape),
364 TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape), equal))}
365
366def fitted_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
367 -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool},
368 -left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
369 -right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
370 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same))>:
371 match same:
372 case False{}:
373 Holds{Unit{}}
374 case True{}:
375 Holds{{\{Holds: proof => proof} :
376 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, Core.new(target, 0.0)))> ->
377 Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, Core.new(target, 0.0)))}(
378 parallel_mapping(shape, tensor, target, plan, Core.new(target, 0.0), {==}, left, right,
379 {\{Holds: proof => proof} :
380 Holds<{Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}> ->
381 {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}(
382 output_numel(shape, plan, decided))))}
383
384def planned_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
385 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
386 -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>}) ->
387 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, result, Reduce.planned(shape, tensor, target, result))>:
388 match result:
389 case Fail{error}:
390 Holds{Unit{}}
391 case Done{+plan}:
392 fitted_mapping(shape, tensor, target, plan, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==},
393 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
394 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources),
395 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
396 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources))
397
398def Laws.reduce_mapping(input, target):
399 Core.Packed{+shape, tensor} = input
400 Laws.MappingModel{
401 {\{Holds: proof => proof} :
402 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Shape.broadcast_checked(target, shape),
403 Reduce.planned(shape, tensor, target, Shape.broadcast_checked(target, shape)))> ->
404 Laws.Mapping(Core.Packed{shape, tensor}, target, Reduce.reduce_to(Core.Packed{shape, tensor}, target))}(
405 planned_mapping(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape)))}
406
407
408
409def indexed_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
410 +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
411 -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
412 map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
413 Laws.Success<Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
414 match map:
415 case Shape.Unindexed{zero}:
416 Laws.Success{{==}}
417 case Shape.Indexed{rows, same}:
418 MatmulProof.take_lift(shape, tensor, pair => Laws.Success<Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
419 kept => copy => taken => Laws.Success{{==}})
420
421def parallel_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
422 result: Result<&2, &1, Core.Error, Core.Tensor<target>>, -done: Allocation.TensorDone<target, result>) ->
423 Laws.Success<Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result)>:
424 match result:
425 case Fail{error}:
426 Laws.Success{Empty.absurd({False{} == True{} : Bool},
427 {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<target>>, Bool,
428 found => Result.is_done(&2, &1, Core.Error, Core.Tensor<target>, found), Fail{error}, Done{tensor},
429 Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{tensor}, Fail{error}, same)))} :
430 Allocation.TensorDone<target, Fail{error}> -> Empty}(done))}
431 case Done{Core.TTensor{storage, exact}}:
432 match storage:
433 case Storage.Empty{}:
434 Laws.Success{{==}}
435 case Storage.Owned{+depth, +length, array, balanced, valid}:
436 indexed_success(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
437 valid, exact, Shape.index_map(plan))
438
439def fitted_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
440 -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool},
441 -truth: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
442 Laws.Success<Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same)>:
443 match same:
444 case False{}:
445 Laws.Success{Empty.absurd({False{} == True{} : Bool},
446 Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), True{}, decided,
447 %truth : {Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), _) == True{} : Bool}
448 TransformProof.words_same_refl(Shape.dimensions(Shape.output_shape(plan))))))}
449 case True{}:
450 parallel_success(shape, tensor, target, plan, Core.new(target, 0.0), AllocationProof.core_new_done(target, 0.0))
451
452def planned_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
453 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
454 -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
455 -built: {ShapeLaws.broadcast_built(result) == True{} : Bool},
456 -alignment: Shape.Broadcast<Shape.extents(target), Shape.extents(shape), Shape.extents(shape)>) ->
457 Laws.Success<Reduce.planned(shape, tensor, target, result)>:
458 match result:
459 case Fail{error}:
460 Laws.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(built))}
461 case Done{+plan}:
462 fitted_success(shape, tensor, target, plan,
463 Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==},
464 ElementwiseProof.planned_output_dimensions(target, shape, plan, Shape.dimensions(shape), alignment, sources))
465
466def Laws.reduce_valid_success(input, target, alignment):
467 Core.Packed{+shape, tensor} = input
468 planned_success(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape),
469 PlanProof.broadcast_checked_complete(target, shape, Shape.dimensions(shape), alignment, rank_of(shape), capacity_of(shape)), alignment)
470
471def empty_fiber(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +index: U32, +count: Nat,
472 -empty: {count == 0n : Nat}) -> Holds<{Laws.fiber(plan, values, index, count) == Some{0.0} : Maybe<&2, F32>}>:
473 Holds{
474 %Equal.sym(Nat, count, 0n, empty) : {Laws.fiber(plan, values, index, _) == Some{0.0} : Maybe<&2, F32>}
475 {==}}
476
477def below_zero(+number: Nat) -> Holds<{Nat.is_lt(number, 0n) == False{} : Bool}>:
478 match number:
479 case 0n:
480 Holds{{==}}
481 case 1n+rest:
482 Holds{{==}}
483
484def empty_unlisted(+depth: Nat, +length: Nat, -array: Array<F32>, +source: U32,
485 -empty: {length == 0n : Nat}) -> Holds<{Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}>:
486 Holds{
487 %Equal.sym(Nat, length, 0n, empty) :
488 {Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), _)) == None{} : Maybe<&2, F32>}
489 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(source), 0n), False{},
490 {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(source), 0n) == False{} : Bool}> -> {Nat.is_lt(U32.to_nat(source), 0n) == False{} : Bool}}(
491 below_zero(U32.to_nat(source)))) :
492 {Lifecycle.observe_allowed(depth, length, array, source, _) == None{} : Maybe<&2, F32>}
493 {==}}
494
495def listed_empty(input: Core.Dynamic, -empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}) -> Holds<Laws.Listed(input, Nil{})>:
496 Core.Packed{+shape, Core.TTensor{storage, exact}} = input
497 match storage:
498 case Storage.Empty{}:
499 Holds{source => {==}}
500 case Storage.Owned{+depth, +length, array, balanced, valid}:
501 Holds{source => {\{Holds: proof => proof} :
502 Holds<{Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}> ->
503 {Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}}(
504 empty_unlisted(depth, length, array, source, Equal.trans(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), 0n, exact, empty)))}
505
506def below_self(+number: Nat) -> {Nat.is_lt(number, number) == False{} : Bool}:
507 match number:
508 case 0n:
509 {==}
510 case 1n+rest:
511 below_self(rest)
512
513def neither_below(+left: Nat, +right: Nat, first: {Nat.is_lt(left, right) == False{} : Bool},
514 second: {Nat.is_lt(right, left) == False{} : Bool}) -> {left == right : Nat}:
515 match left right:
516 case 0n 0n:
517 {==}
518 case 0n 1n+r:
519 Empty.absurd({0n == 1n+r : Nat}, Arith.clash_true(first))
520 case 1n+l 0n:
521 Empty.absurd({1n+l == 0n : Nat}, Arith.clash_true(second))
522 case 1n+l 1n+r:
523 Equal.cong(Nat, Nat, n => 1n+n, l, r, neither_below(l, r, first, second))
524
525def word_presence(+values: List<&2, F32>, +position: Nat) ->
526 {Nat.is_lt(position, List.length(&2, F32, values)) == TransformProof.maybe_present(Laws.word_at(values, position)) : Bool}:
527 match values position:
528 case Nil{} 0n:
529 {==}
530 case Nil{} 1n+next:
531 {==}
532 case value <> rest 0n:
533 {==}
534 case value <> rest 1n+next:
535 word_presence(rest, next)
536
537def absent_observation(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +source: U32,
538 -outside: {Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
539 Holds<{Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}>:
540 Core.TTensor{storage, exact} = tensor
541 match storage:
542 case Storage.Empty{}:
543 Holds{{==}}
544 case Storage.Owned{+depth, +length, array, balanced, valid}:
545 Holds{
546 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(source), length), False{},
547 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(source), _) == False{} : Bool}
548 outside) : {Lifecycle.observe_allowed(depth, length, array, source, _) == None{} : Maybe<&2, F32>}
549 {==}}
550
551def observed_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +source: U32, +inside: Bool,
552 -decision: {inside == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) ->
553 Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == inside : Bool}>:
554 match inside:
555 case False{}:
556 Holds{Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), None{},
557 {\{Holds: proof => proof} : Holds<{Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}> -> {Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}}(
558 absent_observation(shape, tensor, source, Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision))))}
559 case True{}:
560 Holds{{\{TransformProof.PresentObservation: value => equal =>
561 Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), Some{value}, equal)} :
562 TransformProof.PresentObservation<shape, tensor, source> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == True{} : Bool}}(
563 TransformProof.present_observation(shape, tensor, source, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision)))}
564
565def same_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
566 -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +source: U32) ->
567 Holds<{Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
568 Holds{Equal.trans(Bool, Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)), TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
569 Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
570 word_presence(values, U32.to_nat(source)),
571 Equal.trans(Bool, TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
572 TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)), Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
573 Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Laws.word_at(values, U32.to_nat(source)),
574 Core.checked_observe(shape, tensor, source),
575 Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, source), Laws.word_at(values, U32.to_nat(source)), listed(source))),
576 {\{Holds: proof => proof} : Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
577 observed_presence(shape, tensor, source, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), {==}))))}
578
579def natural_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
580 -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +position: Nat, -within: Shape.LE(position, 1048576n)) ->
581 Holds<{Nat.is_lt(position, List.length(&2, F32, values)) == Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
582 Holds{
583 %Conversion.capacity_natural_word_exact(position, within) : {Nat.is_lt(_, List.length(&2, F32, values)) == Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) : Bool}
584 {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
585 same_presence(shape, tensor, values, listed, U32.from_nat(position)))}
586
587def length_decided(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
588 -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +below: Bool,
589 -decision: {below == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) -> Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
590 match below:
591 case True{}:
592 Holds{Empty.absurd({List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, Arith.clash(
593 Equal.trans(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), True{},
594 Equal.sym(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), False{}, below_self(List.length(&2, F32, values))),
595 Equal.trans(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), True{},
596 {\{Holds: proof => proof} : Holds<{Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
597 natural_presence(shape, tensor, values, listed, List.length(&2, F32, values),
598 Shape.LE.from(List.length(&2, F32, values), 1048576n, Equal.sym(Bool, Nat.is_le(List.length(&2, F32, values), 1048576n), True{},
599 Conversion.le_trans(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), 1048576n,
600 Conversion.lt_le(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)),
601 Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), 1048576n), Nats.le_true(Shape.logical_numel(Shape.dimensions(shape)), 1048576n, capacity_of(shape)))))))),
602 Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)))))}
603 case False{}:
604 Holds{neither_below(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision),
605 Equal.trans(Bool, Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)), Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))), False{},
606 {\{Holds: proof => proof} : Holds<{Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
607 natural_presence(shape, tensor, values, listed, Shape.logical_numel(Shape.dimensions(shape)), capacity_of(shape))),
608 below_self(Shape.logical_numel(Shape.dimensions(shape)))))}
609
610def Laws.listed_length(input, values, listed):
611 Core.Packed{+shape, tensor} = input
612 Laws.Length{{\{Holds: proof => proof} : Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}> -> {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}(
613 length_decided(shape, tensor, values, listed, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), {==}))}
614
615def zeros_from_mapping(-input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
616 pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>,
617 -mapping: Laws.MappingWith(input, target, Done{plan}, pair),
618 -listed: Laws.Listed(input, Nil{}),
619 -empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}) -> Laws.Zeros<target, pair>:
620 (owner, outcome) = pair
621 match outcome:
622 case Fail{error}:
623 Laws.Zeros{Unit{}}
624 case Done{output}:
625 Laws.Zeros{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(output, index),
626 Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))), Some{0.0},
627 mapping_values(input, target, plan, output, mapping)(Nil{})(listed)(index)(inside),
628 {\{Holds: proof => proof} : Holds<{Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}> ->
629 {Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}}(
630 empty_fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input)), empty)))}
631
632def planned_zeros(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
633 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
634 -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
635 -empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}) ->
636 Laws.Zeros<target, Reduce.planned(shape, tensor, target, result)>:
637 match result:
638 case Fail{error}:
639 Laws.Zeros{Unit{}}
640 case Done{+plan}:
641 zeros_from_mapping(Core.Packed{shape, tensor}, target, plan, Reduce.planned(shape, tensor, target, Done{plan}),
642 {\{Holds: proof => proof} :
643 Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))> ->
644 Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))}(
645 planned_mapping(shape, tensor, target, Done{plan}, sources)),
646 {\{Holds: proof => proof} : Holds<Laws.Listed(Core.Packed{shape, tensor}, Nil{})> -> Laws.Listed(Core.Packed{shape, tensor}, Nil{})}(
647 listed_empty(Core.Packed{shape, tensor}, empty)),
648 empty)
649
650def Laws.reduce_empty_zeros(input, target, empty):
651 Core.Packed{+shape, tensor} = input
652 planned_zeros(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape), empty)
653
654def Laws.reduce_shape_error(input, target, error, rejected):
655 Core.Packed{+shape, tensor} = input
656 %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(target, shape), Fail{error}, rejected) :
657 {Reduce.planned(shape, tensor, target, _) == (Core.Packed{shape, tensor}, Fail{Reduce.TensorError{Core.ShapeError{error}}}) :
658 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}
659 {==}
660
661def fitted_not_reducible(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +dims: List<&2, U32>, flag: Bool,
662 decided: {flag == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), dims) : Bool},
663 differ: {Shape.dimensions(Shape.output_shape(plan)) != dims : List<&2, U32>}) ->
664 {Reduce.fitted(input, target, plan, flag) == (input, Fail{Reduce.NotReducible{}}) :
665 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}:
666 match flag:
667 case False{}:
668 {==}
669 case True{}:
670 Empty.absurd({Reduce.fitted(input, target, plan, True{}) == (input, Fail{Reduce.NotReducible{}}) :
671 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>},
672 differ(TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), dims, decided)))
673
674def Laws.reduce_not_reducible(input, target, plan, planned, differ):
675 Core.Packed{+shape, tensor} = input
676 %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(target, shape), Done{plan}, planned) :
677 {Reduce.planned(shape, tensor, target, _) == (Core.Packed{shape, tensor}, Fail{Reduce.NotReducible{}}) :
678 Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}
679 fitted_not_reducible(Core.Packed{shape, tensor}, target, plan, Shape.dimensions(shape),
680 Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==}, differ)