1 import Base 2 import ../shape/core.bend as Shape 3 import ../storage/arith.bend as Arith 4 import ./axis_spec.bend as Axis 5 import ./axis_algebra.bend as Algebra 6 import ./axis_PROOF.bend as AxisProof 7 import ./layout.bend as Layout 8 import ./word_conversion.bend as Conversion 9 import ./transpose_spec.bend as Transpose 10 import ./transpose_LAWS.bend as Laws 11 import ./observation.bend as Values 12 import ./matmul.bend as Matrix 13 import ./matrix_index_proof.bend as MatrixIndex 14 import ../shape/nat_proofs.bend as Nats 15 16 def rank_bound(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n): 17 match shape: 18 case Shape.SShape{dims, size, exact, bound, capacity}: 19 bound 20 21 def inside_natural(+shape: Shape.Shape, +a: U32, +b: U32, 22 +inside: {True{} == Transpose.valid(shape, a, b) : Bool}) -> 23 {True{} == Transpose.axes_valid(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : Bool}: 24 inside 25 26 type AxesFacts<-dims: List<&2, U32>, -a: Nat, -b: Nat> is Data: 27 Certified{requested: {Layout.transpose_axes(dims, U32.from_nat(a), U32.from_nat(b), 0) == Transpose.requested_axes(Shape.rank_dimensions(dims), a, b) : List<&2, U32>}, 28 valid: {True{} == Axis.valid(Shape.rank_dimensions(dims), Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b))) : Bool}, 29 inverse: {Axis.inverse_axes(Shape.rank_dimensions(dims), Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b))) == Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b)) : List<&2, Nat>}} 30 31 def axes_facts(+dims: List<&2, U32>, +a: Nat, +b: Nat, +bound: Shape.LE(Shape.rank_dimensions(dims), 4n), 32 +inside: {True{} == Transpose.axes_valid(Shape.rank_dimensions(dims), a, b) : Bool}) -> AxesFacts: 33 match dims a b: 34 case Nil{} 0n 0n: 35 Certified{{==}, {==}, {==}} 36 case Nil{} 1n+p b: 37 Empty.absurd(AxesFacts, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside)))) 38 case Nil{} a 1n+p: 39 Empty.absurd(AxesFacts, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside)))) 40 case +d0 <> Nil{} 0n 0n: 41 Certified{{==}, {==}, {==}} 42 case +d0 <> Nil{} 1n+p b: 43 Empty.absurd(AxesFacts Nil{}, 1n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside)))) 44 case +d0 <> Nil{} a 1n+p: 45 Empty.absurd(AxesFacts Nil{}, a, 1n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside)))) 46 case +d0 <> +d1 <> Nil{} 0n 0n: 47 Certified{{==}, {==}, {==}} 48 case +d0 <> +d1 <> Nil{} 0n 1n: 49 Certified{{==}, {==}, {==}} 50 case +d0 <> +d1 <> Nil{} 1n 0n: 51 Certified{{==}, {==}, {==}} 52 case +d0 <> +d1 <> Nil{} 1n 1n: 53 Certified{{==}, {==}, {==}} 54 case +d0 <> +d1 <> Nil{} 2n+p b: 55 Empty.absurd(AxesFacts d1 <> Nil{}, 2n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n)), inside)))) 56 case +d0 <> +d1 <> Nil{} a 2n+p: 57 Empty.absurd(AxesFacts d1 <> Nil{}, a, 2n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n)), inside)))) 58 case +d0 <> +d1 <> +d2 <> Nil{} 0n 0n: 59 Certified{{==}, {==}, {==}} 60 case +d0 <> +d1 <> +d2 <> Nil{} 0n 1n: 61 Certified{{==}, {==}, {==}} 62 case +d0 <> +d1 <> +d2 <> Nil{} 0n 2n: 63 Certified{{==}, {==}, {==}} 64 case +d0 <> +d1 <> +d2 <> Nil{} 1n 0n: 65 Certified{{==}, {==}, {==}} 66 case +d0 <> +d1 <> +d2 <> Nil{} 1n 1n: 67 Certified{{==}, {==}, {==}} 68 case +d0 <> +d1 <> +d2 <> Nil{} 1n 2n: 69 Certified{{==}, {==}, {==}} 70 case +d0 <> +d1 <> +d2 <> Nil{} 2n 0n: 71 Certified{{==}, {==}, {==}} 72 case +d0 <> +d1 <> +d2 <> Nil{} 2n 1n: 73 Certified{{==}, {==}, {==}} 74 case +d0 <> +d1 <> +d2 <> Nil{} 2n 2n: 75 Certified{{==}, {==}, {==}} 76 case +d0 <> +d1 <> +d2 <> Nil{} 3n+p b: 77 Empty.absurd(AxesFacts d1 <> d2 <> Nil{}, 3n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n)), inside)))) 78 case +d0 <> +d1 <> +d2 <> Nil{} a 3n+p: 79 Empty.absurd(AxesFacts d1 <> d2 <> Nil{}, a, 3n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n)), inside)))) 80 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 0n: 81 Certified{{==}, {==}, {==}} 82 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 1n: 83 Certified{{==}, {==}, {==}} 84 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 2n: 85 Certified{{==}, {==}, {==}} 86 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 3n: 87 Certified{{==}, {==}, {==}} 88 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 0n: 89 Certified{{==}, {==}, {==}} 90 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 1n: 91 Certified{{==}, {==}, {==}} 92 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 2n: 93 Certified{{==}, {==}, {==}} 94 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 3n: 95 Certified{{==}, {==}, {==}} 96 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 0n: 97 Certified{{==}, {==}, {==}} 98 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 1n: 99 Certified{{==}, {==}, {==}} 100 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 2n: 101 Certified{{==}, {==}, {==}} 102 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 3n: 103 Certified{{==}, {==}, {==}} 104 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 0n: 105 Certified{{==}, {==}, {==}} 106 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 1n: 107 Certified{{==}, {==}, {==}} 108 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 2n: 109 Certified{{==}, {==}, {==}} 110 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 3n: 111 Certified{{==}, {==}, {==}} 112 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 4n+p b: 113 Empty.absurd(AxesFacts d1 <> d2 <> d3 <> Nil{}, 4n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n)), inside)))) 114 case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} a 4n+p: 115 Empty.absurd(AxesFacts d1 <> d2 <> d3 <> Nil{}, a, 4n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n)), inside)))) 116 case +d0 <> +d1 <> +d2 <> +d3 <> +d4 <> +tail a b: 117 match bound: 118 119 def requested(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts) -> 120 {Layout.transpose_axes(dims, U32.from_nat(a), U32.from_nat(b), 0) == Transpose.requested_axes(Shape.rank_dimensions(dims), a, b) : List<&2, U32>}: 121 Certified{requested, valid, inverse} = certificate 122 requested 123 124 def requested_valid(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts) -> 125 {True{} == Axis.valid(Shape.rank_dimensions(dims), Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b))) : Bool}: 126 Certified{requested, valid, inverse} = certificate 127 valid 128 129 def requested_inverse(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts) -> 130 {Axis.inverse_axes(Shape.rank_dimensions(dims), Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b))) == Shape.naturals(Transpose.requested_axes(Shape.rank_dimensions(dims), a, b)) : List<&2, Nat>}: 131 Certified{requested, valid, inverse} = certificate 132 inverse 133 134 def transpose_axes_requested(+shape: Shape.Shape, +a: U32, +b: U32, 135 +inside: {True{} == Transpose.valid(shape, a, b) : Bool}) -> 136 {Layout.transpose_axes(Shape.dimensions(shape), a, b, 0) == Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : List<&2, U32>}: 137 %Conversion.word_natural_exact(a) : {Layout.transpose_axes(Shape.dimensions(shape), _, b, 0) == Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : List<&2, U32>} 138 %Conversion.word_natural_exact(b) : {Layout.transpose_axes(Shape.dimensions(shape), U32.from_nat(U32.to_nat(a)), _, 0) == Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : List<&2, U32>} 139 requested(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), axes_facts(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), rank_bound(shape), inside_natural(shape, a, b, inside))) 140 141 def natural_valid_layout(+shape: Shape.Shape, +axes: List<&2, U32>, accepted: {True{} == Axis.valid(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(axes)) : Bool}) -> 142 {True{} == Layout.bijective(shape, axes) : Bool}: 143 %Equal.sym(Nat, Shape.rank_dimensions(axes), List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_naturals(axes)) : 144 {True{} == Bool.and(Nat.is_eq(_, Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Layout.bounded(axes, Shape.rank(shape)), Layout.unique(axes))) : Bool} 145 %Equal.sym(Bool, Layout.unique(axes), Axis.unique(Shape.naturals(axes)), Algebra.unique(axes)) : 146 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Layout.bounded(axes, Shape.rank(shape)), _)) : Bool} 147 %Equal.sym(Bool, Layout.bounded(axes, Shape.rank(shape)), Axis.bounded(Shape.naturals(axes), U32.to_nat(Shape.rank(shape))), Algebra.bounded(axes, Shape.rank(shape))) : 148 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(_, Axis.unique(Shape.naturals(axes)))) : Bool} 149 %Equal.sym(Nat, U32.to_nat(Shape.rank(shape)), Shape.rank_dimensions(Shape.dimensions(shape)), Algebra.rank_exact(shape)) : 150 {True{} == Bool.and(Nat.is_eq(List.length(&2, Nat, Shape.naturals(axes)), Shape.rank_dimensions(Shape.dimensions(shape))), Bool.and(Axis.bounded(Shape.naturals(axes), _), Axis.unique(Shape.naturals(axes)))) : Bool} 151 accepted 152 153 def valid_axes(+shape: Shape.Shape, +a: U32, +b: U32, 154 +inside: {True{} == Transpose.valid(shape, a, b) : Bool}) -> 155 {True{} == Layout.bijective(shape, Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : Bool}: 156 %Equal.sym(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(shape), a, b, 0), Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)), transpose_axes_requested(shape, a, b, inside)) : 157 {True{} == Layout.bijective(shape, _) : Bool} 158 natural_valid_layout(shape, Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)), 159 requested_valid(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), axes_facts(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), rank_bound(shape), inside_natural(shape, a, b, inside)))) 160 161 def inverse_axes(+shape: Shape.Shape, +a: U32, +b: U32, 162 +inside: {True{} == Transpose.valid(shape, a, b) : Bool}) -> 163 {Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0))) == Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : List<&2, Nat>}: 164 %Equal.sym(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(shape), a, b, 0), Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)), transpose_axes_requested(shape, a, b, inside)) : 165 {Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(_)) == Shape.naturals(_) : List<&2, Nat>} 166 requested_inverse(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), axes_facts(Shape.dimensions(shape), U32.to_nat(a), U32.to_nat(b), rank_bound(shape), inside_natural(shape, a, b, inside))) 167 168 def Laws.transpose_axes_requested(shape, a, b, inside): 169 transpose_axes_requested(shape, a, b, inside) 170 171 def Laws.transpose_axes_valid(shape, a, b, inside): 172 valid_axes(shape, a, b, inside) 173 174 def Laws.transpose_axes_self_inverse(shape, a, b, inside): 175 inverse_axes(shape, a, b, inside) 176 177 # What `permute_source(input, [1, 0], index)` computes once the input's 178 # dimensions are known. 179 def transposed_source(+dims: List<&2, U32>, +index: U32) -> Maybe<&2, U32>: 180 Layout.reference_source_coordinates(dims, 181 Axis.scatter(U32, Shape.rank_dimensions(dims), Shape.naturals([1, 0]), 182 Shape.words(Shape.digits(Shape.naturals(Axis.order(U32, dims, Shape.naturals([1, 0]))), U32.to_nat(index))), 0n)) 183 184 # Source of output digits (j, l) of a [columns, rows] transpose: the input 185 # offset l * columns + j, once both digits are words again. 186 def swapped_offset(+rows: U32, +columns: U32, +j: Nat, +l: Nat, 187 +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, 188 +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}) -> 189 {Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(l)), Nat.mul(U32.to_nat(columns), 1n)), 190 Nat.add(Nat.mul(U32.to_nat(U32.from_nat(j)), 1n), 0n)))} == 191 Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}: 192 +c = U32.to_nat(columns) 193 %Equal.sym(Nat, U32.to_nat(U32.from_nat(l)), l, MatrixIndex.word_below(l, rows, l_below)) : 194 {Some{U32.from_nat(Nat.add(Nat.mul(_, Nat.mul(c, 1n)), Nat.add(Nat.mul(U32.to_nat(U32.from_nat(j)), 1n), 0n)))} == 195 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 196 %Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, MatrixIndex.word_below(j, columns, j_below)) : 197 {Some{U32.from_nat(Nat.add(Nat.mul(l, Nat.mul(c, 1n)), Nat.add(Nat.mul(_, 1n), 0n)))} == 198 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 199 %Equal.sym(Nat, Nat.mul(c, 1n), c, Nats.mul_one_right(c)) : 200 {Some{U32.from_nat(Nat.add(Nat.mul(l, _), Nat.add(Nat.mul(j, 1n), 0n)))} == 201 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 202 %Equal.sym(Nat, Nat.mul(j, 1n), j, Nats.mul_one_right(j)) : 203 {Some{U32.from_nat(Nat.add(Nat.mul(l, c), Nat.add(_, 0n)))} == 204 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 205 %Equal.sym(Nat, Nat.add(j, 0n), j, Conversion.add_zero(j)) : 206 {Some{U32.from_nat(Nat.add(Nat.mul(l, c), _))} == 207 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 208 {==} 209 210 def matrix_source(+rows: U32, +columns: U32, +j: Nat, +l: Nat, 211 +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, 212 +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}, 213 +exact: {U32.to_nat(U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) == Nat.add(Nat.mul(j, U32.to_nat(rows)), l) : Nat}) -> 214 {transposed_source([rows, columns], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) == 215 Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}: 216 +r = U32.to_nat(rows) 217 +c = U32.to_nat(columns) 218 +i = Nat.add(Nat.mul(j, r), l) 219 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, exact) : 220 {Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(Matrix.column_of(r, _))), Nat.mul(c, 1n)), 221 Nat.add(Nat.mul(U32.to_nat(U32.from_nat(Matrix.row_of(r, U32.to_nat(U32.from_nat(i))))), 1n), 0n)))} == 222 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 223 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, exact) : 224 {Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(Matrix.column_of(r, i))), Nat.mul(c, 1n)), 225 Nat.add(Nat.mul(U32.to_nat(U32.from_nat(Matrix.row_of(r, _))), 1n), 0n)))} == 226 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 227 %Equal.sym(Nat, Matrix.column_of(r, i), l, MatrixIndex.column_at(j, l, r, l_below)) : 228 {Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(_)), Nat.mul(c, 1n)), 229 Nat.add(Nat.mul(U32.to_nat(U32.from_nat(Matrix.row_of(r, i))), 1n), 0n)))} == 230 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 231 %Equal.sym(Nat, Matrix.row_of(r, i), j, MatrixIndex.row_at(j, l, r, l_below)) : 232 {Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(l)), Nat.mul(c, 1n)), 233 Nat.add(Nat.mul(U32.to_nat(U32.from_nat(_)), 1n), 0n)))} == 234 Some{U32.from_nat(Nat.add(Nat.mul(l, c), j))} : Maybe<&2, U32>} 235 swapped_offset(rows, columns, j, l, j_below, l_below) 236 237 # j * rows + l < rows * columns, so the output index is its own word. 238 def transposed_index_exact(+input: Shape.Shape, +rows: U32, +columns: U32, 239 +matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}, +j: Nat, 240 +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, +l: Nat, 241 +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}) -> 242 {U32.to_nat(U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) == Nat.add(Nat.mul(j, U32.to_nat(rows)), l) : Nat}: 243 +r = U32.to_nat(rows) 244 +c = U32.to_nat(columns) 245 MatrixIndex.word_exact(Nat.add(Nat.mul(j, r), l), input, 246 %Equal.sym(List<&2, U32>, Shape.dimensions(input), [rows, columns], matrix) : 247 {Nat.is_lt(Nat.add(Nat.mul(j, r), l), Shape.logical_numel(_)) == True{} : Bool} 248 %Equal.sym(Nat, Nat.mul(c, 1n), c, Nats.mul_one_right(c)) : 249 {Nat.is_lt(Nat.add(Nat.mul(j, r), l), Nat.mul(r, _)) == True{} : Bool} 250 %Nats.mul_comm(c, r) : 251 {Nat.is_lt(Nat.add(Nat.mul(j, r), l), _) == True{} : Bool} 252 MatrixIndex.lt_mul_add(j, c, l, r, j_below, l_below)) 253 254 def permute_source_transposed(+input: Shape.Shape, +rows: U32, +columns: U32, 255 +matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}, +j: Nat, 256 +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, +l: Nat, 257 +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}) -> 258 {Values.permute_source(input, [1, 0], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) == 259 Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}: 260 +index = U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l)) 261 %Equal.sym(List<&2, U32>, Shape.dimensions(input), [rows, columns], matrix) : 262 {transposed_source(_, index) == Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>} 263 matrix_source(rows, columns, j, l, j_below, l_below, transposed_index_exact(input, rows, columns, matrix, j, j_below, l, l_below)) 264 265 def Laws.permute_source_transposed(input, rows, columns, matrix, j, j_below, l, l_below): 266 permute_source_transposed(input, rows, columns, matrix, j, j_below, l, l_below)