1 import Base 2 import ../shape/core.bend as Shape 3 import ./layout.bend as Layout 4 import ./transform_LAWS.bend as Laws 5 import ./core.bend as Core 6 import ./transforms.bend as Transforms 7 import ./lifecycle.bend as Lifecycle 8 import ../storage/main.bend as Storage 9 import ../storage/model.bend as Model 10 import ../storage/refinement.bend as Refinement 11 import ../storage/PROOF.bend as StorageProof 12 import ../storage/LAWS.bend as StorageLaws 13 import ./core_PROOF.bend as CoreProof 14 import ../storage/arith.bend as Arith 15 import ../shape/coordinate_proofs.bend as Coordinates 16 import ../shape/nat_proofs.bend as Nats 17 import ../storage/route.bend as Route 18 import ./word_conversion.bend as WordConversion 19 import ../shape/index_proofs.bend as ShapeIndex 20 import ../shape/LAWS.bend as ShapeLaws 21 import ../shape/PROOF.bend as ShapeProof 22 import ./axis_spec.bend as Axis 23 import ./axis_algebra.bend as AxisAlgebra 24 import ./transform_totality.bend as Totality 25 import ./permutation_mapping.bend as Mapping 26 import ./allocation_PROOF.bend as AllocationProof 27 import ./allocation_spec.bend as AllocationSpec 28 import ./transpose_PROOF.bend as TransposeProof 29 import ./transpose_spec.bend as TransposeSpec 30 import ./permute_build_proof.bend as PermuteBuild 31 32 def Laws.permutation_checked(input, axes, plan): 33 Mapping.permutation_checked(input, axes, plan) 34 35 def Laws.permutation_dimensions(input, axes, plan): 36 Layout.Permutation{out, valid, ordered, count} = plan 37 ordered 38 39 def Laws.permutation_count(input, axes, plan): 40 Layout.Permutation{out, valid, ordered, count} = plan 41 Transforms.elements_equal(input, out, count) 42 43 def Laws.mapped_inverse(input, axes, plan, i, mapping): 44 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping 45 inverse 46 47 def Laws.mapped_flat(input, axes, plan, i, mapping): 48 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping 49 flattened 50 51 def Laws.mapped_output(input, axes, plan, i, mapping): 52 Layout.Mapped{oi, oc, ic, index, requested, decoded, inverse, flattened, roundtrip} = mapping 53 decoded 54 55 def 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 60 def 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 71 def 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 87 def 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 92 def 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 108 def 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 120 def 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 125 def Laws.reshape_linear_order(input, target, tensor, index, same): 126 Core.TTensor{storage, valid} = tensor 127 {==} 128 129 def Laws.reshape_target_dimensions(input, target, tensor, same): 130 Core.TTensor{storage, valid} = tensor 131 {==} 132 133 def Laws.copy_input_preservation(depth, array, index, other, balanced): 134 Equal.cong(Array, 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 138 def 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 141 def 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 & Result<&2, &1, Transforms.Error, Core.Tensor>} 145 {==} 146 147 def 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 154 def 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 159 def 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 162 def copy_checked_mapping(-input: Shape.Shape, -axes: List<&2, U32>, +plan: Layout.Plan, 163 +depth: Nat, +length: Nat, array: Array, +index: U32, source: Core.Tensor, +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 184 def 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 188 def copy_result_mapping(-input: Shape.Shape, -axes: List<&2, U32>, +plan: Layout.Plan, 189 +depth: Nat, +length: Nat, array: Array, +index: U32, source: Core.Tensor, 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 205 def 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 220 def copy_meaning_from_read(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 221 -mapping: Layout.Mapping, -source: Core.Tensor, 222 -target: Core.Tensor, 223 -read: Core.Read, 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) -> 229 Transforms.CopyMeaning: 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 243 def 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 253 def 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 260 def 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 264 def 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 272 def 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 281 def 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 294 def 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 306 def prefix_written_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, 307 -original: Core.Tensor, -before: Core.Tensor, -after: Core.Tensor, 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 330 def prefix_checked_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, 331 -target: Core.Tensor, -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 344 def 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 356 def 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 368 def observe_index_equal(+depth: Nat, -length: Nat, -array: Array, +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 379 def observe_allowed_equal(+depth: Nat, +length: Nat, -array: Array, +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 390 type ObserveBridge<-shape: Shape.Shape, -tensor: Core.Tensor, -index: U32> is Data: 391 ObserveBridge{-equal: {Core.checked_observe(shape, tensor, index) == Core.observe(shape, tensor, index) : Maybe<&2, F32>}} 392 393 def observe_bridge(-shape: Shape.Shape, tensor: Core.Tensor, +index: U32, 394 checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index)) -> ObserveBridge: 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 403 type ReadInfo<-shape: Shape.Shape, -original: Core.Tensor, -index: U32> is Type: 404 ReadInfo{owner: Core.Tensor, same: {owner == original : Core.Tensor}, 405 -source: Core.SourceRead, -kept: Core.SourceReadKeeps} 406 407 def read_info(-shape: Shape.Shape, original: Core.Tensor, +index: U32) -> ReadInfo: 408 ReadInfo{original, {==}, Core.source_read_model(shape, original, index), Core.source_read_keeps(shape, original, index)} 409 410 type TargetInfo<-shape: Shape.Shape, -original: Core.Tensor, -index: U32, -value: F32> is Type: 411 TargetInfo{owner: Core.Tensor, same: {owner == original : Core.Tensor}, 412 -model: Core.CheckedUpdateModel} 413 414 def target_info(-shape: Shape.Shape, original: Core.Tensor, +index: U32, +value: F32) -> TargetInfo: 415 TargetInfo{original, {==}, CoreProof.checked_update_model(shape, original, index, value)} 416 417 def read_rebased(-shape: Shape.Shape, -original: Core.Tensor, -owner: Core.Tensor, +index: U32, 418 same: {owner == original : Core.Tensor}, certificate: Core.Read) -> Core.Read: 419 Core.Read{tensor, result, exact} = certificate 420 Core.Read{tensor, result, Equal.trans(Core.Tensor & 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, Core.Tensor & Result<&2, &2, Core.Error, F32>, t => Core.read_flat(shape, t, index), owner, original, same))} 423 424 type SourceValue<-shape: Shape.Shape, -original: Core.Tensor, -index: U32, -value: F32> is Data: 425 SourceValue{-equal: {Core.checked_observe(shape, original, index) == Some{value} : Maybe<&2, F32>}} 426 427 def source_value(-shape: Shape.Shape, -original: Core.Tensor, -retained: Core.Tensor, +index: U32, +value: F32, 428 -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor & Result<&2, &2, Core.Error, F32>}, 429 certificate: Core.SourceRead) -> SourceValue: 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 & 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 & Result<&2, &2, Core.Error, F32>, (retained, Done{value}), Core.read_flat(shape, original, index), exact)))} 437 438 type SourceKept<-shape: Shape.Shape, -original: Core.Tensor, -retained: Core.Tensor> is Data: 439 SourceKept{-kept: Transforms.SameSource(shape, original, retained)} 440 441 def source_kept(-shape: Shape.Shape, -original: Core.Tensor, -retained: Core.Tensor, +index: U32, -value: F32, 442 -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor & Result<&2, &2, Core.Error, F32>}, 443 certificate: Core.SourceReadKeeps) -> SourceKept: 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 & 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 450 type MappedValue<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 451 -original: Core.Tensor, -value: F32> is Data: 452 MappedValue{-equal: {Some{value} == Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}} 453 454 def mapped_value(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 455 -original: Core.Tensor, +mapping: Layout.Mapping, +value: F32, 456 -exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, 457 certificate: SourceValue) -> 458 MappedValue: 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 464 type KnownCheckedUpdate<-shape: Shape.Shape, -original: Core.Tensor, -output: Core.Tensor, -index: U32, 465 -value: F32, -unit: Unit> is Data: 466 KnownCheckedUpdate{-meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))} 467 468 def known_checked_update(-shape: Shape.Shape, -original: Core.Tensor, -output: Core.Tensor, +index: U32, 469 +value: F32, -unit: Unit, 470 -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor & Result<&2, &2, Core.Error, Unit>}, 471 certificate: Core.CheckedUpdateModel) -> KnownCheckedUpdate: 472 Core.CheckedUpdateModel{meaning} = certificate 473 KnownCheckedUpdate{ 474 %Equal.sym(Core.Tensor & 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 478 def checked_update_route(-shape: Shape.Shape, -original: Core.Tensor, -output: Core.Tensor, -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 484 def checked_update_value(-shape: Shape.Shape, -original: Core.Tensor, -output: Core.Tensor, -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 491 def checked_update_frame(-shape: Shape.Shape, -original: Core.Tensor, -output: Core.Tensor, -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 501 type SuccessfulStep<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 502 -original_source: Core.Tensor, -original_target: Core.Tensor, 503 -source: Core.Tensor, -target: Core.Tensor> is Data: 504 SuccessfulStep{-meaning: Transforms.StepMeaning(input, axes, plan, index, original_source, original_target, (source, Done{target}))} 505 506 def successful_step(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 507 -original_source: Core.Tensor, -original_target: Core.Tensor, 508 -source: Core.Tensor, -target: Core.Tensor, +mapping: Layout.Mapping, 509 +value: F32, -unit: Unit, 510 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, 511 read_value: SourceValue, 512 read_kept: SourceKept, 513 update: KnownCheckedUpdate) -> 514 SuccessfulStep: 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 -> 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 528 def step_write_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 529 -original_source: Core.Tensor, -original_target: Core.Tensor, 530 +mapping: Layout.Mapping, +value: F32, 531 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, 532 certificate: Core.Write, 533 retained: Core.Tensor, 534 lift: @-pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor> -> 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 & Result<&2, &1, Transforms.Error, Core.Tensor>} -> 538 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) : 539 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>}, 540 -read_exact: {(retained, Done{value}) == Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)) : 541 Core.Tensor & Result<&2, &2, Core.Error, F32>}, 542 -read_model: Core.SourceRead, 543 -keep_model: Core.SourceReadKeeps, 544 -write_model: Core.CheckedUpdateModel) -> 545 Transforms.StepCertificate: 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 & Result<&2, &2, Core.Error, Unit>, 552 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 & Result<&2, &2, Core.Error, Unit>, 559 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 -> 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 569 def step_target_info(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 570 -original_source: Core.Tensor, -original_target: Core.Tensor, 571 +mapping: Layout.Mapping, +value: F32, 572 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, 573 target_info: TargetInfo, retained: Core.Tensor, 574 lift: @-pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor> -> 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 & Result<&2, &1, Transforms.Error, Core.Tensor>} -> 578 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) : 579 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>}, 580 -read_exact: {(retained, Done{value}) == Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)) : 581 Core.Tensor & Result<&2, &2, Core.Error, F32>}) -> Transforms.StepCertificate: 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 589 def step_read_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 590 -original_source: Core.Tensor, original_target: Core.Tensor, 591 +mapping: Layout.Mapping, 592 -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}, 593 lift: @-pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor> -> 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 & Result<&2, &1, Transforms.Error, Core.Tensor>} -> 597 {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) : 598 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>}, 599 certificate: Core.Read) -> 600 Transforms.StepCertificate: 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 & Result<&2, &2, Core.Error, F32>, 607 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 & Result<&2, &2, Core.Error, F32>, 619 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 623 def step_mapped_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 624 source: Core.Tensor, target: Core.Tensor, 625 result: Result<&2, &2, Layout.Error, Layout.Mapping>, 626 exact: {result == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping>}) -> 627 Transforms.StepCertificate: 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>, 632 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 & Result<&2, &1, Transforms.Error, Core.Tensor>, 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>, 641 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 646 def step_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 647 source: Core.Tensor, target: Core.Tensor) -> 648 Transforms.StepCertificate: 649 step_mapped_certificate(input, axes, plan, index, source, target, Layout.map_index(input, axes, plan, index), {==}) 650 651 def natural_step_lift(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, +index: U32, 652 -source: Core.Tensor, -target: Core.Tensor, 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}, 657 certificate: Transforms.StepCertificate) -> 658 Transforms.NaturalCertificate: 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, 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 & Result<&2, &1, Transforms.Error, Core.Tensor>, 666 Transforms.NaturalCopy, 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 670 def natural_decided_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, +index: U32, 671 source: Core.Tensor, target: Core.Tensor, 672 -candidate: {index == U32.from_nat(cursor) : U32}, 673 decision: Shape.BoolCase, 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}) -> 676 Transforms.NaturalCertificate: 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 683 def natural_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 684 source: Core.Tensor, target: Core.Tensor) -> 685 Transforms.NaturalCertificate: 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 689 def words_same_refl(+values: List<&2, U32>) -> {Layout.words_same(values, values) == True{} : Bool}: 690 Mapping.words_same_refl(values) 691 692 def 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 696 def 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 700 def 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 712 def 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 721 type ExpectedSame<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -original: Core.Tensor, 722 -source: Core.Tensor, -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 726 def expected_same_mapped(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 727 -original: Core.Tensor, -source: Core.Tensor, 728 kept: Transforms.SameSource(input, original, source), 729 result: Result<&2, &2, Layout.Error, Layout.Mapping>) -> 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 738 def expected_same(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 739 -original: Core.Tensor, -source: Core.Tensor, +index: U32, 740 -kept: Transforms.SameSource(input, original, source)) -> ExpectedSame: 741 ExpectedSame{expected_same_mapped(input, axes, plan, index, original, source, kept, Layout.map_index(input, axes, plan, index))} 742 743 type PrefixSource<-input: Shape.Shape, -original: Core.Tensor, -source: Core.Tensor> is Data: 744 PrefixSource{-kept: Transforms.SameSource(input, original, source)} 745 746 def prefix_source(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -original: Core.Tensor, 747 -source: Core.Tensor, -target: Core.Tensor, -cursor: Nat, 748 prefix: Transforms.Prefix) -> PrefixSource: 749 Transforms.Prefix{kept, words, checked, written} = prefix 750 PrefixSource{kept} 751 752 type 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 755 def prefix_word(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -original: Core.Tensor, 756 -source: Core.Tensor, -target: Core.Tensor, -cursor: Nat, 757 prefix: Transforms.Prefix) -> PrefixWords: 758 Transforms.Prefix{kept, words, checked, written} = prefix 759 PrefixWords{words} 760 761 type PrefixRoutes<-shape: Shape.Shape, -target: Core.Tensor, -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 765 def prefix_route(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -original: Core.Tensor, 766 -source: Core.Tensor, -target: Core.Tensor, -cursor: Nat, 767 prefix: Transforms.Prefix) -> PrefixRoutes: 768 Transforms.Prefix{kept, words, checked, written} = prefix 769 PrefixRoutes{checked} 770 771 def step_source(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 772 -before_source: Core.Tensor, -before_target: Core.Tensor, 773 -after_source: Core.Tensor, -after_target: Core.Tensor, 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 779 def step_route(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 780 -before_source: Core.Tensor, -before_target: Core.Tensor, 781 -after_source: Core.Tensor, -after_target: Core.Tensor, 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 788 def step_value(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 789 -before_source: Core.Tensor, -before_target: Core.Tensor, 790 -after_source: Core.Tensor, -after_target: Core.Tensor, 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 799 def step_frame(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -index: U32, 800 -before_source: Core.Tensor, -before_target: Core.Tensor, 801 -after_source: Core.Tensor, -after_target: Core.Tensor, 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 813 type CanonicalStep<-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, -cursor: Nat, 814 -before_source: Core.Tensor, -before_target: Core.Tensor, 815 -after_source: Core.Tensor, -after_target: Core.Tensor> 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 819 def canonical_step(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan, +cursor: Nat, -index: U32, 820 -before_source: Core.Tensor, -before_target: Core.Tensor, 821 -after_source: Core.Tensor, -after_target: Core.Tensor, 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: 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 830 type PastFrame<-shape: Shape.Shape, -before: Core.Tensor, -after: Core.Tensor, -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 834 def past_frame(-shape: Shape.Shape, -before: Core.Tensor, -after: Core.Tensor, +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: 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 851 def actual_advanced(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 852 -original: Core.Tensor, -before_source: Core.Tensor, -after_source: Core.Tensor, 853 -before_target: Core.Tensor, -after_target: Core.Tensor, 854 prefix: Transforms.Prefix, 855 canonical: CanonicalStep) -> 856 Transforms.Advanced: 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 -> 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 -> 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 -> 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 884 def 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 891 def loop_continue(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 892 -original: Core.Tensor, -before_source: Core.Tensor, -before_target: Core.Tensor, 893 -after_source: Core.Tensor, -after_target: Core.Tensor, -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}, 897 certificate: Transforms.LoopCertificate) -> 898 Transforms.LoopCertificate: 899 Transforms.LoopCertificate{pair, exact, meaning} = certificate 900 Transforms.LoopCertificate{pair, 901 Equal.trans(Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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, 905 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 913 def loop_after_pair(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 914 -original: Core.Tensor, -before_source: Core.Tensor, -before_target: Core.Tensor, 915 -index: U32, -converted: {U32.to_nat(index) == cursor : Nat}, -candidate: {index == U32.from_nat(cursor) : U32}, 916 -prefix: Transforms.Prefix, 917 pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 918 natural_exact: {Transforms.NaturalCopied{pair, index, converted, candidate} == 919 Transforms.natural_step(input, axes, plan, cursor, before_source, before_target) : Transforms.NaturalCopy}, 920 -meaning: Transforms.StepMeaning(input, axes, plan, index, before_source, before_target, pair), 921 rec: @source: Core.Tensor -> @target: Core.Tensor -> 922 @-prefix: Transforms.Prefix -> 923 Transforms.LoopCertificate) -> 924 Transforms.LoopCertificate: 925 (source, result) = pair 926 match result: 927 case Fail{error}: 928 Transforms.LoopCertificate{(source, Fail{error}), 929 Equal.cong(Transforms.NaturalCopy, 930 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 942 def loop_after_natural(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 943 -original: Core.Tensor, -before_source: Core.Tensor, -before_target: Core.Tensor, 944 -prefix: Transforms.Prefix, 945 certificate: Transforms.NaturalCertificate, 946 rec: @source: Core.Tensor -> @target: Core.Tensor -> 947 @-prefix: Transforms.Prefix -> 948 Transforms.LoopCertificate) -> 949 Transforms.LoopCertificate: 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, 955 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 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 963 def loop_certificate(fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 964 -original: Core.Tensor, source: Core.Tensor, target: Core.Tensor, 965 -prefix: Transforms.Prefix) -> 966 Transforms.LoopCertificate: 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 975 def 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 982 def whole_copy_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 983 source: Core.Tensor, target: Core.Tensor) -> 984 Transforms.LoopCertificate: 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 988 def whole_copy_meaning(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 989 -source: Core.Tensor, -target: Core.Tensor, 990 certificate: Transforms.LoopCertificate) -> 991 Transforms.WholeCopyModel: 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 1000 def 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 1003 def permuted_output(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 1004 -original: Core.Tensor, -source: Core.Tensor, -target: Core.Tensor, 1005 prefix: Transforms.Prefix) -> 1007 Transforms.PermuteOutput: 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 -> 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 1022 def copy_pack_model(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, -original: Core.Tensor, 1023 pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 1024 -meaning: Transforms.LoopMeaning(input, axes, plan, original, 1025 Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), pair)) -> 1026 Transforms.PublicModel: 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 1035 def allocated_model(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, source: Core.Tensor, 1036 allocated: Result<&2, &1, Core.Error, Core.Tensor>) -> 1037 Transforms.PublicModel: 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 1045 def planned_model(+input: Shape.Shape, +axes: List<&2, U32>, source: Core.Tensor, 1046 planned: Result<&2, &2, Layout.Error, Layout.Plan>) -> 1047 Transforms.PublicModel: 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 1054 def Laws.permute_result_interpretation(input, source, axes): 1055 planned_model(input, axes, source, Layout.permutation(input, axes)) 1056 1057 def transpose_decided_model(+input: Shape.Shape, source: Core.Tensor, +a: U32, +b: U32, 1058 decision: Shape.BoolCase) -> 1059 Transforms.PublicModel: 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 1067 def 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 1071 type ReshapeDecidedModel<-input: Shape.Shape, -target: Shape.Shape, -original: Core.Tensor, -dimensions: List<&2, U32>, 1072 -decision: Shape.BoolCase> is Data: 1073 ReshapeDecidedModel{-meaning: Transforms.ReshapeMeaning(input, original, dimensions, 1074 Transforms.reshape_decided(input, target, original, decision))} 1075 1076 def reshape_decided_model(+input: Shape.Shape, +target: Shape.Shape, source: Core.Tensor, -dimensions: List<&2, U32>, 1077 -preserved: {Shape.dimensions(target) == dimensions : List<&2, U32>}, 1078 decision: Shape.BoolCase) -> 1079 ReshapeDecidedModel: 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 1094 type ReshapeBuiltModel<-input: Shape.Shape, -original: Core.Tensor, -dimensions: List<&2, U32>, 1095 -built: Shape.ConstructResult> is Data: 1096 ReshapeBuiltModel{-meaning: Transforms.ReshapeMeaning(input, original, dimensions, 1097 Transforms.reshape_built(input, original, dimensions, built))} 1098 1099 def reshape_built_model(+input: Shape.Shape, source: Core.Tensor, -dimensions: List<&2, U32>, 1100 built: Shape.ConstructResult) -> ReshapeBuiltModel: 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 -> 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 1113 def Laws.reshape_result_interpretation(input, source, dimensions): 1114 Transforms.ReshapeModel{ 1115 {\{ReshapeBuiltModel: meaning => meaning} : ReshapeBuiltModel -> 1116 Transforms.ReshapeMeaning(input, source, dimensions, Transforms.reshape(input, source, dimensions))}( 1117 reshape_built_model(input, source, dimensions, Shape.construct(dimensions)))} 1118 1119 type RestoreModel<-input: Shape.Shape, -original: Core.Tensor, -result: Result<&2, &1, Transforms.Error, Core.Dynamic>> is Data: 1120 RestoreModel{-meaning: Transforms.RestoreMeaning(input, original, result)} 1121 1122 def restore_result_model(-input: Shape.Shape, -original: Core.Tensor, -middle_shape: Shape.Shape, 1123 -middle: Core.Tensor, 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: 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 -> 1137 Transforms.RestoredOutput}(meaning)} 1138 1139 def restore_dynamic_model(+input: Shape.Shape, -original: Core.Tensor, middle: Core.Dynamic, 1140 -prior: @+index: U32 -> {Transforms.dynamic_observe(middle, index) == Core.observe(input, original, index) : Maybe<&2, F32>}) -> 1141 RestoreModel: 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 -> 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 1148 type ReshapeInverseResultModel<-input: Shape.Shape, -original: Core.Tensor, -result: Result<&2, &1, Transforms.Error, Core.Dynamic>> is Data: 1149 ReshapeInverseResultModel{-meaning: Transforms.ReshapeInverseMeaning(input, original, result)} 1150 1151 def reshape_inverse_result_model(-input: Shape.Shape, -original: Core.Tensor, -dimensions: List<&2, U32>, 1152 result: Result<&2, &1, Transforms.Error, Core.Dynamic>, 1153 -meaning: Transforms.ReshapeMeaning(input, original, dimensions, result)) -> ReshapeInverseResultModel: 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 -> 1161 Transforms.RestoreMeaning(input, original, Transforms.reshape_dynamic(output, Shape.dimensions(input)))}( 1162 restore_dynamic_model(input, original, output, linear))} : 1163 Transforms.ReshapeOutput -> 1164 Transforms.RestoreMeaning(input, original, Transforms.reshape_dynamic(output, Shape.dimensions(input)))}(meaning)} 1165 1166 def Laws.reshape_inverse_observations(input, source, dimensions): 1167 Transforms.ReshapeInverseModel{ 1168 {\{ReshapeInverseResultModel: meaning => meaning} : 1169 ReshapeInverseResultModel -> 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 -> 1173 Transforms.ReshapeMeaning(input, source, dimensions, Transforms.reshape(input, source, dimensions))}( 1174 Laws.reshape_result_interpretation(input, source, dimensions))))} 1175 1176 def Laws.mapping_reference(input, axes, plan, index, mapping): 1177 Mapping.mapping_reference(input, axes, plan, index, mapping) 1178 1179 def 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 1183 def 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 1187 def Laws.natural_word_exact(number, limit, within): 1188 natural_word_exact(number, limit, within) 1189 1190 def 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 1197 type CheckedObservationModel<-shape: Shape.Shape, -tensor: Core.Tensor, -index: U32> is Data: 1198 CheckedObservationModel{-checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index)} 1199 1200 def checked_observation_model(+shape: Shape.Shape, tensor: Core.Tensor, +index: U32, 1201 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 1202 CheckedObservationModel: 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 1215 type PresentObservation<-shape: Shape.Shape, -tensor: Core.Tensor, -index: U32> is Data: 1216 PresentObservation{-value: F32, -equal: {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>}} 1217 1218 def present_impossible(-shape: Shape.Shape, -tensor: Core.Tensor, -index: U32, -empty: Empty) -> PresentObservation: 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 1222 def present_observation(+shape: Shape.Shape, tensor: Core.Tensor, +index: U32, 1223 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 1224 PresentObservation: 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 1246 def maybe_present(value: Maybe<&2, F32>) -> Bool: 1247 match value: 1248 case None{}: 1249 False{} 1250 case Some{value}: 1251 True{} 1252 1253 type ReadSuccess<-shape: Shape.Shape, -original: Core.Tensor, -index: U32> is Type: 1254 ReadSuccess{retained: Core.Tensor, value: F32, 1255 exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor & Result<&2, &2, Core.Error, F32>}} 1256 1257 type ReadSuccessModel<-shape: Shape.Shape, -original: Core.Tensor, -index: U32> is Data: 1258 ReadSuccessModel{-success: ReadSuccess} 1259 1260 def read_success_model(-shape: Shape.Shape, -original: Core.Tensor, +index: U32, 1261 certificate: Core.Read, 1262 -model: Core.SourceRead, -present: PresentObservation) -> ReadSuccessModel: 1263 Core.Read{retained, result, exact} = certificate 1264 match result: 1265 case Fail{error}: 1266 ReadSuccessModel{Empty.absurd(ReadSuccess, 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 & 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 -> Empty}(present)} : Core.SourceRead -> Empty}(model))} 1275 case Done{value}: 1276 ReadSuccessModel{ReadSuccess{retained, value, exact}} 1277 1278 type ReadTotalInfo<-shape: Shape.Shape, -original: Core.Tensor, -index: U32> is Type: 1279 ReadTotalInfo{owner: Core.Tensor, same: {owner == original : Core.Tensor}, 1280 -present: PresentObservation, -model: Core.SourceRead} 1281 1282 def read_total_info(+shape: Shape.Shape, original: Core.Tensor, +index: U32, 1283 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 1284 ReadTotalInfo: 1285 ReadTotalInfo{original, {==}, present_observation(shape, original, index, inside), Core.source_read_model(shape, original, index)} 1286 1287 def read_total_certificate(-shape: Shape.Shape, -original: Core.Tensor, +index: U32, 1288 info: ReadTotalInfo) -> ReadSuccessModel: 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 1292 def read_success(+shape: Shape.Shape, original: Core.Tensor, +index: U32, 1293 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 1294 ReadSuccessModel: 1295 read_total_certificate(shape, original, index, read_total_info(shape, original, index, inside)) 1296 1297 def 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 1322 def 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 1341 def 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 1347 type ReshapeDecisionSuccess<-input: Shape.Shape, -target: Shape.Shape, -source: Core.Tensor, 1348 -decision: Shape.BoolCase> 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 1352 def reshape_decision_success(+input: Shape.Shape, +target: Shape.Shape, 1353 decision: Shape.BoolCase, source: Core.Tensor, 1354 -same: {Shape.elements(input) == Shape.elements(target) : Nat}) -> ReshapeDecisionSuccess: 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 1364 type ReshapeBuiltSuccess<-input: Shape.Shape, -target: Shape.Shape, -source: Core.Tensor, 1365 -built: Shape.ConstructResult> 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 1369 def reshape_built_success(+input: Shape.Shape, +target: Shape.Shape, 1370 built: Shape.ConstructResult, source: Core.Tensor, 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: 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 -> 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 1392 def Laws.reshape_valid_success(input, target, source, same): 1393 Transforms.ReshapeSuccessModel{ 1394 {\{ReshapeBuiltSuccess: success => success} : ReshapeBuiltSuccess -> 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 1398 type 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 1402 def 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: 1405 Core.Packed{+shape, tensor} = output 1406 DynamicRestoreSuccess{ 1407 {\{Transforms.ReshapeSuccessModel: success => success} : Transforms.ReshapeSuccessModel -> 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 1412 type 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 1415 def reshape_inverse_success_result(+input: Shape.Shape, -original: Core.Tensor, -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: 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 -> 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 -> 1433 {Result.is_done(&2, &1, Transforms.Error, Core.Dynamic, Transforms.reshape_dynamic(output, Shape.dimensions(input))) == True{} : Bool}}(meaning)} 1434 1435 def Laws.reshape_inverse_valid_success(input, target, source, same): 1436 Transforms.ReshapeInverseSuccessModel{ 1437 {\{ReshapeInverseSuccessResult: success => success} : 1438 ReshapeInverseSuccessResult -> 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 -> 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 -> 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 1448 def 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 1452 def read_success_status(-shape: Shape.Shape, -original: Core.Tensor, -index: U32, 1453 certificate: ReadSuccessModel) -> Totality.ReadSuccess: 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 & Result<&2, &2, Core.Error, F32>, Bool, Totality.read_succeeded(shape), 1459 (retained, Done{value}), Core.read_flat(shape, original, index), exact))} : 1460 ReadSuccess -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(success)} : 1461 ReadSuccessModel -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(certificate)} 1462 1463 def Laws.tensor_read_valid_success(shape, source, index, inside): 1464 read_success_status(shape, source, index, read_success(shape, source, index, inside)) 1465 1466 def 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 1470 type StorageWriteSuccess<-pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>> is Data: 1471 StorageWriteSuccess{-successful: {storage_write_succeeded(pair) == True{} : Bool}} 1472 1473 def storage_set_checked_success(+depth: Nat, +length: Nat, +index: U32, +value: F32, allowed: Bool, array: Array, 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: 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 1485 def 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 1497 def tensor_write_success(+shape: Shape.Shape, original: Core.Tensor, +index: U32, +value: F32, 1498 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Totality.WriteSuccess: 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 -> 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 1520 def Laws.tensor_write_valid_success(shape, target, index, value, inside): 1521 tensor_write_success(shape, target, index, value, inside) 1522 1523 def 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 1527 def permutation_length_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1528 decision: Shape.BoolCase, 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>}: 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>}, 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 1539 def 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>}: 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 1545 def permutation_bounds_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1546 decision: Shape.BoolCase, 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>}: 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>}, 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 1556 def permutation_bounds_ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1557 decision: Shape.BoolCase, 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>}: 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>}, 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 1569 def 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>}: 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 1576 def permutation_unique_decision_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1577 decision: Shape.BoolCase, duplicate: {False{} == Layout.unique(axes) : Bool}) -> 1578 {Layout.plan_unique(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan>}: 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>}, 1584 Lifecycle.false_true(Equal.trans(Bool, True{}, Layout.unique(axes), False{}, equal, Equal.sym(Bool, False{}, Layout.unique(axes), duplicate)))) 1585 1586 def permutation_duplicate_bounded_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1587 decision: Shape.BoolCase, 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>}: 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>}, 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 1598 def permutation_duplicate_ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>, 1599 decision: Shape.BoolCase, 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>}: 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>}, 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 1611 def 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>}: 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 1618 def permute_failure(+input: Shape.Shape, -source: Core.Tensor, +axes: List<&2, U32>, +error: Layout.Error, 1619 certificate: {Layout.permutation(input, axes) == Fail{error} : Result<&2, &2, Layout.Error, Layout.Plan>}) -> 1620 Totality.PermuteFailure: 1621 Totality.PermuteFailure{Equal.cong(Result<&2, &2, Layout.Error, Layout.Plan>, 1622 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic>, result => Transforms.copy_planned(input, axes, source, result), 1623 Layout.permutation(input, axes), Fail{error}, certificate)} 1624 1625 def Laws.permute_axes_length_rejection(input, source, axes, wrong): 1626 Totality.PermuteFailure{ 1627 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure -> 1628 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.AxesLengthMismatch{}}}) : 1629 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic>}}( 1630 permute_failure(input, source, axes, Layout.AxesLengthMismatch{}, permutation_length_failure(input, axes, wrong)))} 1631 1632 def Laws.permute_axis_bounds_rejection(input, source, axes, ranked, outside): 1633 Totality.PermuteFailure{ 1634 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure -> 1635 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : 1636 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic>}}( 1637 permute_failure(input, source, axes, Layout.AxisOutOfBounds{}, permutation_bounds_failure(input, axes, ranked, outside)))} 1638 1639 def Laws.permute_duplicate_axes_rejection(input, source, axes, ranked, bounded, duplicate): 1640 Totality.PermuteFailure{ 1641 {\{Totality.PermuteFailure: exact => exact} : Totality.PermuteFailure -> 1642 {Transforms.permute_copy(input, source, axes) == (source, Fail{Transforms.LayoutError{Layout.DuplicateAxis{}}}) : 1643 Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic>}}( 1644 permute_failure(input, source, axes, Layout.DuplicateAxis{}, permutation_duplicate_failure(input, axes, ranked, bounded, duplicate)))} 1645 1646 type TransposeDecidedFailure<-input: Shape.Shape, -source: Core.Tensor, -a: U32, -b: U32, 1647 -decision: Shape.BoolCase> is Data: 1648 TransposeDecidedFailure{-exact: {Transforms.transpose_decided(input, source, a, b, decision) == 1649 (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor & Result<&2, &1, Transforms.Error, Core.Dynamic>}} 1650 1651 def transpose_decided_failure(+input: Shape.Shape, +a: U32, +b: U32, 1652 decision: Shape.BoolCase, source: Core.Tensor, 1653 -outside: {False{} == TransposeSpec.valid(input, a, b) : Bool}) -> 1654 TransposeDecidedFailure: 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 & 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 1664 def Laws.transpose_axis_bounds_rejection(input, source, a, b, outside): 1665 Totality.TransposeFailure{ 1666 {\{TransposeDecidedFailure: exact => exact} : 1667 TransposeDecidedFailure -> 1668 {Transforms.transpose_copy(input, source, a, b) == (source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : 1669 Core.Tensor & 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 1672 def reshape_decided_failure(+input: Shape.Shape, +target: Shape.Shape, 1673 decision: Shape.BoolCase, -source: Core.Tensor, 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 1686 def reshape_built_failure(+input: Shape.Shape, +target: Shape.Shape, built: Shape.ConstructResult, -source: Core.Tensor, 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 1706 def 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 1709 def mapping_decided_failure(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 1710 decision: Shape.BoolCase, 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>}: 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>}, 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 1723 def 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 1726 def 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 1735 def 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 1756 def 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 1772 def 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 1776 def Laws.natural_cursor_exact_conversion(shape, cursor, within): 1777 Transforms.CursorExact{Mapping.cursor_word_exact(shape, cursor, within)} 1778 1779 def copy_written_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 1780 pair: Core.Tensor & Result<&2, &2, Core.Error, Unit>, -source: Core.Tensor, 1781 -successful: {Totality.write_succeeded(Layout.output(input, axes, plan), pair) == True{} : Bool}) -> 1782 Totality.CopySuccess 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 1791 def copy_value_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 1792 -source: Core.Tensor, target: Core.Tensor, +value: F32, 1793 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) -> 1794 Totality.CopySuccess 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 -> 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 1811 def copy_read_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, +source_index: U32, 1812 -source: Core.Tensor, target: Core.Tensor, 1813 certificate: ReadSuccessModel, 1814 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) -> 1815 Totality.CopySuccess 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 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 -> 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 -> 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 1835 def copy_mapped_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 1836 mapped: Result<&2, &2, Layout.Error, Layout.Mapping>, 1837 source: Core.Tensor, target: Core.Tensor, 1838 +successful: {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, mapped) == True{} : Bool}, 1839 +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) -> 1840 Totality.CopySuccess 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 1850 def Laws.copy_step_valid_success(input, axes, plan, source, target, index, inside): 1851 Totality.CopyStepSuccess{ 1852 {\{Totality.CopySuccess: successful => successful} : 1853 Totality.CopySuccess -> 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 -> 1858 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, Layout.map_index(input, axes, plan, index)) == True{} : Bool}}( 1859 Laws.mapping_valid_success(input, axes, plan, index, inside)), inside))} 1860 1861 def natural_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, +index: U32, 1862 decision: Shape.BoolCase, source: Core.Tensor, target: Core.Tensor, 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: 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 -> 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 1877 def 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 1883 def 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 1890 def loop_pair_success(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 1891 pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 1892 -successful: {Totality.copy_succeeded(input, axes, plan, pair) == True{} : Bool}, 1893 rec: @source: Core.Tensor -> @target: Core.Tensor -> 1894 Totality.CopySuccess) -> 1895 Totality.CopySuccess 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 1904 def loop_natural_success(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +cursor: Nat, 1905 result: Transforms.NaturalCopy, 1906 -successful: {Totality.natural_succeeded(input, axes, plan, cursor, result) == True{} : Bool}, 1907 rec: @source: Core.Tensor -> @target: Core.Tensor -> 1908 Totality.CopySuccess) -> 1909 Totality.CopySuccess 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 1917 def 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 -> 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 1935 def packed_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 1936 pair: Core.Tensor & Result<&2, &1, Transforms.Error, Core.Tensor>, 1937 -successful: {Totality.copy_succeeded(input, axes, plan, pair) == True{} : Bool}) -> 1938 Totality.PublicSuccess: 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 1946 def allocated_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, 1947 allocated: Result<&2, &1, Core.Error, Core.Tensor>, source: Core.Tensor, 1948 -certificate: AllocationSpec.TensorDone) -> 1949 Totality.PublicSuccess: 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>, Bool, 1955 Result.is_done(&2, &1, Core.Error, Core.Tensor), Done{tensor}, Fail{error}, same)))} : 1956 AllocationSpec.TensorDone -> {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 1964 def planned_success(+input: Shape.Shape, +axes: List<&2, U32>, planned: Result<&2, &2, Layout.Error, Layout.Plan>, source: Core.Tensor, 1965 -successful: {Result.is_done(&2, &2, Layout.Error, Layout.Plan, planned) == True{} : Bool}) -> 1966 Totality.PublicSuccess: 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 1974 def 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 -> 1977 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.permutation(input, axes)) == True{} : Bool}}( 1978 Laws.permutation_valid_success(input, axes, valid))) 1979 1980 def 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 1995 def 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))), Lines 1-2000 of 2553. More: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=2001