1	import Base
2	import ../shape/core.bend as Shape
3	import ./layout.bend as Layout
4	import ./core.bend as Core
5	import ./transforms.bend as Transforms
6	import ../storage/main.bend as Storage
7	import ../storage/model.bend as Model
8	import ../storage/refinement.bend as Refinement
9	import ./transform_totality.bend as Totality
10	import ./transpose_spec.bend as Transpose
11	
12	law 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	
18	law 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	
24	law 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	
30	law 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	
39	law 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	
48	law 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	
57	law 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	
65	law 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	
74	law 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	
83	law 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	
90	law 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	
99	law 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	
110	law 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	
121	law 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	
129	law 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	
140	law 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	
152	law 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	
171	law 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	
193	law 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	
212	law 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	
220	law 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	
234	law 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	
242	law 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	
248	law 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	
256	law 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	
262	law 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	
268	law 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	
276	law 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	
285	law 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	
291	law 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	
298	law 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	
305	law 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	
312	law 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	
318	law 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	
325	law 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	
333	law 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	
340	law 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	
347	law 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	
355	law 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	
364	law 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	
372	law 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	
379	law 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	
388	law 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	
395	law 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	
403	law 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	
409	law 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	
419	law 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	
429	law 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	
440	law 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	
447	law 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	
453	law 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	
460	law 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	
472	law 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	
479	law 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	
486	law 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	
494	law 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	
502	law 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>