src/tensor/elementwise_PROOF.bend
bendtorch-core@0.1.0.0 · 896 lines · 76 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/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
5import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
6import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
7import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
8import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
9import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
10import bendtorch-core@0.1.0.0/src/tensor/elementwise_LAWS.bend as Laws
11import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
12import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
13import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
14import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique
15import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
16import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
17import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
18import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
19import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
20import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
21import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
22import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
23import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
24
25def read_owner(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> Storage.Storage:
26 (owner, result) = pair
27 owner
28
29def storage_inspect(property: Totality.Property, storage: Storage.Storage) -> Totality.Inspection:
30 match property:
31 case Totality.Dimensions{}:
32 Totality.Dims{Nil{}}
33 case Totality.Checked{index}:
34 Totality.Value{Lifecycle.checked_observe(storage, index)}
35 case Totality.Raw{index}:
36 Totality.Value{Lifecycle.observe(storage, index)}
37
38def finish_read_inspect(+depth: Nat, +length: Nat, -original: Array<F32>, +index: U32, +property: Totality.Property,
39 pair: Array<F32> & F32, -same: {pair == Array.get(F32, original, index) : Array<F32> & F32},
40 -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
41 {storage_inspect(property, read_owner(Storage.finish_read(depth, length, original, index, pair, same, balanced, valid))) ==
42 storage_inspect(property, Storage.Owned{depth, length, Refinement.first(F32, pair),
43 Certificates.get_result(F32, depth, original, index, pair, same, balanced), valid}) : Totality.Inspection}:
44 (array, value) = pair
45 {==}
46
47def array_inspect(+depth: Nat, +length: Nat, property: Totality.Property, array: Array<F32>) -> Totality.Inspection:
48 match property:
49 case Totality.Dimensions{}:
50 Totality.Dims{Nil{}}
51 case Totality.Checked{index}:
52 Totality.Value{Lifecycle.checked_observe_array(depth, length, array, index)}
53 case Totality.Raw{index}:
54 Totality.Value{Model.observe(F32, depth, array, Refinement.route(depth, index))}
55
56type InspectionModel<-left: Totality.Inspection, -right: Totality.Inspection> is Data:
57 InspectionModel{-equal: {left == right : Totality.Inspection}}
58
59def read_hit_inspect(+depth: Nat, +length: Nat, +index: U32, +property: Totality.Property, array: Array<F32>,
60 balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
61 InspectionModel<storage_inspect(property, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
62 array_inspect(depth, length, property, array)>:
63 match property:
64 case Totality.Dimensions{}:
65 InspectionModel{finish_read_inspect(depth, length, array, index, Totality.Dimensions{}, Array.get(F32, array, index), {==}, balanced, valid)}
66 case Totality.Checked{+other}:
67 InspectionModel{Equal.trans(Totality.Inspection,
68 storage_inspect(Totality.Checked{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
69 array_inspect(depth, length, Totality.Checked{other}, Refinement.first(F32, Array.get(F32, array, index))),
70 array_inspect(depth, length, Totality.Checked{other}, array),
71 finish_read_inspect(depth, length, array, index, Totality.Checked{other}, Array.get(F32, array, index), {==}, balanced, valid),
72 Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Checked{other}, a),
73 Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
74 case Totality.Raw{+other}:
75 InspectionModel{Equal.trans(Totality.Inspection,
76 storage_inspect(Totality.Raw{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
77 array_inspect(depth, length, Totality.Raw{other}, Refinement.first(F32, Array.get(F32, array, index))),
78 array_inspect(depth, length, Totality.Raw{other}, array),
79 finish_read_inspect(depth, length, array, index, Totality.Raw{other}, Array.get(F32, array, index), {==}, balanced, valid),
80 Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Raw{other}, a),
81 Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
82
83def read_checked_inspect(+depth: Nat, +length: Nat, +index: U32, allowed: Bool, +property: Totality.Property, array: Array<F32>,
84 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
85 balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
86 InspectionModel<storage_inspect(property, read_owner(Storage.get_checked(depth, length, array, index, allowed, decision, balanced, valid))),
87 array_inspect(depth, length, property, array)>:
88 match allowed:
89 case False{}:
90 match property:
91 case Totality.Dimensions{}:
92 InspectionModel{{==}}
93 case Totality.Checked{other}:
94 InspectionModel{{==}}
95 case Totality.Raw{other}:
96 InspectionModel{{==}}
97 case True{}:
98 read_hit_inspect(depth, length, index, property, array, balanced, valid)
99
100def tensor_read_owner(-shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) -> Core.Tensor<shape>:
101 (owner, result) = pair
102 owner
103
104def storage_tensor_inspect(shape: Shape.Shape, property: Totality.Property, storage: Storage.Storage) -> Totality.Inspection:
105 match property:
106 case Totality.Dimensions{}:
107 Totality.Dims{Shape.dimensions(shape)}
108 case Totality.Checked{index}:
109 Totality.Value{Lifecycle.checked_observe(storage, index)}
110 case Totality.Raw{index}:
111 Totality.Value{Lifecycle.observe(storage, index)}
112
113def core_read_projection(+shape: Shape.Shape, -original: Storage.Storage,
114 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
115 +property: Totality.Property, pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
116 -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
117 {Totality.inspect(property, Core.Packed{shape, tensor_read_owner(shape, Core.read_result(shape, original, valid, index, pair, same))}) ==
118 storage_tensor_inspect(shape, property, read_owner(pair)) : Totality.Inspection}:
119 match property:
120 case Totality.Dimensions{}:
121 (storage, result) = pair
122 {==}
123 case Totality.Checked{other}:
124 (storage, result) = pair
125 {==}
126 case Totality.Raw{other}:
127 (storage, result) = pair
128 {==}
129
130type SourceModel<-original: Core.Dynamic, -retained: Core.Dynamic> is Data:
131 SourceModel{-same: Totality.SameSource(original, retained)}
132
133def dynamic_read_owner(pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>) -> Core.Dynamic:
134 (owner, result) = pair
135 owner
136
137def tensor_read_dimensions(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
138 {Totality.inspect(Totality.Dimensions{}, Core.Packed{shape, tensor_read_owner(shape, pair)}) == Totality.Dims{Shape.dimensions(shape)} : Totality.Inspection}:
139 (owner, result) = pair
140 {==}
141
142def dynamic_read_projection(+shape: Shape.Shape, +property: Totality.Property,
143 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
144 {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic_result(shape, pair))) ==
145 Totality.inspect(property, Core.Packed{shape, tensor_read_owner(shape, pair)}) : Totality.Inspection}:
146 (owner, result) = pair
147 {==}
148
149def owned_read_property(+shape: Shape.Shape, +depth: Nat, +length: Nat, +index: U32, property: Totality.Property,
150 -array: Array<F32>, -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
151 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
152 InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
153 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}})>:
154 match property:
155 case Totality.Dimensions{}:
156 InspectionModel{Equal.trans(Totality.Inspection,
157 Totality.inspect(Totality.Dimensions{}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
158 Totality.inspect(Totality.Dimensions{}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
159 Totality.Dims{Shape.dimensions(shape)},
160 dynamic_read_projection(shape, Totality.Dimensions{}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
161 tensor_read_dimensions(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)))}
162 case Totality.Checked{+other}:
163 InspectionModel{Equal.trans(Totality.Inspection,
164 Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
165 storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
166 array_inspect(depth, length, Totality.Checked{other}, array),
167 Equal.trans(Totality.Inspection,
168 Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
169 Totality.inspect(Totality.Checked{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
170 storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
171 dynamic_read_projection(shape, Totality.Checked{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
172 core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Checked{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
173 {\{InspectionModel: equal => equal} :
174 InspectionModel<storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
175 array_inspect(depth, length, Totality.Checked{other}, array)> ->
176 {storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
177 array_inspect(depth, length, Totality.Checked{other}, array) : Totality.Inspection}}(
178 read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Checked{other}, array, {==}, balanced, valid)))}
179 case Totality.Raw{+other}:
180 InspectionModel{Equal.trans(Totality.Inspection,
181 Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
182 storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
183 array_inspect(depth, length, Totality.Raw{other}, array),
184 Equal.trans(Totality.Inspection,
185 Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
186 Totality.inspect(Totality.Raw{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
187 storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
188 dynamic_read_projection(shape, Totality.Raw{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
189 core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Raw{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
190 {\{InspectionModel: equal => equal} :
191 InspectionModel<storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
192 array_inspect(depth, length, Totality.Raw{other}, array)> ->
193 {storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
194 array_inspect(depth, length, Totality.Raw{other}, array) : Totality.Inspection}}(
195 read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Raw{other}, array, {==}, balanced, valid)))}
196
197def empty_read_property(+shape: Shape.Shape, +index: U32, property: Totality.Property,
198 -exact: {0n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
199 InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))),
200 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}})>:
201 match property:
202 case Totality.Dimensions{}:
203 InspectionModel{{==}}
204 case Totality.Checked{other}:
205 InspectionModel{{==}}
206 case Totality.Raw{other}:
207 InspectionModel{{==}}
208
209def dynamic_read_retains(original: Core.Dynamic, +index: U32) -> SourceModel<original, dynamic_read_owner(Core.read_dynamic(original, index))>:
210 Core.Packed{+shape, Core.TTensor{storage, exact}} = original
211 match storage:
212 case Storage.Empty{}:
213 SourceModel{property => {\{InspectionModel: equal => equal} :
214 InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))),
215 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}})> ->
216 {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))) ==
217 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}) : Totality.Inspection}}(
218 empty_read_property(shape, index, property, exact))}
219 case Storage.Owned{+depth, +length, array, balanced, valid}:
220 SourceModel{property => {\{InspectionModel: equal => equal} :
221 InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
222 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}})> ->
223 {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))) ==
224 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) : Totality.Inspection}}(
225 owned_read_property(shape, depth, length, index, property, array, balanced, valid, exact))}
226
227def step_left_owner(-shape: Shape.Shape, result: Elementwise.Step<shape>) -> Core.Dynamic:
228 match result:
229 case Elementwise.Stop{left, right, error}:
230 left
231 case Elementwise.Continue{Elementwise.State{left, right, output}}:
232 left
233
234def step_right_owner(-shape: Shape.Shape, result: Elementwise.Step<shape>) -> Core.Dynamic:
235 match result:
236 case Elementwise.Stop{left, right, error}:
237 right
238 case Elementwise.Continue{Elementwise.State{left, right, output}}:
239 right
240
241type StepSources<-shape: Shape.Shape, -left: Core.Dynamic, -right: Core.Dynamic, -result: Elementwise.Step<shape>> is Data:
242 StepSources{-left: Totality.SameSource(left, step_left_owner(shape, result)),
243 -right: Totality.SameSource(right, step_right_owner(shape, result))}
244
245def step_sources_reify(-shape: Shape.Shape, -left: Core.Dynamic, -right: Core.Dynamic, -result: Elementwise.Step<shape>,
246 -model: StepSources<shape, left, right, result>) -> StepSources<shape, left, right, result>:
247 StepSources{
248 {\{StepSources: left_same => right_same => left_same} : StepSources<shape, left, right, result> -> Totality.SameSource(left, step_left_owner(shape, result))}(model),
249 {\{StepSources: left_same => right_same => right_same} : StepSources<shape, left, right, result> -> Totality.SameSource(right, step_right_owner(shape, result))}(model)}
250
251def step_write_retains(-shape: Shape.Shape, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
252 left: Core.Dynamic, right: Core.Dynamic, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
253 -left_same: Totality.SameSource(original_left, left), -right_same: Totality.SameSource(original_right, right)) ->
254 StepSources<shape, original_left, original_right, Elementwise.step_write(shape, left, right, pair)>:
255 (output, result) = pair
256 match result:
257 case Fail{error}:
258 StepSources{left_same, right_same}
259 case Done{unit}:
260 StepSources{left_same, right_same}
261
262def step_right_retains(+operation: Elementwise.Operation, -shape: Shape.Shape, +index: U32,
263 -original_left: Core.Dynamic, -original_right: Core.Dynamic, left: Core.Dynamic,
264 output: Core.Tensor<shape>, left_value: F32, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
265 -left_same: Totality.SameSource(original_left, left),
266 -right_same: Totality.SameSource(original_right, dynamic_read_owner(pair))) ->
267 StepSources<shape, original_left, original_right, Elementwise.step_right(operation, shape, index, left, output, left_value, pair)>:
268 (right, result) = pair
269 match result:
270 case Fail{error}:
271 StepSources{left_same, right_same}
272 case Done{value}:
273 step_write_retains(shape, original_left, original_right, left, right,
274 Core.write_flat(shape, output, index, Elementwise.scalar(operation, left_value, value)), left_same, right_same)
275
276def step_left_retains(+operation: Elementwise.Operation, -shape: Shape.Shape, +index: U32,
277 -original_left: Core.Dynamic, -original_right: Core.Dynamic, right: Core.Dynamic,
278 output: Core.Tensor<shape>, +right_index: U32, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
279 -left_same: Totality.SameSource(original_left, dynamic_read_owner(pair)),
280 -right_same: Totality.SameSource(original_right, right)) ->
281 StepSources<shape, original_left, original_right, Elementwise.step_left(operation, shape, index, right, output, right_index, pair)>:
282 (left, result) = pair
283 match result:
284 case Fail{error}:
285 StepSources{left_same, right_same}
286 case Done{value}:
287 step_sources_reify(shape, original_left, original_right,
288 Elementwise.step_right(operation, shape, index, left, output, value, Core.read_dynamic(right, right_index)),
289 {\{SourceModel: same => step_right_retains(operation, shape, index, original_left, original_right, left, output, value,
290 Core.read_dynamic(right, right_index), left_same,
291 property => Equal.trans(Totality.Inspection,
292 Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(right, right_index))),
293 Totality.inspect(property, right), Totality.inspect(property, original_right), same(property), right_same(property)))} :
294 SourceModel<right, dynamic_read_owner(Core.read_dynamic(right, right_index))> ->
295 StepSources<shape, original_left, original_right, Elementwise.step_right(operation, shape, index, left, output, value, Core.read_dynamic(right, right_index))>}(
296 dynamic_read_retains(right, right_index)))
297
298def step_indices_retains(+operation: Elementwise.Operation, -shape: Shape.Shape, +index: U32,
299 state: Elementwise.State<shape>, result: Result<&2, &1, Core.Error, U32 & U32>) ->
300 StepSources<shape,
301 step_left_owner(shape, Elementwise.Continue{state}), step_right_owner(shape, Elementwise.Continue{state}),
302 Elementwise.step_indices(operation, shape, index, state, result)>:
303 Elementwise.State{left, right, output} = state
304 match result:
305 case Fail{error}:
306 StepSources{property => {==}, property => {==}}
307 case Done{indices}:
308 (+left_index, +right_index) = indices
309 step_sources_reify(shape, left, right,
310 Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index)),
311 {\{SourceModel: same => step_left_retains(operation, shape, index, left, right, right, output, right_index,
312 Core.read_dynamic(left, left_index), same, property => {==})} :
313 SourceModel<left, dynamic_read_owner(Core.read_dynamic(left, left_index))> ->
314 StepSources<shape, left, right, Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index))>}(
315 dynamic_read_retains(left, left_index)))
316
317def natural_left_owner(-shape: Shape.Shape, -cursor: Nat, result: Elementwise.NaturalStep<shape, cursor>) -> Core.Dynamic:
318 match result:
319 case Elementwise.NaturalStop{left, right, error}:
320 left
321 case Elementwise.NaturalContinue{state, index, exact}:
322 step_left_owner(shape, Elementwise.Continue{state})
323
324def natural_right_owner(-shape: Shape.Shape, -cursor: Nat, result: Elementwise.NaturalStep<shape, cursor>) -> Core.Dynamic:
325 match result:
326 case Elementwise.NaturalStop{left, right, error}:
327 right
328 case Elementwise.NaturalContinue{state, index, exact}:
329 step_right_owner(shape, Elementwise.Continue{state})
330
331type NaturalSources<-shape: Shape.Shape, -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic,
332 -result: Elementwise.NaturalStep<shape, cursor>> is Data:
333 NaturalSources{-left: Totality.SameSource(left, natural_left_owner(shape, cursor, result)),
334 -right: Totality.SameSource(right, natural_right_owner(shape, cursor, result))}
335
336def natural_result_retains(-shape: Shape.Shape, -cursor: Nat, -index: U32, -exact: {U32.to_nat(index) == cursor : Nat},
337 -left: Core.Dynamic, -right: Core.Dynamic, result: Elementwise.Step<shape>, -sources: StepSources<shape, left, right, result>) ->
338 NaturalSources<shape, cursor, left, right, Elementwise.natural_step_result(shape, cursor, index, exact, result)>:
339 match result:
340 case Elementwise.Stop{retained_left, retained_right, error}:
341 NaturalSources{
342 {\{StepSources: l => r => l} : StepSources<shape, left, right, Elementwise.Stop{retained_left, retained_right, error}> -> Totality.SameSource(left, retained_left)}(sources),
343 {\{StepSources: l => r => r} : StepSources<shape, left, right, Elementwise.Stop{retained_left, retained_right, error}> -> Totality.SameSource(right, retained_right)}(sources)}
344 case Elementwise.Continue{state}:
345 NaturalSources{
346 {\{StepSources: l => r => l} : StepSources<shape, left, right, Elementwise.Continue{state}> -> Totality.SameSource(left, step_left_owner(shape, Elementwise.Continue{state}))}(sources),
347 {\{StepSources: l => r => r} : StepSources<shape, left, right, Elementwise.Continue{state}> -> Totality.SameSource(right, step_right_owner(shape, Elementwise.Continue{state}))}(sources)}
348
349def natural_decided_retains(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
350 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>) ->
351 NaturalSources<Shape.output_shape(plan), cursor,
352 step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
353 Elementwise.natural_step_decided(operation, plan, cursor, index, state, decision)>:
354 match decision:
355 case Shape.BFalse{equal}:
356 Elementwise.State{left, right, output} = state
357 NaturalSources{property => {==}, property => {==}}
358 case Shape.BTrue{equal}:
359 natural_result_retains(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal),
360 step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
361 Elementwise.step(operation, plan, index, state),
362 step_indices_retains(operation, Shape.output_shape(plan), index, state, Elementwise.input_indices(plan, index)))
363
364def retention_reify(-left: Core.Dynamic, -right: Core.Dynamic,
365 -pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
366 -model: Totality.Retention<left, right, pair>) -> Totality.Retention<left, right, pair>:
367 Totality.Retention{
368 {\{Totality.Retention: l => r => l} : Totality.Retention<left, right, pair> -> Totality.SameSource(left, Totality.retained_left(pair))}(model),
369 {\{Totality.Retention: l => r => r} : Totality.Retention<left, right, pair> -> Totality.SameSource(right, Totality.retained_right(pair))}(model)}
370
371def loop_finish_retains(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
372 -left: Core.Dynamic, -right: Core.Dynamic, result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
373 -sources: NaturalSources<Shape.output_shape(plan), cursor, left, right, result>,
374 -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
375 @-l: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
376 @-r: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
377 Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
378 Totality.Retention<left, right, Elementwise.finish_step(Shape.output_shape(plan), cursor,
379 state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
380 match result:
381 case Elementwise.NaturalStop{retained_left, retained_right, error}:
382 Totality.Retention{
383 {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(left, retained_left)}(sources),
384 {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(right, retained_right)}(sources)}
385 case Elementwise.NaturalContinue{state, index, exact}:
386 retention_reify(left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state),
387 rec(state)(
388 {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
389 Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources))(
390 {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
391 Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources)))
392
393def loop_retains(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
394 -left: Core.Dynamic, -right: Core.Dynamic, state: Elementwise.State<Shape.output_shape(plan)>,
395 -left_same: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})),
396 -right_same: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))) ->
397 Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, cursor, state)>:
398 match fuel:
399 case 0n:
400 Elementwise.State{retained_left, retained_right, output} = state
401 Totality.Retention{left_same, right_same}
402 case 1n+remaining:
403 loop_finish_retains(remaining, operation, plan, cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state),
404 {\{NaturalSources: l => r => NaturalSources{
405 property => Equal.trans(Totality.Inspection,
406 Totality.inspect(property, natural_left_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
407 Totality.inspect(property, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, left), l(property), left_same(property)),
408 property => Equal.trans(Totality.Inspection,
409 Totality.inspect(property, natural_right_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
410 Totality.inspect(property, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, right), r(property), right_same(property))}} :
411 NaturalSources<Shape.output_shape(plan), cursor, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
412 Elementwise.natural_step(operation, plan, cursor, state)> ->
413 NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state)>}(
414 natural_decided_retains(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state)),
415 state => l => r => loop_retains(remaining, operation, plan, 1n+cursor, left, right, state, l, r))
416
417def allocated_retains(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
418 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>) ->
419 Totality.Retention<left, right, Elementwise.allocated(operation, plan, left, right, result)>:
420 match result:
421 case Fail{error}:
422 Totality.Retention{property => {==}, property => {==}}
423 case Done{output}:
424 loop_retains(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, left, right, Elementwise.State{left, right, output}, property => {==}, property => {==})
425
426def output_retains(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
427 -valid: {Storage.bounds(depth, length) == True{} : Bool},
428 -exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
429 -left: Core.Dynamic, -right: Core.Dynamic, taken_left: Core.Dynamic & Array<F32>, taken_right: Core.Dynamic & Array<F32>,
430 -left_taken: Parallel.Taken<left, taken_left>, -right_taken: Parallel.Taken<right, taken_right>) ->
431 Totality.Retention<left, right, Elementwise.parallel_output(operation, plan, depth, length, valid, exact, taken_left, taken_right)>:
432 (kept_left, la) = taken_left
433 (kept_right, ra) = taken_right
434 Totality.Retention{
435 {\{Parallel.Taken: depth => balanced => reads => same => same} : Parallel.Taken<left, (kept_left, la)> -> Totality.SameSource(left, kept_left)}(left_taken),
436 {\{Parallel.Taken: depth => balanced => reads => same => same} : Parallel.Taken<right, (kept_right, ra)> -> Totality.SameSource(right, kept_right)}(right_taken)}
437
438def parallel_allocated_retains(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
439 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>) ->
440 Totality.Retention<left, right, Elementwise.parallel_allocated(operation, plan, left, right, result)>:
441 match result:
442 case Fail{error}:
443 Totality.Retention{property => {==}, property => {==}}
444 case Done{Core.TTensor{storage, exact}}:
445 match storage:
446 case Storage.Empty{}:
447 Totality.Retention{property => {==}, property => {==}}
448 case Storage.Owned{+depth, +length, array, balanced, valid}:
449 output_retains(operation, plan, depth, length, valid, exact, left, right, Elementwise.take(left), Elementwise.take(right),
450 Parallel.taken(left), Parallel.taken(right))
451
452def planned_retains(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic,
453 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>) ->
454 Totality.Retention<left, right, Elementwise.parallel_planned(operation, left, right, result)>:
455 match result:
456 case Fail{error}:
457 Totality.Retention{property => {==}, property => {==}}
458 case Done{+plan}:
459 parallel_allocated_retains(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))
460
461def Laws.binary_retains_inputs(operation, left, right):
462 Core.Packed{+left_shape, left_tensor} = left
463 Core.Packed{+right_shape, right_tensor} = right
464 planned_retains(operation, Core.Packed{left_shape, left_tensor}, Core.Packed{right_shape, right_tensor},
465 Shape.broadcast_checked(left_shape, right_shape))
466
467def dimensions_reify(-output: List<&2, U32>, -pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
468 -model: Totality.DimensionsModel<output, pair>) -> Totality.DimensionsModel<output, pair>:
469 Totality.DimensionsModel{{\{Totality.DimensionsModel: exact => exact} : Totality.DimensionsModel<output, pair> -> Totality.OutputDimensions(output, pair)}(model)}
470
471def loop_finish_dimensions(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
472 result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
473 -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
474 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
475 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.finish_step(Shape.output_shape(plan), cursor,
476 state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
477 match result:
478 case Elementwise.NaturalStop{left, right, error}:
479 Totality.DimensionsModel{Unit{}}
480 case Elementwise.NaturalContinue{state, index, exact}:
481 dimensions_reify(Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, 1n+cursor, state), rec(state))
482
483def loop_dimensions(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
484 state: Elementwise.State<Shape.output_shape(plan)>) ->
485 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, cursor, state)>:
486 match fuel:
487 case 0n:
488 Elementwise.State{left, right, output} = state
489 Totality.DimensionsModel{{==}}
490 case 1n+remaining:
491 loop_finish_dimensions(remaining, operation, plan, cursor, Elementwise.natural_step(operation, plan, cursor, state),
492 state => loop_dimensions(remaining, operation, plan, 1n+cursor, state))
493
494def allocated_dimensions(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
495 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>) ->
496 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.allocated(operation, plan, left, right, result)>:
497 match result:
498 case Fail{error}:
499 Totality.DimensionsModel{Unit{}}
500 case Done{output}:
501 loop_dimensions(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})
502
503def words_naturals(+dimensions: List<&2, U32>) -> {Shape.words(Shape.naturals(dimensions)) == dimensions : List<&2, U32>}:
504 match dimensions:
505 case Nil{}:
506 {==}
507 case +head <> +tail:
508 %words_naturals(tail) : {U32.from_nat(U32.to_nat(head)) <> Shape.words(Shape.naturals(tail)) == head <> _ : List<&2, U32>}
509 %Conversion.word_natural_exact(head) : {U32.from_nat(U32.to_nat(head)) <> Shape.words(Shape.naturals(tail)) == _ <> Shape.words(Shape.naturals(tail)) : List<&2, U32>}
510 {==}
511
512def natural_dimensions_equal(+left: List<&2, U32>, +right: List<&2, U32>,
513 equal: {Shape.naturals(left) == Shape.naturals(right) : List<&2, Nat>}) -> {left == right : List<&2, U32>}:
514 Equal.trans(List<&2, U32>, left, Shape.words(Shape.naturals(left)), right,
515 Equal.sym(List<&2, U32>, Shape.words(Shape.naturals(left)), left, words_naturals(left)),
516 Equal.trans(List<&2, U32>, Shape.words(Shape.naturals(left)), Shape.words(Shape.naturals(right)), right,
517 Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Shape.naturals(left), Shape.naturals(right), equal), words_naturals(right)))
518
519def planned_output_dimensions(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, +output: List<&2, U32>,
520 +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.naturals(output)>,
521 +sources: {(Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))) ==
522 (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}) ->
523 {Shape.dimensions(Shape.output_shape(plan)) == output : List<&2, U32>}:
524 natural_dimensions_equal(Shape.dimensions(Shape.output_shape(plan)), output,
525 Unique.broadcast_unique(Shape.extents(left), Shape.extents(right), Shape.extents(Shape.output_shape(plan)), Shape.naturals(output),
526 %Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, Nat>, pair => Shape.naturals(Pair.fst(List<&2, U32>, List<&2, U32>, pair)),
527 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), sources) :
528 Shape.Broadcast<_, Shape.extents(right), Shape.extents(Shape.output_shape(plan))>
529 %Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, Nat>, pair => Shape.naturals(Pair.snd(List<&2, U32>, List<&2, U32>, pair)),
530 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), sources) :
531 Shape.Broadcast<Shape.extents(Shape.left_shape(plan)), _, Shape.extents(Shape.output_shape(plan))>
532 Shape.alignment(plan), alignment))
533
534def output_dimensions(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
535 -valid: {Storage.bounds(depth, length) == True{} : Bool},
536 -exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
537 taken_left: Core.Dynamic & Array<F32>, taken_right: Core.Dynamic & Array<F32>) ->
538 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.parallel_output(operation, plan, depth, length, valid, exact, taken_left, taken_right)>:
539 (kept_left, la) = taken_left
540 (kept_right, ra) = taken_right
541 Totality.DimensionsModel{{==}}
542
543def parallel_allocated_dimensions(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
544 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>) ->
545 Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.parallel_allocated(operation, plan, left, right, result)>:
546 match result:
547 case Fail{error}:
548 Totality.DimensionsModel{Unit{}}
549 case Done{Core.TTensor{storage, exact}}:
550 match storage:
551 case Storage.Empty{}:
552 Totality.DimensionsModel{{==}}
553 case Storage.Owned{+depth, +length, array, balanced, valid}:
554 output_dimensions(operation, plan, depth, length, valid, exact, Elementwise.take(left), Elementwise.take(right))
555
556def planned_dimensions(+operation: Elementwise.Operation, +left_shape: Shape.Shape, +right_shape: Shape.Shape, +output: List<&2, U32>,
557 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, left: Core.Tensor<left_shape>, right: Core.Tensor<right_shape>,
558 -sources: {ShapeLaws.planned_dimensions(left_shape, right_shape, result) == (Shape.dimensions(left_shape), Shape.dimensions(right_shape)) : List<&2, U32> & List<&2, U32>},
559 -alignment: Shape.Broadcast<Shape.extents(left_shape), Shape.extents(right_shape), Shape.naturals(output)>) ->
560 Totality.DimensionsModel<output, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, result)>:
561 match result:
562 case Fail{error}:
563 Totality.DimensionsModel{Unit{}}
564 case Done{+plan}:
565 dimensions_reify(output, Elementwise.parallel_allocated(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0)),
566 %planned_output_dimensions(left_shape, right_shape, plan, output, alignment, sources) :
567 Totality.DimensionsModel<_, Elementwise.parallel_allocated(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0))>
568 parallel_allocated_dimensions(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0)))
569
570def Laws.binary_successful_output_dimensions(operation, left, right, output, alignment):
571 Core.Packed{+left_shape, left_tensor} = left
572 Core.Packed{+right_shape, right_tensor} = right
573 planned_dimensions(operation, left_shape, right_shape, output, Shape.broadcast_checked(left_shape, right_shape), left_tensor, right_tensor,
574 PlanProof.broadcast_checked_plan(left_shape, right_shape), alignment)
575
576def dynamic_read_succeeded(pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>) -> Bool:
577 (owner, result) = pair
578 Result.is_done(&2, &2, Core.Error, F32, result)
579
580def dynamic_read_status(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
581 {dynamic_read_succeeded(Core.read_dynamic_result(shape, pair)) == TransformTotality.read_succeeded(shape, pair) : Bool}:
582 (owner, result) = pair
583 {==}
584
585type DynamicReadSuccess<-owner: Core.Dynamic, -index: U32> is Data:
586 DynamicReadSuccess{-successful: {dynamic_read_succeeded(Core.read_dynamic(owner, index)) == True{} : Bool}}
587
588def dynamic_read_success(original: Core.Dynamic, +index: U32,
589 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Totality.dimensions(original))) == True{} : Bool}) -> DynamicReadSuccess<original, index>:
590 Core.Packed{+shape, tensor} = original
591 DynamicReadSuccess{Equal.trans(Bool, dynamic_read_succeeded(Core.read_dynamic(Core.Packed{shape, tensor}, index)),
592 TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, index)), True{},
593 dynamic_read_status(shape, Core.read_flat(shape, tensor, index)),
594 {\{TransformTotality.ReadSuccess: successful => successful} : TransformTotality.ReadSuccess<shape, tensor, index> ->
595 {TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, index)) == True{} : Bool}}(
596 TransformProof.read_success_status(shape, tensor, index, TransformProof.read_success(shape, tensor, index, inside))))}
597
598def flat_index_inside(+shape: Shape.Shape, +index: Shape.FlatIndex<shape>) ->
599 {Nat.is_lt(U32.to_nat(Shape.index_value(shape, index)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
600 Shape.FIndex{+value, +bound} = index
601 %Shape.elements_exact(shape) :
602 {Nat.is_lt(U32.to_nat(U32.from_nat(value)), _) == True{} : Bool}
603 %Equal.sym(Nat, U32.to_nat(U32.from_nat(value)), value,
604 TransformProof.cursor_word_exact(shape, value, Conversion.lt_le(value, Shape.elements(shape), Equal.sym(Bool, True{}, Nat.is_lt(value, Shape.elements(shape)), bound)))) :
605 {Nat.is_lt(_, Shape.elements(shape)) == True{} : Bool}
606 Equal.sym(Bool, True{}, Nat.is_lt(value, Shape.elements(shape)), bound)
607
608type IndicesDone<-plan: Shape.BroadcastPlan, -result: Result<&2, &1, Core.Error, U32 & U32>> is Data:
609 IndicesDone{-left: U32, -right: U32,
610 -exact: {Done{(left, right)} == result : Result<&2, &1, Core.Error, U32 & U32>},
611 -left_bound: {Nat.is_lt(U32.to_nat(left), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))) == True{} : Bool},
612 -right_bound: {Nat.is_lt(U32.to_nat(right), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool}}
613
614def checked_indices_success(+plan: Shape.BroadcastPlan, +index: U32,
615 decision: Shape.BoolCase<Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))>,
616 -inside: {Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
617 IndicesDone<plan, Elementwise.flat_input_indices(plan, Shape.flat_checked.finish(Shape.output_shape(plan), U32.to_nat(index), decision))>:
618 match decision:
619 case Shape.BFalse{equal}:
620 IndicesDone{0, 0,
621 Empty.absurd({Done{(0, 0)} == Fail{Core.ShapeError{Shape.FlatIndexOutOfBounds{}}} : Result<&2, &1, Core.Error, U32 & U32>},
622 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside))),
623 Empty.absurd({Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))) == True{} : Bool},
624 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside))),
625 Empty.absurd({Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool},
626 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside)))}
627 case Shape.BTrue{equal}:
628 +flat = {Shape.FIndex{U32.to_nat(index), equal} : Shape.FlatIndex<Shape.output_shape(plan)>}
629 +left = Flat.project_left_index(plan, Shape.index_map(plan), flat)
630 +right = Flat.project_right_index(plan, Shape.index_map(plan), flat)
631 IndicesDone{Shape.index_value(Shape.left_shape(plan), left), Shape.index_value(Shape.right_shape(plan), right), {==},
632 flat_index_inside(Shape.left_shape(plan), left), flat_index_inside(Shape.right_shape(plan), right)}
633
634def indices_success(+plan: Shape.BroadcastPlan, +index: U32,
635 -inside: {Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
636 IndicesDone<plan, Elementwise.input_indices(plan, index)>:
637 checked_indices_success(plan, index, Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))), inside)
638
639def step_succeeded(-shape: Shape.Shape, result: Elementwise.Step<shape>) -> Bool:
640 match result:
641 case Elementwise.Stop{left, right, error}:
642 False{}
643 case Elementwise.Continue{state}:
644 True{}
645
646type StepSuccess<-shape: Shape.Shape, -result: Elementwise.Step<shape>> is Data:
647 StepSuccess{-successful: {step_succeeded(shape, result) == True{} : Bool}}
648
649type FittingSources<-plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic> is Data:
650 FittingSources{-left: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
651 -right: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}}
652
653def step_write_success(-shape: Shape.Shape, left: Core.Dynamic, right: Core.Dynamic,
654 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
655 -successful: {TransformTotality.write_succeeded(shape, pair) == True{} : Bool}) -> StepSuccess<shape, Elementwise.step_write(shape, left, right, pair)>:
656 (output, result) = pair
657 match result:
658 case Fail{error}:
659 StepSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
660 case Done{unit}:
661 StepSuccess{{==}}
662
663def step_right_success(+operation: Elementwise.Operation, +shape: Shape.Shape, +index: U32,
664 left: Core.Dynamic, output: Core.Tensor<shape>, left_value: F32, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
665 -successful: {dynamic_read_succeeded(pair) == True{} : Bool},
666 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
667 StepSuccess<shape, Elementwise.step_right(operation, shape, index, left, output, left_value, pair)>:
668 (right, result) = pair
669 match result:
670 case Fail{error}:
671 StepSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
672 case Done{+value}:
673 step_write_success(shape, left, right, Core.write_flat(shape, output, index, Elementwise.scalar(operation, left_value, value)),
674 {\{TransformTotality.WriteSuccess: successful => successful} :
675 TransformTotality.WriteSuccess<shape, output, index, Elementwise.scalar(operation, left_value, value)> ->
676 {TransformTotality.write_succeeded(shape, Core.write_flat(shape, output, index, Elementwise.scalar(operation, left_value, value))) == True{} : Bool}}(
677 TransformProof.tensor_write_success(shape, output, index, Elementwise.scalar(operation, left_value, value), inside)))
678
679def step_left_success(+operation: Elementwise.Operation, +shape: Shape.Shape, +index: U32,
680 right: Core.Dynamic, output: Core.Tensor<shape>, +right_index: U32, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
681 -successful: {dynamic_read_succeeded(pair) == True{} : Bool},
682 -right_inside: {Nat.is_lt(U32.to_nat(right_index), Shape.logical_numel(Totality.dimensions(right))) == True{} : Bool},
683 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
684 StepSuccess<shape, Elementwise.step_left(operation, shape, index, right, output, right_index, pair)>:
685 (left, result) = pair
686 match result:
687 case Fail{error}:
688 StepSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
689 case Done{value}:
690 step_right_success(operation, shape, index, left, output, value, Core.read_dynamic(right, right_index),
691 {\{DynamicReadSuccess: successful => successful} : DynamicReadSuccess<right, right_index> ->
692 {dynamic_read_succeeded(Core.read_dynamic(right, right_index)) == True{} : Bool}}(dynamic_read_success(right, right_index, right_inside)), inside)
693
694def actual_step_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
695 state: Elementwise.State<Shape.output_shape(plan)>,
696 -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
697 -inside: {Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
698 StepSuccess<Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)>:
699 Elementwise.State{left, right, output} = state
700 StepSuccess{{\{IndicesDone: li => ri => exact => lb => rb =>
701 %exact : {step_succeeded(Shape.output_shape(plan), Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, _)) == True{} : Bool}
702 {\{StepSuccess: successful => successful} :
703 StepSuccess<Shape.output_shape(plan), Elementwise.step_left(operation, Shape.output_shape(plan), index, right, output, ri, Core.read_dynamic(left, li))> ->
704 {step_succeeded(Shape.output_shape(plan), Elementwise.step_left(operation, Shape.output_shape(plan), index, right, output, ri, Core.read_dynamic(left, li))) == True{} : Bool}}(
705 step_left_success(operation, Shape.output_shape(plan), index, right, output, ri, Core.read_dynamic(left, li),
706 {\{DynamicReadSuccess: successful => successful} : DynamicReadSuccess<left, li> -> {dynamic_read_succeeded(Core.read_dynamic(left, li)) == True{} : Bool}}(
707 dynamic_read_success(left, li,
708 %Equal.sym(List<&2, U32>, Totality.dimensions(left), Shape.dimensions(Shape.left_shape(plan)),
709 {\{FittingSources: l => r => l} : FittingSources<plan, left, right> -> {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}}(fits)) :
710 {Nat.is_lt(U32.to_nat(li), Shape.logical_numel(_)) == True{} : Bool}
711 lb)),
712 %Equal.sym(List<&2, U32>, Totality.dimensions(right), Shape.dimensions(Shape.right_shape(plan)),
713 {\{FittingSources: l => r => r} : FittingSources<plan, left, right> -> {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}}(fits)) :
714 {Nat.is_lt(U32.to_nat(ri), Shape.logical_numel(_)) == True{} : Bool}
715 rb,
716 %Shape.elements_exact(Shape.output_shape(plan)) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
717 inside))} : IndicesDone<plan, Elementwise.input_indices(plan, index)> ->
718 {step_succeeded(Shape.output_shape(plan), Elementwise.step(operation, plan, index, Elementwise.State{left, right, output})) == True{} : Bool}}(
719 indices_success(plan, index, inside))}
720
721def natural_succeeded(-shape: Shape.Shape, -cursor: Nat, result: Elementwise.NaturalStep<shape, cursor>) -> Bool:
722 match result:
723 case Elementwise.NaturalStop{left, right, error}:
724 False{}
725 case Elementwise.NaturalContinue{state, index, exact}:
726 True{}
727
728type NaturalSuccess<-shape: Shape.Shape, -cursor: Nat, -result: Elementwise.NaturalStep<shape, cursor>> is Data:
729 NaturalSuccess{-successful: {natural_succeeded(shape, cursor, result) == True{} : Bool}}
730
731def natural_result_success(-shape: Shape.Shape, -cursor: Nat, -index: U32, -exact: {U32.to_nat(index) == cursor : Nat},
732 result: Elementwise.Step<shape>, -successful: {step_succeeded(shape, result) == True{} : Bool}) ->
733 NaturalSuccess<shape, cursor, Elementwise.natural_step_result(shape, cursor, index, exact, result)>:
734 match result:
735 case Elementwise.Stop{left, right, error}:
736 NaturalSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
737 case Elementwise.Continue{state}:
738 NaturalSuccess{{==}}
739
740def natural_decided_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
741 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>,
742 -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
743 -exact: {U32.to_nat(index) == cursor : Nat}, -inside: {Nat.is_lt(cursor, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
744 NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step_decided(operation, plan, cursor, index, state, decision)>:
745 match decision:
746 case Shape.BFalse{equal}:
747 Elementwise.State{left, right, output} = state
748 NaturalSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor), PlanProof.eq_true(U32.to_nat(index), cursor, exact), equal))}
749 case Shape.BTrue{equal}:
750 natural_result_success(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal),
751 Elementwise.step(operation, plan, index, state),
752 {\{StepSuccess: successful => successful} : StepSuccess<Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)> ->
753 {step_succeeded(Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)) == True{} : Bool}}(
754 actual_step_success(operation, plan, index, state, fits,
755 %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}
756 inside)))
757
758def natural_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
759 state: Elementwise.State<Shape.output_shape(plan)>,
760 -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
761 -inside: {Nat.is_lt(cursor, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
762 NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state)>:
763 natural_decided_success(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state, fits,
764 TransformProof.cursor_word_exact(Shape.output_shape(plan), cursor, Conversion.lt_le(cursor, Shape.elements(Shape.output_shape(plan)), inside)), inside)
765
766def inspection_dimensions(value: Totality.Inspection) -> List<&2, U32>:
767 match value:
768 case Totality.Dims{dimensions}:
769 dimensions
770 case Totality.Value{value}:
771 Nil{}
772
773def retained_fits(+plan: Shape.BroadcastPlan, -before_left: Core.Dynamic, -before_right: Core.Dynamic,
774 -after_left: Core.Dynamic, -after_right: Core.Dynamic,
775 -left_same: Totality.SameSource(before_left, after_left), -right_same: Totality.SameSource(before_right, after_right),
776 -fits: FittingSources<plan, before_left, before_right>) -> FittingSources<plan, after_left, after_right>:
777 FittingSources{
778 Equal.trans(List<&2, U32>, Totality.dimensions(after_left), Totality.dimensions(before_left), Shape.dimensions(Shape.left_shape(plan)),
779 Equal.cong(Totality.Inspection, List<&2, U32>, inspection_dimensions,
780 Totality.inspect(Totality.Dimensions{}, after_left), Totality.inspect(Totality.Dimensions{}, before_left), left_same(Totality.Dimensions{})),
781 {\{FittingSources: l => r => l} : FittingSources<plan, before_left, before_right> -> {Totality.dimensions(before_left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}}(fits)),
782 Equal.trans(List<&2, U32>, Totality.dimensions(after_right), Totality.dimensions(before_right), Shape.dimensions(Shape.right_shape(plan)),
783 Equal.cong(Totality.Inspection, List<&2, U32>, inspection_dimensions,
784 Totality.inspect(Totality.Dimensions{}, after_right), Totality.inspect(Totality.Dimensions{}, before_right), right_same(Totality.Dimensions{})),
785 {\{FittingSources: l => r => r} : FittingSources<plan, before_left, before_right> -> {Totality.dimensions(before_right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}}(fits))}
786
787def success_reify(-pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
788 -model: Totality.Success<pair>) -> Totality.Success<pair>:
789 Totality.Success{{\{Totality.Success: successful => successful} : Totality.Success<pair> -> {Totality.succeeded(pair) == True{} : Bool}}(model)}
790
791def loop_finish_success(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
792 -before_left: Core.Dynamic, -before_right: Core.Dynamic,
793 result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
794 -successful: {natural_succeeded(Shape.output_shape(plan), cursor, result) == True{} : Bool},
795 -sources: NaturalSources<Shape.output_shape(plan), cursor, before_left, before_right, result>,
796 -fits: FittingSources<plan, before_left, before_right>,
797 -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
798 @-next_fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})> ->
799 Totality.Success<Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
800 Totality.Success<Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
801 match result:
802 case Elementwise.NaturalStop{left, right, error}:
803 Totality.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
804 case Elementwise.NaturalContinue{state, index, exact}:
805 success_reify(Elementwise.loop(fuel, operation, plan, 1n+cursor, state),
806 rec(state)(retained_fits(plan, before_left, before_right,
807 step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
808 {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, before_left, before_right, Elementwise.NaturalContinue{state, index, exact}> ->
809 Totality.SameSource(before_left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources),
810 {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, before_left, before_right, Elementwise.NaturalContinue{state, index, exact}> ->
811 Totality.SameSource(before_right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources), fits)))
812
813def loop_success(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
814 state: Elementwise.State<Shape.output_shape(plan)>,
815 -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
816 -within: {Nat.is_le(Nat.add(fuel, cursor), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
817 Totality.Success<Elementwise.loop(fuel, operation, plan, cursor, state)>:
818 match fuel:
819 case 0n:
820 Elementwise.State{left, right, output} = state
821 Totality.Success{{==}}
822 case 1n+remaining:
823 loop_finish_success(remaining, operation, plan, cursor,
824 step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
825 Elementwise.natural_step(operation, plan, cursor, state),
826 {\{NaturalSuccess: successful => successful} : NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state)> ->
827 {natural_succeeded(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state)) == True{} : Bool}}(
828 natural_success(operation, plan, cursor, state, fits,
829 Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(Shape.output_shape(plan)),
830 Arith.lt_succ(cursor, Nat.add(remaining, cursor), TransformProof.add_cursor_le(remaining, cursor)), within))),
831 natural_decided_retains(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state), fits,
832 state => next_fits => loop_success(remaining, operation, plan, 1n+cursor, state, next_fits,
833 %Equal.sym(Nat, Nat.add(remaining, 1n+cursor), 1n+Nat.add(remaining, cursor), Arith.add_succ(remaining, cursor)) :
834 {Nat.is_le(_, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}
835 within))
836
837def allocated_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
838 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>,
839 -fits: FittingSources<plan, left, right>, -done: Allocation.TensorDone<Shape.output_shape(plan), result>) ->
840 Totality.Success<Elementwise.allocated(operation, plan, left, right, result)>:
841 match result:
842 case Fail{error}:
843 Totality.Success{Empty.absurd({False{} == True{} : Bool},
844 {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, Bool,
845 result => Result.is_done(&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>, result), Fail{error}, Done{tensor},
846 Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, Done{tensor}, Fail{error}, same)))} :
847 Allocation.TensorDone<Shape.output_shape(plan), Fail{error}> -> Empty}(done))}
848 case Done{output}:
849 loop_success(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}, fits,
850 %Equal.sym(Nat, Nat.add(Shape.elements(Shape.output_shape(plan)), 0n), Shape.elements(Shape.output_shape(plan)), TransformProof.add_zero_right(Shape.elements(Shape.output_shape(plan)))) :
851 {Nat.is_le(_, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}
852 Conversion.le_reflexive(Shape.elements(Shape.output_shape(plan))))
853
854def output_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
855 -valid: {Storage.bounds(depth, length) == True{} : Bool},
856 -exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
857 taken_left: Core.Dynamic & Array<F32>, taken_right: Core.Dynamic & Array<F32>) ->
858 Totality.Success<Elementwise.parallel_output(operation, plan, depth, length, valid, exact, taken_left, taken_right)>:
859 (kept_left, la) = taken_left
860 (kept_right, ra) = taken_right
861 Totality.Success{{==}}
862
863def parallel_allocated_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
864 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, -done: Allocation.TensorDone<Shape.output_shape(plan), result>) ->
865 Totality.Success<Elementwise.parallel_allocated(operation, plan, left, right, result)>:
866 match result:
867 case Fail{error}:
868 Totality.Success{Empty.absurd({False{} == True{} : Bool},
869 {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, Bool,
870 result => Result.is_done(&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>, result), Fail{error}, Done{tensor},
871 Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, Done{tensor}, Fail{error}, same)))} :
872 Allocation.TensorDone<Shape.output_shape(plan), Fail{error}> -> Empty}(done))}
873 case Done{Core.TTensor{storage, exact}}:
874 match storage:
875 case Storage.Empty{}:
876 Totality.Success{{==}}
877 case Storage.Owned{+depth, +length, array, balanced, valid}:
878 output_success(operation, plan, depth, length, valid, exact, Elementwise.take(left), Elementwise.take(right))
879
880def planned_success(+operation: Elementwise.Operation, +left_shape: Shape.Shape, +right_shape: Shape.Shape,
881 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, left: Core.Tensor<left_shape>, right: Core.Tensor<right_shape>,
882 -built: {ShapeLaws.broadcast_built(result) == True{} : Bool}) ->
883 Totality.Success<Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, result)>:
884 match result:
885 case Fail{error}:
886 Totality.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(built))}
887 case Done{+plan}:
888 parallel_allocated_success(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0),
889 AllocationProof.core_new_done(Shape.output_shape(plan), 0.0))
890
891def Laws.binary_valid_success(operation, left, right, output, compatible):
892 Core.Packed{+left_shape, left_tensor} = left
893 Core.Packed{+right_shape, right_tensor} = right
894 Totality.Compatible{+alignment, +rank, +capacity} = compatible
895 planned_success(operation, left_shape, right_shape, Shape.broadcast_checked(left_shape, right_shape), left_tensor, right_tensor,
896 PlanProof.broadcast_checked_complete(left_shape, right_shape, output, alignment, rank, capacity))