1 import Base 2 import ../shape/core.bend as Shape 3 import ./layout.bend as Layout 4 import ./lifecycle.bend as Lifecycle 5 import ../storage/arith.bend as Arith 6 import ../shape/coordinate_proofs.bend as Coordinates 7 import ../shape/nat_proofs.bend as Nats 8 import ./word_conversion.bend as WordConversion 9 import ../shape/LAWS.bend as ShapeLaws 10 import ../shape/PROOF.bend as ShapeProof 11 import ./axis_spec.bend as Axis 12 import ./axis_algebra.bend as AxisAlgebra 13 14 def permutation_checked(+input: Shape.Shape, +axes: List<&2, U32>, plan: Layout.Plan) -> 15 {True{} == Layout.bijective(input, axes) : Bool}: 16 Layout.Permutation{out, valid, ordered, count} = plan 17 valid 18 19 def and_left(a: Bool, -b: Bool, equal: {True{} == Bool.and(a, b) : Bool}) -> {True{} == a : Bool}: 20 match a: 21 case False{}: 22 equal 23 case True{}: 24 {==} 25 26 def and_right(a: Bool, -b: Bool, equal: {True{} == Bool.and(a, b) : Bool}) -> {True{} == b : Bool}: 27 match a: 28 case False{}: 29 Empty.absurd({True{} == b : Bool}, Lifecycle.false_true(equal)) 30 case True{}: 31 equal 32 33 def reverse_go_cancel(+values: List<&2, U32>, +accumulator: List<&2, U32>) -> 34 {Layout.reverse_words_go(Layout.reverse_words_go(values, accumulator), Nil{}) == 35 Layout.reverse_words_go(accumulator, values) : List<&2, U32>}: 36 match values: 37 case Nil{}: 38 {==} 39 case +head <> +tail: 40 reverse_go_cancel(tail, head <> accumulator) 41 42 def reverse_involution(+values: List<&2, U32>) -> {Layout.reverse_words(Layout.reverse_words(values)) == values : List<&2, U32>}: 43 reverse_go_cancel(values, Nil{}) 44 45 def codec_decoded(+dimensions: List<&2, U32>, +index: U32) -> 46 {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)) == 47 Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))) : List<&2, U32>}: 48 Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)), 49 Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))), 50 Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))), 51 Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)), 52 Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))), 53 Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))), 54 Equal.cong(List<&2, U32>, List<&2, U32>, dims => 55 Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dims, U32.to_nat(index))))), 56 Layout.reverse_words(Layout.reverse_words(dimensions)), dimensions, reverse_involution(dimensions)), 57 reverse_involution(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))), 58 Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Shape.digits_words(dimensions, U32.to_nat(index)), 59 Shape.digits(Shape.naturals(dimensions), U32.to_nat(index)), Coordinates.digits_words_spec(dimensions, U32.to_nat(index)))) 60 61 def coordinate_fits(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) -> 62 Coordinates.Fits(Shape.naturals(dimensions), Shape.naturals(values)): 63 match dimensions values: 64 case Nil{} Nil{}: 65 Unit{} 66 case +dimension <> +dt +value <> +vt: 67 Layout.WStep{bound, tail} = valid 68 Coordinates.FStep{ 69 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(value), U32.to_nat(dimension)), U32.is_lt(value, dimension), Arith.u32_lt(value, dimension)) : 70 {True{} == _ : Bool} 71 bound, 72 coordinate_fits(dt, vt, tail)} 73 case Nil{} head <> tail: 74 match valid: 75 case head <> tail Nil{}: 76 match valid: 77 78 def codec_flattened(+dimensions: List<&2, U32>, +values: List<&2, U32>, +valid: Layout.WordsValid(dimensions, values)) -> 79 {Layout.flatten_words(dimensions, values, 0) == U32.from_nat(Shape.offset(Shape.naturals(dimensions), Shape.naturals(values))) : U32}: 80 Equal.cong(Nat, U32, U32.from_nat, Shape.horner(dimensions, values, 0n), Shape.offset(Shape.naturals(dimensions), Shape.naturals(values)), 81 Coordinates.horner_spec(dimensions, values, 0n, coordinate_fits(dimensions, values, valid))) 82 83 def mapping_reference(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 84 mapping: Layout.Mapping) -> 85 {Some{Layout.source_index(input, axes, plan, index, mapping)} == Layout.reference_source(input, axes, plan, index) : Maybe<&2, U32>}: 86 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping 87 Layout.CWord{+values, +valid} = ic 88 %AxisAlgebra.inverse_coordinates(input, axes, 89 Shape.words(Shape.digits(Shape.extents(Layout.output(input, axes, plan)), U32.to_nat(index)))) : 90 {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input), _) : Maybe<&2, U32>} 91 %Equal.trans(List<&2, U32>, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 92 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)), 93 Shape.words(Shape.digits(Shape.extents(Layout.output(input, axes, plan)), U32.to_nat(index))), decoded, 94 codec_decoded(Shape.dimensions(Layout.output(input, axes, plan)), index)) : 95 {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input), 96 Layout.inverse_coordinates(Shape.dimensions(input), axes, _, 0)) : Maybe<&2, U32>} 97 %inverse : {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input), _) : Maybe<&2, U32>} 98 Equal.cong(U32, Maybe<&2, U32>, value => Some{value}, Layout.index_value(input, source), 99 U32.from_nat(Shape.offset(Shape.extents(input), Shape.naturals(values))), 100 Equal.trans(U32, Layout.index_value(input, source), Layout.flatten_words(Shape.dimensions(input), values, 0), 101 U32.from_nat(Shape.offset(Shape.extents(input), Shape.naturals(values))), flattened, 102 codec_flattened(Shape.dimensions(input), values, valid))) 103 104 def flat_mathematical_bounded(+shape: Shape.Shape, index: Layout.FlatIndex) -> 105 {Nat.is_lt(U32.to_nat(Layout.index_value(shape, index)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}: 106 Layout.FIndex{+value, bound} = index 107 %Shape.elements_exact(shape) : {Nat.is_lt(U32.to_nat(value), _) == True{} : Bool} 108 Arith.lt_le_trans(U32.to_nat(value), U32.to_nat(Shape.count(shape)), Shape.elements(shape), 109 Equal.trans(Bool, Nat.is_lt(U32.to_nat(value), U32.to_nat(Shape.count(shape))), U32.is_lt(value, Shape.count(shape)), True{}, 110 Arith.u32_lt(value, Shape.count(shape)), Equal.sym(Bool, True{}, U32.is_lt(value, Shape.count(shape)), bound)), 111 WordConversion.natural_word_le(Shape.elements(shape))) 112 113 def decoded_coordinate(+shape: Shape.Shape, +index: U32, 114 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> Shape.Coordinate(Shape.extents(shape)): 115 Shape.unflatten(Shape.extents(shape), Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), 116 Coordinates.size_fits(shape, U32.to_nat(index), inside))) 117 118 def decoded_indices(+shape: Shape.Shape, +index: U32, 119 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> 120 {Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)) == 121 Shape.digits(Shape.extents(shape), U32.to_nat(index)) : List<&2, Nat>}: 122 Equal.trans(List<&2, Nat>, Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)), 123 Shape.digits(Shape.extents(shape), Shape.Fin.value(Shape.numel(Shape.extents(shape)), 124 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)))), 125 Shape.digits(Shape.extents(shape), U32.to_nat(index)), 126 Coordinates.digits_unflatten(Shape.extents(shape), 127 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))), 128 Equal.cong(Nat, List<&2, Nat>, value => Shape.digits(Shape.extents(shape), value), 129 Shape.Fin.value(Shape.numel(Shape.extents(shape)), 130 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))), 131 U32.to_nat(index), Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), U32.to_nat(index), 132 Coordinates.size_fits(shape, U32.to_nat(index), inside)))) 133 134 def decoded_fit(+shape: Shape.Shape, +index: U32, 135 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> 136 {True{} == Shape.fit(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index))) : Bool}: 137 %decoded_indices(shape, index, inside) : {True{} == Shape.fit(Shape.extents(shape), _) : Bool} 138 Coordinates.fit_indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)) 139 140 def decoded_word_fits(+shape: Shape.Shape, +index: U32, 141 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> 142 Coordinates.Fits(Shape.extents(shape), Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))))): 143 %Equal.sym(List<&2, Nat>, Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index)))), 144 Shape.digits(Shape.extents(shape), U32.to_nat(index)), 145 WordConversion.naturals_words_fitting(Shape.dimensions(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside))) : 146 Coordinates.Fits(Shape.extents(shape), _) 147 Coordinates.fits_of(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside)) 148 149 def element_counts_same(+input: Shape.Shape, +target: Shape.Shape, 150 same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) -> 151 {Shape.elements(input) == Shape.elements(target) : Nat}: 152 Equal.trans(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements(target), Shape.elements_exact(input), 153 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Shape.elements(target), same, 154 Equal.sym(Nat, Shape.elements(target), Shape.logical_numel(Shape.dimensions(target)), Shape.elements_exact(target)))) 155 156 def natural_equal_true(+left: Nat, +right: Nat, same: {left == right : Nat}) -> {Nat.is_eq(left, right) == True{} : Bool}: 157 %same : {Nat.is_eq(left, _) == True{} : Bool} 158 Arith.eq_refl(left) 159 160 def metadata_present(value: Maybe<&2, List<&2, U32>>) -> Bool: 161 match value: 162 case None{}: 163 False{} 164 case Some{values}: 165 True{} 166 167 def reordered_rank_bound(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 168 Shape.LE(Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), 4n): 169 match input: 170 case Shape.SShape{+dimensions, +size, +exact, +rank_bound, +capacity_bound}: 171 %Equal.sym(Nat, Shape.rank_dimensions(Axis.order(U32, dimensions, Shape.naturals(axes))), Shape.rank_dimensions(dimensions), 172 AxisAlgebra.permutation_rank(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, axes, valid)) : Shape.LE(_, 4n) 173 rank_bound 174 175 def reordered_capacity_bound(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 176 Shape.LE(Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), 1048576n): 177 match input: 178 case Shape.SShape{+dimensions, +size, +exact, +rank_bound, +capacity_bound}: 179 %Equal.sym(Nat, Shape.logical_numel(Axis.order(U32, dimensions, Shape.naturals(axes))), Shape.logical_numel(dimensions), 180 AxisAlgebra.permutation_product(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, axes, valid)) : Shape.LE(_, 1048576n) 181 capacity_bound 182 183 def reordered_construct_complete(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 184 {ShapeLaws.built(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), 185 Shape.construct(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)))) == 186 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))} : Maybe<&2, List<&2, U32>>}: 187 ShapeLaws.construction_complete(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), 188 reordered_rank_bound(input, axes, valid), reordered_capacity_bound(input, axes, valid)) 189 190 def selected_construct_complete(+input: Shape.Shape, +axes: List<&2, U32>, +dimensions: List<&2, U32>, 191 +valid: {True{} == Layout.bijective(input, axes) : Bool}, 192 same: {dimensions == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) -> 193 {ShapeLaws.built(dimensions, Shape.construct(dimensions)) == Some{dimensions} : Maybe<&2, List<&2, U32>>}: 194 %Equal.sym(List<&2, U32>, dimensions, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), same) : 195 {ShapeLaws.built(_, Shape.construct(_)) == Some{_} : Maybe<&2, List<&2, U32>>} 196 reordered_construct_complete(input, axes, valid) 197 198 def reordered_elements_same(+input: Shape.Shape, +axes: List<&2, U32>, +output: Shape.Shape, 199 +valid: {True{} == Layout.bijective(input, axes) : Bool}, 200 preserved: {Shape.dimensions(output) == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) -> 201 {Shape.elements(input) == Shape.elements(output) : Nat}: 202 element_counts_same(input, output, 203 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), 204 Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.logical_numel(Shape.dimensions(output)), 205 Equal.sym(Nat, Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.logical_numel(Shape.dimensions(input)), 206 AxisAlgebra.permutation_product(input, axes, valid)), 207 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), Shape.dimensions(output), 208 Equal.sym(List<&2, U32>, Shape.dimensions(output), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), preserved)))) 209 210 def plan_counted_success(+input: Shape.Shape, +axes: List<&2, U32>, +output: Shape.Shape, 211 +valid: {True{} == Layout.bijective(input, axes) : Bool}, 212 +ordered: {Some{Shape.dimensions(output)} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>}, 213 decision: Shape.BoolCase, 214 same: {Shape.elements(input) == Shape.elements(output) : Nat}) -> 215 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_counted(input, axes, output, valid, ordered, decision)) == True{} : Bool}: 216 match decision: 217 case Shape.BFalse{equal}: 218 Empty.absurd({False{} == True{} : Bool}, 219 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(output)), True{}, equal, 220 natural_equal_true(Shape.elements(input), Shape.elements(output), same)))) 221 case Shape.BTrue{equal}: 222 {==} 223 224 def plan_built_success(+input: Shape.Shape, +axes: List<&2, U32>, +dimensions: List<&2, U32>, 225 +valid: {True{} == Layout.bijective(input, axes) : Bool}, 226 +selected: {Some{dimensions} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>}, 227 built: Shape.ConstructResult, 228 complete: {ShapeLaws.built(dimensions, built) == Some{dimensions} : Maybe<&2, List<&2, U32>>}, 229 +same: {dimensions == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) -> 230 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_built(input, axes, dimensions, valid, selected, built)) == True{} : Bool}: 231 match built: 232 case Shape.SError{error}: 233 Empty.absurd({False{} == True{} : Bool}, 234 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{}, Some{dimensions}, complete))) 235 case Shape.SBuilt{+output, +preserved}: 236 plan_counted_success(input, axes, output, valid, 237 Equal.trans(Maybe<&2, List<&2, U32>>, Some{Shape.dimensions(output)}, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes), 238 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, values => Some{values}, Shape.dimensions(output), dimensions, preserved), selected), 239 Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), 240 reordered_elements_same(input, axes, output, valid, 241 Equal.trans(List<&2, U32>, Shape.dimensions(output), dimensions, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), preserved, same))) 242 243 def plan_selected_success(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}, 244 selected: Maybe<&2, List<&2, U32>>, +same: {selected == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>}) -> 245 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_selected(input, axes, valid, selected, same)) == True{} : Bool}: 246 match selected: 247 case None{}: 248 Empty.absurd({False{} == True{} : Bool}, 249 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{}, 250 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, 251 Equal.trans(Maybe<&2, List<&2, U32>>, None{}, Layout.reorder(Shape.dimensions(input), axes), 252 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid))))) 253 case Some{+dimensions}: 254 plan_built_success(input, axes, dimensions, valid, same, Shape.construct(dimensions), 255 selected_construct_complete(input, axes, dimensions, valid, 256 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{dimensions}, 257 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, 258 Equal.trans(Maybe<&2, List<&2, U32>>, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes), 259 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid)))), 260 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{dimensions}, 261 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, 262 Equal.trans(Maybe<&2, List<&2, U32>>, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes), 263 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid)))) 264 265 def plan_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase, 266 +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 267 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_decided(input, axes, decision)) == True{} : Bool}: 268 match decision: 269 case Shape.BFalse{equal}: 270 Empty.absurd({False{} == True{} : Bool}, 271 Arith.clash(Equal.trans(Bool, False{}, Layout.bijective(input, axes), True{}, equal, 272 Equal.sym(Bool, True{}, Layout.bijective(input, axes), valid)))) 273 case Shape.BTrue{equal}: 274 plan_selected_success(input, axes, equal, Layout.reorder(Shape.dimensions(input), axes), {==}) 275 276 def plan_unique_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase, 277 +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 278 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_unique(input, axes, decision)) == True{} : Bool}: 279 match decision: 280 case Shape.BFalse{equal}: 281 Empty.absurd({False{} == True{} : Bool}, 282 Arith.clash(Equal.trans(Bool, False{}, Layout.unique(axes), True{}, equal, 283 Equal.sym(Bool, True{}, Layout.unique(axes), 284 and_right(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes), 285 and_right(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), 286 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid)))))) 287 case Shape.BTrue{equal}: 288 plan_decided_success(input, axes, Shape.bool_case(Layout.bijective(input, axes)), valid) 289 290 def plan_bounded_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase, 291 +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 292 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_bounded(input, axes, decision)) == True{} : Bool}: 293 match decision: 294 case Shape.BFalse{equal}: 295 Empty.absurd({False{} == True{} : Bool}, 296 Arith.clash(Equal.trans(Bool, False{}, Layout.bounded(axes, Shape.rank(input)), True{}, equal, 297 Equal.sym(Bool, True{}, Layout.bounded(axes, Shape.rank(input)), 298 and_left(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes), 299 and_right(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), 300 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid)))))) 301 case Shape.BTrue{equal}: 302 plan_unique_success(input, axes, Shape.bool_case(Layout.unique(axes)), valid) 303 304 def plan_ranked_success(+input: Shape.Shape, +axes: List<&2, U32>, 305 decision: Shape.BoolCase, 306 +valid: {True{} == Layout.bijective(input, axes) : Bool}) -> 307 {Result.is_done(&2, &2, Layout.Error, Layout.Plan, Layout.plan_ranked(input, axes, decision)) == True{} : Bool}: 308 match decision: 309 case Shape.BFalse{equal}: 310 Empty.absurd({False{} == True{} : Bool}, 311 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, equal, 312 Equal.sym(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), 313 and_left(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), 314 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid))))) 315 case Shape.BTrue{equal}: 316 plan_bounded_success(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), valid) 317 318 def words_valid_of(+dimensions: List<&2, U32>, +values: List<&2, U32>, 319 fits: Coordinates.Fits(Shape.naturals(dimensions), Shape.naturals(values))) -> Layout.WordsValid(dimensions, values): 320 match dimensions values: 321 case Nil{} Nil{}: 322 Unit{} 323 case +dimension <> +dt +value <> +vt: 324 Coordinates.FStep{bound, tail} = fits 325 Layout.WStep{ 326 %Arith.u32_lt(value, dimension) : {True{} == _ : Bool} 327 bound, 328 words_valid_of(dt, vt, tail)} 329 case Nil{} head <> tail: 330 match fits: 331 case head <> tail Nil{}: 332 match fits: 333 334 def words_finish_success(-dimension: U32, -dt: List<&2, U32>, -value: U32, -vt: List<&2, U32>, 335 bound: {True{} == U32.is_lt(value, dimension) : Bool}, result: Result<&2, &2, Shape.Error, Layout.WordsValid(dt, vt)>, 336 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dt, vt), result) == True{} : Bool}) -> 337 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimension <> dt, value <> vt), 338 Layout.words_finish(dimension, dt, value, vt, bound, result)) == True{} : Bool}: 339 match result: 340 case Fail{error}: 341 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful)) 342 case Done{tail}: 343 {==} 344 345 def words_decided_success(+dimension: U32, +dt: List<&2, U32>, +value: U32, +vt: List<&2, U32>, 346 decision: Shape.BoolCase, bound: {True{} == U32.is_lt(value, dimension) : Bool}, 347 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dt, vt), Layout.words_check(dt, vt)) == True{} : Bool}) -> 348 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimension <> dt, value <> vt), 349 Layout.words_decided(dimension, dt, value, vt, unit => Layout.words_check(dt, vt), decision)) == True{} : Bool}: 350 match decision: 351 case Shape.BFalse{equal}: 352 Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(Equal.trans(Bool, True{}, U32.is_lt(value, dimension), False{}, bound, 353 Equal.sym(Bool, False{}, U32.is_lt(value, dimension), equal)))) 354 case Shape.BTrue{equal}: 355 words_finish_success(dimension, dt, value, vt, equal, Layout.words_check(dt, vt), successful) 356 357 def words_check_success(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) -> 358 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimensions, values), Layout.words_check(dimensions, values)) == True{} : Bool}: 359 match dimensions values: 360 case Nil{} Nil{}: 361 {==} 362 case +dimension <> +dt +value <> +vt: 363 Layout.WStep{bound, tail} = valid 364 words_decided_success(dimension, dt, value, vt, Shape.bool_case(U32.is_lt(value, dimension)), bound, words_check_success(dt, vt, tail)) 365 case Nil{} head <> tail: 366 match valid: 367 case head <> tail Nil{}: 368 match valid: 369 370 def decoded_words_valid(+shape: Shape.Shape, +index: U32, 371 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> 372 Layout.WordsValid(Shape.dimensions(shape), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index))): 373 %Equal.sym(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index)), 374 Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), codec_decoded(Shape.dimensions(shape), index)) : 375 Layout.WordsValid(Shape.dimensions(shape), _) 376 words_valid_of(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), decoded_word_fits(shape, index, inside)) 377 378 def coordinate_offset_bound(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) -> 379 Shape.LT(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape)): 380 %Equal.sym(Nat, Shape.elements(shape), Shape.numel(Shape.extents(shape)), Shape.elements_exact(shape)) : 381 Shape.LT(Shape.offset(Shape.extents(shape), Shape.naturals(values)), _) 382 %Coordinates.offset_of(Shape.extents(shape), Shape.naturals(values), coordinate_fits(Shape.dimensions(shape), values, valid)) : 383 Shape.LT(_, Shape.numel(Shape.extents(shape))) 384 Coordinates.row_major_lt(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), 385 coordinate_fits(Shape.dimensions(shape), values, valid))) 386 387 def coordinate_offset_exact(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) -> 388 {U32.to_nat(U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values)))) == Shape.offset(Shape.extents(shape), Shape.naturals(values)) : Nat}: 389 WordConversion.natural_word_exact(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.count(shape), 390 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : 391 {Nat.is_le(Shape.offset(Shape.extents(shape), Shape.naturals(values)), _) == True{} : Bool} 392 WordConversion.lt_le(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape), 393 Equal.sym(Bool, True{}, Nat.is_lt(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape)), 394 Nats.lt_true(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape), coordinate_offset_bound(shape, values, valid))))) 395 396 def coordinate_flatten_exact(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) -> 397 {U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)) == Shape.offset(Shape.extents(shape), Shape.naturals(values)) : Nat}: 398 Equal.trans(Nat, U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)), 399 U32.to_nat(U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values)))), Shape.offset(Shape.extents(shape), Shape.naturals(values)), 400 Equal.cong(U32, Nat, U32.to_nat, Layout.flatten_words(Shape.dimensions(shape), values, 0), 401 U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values))), codec_flattened(Shape.dimensions(shape), values, valid)), 402 coordinate_offset_exact(shape, values, valid)) 403 404 def words_valid_rank(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) -> 405 {Shape.rank_dimensions(values) == Shape.rank_dimensions(dimensions) : Nat}: 406 match dimensions values: 407 case Nil{} Nil{}: 408 {==} 409 case +dimension <> +dt +value <> +vt: 410 Layout.WStep{bound, tail} = valid 411 Equal.cong(Nat, Nat, n => 1n+n, Shape.rank_dimensions(vt), Shape.rank_dimensions(dt), words_valid_rank(dt, vt, tail)) 412 case Nil{} head <> tail: 413 match valid: 414 case head <> tail Nil{}: 415 match valid: 416 417 def words_fit_true(+dimensions: List<&2, U32>, +values: List<&2, U32>, +valid: Layout.WordsValid(dimensions, values)) -> 418 {True{} == Shape.fit(Shape.naturals(dimensions), Shape.naturals(values)) : Bool}: 419 %Coordinates.indices_of(Shape.naturals(dimensions), Shape.naturals(values), coordinate_fits(dimensions, values, valid)) : 420 {True{} == Shape.fit(Shape.naturals(dimensions), _) : Bool} 421 Coordinates.fit_indices(Shape.naturals(dimensions), Coordinates.coordinate_of(Shape.naturals(dimensions), Shape.naturals(values), 422 coordinate_fits(dimensions, values, valid))) 423 424 def permutation_dimensions_order(+input: Shape.Shape, +axes: List<&2, U32>, plan: Layout.Plan) -> 425 {Shape.dimensions(Layout.output(input, axes, plan)) == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}: 426 Layout.Permutation{+output, valid, ordered, count} = plan 427 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{Shape.dimensions(output)}, 428 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, 429 Equal.trans(Maybe<&2, List<&2, U32>>, Some{Shape.dimensions(output)}, Layout.reorder(Shape.dimensions(input), axes), 430 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, ordered, AxisAlgebra.permutation_complete(input, axes, valid))) 431 432 def shape_rank_bound(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n): 433 match shape: 434 case Shape.SShape{dimensions, size, exact, ranked, capacity}: 435 ranked 436 437 def reverse_restored(-A: Data, -rank: Nat, -axes: List<&2, Nat>, -items: List<&2, A>, certificate: AxisAlgebra.ListFacts) -> 438 {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}: 439 AxisAlgebra.Lists{selected, ranked, scattered, restored, reverse, scatter_restored} = certificate 440 reverse 441 442 def natural_coordinate_length(+input: Shape.Shape, +coordinates: List<&2, U32>, 443 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}) -> 444 {List.length(&2, Nat, Shape.naturals(coordinates)) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}: 445 Equal.trans(Nat, List.length(&2, Nat, Shape.naturals(coordinates)), Shape.rank_dimensions(coordinates), Shape.rank_dimensions(Shape.dimensions(input)), 446 Equal.sym(Nat, Shape.rank_dimensions(coordinates), List.length(&2, Nat, Shape.naturals(coordinates)), Shape.rank_naturals(coordinates)), length) 447 448 def inverse_coordinate_length(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>, 449 accepted: {True{} == Layout.bijective(input, axes) : Bool}, 450 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}) -> 451 {List.length(&2, Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))) == 452 Shape.rank_dimensions(Shape.dimensions(input)) : Nat}: 453 AxisAlgebra.ranked(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), 454 Shape.naturals(coordinates), 455 AxisAlgebra.facts_lists(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), 456 Shape.naturals(coordinates), natural_coordinate_length(input, coordinates, length), 457 AxisAlgebra.facts(Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), 458 shape_rank_bound(input), AxisAlgebra.facts_inverse_valid(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), AxisAlgebra.shape_facts(input, axes, accepted))))) 459 460 def inverse_coordinate_fit_certified(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>, 461 +accepted: {True{} == Layout.bijective(input, axes) : Bool}, 462 +length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}, 463 fitted: {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.naturals(coordinates)) : Bool}, 464 certificate: AxisAlgebra.Facts) -> 465 {True{} == Shape.fit(Shape.extents(input), 466 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))))) : Bool}: 467 AxisAlgebra.Certified{iv, selected, restored, lists, product, fit} = certificate 468 %Equal.sym(List<&2, Nat>, 469 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))), 470 Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), 471 AxisAlgebra.order_naturals(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), coordinates)) : 472 {True{} == Shape.fit(Shape.extents(input), _) : Bool} 473 Equal.trans(Bool, True{}, 474 Shape.fit(Axis.order(Nat, Shape.extents(input), Shape.naturals(axes)), 475 Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes))), 476 Shape.fit(Shape.extents(input), Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))), 477 %AxisAlgebra.order_naturals(Shape.naturals(axes), Shape.dimensions(input)) : 478 {True{} == Shape.fit(_, Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes))) : Bool} 479 %Equal.sym(List<&2, Nat>, 480 Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes)), 481 Shape.naturals(coordinates), reverse_restored(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Shape.naturals(coordinates), 482 AxisAlgebra.facts_lists(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Shape.naturals(coordinates), 483 natural_coordinate_length(input, coordinates, length), AxisAlgebra.shape_facts(input, axes, accepted)))) : 484 {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), _) : Bool} 485 fitted, 486 fit(Shape.extents(input), Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), 487 Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(input)), List.length(&2, Nat, Shape.extents(input)), Shape.rank_naturals(Shape.dimensions(input))), 488 inverse_coordinate_length(input, axes, coordinates, accepted, length))) 489 490 def inverse_coordinate_fit(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>, 491 +accepted: {True{} == Layout.bijective(input, axes) : Bool}, 492 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}, 493 fitted: {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.naturals(coordinates)) : Bool}) -> 494 {True{} == Shape.fit(Shape.extents(input), 495 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))))) : Bool}: 496 inverse_coordinate_fit_certified(input, axes, coordinates, accepted, length, fitted, AxisAlgebra.shape_facts(input, axes, accepted)) 497 498 def output_coordinate_rank(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +coordinate: Layout.CheckedCoordinate) -> 499 {Shape.rank_dimensions(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}: 500 Layout.Permutation{+output, +accepted, +ordered, +count} = plan 501 Layout.CWord{+values, valid} = coordinate 502 Equal.trans(Nat, Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(Shape.dimensions(input)), 503 words_valid_rank(Shape.dimensions(output), values, valid), 504 Equal.trans(Nat, Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), 505 Shape.rank_dimensions(Shape.dimensions(input)), 506 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, Shape.dimensions(output), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), 507 permutation_dimensions_order(input, axes, Layout.Permutation{output, accepted, ordered, count})), AxisAlgebra.permutation_rank(input, axes, accepted))) 508 509 def inverse_words_valid(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +coordinate: Layout.CheckedCoordinate, 510 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) -> 511 Layout.WordsValid(Shape.dimensions(input), values): 512 Layout.Permutation{+output, +accepted, +ordered, +count} = plan 513 Layout.CWord{+coordinates, +valid} = coordinate 514 %Equal.sym(List<&2, U32>, values, Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), 515 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{values}, 516 Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, 517 Equal.trans(Maybe<&2, List<&2, U32>>, Some{values}, Layout.inverse_coordinates(Shape.dimensions(input), axes, coordinates, 0), 518 Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, inverse, 519 AxisAlgebra.scatter_complete(input, axes, coordinates, accepted, 520 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}))))) : 521 Layout.WordsValid(Shape.dimensions(input), _) 522 words_valid_of(Shape.dimensions(input), Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), 523 Coordinates.fits_of(Shape.extents(input), 524 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))), 525 inverse_coordinate_fit(input, axes, coordinates, accepted, 526 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}), 527 %permutation_dimensions_order(input, axes, Layout.Permutation{output, accepted, ordered, count}) : 528 {True{} == Shape.fit(Shape.naturals(_), Shape.naturals(coordinates)) : Bool} 529 words_fit_true(Shape.dimensions(output), coordinates, valid)))) 530 531 def coordinate_flatten_bounded(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) -> 532 {True{} == U32.is_lt(Layout.flatten_words(Shape.dimensions(shape), values, 0), Shape.count(shape)) : Bool}: 533 %Arith.u32_lt(Layout.flatten_words(Shape.dimensions(shape), values, 0), Shape.count(shape)) : {True{} == _ : Bool} 534 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : 535 {True{} == Nat.is_lt(U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)), _) : Bool} 536 %Equal.sym(Nat, U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)), Shape.offset(Shape.extents(shape), Shape.naturals(values)), 537 coordinate_flatten_exact(shape, values, valid)) : {True{} == Nat.is_lt(_, Shape.elements(shape)) : Bool} 538 Nats.lt_true(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape), coordinate_offset_bound(shape, values, valid)) 539 540 def checked_coordinate_flatten_bounded(+shape: Shape.Shape, coordinate: Layout.CheckedCoordinate) -> 541 {True{} == U32.is_lt(Layout.flatten_words(Shape.dimensions(shape), Layout.coordinate_values(shape, coordinate), 0), Shape.count(shape)) : Bool}: 542 Layout.CWord{values, valid} = coordinate 543 coordinate_flatten_bounded(shape, values, valid) 544 545 def word_same_refl(+width: Nat, +word: Word(width)) -> {Layout.word_same(width, word, word) == True{} : Bool}: 546 match width: 547 case 0n: 548 {==} 549 case 1n+p: 550 match word: 551 case WCon{False{}, +tail}: 552 word_same_refl(p, tail) 553 case WCon{True{}, +tail}: 554 word_same_refl(p, tail) 555 556 def word_value_same_refl(+value: U32) -> {Layout.word_value_same(value, value) == True{} : Bool}: 557 match value: 558 case U32{+word}: 559 word_same_refl(32n, word) 560 561 def words_same_refl(+values: List<&2, U32>) -> {Layout.words_same(values, values) == True{} : Bool}: 562 match values: 563 case Nil{}: 564 {==} 565 case +head <> +tail: 566 %Equal.sym(Bool, Layout.word_value_same(head, head), True{}, word_value_same_refl(head)) : 567 {Bool.and(_, Layout.words_same(tail, tail)) == True{} : Bool} 568 words_same_refl(tail) 569 570 def inverse_words_order(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +coordinate: Layout.CheckedCoordinate, 571 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) -> 572 {values == Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 573 Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))) : List<&2, U32>}: 574 Layout.Permutation{output, accepted, ordered, count} = plan 575 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{values}, 576 Some{Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, 577 Equal.trans(Maybe<&2, List<&2, U32>>, Some{values}, Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(output, coordinate), 0), 578 Some{Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, inverse, 579 AxisAlgebra.scatter_complete(input, axes, Layout.coordinate_values(output, coordinate), accepted, 580 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate)))) 581 582 def inverse_words_reordered(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +coordinate: Layout.CheckedCoordinate, 583 +values: List<&2, U32>, +inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) -> 584 {Layout.reorder(values, axes) == Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)} : Maybe<&2, List<&2, U32>>}: 585 Layout.Permutation{+output, +accepted, +ordered, +count} = plan 586 Equal.trans(Maybe<&2, List<&2, U32>>, Layout.reorder(values, axes), Axis.gather(U32, values, Shape.naturals(axes)), 587 Some{Layout.coordinate_values(output, coordinate)}, AxisAlgebra.reorder(axes, values), 588 Equal.trans(Maybe<&2, List<&2, U32>>, Axis.gather(U32, values, Shape.naturals(axes)), Some{Axis.order(U32, values, Shape.naturals(axes))}, 589 Some{Layout.coordinate_values(output, coordinate)}, 590 AxisAlgebra.selected(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), values, 591 AxisAlgebra.facts_lists(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), values, 592 Equal.trans(Nat, List.length(&2, U32, values), Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(input)), 593 AxisAlgebra.word_length(values), words_valid_rank(Shape.dimensions(input), values, 594 inverse_words_valid(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate, values, inverse))), 595 AxisAlgebra.shape_facts(input, axes, accepted))), 596 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, items => Some{items}, Axis.order(U32, values, Shape.naturals(axes)), 597 Layout.coordinate_values(output, coordinate), 598 Equal.trans(List<&2, U32>, Axis.order(U32, values, Shape.naturals(axes)), 599 Axis.order(U32, Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes)), 600 Layout.coordinate_values(output, coordinate), 601 Equal.cong(List<&2, U32>, List<&2, U32>, items => Axis.order(U32, items, Shape.naturals(axes)), values, 602 Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), 603 inverse_words_order(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate, values, inverse)), 604 reverse_restored(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Layout.coordinate_values(output, coordinate), 605 AxisAlgebra.facts_lists(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Layout.coordinate_values(output, coordinate), 606 Equal.trans(Nat, List.length(&2, U32, Layout.coordinate_values(output, coordinate)), Shape.rank_dimensions(Layout.coordinate_values(output, coordinate)), 607 Shape.rank_dimensions(Shape.dimensions(input)), AxisAlgebra.word_length(Layout.coordinate_values(output, coordinate)), 608 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate)), AxisAlgebra.shape_facts(input, axes, accepted))))))) 609 610 def inverse_words_roundtrip(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +coordinate: Layout.CheckedCoordinate, 611 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) -> 612 {True{} == Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool}: 613 %Equal.sym(Maybe<&2, List<&2, U32>>, Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}, 614 inverse_words_reordered(input, axes, plan, coordinate, values, inverse)) : 615 {True{} == Layout.maybe_same(_, Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool} 616 Equal.sym(Bool, Layout.words_same(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)), True{}, 617 words_same_refl(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate))) 618 619 def mapping_flat_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 620 oi: Layout.FlatIndex, oc: Layout.CheckedCoordinate, +ic: Layout.CheckedCoordinate, 621 requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32}, 622 decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}, 623 inverse: {Some{Layout.coordinate_values(input, ic)} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}, 624 roundtrip: {True{} == Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}) : Bool}, 625 +source_index: U32, flat: {source_index == Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0) : U32}, 626 decision: Shape.BoolCase, bounded: {True{} == U32.is_lt(source_index, Shape.count(input)) : Bool}) -> 627 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, 628 Layout.map_flat(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, roundtrip, source_index, flat, decision)) == True{} : Bool}: 629 match decision: 630 case Shape.BFalse{equal}: 631 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, U32.is_lt(source_index, Shape.count(input)), True{}, equal, 632 Equal.sym(Bool, True{}, U32.is_lt(source_index, Shape.count(input)), bounded)))) 633 case Shape.BTrue{equal}: 634 {==} 635 636 def mapping_roundtrip_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 637 +oi: Layout.FlatIndex, +oc: Layout.CheckedCoordinate, +ic: Layout.CheckedCoordinate, 638 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32}, 639 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}, 640 +inverse: {Some{Layout.coordinate_values(input, ic)} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}, 641 decision: Shape.BoolCase, 642 roundtrip: {True{} == Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}) : Bool}) -> 643 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, 644 Layout.map_roundtrip(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, decision)) == True{} : Bool}: 645 match decision: 646 case Shape.BFalse{equal}: 647 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, 648 Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}), True{}, equal, 649 Equal.sym(Bool, True{}, Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}), roundtrip)))) 650 case Shape.BTrue{equal}: 651 mapping_flat_success(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, equal, 652 Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0), {==}, 653 Shape.bool_case(U32.is_lt(Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0), Shape.count(input))), 654 checked_coordinate_flatten_bounded(input, ic)) 655 656 def mapping_input_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 657 +oi: Layout.FlatIndex, +oc: Layout.CheckedCoordinate, 658 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32}, 659 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}, 660 +values: List<&2, U32>, +inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}, 661 checked: Result<&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values)>, 662 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values), checked) == True{} : Bool}) -> 663 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, 664 Layout.map_input(input, axes, plan, index, oi, oc, requested, decoded, values, inverse, checked)) == True{} : Bool}: 665 match checked: 666 case Fail{error}: 667 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful)) 668 case Done{+valid}: 669 mapping_roundtrip_success(input, axes, plan, index, oi, oc, Layout.CWord{values, valid}, requested, decoded, inverse, 670 Shape.bool_case(Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)})), 671 inverse_words_roundtrip(input, axes, plan, oc, values, inverse)) 672 673 def mapping_inverse_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 674 +oi: Layout.FlatIndex, +oc: Layout.CheckedCoordinate, 675 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32}, 676 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}, 677 result: Maybe<&2, List<&2, U32>>, 678 +same: {result == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}) -> 679 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, 680 Layout.map_inverse(input, axes, plan, index, oi, oc, requested, decoded, result, same)) == True{} : Bool}: 681 match result: 682 case None{}: 683 Empty.absurd({False{} == True{} : Bool}, 684 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{}, 685 Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, 686 Equal.trans(Maybe<&2, List<&2, U32>>, None{}, Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0), 687 Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, same, 688 AxisAlgebra.scatter_complete(input, axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), permutation_checked(input, axes, plan), 689 output_coordinate_rank(input, axes, plan, oc)))))) 690 case Some{+values}: 691 mapping_input_success(input, axes, plan, index, oi, oc, requested, decoded, values, same, Layout.words_check(Shape.dimensions(input), values), 692 words_check_success(Shape.dimensions(input), values, inverse_words_valid(input, axes, plan, oc, values, same))) 693 694 def mapping_output_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 695 +oi: Layout.FlatIndex, +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32}, 696 +values: List<&2, U32>, +decoded: {values == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>}, 697 checked: Result<&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(Layout.output(input, axes, plan)), values)>, 698 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(Layout.output(input, axes, plan)), values), checked) == True{} : Bool}) -> 699 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, 700 Layout.map_output(input, axes, plan, index, oi, requested, values, decoded, checked)) == True{} : Bool}: 701 match checked: 702 case Fail{error}: 703 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful)) 704 case Done{+valid}: 705 mapping_inverse_success(input, axes, plan, index, oi, Layout.CWord{values, valid}, requested, decoded, 706 Layout.inverse_coordinates(Shape.dimensions(input), axes, values, 0), {==}) 707 708 def mapping_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +index: U32, 709 decision: Shape.BoolCase, 710 inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) -> 711 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping, Layout.map_decided(input, axes, plan, index, decision)) == True{} : Bool}: 712 match decision: 713 case Shape.BFalse{equal}: 714 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), True{}, equal, 715 Equal.sym(Bool, True{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), inside)))) 716 case Shape.BTrue{+equal}: 717 mapping_output_success(input, axes, plan, index, Layout.FIndex{index, equal}, {==}, 718 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)), {==}, 719 Layout.words_check(Shape.dimensions(Layout.output(input, axes, plan)), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index))), 720 words_check_success(Shape.dimensions(Layout.output(input, axes, plan)), 721 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)), 722 decoded_words_valid(Layout.output(input, axes, plan), index, 723 %Equal.sym(Nat, Shape.elements(Layout.output(input, axes, plan)), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.elements_exact(Layout.output(input, axes, plan))) : 724 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool} 725 Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))), True{}, 726 flat_mathematical_bounded(Layout.output(input, axes, plan), Layout.FIndex{index, equal}))))) 727 728 def cursor_word_exact(+shape: Shape.Shape, +cursor: Nat, within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}) -> 729 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}: 730 WordConversion.natural_word_exact(cursor, Shape.count(shape), 731 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : 732 {Nat.is_le(cursor, _) == True{} : Bool} 733 within) 734 735 def cursor_index_bounded(+shape: Shape.Shape, +cursor: Nat, +inside: {True{} == Nat.is_lt(cursor, Shape.elements(shape)) : Bool}) -> 736 {True{} == U32.is_lt(U32.from_nat(cursor), Shape.count(shape)) : Bool}: 737 %Arith.u32_lt(U32.from_nat(cursor), Shape.count(shape)) : {True{} == _ : Bool} 738 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : 739 {True{} == Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) : Bool} 740 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_word_exact(shape, cursor, 741 WordConversion.lt_le(cursor, Shape.elements(shape), Equal.sym(Bool, True{}, Nat.is_lt(cursor, Shape.elements(shape)), inside)))) : 742 {True{} == Nat.is_lt(_, Shape.elements(shape)) : Bool} 743 inside 744 745 def permutation_output_rank(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan) -> 746 {Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}: 747 Equal.trans(Nat, Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))), 748 Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.rank_dimensions(Shape.dimensions(input)), 749 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, Shape.dimensions(Layout.output(input, axes, plan)), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), 750 permutation_dimensions_order(input, axes, plan)), AxisAlgebra.permutation_rank(input, axes, permutation_checked(input, axes, plan)))