src/tensor/transform_LAWS.bend
bendtorch-core@0.1.0.0 · 508 lines · 57 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
4import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
5import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
6import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
7import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
8import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
9import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality
10import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
11
12law permutation_checked:
13 for +input: Shape.Shape
14 for +axes: List<&2, U32>
15 for plan: Layout.Plan<input, axes>
16 {True{} == Layout.bijective(input, axes) : Bool}
17
18law permutation_dimensions:
19 for +input: Shape.Shape
20 for +axes: List<&2, U32>
21 for +plan: Layout.Plan<input, axes>
22 {Some{Shape.dimensions(Layout.output(input, axes, plan))} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>}
23
24law permutation_count:
25 for +input: Shape.Shape
26 for +axes: List<&2, U32>
27 for +plan: Layout.Plan<input, axes>
28 {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}
29
30law mapped_inverse:
31 for -input: Shape.Shape
32 for -axes: List<&2, U32>
33 for -plan: Layout.Plan<input, axes>
34 for -i: U32
35 for +mapping: Layout.Mapping<input, axes, plan, i>
36 {Some{Layout.input_words(input, axes, plan, i, mapping)} ==
37 Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.output_words(input, axes, plan, i, mapping), 0) : Maybe<&2, List<&2, U32>>}
38
39law mapped_flat:
40 for -input: Shape.Shape
41 for -axes: List<&2, U32>
42 for -plan: Layout.Plan<input, axes>
43 for -i: U32
44 for +mapping: Layout.Mapping<input, axes, plan, i>
45 {Layout.source_index(input, axes, plan, i, mapping) ==
46 Layout.flatten_words(Shape.dimensions(input), Layout.input_words(input, axes, plan, i, mapping), 0) : U32}
47
48law mapped_output:
49 for -input: Shape.Shape
50 for -axes: List<&2, U32>
51 for -plan: Layout.Plan<input, axes>
52 for -i: U32
53 for mapping: Layout.Mapping<input, axes, plan, i>
54 {Layout.output_words(input, axes, plan, i, mapping) ==
55 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), i)) : List<&2, U32>}
56
57law mapped_bounded:
58 for -input: Shape.Shape
59 for -axes: List<&2, U32>
60 for -plan: Layout.Plan<input, axes>
61 for -i: U32
62 for mapping: Layout.Mapping<input, axes, plan, i>
63 {True{} == U32.is_lt(Layout.source_index(input, axes, plan, i, mapping), Shape.count(input)) : Bool}
64
65law inverse_coordinate_roundtrip:
66 for -input: Shape.Shape
67 for +axes: List<&2, U32>
68 for -plan: Layout.Plan<input, axes>
69 for -i: U32
70 for +mapping: Layout.Mapping<input, axes, plan, i>
71 {Layout.reorder(Layout.input_words(input, axes, plan, i, mapping), axes) ==
72 Some{Layout.output_words(input, axes, plan, i, mapping)} : Maybe<&2, List<&2, U32>>}
73
74law reshape_linear_order:
75 for +input: Shape.Shape
76 for +target: Shape.Shape
77 for tensor: Core.Tensor<input>
78 for +index: U32
79 for -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
80 {Transforms.dynamic_observe(Transforms.reshape_equal(input, target, tensor, same), index) ==
81 Core.observe(input, tensor, index) : Maybe<&2, F32>}
82
83law reshape_target_dimensions:
84 for +input: Shape.Shape
85 for +target: Shape.Shape
86 for tensor: Core.Tensor<input>
87 for -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
88 {Transforms.dynamic_dimensions(Transforms.reshape_equal(input, target, tensor, same)) == Shape.dimensions(target) : List<&2, U32>}
89
90law copy_input_preservation:
91 for +depth: Nat
92 for array: Array<F32>
93 for +index: U32
94 for +other: U32
95 for balanced: Model.Balanced(F32, depth, array)
96 {Model.observe(F32, depth, Refinement.first(F32, Array.get(F32, array, index)), Refinement.route(depth, other)) ==
97 Model.observe(F32, depth, array, Refinement.route(depth, other)) : Maybe<&2, F32>}
98
99law copy_write_frame:
100 for +depth: Nat
101 for array: Array<F32>
102 for +index: U32
103 for +other: U32
104 for +value: F32
105 for balanced: Model.Balanced(F32, depth, array)
106 {Model.observe(F32, depth, Array.set(F32, array, index, value), Refinement.route(depth, other)) ==
107 Model.select(F32, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), value,
108 Model.observe(F32, depth, array, Refinement.route(depth, other))) : Maybe<&2, F32>}
109
110law zero_count_skips_copy:
111 for +input: Shape.Shape
112 for +axes: List<&2, U32>
113 for +plan: Layout.Plan<input, axes>
114 for source: Core.Tensor<input>
115 for target: Core.Tensor<Layout.output(input, axes, plan)>
116 for +cursor: Nat
117 for empty: {Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) == 0n : Nat}
118 {Transforms.copy_loop(Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), input, axes, plan, source, target, cursor) ==
119 (source, Done{target}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>}
120
121law natural_cursor_checked:
122 for -input: Shape.Shape
123 for -axes: List<&2, U32>
124 for -plan: Layout.Plan<input, axes>
125 for -cursor: Nat
126 for result: Transforms.NaturalCopy<input, axes, plan, cursor>
127 Transforms.CursorValid(input, axes, plan, cursor, result)
128
129law copy_source_mapping:
130 for -input: Shape.Shape
131 for -axes: List<&2, U32>
132 for -plan: Layout.Plan<input, axes>
133 for -output_index: U32
134 for -mapping: Layout.Mapping<input, axes, plan, output_index>
135 for -source: Core.Tensor<input>
136 for certificate: Core.Read<input, source, Layout.source_index(input, axes, plan, output_index, mapping)>
137 {Core.read_value(input, Core.read_flat(input, source, Layout.source_index(input, axes, plan, output_index, mapping))) ==
138 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, output_index, mapping), certificate) : Maybe<&2, F32>}
139
140law primitive_source_mapping:
141 for -input: Shape.Shape
142 for -axes: List<&2, U32>
143 for -plan: Layout.Plan<input, axes>
144 for -output_index: U32
145 for +mapping: Layout.Mapping<input, axes, plan, output_index>
146 for +depth: Nat
147 for array: Array<F32>
148 for balanced: Model.Balanced(F32, depth, array)
149 {Some{Refinement.second(F32, Array.get(F32, array, Layout.source_index(input, axes, plan, output_index, mapping)))} ==
150 Model.observe(F32, depth, array, Refinement.route(depth, Layout.source_index(input, axes, plan, output_index, mapping))) : Maybe<&2, F32>}
151
152law copy_value_mapping:
153 for -input: Shape.Shape
154 for -axes: List<&2, U32>
155 for +plan: Layout.Plan<input, axes>
156 for +depth: Nat
157 for +length: Nat
158 for array: Array<F32>
159 for +index: U32
160 for source: Core.Tensor<input>
161 for +value: F32
162 for balanced: Model.Balanced(F32, depth, array)
163 for -valid: {Storage.bounds(depth, length) == True{} : Bool}
164 for -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}
165 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
166 for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
167 {Transforms.copy_observe(input, axes, plan,
168 Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}),
169 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, (source, Done{value})), index) == Some{value} : Maybe<&2, F32>}
170
171law checked_copy_step_mapping:
172 for +input: Shape.Shape
173 for +axes: List<&2, U32>
174 for +plan: Layout.Plan<input, axes>
175 for +index: U32
176 for +mapping: Layout.Mapping<input, axes, plan, index>
177 for map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}
178 for -source: Core.Tensor<input>
179 for certificate: Core.Read<input, source, Layout.source_index(input, axes, plan, index, mapping)>
180 for +depth: Nat
181 for +length: Nat
182 for array: Array<F32>
183 for balanced: Model.Balanced(F32, depth, array)
184 for -valid: {Storage.bounds(depth, length) == True{} : Bool}
185 for -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}
186 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
187 for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
188 {Transforms.copy_observe(input, axes, plan,
189 Transforms.copy_step(input, axes, plan, source,
190 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index), index) ==
191 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, index, mapping), certificate) : Maybe<&2, F32>}
192
193law checked_copy_source_meaning:
194 for +input: Shape.Shape
195 for +axes: List<&2, U32>
196 for +plan: Layout.Plan<input, axes>
197 for +index: U32
198 for +mapping: Layout.Mapping<input, axes, plan, index>
199 for map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}
200 for source: Core.Tensor<input>
201 for +depth: Nat
202 for +length: Nat
203 for array: Array<F32>
204 for balanced: Model.Balanced(F32, depth, array)
205 for -valid: {Storage.bounds(depth, length) == True{} : Bool}
206 for -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}
207 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
208 for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
209 Transforms.CopyMeaning<input, axes, plan, index, mapping, source,
210 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}>
211
212law initial_prefix:
213 for -input: Shape.Shape
214 for -axes: List<&2, U32>
215 for -plan: Layout.Plan<input, axes>
216 for -source: Core.Tensor<input>
217 for -target: Core.Tensor<Layout.output(input, axes, plan)>
218 Transforms.Prefix<input, axes, plan, source, source, target, 0n>
219
220law advance_prefix:
221 for -input: Shape.Shape
222 for -axes: List<&2, U32>
223 for -plan: Layout.Plan<input, axes>
224 for -original: Core.Tensor<input>
225 for -before_source: Core.Tensor<input>
226 for -after_source: Core.Tensor<input>
227 for -before_target: Core.Tensor<Layout.output(input, axes, plan)>
228 for -after_target: Core.Tensor<Layout.output(input, axes, plan)>
229 for -cursor: Nat
230 for prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>
231 for advanced: Transforms.Advanced<input, axes, plan, original, before_source, after_source, before_target, after_target, cursor>
232 Transforms.Prefix<input, axes, plan, original, after_source, after_target, 1n+cursor>
233
234law whole_copy_interpretation:
235 for +input: Shape.Shape
236 for +axes: List<&2, U32>
237 for +plan: Layout.Plan<input, axes>
238 for source: Core.Tensor<input>
239 for target: Core.Tensor<Layout.output(input, axes, plan)>
240 Transforms.WholeCopyModel<input, axes, plan, source, target>
241
242law permute_result_interpretation:
243 for +input: Shape.Shape
244 for source: Core.Tensor<input>
245 for +axes: List<&2, U32>
246 Transforms.PublicModel<input, axes, source, Transforms.permute_copy(input, source, axes)>
247
248law transpose_result_interpretation:
249 for +input: Shape.Shape
250 for source: Core.Tensor<input>
251 for +a: U32
252 for +b: U32
253 Transforms.PublicModel<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source,
254 Transforms.transpose_copy(input, source, a, b)>
255
256law reshape_result_interpretation:
257 for +input: Shape.Shape
258 for source: Core.Tensor<input>
259 for +dimensions: List<&2, U32>
260 Transforms.ReshapeModel<input, source, dimensions>
261
262law reshape_inverse_observations:
263 for +input: Shape.Shape
264 for source: Core.Tensor<input>
265 for +dimensions: List<&2, U32>
266 Transforms.ReshapeInverseModel<input, source, dimensions>
267
268law mapping_reference:
269 for +input: Shape.Shape
270 for +axes: List<&2, U32>
271 for +plan: Layout.Plan<input, axes>
272 for +index: U32
273 for mapping: Layout.Mapping<input, axes, plan, index>
274 {Some{Layout.source_index(input, axes, plan, index, mapping)} == Layout.reference_source(input, axes, plan, index) : Maybe<&2, U32>}
275
276law mapped_mathematical_bounded:
277 for +input: Shape.Shape
278 for +axes: List<&2, U32>
279 for +plan: Layout.Plan<input, axes>
280 for +index: U32
281 for mapping: Layout.Mapping<input, axes, plan, index>
282 {Nat.is_lt(U32.to_nat(Layout.source_index(input, axes, plan, index, mapping)),
283 Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}
284
285law natural_word_exact:
286 for +number: Nat
287 for +limit: U32
288 for +within: {Nat.is_le(number, U32.to_nat(limit)) == True{} : Bool}
289 {U32.to_nat(U32.from_nat(number)) == number : Nat}
290
291law codec_flatten_decode:
292 for +shape: Shape.Shape
293 for +index: U32
294 for +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}
295 {Layout.flatten_words(Shape.dimensions(shape),
296 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index)), 0) == index : U32}
297
298law reshape_valid_success:
299 for +input: Shape.Shape
300 for +target: Shape.Shape
301 for source: Core.Tensor<input>
302 for -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
303 Transforms.ReshapeSuccessModel<input, target, source>
304
305law reshape_inverse_valid_success:
306 for +input: Shape.Shape
307 for +target: Shape.Shape
308 for source: Core.Tensor<input>
309 for -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
310 Transforms.ReshapeInverseSuccessModel<input, target, source>
311
312law permutation_valid_success:
313 for +input: Shape.Shape
314 for +axes: List<&2, U32>
315 for +valid: {True{} == Layout.bijective(input, axes) : Bool}
316 Totality.PlanSuccess<input, axes>
317
318law tensor_read_valid_success:
319 for +shape: Shape.Shape
320 for source: Core.Tensor<shape>
321 for +index: U32
322 for -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
323 Totality.ReadSuccess<shape, source, index>
324
325law tensor_write_valid_success:
326 for +shape: Shape.Shape
327 for target: Core.Tensor<shape>
328 for +index: U32
329 for +value: F32
330 for -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
331 Totality.WriteSuccess<shape, target, index, value>
332
333law decoded_words_valid_success:
334 for +shape: Shape.Shape
335 for +index: U32
336 for +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}
337 Totality.WordsSuccess<Shape.dimensions(shape),
338 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index))>
339
340law permute_axes_length_rejection:
341 for +input: Shape.Shape
342 for source: Core.Tensor<input>
343 for +axes: List<&2, U32>
344 for -wrong: {False{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool}
345 Totality.PermuteFailure<input, axes, source, Layout.AxesLengthMismatch{}>
346
347law permute_axis_bounds_rejection:
348 for +input: Shape.Shape
349 for source: Core.Tensor<input>
350 for +axes: List<&2, U32>
351 for -ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool}
352 for -outside: {False{} == Layout.bounded(axes, Shape.rank(input)) : Bool}
353 Totality.PermuteFailure<input, axes, source, Layout.AxisOutOfBounds{}>
354
355law permute_duplicate_axes_rejection:
356 for +input: Shape.Shape
357 for source: Core.Tensor<input>
358 for +axes: List<&2, U32>
359 for -ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool}
360 for -bounded: {True{} == Layout.bounded(axes, Shape.rank(input)) : Bool}
361 for -duplicate: {False{} == Layout.unique(axes) : Bool}
362 Totality.PermuteFailure<input, axes, source, Layout.DuplicateAxis{}>
363
364law transpose_axis_bounds_rejection:
365 for +input: Shape.Shape
366 for source: Core.Tensor<input>
367 for +a: U32
368 for +b: U32
369 for -outside: {False{} == Transpose.valid(input, a, b) : Bool}
370 Totality.TransposeFailure<input, source, a, b>
371
372law reshape_element_count_rejection:
373 for +input: Shape.Shape
374 for +target: Shape.Shape
375 for source: Core.Tensor<input>
376 for -different: {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) : Bool}
377 Totality.ReshapeFailure<input, target, source>
378
379law mapping_index_rejection:
380 for +input: Shape.Shape
381 for +axes: List<&2, U32>
382 for +plan: Layout.Plan<input, axes>
383 for +index: U32
384 for +outside: {False{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}
385 {Layout.map_index(input, axes, plan, index) == Fail{Layout.ShapeError{Shape.FlatIndexOutOfBounds{}}} :
386 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}
387
388law codec_decode_flatten:
389 for +shape: Shape.Shape
390 for +values: List<&2, U32>
391 for +valid: Layout.WordsValid(Shape.dimensions(shape), values)
392 {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)),
393 Layout.flatten_words(Shape.dimensions(shape), values, 0))) == values : List<&2, U32>}
394
395law mapping_valid_success:
396 for +input: Shape.Shape
397 for +axes: List<&2, U32>
398 for +plan: Layout.Plan<input, axes>
399 for +index: U32
400 for +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}
401 Totality.MappingSuccess<input, axes, plan, index>
402
403law natural_cursor_exact_conversion:
404 for +shape: Shape.Shape
405 for +cursor: Nat
406 for +within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}
407 Transforms.CursorExact<cursor, U32.from_nat(cursor)>
408
409law copy_step_valid_success:
410 for +input: Shape.Shape
411 for +axes: List<&2, U32>
412 for +plan: Layout.Plan<input, axes>
413 for source: Core.Tensor<input>
414 for target: Core.Tensor<Layout.output(input, axes, plan)>
415 for +index: U32
416 for +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}
417 Totality.CopyStepSuccess<input, axes, plan, source, target, index>
418
419law natural_step_valid_success:
420 for +input: Shape.Shape
421 for +axes: List<&2, U32>
422 for +plan: Layout.Plan<input, axes>
423 for +cursor: Nat
424 for source: Core.Tensor<input>
425 for target: Core.Tensor<Layout.output(input, axes, plan)>
426 for +inside: {True{} == Nat.is_lt(cursor, Shape.elements(Layout.output(input, axes, plan))) : Bool}
427 Totality.NaturalSuccess<input, axes, plan, cursor, Transforms.natural_step(input, axes, plan, cursor, source, target)>
428
429law copy_loop_valid_success:
430 for +fuel: Nat
431 for +input: Shape.Shape
432 for +axes: List<&2, U32>
433 for +plan: Layout.Plan<input, axes>
434 for +cursor: Nat
435 for source: Core.Tensor<input>
436 for target: Core.Tensor<Layout.output(input, axes, plan)>
437 for +within: {Nat.is_le(Nat.add(fuel, cursor), Shape.elements(Layout.output(input, axes, plan))) == True{} : Bool}
438 Totality.CopySuccess<input, axes, plan, Transforms.copy_loop(fuel, input, axes, plan, source, target, cursor)>
439
440law permute_valid_success:
441 for +input: Shape.Shape
442 for source: Core.Tensor<input>
443 for +axes: List<&2, U32>
444 for +valid: {True{} == Layout.bijective(input, axes) : Bool}
445 Totality.PublicSuccess<input, Transforms.permute_copy(input, source, axes)>
446
447law inverse_axes_valid:
448 for +input: Shape.Shape
449 for +axes: List<&2, U32>
450 for +plan: Layout.Plan<input, axes>
451 {True{} == Layout.bijective(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)) : Bool}
452
453law inverse_permutation_dimensions:
454 for +input: Shape.Shape
455 for +axes: List<&2, U32>
456 for +plan: Layout.Plan<input, axes>
457 for +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>
458 {Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)) == Shape.dimensions(input) : List<&2, U32>}
459
460law inverse_mapping_restores_index:
461 for +input: Shape.Shape
462 for +axes: List<&2, U32>
463 for +plan: Layout.Plan<input, axes>
464 for +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>
465 for +index: U32
466 for +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>
467 for +first: Layout.Mapping<input, axes, plan,
468 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>
469 {Layout.source_index(input, axes, plan,
470 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first) == index : U32}
471
472law permute_typed_success:
473 for +input: Shape.Shape
474 for source: Core.Tensor<input>
475 for +axes: List<&2, U32>
476 for +valid: {True{} == Layout.bijective(input, axes) : Bool}
477 Totality.TypedPermutation<input, axes, source, Transforms.permute_copy(input, source, axes)>
478
479law permute_inverse_restoration:
480 for +input: Shape.Shape
481 for source: Core.Tensor<input>
482 for +axes: List<&2, U32>
483 for +valid: {True{} == Layout.bijective(input, axes) : Bool}
484 Totality.PermutationInverse<input, axes, source>
485
486law transpose_valid_success:
487 for +input: Shape.Shape
488 for source: Core.Tensor<input>
489 for +a: U32
490 for +b: U32
491 for +inside: {True{} == Transpose.valid(input, a, b) : Bool}
492 Totality.PublicSuccess<input, Transforms.transpose_copy(input, source, a, b)>
493
494law transpose_requested_result:
495 for +input: Shape.Shape
496 for source: Core.Tensor<input>
497 for +a: U32
498 for +b: U32
499 for +inside: {True{} == Transpose.valid(input, a, b) : Bool}
500 Totality.RequestedTranspose<input, source, a, b>
501
502law transpose_inverse_restoration:
503 for +input: Shape.Shape
504 for source: Core.Tensor<input>
505 for +a: U32
506 for +b: U32
507 for +inside: {True{} == Transpose.valid(input, a, b) : Bool}
508 Totality.TransposeInverse<input, source, a, b>