src/tensor/transform_PROOF.bend
bendtorch-core@0.1.0.0 · 2,553 lines · 178 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/transform_LAWS.bend as Laws
5import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
6import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
7import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
8import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
9import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
10import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
11import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
12import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
13import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
14import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
15import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
16import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
17import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
18import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
19import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as ShapeIndex
20import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
21import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
22import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
23import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
24import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality
25import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping
26import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
27import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as AllocationSpec
28import bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend as TransposeProof
29import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec
30import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuild
31
32def Laws.permutation_checked(input, axes, plan):
33 Mapping.permutation_checked(input, axes, plan)
34
35def Laws.permutation_dimensions(input, axes, plan):
36 Layout.Permutation{out, valid, ordered, count} = plan
37 ordered
38
39def Laws.permutation_count(input, axes, plan):
40 Layout.Permutation{out, valid, ordered, count} = plan
41 Transforms.elements_equal(input, out, count)
42
43def Laws.mapped_inverse(input, axes, plan, i, mapping):
44 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping
45 inverse
46
47def Laws.mapped_flat(input, axes, plan, i, mapping):
48 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping
49 flattened
50
51def Laws.mapped_output(input, axes, plan, i, mapping):
52 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping
53 decoded
54
55def Laws.mapped_bounded(input, axes, plan, i, mapping):
56 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping
57 Layout.FIndex{value, bound} = index
58 bound
59
60def bit_equal(a: Bool, b: Bool, equal: {True{} == Bool.not(Bool.xor(a, b)) : Bool}) -> {a == b : Bool}:
61 match a b:
62 case False{} False{}:
63 {==}
64 case True{} True{}:
65 {==}
66 case False{} True{}:
67 Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(equal))
68 case True{} False{}:
69 Empty.absurd({True{} == False{} : Bool}, Lifecycle.false_true(equal))
70
71def word_equal(+n: Nat, +a: Word(n), +b: Word(n),
72 +equal: {True{} == Layout.word_same(n, a, b) : Bool}) -> {a == b : Word(n)}:
73 match n:
74 case 0n:
75 match a b:
76 case WNil{} WNil{}:
77 {==}
78 case 1n++p:
79 WCon{+ab, +at} = a
80 WCon{+bb, +bt} = b
81 %bit_equal(ab, bb, Mapping.and_left(Bool.not(Bool.xor(ab, bb)), Layout.word_same(p, at, bt), equal)) :
82 {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
83 %word_equal(p, at, bt, Mapping.and_right(Bool.not(Bool.xor(ab, bb)), Layout.word_same(p, at, bt), equal)) :
84 {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
85 {==}
86
87def word_value_equal(+a: U32, +b: U32, equal: {True{} == Layout.word_value_same(a, b) : Bool}) -> {a == b : U32}:
88 match a b:
89 case U32{x} U32{y}:
90 Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_equal(32n, x, y, equal))
91
92def words_equal(+a: List<&2, U32>, +b: List<&2, U32>,
93 +equal: {True{} == Layout.words_same(a, b) : Bool}) -> {a == b : List<&2, U32>}:
94 match a b:
95 case Nil{} Nil{}:
96 {==}
97 case +ah <> +at +bh <> +bt:
98 %word_value_equal(ah, bh, Mapping.and_left(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
99 {ah <> at == _ <> bt : List<&2, U32>}
100 %words_equal(at, bt, Mapping.and_right(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
101 {ah <> at == ah <> _ : List<&2, U32>}
102 {==}
103 case Nil{} bh <> bt:
104 Empty.absurd({Nil{} == bh <> bt : List<&2, U32>}, Lifecycle.false_true(equal))
105 case ah <> at Nil{}:
106 Empty.absurd({ah <> at == Nil{} : List<&2, U32>}, Lifecycle.false_true(equal))
107
108def maybe_equal(+a: Maybe<&2, List<&2, U32>>, +b: Maybe<&2, List<&2, U32>>,
109 equal: {True{} == Layout.maybe_same(a, b) : Bool}) -> {a == b : Maybe<&2, List<&2, U32>>}:
110 match a b:
111 case None{} None{}:
112 {==}
113 case Some{xs} Some{ys}:
114 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, xs => Some{xs}, xs, ys, words_equal(xs, ys, equal))
115 case None{} Some{ys}:
116 Empty.absurd({None{} == Some{ys} : Maybe<&2, List<&2, U32>>}, Lifecycle.false_true(equal))
117 case Some{xs} None{}:
118 Empty.absurd({Some{xs} == None{} : Maybe<&2, List<&2, U32>>}, Lifecycle.false_true(equal))
119
120def Laws.inverse_coordinate_roundtrip(input, axes, plan, i, mapping):
121 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping
122 maybe_equal(Layout.reorder(Layout.coordinate_values(input, ic), axes),
123 Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}, roundtrip)
124
125def Laws.reshape_linear_order(input, target, tensor, index, same):
126 Core.TTensor{storage, valid} = tensor
127 {==}
128
129def Laws.reshape_target_dimensions(input, target, tensor, same):
130 Core.TTensor{storage, valid} = tensor
131 {==}
132
133def Laws.copy_input_preservation(depth, array, index, other, balanced):
134 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, other)),
135 Refinement.first(F32, Array.get(F32, array, index)), array,
136 Refinement.law_get_retains(F32, depth, array, index, balanced))
137
138def Laws.copy_write_frame(depth, array, index, other, value, balanced):
139 StorageLaws.primitive_update_frame(F32, depth, array, index, Refinement.route(depth, other), value, balanced)
140
141def Laws.zero_count_skips_copy(input, axes, plan, source, target, cursor, empty):
142 %Equal.sym(Nat, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), 0n, empty) :
143 {Transforms.copy_loop(_, input, axes, plan, source, target, cursor) ==
144 (source, Done{target}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>}
145 {==}
146
147def Laws.natural_cursor_checked(input, axes, plan, cursor, result):
148 match result:
149 case Transforms.NaturalCopied{pair, index, exact, candidate}:
150 Transforms.CursorExact{exact}
151 case Transforms.NaturalError{source}:
152 Unit{}
153
154def Laws.copy_source_mapping(input, axes, plan, output_index, mapping, source, certificate):
155 Core.Read{tensor, result, exact} = certificate
156 %exact : {Core.read_value(input, _) == Core.result_value(result) : Maybe<&2, F32>}
157 {==}
158
159def Laws.primitive_source_mapping(input, axes, plan, output_index, mapping, depth, array, balanced):
160 Refinement.law_get_refines(F32, depth, array, Layout.source_index(input, axes, plan, output_index, mapping), balanced)
161
162def copy_checked_mapping(-input: Shape.Shape, -axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
163 +depth: Nat, +length: Nat, array: Array<F32>, +index: U32, source: Core.Tensor<input>, +value: F32,
164 balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
165 -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, allowed: Bool,
166 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
167 -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
168 Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
169 accepted: {allowed == True{} : Bool}) ->
170 {Transforms.copy_observe(input, axes, plan,
171 Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), source,
172 Core.write_result(Layout.output(input, axes, plan), Storage.Owned{depth, length, array, balanced, valid}, exact, index, value,
173 Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid), same)), index) == Some{value} : Maybe<&2, F32>}:
174 match allowed:
175 case False{}:
176 Empty.absurd({Transforms.copy_observe(input, axes, plan,
177 Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), source,
178 Core.write_result(Layout.output(input, axes, plan), Storage.Owned{depth, length, array, balanced, valid}, exact, index, value,
179 Storage.set_checked(depth, length, array, index, value, False{}, decision, balanced, valid), same)), index) == Some{value} : Maybe<&2, F32>},
180 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
181 case True{}:
182 StorageLaws.primitive_write_read(F32, depth, array, index, value, balanced)
183
184def Laws.copy_value_mapping(input, axes, plan, depth, length, array, index, source, value, balanced, valid, exact, allowed, matched):
185 copy_checked_mapping(input, axes, plan, depth, length, array, index, source, value, balanced, valid, exact,
186 Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
187
188def copy_result_mapping(-input: Shape.Shape, -axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
189 +depth: Nat, +length: Nat, array: Array<F32>, +index: U32, source: Core.Tensor<input>,
190 result: Result<&2, &2, Core.Error, F32>, balanced: Model.Balanced(F32, depth, array),
191 -valid: {Storage.bounds(depth, length) == True{} : Bool},
192 -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat},
193 allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
194 {Transforms.copy_observe(input, axes, plan,
195 Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}),
196 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, (source, result)), index) ==
197 Core.result_value(result) : Maybe<&2, F32>}:
198 match result:
199 case Fail{error}:
200 {==}
201 case Done{value}:
202 copy_checked_mapping(input, axes, plan, depth, length, array, index, source, value, balanced, valid, exact,
203 Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
204
205def Laws.checked_copy_step_mapping(input, axes, plan, index, mapping, map_exact, source, certificate,
206 depth, length, array, balanced, valid, exact, allowed, matched):
207 Core.Read{retained, result, read_exact} = certificate
208 %map_exact :
209 {Transforms.copy_observe(input, axes, plan,
210 Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source,
211 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, _), index) ==
212 Core.result_value(result) : Maybe<&2, F32>}
213 %read_exact :
214 {Transforms.copy_observe(input, axes, plan,
215 Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}),
216 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, _), index) ==
217 Core.result_value(result) : Maybe<&2, F32>}
218 copy_result_mapping(input, axes, plan, depth, length, array, index, retained, result, balanced, valid, exact, allowed)
219
220def copy_meaning_from_read(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
221 -mapping: Layout.Mapping<input, axes, plan, index>, -source: Core.Tensor<input>,
222 -target: Core.Tensor<Layout.output(input, axes, plan)>,
223 -read: Core.Read<input, source, Layout.source_index(input, axes, plan, index, mapping)>,
224 -copied: {Transforms.copy_observe(input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index), index) ==
225 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, index, mapping), read) : Maybe<&2, F32>},
226 -read_exact: {Core.read_value(input, Core.read_flat(input, source, Layout.source_index(input, axes, plan, index, mapping))) ==
227 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, index, mapping), read) : Maybe<&2, F32>},
228 model: Core.SourceRead<input, source, Layout.source_index(input, axes, plan, index, mapping)>) ->
229 Transforms.CopyMeaning<input, axes, plan, index, mapping, source, target>:
230 Core.SourceRead{meaning} = model
231 Transforms.CopyMeaning{Equal.trans(Maybe<&2, F32>,
232 Transforms.copy_observe(input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index), index),
233 Core.read_value(input, Core.read_flat(input, source, Layout.source_index(input, axes, plan, index, mapping))),
234 Core.checked_observe(input, source, Layout.source_index(input, axes, plan, index, mapping)),
235 Equal.trans(Maybe<&2, F32>,
236 Transforms.copy_observe(input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index), index),
237 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, index, mapping), read),
238 Core.read_value(input, Core.read_flat(input, source, Layout.source_index(input, axes, plan, index, mapping))), copied,
239 Equal.sym(Maybe<&2, F32>,
240 Core.read_value(input, Core.read_flat(input, source, Layout.source_index(input, axes, plan, index, mapping))),
241 Core.certificate_value(input, source, Layout.source_index(input, axes, plan, index, mapping), read), read_exact)), meaning)}
242
243def Laws.checked_copy_source_meaning(input, axes, plan, index, mapping, map_exact, source,
244 depth, length, array, balanced, valid, exact, allowed, matched):
245 -read = Core.read_certificate(input, source, Layout.source_index(input, axes, plan, index, mapping))
246 copy_meaning_from_read(input, axes, plan, index, mapping, source,
247 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, read,
248 Laws.checked_copy_step_mapping(input, axes, plan, index, mapping, map_exact, source, read,
249 depth, length, array, balanced, valid, exact, allowed, matched),
250 Laws.copy_source_mapping(input, axes, plan, index, mapping, source, read),
251 Core.source_read_model(input, source, Layout.source_index(input, axes, plan, index, mapping)))
252
253def lt_zero_false(a: Nat) -> {Nat.is_lt(a, 0n) == False{} : Bool}:
254 match a:
255 case 0n:
256 {==}
257 case 1n+p:
258 {==}
259
260def earlier_zero_false(+other: Nat, earlier: {Nat.is_lt(other, 0n) == True{} : Bool}) -> Empty:
261 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_lt(other, 0n), False{},
262 Equal.sym(Bool, Nat.is_lt(other, 0n), True{}, earlier), lt_zero_false(other)))
263
264def Laws.initial_prefix(input, axes, plan, source, target):
265 Transforms.Prefix{other => {==},
266 other => earlier => Empty.absurd({U32.to_nat(U32.from_nat(other)) == other : Nat}, earlier_zero_false(other, earlier)),
267 other => earlier => Empty.absurd(Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(other)),
268 earlier_zero_false(other, earlier)),
269 other => earlier => Empty.absurd({Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) ==
270 Transforms.expected_output(input, axes, plan, source, U32.from_nat(other)) : Maybe<&2, F32>}, earlier_zero_false(other, earlier))}
271
272def earlier_lift(-a: Nat, -b: Nat,
273 result: Either<&2, &2, {Nat.is_lt(a, b) == True{} : Bool}, {a == b : Nat}>) ->
274 Either<&2, &2, {Nat.is_lt(1n+a, 1n+b) == True{} : Bool}, {1n+a == 1n+b : Nat}>:
275 match result:
276 case Inl{earlier}:
277 Inl{earlier}
278 case Inr{equal}:
279 Inr{Equal.cong(Nat, Nat, n => 1n+n, a, b, equal)}
280
281def earlier_split(+a: Nat, +b: Nat, earlier: {Nat.is_lt(a, 1n+b) == True{} : Bool}) ->
282 Either<&2, &2, {Nat.is_lt(a, b) == True{} : Bool}, {a == b : Nat}>:
283 match a b:
284 case 0n 0n:
285 Inr{{==}}
286 case 0n 1n+q:
287 Inl{{==}}
288 case 1n+p 0n:
289 Empty.absurd(Either<&2, &2, {Nat.is_lt(1n+p, 0n) == True{} : Bool}, {1n+p == 0n : Nat}>,
290 earlier_zero_false(p, earlier))
291 case 1n+p 1n+q:
292 earlier_lift(p, q, earlier_split(p, q, earlier))
293
294def prefix_words_case(-cursor: Nat, +other: Nat,
295 prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} -> {U32.to_nat(U32.from_nat(j)) == j : Nat},
296 current: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
297 split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
298 {U32.to_nat(U32.from_nat(other)) == other : Nat}:
299 match split:
300 case Inl{earlier}:
301 prior(other, earlier)
302 case Inr{equal}:
303 %Equal.sym(Nat, other, cursor, equal) : {U32.to_nat(U32.from_nat(_)) == _ : Nat}
304 current
305
306def prefix_written_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>,
307 -original: Core.Tensor<input>, -before: Core.Tensor<Layout.output(input, axes, plan)>, -after: Core.Tensor<Layout.output(input, axes, plan)>,
308 -cursor: Nat, +other: Nat,
309 prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
310 {Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) ==
311 Transforms.expected_output(input, axes, plan, original, U32.from_nat(j)) : Maybe<&2, F32>},
312 current: {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(cursor)) ==
313 Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
314 frame: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
315 {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(j)) ==
316 Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(j)) : Maybe<&2, F32>},
317 split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
318 {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)) ==
319 Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)) : Maybe<&2, F32>}:
320 match split:
321 case Inl{+earlier}:
322 Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(other)),
323 Core.checked_observe(Layout.output(input, axes, plan), before, U32.from_nat(other)),
324 Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)), frame(other, earlier), prior(other, earlier))
325 case Inr{equal}:
326 %Equal.sym(Nat, other, cursor, equal) : {Core.checked_observe(Layout.output(input, axes, plan), after, U32.from_nat(_)) ==
327 Transforms.expected_output(input, axes, plan, original, U32.from_nat(_)) : Maybe<&2, F32>}
328 current
329
330def prefix_checked_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>,
331 -target: Core.Tensor<Layout.output(input, axes, plan)>, -cursor: Nat, +other: Nat,
332 prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
333 Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(j)),
334 current: Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(cursor)),
335 split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
336 Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(other)):
337 match split:
338 case Inl{earlier}:
339 prior(other, earlier)
340 case Inr{equal}:
341 %Equal.sym(Nat, other, cursor, equal) : Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(_))
342 current
343
344def Laws.advance_prefix(input, axes, plan, original, before_source, after_source, before_target, after_target, cursor, prefix, advanced):
345 Transforms.Prefix{source_prior, words_prior, checked_prior, written_prior} = prefix
346 Transforms.Advanced{word_exact, source_kept, current, current_checked, past_checked, frame} = advanced
347 Transforms.Prefix{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(input, after_source, other),
348 Core.checked_observe(input, before_source, other), Core.checked_observe(input, original, other),
349 source_kept(other), source_prior(other)),
350 other => earlier => prefix_words_case(cursor, other, words_prior, word_exact, earlier_split(other, cursor, earlier)),
351 other => earlier => prefix_checked_case(input, axes, plan, after_target, cursor, other,
352 past_checked, current_checked, earlier_split(other, cursor, earlier)),
353 other => earlier => prefix_written_case(input, axes, plan, original, before_target, after_target, cursor, other,
354 written_prior, current, frame, earlier_split(other, cursor, earlier))}
355
356def route_allowed(+depth: Nat, +length: Nat, +index: U32,
357 +matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
358 {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
359 +offset = Model.offset(depth, Refinement.route(depth, index))
360 %Lifecycle.natural_equal(offset, U32.to_nat(index),
361 Mapping.and_left(Nat.is_eq(offset, U32.to_nat(index)), Nat.is_lt(offset, length),
362 Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched))) :
363 {Nat.is_lt(_, length) == True{} : Bool}
364 Equal.sym(Bool, True{}, Nat.is_lt(offset, length),
365 Mapping.and_right(Nat.is_eq(offset, U32.to_nat(index)), Nat.is_lt(offset, length),
366 Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched)))
367
368def observe_index_equal(+depth: Nat, -length: Nat, -array: Array<F32>, +index: U32, matched: Bool,
369 accepted: {matched == True{} : Bool}) ->
370 {Lifecycle.observe_index(depth, length, array, index, matched) ==
371 Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}:
372 match matched:
373 case False{}:
374 Empty.absurd({None{} == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>},
375 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
376 case True{}:
377 {==}
378
379def observe_allowed_equal(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
380 accepted: {allowed == True{} : Bool}, matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
381 {Lifecycle.observe_allowed(depth, length, array, index, allowed) ==
382 Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}:
383 match allowed:
384 case False{}:
385 Empty.absurd({None{} == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>},
386 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
387 case True{}:
388 observe_index_equal(depth, length, array, index, Storage.index_matches(depth, length, index), matched)
389
390type ObserveBridge<-shape: Shape.Shape, -tensor: Core.Tensor<shape>, -index: U32> is Data:
391 ObserveBridge{-equal: {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}}
392
393def observe_bridge(-shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
394 checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index)) -> ObserveBridge<shape, tensor, index>:
395 Core.TTensor{storage, exact} = tensor
396 match storage:
397 case Storage.Empty{}:
398 ObserveBridge{{==}}
399 case Storage.Owned{+depth, +length, array, balanced, valid}:
400 ObserveBridge{observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
401 route_allowed(depth, length, index, checked), checked)}
402
403type ReadInfo<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32> is Type:
404 ReadInfo{owner: Core.Tensor<shape>, same: {owner == original : Core.Tensor<shape>},
405 -source: Core.SourceRead<shape, original, index>, -kept: Core.SourceReadKeeps<shape, original, index>}
406
407def read_info(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32) -> ReadInfo<shape, original, index>:
408 ReadInfo{original, {==}, Core.source_read_model(shape, original, index), Core.source_read_keeps(shape, original, index)}
409
410type TargetInfo<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32> is Type:
411 TargetInfo{owner: Core.Tensor<shape>, same: {owner == original : Core.Tensor<shape>},
412 -model: Core.CheckedUpdateModel<shape, original, index, value>}
413
414def target_info(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> TargetInfo<shape, original, index, value>:
415 TargetInfo{original, {==}, CoreProof.checked_update_model(shape, original, index, value)}
416
417def read_rebased(-shape: Shape.Shape, -original: Core.Tensor<shape>, -owner: Core.Tensor<shape>, +index: U32,
418 same: {owner == original : Core.Tensor<shape>}, certificate: Core.Read<shape, owner, index>) -> Core.Read<shape, original, index>:
419 Core.Read{tensor, result, exact} = certificate
420 Core.Read{tensor, result, Equal.trans(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, (tensor, result),
421 Core.read_flat(shape, owner, index), Core.read_flat(shape, original, index), exact,
422 Equal.cong(Core.Tensor<shape>, Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, t => Core.read_flat(shape, t, index), owner, original, same))}
423
424type SourceValue<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32> is Data:
425 SourceValue{-equal: {Core.checked_observe(shape, original, index) == Some{value} : Maybe<&2, F32>}}
426
427def source_value(-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>, +index: U32, +value: F32,
428 -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
429 certificate: Core.SourceRead<shape, original, index>) -> SourceValue<shape, original, index, value>:
430 Core.SourceRead{meaning} = certificate
431 SourceValue{Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, original, index),
432 Core.read_value(shape, Core.read_flat(shape, original, index)), Some{value},
433 Equal.sym(Maybe<&2, F32>, Core.read_value(shape, Core.read_flat(shape, original, index)), Core.checked_observe(shape, original, index), meaning),
434 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
435 Core.read_flat(shape, original, index), (retained, Done{value}),
436 Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, (retained, Done{value}), Core.read_flat(shape, original, index), exact)))}
437
438type SourceKept<-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>> is Data:
439 SourceKept{-kept: Transforms.SameSource(shape, original, retained)}
440
441def source_kept(-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>, +index: U32, -value: F32,
442 -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
443 certificate: Core.SourceReadKeeps<shape, original, index>) -> SourceKept<shape, original, retained>:
444 Core.SourceReadKeeps{kept} = certificate
445 SourceKept{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, retained, other),
446 Core.retained_read_observe(shape, Core.read_flat(shape, original, index), other), Core.checked_observe(shape, original, other),
447 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
448 (retained, Done{value}), Core.read_flat(shape, original, index), exact), kept(other))}
449
450type MappedValue<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
451 -original: Core.Tensor<input>, -value: F32> is Data:
452 MappedValue{-equal: {Some{value} == Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}}
453
454def mapped_value(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
455 -original: Core.Tensor<input>, +mapping: Layout.Mapping<input, axes, plan, index>, +value: F32,
456 -exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
457 certificate: SourceValue<input, original, Layout.source_index(input, axes, plan, index, mapping), value>) ->
458 MappedValue<input, axes, plan, index, original, value>:
459 SourceValue{equal} = certificate
460 MappedValue{
461 %exact : {Some{value} == Transforms.expected_mapped(input, axes, plan, index, original, _) : Maybe<&2, F32>}
462 Equal.sym(Maybe<&2, F32>, Core.checked_observe(input, original, Layout.source_index(input, axes, plan, index, mapping)), Some{value}, equal)}
463
464type KnownCheckedUpdate<-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32,
465 -value: F32, -unit: Unit> is Data:
466 KnownCheckedUpdate{-meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))}
467
468def known_checked_update(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +index: U32,
469 +value: F32, -unit: Unit,
470 -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
471 certificate: Core.CheckedUpdateModel<shape, original, index, value>) -> KnownCheckedUpdate<shape, original, output, index, value, unit>:
472 Core.CheckedUpdateModel{meaning} = certificate
473 KnownCheckedUpdate{
474 %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (output, Done{unit}), Core.write_flat(shape, original, index, value), exact) :
475 Core.CheckedUpdateMeaning(shape, original, index, value, _)
476 meaning}
477
478def checked_update_route(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32,
479 -value: F32, -unit: Unit, meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
480 Core.ObservationChecked(Core.Packed{shape, output}, index):
481 (checked, rest) = meaning
482 checked
483
484def checked_update_value(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32,
485 -value: F32, -unit: Unit, meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
486 {Core.checked_observe(shape, output, index) == Some{value} : Maybe<&2, F32>}:
487 (checked, rest) = meaning
488 (observed, frame) = rest
489 observed
490
491def checked_update_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32,
492 -value: F32, -unit: Unit, meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
493 @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
494 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
495 Core.ObservationChecked(Core.Packed{shape, output}, other) &
496 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}:
497 (checked, rest) = meaning
498 (observed, frame) = rest
499 frame
500
501type SuccessfulStep<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
502 -original_source: Core.Tensor<input>, -original_target: Core.Tensor<Layout.output(input, axes, plan)>,
503 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>> is Data:
504 SuccessfulStep{-meaning: Transforms.StepMeaning(input, axes, plan, index, original_source, original_target, (source, Done{target}))}
505
506def successful_step(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
507 -original_source: Core.Tensor<input>, -original_target: Core.Tensor<Layout.output(input, axes, plan)>,
508 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, +mapping: Layout.Mapping<input, axes, plan, index>,
509 +value: F32, -unit: Unit,
510 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
511 read_value: SourceValue<input, original_source, Layout.source_index(input, axes, plan, index, mapping), value>,
512 read_kept: SourceKept<input, original_source, source>,
513 update: KnownCheckedUpdate<Layout.output(input, axes, plan), original_target, target, index, value, unit>) ->
514 SuccessfulStep<input, axes, plan, index, original_source, original_target, source, target>:
515 SourceValue{read_equal} = read_value
516 SourceKept{kept} = read_kept
517 KnownCheckedUpdate{meaning} = update
518 SuccessfulStep{(kept,
519 (checked_update_route(Layout.output(input, axes, plan), original_target, target, index, value, unit, meaning),
520 (Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), target, index), Some{value},
521 Transforms.expected_output(input, axes, plan, original_source, index),
522 checked_update_value(Layout.output(input, axes, plan), original_target, target, index, value, unit, meaning),
523 {\{MappedValue: equal => equal} : MappedValue<input, axes, plan, index, original_source, value> ->
524 {Some{value} == Transforms.expected_output(input, axes, plan, original_source, index) : Maybe<&2, F32>}}(
525 mapped_value(input, axes, plan, index, original_source, mapping, value, map_exact, SourceValue{read_equal}))),
526 checked_update_frame(Layout.output(input, axes, plan), original_target, target, index, value, unit, meaning))))}
527
528def step_write_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
529 -original_source: Core.Tensor<input>, -original_target: Core.Tensor<Layout.output(input, axes, plan)>,
530 +mapping: Layout.Mapping<input, axes, plan, index>, +value: F32,
531 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
532 certificate: Core.Write<Layout.output(input, axes, plan), original_target, index, value>,
533 retained: Core.Tensor<input>,
534 lift: @-pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>> ->
535 {pair == Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained,
536 Core.write_flat(Layout.output(input, axes, plan), original_target, index, value)) :
537 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>} ->
538 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) :
539 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
540 -read_exact: {(retained, Done{value}) == Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)) :
541 Core.Tensor<input> & Result<&2, &2, Core.Error, F32>},
542 -read_model: Core.SourceRead<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>,
543 -keep_model: Core.SourceReadKeeps<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>,
544 -write_model: Core.CheckedUpdateModel<Layout.output(input, axes, plan), original_target, index, value>) ->
545 Transforms.StepCertificate<input, axes, plan, index, original_source, original_target>:
546 Core.Write{target, result, exact} = certificate
547 match result:
548 case Fail{error}:
549 Transforms.StepCertificate{(retained, Fail{Transforms.TensorError{error}}),
550 lift((retained, Fail{Transforms.TensorError{error}}),
551 Equal.cong(Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &2, Core.Error, Unit>,
552 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
553 pair => Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained, pair),
554 (target, Fail{error}), Core.write_flat(Layout.output(input, axes, plan), original_target, index, value), exact)), Unit{}}
555 case Done{unit}:
556 Transforms.StepCertificate{(retained, Done{target}),
557 lift((retained, Done{target}),
558 Equal.cong(Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &2, Core.Error, Unit>,
559 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
560 pair => Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained, pair),
561 (target, Done{unit}), Core.write_flat(Layout.output(input, axes, plan), original_target, index, value), exact)),
562 {\{SuccessfulStep: meaning => meaning} : SuccessfulStep<input, axes, plan, index, original_source, original_target, retained, target> ->
563 Transforms.StepMeaning(input, axes, plan, index, original_source, original_target, (retained, Done{target}))}(
564 successful_step(input, axes, plan, index, original_source, original_target, retained, target, mapping, value, unit, map_exact,
565 source_value(input, original_source, retained, Layout.source_index(input, axes, plan, index, mapping), value, read_exact, read_model),
566 source_kept(input, original_source, retained, Layout.source_index(input, axes, plan, index, mapping), value, read_exact, keep_model),
567 known_checked_update(Layout.output(input, axes, plan), original_target, target, index, value, unit, exact, write_model)))}
568
569def step_target_info(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
570 -original_source: Core.Tensor<input>, -original_target: Core.Tensor<Layout.output(input, axes, plan)>,
571 +mapping: Layout.Mapping<input, axes, plan, index>, +value: F32,
572 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
573 target_info: TargetInfo<Layout.output(input, axes, plan), original_target, index, value>, retained: Core.Tensor<input>,
574 lift: @-pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>> ->
575 {pair == Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained,
576 Core.write_flat(Layout.output(input, axes, plan), original_target, index, value)) :
577 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>} ->
578 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) :
579 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
580 -read_exact: {(retained, Done{value}) == Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)) :
581 Core.Tensor<input> & Result<&2, &2, Core.Error, F32>}) -> Transforms.StepCertificate<input, axes, plan, index, original_source, original_target>:
582 TargetInfo{owner, same, model} = target_info
583 step_write_certificate(input, axes, plan, index, original_source, original_target, mapping, value, map_exact,
584 CoreProof.write_original(Layout.output(input, axes, plan), original_target, owner, index, value, same,
585 Core.write_certificate(Layout.output(input, axes, plan), owner, index, value)), retained, lift, read_exact,
586 Core.source_read_model(input, original_source, Layout.source_index(input, axes, plan, index, mapping)),
587 Core.source_read_keeps(input, original_source, Layout.source_index(input, axes, plan, index, mapping)), model)
588
589def step_read_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
590 -original_source: Core.Tensor<input>, original_target: Core.Tensor<Layout.output(input, axes, plan)>,
591 +mapping: Layout.Mapping<input, axes, plan, index>,
592 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
593 lift: @-pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>> ->
594 {pair == Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target,
595 Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping))) :
596 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>} ->
597 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) :
598 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
599 certificate: Core.Read<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>) ->
600 Transforms.StepCertificate<input, axes, plan, index, original_source, original_target>:
601 Core.Read{retained, result, exact} = certificate
602 match result:
603 case Fail{error}:
604 Transforms.StepCertificate{(retained, Fail{Transforms.TensorError{error}}),
605 lift((retained, Fail{Transforms.TensorError{error}}),
606 Equal.cong(Core.Tensor<input> & Result<&2, &2, Core.Error, F32>,
607 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
608 pair => Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, pair),
609 (retained, Fail{error}), Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)), exact)), Unit{}}
610 case Done{+value}:
611 step_target_info(input, axes, plan, index, original_source, original_target, mapping, value, map_exact,
612 target_info(Layout.output(input, axes, plan), original_target, index, value), retained,
613 pair => equality => lift(pair,
614 Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
615 pair, Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, (retained, Done{value})),
616 Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target,
617 Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping))), equality,
618 Equal.cong(Core.Tensor<input> & Result<&2, &2, Core.Error, F32>,
619 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
620 read => Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, read),
621 (retained, Done{value}), Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)), exact))), exact)
622
623def step_mapped_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
624 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
625 result: Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
626 exact: {result == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}) ->
627 Transforms.StepCertificate<input, axes, plan, index, source, target>:
628 match result:
629 case Fail{error}:
630 Transforms.StepCertificate{(source, Fail{Transforms.LayoutError{error}}),
631 Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
632 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
633 mapped => Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, mapped),
634 Fail{error}, Layout.map_index(input, axes, plan, index), exact), Unit{}}
635 case Done{+mapping}:
636 step_read_certificate(input, axes, plan, index, source, target, mapping, exact,
637 pair => equality => Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
638 pair, Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, Done{mapping}),
639 Transforms.copy_step(input, axes, plan, source, target, index), equality,
640 Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
641 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
642 mapped => Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, mapped),
643 Done{mapping}, Layout.map_index(input, axes, plan, index), exact)),
644 Core.read_certificate(input, source, Layout.source_index(input, axes, plan, index, mapping)))
645
646def step_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
647 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>) ->
648 Transforms.StepCertificate<input, axes, plan, index, source, target>:
649 step_mapped_certificate(input, axes, plan, index, source, target, Layout.map_index(input, axes, plan, index), {==})
650
651def natural_step_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat, +index: U32,
652 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>,
653 -candidate: {index == U32.from_nat(cursor) : U32},
654 -conversion: {True{} == Nat.is_eq(U32.to_nat(index), cursor) : Bool},
655 same: {Transforms.natural_decided(input, axes, plan, cursor, index, source, target, candidate, Shape.BTrue{conversion}) ==
656 Transforms.natural_step(input, axes, plan, cursor, source, target) : Transforms.NaturalCopy<input, axes, plan, cursor>},
657 certificate: Transforms.StepCertificate<input, axes, plan, index, source, target>) ->
658 Transforms.NaturalCertificate<input, axes, plan, cursor, source, target>:
659 Transforms.StepCertificate{pair, exact, meaning} = certificate
660 Transforms.NaturalCertificate{Transforms.NaturalCopied{pair, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, conversion), candidate},
661 Equal.trans(Transforms.NaturalCopy<input, axes, plan, cursor>,
662 Transforms.NaturalCopied{pair, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, conversion), candidate},
663 Transforms.natural_decided(input, axes, plan, cursor, index, source, target, candidate, Shape.BTrue{conversion}),
664 Transforms.natural_step(input, axes, plan, cursor, source, target),
665 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
666 Transforms.NaturalCopy<input, axes, plan, cursor>,
667 result => Transforms.natural_result(input, axes, plan, cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, conversion), candidate, result),
668 pair, Transforms.copy_step(input, axes, plan, source, target, index), exact), same), meaning}
669
670def natural_decided_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat, +index: U32,
671 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
672 -candidate: {index == U32.from_nat(cursor) : U32},
673 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
674 same: {Transforms.natural_decided(input, axes, plan, cursor, index, source, target, candidate, decision) ==
675 Transforms.natural_step(input, axes, plan, cursor, source, target) : Transforms.NaturalCopy<input, axes, plan, cursor>}) ->
676 Transforms.NaturalCertificate<input, axes, plan, cursor, source, target>:
677 match decision:
678 case Shape.BFalse{equal}:
679 Transforms.NaturalCertificate{Transforms.NaturalError{source}, same, Unit{}}
680 case Shape.BTrue{equal}:
681 natural_step_lift(input, axes, plan, cursor, index, source, target, candidate, equal, same, step_certificate(input, axes, plan, index, source, target))
682
683def natural_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
684 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>) ->
685 Transforms.NaturalCertificate<input, axes, plan, cursor, source, target>:
686 +index = U32.from_nat(cursor)
687 natural_decided_certificate(input, axes, plan, cursor, index, source, target, {==}, Shape.bool_case(Nat.is_eq(U32.to_nat(index), cursor)), {==})
688
689def words_same_refl(+values: List<&2, U32>) -> {Layout.words_same(values, values) == True{} : Bool}:
690 Mapping.words_same_refl(values)
691
692def cursor_word_exact(+shape: Shape.Shape, +cursor: Nat, within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}) ->
693 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
694 Mapping.cursor_word_exact(shape, cursor, within)
695
696def decoded_coordinate(+shape: Shape.Shape, +index: U32,
697 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> Shape.Coordinate(Shape.extents(shape)):
698 Mapping.decoded_coordinate(shape, index, inside)
699
700def natural_lt_different(+a: Nat, +b: Nat, earlier: {Nat.is_lt(a, b) == True{} : Bool}) ->
701 {Nat.is_eq(b, a) == False{} : Bool}:
702 match a b:
703 case 0n 0n:
704 Empty.absurd({True{} == False{} : Bool}, Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, earlier)))
705 case 0n 1n+q:
706 {==}
707 case 1n+p 0n:
708 {==}
709 case 1n+p 1n+q:
710 natural_lt_different(p, q, earlier)
711
712def natural_words_different(+cursor: Nat, +other: Nat,
713 converted: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
714 prior: {U32.to_nat(U32.from_nat(other)) == other : Nat},
715 earlier: {Nat.is_lt(other, cursor) == True{} : Bool}) ->
716 {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(U32.from_nat(other))) == False{} : Bool}:
717 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, converted) : {Nat.is_eq(_, U32.to_nat(U32.from_nat(other))) == False{} : Bool}
718 %Equal.sym(Nat, U32.to_nat(U32.from_nat(other)), other, prior) : {Nat.is_eq(cursor, _) == False{} : Bool}
719 natural_lt_different(other, cursor, earlier)
720
721type ExpectedSame<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
722 -source: Core.Tensor<input>, -index: U32> is Data:
723 ExpectedSame{-equal: {Transforms.expected_output(input, axes, plan, source, index) ==
724 Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}}
725
726def expected_same_mapped(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
727 -original: Core.Tensor<input>, -source: Core.Tensor<input>,
728 kept: Transforms.SameSource(input, original, source),
729 result: Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>) ->
730 {Transforms.expected_mapped(input, axes, plan, index, source, result) ==
731 Transforms.expected_mapped(input, axes, plan, index, original, result) : Maybe<&2, F32>}:
732 match result:
733 case Fail{error}:
734 {==}
735 case Done{mapping}:
736 kept(Layout.source_index(input, axes, plan, index, mapping))
737
738def expected_same(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
739 -original: Core.Tensor<input>, -source: Core.Tensor<input>, +index: U32,
740 -kept: Transforms.SameSource(input, original, source)) -> ExpectedSame<input, axes, plan, original, source, index>:
741 ExpectedSame{expected_same_mapped(input, axes, plan, index, original, source, kept, Layout.map_index(input, axes, plan, index))}
742
743type PrefixSource<-input: Shape.Shape, -original: Core.Tensor<input>, -source: Core.Tensor<input>> is Data:
744 PrefixSource{-kept: Transforms.SameSource(input, original, source)}
745
746def prefix_source(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
747 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, -cursor: Nat,
748 prefix: Transforms.Prefix<input, axes, plan, original, source, target, cursor>) -> PrefixSource<input, original, source>:
749 Transforms.Prefix{kept, words, checked, written} = prefix
750 PrefixSource{kept}
751
752type PrefixWords<-cursor: Nat> is Data:
753 PrefixWords{-words: @+other: Nat -> @-earlier: {Nat.is_lt(other, cursor) == True{} : Bool} -> {U32.to_nat(U32.from_nat(other)) == other : Nat}}
754
755def prefix_word(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
756 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, -cursor: Nat,
757 prefix: Transforms.Prefix<input, axes, plan, original, source, target, cursor>) -> PrefixWords<cursor>:
758 Transforms.Prefix{kept, words, checked, written} = prefix
759 PrefixWords{words}
760
761type PrefixRoutes<-shape: Shape.Shape, -target: Core.Tensor<shape>, -cursor: Nat> is Data:
762 PrefixRoutes{-checked: @+other: Nat -> @-earlier: {Nat.is_lt(other, cursor) == True{} : Bool} ->
763 Core.ObservationChecked(Core.Packed{shape, target}, U32.from_nat(other))}
764
765def prefix_route(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
766 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, -cursor: Nat,
767 prefix: Transforms.Prefix<input, axes, plan, original, source, target, cursor>) -> PrefixRoutes<Layout.output(input, axes, plan), target, cursor>:
768 Transforms.Prefix{kept, words, checked, written} = prefix
769 PrefixRoutes{checked}
770
771def step_source(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
772 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
773 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
774 meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, (after_source, Done{after_target}))) ->
775 Transforms.SameSource(input, before_source, after_source):
776 (kept, rest) = meaning
777 kept
778
779def step_route(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
780 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
781 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
782 meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, (after_source, Done{after_target}))) ->
783 Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), after_target}, index):
784 (kept, rest) = meaning
785 (checked, values) = rest
786 checked
787
788def step_value(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
789 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
790 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
791 meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, (after_source, Done{after_target}))) ->
792 {Core.checked_observe(Layout.output(input, axes, plan), after_target, index) ==
793 Transforms.expected_output(input, axes, plan, before_source, index) : Maybe<&2, F32>}:
794 (kept, rest) = meaning
795 (checked, values) = rest
796 (observed, frame) = values
797 observed
798
799def step_frame(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -index: U32,
800 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
801 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
802 meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, (after_source, Done{after_target}))) ->
803 @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), before_target}, other) ->
804 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
805 Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), after_target}, other) &
806 {Core.checked_observe(Layout.output(input, axes, plan), after_target, other) ==
807 Core.checked_observe(Layout.output(input, axes, plan), before_target, other) : Maybe<&2, F32>}:
808 (kept, rest) = meaning
809 (checked, values) = rest
810 (observed, frame) = values
811 frame
812
813type CanonicalStep<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, -cursor: Nat,
814 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
815 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>> is Data:
816 CanonicalStep{-converted: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
817 -meaning: Transforms.StepMeaning(input, axes, plan, U32.from_nat(cursor), before_source, before_target, (after_source, Done{after_target}))}
818
819def canonical_step(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>, +cursor: Nat, -index: U32,
820 -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
821 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
822 -candidate: {index == U32.from_nat(cursor) : U32}, -converted: {U32.to_nat(index) == cursor : Nat},
823 -meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, (after_source, Done{after_target}))) ->
824 CanonicalStep<input, axes, plan, cursor, before_source, before_target, after_source, after_target>:
825 CanonicalStep{Equal.trans(Nat, U32.to_nat(U32.from_nat(cursor)), U32.to_nat(index), cursor,
826 Equal.cong(U32, Nat, U32.to_nat, U32.from_nat(cursor), index, Equal.sym(U32, index, U32.from_nat(cursor), candidate)), converted),
827 %candidate : Transforms.StepMeaning(input, axes, plan, _, before_source, before_target, (after_source, Done{after_target}))
828 meaning}
829
830type PastFrame<-shape: Shape.Shape, -before: Core.Tensor<shape>, -after: Core.Tensor<shape>, -other: Nat> is Data:
831 PastFrame{-checked: Core.ObservationChecked(Core.Packed{shape, after}, U32.from_nat(other)),
832 -equal: {Core.checked_observe(shape, after, U32.from_nat(other)) == Core.checked_observe(shape, before, U32.from_nat(other)) : Maybe<&2, F32>}}
833
834def past_frame(-shape: Shape.Shape, -before: Core.Tensor<shape>, -after: Core.Tensor<shape>, +cursor: Nat, +other: Nat,
835 -converted: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, -prior_word: {U32.to_nat(U32.from_nat(other)) == other : Nat},
836 -prior_checked: Core.ObservationChecked(Core.Packed{shape, before}, U32.from_nat(other)),
837 -earlier: {Nat.is_lt(other, cursor) == True{} : Bool},
838 -frame: @+j: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, before}, j) ->
839 @different: {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(j)) == False{} : Bool} ->
840 Core.ObservationChecked(Core.Packed{shape, after}, j) &
841 {Core.checked_observe(shape, after, j) == Core.checked_observe(shape, before, j) : Maybe<&2, F32>}) ->
842 PastFrame<shape, before, after, other>:
843 PastFrame{
844 Pair.fst(Core.ObservationChecked(Core.Packed{shape, after}, U32.from_nat(other)),
845 {Core.checked_observe(shape, after, U32.from_nat(other)) == Core.checked_observe(shape, before, U32.from_nat(other)) : Maybe<&2, F32>},
846 frame(U32.from_nat(other))(prior_checked)(natural_words_different(cursor, other, converted, prior_word, earlier))),
847 Pair.snd(Core.ObservationChecked(Core.Packed{shape, after}, U32.from_nat(other)),
848 {Core.checked_observe(shape, after, U32.from_nat(other)) == Core.checked_observe(shape, before, U32.from_nat(other)) : Maybe<&2, F32>},
849 frame(U32.from_nat(other))(prior_checked)(natural_words_different(cursor, other, converted, prior_word, earlier)))}
850
851def actual_advanced(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
852 -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -after_source: Core.Tensor<input>,
853 -before_target: Core.Tensor<Layout.output(input, axes, plan)>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
854 prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>,
855 canonical: CanonicalStep<input, axes, plan, cursor, before_source, before_target, after_source, after_target>) ->
856 Transforms.Advanced<input, axes, plan, original, before_source, after_source, before_target, after_target, cursor>:
857 Transforms.Prefix{source_prior, words_prior, checked_prior, written_prior} = prefix
858 CanonicalStep{converted, meaning} = canonical
859 Transforms.Advanced{converted,
860 step_source(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
861 Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(cursor)),
862 Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)),
863 Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)),
864 step_value(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
865 {\{ExpectedSame: equal => equal} : ExpectedSame<input, axes, plan, original, before_source, U32.from_nat(cursor)> ->
866 {Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)) ==
867 Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>}}(
868 expected_same(input, axes, plan, original, before_source, U32.from_nat(cursor), source_prior))),
869 step_route(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
870 other => earlier => {\{PastFrame: checked => equal => checked} :
871 PastFrame<Layout.output(input, axes, plan), before_target, after_target, other> ->
872 Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), after_target}, U32.from_nat(other))}(
873 past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted,
874 words_prior(other, earlier), checked_prior(other, earlier), earlier,
875 step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning))),
876 other => earlier => {\{PastFrame: checked => equal => equal} :
877 PastFrame<Layout.output(input, axes, plan), before_target, after_target, other> ->
878 {Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(other)) ==
879 Core.checked_observe(Layout.output(input, axes, plan), before_target, U32.from_nat(other)) : Maybe<&2, F32>}}(
880 past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted,
881 words_prior(other, earlier), checked_prior(other, earlier), earlier,
882 step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning)))}
883
884def add_successor_right(+left: Nat, -right: Nat) -> {Nat.add(left, 1n+right) == 1n+Nat.add(left, right) : Nat}:
885 match left:
886 case 0n:
887 {==}
888 case 1n+p:
889 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+right), 1n+Nat.add(p, right), add_successor_right(p, right))
890
891def loop_continue(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
892 -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
893 -after_source: Core.Tensor<input>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>, -index: U32,
894 -converted: {U32.to_nat(index) == cursor : Nat}, -candidate: {index == U32.from_nat(cursor) : U32},
895 natural_exact: {Transforms.NaturalCopied{(after_source, Done{after_target}), index, converted, candidate} ==
896 Transforms.natural_step(input, axes, plan, cursor, before_source, before_target) : Transforms.NaturalCopy<input, axes, plan, cursor>},
897 certificate: Transforms.LoopCertificate<input, axes, plan, original, fuel, 1n+cursor, after_source, after_target>) ->
898 Transforms.LoopCertificate<input, axes, plan, original, 1n+fuel, cursor, before_source, before_target>:
899 Transforms.LoopCertificate{pair, exact, meaning} = certificate
900 Transforms.LoopCertificate{pair,
901 Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>, pair,
902 Transforms.copy_loop(fuel, input, axes, plan, after_source, after_target, 1n+cursor),
903 Transforms.copy_loop(1n+fuel, input, axes, plan, before_source, before_target, cursor), exact,
904 Equal.cong(Transforms.NaturalCopy<input, axes, plan, cursor>,
905 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
906 result => Transforms.natural_next(input, axes, plan, cursor,
907 source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor), result),
908 Transforms.NaturalCopied{(after_source, Done{after_target}), index, converted, candidate},
909 Transforms.natural_step(input, axes, plan, cursor, before_source, before_target), natural_exact)),
910 %add_successor_right(fuel, cursor) : Transforms.LoopMeaning(input, axes, plan, original, _, pair)
911 meaning}
912
913def loop_after_pair(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
914 -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
915 -index: U32, -converted: {U32.to_nat(index) == cursor : Nat}, -candidate: {index == U32.from_nat(cursor) : U32},
916 -prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>,
917 pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
918 natural_exact: {Transforms.NaturalCopied{pair, index, converted, candidate} ==
919 Transforms.natural_step(input, axes, plan, cursor, before_source, before_target) : Transforms.NaturalCopy<input, axes, plan, cursor>},
920 -meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, pair),
921 rec: @source: Core.Tensor<input> -> @target: Core.Tensor<Layout.output(input, axes, plan)> ->
922 @-prefix: Transforms.Prefix<input, axes, plan, original, source, target, 1n+cursor> ->
923 Transforms.LoopCertificate<input, axes, plan, original, fuel, 1n+cursor, source, target>) ->
924 Transforms.LoopCertificate<input, axes, plan, original, 1n+fuel, cursor, before_source, before_target>:
925 (source, result) = pair
926 match result:
927 case Fail{error}:
928 Transforms.LoopCertificate{(source, Fail{error}),
929 Equal.cong(Transforms.NaturalCopy<input, axes, plan, cursor>,
930 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
931 step => Transforms.natural_next(input, axes, plan, cursor,
932 source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor), step),
933 Transforms.NaturalCopied{(source, Fail{error}), index, converted, candidate},
934 Transforms.natural_step(input, axes, plan, cursor, before_source, before_target), natural_exact), Unit{}}
935 case Done{target}:
936 loop_continue(fuel, input, axes, plan, cursor, original, before_source, before_target, source, target, index, converted, candidate,
937 natural_exact, rec(source)(target)(
938 Laws.advance_prefix(input, axes, plan, original, before_source, source, before_target, target, cursor, prefix,
939 actual_advanced(input, axes, plan, cursor, original, before_source, source, before_target, target, prefix,
940 canonical_step(input, axes, plan, cursor, index, before_source, before_target, source, target, candidate, converted, meaning)))))
941
942def loop_after_natural(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
943 -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
944 -prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>,
945 certificate: Transforms.NaturalCertificate<input, axes, plan, cursor, before_source, before_target>,
946 rec: @source: Core.Tensor<input> -> @target: Core.Tensor<Layout.output(input, axes, plan)> ->
947 @-prefix: Transforms.Prefix<input, axes, plan, original, source, target, 1n+cursor> ->
948 Transforms.LoopCertificate<input, axes, plan, original, fuel, 1n+cursor, source, target>) ->
949 Transforms.LoopCertificate<input, axes, plan, original, 1n+fuel, cursor, before_source, before_target>:
950 Transforms.NaturalCertificate{result, exact, meaning} = certificate
951 match result:
952 case Transforms.NaturalError{source}:
953 Transforms.LoopCertificate{(source, Fail{Transforms.LayoutError{Layout.MappingError{}}}),
954 Equal.cong(Transforms.NaturalCopy<input, axes, plan, cursor>,
955 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
956 step => Transforms.natural_next(input, axes, plan, cursor,
957 source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor), step),
958 Transforms.NaturalError{source}, Transforms.natural_step(input, axes, plan, cursor, before_source, before_target), exact), Unit{}}
959 case Transforms.NaturalCopied{pair, index, converted, candidate}:
960 loop_after_pair(fuel, input, axes, plan, cursor, original, before_source, before_target, index, converted, candidate, prefix,
961 pair, exact, meaning, rec)
962
963def loop_certificate(fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
964 -original: Core.Tensor<input>, source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
965 -prefix: Transforms.Prefix<input, axes, plan, original, source, target, cursor>) ->
966 Transforms.LoopCertificate<input, axes, plan, original, fuel, cursor, source, target>:
967 match fuel:
968 case 0n:
969 Transforms.LoopCertificate{(source, Done{target}), {==}, prefix}
970 case 1n++remaining:
971 loop_after_natural(remaining, input, axes, plan, cursor, original, source, target, prefix,
972 natural_certificate(input, axes, plan, cursor, source, target),
973 source => target => invariant => loop_certificate(remaining, input, axes, plan, 1n+cursor, original, source, target, invariant))
974
975def add_zero_right(+left: Nat) -> {Nat.add(left, 0n) == left : Nat}:
976 match left:
977 case 0n:
978 {==}
979 case 1n+p:
980 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p))
981
982def whole_copy_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
983 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>) ->
984 Transforms.LoopCertificate<input, axes, plan, source, Shape.elements(Layout.output(input, axes, plan)), 0n, source, target>:
985 loop_certificate(Shape.elements(Layout.output(input, axes, plan)), input, axes, plan, 0n, source, source, target,
986 Laws.initial_prefix(input, axes, plan, source, target))
987
988def whole_copy_meaning(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
989 -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>,
990 certificate: Transforms.LoopCertificate<input, axes, plan, source, Shape.elements(Layout.output(input, axes, plan)), 0n, source, target>) ->
991 Transforms.WholeCopyModel<input, axes, plan, source, target>:
992 Transforms.LoopCertificate{pair, exact, meaning} = certificate
993 Transforms.WholeCopyModel{
994 %exact : Transforms.LoopMeaning(input, axes, plan, source,
995 Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), _)
996 %Shape.elements_exact(Layout.output(input, axes, plan)) : Transforms.LoopMeaning(input, axes, plan, source, _, pair)
997 %add_zero_right(Shape.elements(Layout.output(input, axes, plan))) : Transforms.LoopMeaning(input, axes, plan, source, _, pair)
998 meaning}
999
1000def Laws.whole_copy_interpretation(input, axes, plan, source, target):
1001 whole_copy_meaning(input, axes, plan, source, target, whole_copy_certificate(input, axes, plan, source, target))
1002
1003def permuted_output(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
1004 -original: Core.Tensor<input>, -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>,
1005 prefix: Transforms.Prefix<input, axes, plan, original, source, target,
1006 Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>) ->
1007 Transforms.PermuteOutput<input, axes, original, source, Core.Packed{Layout.output(input, axes, plan), target}>:
1008 Transforms.Prefix{kept, words, checked, written} = prefix
1009 Transforms.PermuteOutput{plan, {==}, kept, words, checked, written,
1010 other => bound => Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1011 Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1012 Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)),
1013 {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>,
1014 Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1015 Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)), equal)} :
1016 ObserveBridge<Layout.output(input, axes, plan), target, U32.from_nat(other)> ->
1017 {Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) ==
1018 Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) : Maybe<&2, F32>}}(
1019 observe_bridge(Layout.output(input, axes, plan), target, U32.from_nat(other), checked(other, bound))),
1020 written(other, bound))}
1021
1022def copy_pack_model(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
1023 pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
1024 -meaning: Transforms.LoopMeaning(input, axes, plan, original,
1025 Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), pair)) ->
1026 Transforms.PublicModel<input, axes, original, Transforms.copy_pack(input, axes, plan, pair)>:
1027 (source, result) = pair
1028 match result:
1029 case Fail{error}:
1030 Transforms.PublicModel{Unit{}}
1031 case Done{target}:
1032 Transforms.PublicModel{
1033 permuted_output(input, axes, plan, original, source, target, meaning)}
1034
1035def allocated_model(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, source: Core.Tensor<input>,
1036 allocated: Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>) ->
1037 Transforms.PublicModel<input, axes, source, Transforms.copy_allocated(input, axes, plan, source, allocated)>:
1038 match allocated:
1039 case Fail{error}:
1040 Transforms.PublicModel{Unit{}}
1041 case Done{target}:
1042 copy_pack_model(input, axes, plan, source, Transforms.built(input, axes, plan, source, target),
1043 PermuteBuild.built_meaning(input, axes, plan, source, target))
1044
1045def planned_model(+input: Shape.Shape, +axes: List<&2, U32>, source: Core.Tensor<input>,
1046 planned: Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>) ->
1047 Transforms.PublicModel<input, axes, source, Transforms.copy_planned(input, axes, source, planned)>:
1048 match planned:
1049 case Fail{error}:
1050 Transforms.PublicModel{Unit{}}
1051 case Done{+plan}:
1052 allocated_model(input, axes, plan, source, Core.new(Layout.output(input, axes, plan), 0.0))
1053
1054def Laws.permute_result_interpretation(input, source, axes):
1055 planned_model(input, axes, source, Layout.permutation(input, axes))
1056
1057def transpose_decided_model(+input: Shape.Shape, source: Core.Tensor<input>, +a: U32, +b: U32,
1058 decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>) ->
1059 Transforms.PublicModel<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source,
1060 Transforms.transpose_decided(input, source, a, b, decision)>:
1061 match decision:
1062 case Shape.BFalse{equal}:
1063 Transforms.PublicModel{Unit{}}
1064 case Shape.BTrue{equal}:
1065 Laws.permute_result_interpretation(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))
1066
1067def Laws.transpose_result_interpretation(input, source, a, b):
1068 transpose_decided_model(input, source, a, b,
1069 Shape.bool_case(TransposeSpec.valid(input, a, b)))
1070
1071type ReshapeDecidedModel<-input: Shape.Shape, -target: Shape.Shape, -original: Core.Tensor<input>, -dimensions: List<&2, U32>,
1072 -decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>> is Data:
1073 ReshapeDecidedModel{-meaning: Transforms.ReshapeMeaning(input, original, dimensions,
1074 Transforms.reshape_decided(input, target, original, decision))}
1075
1076def reshape_decided_model(+input: Shape.Shape, +target: Shape.Shape, source: Core.Tensor<input>, -dimensions: List<&2, U32>,
1077 -preserved: {Shape.dimensions(target) == dimensions : List<&2, U32>},
1078 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>) ->
1079 ReshapeDecidedModel<input, target, source, dimensions, decision>:
1080 match decision:
1081 case Shape.BFalse{equal}:
1082 ReshapeDecidedModel{Unit{}}
1083 case Shape.BTrue{equal}:
1084 ReshapeDecidedModel{Transforms.ReshapeOutput{target,
1085 Equal.trans(List<&2, U32>, Transforms.dynamic_dimensions(Transforms.reshape_equal(input, target, source,
1086 Transforms.elements_equal(input, target, equal))), Shape.dimensions(target), dimensions,
1087 Laws.reshape_target_dimensions(input, target, source, Transforms.elements_equal(input, target, equal)), preserved),
1088 preserved,
1089 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)),
1090 Shape.logical_numel(dimensions), Transforms.elements_equal(input, target, equal),
1091 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(target), dimensions, preserved)),
1092 index => Laws.reshape_linear_order(input, target, source, index, Transforms.elements_equal(input, target, equal))}}
1093
1094type ReshapeBuiltModel<-input: Shape.Shape, -original: Core.Tensor<input>, -dimensions: List<&2, U32>,
1095 -built: Shape.ConstructResult<dimensions>> is Data:
1096 ReshapeBuiltModel{-meaning: Transforms.ReshapeMeaning(input, original, dimensions,
1097 Transforms.reshape_built(input, original, dimensions, built))}
1098
1099def reshape_built_model(+input: Shape.Shape, source: Core.Tensor<input>, -dimensions: List<&2, U32>,
1100 built: Shape.ConstructResult<dimensions>) -> ReshapeBuiltModel<input, source, dimensions, built>:
1101 match built:
1102 case Shape.SError{error}:
1103 ReshapeBuiltModel{Unit{}}
1104 case Shape.SBuilt{+target, preserved}:
1105 ReshapeBuiltModel{
1106 {\{ReshapeDecidedModel: meaning => meaning} :
1107 ReshapeDecidedModel<input, target, source, dimensions, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))> ->
1108 Transforms.ReshapeMeaning(input, source, dimensions,
1109 Transforms.reshape_decided(input, target, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))))}(
1110 reshape_decided_model(input, target, source, dimensions, preserved,
1111 Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(target)))))}
1112
1113def Laws.reshape_result_interpretation(input, source, dimensions):
1114 Transforms.ReshapeModel{
1115 {\{ReshapeBuiltModel: meaning => meaning} : ReshapeBuiltModel<input, source, dimensions, Shape.construct(dimensions)> ->
1116 Transforms.ReshapeMeaning(input, source, dimensions, Transforms.reshape(input, source, dimensions))}(
1117 reshape_built_model(input, source, dimensions, Shape.construct(dimensions)))}
1118
1119type RestoreModel<-input: Shape.Shape, -original: Core.Tensor<input>, -result: Result<&2, &1, Transforms.Error, Core.Dynamic>> is Data:
1120 RestoreModel{-meaning: Transforms.RestoreMeaning(input, original, result)}
1121
1122def restore_result_model(-input: Shape.Shape, -original: Core.Tensor<input>, -middle_shape: Shape.Shape,
1123 -middle: Core.Tensor<middle_shape>, result: Result<&2, &1, Transforms.Error, Core.Dynamic>,
1124 -meaning: Transforms.ReshapeMeaning(middle_shape, middle, Shape.dimensions(input), result),
1125 -prior: @+index: U32 -> {Core.observe(middle_shape, middle, index) == Core.observe(input, original, index) : Maybe<&2, F32>}) ->
1126 RestoreModel<input, original, result>:
1127 match result:
1128 case Fail{error}:
1129 RestoreModel{Unit{}}
1130 case Done{output}:
1131 RestoreModel{
1132 {\{Transforms.ReshapeOutput: shape => dimensions => shape_exact => count => linear =>
1133 Transforms.RestoredOutput{dimensions,
1134 index => Equal.trans(Maybe<&2, F32>, Transforms.dynamic_observe(output, index),
1135 Core.observe(middle_shape, middle, index), Core.observe(input, original, index), linear(index), prior(index))}} :
1136 Transforms.ReshapeOutput<middle_shape, middle, Shape.dimensions(input), output> ->
1137 Transforms.RestoredOutput<input, original, output>}(meaning)}
1138
1139def restore_dynamic_model(+input: Shape.Shape, -original: Core.Tensor<input>, middle: Core.Dynamic,
1140 -prior: @+index: U32 -> {Transforms.dynamic_observe(middle, index) == Core.observe(input, original, index) : Maybe<&2, F32>}) ->
1141 RestoreModel<input, original, Transforms.reshape_dynamic(middle, Shape.dimensions(input))>:
1142 Core.Packed{+shape, tensor} = middle
1143 restore_result_model(input, original, shape, tensor, Transforms.reshape(shape, tensor, Shape.dimensions(input)),
1144 {\{Transforms.ReshapeModel: meaning => meaning} : Transforms.ReshapeModel<shape, tensor, Shape.dimensions(input)> ->
1145 Transforms.ReshapeMeaning(shape, tensor, Shape.dimensions(input), Transforms.reshape(shape, tensor, Shape.dimensions(input)))}(
1146 Laws.reshape_result_interpretation(shape, tensor, Shape.dimensions(input))), prior)
1147
1148type ReshapeInverseResultModel<-input: Shape.Shape, -original: Core.Tensor<input>, -result: Result<&2, &1, Transforms.Error, Core.Dynamic>> is Data:
1149 ReshapeInverseResultModel{-meaning: Transforms.ReshapeInverseMeaning(input, original, result)}
1150
1151def reshape_inverse_result_model(-input: Shape.Shape, -original: Core.Tensor<input>, -dimensions: List<&2, U32>,
1152 result: Result<&2, &1, Transforms.Error, Core.Dynamic>,
1153 -meaning: Transforms.ReshapeMeaning(input, original, dimensions, result)) -> ReshapeInverseResultModel<input, original, result>:
1154 match result:
1155 case Fail{error}:
1156 ReshapeInverseResultModel{Unit{}}
1157 case Done{output}:
1158 ReshapeInverseResultModel{
1159 {\{Transforms.ReshapeOutput: shape => dimensions_exact => shape_exact => count => linear =>
1160 {\{RestoreModel: meaning => meaning} : RestoreModel<input, original, Transforms.reshape_dynamic(output, Shape.dimensions(input))> ->
1161 Transforms.RestoreMeaning(input, original, Transforms.reshape_dynamic(output, Shape.dimensions(input)))}(
1162 restore_dynamic_model(input, original, output, linear))} :
1163 Transforms.ReshapeOutput<input, original, dimensions, output> ->
1164 Transforms.RestoreMeaning(input, original, Transforms.reshape_dynamic(output, Shape.dimensions(input)))}(meaning)}
1165
1166def Laws.reshape_inverse_observations(input, source, dimensions):
1167 Transforms.ReshapeInverseModel{
1168 {\{ReshapeInverseResultModel: meaning => meaning} :
1169 ReshapeInverseResultModel<input, source, Transforms.reshape(input, source, dimensions)> ->
1170 Transforms.ReshapeInverseMeaning(input, source, Transforms.reshape(input, source, dimensions))}(
1171 reshape_inverse_result_model(input, source, dimensions, Transforms.reshape(input, source, dimensions),
1172 {\{Transforms.ReshapeModel: meaning => meaning} : Transforms.ReshapeModel<input, source, dimensions> ->
1173 Transforms.ReshapeMeaning(input, source, dimensions, Transforms.reshape(input, source, dimensions))}(
1174 Laws.reshape_result_interpretation(input, source, dimensions))))}
1175
1176def Laws.mapping_reference(input, axes, plan, index, mapping):
1177 Mapping.mapping_reference(input, axes, plan, index, mapping)
1178
1179def Laws.mapped_mathematical_bounded(input, axes, plan, index, mapping):
1180 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
1181 Mapping.flat_mathematical_bounded(input, source)
1182
1183def natural_word_exact(+number: Nat, +limit: U32, +within: {Nat.is_le(number, U32.to_nat(limit)) == True{} : Bool}) ->
1184 {U32.to_nat(U32.from_nat(number)) == number : Nat}:
1185 WordConversion.natural_word_exact(number, limit, within)
1186
1187def Laws.natural_word_exact(number, limit, within):
1188 natural_word_exact(number, limit, within)
1189
1190def shape_count_bound(+shape: Shape.Shape) -> {Nat.is_le(Shape.elements(shape), 1048576n) == True{} : Bool}:
1191 match shape:
1192 case Shape.SShape{+dimensions, +size, +exact, rank_bound, capacity_bound}:
1193 %Equal.sym(Nat, size, Shape.logical_numel(dimensions), exact) : {Nat.is_le(_, 1048576n) == True{} : Bool}
1194 Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(dimensions), 1048576n),
1195 Nats.le_true(Shape.logical_numel(dimensions), 1048576n, capacity_bound))
1196
1197type CheckedObservationModel<-shape: Shape.Shape, -tensor: Core.Tensor<shape>, -index: U32> is Data:
1198 CheckedObservationModel{-checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index)}
1199
1200def checked_observation_model(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
1201 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1202 CheckedObservationModel<shape, tensor, index>:
1203 Core.TTensor{storage, exact} = tensor
1204 match storage:
1205 case Storage.Empty{}:
1206 CheckedObservationModel{Arith.lt_zero(U32.to_nat(index),
1207 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1208 inside)}
1209 case Storage.Owned{+depth, +length, array, balanced, valid}:
1210 CheckedObservationModel{Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
1211 Route.index_complete(depth, length, index, valid,
1212 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1213 inside))}
1214
1215type PresentObservation<-shape: Shape.Shape, -tensor: Core.Tensor<shape>, -index: U32> is Data:
1216 PresentObservation{-value: F32, -equal: {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>}}
1217
1218def present_impossible(-shape: Shape.Shape, -tensor: Core.Tensor<shape>, -index: U32, -empty: Empty) -> PresentObservation<shape, tensor, index>:
1219 PresentObservation{Empty.absurd(F32, empty),
1220 Empty.absurd({Core.checked_observe(shape, tensor, index) == Some{Empty.absurd(F32, empty)} : Maybe<&2, F32>}, empty)}
1221
1222def present_observation(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
1223 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1224 PresentObservation<shape, tensor, index>:
1225 Core.TTensor{storage, exact} = tensor
1226 match storage:
1227 case Storage.Empty{}:
1228 present_impossible(shape, Core.TTensor{Storage.Empty{}, exact}, index,
1229 Arith.lt_zero(U32.to_nat(index),
1230 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1231 inside))
1232 case Storage.Owned{+depth, +length, array, balanced, valid}:
1233 PresentObservation{Refinement.second(F32, Array.get(F32, array, index)),
1234 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index),
1235 Model.observe(F32, depth, array, Refinement.route(depth, index)), Some{Refinement.second(F32, Array.get(F32, array, index))},
1236 observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
1237 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1238 inside,
1239 Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
1240 Route.index_complete(depth, length, index, valid,
1241 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1242 inside))),
1243 Equal.sym(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, array, index))},
1244 Model.observe(F32, depth, array, Refinement.route(depth, index)), Refinement.law_get_refines(F32, depth, array, index, balanced)))}
1245
1246def maybe_present(value: Maybe<&2, F32>) -> Bool:
1247 match value:
1248 case None{}:
1249 False{}
1250 case Some{value}:
1251 True{}
1252
1253type ReadSuccess<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32> is Type:
1254 ReadSuccess{retained: Core.Tensor<shape>, value: F32,
1255 exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>}}
1256
1257type ReadSuccessModel<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32> is Data:
1258 ReadSuccessModel{-success: ReadSuccess<shape, original, index>}
1259
1260def read_success_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32,
1261 certificate: Core.Read<shape, original, index>,
1262 -model: Core.SourceRead<shape, original, index>, -present: PresentObservation<shape, original, index>) -> ReadSuccessModel<shape, original, index>:
1263 Core.Read{retained, result, exact} = certificate
1264 match result:
1265 case Fail{error}:
1266 ReadSuccessModel{Empty.absurd(ReadSuccess<shape, original, index>,
1267 {\{Core.SourceRead: meaning =>
1268 {\{PresentObservation: value => equal => Arith.clash(Equal.cong(Maybe<&2, F32>, Bool, maybe_present, None{}, Some{value},
1269 Equal.trans(Maybe<&2, F32>, None{}, Core.checked_observe(shape, original, index), Some{value},
1270 Equal.trans(Maybe<&2, F32>, None{}, Core.read_value(shape, Core.read_flat(shape, original, index)),
1271 Core.checked_observe(shape, original, index),
1272 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
1273 (retained, Fail{error}), Core.read_flat(shape, original, index), exact), meaning), equal)))} :
1274 PresentObservation<shape, original, index> -> Empty}(present)} : Core.SourceRead<shape, original, index> -> Empty}(model))}
1275 case Done{value}:
1276 ReadSuccessModel{ReadSuccess{retained, value, exact}}
1277
1278type ReadTotalInfo<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32> is Type:
1279 ReadTotalInfo{owner: Core.Tensor<shape>, same: {owner == original : Core.Tensor<shape>},
1280 -present: PresentObservation<shape, original, index>, -model: Core.SourceRead<shape, original, index>}
1281
1282def read_total_info(+shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32,
1283 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1284 ReadTotalInfo<shape, original, index>:
1285 ReadTotalInfo{original, {==}, present_observation(shape, original, index, inside), Core.source_read_model(shape, original, index)}
1286
1287def read_total_certificate(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32,
1288 info: ReadTotalInfo<shape, original, index>) -> ReadSuccessModel<shape, original, index>:
1289 ReadTotalInfo{owner, same, present, model} = info
1290 read_success_model(shape, original, index, read_rebased(shape, original, owner, index, same, Core.read_certificate(shape, owner, index)), model, present)
1291
1292def read_success(+shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32,
1293 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
1294 ReadSuccessModel<shape, original, index>:
1295 read_total_certificate(shape, original, index, read_total_info(shape, original, index, inside))
1296
1297def decoded_offset(+shape: Shape.Shape, +index: U32,
1298 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
1299 {Shape.offset(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index))) == U32.to_nat(index) : Nat}:
1300 %Mapping.decoded_indices(shape, index, inside) : {Shape.offset(Shape.extents(shape), _) == U32.to_nat(index) : Nat}
1301 Equal.trans(Nat, Shape.offset(Shape.extents(shape), Shape.indices(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1302 Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)), U32.to_nat(index),
1303 Coordinates.offset_indices(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1304 Equal.trans(Nat, Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1305 Shape.Fin.value(Shape.numel(Shape.extents(shape)),
1306 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
1307 U32.to_nat(index),
1308 Equal.trans(Nat, Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1309 Shape.Fin.value(Shape.numel(Shape.extents(shape)), Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1310 Shape.Fin.value(Shape.numel(Shape.extents(shape)),
1311 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
1312 Equal.sym(Nat, Shape.Fin.value(Shape.numel(Shape.extents(shape)), Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1313 Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1314 ShapeIndex.flatten_row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1315 Equal.cong(Shape.Fin(Shape.numel(Shape.extents(shape))), Nat, value => Shape.Fin.value(Shape.numel(Shape.extents(shape)), value),
1316 Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1317 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)),
1318 ShapeIndex.flatten_unflatten(Shape.extents(shape),
1319 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))))),
1320 Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))))
1321
1322def Laws.codec_flatten_decode(shape, index, inside):
1323 %Equal.sym(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index)),
1324 Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), Mapping.codec_decoded(Shape.dimensions(shape), index)) :
1325 {Layout.flatten_words(Shape.dimensions(shape), _, 0) == index : U32}
1326 Equal.trans(U32, Layout.flatten_words(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), 0),
1327 U32.from_nat(U32.to_nat(index)), index,
1328 Equal.cong(Nat, U32, U32.from_nat,
1329 Shape.horner(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), 0n), U32.to_nat(index),
1330 Equal.trans(Nat, Shape.horner(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), 0n),
1331 Shape.offset(Shape.extents(shape), Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))))), U32.to_nat(index),
1332 Coordinates.horner_spec(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), 0n,
1333 Mapping.decoded_word_fits(shape, index, inside)),
1334 %Equal.sym(List<&2, Nat>, Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index)))),
1335 Shape.digits(Shape.extents(shape), U32.to_nat(index)),
1336 WordConversion.naturals_words_fitting(Shape.dimensions(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), Mapping.decoded_fit(shape, index, inside))) :
1337 {Shape.offset(Shape.extents(shape), _) == U32.to_nat(index) : Nat}
1338 decoded_offset(shape, index, inside))),
1339 WordConversion.word_natural_exact(index))
1340
1341def shape_construct_complete(+shape: Shape.Shape) ->
1342 {ShapeLaws.built(Shape.dimensions(shape), Shape.construct(Shape.dimensions(shape))) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
1343 match shape:
1344 case Shape.SShape{+dimensions, size, exact, rank_bound, capacity_bound}:
1345 ShapeLaws.construction_complete(dimensions, rank_bound, capacity_bound)
1346
1347type ReshapeDecisionSuccess<-input: Shape.Shape, -target: Shape.Shape, -source: Core.Tensor<input>,
1348 -decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>> is Data:
1349 ReshapeDecisionSuccess{-success: {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1350 Transforms.reshape_decided(input, target, source, decision)) == True{} : Bool}}
1351
1352def reshape_decision_success(+input: Shape.Shape, +target: Shape.Shape,
1353 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>, source: Core.Tensor<input>,
1354 -same: {Shape.elements(input) == Shape.elements(target) : Nat}) -> ReshapeDecisionSuccess<input, target, source, decision>:
1355 match decision:
1356 case Shape.BFalse{equal}:
1357 ReshapeDecisionSuccess{Empty.absurd({Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1358 Transforms.reshape_decided(input, target, source, Shape.BFalse{equal})) == True{} : Bool},
1359 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(target)), True{}, equal,
1360 Mapping.natural_equal_true(Shape.elements(input), Shape.elements(target), same))))}
1361 case Shape.BTrue{equal}:
1362 ReshapeDecisionSuccess{{==}}
1363
1364type ReshapeBuiltSuccess<-input: Shape.Shape, -target: Shape.Shape, -source: Core.Tensor<input>,
1365 -built: Shape.ConstructResult<Shape.dimensions(target)>> is Data:
1366 ReshapeBuiltSuccess{-success: {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1367 Transforms.reshape_built(input, source, Shape.dimensions(target), built)) == True{} : Bool}}
1368
1369def reshape_built_success(+input: Shape.Shape, +target: Shape.Shape,
1370 built: Shape.ConstructResult<Shape.dimensions(target)>, source: Core.Tensor<input>,
1371 -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
1372 -complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}) ->
1373 ReshapeBuiltSuccess<input, target, source, built>:
1374 match built:
1375 case Shape.SError{error}:
1376 ReshapeBuiltSuccess{Empty.absurd({Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1377 Transforms.reshape_built(input, source, Shape.dimensions(target), Shape.SError{error})) == True{} : Bool},
1378 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Mapping.metadata_present, None{}, Some{Shape.dimensions(target)}, complete)))}
1379 case Shape.SBuilt{+output, preserved}:
1380 ReshapeBuiltSuccess{
1381 {\{ReshapeDecisionSuccess: success => success} :
1382 ReshapeDecisionSuccess<input, output, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output)))> ->
1383 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1384 Transforms.reshape_decided(input, output, source, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))))) == True{} : Bool}}(
1385 reshape_decision_success(input, output, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), source,
1386 Mapping.element_counts_same(input, output,
1387 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)),
1388 Shape.logical_numel(Shape.dimensions(output)), same,
1389 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(target), Shape.dimensions(output),
1390 Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved))))))}
1391
1392def Laws.reshape_valid_success(input, target, source, same):
1393 Transforms.ReshapeSuccessModel{
1394 {\{ReshapeBuiltSuccess: success => success} : ReshapeBuiltSuccess<input, target, source, Shape.construct(Shape.dimensions(target))> ->
1395 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape(input, source, Shape.dimensions(target))) == True{} : Bool}}(
1396 reshape_built_success(input, target, Shape.construct(Shape.dimensions(target)), source, same, shape_construct_complete(target)))}
1397
1398type DynamicRestoreSuccess<-input: Shape.Shape, -output: Core.Dynamic> is Data:
1399 DynamicRestoreSuccess{-success: {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic,
1400 Transforms.reshape_dynamic(output, Shape.dimensions(input))) == True{} : Bool}}
1401
1402def dynamic_restore_success(+input: Shape.Shape, output: Core.Dynamic,
1403 -same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Transforms.dynamic_dimensions(output)) : Nat}) ->
1404 DynamicRestoreSuccess<input, output>:
1405 Core.Packed{+shape, tensor} = output
1406 DynamicRestoreSuccess{
1407 {\{Transforms.ReshapeSuccessModel: success => success} : Transforms.ReshapeSuccessModel<shape, input, tensor> ->
1408 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape(shape, tensor, Shape.dimensions(input))) == True{} : Bool}}(
1409 Laws.reshape_valid_success(shape, input, tensor,
1410 Equal.sym(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(shape)), same)))}
1411
1412type ReshapeInverseSuccessResult<-input: Shape.Shape, -result: Result<&2, &1, Transforms.Error, Core.Dynamic>> is Data:
1413 ReshapeInverseSuccessResult{-success: {Transforms.reshape_inverse_success(input, result) == True{} : Bool}}
1414
1415def reshape_inverse_success_result(+input: Shape.Shape, -original: Core.Tensor<input>, -dimensions: List<&2, U32>,
1416 result: Result<&2, &1, Transforms.Error, Core.Dynamic>,
1417 -successful: {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, result) == True{} : Bool},
1418 -meaning: Transforms.ReshapeMeaning(input, original, dimensions, result)) -> ReshapeInverseSuccessResult<input, result>:
1419 match result:
1420 case Fail{error}:
1421 ReshapeInverseSuccessResult{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1422 case Done{output}:
1423 ReshapeInverseSuccessResult{
1424 {\{Transforms.ReshapeOutput: shape => dims => shape_exact => count => linear =>
1425 {\{DynamicRestoreSuccess: success => success} : DynamicRestoreSuccess<input, output> ->
1426 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape_dynamic(output, Shape.dimensions(input))) == True{} : Bool}}(
1427 dynamic_restore_success(input, output,
1428 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(dimensions),
1429 Shape.logical_numel(Transforms.dynamic_dimensions(output)), count,
1430 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, dimensions, Transforms.dynamic_dimensions(output),
1431 Equal.sym(List<&2, U32>, Transforms.dynamic_dimensions(output), dimensions, dims)))))} :
1432 Transforms.ReshapeOutput<input, original, dimensions, output> ->
1433 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape_dynamic(output, Shape.dimensions(input))) == True{} : Bool}}(meaning)}
1434
1435def Laws.reshape_inverse_valid_success(input, target, source, same):
1436 Transforms.ReshapeInverseSuccessModel{
1437 {\{ReshapeInverseSuccessResult: success => success} :
1438 ReshapeInverseSuccessResult<input, Transforms.reshape(input, source, Shape.dimensions(target))> ->
1439 {Transforms.reshape_inverse_success(input, Transforms.reshape(input, source, Shape.dimensions(target))) == True{} : Bool}}(
1440 reshape_inverse_success_result(input, source, Shape.dimensions(target), Transforms.reshape(input, source, Shape.dimensions(target)),
1441 {\{Transforms.ReshapeSuccessModel: success => success} : Transforms.ReshapeSuccessModel<input, target, source> ->
1442 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape(input, source, Shape.dimensions(target))) == True{} : Bool}}(
1443 Laws.reshape_valid_success(input, target, source, same)),
1444 {\{Transforms.ReshapeModel: meaning => meaning} : Transforms.ReshapeModel<input, source, Shape.dimensions(target)> ->
1445 Transforms.ReshapeMeaning(input, source, Shape.dimensions(target), Transforms.reshape(input, source, Shape.dimensions(target)))}(
1446 Laws.reshape_result_interpretation(input, source, Shape.dimensions(target)))))}
1447
1448def Laws.permutation_valid_success(input, axes, valid):
1449 Totality.PlanSuccess{Mapping.plan_ranked_success(input, axes,
1450 Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), valid)}
1451
1452def read_success_status(-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32,
1453 certificate: ReadSuccessModel<shape, original, index>) -> Totality.ReadSuccess<shape, original, index>:
1454 Totality.ReadSuccess{
1455 {\{ReadSuccessModel: success =>
1456 {\{ReadSuccess: retained => value => exact =>
1457 Equal.sym(Bool, True{}, Totality.read_succeeded(shape, Core.read_flat(shape, original, index)),
1458 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Bool, Totality.read_succeeded(shape),
1459 (retained, Done{value}), Core.read_flat(shape, original, index), exact))} :
1460 ReadSuccess<shape, original, index> -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(success)} :
1461 ReadSuccessModel<shape, original, index> -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(certificate)}
1462
1463def Laws.tensor_read_valid_success(shape, source, index, inside):
1464 read_success_status(shape, source, index, read_success(shape, source, index, inside))
1465
1466def storage_write_succeeded(pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>) -> Bool:
1467 (storage, result) = pair
1468 Result.is_done(&2, &2, Storage.Error, Unit, result)
1469
1470type StorageWriteSuccess<-pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>> is Data:
1471 StorageWriteSuccess{-successful: {storage_write_succeeded(pair) == True{} : Bool}}
1472
1473def storage_set_checked_success(+depth: Nat, +length: Nat, +index: U32, +value: F32, allowed: Bool, array: Array<F32>,
1474 -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
1475 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
1476 -inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
1477 StorageWriteSuccess<Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid)>:
1478 match allowed:
1479 case False{}:
1480 StorageWriteSuccess{Empty.absurd({False{} == True{} : Bool},
1481 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), length), True{}, decision, inside)))}
1482 case True{}:
1483 StorageWriteSuccess{{==}}
1484
1485def write_result_status(-shape: Shape.Shape, -original: Storage.Storage,
1486 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
1487 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
1488 -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
1489 {Totality.write_succeeded(shape, Core.write_result(shape, original, valid, index, value, pair, same)) == storage_write_succeeded(pair) : Bool}:
1490 (storage, result) = pair
1491 match result:
1492 case Fail{error}:
1493 {==}
1494 case Done{unit}:
1495 {==}
1496
1497def tensor_write_success(+shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32,
1498 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Totality.WriteSuccess<shape, original, index, value>:
1499 Core.TTensor{storage, exact} = original
1500 match storage:
1501 case Storage.Empty{}:
1502 Totality.WriteSuccess{Empty.absurd({False{} == True{} : Bool},
1503 Arith.lt_zero(U32.to_nat(index),
1504 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1505 inside))}
1506 case Storage.Owned{+depth, +length, array, balanced, valid}:
1507 Totality.WriteSuccess{
1508 Equal.trans(Bool, Totality.write_succeeded(shape,
1509 Core.write_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index, value)),
1510 storage_write_succeeded(Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value)), True{},
1511 write_result_status(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, value,
1512 Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value), {==}),
1513 {\{StorageWriteSuccess: successful => successful} :
1514 StorageWriteSuccess<Storage.set_checked(depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid)> ->
1515 {storage_write_succeeded(Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value)) == True{} : Bool}}(
1516 storage_set_checked_success(depth, length, index, value, Nat.is_lt(U32.to_nat(index), length), array, {==}, balanced, valid,
1517 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1518 inside)))}
1519
1520def Laws.tensor_write_valid_success(shape, target, index, value, inside):
1521 tensor_write_success(shape, target, index, value, inside)
1522
1523def Laws.decoded_words_valid_success(shape, index, inside):
1524 Totality.WordsSuccess{Mapping.words_check_success(Shape.dimensions(shape),
1525 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index)), Mapping.decoded_words_valid(shape, index, inside))}
1526
1527def permutation_length_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1528 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
1529 wrong: {False{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool}) ->
1530 {Layout.plan_ranked(input, axes, decision) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1531 match decision:
1532 case Shape.BFalse{equal}:
1533 {==}
1534 case Shape.BTrue{equal}:
1535 Empty.absurd({Layout.plan_ranked(input, axes, Shape.BTrue{equal}) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1536 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), False{}, equal,
1537 Equal.sym(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), wrong))))
1538
1539def permutation_length_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1540 wrong: {False{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool}) ->
1541 {Layout.permutation(input, axes) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1542 permutation_length_decision_failure(input, axes,
1543 Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)
1544
1545def permutation_bounds_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1546 decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>, outside: {False{} == Layout.bounded(axes, Shape.rank(input)) : Bool}) ->
1547 {Layout.plan_bounded(input, axes, decision) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1548 match decision:
1549 case Shape.BFalse{equal}:
1550 {==}
1551 case Shape.BTrue{equal}:
1552 Empty.absurd({Layout.plan_bounded(input, axes, Shape.BTrue{equal}) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1553 Lifecycle.false_true(Equal.trans(Bool, True{}, Layout.bounded(axes, Shape.rank(input)), False{}, equal,
1554 Equal.sym(Bool, False{}, Layout.bounded(axes, Shape.rank(input)), outside))))
1555
1556def permutation_bounds_ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1557 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
1558 ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool},
1559 outside: {False{} == Layout.bounded(axes, Shape.rank(input)) : Bool}) ->
1560 {Layout.plan_ranked(input, axes, decision) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1561 match decision:
1562 case Shape.BFalse{equal}:
1563 Empty.absurd({Layout.plan_ranked(input, axes, Shape.BFalse{equal}) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1564 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, equal,
1565 Equal.sym(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), ranked))))
1566 case Shape.BTrue{equal}:
1567 permutation_bounds_decision_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside)
1568
1569def permutation_bounds_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1570 ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool},
1571 outside: {False{} == Layout.bounded(axes, Shape.rank(input)) : Bool}) ->
1572 {Layout.permutation(input, axes) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1573 permutation_bounds_ranked_failure(input, axes,
1574 Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked, outside)
1575
1576def permutation_unique_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1577 decision: Shape.BoolCase<Layout.unique(axes)>, duplicate: {False{} == Layout.unique(axes) : Bool}) ->
1578 {Layout.plan_unique(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1579 match decision:
1580 case Shape.BFalse{equal}:
1581 {==}
1582 case Shape.BTrue{equal}:
1583 Empty.absurd({Layout.plan_unique(input, axes, Shape.BTrue{equal}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1584 Lifecycle.false_true(Equal.trans(Bool, True{}, Layout.unique(axes), False{}, equal, Equal.sym(Bool, False{}, Layout.unique(axes), duplicate))))
1585
1586def permutation_duplicate_bounded_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1587 decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>, bounded: {True{} == Layout.bounded(axes, Shape.rank(input)) : Bool},
1588 duplicate: {False{} == Layout.unique(axes) : Bool}) ->
1589 {Layout.plan_bounded(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1590 match decision:
1591 case Shape.BFalse{equal}:
1592 Empty.absurd({Layout.plan_bounded(input, axes, Shape.BFalse{equal}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1593 Arith.clash(Equal.trans(Bool, False{}, Layout.bounded(axes, Shape.rank(input)), True{}, equal,
1594 Equal.sym(Bool, True{}, Layout.bounded(axes, Shape.rank(input)), bounded))))
1595 case Shape.BTrue{equal}:
1596 permutation_unique_decision_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)
1597
1598def permutation_duplicate_ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1599 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
1600 ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool},
1601 bounded: {True{} == Layout.bounded(axes, Shape.rank(input)) : Bool}, duplicate: {False{} == Layout.unique(axes) : Bool}) ->
1602 {Layout.plan_ranked(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1603 match decision:
1604 case Shape.BFalse{equal}:
1605 Empty.absurd({Layout.plan_ranked(input, axes, Shape.BFalse{equal}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
1606 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, equal,
1607 Equal.sym(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), ranked))))
1608 case Shape.BTrue{equal}:
1609 permutation_duplicate_bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded, duplicate)
1610
1611def permutation_duplicate_failure(+input: Shape.Shape, +axes: List<&2, U32>,
1612 ranked: {True{} == Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) : Bool},
1613 bounded: {True{} == Layout.bounded(axes, Shape.rank(input)) : Bool}, duplicate: {False{} == Layout.unique(axes) : Bool}) ->
1614 {Layout.permutation(input, axes) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
1615 permutation_duplicate_ranked_failure(input, axes,
1616 Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked, bounded, duplicate)
1617
1618def permute_failure(+input: Shape.Shape, -source: Core.Tensor<input>, +axes: List<&2, U32>, +error: Layout.Error,
1619 certificate: {Layout.permutation(input, axes) == Fail{error} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}) ->
1620 Totality.PermuteFailure<input, axes, source, error>:
1621 Totality.PermuteFailure{Equal.cong(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>,
1622 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, result => Transforms.copy_planned(input, axes, source, result),
1623 Layout.permutation(input, axes), Fail{error}, certificate)}
1624
1625def Laws.permute_axes_length_rejection(input, source, axes, wrong):
1626 Totality.PermuteFailure{
1627 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure<input, axes, source, Layout.AxesLengthMismatch{}> ->
1628 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.AxesLengthMismatch{}}}) :
1629 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}}(
1630 permute_failure(input, source, axes, Layout.AxesLengthMismatch{}, permutation_length_failure(input, axes, wrong)))}
1631
1632def Laws.permute_axis_bounds_rejection(input, source, axes, ranked, outside):
1633 Totality.PermuteFailure{
1634 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure<input, axes, source, Layout.AxisOutOfBounds{}> ->
1635 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) :
1636 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}}(
1637 permute_failure(input, source, axes, Layout.AxisOutOfBounds{}, permutation_bounds_failure(input, axes, ranked, outside)))}
1638
1639def Laws.permute_duplicate_axes_rejection(input, source, axes, ranked, bounded, duplicate):
1640 Totality.PermuteFailure{
1641 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure<input, axes, source, Layout.DuplicateAxis{}> ->
1642 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.DuplicateAxis{}}}) :
1643 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}}(
1644 permute_failure(input, source, axes, Layout.DuplicateAxis{}, permutation_duplicate_failure(input, axes, ranked, bounded, duplicate)))}
1645
1646type TransposeDecidedFailure<-input: Shape.Shape, -source: Core.Tensor<input>, -a: U32, -b: U32,
1647 -decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>> is Data:
1648 TransposeDecidedFailure{-exact: {Transforms.transpose_decided(input, source, a, b, decision) ==
1649 (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}}
1650
1651def transpose_decided_failure(+input: Shape.Shape, +a: U32, +b: U32,
1652 decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>, source: Core.Tensor<input>,
1653 -outside: {False{} == TransposeSpec.valid(input, a, b) : Bool}) ->
1654 TransposeDecidedFailure<input, source, a, b, decision>:
1655 match decision:
1656 case Shape.BFalse{equal}:
1657 TransposeDecidedFailure{{==}}
1658 case Shape.BTrue{equal}:
1659 TransposeDecidedFailure{Empty.absurd({Transforms.transpose_decided(input, source, a, b, Shape.BTrue{equal}) ==
1660 (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
1661 Lifecycle.false_true(Equal.trans(Bool, True{}, TransposeSpec.valid(input, a, b), False{}, equal,
1662 Equal.sym(Bool, False{}, TransposeSpec.valid(input, a, b), outside))))}
1663
1664def Laws.transpose_axis_bounds_rejection(input, source, a, b, outside):
1665 Totality.TransposeFailure{
1666 {\{TransposeDecidedFailure: exact => exact} :
1667 TransposeDecidedFailure<input, source, a, b, Shape.bool_case(TransposeSpec.valid(input, a, b))> ->
1668 {Transforms.transpose_copy(input, source, a, b) == (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) :
1669 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}}(
1670 transpose_decided_failure(input, a, b, Shape.bool_case(TransposeSpec.valid(input, a, b)), source, outside))}
1671
1672def reshape_decided_failure(+input: Shape.Shape, +target: Shape.Shape,
1673 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(target))>, -source: Core.Tensor<input>,
1674 different: {False{} == Nat.is_eq(Shape.elements(input), Shape.elements(target)) : Bool}) ->
1675 {Transforms.reshape_decided(input, target, source, decision) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} :
1676 Result<&2, &1, Transforms.Error, Core.Dynamic>}:
1677 match decision:
1678 case Shape.BFalse{equal}:
1679 {==}
1680 case Shape.BTrue{equal}:
1681 Empty.absurd({Transforms.reshape_decided(input, target, source, Shape.BTrue{equal}) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} :
1682 Result<&2, &1, Transforms.Error, Core.Dynamic>},
1683 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(Shape.elements(input), Shape.elements(target)), False{}, equal,
1684 Equal.sym(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(target)), different))))
1685
1686def reshape_built_failure(+input: Shape.Shape, +target: Shape.Shape, built: Shape.ConstructResult<Shape.dimensions(target)>, -source: Core.Tensor<input>,
1687 different: {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) : Bool},
1688 complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}) ->
1689 {Transforms.reshape_built(input, source, Shape.dimensions(target), built) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} :
1690 Result<&2, &1, Transforms.Error, Core.Dynamic>}:
1691 match built:
1692 case Shape.SError{error}:
1693 Empty.absurd({Transforms.reshape_built(input, source, Shape.dimensions(target), Shape.SError{error}) ==
1694 Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>},
1695 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Mapping.metadata_present, None{}, Some{Shape.dimensions(target)}, complete)))
1696 case Shape.SBuilt{+output, preserved}:
1697 reshape_decided_failure(input, output, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), source,
1698 %Equal.sym(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements_exact(input)) :
1699 {False{} == Nat.is_eq(_, Shape.elements(output)) : Bool}
1700 %Equal.sym(Nat, Shape.elements(output), Shape.logical_numel(Shape.dimensions(output)), Shape.elements_exact(output)) :
1701 {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), _) : Bool}
1702 %Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved) :
1703 {False{} == Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(_)) : Bool}
1704 different)
1705
1706def Laws.reshape_element_count_rejection(input, target, source, different):
1707 Totality.ReshapeFailure{reshape_built_failure(input, target, Shape.construct(Shape.dimensions(target)), source, different, shape_construct_complete(target))}
1708
1709def mapping_decided_failure(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
1710 decision: Shape.BoolCase<U32.is_lt(index, Shape.count(Layout.output(input, axes, plan)))>,
1711 outside: {False{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1712 {Layout.map_decided(input, axes, plan, index, decision) == Fail{Layout.ShapeError{Shape.FlatIndexOutOfBounds{}}} :
1713 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}:
1714 match decision:
1715 case Shape.BFalse{equal}:
1716 {==}
1717 case Shape.BTrue{equal}:
1718 Empty.absurd({Layout.map_decided(input, axes, plan, index, Shape.BTrue{equal}) == Fail{Layout.ShapeError{Shape.FlatIndexOutOfBounds{}}} :
1719 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
1720 Lifecycle.false_true(Equal.trans(Bool, True{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), False{}, equal,
1721 Equal.sym(Bool, False{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), outside))))
1722
1723def Laws.mapping_index_rejection(input, axes, plan, index, outside):
1724 mapping_decided_failure(input, axes, plan, index, Shape.bool_case(U32.is_lt(index, Shape.count(Layout.output(input, axes, plan)))), outside)
1725
1726def words_naturals(+values: List<&2, U32>) -> {Shape.words(Shape.naturals(values)) == values : List<&2, U32>}:
1727 match values:
1728 case Nil{}:
1729 {==}
1730 case +head <> +tail:
1731 %Equal.sym(U32, U32.from_nat(U32.to_nat(head)), head, WordConversion.word_natural_exact(head)) :
1732 {_ <> Shape.words(Shape.naturals(tail)) == head <> tail : List<&2, U32>}
1733 Equal.cong(List<&2, U32>, List<&2, U32>, rest => head <> rest, Shape.words(Shape.naturals(tail)), tail, words_naturals(tail))
1734
1735def digits_offset(+dimensions: List<&2, Nat>, +values: List<&2, Nat>, +fits: Coordinates.Fits(dimensions, values)) ->
1736 {Shape.digits(dimensions, Shape.offset(dimensions, values)) == values : List<&2, Nat>}:
1737 %Equal.trans(Nat, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1738 Shape.row_major(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), Shape.offset(dimensions, values),
1739 ShapeIndex.flatten_row_major(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), Coordinates.offset_of(dimensions, values, fits)) :
1740 {Shape.digits(dimensions, _) == values : List<&2, Nat>}
1741 Equal.trans(List<&2, Nat>,
1742 Shape.digits(dimensions, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1743 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))), values,
1744 Equal.sym(List<&2, Nat>,
1745 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1746 Shape.digits(dimensions, Shape.Fin.value(Shape.numel(dimensions), Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1747 Coordinates.digits_unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1748 Equal.trans(List<&2, Nat>,
1749 Shape.indices(dimensions, Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits)))),
1750 Shape.indices(dimensions, Coordinates.coordinate_of(dimensions, values, fits)), values,
1751 Equal.cong(Shape.Coordinate(dimensions), List<&2, Nat>, Shape.indices(dimensions),
1752 Shape.unflatten(dimensions, Shape.flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1753 Coordinates.coordinate_of(dimensions, values, fits), ShapeIndex.unflatten_flatten(dimensions, Coordinates.coordinate_of(dimensions, values, fits))),
1754 Coordinates.indices_of(dimensions, values, fits)))
1755
1756def Laws.codec_decode_flatten(shape, values, valid):
1757 Equal.trans(List<&2, U32>,
1758 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), Layout.flatten_words(Shape.dimensions(shape), values, 0))),
1759 Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)))), values,
1760 Mapping.codec_decoded(Shape.dimensions(shape), Layout.flatten_words(Shape.dimensions(shape), values, 0)),
1761 Equal.trans(List<&2, U32>, Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)))),
1762 Shape.words(Shape.naturals(values)), values,
1763 Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words,
1764 Shape.digits(Shape.extents(shape), U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0))), Shape.naturals(values),
1765 Equal.trans(List<&2, Nat>, Shape.digits(Shape.extents(shape), U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0))),
1766 Shape.digits(Shape.extents(shape), Shape.offset(Shape.extents(shape), Shape.naturals(values))), Shape.naturals(values),
1767 Equal.cong(Nat, List<&2, Nat>, offset => Shape.digits(Shape.extents(shape), offset), U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)),
1768 Shape.offset(Shape.extents(shape), Shape.naturals(values)), Mapping.coordinate_flatten_exact(shape, values, valid)),
1769 digits_offset(Shape.extents(shape), Shape.naturals(values), Mapping.coordinate_fits(Shape.dimensions(shape), values, valid)))),
1770 words_naturals(values)))
1771
1772def Laws.mapping_valid_success(input, axes, plan, index, inside):
1773 Totality.MappingSuccess{Mapping.mapping_decided_success(input, axes, plan, index,
1774 Shape.bool_case(U32.is_lt(index, Shape.count(Layout.output(input, axes, plan)))), inside)}
1775
1776def Laws.natural_cursor_exact_conversion(shape, cursor, within):
1777 Transforms.CursorExact{Mapping.cursor_word_exact(shape, cursor, within)}
1778
1779def copy_written_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
1780 pair: Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &2, Core.Error, Unit>, -source: Core.Tensor<input>,
1781 -successful: {Totality.write_succeeded(Layout.output(input, axes, plan), pair) == True{} : Bool}) ->
1782 Totality.CopySuccess<input, axes, plan,
1783 Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), source, pair)>:
1784 (target, result) = pair
1785 match result:
1786 case Fail{error}:
1787 Totality.CopySuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1788 case Done{unit}:
1789 Totality.CopySuccess{{==}}
1790
1791def copy_value_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
1792 -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>, +value: F32,
1793 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1794 Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1795 source => target => (source, Done{target}), target, (source, Done{value}))>:
1796 copy_written_success(input, axes, plan, Core.write_flat(Layout.output(input, axes, plan), target, index, value), source,
1797 {\{Totality.WriteSuccess: successful => successful} :
1798 Totality.WriteSuccess<Layout.output(input, axes, plan), target, index, value> ->
1799 {Totality.write_succeeded(Layout.output(input, axes, plan), Core.write_flat(Layout.output(input, axes, plan), target, index, value)) == True{} : Bool}}(
1800 tensor_write_success(Layout.output(input, axes, plan), target, index, value,
1801 Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))),
1802 %Shape.elements_exact(Layout.output(input, axes, plan)) :
1803 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
1804 %WordConversion.shape_count_exact(Layout.output(input, axes, plan)) :
1805 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
1806 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(Layout.output(input, axes, plan)))),
1807 U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), Arith.u32_lt(index, Shape.count(Layout.output(input, axes, plan)))) :
1808 {True{} == _ : Bool}
1809 inside))))
1810
1811def copy_read_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32, +source_index: U32,
1812 -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
1813 certificate: ReadSuccessModel<input, source, source_index>,
1814 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1815 Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1816 source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))>:
1817 Totality.CopySuccess{
1818 {\{ReadSuccessModel: success =>
1819 {\{ReadSuccess: retained => value => exact =>
1820 %exact : {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1821 source => target => (source, Done{target}), target, _)) == True{} : Bool}
1822 {\{Totality.CopySuccess: successful => successful} :
1823 Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1824 source => target => (source, Done{target}), target, (retained, Done{value}))> ->
1825 {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1826 source => target => (source, Done{target}), target, (retained, Done{value}))) == True{} : Bool}}(
1827 copy_value_success(input, axes, plan, index, retained, target, value, inside))} :
1828 ReadSuccess<input, source, source_index> ->
1829 {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1830 source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(success)} :
1831 ReadSuccessModel<input, source, source_index> ->
1832 {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1833 source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(certificate)}
1834
1835def copy_mapped_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
1836 mapped: Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
1837 source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
1838 +successful: {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, mapped) == True{} : Bool},
1839 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1840 Totality.CopySuccess<input, axes, plan, Transforms.copy_mapped(input, axes, plan, index,
1841 source => target => (source, Done{target}), source, target, mapped)>:
1842 match mapped:
1843 case Fail{error}:
1844 Totality.CopySuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1845 case Done{+mapping}:
1846 copy_read_success(input, axes, plan, index, Layout.source_index(input, axes, plan, index, mapping), source, target,
1847 read_success(input, source, Layout.source_index(input, axes, plan, index, mapping),
1848 Laws.mapped_mathematical_bounded(input, axes, plan, index, mapping)), inside)
1849
1850def Laws.copy_step_valid_success(input, axes, plan, source, target, index, inside):
1851 Totality.CopyStepSuccess{
1852 {\{Totality.CopySuccess: successful => successful} :
1853 Totality.CopySuccess<input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index)> ->
1854 {Totality.copy_succeeded(input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index)) == True{} : Bool}}(
1855 copy_mapped_success(input, axes, plan, index, Layout.map_index(input, axes, plan, index), source, target,
1856 {\{Totality.MappingSuccess: successful => successful} :
1857 Totality.MappingSuccess<input, axes, plan, index> ->
1858 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, Layout.map_index(input, axes, plan, index)) == True{} : Bool}}(
1859 Laws.mapping_valid_success(input, axes, plan, index, inside)), inside))}
1860
1861def natural_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat, +index: U32,
1862 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
1863 -candidate: {index == U32.from_nat(cursor) : U32}, -word_exact: {U32.to_nat(index) == cursor : Nat},
1864 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1865 Totality.NaturalSuccess<input, axes, plan, cursor, Transforms.natural_decided(input, axes, plan, cursor, index, source, target, candidate, decision)>:
1866 match decision:
1867 case Shape.BFalse{equal}:
1868 Totality.NaturalSuccess{Empty.absurd({False{} == True{} : Bool},
1869 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(U32.to_nat(index), cursor), True{}, equal, Mapping.natural_equal_true(U32.to_nat(index), cursor, word_exact))))}
1870 case Shape.BTrue{equal}:
1871 Totality.NaturalSuccess{
1872 {\{Totality.CopyStepSuccess: successful => successful} :
1873 Totality.CopyStepSuccess<input, axes, plan, source, target, index> ->
1874 {Totality.copy_succeeded(input, axes, plan, Transforms.copy_step(input, axes, plan, source, target, index)) == True{} : Bool}}(
1875 Laws.copy_step_valid_success(input, axes, plan, source, target, index, inside))}
1876
1877def Laws.natural_step_valid_success(input, axes, plan, cursor, source, target, inside):
1878 natural_decided_success(input, axes, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), source, target,
1879 {==}, Mapping.cursor_word_exact(Layout.output(input, axes, plan), cursor,
1880 WordConversion.lt_le(cursor, Shape.elements(Layout.output(input, axes, plan)), Equal.sym(Bool, True{}, Nat.is_lt(cursor, Shape.elements(Layout.output(input, axes, plan))), inside))),
1881 Mapping.cursor_index_bounded(Layout.output(input, axes, plan), cursor, inside))
1882
1883def add_cursor_le(+fuel: Nat, +cursor: Nat) -> {Nat.is_le(cursor, Nat.add(fuel, cursor)) == True{} : Bool}:
1884 match fuel:
1885 case 0n:
1886 WordConversion.le_reflexive(cursor)
1887 case 1n+remaining:
1888 Arith.le_succ(cursor, Nat.add(remaining, cursor), add_cursor_le(remaining, cursor))
1889
1890def loop_pair_success(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
1891 pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
1892 -successful: {Totality.copy_succeeded(input, axes, plan, pair) == True{} : Bool},
1893 rec: @source: Core.Tensor<input> -> @target: Core.Tensor<Layout.output(input, axes, plan)> ->
1894 Totality.CopySuccess<input, axes, plan, Transforms.copy_loop(fuel, input, axes, plan, source, target, cursor)>) ->
1895 Totality.CopySuccess<input, axes, plan, Transforms.copy_next(input, axes, plan,
1896 source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, cursor), pair)>:
1897 (source, result) = pair
1898 match result:
1899 case Fail{error}:
1900 Totality.CopySuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1901 case Done{target}:
1902 rec(source)(target)
1903
1904def loop_natural_success(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
1905 result: Transforms.NaturalCopy<input, axes, plan, cursor>,
1906 -successful: {Totality.natural_succeeded(input, axes, plan, cursor, result) == True{} : Bool},
1907 rec: @source: Core.Tensor<input> -> @target: Core.Tensor<Layout.output(input, axes, plan)> ->
1908 Totality.CopySuccess<input, axes, plan, Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor)>) ->
1909 Totality.CopySuccess<input, axes, plan, Transforms.natural_next(input, axes, plan, cursor,
1910 source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor), result)>:
1911 match result:
1912 case Transforms.NaturalError{source}:
1913 Totality.CopySuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1914 case Transforms.NaturalCopied{pair, index, exact, candidate}:
1915 loop_pair_success(fuel, input, axes, plan, 1n+cursor, pair, successful, rec)
1916
1917def Laws.copy_loop_valid_success(fuel, input, axes, plan, cursor, source, target, within):
1918 match fuel:
1919 case 0n:
1920 Totality.CopySuccess{{==}}
1921 case 1n++remaining:
1922 loop_natural_success(remaining, input, axes, plan, cursor, Transforms.natural_step(input, axes, plan, cursor, source, target),
1923 {\{Totality.NaturalSuccess: successful => successful} :
1924 Totality.NaturalSuccess<input, axes, plan, cursor, Transforms.natural_step(input, axes, plan, cursor, source, target)> ->
1925 {Totality.natural_succeeded(input, axes, plan, cursor, Transforms.natural_step(input, axes, plan, cursor, source, target)) == True{} : Bool}}(
1926 Laws.natural_step_valid_success(input, axes, plan, cursor, source, target,
1927 Equal.sym(Bool, Nat.is_lt(cursor, Shape.elements(Layout.output(input, axes, plan))), True{},
1928 Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(Layout.output(input, axes, plan)),
1929 Arith.lt_succ(cursor, Nat.add(remaining, cursor), add_cursor_le(remaining, cursor)), within)))),
1930 source => target => Laws.copy_loop_valid_success(remaining, input, axes, plan, 1n+cursor, source, target,
1931 %Equal.sym(Nat, Nat.add(remaining, 1n+cursor), 1n+Nat.add(remaining, cursor), Arith.add_succ(remaining, cursor)) :
1932 {Nat.is_le(_, Shape.elements(Layout.output(input, axes, plan))) == True{} : Bool}
1933 within))
1934
1935def packed_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
1936 pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
1937 -successful: {Totality.copy_succeeded(input, axes, plan, pair) == True{} : Bool}) ->
1938 Totality.PublicSuccess<input, Transforms.copy_pack(input, axes, plan, pair)>:
1939 (source, result) = pair
1940 match result:
1941 case Fail{error}:
1942 Totality.PublicSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1943 case Done{target}:
1944 Totality.PublicSuccess{{==}}
1945
1946def allocated_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
1947 allocated: Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>, source: Core.Tensor<input>,
1948 -certificate: AllocationSpec.TensorDone<Layout.output(input, axes, plan), allocated>) ->
1949 Totality.PublicSuccess<input, Transforms.copy_allocated(input, axes, plan, source, allocated)>:
1950 match allocated:
1951 case Fail{error}:
1952 Totality.PublicSuccess{
1953 {\{AllocationSpec.TensorDone: tensor => same =>
1954 Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>, Bool,
1955 Result.is_done(&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>), Done{tensor}, Fail{error}, same)))} :
1956 AllocationSpec.TensorDone<Layout.output(input, axes, plan), Fail{error}> -> {False{} == True{} : Bool}}(certificate)}
1957 case Done{target}:
1958 packed_success(input, axes, plan, Transforms.built(input, axes, plan, source, target),
1959 {\{PermuteBuild.Fact: successful => successful} :
1960 PermuteBuild.Fact<{Totality.copy_succeeded(input, axes, plan, Transforms.built(input, axes, plan, source, target)) == True{} : Bool}> ->
1961 {Totality.copy_succeeded(input, axes, plan, Transforms.built(input, axes, plan, source, target)) == True{} : Bool}}(
1962 PermuteBuild.built_success(input, axes, plan, source, target)))
1963
1964def planned_success(+input: Shape.Shape, +axes: List<&2, U32>, planned: Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, source: Core.Tensor<input>,
1965 -successful: {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, planned) == True{} : Bool}) ->
1966 Totality.PublicSuccess<input, Transforms.copy_planned(input, axes, source, planned)>:
1967 match planned:
1968 case Fail{error}:
1969 Totality.PublicSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
1970 case Done{+plan}:
1971 allocated_success(input, axes, plan, Core.new(Layout.output(input, axes, plan), 0.0), source,
1972 AllocationProof.core_new_done(Layout.output(input, axes, plan), 0.0))
1973
1974def Laws.permute_valid_success(input, source, axes, valid):
1975 planned_success(input, axes, Layout.permutation(input, axes), source,
1976 {\{Totality.PlanSuccess: successful => successful} : Totality.PlanSuccess<input, axes> ->
1977 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.permutation(input, axes)) == True{} : Bool}}(
1978 Laws.permutation_valid_success(input, axes, valid)))
1979
1980def words_bounded_exact(+values: List<&2, Nat>, +rank: U32,
1981 +bounded: {True{} == Axis.bounded(values, U32.to_nat(rank)) : Bool}) ->
1982 {Shape.naturals(Shape.words(values)) == values : List<&2, Nat>}:
1983 match values:
1984 case Nil{}:
1985 {==}
1986 case +head <> +tail:
1987 %Equal.sym(Nat, U32.to_nat(U32.from_nat(head)), head,
1988 WordConversion.natural_word_exact(head, rank,
1989 WordConversion.lt_le(head, U32.to_nat(rank), Equal.sym(Bool, True{}, Nat.is_lt(head, U32.to_nat(rank)),
1990 Mapping.and_left(Nat.is_lt(head, U32.to_nat(rank)), Axis.bounded(tail, U32.to_nat(rank)), bounded))))) :
1991 {_ <> Shape.naturals(Shape.words(tail)) == head <> tail : List<&2, Nat>}
1992 Equal.cong(List<&2, Nat>, List<&2, Nat>, rest => head <> rest, Shape.naturals(Shape.words(tail)), tail,
1993 words_bounded_exact(tail, rank, Mapping.and_right(Nat.is_lt(head, U32.to_nat(rank)), Axis.bounded(tail, U32.to_nat(rank)), bounded)))
1994
1995def inverse_axes_naturals(+input: Shape.Shape, +axes: List<&2, U32>, +accepted: {True{} == Layout.bijective(input, axes) : Bool}) ->
1996 {Shape.naturals(Totality.inverse_axes(input, axes)) == Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)) : List<&2, Nat>}:
1997 words_bounded_exact(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank(input),
1998 %Equal.sym(Nat, U32.to_nat(Shape.rank(input)), Shape.rank_dimensions(Shape.dimensions(input)), AxisAlgebra.rank_exact(input)) :
1999 {True{} == Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), _) : Bool}
2000 Mapping.and_left(Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(input))),
2001 Axis.unique(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
2002 Mapping.and_right(Nat.is_eq(List.length(&2, Nat, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.rank_dimensions(Shape.dimensions(input))),
2003 Bool.and(Axis.bounded(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(input))),
2004 Axis.unique(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
2005 AxisAlgebra.facts_inverse_valid(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), AxisAlgebra.shape_facts(input, axes, accepted)))))
2006
2007def native_axes_valid(+shape: Shape.Shape, +axes: List<&2, U32>,
2008 accepted: {True{} == Axis.valid(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(axes)) : Bool}) ->
2009 {True{} == Layout.bijective(shape, axes) : Bool}:
2010 %Equal.sym(Nat, Shape.rank_dimensions(axes), List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_naturals(axes)) :
2011 {True{} == Bool.and(Nat.is_eq(_, Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Layout.bounded(axes, Shape.rank(shape)), Layout.unique(axes))) : Bool}
2012 %Equal.sym(Bool, Layout.unique(axes), Axis.unique(Shape.naturals(axes)), AxisAlgebra.unique(axes)) :
2013 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Layout.bounded(axes, Shape.rank(shape)), _)) : Bool}
2014 %Equal.sym(Bool, Layout.bounded(axes, Shape.rank(shape)), Axis.bounded(Shape.naturals(axes), U32.to_nat(Shape.rank(shape))), AxisAlgebra.bounded(axes, Shape.rank(shape))) :
2015 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(_, Axis.unique(Shape.naturals(axes)))) : Bool}
2016 %Equal.sym(Nat, U32.to_nat(Shape.rank(shape)), Shape.rank_dimensions(Shape.dimensions(shape)), AxisAlgebra.rank_exact(shape)) :
2017 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Axis.bounded(Shape.naturals(axes), _), Axis.unique(Shape.naturals(axes)))) : Bool}
2018 accepted
2019
2020def Laws.inverse_axes_valid(input, axes, plan):
2021 native_axes_valid(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes),
2022 %Equal.sym(List<&2, Nat>, Shape.naturals(Totality.inverse_axes(input, axes)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)),
2023 inverse_axes_naturals(input, axes, Laws.permutation_checked(input, axes, plan))) :
2024 {True{} == Axis.valid(Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))), _) : Bool}
2025 %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))), Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, axes, plan)) :
2026 {True{} == Axis.valid(_, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))) : Bool}
2027 AxisAlgebra.facts_inverse_valid(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes),
2028 AxisAlgebra.shape_facts(input, axes, Laws.permutation_checked(input, axes, plan))))
2029
2030def Laws.inverse_permutation_dimensions(input, axes, plan, inverse):
2031 Equal.trans(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)),
2032 Axis.order(U32, Shape.dimensions(Layout.output(input, axes, plan)), Shape.naturals(Totality.inverse_axes(input, axes))), Shape.dimensions(input),
2033 Mapping.permutation_dimensions_order(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse),
2034 %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(input, axes, plan)), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
2035 Mapping.permutation_dimensions_order(input, axes, plan)) :
2036 {Axis.order(U32, _, Shape.naturals(Totality.inverse_axes(input, axes))) == Shape.dimensions(input) : List<&2, U32>}
2037 %Equal.sym(List<&2, Nat>, Shape.naturals(Totality.inverse_axes(input, axes)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)),
2038 inverse_axes_naturals(input, axes, Laws.permutation_checked(input, axes, plan))) :
2039 {Axis.order(U32, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), _) == Shape.dimensions(input) : List<&2, U32>}
2040 AxisAlgebra.inverse_composition(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Shape.dimensions(input), Mapping.shape_rank_bound(input),
2041 AxisAlgebra.valid(input, axes, Laws.permutation_checked(input, axes, plan)), AxisAlgebra.word_length(Shape.dimensions(input))))
2042
2043def mapping_input_valid(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2044 mapping: Layout.Mapping<input, axes, plan, index>) -> Layout.WordsValid(Shape.dimensions(input), Layout.input_words(input, axes, plan, index, mapping)):
2045 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
2046 Layout.CWord{values, valid} = ic
2047 valid
2048
2049def mapping_input_order(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2050 mapping: Layout.Mapping<input, axes, plan, index>) ->
2051 {Layout.input_words(input, axes, plan, index, mapping) == Axis.order(U32, Layout.output_words(input, axes, plan, index, mapping),
2052 Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))) : List<&2, U32>}:
2053 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
2054 Mapping.inverse_words_order(input, axes, plan, oc, Layout.coordinate_values(input, ic), inverse)
2055
2056def mapping_output_decoded(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2057 mapping: Layout.Mapping<input, axes, plan, index>) ->
2058 {Layout.output_words(input, axes, plan, index, mapping) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}:
2059 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
2060 decoded
2061
2062def mapping_output_mathematical_bounded(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2063 mapping: Layout.Mapping<input, axes, plan, index>) ->
2064 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}:
2065 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
2066 %requested : {Nat.is_lt(U32.to_nat(_), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}
2067 Mapping.flat_mathematical_bounded(Layout.output(input, axes, plan), oi)
2068
2069def mapping_order_forward(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2070 +mapping: Layout.Mapping<input, axes, plan, index>) ->
2071 {Axis.order(U32, Layout.input_words(input, axes, plan, index, mapping), Shape.naturals(axes)) == Layout.output_words(input, axes, plan, index, mapping) : List<&2, U32>}:
2072 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32),
2073 Axis.gather(U32, Layout.input_words(input, axes, plan, index, mapping), Shape.naturals(axes)), Some{Layout.output_words(input, axes, plan, index, mapping)},
2074 Equal.trans(Maybe<&2, List<&2, U32>>, Axis.gather(U32, Layout.input_words(input, axes, plan, index, mapping), Shape.naturals(axes)),
2075 Layout.reorder(Layout.input_words(input, axes, plan, index, mapping), axes), Some{Layout.output_words(input, axes, plan, index, mapping)},
2076 Equal.sym(Maybe<&2, List<&2, U32>>, Layout.reorder(Layout.input_words(input, axes, plan, index, mapping), axes),
2077 Axis.gather(U32, Layout.input_words(input, axes, plan, index, mapping), Shape.naturals(axes)), AxisAlgebra.reorder(axes, Layout.input_words(input, axes, plan, index, mapping))),
2078 Laws.inverse_coordinate_roundtrip(input, axes, plan, index, mapping)))
2079
2080def mapping_coordinates_join(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2081 +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>, +index: U32,
2082 +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>,
2083 +first: Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>) ->
2084 {Layout.output_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first) ==
2085 Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second) : List<&2, U32>}:
2086 Equal.trans(List<&2, U32>, Layout.output_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2087 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))),
2088 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
2089 Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2090 mapping_output_decoded(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2091 %Equal.sym(U32, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2092 Layout.flatten_words(Shape.dimensions(Layout.output(input, axes, plan)), Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), 0),
2093 Laws.mapped_flat(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) :
2094 {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), _)) ==
2095 Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second) : List<&2, U32>}
2096 Laws.codec_decode_flatten(Layout.output(input, axes, plan), Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2097 mapping_input_valid(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)))
2098
2099def inverse_mapping_coordinates(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2100 +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>, +index: U32,
2101 +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>,
2102 +first: Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>) ->
2103 {Layout.input_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first) ==
2104 Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second) : List<&2, U32>}:
2105 Equal.trans(List<&2, U32>, Layout.input_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2106 Axis.order(U32, Layout.output_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2107 Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
2108 Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2109 mapping_input_order(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2110 %Equal.sym(List<&2, U32>, Layout.output_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2111 Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), mapping_coordinates_join(input, axes, plan, inverse, index, second, first)) :
2112 {Axis.order(U32, _, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))) ==
2113 Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second) : List<&2, U32>}
2114 %inverse_axes_naturals(input, axes, Laws.permutation_checked(input, axes, plan)) :
2115 {Axis.order(U32, Layout.input_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), _) ==
2116 Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second) : List<&2, U32>}
2117 mapping_order_forward(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))
2118
2119def Laws.inverse_mapping_restores_index(input, axes, plan, inverse, index, second, first):
2120 Equal.trans(U32, Layout.source_index(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2121 Layout.flatten_words(Shape.dimensions(input), Layout.input_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first), 0), index,
2122 Laws.mapped_flat(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2123 %Equal.sym(List<&2, U32>, Layout.input_words(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first),
2124 Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), inverse_mapping_coordinates(input, axes, plan, inverse, index, second, first)) :
2125 {Layout.flatten_words(Shape.dimensions(input), _, 0) == index : U32}
2126 %Equal.sym(List<&2, U32>, Layout.output_words(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2127 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse))), index)),
2128 mapping_output_decoded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) :
2129 {Layout.flatten_words(Shape.dimensions(input), _, 0) == index : U32}
2130 %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)), Shape.dimensions(input),
2131 Laws.inverse_permutation_dimensions(input, axes, plan, inverse)) :
2132 {Layout.flatten_words(Shape.dimensions(input), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(_), index)), 0) == index : U32}
2133 Laws.codec_flatten_decode(input, index,
2134 %Equal.sym(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements_exact(input)) :
2135 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
2136 %Laws.inverse_permutation_dimensions(input, axes, plan, inverse) :
2137 {True{} == Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) : Bool}
2138 Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)))), True{},
2139 mapping_output_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))))
2140
2141def typed_permutation_impossible(-input: Shape.Shape, -axes: List<&2, U32>, -original: Core.Tensor<input>,
2142 -pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, -empty: Empty) -> Totality.TypedPermutation<input, axes, original, pair>:
2143 Totality.TypedPermutation{Empty.absurd(Layout.Plan<input, axes>, empty), Empty.absurd(Core.Tensor<input>, empty),
2144 Empty.absurd(Core.Tensor<Layout.output(input, axes, Empty.absurd(Layout.Plan<input, axes>, empty))>, empty),
2145 Empty.absurd({(Empty.absurd(Core.Tensor<input>, empty), Done{Core.Packed{Layout.output(input, axes, Empty.absurd(Layout.Plan<input, axes>, empty)),
2146 Empty.absurd(Core.Tensor<Layout.output(input, axes, Empty.absurd(Layout.Plan<input, axes>, empty))>, empty)}}) == pair :
2147 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}, empty),
2148 Empty.absurd(Transforms.Prefix<input, axes, Empty.absurd(Layout.Plan<input, axes>, empty), original, Empty.absurd(Core.Tensor<input>, empty),
2149 Empty.absurd(Core.Tensor<Layout.output(input, axes, Empty.absurd(Layout.Plan<input, axes>, empty))>, empty),
2150 Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, Empty.absurd(Layout.Plan<input, axes>, empty))))>, empty)}
2151
2152def typed_built_result(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>,
2153 -initial_target: Core.Tensor<Layout.output(input, axes, plan)>,
2154 pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
2155 -exact: {pair == Transforms.built(input, axes, plan, original, initial_target) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
2156 -meaning: Transforms.LoopMeaning(input, axes, plan, original, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), pair),
2157 -successful: {Totality.copy_succeeded(input, axes, plan, pair) == True{} : Bool}) ->
2158 Totality.TypedPermutation<input, axes, original, Transforms.copy_pack(input, axes, plan, Transforms.built(input, axes, plan, original, initial_target))>:
2159 (retained, result) = pair
2160 match result:
2161 case Fail{error}:
2162 typed_permutation_impossible(input, axes, original, Transforms.copy_pack(input, axes, plan,
2163 Transforms.built(input, axes, plan, original, initial_target)), Arith.clash(successful))
2164 case Done{target}:
2165 Totality.TypedPermutation{plan, retained, target,
2166 Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
2167 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.copy_pack(input, axes, plan),
2168 (retained, Done{target}), Transforms.built(input, axes, plan, original, initial_target), exact),
2169 meaning}
2170
2171def typed_allocated_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2172 allocated: Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>, source: Core.Tensor<input>,
2173 -certificate: AllocationSpec.TensorDone<Layout.output(input, axes, plan), allocated>) ->
2174 Totality.TypedPermutation<input, axes, source, Transforms.copy_allocated(input, axes, plan, source, allocated)>:
2175 match allocated:
2176 case Fail{error}:
2177 typed_permutation_impossible(input, axes, source, Transforms.copy_allocated(input, axes, plan, source, Fail{error}),
2178 {\{AllocationSpec.TensorDone: tensor => same =>
2179 Lifecycle.false_true(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>>, Bool,
2180 Result.is_done(&2, &1, Core.Error, Core.Tensor<Layout.output(input, axes, plan)>), Done{tensor}, Fail{error}, same))} :
2181 AllocationSpec.TensorDone<Layout.output(input, axes, plan), Fail{error}> -> Empty}(certificate))
2182 case Done{target}:
2183 typed_built_result(input, axes, plan, source, target, Transforms.built(input, axes, plan, source, target), {==},
2184 PermuteBuild.built_meaning(input, axes, plan, source, target),
2185 {\{PermuteBuild.Fact: successful => successful} :
2186 PermuteBuild.Fact<{Totality.copy_succeeded(input, axes, plan, Transforms.built(input, axes, plan, source, target)) == True{} : Bool}> ->
2187 {Totality.copy_succeeded(input, axes, plan, Transforms.built(input, axes, plan, source, target)) == True{} : Bool}}(
2188 PermuteBuild.built_success(input, axes, plan, source, target)))
2189
2190def typed_planned_success(+input: Shape.Shape, +axes: List<&2, U32>, planned: Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, source: Core.Tensor<input>,
2191 -successful: {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, planned) == True{} : Bool}) ->
2192 Totality.TypedPermutation<input, axes, source, Transforms.copy_planned(input, axes, source, planned)>:
2193 match planned:
2194 case Fail{error}:
2195 typed_permutation_impossible(input, axes, source, Transforms.copy_planned(input, axes, source, Fail{error}), Arith.clash(successful))
2196 case Done{+plan}:
2197 typed_allocated_success(input, axes, plan, Core.new(Layout.output(input, axes, plan), 0.0), source,
2198 AllocationProof.core_new_done(Layout.output(input, axes, plan), 0.0))
2199
2200def Laws.permute_typed_success(input, source, axes, valid):
2201 typed_planned_success(input, axes, Layout.permutation(input, axes), source,
2202 {\{Totality.PlanSuccess: successful => successful} : Totality.PlanSuccess<input, axes> ->
2203 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.permutation(input, axes)) == True{} : Bool}}(
2204 Laws.permutation_valid_success(input, axes, valid)))
2205
2206def logical_index_bounded(+shape: Shape.Shape, +index: U32,
2207 +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
2208 {True{} == U32.is_lt(index, Shape.count(shape)) : Bool}:
2209 %Arith.u32_lt(index, Shape.count(shape)) : {True{} == _ : Bool}
2210 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
2211 %Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)) : {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
2212 Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))), True{}, inside)
2213
2214def mapping_done_result(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2215 result: Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
2216 -successful: {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, result) == True{} : Bool}) ->
2217 Totality.MappingDone<input, axes, plan, index, result>:
2218 match result:
2219 case Fail{error}:
2220 Totality.MappingDone{Empty.absurd(Layout.Mapping<input, axes, plan, index>, Arith.clash(successful)),
2221 Empty.absurd({Done{Empty.absurd(Layout.Mapping<input, axes, plan, index>, Arith.clash(successful))} == Fail{error} :
2222 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}, Arith.clash(successful))}
2223 case Done{mapping}:
2224 Totality.MappingDone{mapping, {==}}
2225
2226def mapping_done(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
2227 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
2228 Totality.MappingDone<input, axes, plan, index, Layout.map_index(input, axes, plan, index)>:
2229 mapping_done_result(input, axes, plan, index, Layout.map_index(input, axes, plan, index),
2230 {\{Totality.MappingSuccess: successful => successful} : Totality.MappingSuccess<input, axes, plan, index> ->
2231 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, Layout.map_index(input, axes, plan, index)) == True{} : Bool}}(
2232 Laws.mapping_valid_success(input, axes, plan, index, inside)))
2233
2234def prefix_observation(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2235 -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, +index: U32,
2236 -prefix: Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
2237 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) ->
2238 Totality.CopyObservation<input, axes, plan, original, target, index>:
2239 Totality.CopyObservation{
2240 {\{Transforms.Prefix: kept => words => checked => written =>
2241 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, index), Core.checked_observe(Layout.output(input, axes, plan), target, index),
2242 Transforms.expected_output(input, axes, plan, original, index),
2243 {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), target, index), Core.observe(Layout.output(input, axes, plan), target, index), equal)} :
2244 ObserveBridge<Layout.output(input, axes, plan), target, index> ->
2245 {Core.observe(Layout.output(input, axes, plan), target, index) == Core.checked_observe(Layout.output(input, axes, plan), target, index) : Maybe<&2, F32>}}(
2246 observe_bridge(Layout.output(input, axes, plan), target, index,
2247 %WordConversion.word_natural_exact(index) : Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, _)
2248 checked(U32.to_nat(index), inside))),
2249 %WordConversion.word_natural_exact(index) :
2250 {Core.checked_observe(Layout.output(input, axes, plan), target, _) == Transforms.expected_output(input, axes, plan, original, _) : Maybe<&2, F32>}
2251 written(U32.to_nat(index), inside))} :
2252 Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))> ->
2253 {Core.observe(Layout.output(input, axes, plan), target, index) == Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}}(prefix)}
2254
2255def logical_observe_bridge(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +index: U32,
2256 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> ObserveBridge<shape, tensor, index>:
2257 ObserveBridge{
2258 {\{CheckedObservationModel: checked =>
2259 {\{ObserveBridge: equal => equal} : ObserveBridge<shape, tensor, index> ->
2260 {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}}(
2261 observe_bridge(shape, tensor, index, checked))} : CheckedObservationModel<shape, tensor, index> ->
2262 {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}}(
2263 checked_observation_model(shape, tensor, index, inside))}
2264
2265def inverse_observation_mapped(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2266 +inverse: Layout.Plan<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes)>,
2267 -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -middle: Core.Tensor<Layout.output(input, axes, plan)>,
2268 -middle_retained: Core.Tensor<Layout.output(input, axes, plan)>,
2269 -restored: Core.Tensor<Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)>, +index: U32,
2270 +second: Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>,
2271 -second_exact: {Done{second} == Layout.map_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index) :
2272 Result<&2, &2, Layout.Error, Layout.Mapping<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index>>},
2273 +first: Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>,
2274 -first_exact: {Done{first} == Layout.map_index(input, axes, plan,
2275 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) :
2276 Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)>>},
2277 -first_prefix: Transforms.Prefix<input, axes, plan, original, retained, middle, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
2278 -second_prefix: Transforms.Prefix<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored,
2279 Shape.logical_numel(Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)))>,
2280 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}) ->
2281 Totality.RestoreObservation<input, Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), original, restored, index>:
2282 Totality.RestoreObservation{
2283 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index),
2284 Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index), Core.observe(input, original, index),
2285 {\{Totality.CopyObservation: equal => equal} :
2286 Totality.CopyObservation<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, restored, index> ->
2287 {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) ==
2288 Transforms.expected_output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, index) : Maybe<&2, F32>}}(
2289 prefix_observation(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, middle, middle_retained, restored, index, second_prefix,
2290 %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)), Shape.dimensions(input),
2291 Laws.inverse_permutation_dimensions(input, axes, plan, inverse)) : {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
2292 inside)),
2293 %second_exact : {Transforms.expected_mapped(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, middle, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2294 Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), middle,
2295 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)),
2296 Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)), Core.observe(input, original, index),
2297 {\{ObserveBridge: equal => equal} : ObserveBridge<Layout.output(input, axes, plan), middle,
2298 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
2299 {Core.checked_observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) ==
2300 Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) : Maybe<&2, F32>}}(
2301 logical_observe_bridge(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2302 Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
2303 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)),
2304 Transforms.expected_output(input, axes, plan, original, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)), Core.observe(input, original, index),
2305 {\{Totality.CopyObservation: equal => equal} : Totality.CopyObservation<input, axes, plan, original, middle,
2306 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)> ->
2307 {Core.observe(Layout.output(input, axes, plan), middle, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) ==
2308 Transforms.expected_output(input, axes, plan, original, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)) : Maybe<&2, F32>}}(
2309 prefix_observation(input, axes, plan, original, retained, middle,
2310 Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first_prefix,
2311 Laws.mapped_mathematical_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))),
2312 %first_exact : {Transforms.expected_mapped(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), original, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2313 %Equal.sym(U32, Layout.source_index(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second), first), index,
2314 Laws.inverse_mapping_restores_index(input, axes, plan, inverse, index, second, first)) : {Core.checked_observe(input, original, _) == Core.observe(input, original, index) : Maybe<&2, F32>}
2315 {\{ObserveBridge: equal => equal} : ObserveBridge<input, original, index> ->
2316 {Core.checked_observe(input, original, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
2317 logical_observe_bridge(input, original, index, inside)))))}
2318
2319def inverse_restoration_second(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, -original: Core.Tensor<input>, -retained: Core.Tensor<input>,
2320 -middle: Core.Tensor<Layout.output(input, axes, plan)>,
2321 -first_exact: {(retained, Done{Core.Packed{Layout.output(input, axes, plan), middle}}) == Transforms.permute_copy(input, original, axes) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
2322 -first_prefix: Transforms.Prefix<input, axes, plan, original, retained, middle, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
2323 certificate: Totality.TypedPermutation<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), middle,
2324 Transforms.permute_copy(Layout.output(input, axes, plan), middle, Totality.inverse_axes(input, axes))>) -> Totality.PermutationRestoration<input, axes, original>:
2325 Totality.TypedPermutation{+inverse, middle_retained, restored, second_exact, second_prefix} = certificate
2326 Totality.PermutationRestoration{plan, retained, middle, first_exact, inverse, middle_retained, restored,
2327 Equal.cong(Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2328 Transforms.dynamic_result(Layout.output(input, axes, plan)), (middle_retained, Done{Core.Packed{Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored}}),
2329 Transforms.permute_copy(Layout.output(input, axes, plan), middle, Totality.inverse_axes(input, axes)), second_exact),
2330 Laws.inverse_permutation_dimensions(input, axes, plan, inverse),
2331 index => inside =>
2332 {\{Totality.MappingDone: second => second_exact =>
2333 {\{Totality.MappingDone: first => first_mapping_exact =>
2334 {\{Totality.RestoreObservation: equal => equal} :
2335 Totality.RestoreObservation<input, Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), original, restored, index> ->
2336 {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
2337 inverse_observation_mapped(input, axes, plan, inverse, original, retained, middle, middle_retained, restored, index,
2338 second, second_exact, first, first_mapping_exact, first_prefix, second_prefix, inside))} :
2339 Totality.MappingDone<input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2340 Layout.map_index(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second))> ->
2341 {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
2342 mapping_done(input, axes, plan, Layout.source_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second),
2343 Laws.mapped_bounded(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index, second)))} :
2344 Totality.MappingDone<Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index,
2345 Layout.map_index(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index)> ->
2346 {Core.observe(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), restored, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}(
2347 mapping_done(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse, index,
2348 logical_index_bounded(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse), index,
2349 %Equal.sym(List<&2, U32>, Shape.dimensions(Layout.output(Layout.output(input, axes, plan), Totality.inverse_axes(input, axes), inverse)), Shape.dimensions(input),
2350 Laws.inverse_permutation_dimensions(input, axes, plan, inverse)) : {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
2351 inside)))}
2352
2353def Laws.permute_inverse_restoration(input, source, axes, valid):
2354 Totality.PermutationInverse{
2355 {\{Totality.TypedPermutation: plan => retained => middle => first_exact => first_prefix =>
2356 inverse_restoration_second(input, axes, plan, source, retained, middle, first_exact, first_prefix,
2357 Laws.permute_typed_success(Layout.output(input, axes, plan), middle, Totality.inverse_axes(input, axes), Laws.inverse_axes_valid(input, axes, plan)))} :
2358 Totality.TypedPermutation<input, axes, source, Transforms.permute_copy(input, source, axes)> -> Totality.PermutationRestoration<input, axes, source>}(
2359 Laws.permute_typed_success(input, source, axes, valid))}
2360
2361def transpose_decided_permutation(+input: Shape.Shape, +a: U32, +b: U32,
2362 decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>, source: Core.Tensor<input>,
2363 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2364 {Transforms.transpose_decided(input, source, a, b, decision) == Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) :
2365 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
2366 match decision:
2367 case Shape.BFalse{equal}:
2368 Empty.absurd({(source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) ==
2369 Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
2370 Arith.clash(Equal.trans(Bool, False{}, TransposeSpec.valid(input, a, b), True{}, equal,
2371 Equal.sym(Bool, True{}, TransposeSpec.valid(input, a, b), inside))))
2372 case Shape.BTrue{equal}:
2373 {==}
2374
2375def transpose_permutation(+input: Shape.Shape, source: Core.Tensor<input>, +a: U32, +b: U32,
2376 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2377 {Transforms.transpose_copy(input, source, a, b) == Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) :
2378 Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
2379 transpose_decided_permutation(input, a, b, Shape.bool_case(TransposeSpec.valid(input, a, b)), source, inside)
2380
2381def Laws.transpose_valid_success(input, source, a, b, inside):
2382 Totality.PublicSuccess{
2383 %Equal.sym(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.transpose_copy(input, source, a, b),
2384 Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), transpose_permutation(input, source, a, b, inside)) :
2385 {Totality.public_succeeded(input, _) == True{} : Bool}
2386 {\{Totality.PublicSuccess: successful => successful} :
2387 Totality.PublicSuccess<input, Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))> ->
2388 {Totality.public_succeeded(input, Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))) == True{} : Bool}}(
2389 Laws.permute_valid_success(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeProof.valid_axes(input, a, b, inside)))}
2390
2391def transpose_observation_mapped(+input: Shape.Shape, +a: U32, +b: U32, +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2392 -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)>, +index: U32,
2393 +mapping: Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>,
2394 -map_exact: {Done{mapping} == Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index) :
2395 Result<&2, &2, Layout.Error, Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>>},
2396 -prefix: Transforms.Prefix<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target,
2397 Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))>,
2398 +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)))) == True{} : Bool},
2399 +axes_inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2400 Totality.TransposeObservation<input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), original, target, a, b, index>:
2401 Totality.TransposeObservation{
2402 Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index),
2403 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2404 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2405 {\{Totality.CopyObservation: equal => equal} :
2406 Totality.CopyObservation<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, target, index> ->
2407 {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2408 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index) : Maybe<&2, F32>}}(
2409 prefix_observation(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, retained, target, index, prefix, inside)),
2410 Equal.trans(Maybe<&2, F32>, Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2411 Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2412 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2413 Equal.sym(Maybe<&2, F32>, Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2414 Transforms.expected_output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, original, index),
2415 Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index>>, Maybe<&2, F32>,
2416 Transforms.expected_mapped(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, original),
2417 Done{mapping}, Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index), map_exact)),
2418 Equal.trans(Maybe<&2, F32>, Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2419 Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)),
2420 Totality.reference_observe(input, original, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)),
2421 {\{ObserveBridge: equal => equal} :
2422 ObserveBridge<input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)> ->
2423 {Core.checked_observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) ==
2424 Core.observe(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)) : Maybe<&2, F32>}}(
2425 logical_observe_bridge(input, original, Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping),
2426 Laws.mapped_mathematical_bounded(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping))),
2427 Equal.cong(Maybe<&2, U32>, Maybe<&2, F32>, Totality.reference_observe(input, original),
2428 Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)},
2429 Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index),
2430 %TransposeProof.transpose_axes_requested(input, a, b, axes_inside) :
2431 {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} ==
2432 Layout.reference_source_coordinates(Shape.dimensions(input), Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(_),
2433 Shape.words(Shape.digits(Shape.extents(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), U32.to_nat(index))), 0n)) : Maybe<&2, U32>}
2434 Laws.mapping_reference(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)))))}
2435
2436def transpose_requested_certificate(+input: Shape.Shape, -source: Core.Tensor<input>, +a: U32, +b: U32,
2437 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool},
2438 certificate: Totality.TypedPermutation<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source,
2439 Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))>) -> Totality.RequestedTranspose<input, source, a, b>:
2440 Totality.TypedPermutation{+plan, retained, target, exact, prefix} = certificate
2441 Totality.RequestedTranspose{plan, retained, target,
2442 Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2443 (retained, Done{Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target}}),
2444 Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Transforms.transpose_copy(input, source, a, b), exact,
2445 Equal.sym(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.transpose_copy(input, source, a, b),
2446 Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), transpose_permutation(input, source, a, b, inside))),
2447 Equal.trans(List<&2, U32>, Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)),
2448 Axis.order(U32, Shape.dimensions(input), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2449 Axis.order(U32, Shape.dimensions(input), Shape.naturals(TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)))),
2450 Mapping.permutation_dimensions_order(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan),
2451 Equal.cong(List<&2, U32>, List<&2, U32>, axes => Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
2452 Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2453 TransposeProof.transpose_axes_requested(input, a, b, inside))),
2454 prefix, index => mapping =>
2455 %TransposeProof.transpose_axes_requested(input, a, b, inside) :
2456 {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} ==
2457 Layout.reference_source_coordinates(Shape.dimensions(input), Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(_),
2458 Shape.words(Shape.digits(Shape.extents(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), U32.to_nat(index))), 0n)) : Maybe<&2, U32>}
2459 Laws.mapping_reference(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping),
2460 index => logical =>
2461 {\{Totality.MappingDone: mapping => map_exact =>
2462 {\{Totality.TransposeObservation: equal => equal} :
2463 Totality.TransposeObservation<input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), source, target, a, b, index> ->
2464 {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2465 Totality.reference_observe(input, source, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)) : Maybe<&2, F32>}}(
2466 transpose_observation_mapped(input, a, b, plan, source, retained, target, index, mapping, map_exact, prefix, logical, inside))} :
2467 Totality.MappingDone<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index,
2468 Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index)> ->
2469 {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2470 Totality.reference_observe(input, source, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)) : Maybe<&2, F32>}}(
2471 mapping_done(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index,
2472 logical_index_bounded(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), index, logical)))}
2473
2474def Laws.transpose_requested_result(input, source, a, b, inside):
2475 transpose_requested_certificate(input, source, a, b, inside,
2476 Laws.permute_typed_success(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeProof.valid_axes(input, a, b, inside)))
2477
2478def transpose_output_inside(+input: Shape.Shape, +a: U32, +b: U32,
2479 +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2480 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2481 {True{} == TransposeSpec.valid(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b) : Bool}:
2482 %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2483 Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)) :
2484 {True{} == TransposeSpec.axes_valid(_, U32.to_nat(a), U32.to_nat(b)) : Bool}
2485 inside
2486
2487def transpose_output_axes(+input: Shape.Shape, +a: U32, +b: U32,
2488 +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2489 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2490 {Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0) ==
2491 Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) : List<&2, U32>}:
2492 Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0),
2493 TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2494 Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2495 Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0),
2496 TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))), U32.to_nat(a), U32.to_nat(b)),
2497 TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2498 TransposeProof.transpose_axes_requested(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, transpose_output_inside(input, a, b, plan, inside)),
2499 Equal.cong(Nat, List<&2, U32>, rank => TransposeSpec.requested_axes(rank, U32.to_nat(a), U32.to_nat(b)),
2500 Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2501 Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2502 Equal.trans(List<&2, U32>, TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2503 Layout.transpose_axes(Shape.dimensions(input), a, b, 0), Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2504 Equal.sym(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2505 TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), TransposeProof.transpose_axes_requested(input, a, b, inside)),
2506 Equal.sym(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2507 Equal.trans(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2508 Shape.words(Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))), Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2509 Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words,
2510 Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2511 Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), TransposeProof.inverse_axes(input, a, b, inside)),
2512 words_naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))))))
2513
2514def transpose_restoration_certificate(+input: Shape.Shape, -original: Core.Tensor<input>, +a: U32, +b: U32,
2515 +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool},
2516 certificate: Totality.PermutationRestoration<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), original>) -> Totality.TransposeRestoration<input, original, a, b>:
2517 Totality.PermutationRestoration{+first, retained, middle, first_exact, second, middle_retained, restored, second_exact, dimensions, linear} = certificate
2518 Totality.TransposeRestoration{first, retained, middle,
2519 Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2520 (retained, Done{Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}}),
2521 Transforms.permute_copy(input, original, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Transforms.transpose_copy(input, original, a, b), first_exact,
2522 Equal.sym(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.transpose_copy(input, original, a, b),
2523 Transforms.permute_copy(input, original, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), transpose_permutation(input, original, a, b, inside))),
2524 second, middle_retained, restored,
2525 Equal.trans(Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2526 (Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle_retained},
2527 Done{Core.Packed{Layout.output(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), second), restored}}),
2528 Transforms.permute_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2529 Transforms.transpose_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, a, b), second_exact,
2530 Equal.sym(Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2531 Transforms.transpose_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, a, b),
2532 Transforms.permute_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2533 Equal.trans(Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2534 Transforms.transpose_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, a, b),
2535 Transforms.permute_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle},
2536 Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first)), a, b, 0)),
2537 Transforms.permute_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2538 Equal.cong(Core.Tensor<Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first)> & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2539 Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.dynamic_result(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first)),
2540 Transforms.transpose_copy(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle, a, b),
2541 Transforms.permute_copy(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle,
2542 Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first)), a, b, 0)),
2543 transpose_permutation(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle, a, b, transpose_output_inside(input, a, b, first, inside))),
2544 Equal.cong(List<&2, U32>, Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2545 axes => Transforms.permute_dynamic(Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first), middle}, axes),
2546 Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), first)), a, b, 0),
2547 Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), transpose_output_axes(input, a, b, first, inside))))), dimensions, linear}
2548
2549def Laws.transpose_inverse_restoration(input, source, a, b, inside):
2550 Totality.TransposeInverse{
2551 {\{Totality.PermutationInverse: restoration => transpose_restoration_certificate(input, source, a, b, inside, restoration)} :
2552 Totality.PermutationInverse<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source> -> Totality.TransposeRestoration<input, source, a, b>}(
2553 Laws.permute_inverse_restoration(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeProof.valid_axes(input, a, b, inside)))}