src/tensor/transpose_PROOF.bend
bendtorch-core@0.1.0.0 · 266 lines · 16 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
4import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
5import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as Algebra
6import bendtorch-core@0.1.0.0/src/tensor/axis_PROOF.bend as AxisProof
7import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
8import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
9import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
10import bendtorch-core@0.1.0.0/src/tensor/transpose_LAWS.bend as Laws
11import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
12import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
13import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
14import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
15
16def 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
21def 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
26type 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
31def 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<dims, a, b>:
33 match dims a b:
34 case Nil{} 0n 0n:
35 Certified{{==}, {==}, {==}}
36 case Nil{} 1n+p b:
37 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))))
38 case Nil{} a 1n+p:
39 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))))
40 case +d0 <> Nil{} 0n 0n:
41 Certified{{==}, {==}, {==}}
42 case +d0 <> Nil{} 1n+p b:
43 Empty.absurd(AxesFacts<d0 <> 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<d0 <> 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<d0 <> 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<d0 <> 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<d0 <> 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<d0 <> 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<d0 <> 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<d0 <> 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
119def requested(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts<dims, a, b>) ->
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
124def requested_valid(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts<dims, a, b>) ->
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
129def requested_inverse(-dims: List<&2, U32>, -a: Nat, -b: Nat, certificate: AxesFacts<dims, a, b>) ->
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
134def 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
141def 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
153def 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
161def 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
168def Laws.transpose_axes_requested(shape, a, b, inside):
169 transpose_axes_requested(shape, a, b, inside)
170
171def Laws.transpose_axes_valid(shape, a, b, inside):
172 valid_axes(shape, a, b, inside)
173
174def Laws.transpose_axes_self_inverse(shape, a, b, inside):
175 inverse_axes(shape, a, b, inside)
176
177
178
179def 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
185
186def 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
210def 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
238def 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
254def 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
265def 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)