src/tensor/matmul_PROOF.bend
bendtorch-core@0.1.0.0 · 1,682 lines · 101 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
5import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
6import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
7import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws
8import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
9import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
10import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as MathProof
11import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
12import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
13import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
14import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
15import bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend as TransformLaws
16import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
17import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
18import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
19import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as Boundary
20import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
21import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
22import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
23import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
24import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
25import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
26import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
27import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
28import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
29import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as ElementwiseTotality
30import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
31import bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend as MatmulParallel
32import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
33
34type CoordinateRead<-shape: Shape.Shape, -original: Core.Tensor<shape>, -coordinates: List<&2, U32>> is Type:
35 CoordinateRead{tensor: Core.Tensor<shape>, result: Result<&2, &2, Core.Error, F32>,
36 exact: {(tensor, result) == Core.read_coordinate(shape, original, coordinates) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
37 -meaning: @unit: Unit -> {Core.result_value(result) == Laws.coordinate_observe(shape, original, coordinates) : Maybe<&2, F32>},
38 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}
39
40def coordinate_flat(+shape: Shape.Shape, -original: Core.Tensor<shape>, -coordinates: List<&2, U32>, +index: Shape.FlatIndex<shape>,
41 same: {Done{index} == Shape.flatten_checked(shape, coordinates) : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>},
42 certificate: Core.Read<shape, original, Shape.index_value(shape, index)>,
43 -source: Core.SourceRead<shape, original, Shape.index_value(shape, index)>,
44 -retention: Core.SourceReadKeeps<shape, original, Shape.index_value(shape, index)>) -> CoordinateRead<shape, original, coordinates>:
45 Core.Read{tensor, +result, +exact} = certificate
46 CoordinateRead{tensor, result,
47 %same : {(tensor, result) == Core.read_coordinate_result(shape, original, _) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>}
48 exact,
49 unit =>
50 prove : @source: Core.SourceRead<shape, original, Shape.index_value(shape, index)> ->
51 {Core.result_value(result) == Laws.coordinate_observe(shape, original, coordinates) : Maybe<&2, F32>} =
52 \{Core.SourceRead: meaning =>
53 %same : {Core.result_value(result) == Laws.coordinate_observe_result(shape, original, _) : Maybe<&2, F32>}
54 Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.read_value(shape, Core.read_flat(shape, original, Shape.index_value(shape, index))),
55 Core.checked_observe(shape, original, Shape.index_value(shape, index)),
56 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
57 (tensor, result), Core.read_flat(shape, original, Shape.index_value(shape, index)), exact), meaning)}
58 prove(source),
59 other =>
60 prove : @retention: Core.SourceReadKeeps<shape, original, Shape.index_value(shape, index)> ->
61 {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>} =
62 \{Core.SourceReadKeeps: kept => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other),
63 Core.retained_read_observe(shape, Core.read_flat(shape, original, Shape.index_value(shape, index)), other), Core.checked_observe(shape, original, other),
64 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
65 (tensor, result), Core.read_flat(shape, original, Shape.index_value(shape, index)), exact), kept(other))}
66 prove(retention)}
67
68def coordinate_decided(+shape: Shape.Shape, tensor: Core.Tensor<shape>, -coordinates: List<&2, U32>,
69 result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
70 same: {result == Shape.flatten_checked(shape, coordinates) : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}) -> CoordinateRead<shape, tensor, coordinates>:
71 match result:
72 case Fail{error}:
73 CoordinateRead{tensor, Fail{Core.ShapeError{error}},
74 %same : {(tensor, Fail{Core.ShapeError{error}}) == Core.read_coordinate_result(shape, tensor, _) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>}
75 {==},
76 unit => %same : {None{} == Laws.coordinate_observe_result(shape, tensor, _) : Maybe<&2, F32>}
77 {==}, other => {==}}
78 case Done{+index}:
79 coordinate_flat(shape, tensor, coordinates, index, same, Core.read_certificate(shape, tensor, Shape.index_value(shape, index)),
80 Core.source_read_model(shape, tensor, Shape.index_value(shape, index)), Core.source_read_keeps(shape, tensor, Shape.index_value(shape, index)))
81
82def coordinate_certificate(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +coordinates: List<&2, U32>) -> CoordinateRead<shape, tensor, coordinates>:
83 coordinate_decided(shape, tensor, coordinates, Shape.flatten_checked(shape, coordinates), {==})
84
85def coordinate_keeps_result(+shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>,
86 result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
87 kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
88 {Laws.coordinate_observe_result(shape, tensor, result) == Laws.coordinate_observe_result(shape, original, result) : Maybe<&2, F32>}:
89 match result:
90 case Fail{error}:
91 {==}
92 case Done{index}:
93 kept(Shape.index_value(shape, index))
94
95def coordinate_keeps(+shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +coordinates: List<&2, U32>,
96 kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
97 {Laws.coordinate_observe(shape, tensor, coordinates) == Laws.coordinate_observe(shape, original, coordinates) : Maybe<&2, F32>}:
98 coordinate_keeps_result(shape, original, tensor, Shape.flatten_checked(shape, coordinates), kept)
99
100def logical_dot_original(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
101 -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, +row: U32, +column: U32, +cursor: Nat, values: List<&2, DotFold.Factors>,
102 logical: Laws.LogicalDot(fuel, left, right, ra, rb, row, column, cursor, values),
103 -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
104 -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}) ->
105 Laws.LogicalDot(fuel, left, right, a, b, row, column, cursor, values):
106 match fuel values:
107 case 0n Nil{}:
108 Unit{}
109 case 1n+tail DotFold.Factors{+lv, +rv} <> rest:
110 Laws.DotStep{exact, lo, ro, remaining} = logical
111 Laws.DotStep{exact,
112 Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]),
113 Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]), Some{lv},
114 Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]),
115 Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]), coordinate_keeps(left, a, ra, [row, U32.from_nat(cursor)], left_kept)), lo),
116 Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]),
117 Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]), Some{rv},
118 Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]),
119 Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]), coordinate_keeps(right, b, rb, [U32.from_nat(cursor), column], right_kept)), ro),
120 logical_dot_original(tail, left, right, a, b, ra, rb, row, column, 1n+cursor, rest, remaining, left_kept, right_kept)}
121 case 0n DotFold.Factors{lv, rv} <> rest:
122 Empty.absurd(Laws.LogicalDot(0n, left, right, a, b, row, column, cursor, DotFold.Factors{lv, rv} <> rest), logical)
123 case 1n+tail Nil{}:
124 Empty.absurd(Laws.LogicalDot(1n+tail, left, right, a, b, row, column, cursor, Nil{}), logical)
125
126def dot_extend(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
127 -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32, +rv: F32,
128 result: Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32>,
129 next: Laws.DotResultMeaning(fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv)), result),
130 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
131 -lo: {Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]) == Some{lv} : Maybe<&2, F32>},
132 -ro: {Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]) == Some{rv} : Maybe<&2, F32>},
133 -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
134 -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}) ->
135 Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, result):
136 match result:
137 case Fail{error}:
138 Unit{}
139 case Done{pair}:
140 (final_a, final_b, value) = pair
141 Laws.DotMeaning{values, logical, fold, lk, rk} = next
142 Laws.DotMeaning{DotFold.Factors{lv, rv} <> values,
143 Laws.DotStep{exact, lo, ro, logical_dot_original(fuel, left, right, a, b, ra, rb, row, column, 1n+cursor, values, logical, left_kept, right_kept)}, fold,
144 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(left, final_a, other),
145 Core.checked_observe(left, ra, other), Core.checked_observe(left, a, other), lk(other), left_kept(other)),
146 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(right, final_b, other),
147 Core.checked_observe(right, rb, other), Core.checked_observe(right, b, other), rk(other), right_kept(other))}
148
149def right_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
150 -ra: Core.Tensor<left>, rb: Core.Tensor<right>, result: Result<&2, &2, Core.Error, F32>,
151 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32,
152 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
153 Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
154 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
155 -lo: {Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]) == Some{lv} : Maybe<&2, F32>},
156 -meaning: @unit: Unit -> {Core.result_value(result) == Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]) : Maybe<&2, F32>},
157 -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
158 -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}) ->
159 Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.right_read(left, right,
160 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), ra, lv, accumulator, (rb, result))>:
161 match result:
162 case Fail{error}:
163 Laws.SourceDot{unit => Unit{}}
164 case Done{+rv}:
165 Laws.SourceDot{unit =>
166 claim : @certificate: Laws.SourceDot<fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv)),
167 Matrix.natural_dot(fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv)))> ->
168 Laws.DotResultMeaning(fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv)),
169 Matrix.natural_dot(fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv)))) =
170 \{Laws.SourceDot: proof => proof(Unit{})}
171 dot_extend(fuel, left, right, a, b, ra, rb, row, column, cursor, accumulator, lv, rv,
172 Matrix.natural_dot(fuel, left, right, ra, rb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(lv, rv))),
173 claim(rec(ra, rb, F32.add(accumulator, F32.mul(lv, rv)))), exact, lo,
174 Equal.sym(Maybe<&2, F32>, Some{rv}, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]), meaning(Unit{})), left_kept, right_kept)}
175
176def right_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, -ra: Core.Tensor<left>,
177 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32,
178 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
179 Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
180 -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
181 -lo: {Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]) == Some{lv} : Maybe<&2, F32>},
182 -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
183 certificate: CoordinateRead<right, b, [U32.from_nat(cursor), column]>) ->
184 Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.right_read(left, right,
185 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), ra, lv, accumulator,
186 Core.read_coordinate(right, b, [U32.from_nat(cursor), column]))>:
187 CoordinateRead{rb, +result, +exact, meaning, right_kept} = certificate
188 Laws.SourceDot{unit =>
189 claim : @certificate: Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.right_read(left, right,
190 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), ra, lv, accumulator, (rb, result))> ->
191 Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.right_read(left, right,
192 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), ra, lv, accumulator, (rb, result))) =
193 \{Laws.SourceDot: proof => proof(Unit{})}
194 %exact : Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.right_read(left, right,
195 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), ra, lv, accumulator, _))
196 claim(right_pair(fuel, left, right, a, b, ra, rb, result, row, column, cursor, accumulator, lv, rec, exact_cursor, lo, meaning, left_kept, right_kept))}
197
198def left_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, b: Core.Tensor<right>,
199 ra: Core.Tensor<left>, result: Result<&2, &2, Core.Error, F32>,
200 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
201 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
202 Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
203 -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
204 -meaning: @unit: Unit -> {Core.result_value(result) == Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]) : Maybe<&2, F32>},
205 -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>}) ->
206 Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
207 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, (ra, result))>:
208 match result:
209 case Fail{error}:
210 Laws.SourceDot{unit => Unit{}}
211 case Done{+lv}:
212 right_certificate(fuel, left, right, a, b, ra, row, column, cursor, accumulator, lv, rec, exact_cursor,
213 Equal.sym(Maybe<&2, F32>, Some{lv}, Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]), meaning(Unit{})), left_kept,
214 coordinate_certificate(right, b, [U32.from_nat(cursor), column]))
215
216def left_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
217 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
218 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
219 Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
220 -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
221 certificate: CoordinateRead<left, a, [row, U32.from_nat(cursor)]>) ->
222 Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
223 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator,
224 Core.read_coordinate(left, a, [row, U32.from_nat(cursor)]))>:
225 CoordinateRead{ra, +result, +exact, meaning, left_kept} = certificate
226 Laws.SourceDot{unit =>
227 claim : @certificate: Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
228 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, (ra, result))> ->
229 Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
230 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, (ra, result))) =
231 \{Laws.SourceDot: proof => proof(Unit{})}
232 %exact : Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
233 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, _))
234 claim(left_pair(fuel, left, right, a, b, ra, result, row, column, cursor, accumulator, rec, exact_cursor, meaning, left_kept))}
235
236def dot_decision(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, a: Core.Tensor<left>, -b: Core.Tensor<right>,
237 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
238 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
239 Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
240 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
241 Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.dot_decided(left, right,
242 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), a, b, row, column, cursor, U32.from_nat(cursor), accumulator, decision)>:
243 match decision:
244 case Shape.BFalse{equal}:
245 Laws.SourceDot{unit => Unit{}}
246 case Shape.BTrue{equal}:
247 left_certificate(fuel, left, right, a, b, row, column, cursor, accumulator, rec,
248 Lifecycle.natural_equal(U32.to_nat(U32.from_nat(cursor)), cursor, equal), coordinate_certificate(left, a, [row, U32.from_nat(cursor)]))
249
250def Laws.successful_dot_interpretation(fuel, left, right, a, b, row, column, cursor, accumulator):
251 match fuel:
252 case 0n:
253 Laws.SourceDot{unit => Laws.DotMeaning{Nil{}, Unit{}, {==}, other => {==}, other => {==}}}
254 case 1n+tail:
255 dot_decision(tail, left, right, a, b, row, column, cursor, accumulator,
256 a => b => value => Laws.successful_dot_interpretation(tail, left, right, a, b, row, column, 1n+cursor, value),
257 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))
258
259def lt_zero_false(+value: Nat) -> {Nat.is_lt(value, 0n) == False{} : Bool}:
260 match value:
261 case 0n:
262 {==}
263 case 1n+tail:
264 {==}
265
266def no_earlier_zero(+value: Nat, earlier: {Nat.is_lt(value, 0n) == True{} : Bool}) -> Empty:
267 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_lt(value, 0n), False{},
268 Equal.sym(Bool, Nat.is_lt(value, 0n), True{}, earlier), lt_zero_false(value)))
269
270def earlier_lift(-a: Nat, -b: Nat, split: Either<&2, &2, {Nat.is_lt(a, b) == True{} : Bool}, {a == b : Nat}>) ->
271 Either<&2, &2, {Nat.is_lt(1n+a, 1n+b) == True{} : Bool}, {1n+a == 1n+b : Nat}>:
272 match split:
273 case Inl{earlier}:
274 Inl{earlier}
275 case Inr{equal}:
276 Inr{Equal.cong(Nat, Nat, n => 1n+n, a, b, equal)}
277
278def earlier_split(+a: Nat, +b: Nat, earlier: {Nat.is_lt(a, 1n+b) == True{} : Bool}) ->
279 Either<&2, &2, {Nat.is_lt(a, b) == True{} : Bool}, {a == b : Nat}>:
280 match a b:
281 case 0n 0n:
282 Inr{{==}}
283 case 0n 1n+q:
284 Inl{{==}}
285 case 1n+p 0n:
286 Empty.absurd(Either<&2, &2, {Nat.is_lt(1n+p, 0n) == True{} : Bool}, {1n+p == 0n : Nat}>, no_earlier_zero(p, earlier))
287 case 1n+p 1n+q:
288 earlier_lift(p, q, earlier_split(p, q, earlier))
289
290def earlier_different(+a: Nat, +b: Nat, earlier: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_eq(b, a) == False{} : Bool}:
291 match a b:
292 case 0n 0n:
293 Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, no_earlier_zero(0n, earlier))
294 case 0n 1n+q:
295 {==}
296 case 1n+p 0n:
297 Empty.absurd({Nat.is_eq(0n, 1n+p) == False{} : Bool}, no_earlier_zero(1n+p, earlier))
298 case 1n+p 1n+q:
299 earlier_different(p, q, earlier)
300
301def checked_different(+position: Nat, +cursor: Nat,
302 position_exact: {U32.to_nat(U32.from_nat(position)) == position : Nat}, cursor_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
303 earlier: {Nat.is_lt(position, cursor) == True{} : Bool}) ->
304 {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(U32.from_nat(position))) == False{} : Bool}:
305 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact) : {Nat.is_eq(_, U32.to_nat(U32.from_nat(position))) == False{} : Bool}
306 %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, position_exact) : {Nat.is_eq(cursor, _) == False{} : Bool}
307 earlier_different(position, cursor, earlier)
308
309def frame_cell(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
310 +output: Shape.Shape, -before: Core.Tensor<output>, -after: Core.Tensor<output>, +cursor: Nat, +position: Nat,
311 cell: Laws.ProductCell<inner, left, right, a, b, output, before, position>,
312 -cursor_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, -earlier: {Nat.is_lt(position, cursor) == True{} : Bool},
313 -frame: @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{output, before}, other) ->
314 @different: {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(other)) == False{} : Bool} ->
315 Core.ObservationChecked(Core.Packed{output, after}, other) &
316 {Core.checked_observe(output, after, other) == Core.checked_observe(output, before, other) : Maybe<&2, F32>}) ->
317 Laws.ProductCell<inner, left, right, a, b, output, after, position>:
318 Laws.ProductCell{row, column, coordinate, decoded, coordinates, word_exact, factors, logical, value, fold, checked, observed} = cell
319 Laws.ProductCell{row, column, coordinate, decoded, coordinates, word_exact, factors, logical, value, fold,
320 Pair.fst(Core.ObservationChecked(Core.Packed{output, after}, U32.from_nat(position)),
321 {Core.checked_observe(output, after, U32.from_nat(position)) == Core.checked_observe(output, before, U32.from_nat(position)) : Maybe<&2, F32>},
322 frame(U32.from_nat(position), checked, checked_different(position, cursor, word_exact, cursor_exact, earlier))),
323 Equal.trans(Maybe<&2, F32>, Core.checked_observe(output, after, U32.from_nat(position)),
324 Core.checked_observe(output, before, U32.from_nat(position)), Some{value},
325 Pair.snd(Core.ObservationChecked(Core.Packed{output, after}, U32.from_nat(position)),
326 {Core.checked_observe(output, after, U32.from_nat(position)) == Core.checked_observe(output, before, U32.from_nat(position)) : Maybe<&2, F32>},
327 frame(U32.from_nat(position), checked, checked_different(position, cursor, word_exact, cursor_exact, earlier))), observed)}
328
329def prefix_cell_case(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
330 +output: Shape.Shape, -out: Core.Tensor<output>, +cursor: Nat, +position: Nat,
331 current: Laws.ProductCell<inner, left, right, a, b, output, out, cursor>,
332 prior: @+position: Nat -> @earlier: {Nat.is_lt(position, cursor) == True{} : Bool} -> Laws.ProductCell<inner, left, right, a, b, output, out, position>,
333 split: Either<&2, &2, {Nat.is_lt(position, cursor) == True{} : Bool}, {position == cursor : Nat}>) -> Laws.ProductCell<inner, left, right, a, b, output, out, position>:
334 match split:
335 case Inl{earlier}:
336 prior(position, earlier)
337 case Inr{equal}:
338 %Equal.sym(Nat, position, cursor, equal) : Laws.ProductCell<inner, left, right, a, b, output, out, _>
339 current
340
341def advance_prefix(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
342 -before_a: Core.Tensor<left>, -before_b: Core.Tensor<right>, -after_a: Core.Tensor<left>, -after_b: Core.Tensor<right>,
343 +output: Shape.Shape, -before: Core.Tensor<output>, -after: Core.Tensor<output>, +cursor: Nat,
344 +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate<output>, +value: F32,
345 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
346 -coordinates: {Shape.coordinate_values(output, coordinate) == [row, column] : List<&2, U32>},
347 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
348 prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, before, cursor>,
349 dot: Laws.DotMeaning<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0, after_a, after_b, value>,
350 update: Core.CheckedUpdateMeaning(output, before, U32.from_nat(cursor), value, (after, Done{Unit{}}))) ->
351 Laws.ProductPrefix<inner, left, right, a, b, output, after_a, after_b, after, 1n+cursor>:
352 Laws.ProductPrefix{left_prior, right_prior, cells} = prefix
353 Laws.DotMeaning{factors, logical, fold, left_kept, right_kept} = dot
354 (checked, pair) = update
355 (observed, frame) = pair
356 Laws.ProductPrefix{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(left, after_a, other),
357 Core.checked_observe(left, before_a, other), Core.checked_observe(left, a, other), left_kept(other), left_prior(other)),
358 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(right, after_b, other),
359 Core.checked_observe(right, before_b, other), Core.checked_observe(right, b, other), right_kept(other), right_prior(other)),
360 position => earlier => prefix_cell_case(inner, left, right, a, b, output, after, cursor, position,
361 Laws.ProductCell{row, column, coordinate, decoded, coordinates, word_exact, factors,
362 logical_dot_original(U32.to_nat(inner), left, right, a, b, before_a, before_b, row, column, 0n, factors, logical, left_prior, right_prior),
363 value, fold, checked, observed},
364 position => earlier => frame_cell(inner, left, right, a, b, output, before, after, cursor, position, cells(position, earlier), word_exact, earlier, frame),
365 earlier_split(position, cursor, earlier))}
366
367def add_successor(+fuel: Nat, +cursor: Nat) -> {Nat.add(fuel, 1n+cursor) == 1n+Nat.add(fuel, cursor) : Nat}:
368 match fuel:
369 case 0n:
370 {==}
371 case 1n+tail:
372 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), add_successor(tail, cursor))
373
374def add_zero(+value: Nat) -> {Nat.add(value, 0n) == value : Nat}:
375 match value:
376 case 0n:
377 {==}
378 case 1n+tail:
379 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(tail, 0n), tail, add_zero(tail))
380
381def write_product_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
382 -a: Core.Tensor<left>, -b: Core.Tensor<right>, -before_a: Core.Tensor<left>, -before_b: Core.Tensor<right>,
383 -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, -before: Core.Tensor<output>, out: Core.Tensor<output>, result: Result<&2, &2, Core.Error, Unit>,
384 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate<output>, +value: F32,
385 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
386 -coordinates: {Shape.coordinate_values(output, coordinate) == [row, column] : List<&2, U32>},
387 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
388 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, before, cursor>,
389 -dot: Laws.DotMeaning<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0, ra, rb, value>,
390 -update: Core.CheckedUpdateMeaning(output, before, U32.from_nat(cursor), value, (out, result)),
391 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
392 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
393 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
394 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>) ->
395 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
396 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb, (out, result))>:
397 match result:
398 case Fail{error}:
399 Laws.SourceProduct{unit => Unit{}}
400 case Done{Unit{}}:
401 Laws.SourceProduct{unit =>
402 claim : @certificate: Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
403 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)> ->
404 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
405 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)) =
406 \{Laws.SourceProduct: proof => proof(Unit{})}
407 %add_successor(fuel, cursor) : Laws.ProductMeaning(inner, left, right, a, b, output, _,
408 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor))
409 claim(rec(ra, rb, out, advance_prefix(inner, left, right, a, b, before_a, before_b, ra, rb, output, before, out, cursor,
410 row, column, coordinate, value, decoded, coordinates, word_exact, prefix, dot, update)))}
411
412def write_product_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
413 -a: Core.Tensor<left>, -b: Core.Tensor<right>, -before_a: Core.Tensor<left>, -before_b: Core.Tensor<right>,
414 -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, -before: Core.Tensor<output>,
415 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate<output>, +value: F32,
416 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
417 -coordinates: {Shape.coordinate_values(output, coordinate) == [row, column] : List<&2, U32>},
418 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
419 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, before, cursor>,
420 -dot: Laws.DotMeaning<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0, ra, rb, value>,
421 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
422 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
423 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
424 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>,
425 certificate: Core.Write<output, before, U32.from_nat(cursor), value>, -model: Core.CheckedUpdateModel<output, before, U32.from_nat(cursor), value>) ->
426 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
427 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
428 Core.write_flat(output, before, U32.from_nat(cursor), value))>:
429 Core.Write{out, +result, +exact} = certificate
430 Laws.SourceProduct{unit =>
431 claim : @certificate: Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
432 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb, (out, result))> ->
433 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
434 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb, (out, result))) =
435 \{Laws.SourceProduct: proof => proof(Unit{})}
436 prove : @model: Core.CheckedUpdateModel<output, before, U32.from_nat(cursor), value> ->
437 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
438 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
439 Core.write_flat(output, before, U32.from_nat(cursor), value))) =
440 \{Core.CheckedUpdateModel: meaning =>
441 %exact : Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
442 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb, _))
443 claim(write_product_pair(fuel, left, right, output, inner, columns, a, b, before_a, before_b, ra, rb, before, out, result,
444 cursor, row, column, coordinate, value, decoded, coordinates, word_exact, prefix, dot,
445 %Equal.sym(Core.Tensor<output> & Result<&2, &2, Core.Error, Unit>, (out, result), Core.write_flat(output, before, U32.from_nat(cursor), value), exact) :
446 Core.CheckedUpdateMeaning(output, before, U32.from_nat(cursor), value, _)
447 meaning, rec))}
448 prove(model)}
449
450def product_dot_result(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
451 -a: Core.Tensor<left>, -b: Core.Tensor<right>, -before_a: Core.Tensor<left>, -before_b: Core.Tensor<right>, -out: Core.Tensor<output>,
452 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate<output>,
453 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
454 -coordinates: {Shape.coordinate_values(output, coordinate) == [row, column] : List<&2, U32>},
455 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
456 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, out, cursor>,
457 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
458 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
459 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
460 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>,
461 result: Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32>,
462 -source: Laws.SourceDot<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0, result>) ->
463 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.dotted(left, right, output,
464 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), out, U32.from_nat(cursor), result)>:
465 match result:
466 case Fail{error}:
467 Laws.SourceProduct{unit => Unit{}}
468 case Done{pair}:
469 (ra, rb, value) = pair
470 Laws.SourceProduct{unit =>
471 claim : @certificate: Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
472 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
473 Core.write_flat(output, out, U32.from_nat(cursor), value))> ->
474 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
475 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
476 Core.write_flat(output, out, U32.from_nat(cursor), value))) = \{Laws.SourceProduct: proof => proof(Unit{})}
477 prove : @dot: Laws.DotMeaning<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0, ra, rb, value> ->
478 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
479 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
480 Core.write_flat(output, out, U32.from_nat(cursor), value))) = dot =>
481 claim(write_product_certificate(fuel, left, right, output, inner, columns, a, b, before_a, before_b, ra, rb, out,
482 cursor, row, column, coordinate, value, decoded, coordinates, word_exact, prefix, dot, rec,
483 Core.write_certificate(output, out, U32.from_nat(cursor), value), CoreProof.checked_update_model(output, out, U32.from_nat(cursor), value)))
484 from_source : @source: Laws.SourceDot<U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0,
485 (Done{(ra, rb, value)} : Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32>)> ->
486 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.wrote(left, right, output,
487 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), ra, rb,
488 Core.write_flat(output, out, U32.from_nat(cursor), value))) = \{Laws.SourceDot: meaning => prove(meaning(Unit{}))}
489 from_source(source)}
490
491def product_coordinates_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
492 -a: Core.Tensor<left>, -b: Core.Tensor<right>, before_a: Core.Tensor<left>, before_b: Core.Tensor<right>, -out: Core.Tensor<output>,
493 +cursor: Nat, +coordinate: Shape.CheckedCoordinate<output>,
494 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
495 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
496 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, out, cursor>,
497 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
498 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
499 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
500 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>,
501 values: List<&2, U32>, -same: {values == Shape.coordinate_values(output, coordinate) : List<&2, U32>}) ->
502 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.product_coordinates(left, right, output,
503 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), inner, before_a, before_b, out, U32.from_nat(cursor), values)>:
504 match values:
505 case +row <> +column <> Nil{}:
506 product_dot_result(fuel, left, right, output, inner, columns, a, b, before_a, before_b, out, cursor, row, column, coordinate,
507 decoded, Equal.sym(List<&2, U32>, [row, column], Shape.coordinate_values(output, coordinate), same), word_exact, prefix, rec,
508 Matrix.natural_dot(U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0),
509 Laws.successful_dot_interpretation(U32.to_nat(inner), left, right, before_a, before_b, row, column, 0n, 0.0))
510 case Nil{}:
511 Laws.SourceProduct{unit => Unit{}}
512 case row <> Nil{}:
513 Laws.SourceProduct{unit => Unit{}}
514 case row <> column <> third <> rest:
515 Laws.SourceProduct{unit => Unit{}}
516
517def product_unflattened_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
518 -a: Core.Tensor<left>, -b: Core.Tensor<right>, before_a: Core.Tensor<left>, before_b: Core.Tensor<right>, -out: Core.Tensor<output>, +cursor: Nat,
519 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
520 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, out, cursor>,
521 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
522 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
523 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
524 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>,
525 result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>,
526 -same: {result == Shape.unflatten_checked(output, U32.from_nat(cursor)) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>}) ->
527 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.product_unflattened(left, right, output,
528 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor), inner, before_a, before_b, out, U32.from_nat(cursor), result)>:
529 match result:
530 case Fail{error}:
531 Laws.SourceProduct{unit => Unit{}}
532 case Done{+coordinate}:
533 product_coordinates_proof(fuel, left, right, output, inner, columns, a, b, before_a, before_b, out, cursor, coordinate,
534 Equal.sym(Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>, Done{coordinate}, Shape.unflatten_checked(output, U32.from_nat(cursor)), same),
535 word_exact, prefix, rec, Shape.coordinate_values(output, coordinate), {==})
536
537def product_decision_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
538 -a: Core.Tensor<left>, -b: Core.Tensor<right>, before_a: Core.Tensor<left>, before_b: Core.Tensor<right>, -out: Core.Tensor<output>, +cursor: Nat,
539 -prefix: Laws.ProductPrefix<inner, left, right, a, b, output, before_a, before_b, out, cursor>,
540 -rec: @ra: Core.Tensor<left> -> @rb: Core.Tensor<right> -> @out: Core.Tensor<output> ->
541 @prefix: Laws.ProductPrefix<inner, left, right, a, b, output, ra, rb, out, 1n+cursor> ->
542 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(fuel, 1n+cursor),
543 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor)>,
544 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
545 Laws.SourceProduct<inner, left, right, a, b, output, Nat.add(1n+fuel, cursor), Matrix.product_decided(left, right, output,
546 ra => rb => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, ra, rb, out, 1n+cursor),
547 inner, columns, before_a, before_b, out, cursor, U32.from_nat(cursor), decision)>:
548 match decision:
549 case Shape.BFalse{equal}:
550 Laws.SourceProduct{unit => Unit{}}
551 case Shape.BTrue{equal}:
552 product_unflattened_proof(fuel, left, right, output, inner, columns, a, b, before_a, before_b, out, cursor,
553 Lifecycle.natural_equal(U32.to_nat(U32.from_nat(cursor)), cursor, equal), prefix, rec, Shape.unflatten_checked(output, U32.from_nat(cursor)), {==})
554
555def Laws.successful_product_interpretation(fuel, left, right, output, inner, columns, a, b, ra, rb, out, cursor, prefix):
556 match fuel:
557 case 0n:
558 Laws.SourceProduct{unit => prefix}
559 case 1n+tail:
560 product_decision_proof(tail, left, right, output, inner, columns, a, b, ra, rb, out, cursor, prefix,
561 ra => rb => out => prefix => Laws.successful_product_interpretation(tail, left, right, output, inner, columns, a, b, ra, rb, out, 1n+cursor, prefix),
562 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))
563
564def empty_prefix(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
565 +output: Shape.Shape, -out: Core.Tensor<output>) -> Laws.ProductPrefix<inner, left, right, a, b, output, a, b, out, 0n>:
566 Laws.ProductPrefix{other => {==}, other => {==}, position => earlier =>
567 Empty.absurd(Laws.ProductCell<inner, left, right, a, b, output, out, position>, no_earlier_zero(position, earlier))}
568
569def created_product(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32,
570 a: Core.Tensor<left>, b: Core.Tensor<right>, result: Result<&2, &1, Core.Error, Core.Tensor<output>>) ->
571 Laws.SourceProduct<inner, left, right, a, b, output, Shape.logical_numel(Shape.dimensions(output)), Matrix.created(left, right, output, inner, columns, a, b, result)>:
572 match result:
573 case Fail{error}:
574 Laws.SourceProduct{unit => Unit{}}
575 case Done{out}:
576 Laws.SourceProduct{unit =>
577 claim : @certificate: Laws.SourceProduct<inner, left, right, a, b, output,
578 Nat.add(Shape.logical_numel(Shape.dimensions(output)), 0n),
579 Matrix.natural_product_loop(Shape.logical_numel(Shape.dimensions(output)), left, right, output, inner, columns, a, b, out, 0n)> ->
580 Laws.ProductMeaning(inner, left, right, a, b, output, Nat.add(Shape.logical_numel(Shape.dimensions(output)), 0n),
581 Matrix.natural_product_loop(Shape.logical_numel(Shape.dimensions(output)), left, right, output, inner, columns, a, b, out, 0n)) =
582 \{Laws.SourceProduct: meaning => meaning(Unit{})}
583 %Equal.sym(Nat, Shape.elements(output), Shape.logical_numel(Shape.dimensions(output)), Shape.elements_exact(output)) :
584 Laws.ProductMeaning(inner, left, right, a, b, output, Shape.logical_numel(Shape.dimensions(output)),
585 Matrix.natural_product_loop(_, left, right, output, inner, columns, a, b, out, 0n))
586 %add_zero(Shape.logical_numel(Shape.dimensions(output))) : Laws.ProductMeaning(inner, left, right, a, b, output, _,
587 Matrix.natural_product_loop(Shape.logical_numel(Shape.dimensions(output)), left, right, output, inner, columns, a, b, out, 0n))
588 claim(Laws.successful_product_interpretation(Shape.logical_numel(Shape.dimensions(output)), left, right, output, inner, columns, a, b,
589 a, b, out, 0n, empty_prefix(inner, left, right, a, b, output, out)))}
590
591def Laws.successful_multiply_interpretation(left, right, plan, a, b):
592 match plan:
593 case Matrix.Plan{+output, rows, +inner, right_inner, +columns, le, re, oe, compatible}:
594 created_product(left, right, output, inner, columns, a, b, Core.new(output, 0.0))
595
596def zero_fold(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +row: U32, +column: U32,
597 values: List<&2, DotFold.Factors>, logical: Laws.LogicalDot(0n, left, right, a, b, row, column, 0n, values)) -> {DotFold.dot_fold(values, 0.0) == 0.0 : F32}:
598 match values:
599 case Nil{}:
600 {==}
601 case DotFold.Factors{lv, rv} <> rest:
602 Empty.absurd({DotFold.dot_fold(DotFold.Factors{lv, rv} <> rest, 0.0) == 0.0 : F32}, logical)
603
604type ZeroCell<-output: Shape.Shape, -out: Core.Tensor<output>, -position: Nat> is Data:
605 ZeroCell{-observed: {Core.checked_observe(output, out, U32.from_nat(position)) == Some{0.0} : Maybe<&2, F32>}}
606
607def zero_cell(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +output: Shape.Shape,
608 -out: Core.Tensor<output>, +position: Nat, cell: Laws.ProductCell<0, left, right, a, b, output, out, position>) -> ZeroCell<output, out, position>:
609 Laws.ProductCell{row, column, coordinate, decoded, coordinates, word_exact, factors, logical, value, fold, checked, observed} = cell
610 ZeroCell{Equal.trans(Maybe<&2, F32>, Core.checked_observe(output, out, U32.from_nat(position)), Some{value}, Some{0.0}, observed,
611 Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, 0.0,
612 Equal.trans(F32, value, DotFold.dot_fold(factors, 0.0), 0.0, fold, zero_fold(left, right, a, b, row, column, factors, logical))))}
613
614def zero_prefix(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +output: Shape.Shape,
615 -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, -out: Core.Tensor<output>, +end: Nat,
616 prefix: Laws.ProductPrefix<0, left, right, a, b, output, ra, rb, out, end>) -> Laws.ZeroPrefix<left, right, output, out, end>:
617 Laws.ProductPrefix{left_kept, right_kept, cells} = prefix
618 Laws.ZeroPrefix{position => earlier =>
619 claim : @certificate: ZeroCell<output, out, position> -> {Core.checked_observe(output, out, U32.from_nat(position)) == Some{0.0} : Maybe<&2, F32>} =
620 \{ZeroCell: observed => observed}
621 claim(zero_cell(left, right, a, b, output, out, position, cells(position, earlier)))}
622
623def zero_result(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +output: Shape.Shape, -end: Nat,
624 result: Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>>,
625 -source: Laws.SourceProduct<0, left, right, a, b, output, end, result>) -> Laws.ZeroResult<left, right, output, end, result>:
626 match result:
627 case Fail{error}:
628 Laws.ZeroResult{unit => Unit{}}
629 case Done{pair}:
630 (ra, rb, out) = pair
631 Laws.ZeroResult{unit =>
632 prove : @source: Laws.SourceProduct<0, left, right, a, b, output, end,
633 (Done{(ra, rb, out)} : Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>>)> ->
634 Laws.ZeroPrefix<left, right, output, out, end> = \{Laws.SourceProduct: meaning =>
635 zero_prefix(left, right, a, b, output, ra, rb, out, end, meaning(Unit{}))}
636 prove(source)}
637
638def Laws.zero_inner_multiply(left, right, output, rows, right_inner, columns, le, re, oe, compatible, a, b):
639 zero_result(left, right, a, b, output, Shape.logical_numel(Shape.dimensions(output)),
640 Matrix.multiply(left, right, Matrix.Plan{output, rows, 0, right_inner, columns, le, re, oe, compatible}, a, b),
641 Laws.successful_multiply_interpretation(left, right, Matrix.Plan{output, rows, 0, right_inner, columns, le, re, oe, compatible}, a, b))
642
643def Laws.zero_inner_dot(left, right, a, b, row, column):
644 {==}
645
646def Laws.output_dimensions(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible):
647 oe
648
649def word_cursor_exact(+fuel: Nat, +cursor: Nat, +limit: U32,
650 bound: Shape.LE(Nat.add(1n+fuel, cursor), U32.to_nat(limit))) -> {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
651 Conversion.natural_word_exact(cursor, limit,
652 Conversion.le_predecessor(cursor, U32.to_nat(limit),
653 Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, U32.to_nat(limit)),
654 Nats.le_true(1n+cursor, U32.to_nat(limit),
655 Nats.le_add_left(1n+cursor, fuel, U32.to_nat(limit),
656 %MathProof.add_comm(fuel, cursor) : Shape.LE(1n+_, U32.to_nat(limit))
657 bound)))))
658
659def inside_le(+index: Nat, +limit: Nat, inside: {Nat.is_lt(index, limit) == True{} : Bool}) -> {Nat.is_le(index, limit) == True{} : Bool}:
660 match index limit:
661 case 0n 0n:
662 Empty.absurd({True{} == True{} : Bool}, Arith.clash(inside))
663 case 0n 1n+q:
664 {==}
665 case 1n+p 0n:
666 Empty.absurd({False{} == True{} : Bool}, Arith.clash(inside))
667 case 1n+p 1n+q:
668 inside_le(p, q, inside)
669
670def index_inside(+shape: Shape.Shape, +position: Nat,
671 +bound: {True{} == Nat.is_lt(position, Shape.elements(shape)) : Bool}) ->
672 {Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
673 %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position,
674 Conversion.natural_word_exact(position, Shape.count(shape),
675 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape)) : {Nat.is_le(position, _) == True{} : Bool}
676 inside_le(position, Shape.elements(shape), Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(shape)), bound)))) :
677 {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
678 %Shape.elements_exact(shape) : {Nat.is_lt(position, _) == True{} : Bool}
679 Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(shape)), bound)
680
681def flatten_done(+shape: Shape.Shape, +coordinates: List<&2, U32>,
682 result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
683 +fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(coordinates)),
684 same: {result == Shape.flatten_checked(shape, coordinates) : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}) ->
685 {Result.is_done(&2, &2, Shape.Error, Shape.FlatIndex<shape>, result) == True{} : Bool}:
686 match result:
687 case Fail{error}:
688 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, value => Maybe.is_some(&2, U32, value), None{},
689 Some{U32.from_nat(Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(coordinates), fits)))},
690 Equal.trans(Maybe<&2, U32>, None{}, ShapeLaws.index_result(shape, Shape.flatten_checked(shape, coordinates)),
691 Some{U32.from_nat(Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(coordinates), fits)))},
692 Equal.cong(Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>, Maybe<&2, U32>, ShapeLaws.index_result(shape),
693 Fail{error}, Shape.flatten_checked(shape, coordinates), same),
694 %Boundary.decode_fit(Shape.extents(shape), Shape.naturals(coordinates), fits) :
695 {ShapeLaws.index_result(shape, Shape.flatten_checked(shape, coordinates)) == ShapeLaws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
696 ShapeLaws.flatten_checked_refines(shape, coordinates)))))
697 case Done{index}:
698 {==}
699
700def coordinate_read_result_status(+shape: Shape.Shape, result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
701 tensor: Core.Tensor<shape>, -successful: {Result.is_done(&2, &2, Shape.Error, Shape.FlatIndex<shape>, result) == True{} : Bool}) ->
702 Totality.ReadStatus<shape, Core.read_coordinate_result(shape, tensor, result)>:
703 match result:
704 case Fail{error}:
705 Totality.ReadStatus{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
706 case Done{index}:
707 Shape.FIndex{+position, +bound} = index
708 Totality.ReadStatus{{\{TransformTotality.ReadSuccess: successful => successful} :
709 TransformTotality.ReadSuccess<shape, tensor, U32.from_nat(position)> ->
710 {TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, U32.from_nat(position))) == True{} : Bool}}(
711 TransformLaws.tensor_read_valid_success(shape, tensor, U32.from_nat(position), index_inside(shape, position, bound)))}
712
713def coordinate_read_status(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +coordinates: List<&2, U32>,
714 -fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(coordinates))) ->
715 Totality.ReadStatus<shape, Core.read_coordinate(shape, tensor, coordinates)>:
716 coordinate_read_result_status(shape, Shape.flatten_checked(shape, coordinates), tensor,
717 flatten_done(shape, coordinates, Shape.flatten_checked(shape, coordinates), fits, {==}))
718
719def dot_right_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +row: U32, +column: U32, +cursor: Nat,
720 +left_value: F32, +accumulator: F32,
721 pair: Core.Tensor<right> & Result<&2, &2, Core.Error, F32>, a: Core.Tensor<left>,
722 -successful: {TransformTotality.read_succeeded(right, pair) == True{} : Bool},
723 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 -> Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32,
724 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) ->
725 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.right_read(left, right,
726 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), a, left_value, accumulator, pair)>:
727 (b, result) = pair
728 match result:
729 case Fail{error}:
730 Totality.Status{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
731 case Done{+value}:
732 Totality.Status{{\{Totality.Status: successful => successful} :
733 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32,
734 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, F32.add(accumulator, F32.mul(left_value, value)))> ->
735 {Result.is_done(&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32,
736 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, F32.add(accumulator, F32.mul(left_value, value)))) == True{} : Bool}}(
737 rec(a, b, F32.add(accumulator, F32.mul(left_value, value))))}
738
739def dot_left_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
740 pair: Core.Tensor<left> & Result<&2, &2, Core.Error, F32>, b: Core.Tensor<right>,
741 -successful: {TransformTotality.read_succeeded(left, pair) == True{} : Bool},
742 -right_fits: Coordinates.Fits(Shape.extents(right), [U32.to_nat(U32.from_nat(cursor)), U32.to_nat(column)]),
743 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 -> Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32,
744 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) ->
745 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.left_read(left, right,
746 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, pair)>:
747 (a, result) = pair
748 match result:
749 case Fail{error}:
750 Totality.Status{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
751 case Done{+value}:
752 dot_right_status(fuel, left, right, row, column, cursor, value, accumulator,
753 Core.read_coordinate(right, b, [U32.from_nat(cursor), column]), a,
754 {\{Totality.ReadStatus: successful => successful} : Totality.ReadStatus<right, Core.read_coordinate(right, b, [U32.from_nat(cursor), column])> ->
755 {TransformTotality.read_succeeded(right, Core.read_coordinate(right, b, [U32.from_nat(cursor), column])) == True{} : Bool}}(
756 coordinate_read_status(right, b, [U32.from_nat(cursor), column], right_fits)), rec)
757
758def dot_decision_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
759 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>, a: Core.Tensor<left>, b: Core.Tensor<right>,
760 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
761 -left_fits: Coordinates.Fits(Shape.extents(left), [U32.to_nat(row), U32.to_nat(U32.from_nat(cursor))]),
762 -right_fits: Coordinates.Fits(Shape.extents(right), [U32.to_nat(U32.from_nat(cursor)), U32.to_nat(column)]),
763 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 -> Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32,
764 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) ->
765 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.dot_decided(left, right,
766 a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), a, b, row, column, cursor, U32.from_nat(cursor), accumulator, decision)>:
767 match decision:
768 case Shape.BFalse{equal}:
769 Totality.Status{Empty.absurd({False{} == True{} : Bool}, MathProof.conversion_clash(U32.to_nat(U32.from_nat(cursor)), cursor, exact, equal))}
770 case Shape.BTrue{equal}:
771 dot_left_status(fuel, left, right, row, column, cursor, accumulator, Core.read_coordinate(left, a, [row, U32.from_nat(cursor)]), b,
772 {\{Totality.ReadStatus: successful => successful} : Totality.ReadStatus<left, Core.read_coordinate(left, a, [row, U32.from_nat(cursor)])> ->
773 {TransformTotality.read_succeeded(left, Core.read_coordinate(left, a, [row, U32.from_nat(cursor)])) == True{} : Bool}}(
774 coordinate_read_status(left, a, [row, U32.from_nat(cursor)], left_fits)), right_fits, rec)
775
776def dot_loop_status(fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
777 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, a: Core.Tensor<left>, b: Core.Tensor<right>,
778 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
779 -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
780 -row_inside: {Nat.is_lt(U32.to_nat(row), U32.to_nat(rows)) == True{} : Bool},
781 -column_inside: {Nat.is_lt(U32.to_nat(column), U32.to_nat(columns)) == True{} : Bool},
782 -bound: Shape.LE(Nat.add(fuel, cursor), U32.to_nat(inner))) ->
783 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.natural_dot(fuel, left, right, a, b, row, column, cursor, accumulator)>:
784 match fuel:
785 case 0n:
786 Totality.Status{{==}}
787 case 1n+tail:
788 dot_decision_status(tail, left, right, row, column, cursor, accumulator,
789 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), a, b, word_cursor_exact(tail, cursor, inner, bound),
790 Coordinates.pair_fits(left, rows, inner, row, U32.from_nat(cursor), le, row_inside,
791 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, word_cursor_exact(tail, cursor, inner, bound)) : {Nat.is_lt(_, U32.to_nat(inner)) == True{} : Bool}
792 MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound)),
793 Coordinates.pair_fits(right, right_inner, columns, U32.from_nat(cursor), column, re,
794 %compatible : {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) == True{} : Bool}
795 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, word_cursor_exact(tail, cursor, inner, bound)) : {Nat.is_lt(_, U32.to_nat(inner)) == True{} : Bool}
796 MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound), column_inside),
797 a => b => value => dot_loop_status(tail, left, right, rows, inner, right_inner, columns, row, column, 1n+cursor, value,
798 a, b, le, re, compatible, row_inside, column_inside,
799 %Equal.sym(Nat, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), Arith.add_succ(tail, cursor)) : Shape.LE(_, U32.to_nat(inner))
800 bound))
801
802def product_write_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, +cursor: Nat,
803 pair: Core.Tensor<output> & Result<&2, &2, Core.Error, Unit>, a: Core.Tensor<left>, b: Core.Tensor<right>,
804 -successful: {TransformTotality.write_succeeded(output, pair) == True{} : Bool},
805 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
806 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
807 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
808 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.wrote(left, right, output,
809 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), a, b, pair)>:
810 (out, result) = pair
811 match result:
812 case Fail{error}:
813 Totality.Status{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
814 case Done{unit}:
815 Totality.Status{{\{Totality.Status: successful => successful} :
816 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
817 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)> ->
818 {Result.is_done(&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
819 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)) == True{} : Bool}}(rec(a, b, out))}
820
821def product_dot_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, +cursor: Nat, +index: U32,
822 result: Result<&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32>, out: Core.Tensor<output>,
823 -status: Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, result>,
824 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool},
825 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
826 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
827 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
828 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.dotted(left, right, output,
829 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), out, index, result)>:
830 match result:
831 case Fail{error}:
832 Totality.Status{{\{Totality.Status: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
833 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Fail{error}> -> {False{} == True{} : Bool}}(status)}
834 case Done{pair}:
835 (a, b, value) = pair
836 product_write_status(fuel, left, right, output, inner, columns, cursor, Core.write_flat(output, out, index, value), a, b,
837 {\{TransformTotality.WriteSuccess: successful => successful} : TransformTotality.WriteSuccess<output, out, index, value> ->
838 {TransformTotality.write_succeeded(output, Core.write_flat(output, out, index, value)) == True{} : Bool}}(
839 TransformLaws.tensor_write_valid_success(output, out, index, value, inside)), rec)
840
841def coordinate_word_inside(+value: Nat, +extent: U32, +inside: {True{} == Nat.is_lt(value, U32.to_nat(extent)) : Bool}) ->
842 {Nat.is_lt(U32.to_nat(U32.from_nat(value)), U32.to_nat(extent)) == True{} : Bool}:
843 %Equal.sym(Nat, U32.to_nat(U32.from_nat(value)), value,
844 Conversion.natural_word_exact(value, extent, inside_le(value, U32.to_nat(extent), Equal.sym(Bool, True{}, Nat.is_lt(value, U32.to_nat(extent)), inside)))) :
845 {Nat.is_lt(_, U32.to_nat(extent)) == True{} : Bool}
846 Equal.sym(Bool, True{}, Nat.is_lt(value, U32.to_nat(extent)), inside)
847
848def product_natural_coordinates_status(values: List<&2, Nat>, +fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape,
849 +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +cursor: Nat, +index: U32,
850 a: Core.Tensor<left>, b: Core.Tensor<right>, out: Core.Tensor<output>,
851 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
852 -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
853 -fits: Coordinates.Fits([U32.to_nat(rows), U32.to_nat(columns)], values),
854 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool},
855 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
856 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
857 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
858 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_coordinates(left, right, output,
859 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, a, b, out, index, Shape.words(values))>:
860 match values:
861 case +row <> +column <> Nil{}:
862 Totality.Status{
863 {\{Coordinates.FStep: row_inside => tail =>
864 {\{Coordinates.FStep: column_inside => rest =>
865 {\{Totality.Status: successful => successful} :
866 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.dotted(left, right, output,
867 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), out, index,
868 Matrix.natural_dot(U32.to_nat(inner), left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, 0.0))> ->
869 {Result.is_done(&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.dotted(left, right, output,
870 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), out, index,
871 Matrix.natural_dot(U32.to_nat(inner), left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, 0.0))) == True{} : Bool}}(
872 product_dot_status(fuel, left, right, output, inner, columns, cursor, index,
873 Matrix.natural_dot(U32.to_nat(inner), left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, 0.0), out,
874 dot_loop_status(U32.to_nat(inner), left, right, rows, inner, right_inner, columns, U32.from_nat(row), U32.from_nat(column), 0n, 0.0,
875 a, b, le, re, compatible, coordinate_word_inside(row, rows, row_inside), coordinate_word_inside(column, columns, column_inside),
876 %Equal.sym(Nat, Nat.add(U32.to_nat(inner), 0n), U32.to_nat(inner), add_zero(U32.to_nat(inner))) : Shape.LE(_, U32.to_nat(inner))
877 Shape.LE.from(U32.to_nat(inner), U32.to_nat(inner), Equal.sym(Bool, Nat.is_le(U32.to_nat(inner), U32.to_nat(inner)), True{}, Conversion.le_reflexive(U32.to_nat(inner))))), inside, rec))} :
878 Coordinates.Fits([U32.to_nat(columns)], [column]) ->
879 {Result.is_done(&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_coordinates(left, right, output,
880 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, a, b, out, index,
881 [U32.from_nat(row), U32.from_nat(column)])) == True{} : Bool}}(tail)} :
882 Coordinates.Fits([U32.to_nat(rows), U32.to_nat(columns)], [row, column]) ->
883 {Result.is_done(&2, &1, Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_coordinates(left, right, output,
884 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, a, b, out, index,
885 [U32.from_nat(row), U32.from_nat(column)])) == True{} : Bool}}(fits)}
886 case Nil{}:
887 Totality.Status{Empty.absurd({False{} == True{} : Bool}, fits)}
888 case head <> Nil{}:
889 Totality.Status{{\{Coordinates.FStep: bound => tail => Empty.absurd({False{} == True{} : Bool}, tail)} :
890 Coordinates.Fits([U32.to_nat(rows), U32.to_nat(columns)], [head]) -> {False{} == True{} : Bool}}(fits)}
891 case first <> second <> third <> tail:
892 Totality.Status{{\{Coordinates.FStep: bound => rest =>
893 {\{Coordinates.FStep: bound => extra => Empty.absurd({False{} == True{} : Bool}, extra)} :
894 Coordinates.Fits([U32.to_nat(columns)], second <> third <> tail) -> {False{} == True{} : Bool}}(rest)} :
895 Coordinates.Fits([U32.to_nat(rows), U32.to_nat(columns)], first <> second <> third <> tail) -> {False{} == True{} : Bool}}(fits)}
896
897def product_coordinate_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape,
898 +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +cursor: Nat, +index: U32, coordinate: Shape.CheckedCoordinate<output>,
899 a: Core.Tensor<left>, b: Core.Tensor<right>, out: Core.Tensor<output>,
900 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
901 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
902 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool},
903 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
904 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
905 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
906 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_coordinates(left, right, output,
907 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, a, b, out, index, Shape.coordinate_values(output, coordinate))>:
908 Shape.CValues{+values, +valid} = coordinate
909 product_natural_coordinates_status(values, fuel, left, right, output, rows, inner, right_inner, columns, cursor, index, a, b, out, le, re, compatible,
910 %oe : Coordinates.Fits(Shape.naturals(_), values)
911 Coordinates.fits_of(Shape.extents(output), values, valid), inside, rec)
912
913def unflatten_done(+shape: Shape.Shape, +index: U32, result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<shape>>,
914 same: {result == Shape.unflatten_checked(shape, index) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<shape>>},
915 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
916 {Result.is_done(&2, &2, Shape.Error, Shape.CheckedCoordinate<shape>, result) == True{} : Bool}:
917 match result:
918 case Fail{error}:
919 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, value => Maybe.is_some(&2, List<&2, U32>, value), None{},
920 Some{Shape.words(Shape.indices(Shape.extents(shape), TransformProof.decoded_coordinate(shape, index, inside)))},
921 Equal.trans(Maybe<&2, List<&2, U32>>, None{}, ShapeLaws.coordinate_result(shape, Shape.unflatten_checked(shape, index)),
922 Some{Shape.words(Shape.indices(Shape.extents(shape), TransformProof.decoded_coordinate(shape, index, inside)))},
923 Equal.cong(Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<shape>>, Maybe<&2, List<&2, U32>>, ShapeLaws.coordinate_result(shape), Fail{error}, Shape.unflatten_checked(shape, index), same),
924 %Boundary.fin_of_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)) :
925 {ShapeLaws.coordinate_result(shape, Shape.unflatten_checked(shape, index)) == ShapeLaws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>}
926 ShapeLaws.unflatten_checked_refines(shape, index)))))
927 case Done{coordinate}:
928 {==}
929
930def product_unflattened_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape,
931 +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +cursor: Nat, +index: U32,
932 result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>, a: Core.Tensor<left>, b: Core.Tensor<right>, out: Core.Tensor<output>,
933 -successful: {Result.is_done(&2, &2, Shape.Error, Shape.CheckedCoordinate<output>, result) == True{} : Bool},
934 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
935 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
936 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool},
937 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
938 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
939 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
940 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_unflattened(left, right, output,
941 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, a, b, out, index, result)>:
942 match result:
943 case Fail{error}:
944 Totality.Status{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
945 case Done{coordinate}:
946 product_coordinate_status(fuel, left, right, output, rows, inner, right_inner, columns, cursor, index, coordinate, a, b, out, le, re, oe, compatible, inside, rec)
947
948def product_decision_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape,
949 +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +cursor: Nat,
950 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>, a: Core.Tensor<left>, b: Core.Tensor<right>, out: Core.Tensor<output>,
951 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
952 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
953 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
954 -inside: {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool},
955 -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @out: Core.Tensor<output> ->
956 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>,
957 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) ->
958 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.product_decided(left, right, output,
959 a => b => out => Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor), inner, columns, a, b, out, cursor, U32.from_nat(cursor), decision)>:
960 match decision:
961 case Shape.BFalse{equal}:
962 Totality.Status{Empty.absurd({False{} == True{} : Bool}, MathProof.conversion_clash(U32.to_nat(U32.from_nat(cursor)), cursor, exact, equal))}
963 case Shape.BTrue{equal}:
964 product_unflattened_status(fuel, left, right, output, rows, inner, right_inner, columns, cursor, U32.from_nat(cursor), Shape.unflatten_checked(output, U32.from_nat(cursor)), a, b, out,
965 unflatten_done(output, U32.from_nat(cursor), Shape.unflatten_checked(output, U32.from_nat(cursor)), {==},
966 %Equal.sym(Nat, Shape.elements(output), Shape.logical_numel(Shape.dimensions(output)), Shape.elements_exact(output)) : {True{} == Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) : Bool}
967 Equal.sym(Bool, Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), Shape.logical_numel(Shape.dimensions(output))), True{}, inside)),
968 le, re, oe, compatible, inside, rec)
969
970def product_loop_status(fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape,
971 +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +cursor: Nat, a: Core.Tensor<left>, b: Core.Tensor<right>, out: Core.Tensor<output>,
972 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
973 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
974 -bound: Shape.LE(Nat.add(fuel, cursor), Shape.elements(output))) ->
975 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, cursor)>:
976 match fuel:
977 case 0n:
978 Totality.Status{{==}}
979 case 1n+tail:
980 product_decision_status(tail, left, right, output, rows, inner, right_inner, columns, cursor,
981 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), a, b, out, MathProof.cursor_exact(tail, output, cursor, bound), le, re, oe, compatible,
982 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, MathProof.cursor_exact(tail, output, cursor, bound)) : {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}
983 %Shape.elements_exact(output) : {Nat.is_lt(cursor, _) == True{} : Bool}
984 MathProof.cursor_bounds(tail, cursor, Shape.elements(output), bound),
985 a => b => out => product_loop_status(tail, left, right, output, rows, inner, right_inner, columns, 1n+cursor, a, b, out, le, re, oe, compatible,
986 %Equal.sym(Nat, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), Arith.add_succ(tail, cursor)) : Shape.LE(_, Shape.elements(output))
987 bound))
988
989def created_status(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
990 result: Result<&2, &1, Core.Error, Core.Tensor<output>>, a: Core.Tensor<left>, b: Core.Tensor<right>,
991 -done: Allocation.TensorDone<output, result>,
992 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
993 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}) ->
994 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<output>, Matrix.created(left, right, output, inner, columns, a, b, result)>:
995 match result:
996 case Fail{error}:
997 Totality.Status{{\{Allocation.TensorDone: tensor => exact =>
998 Empty.absurd({False{} == True{} : Bool}, Shape.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<output>>, Bool,
999 Result.is_done(&2, &1, Core.Error, Core.Tensor<output>), Done{tensor}, Fail{error}, exact)))} :
1000 Allocation.TensorDone<output, Fail{error}> -> {False{} == True{} : Bool}}(done)}
1001 case Done{out}:
1002 product_loop_status(Shape.elements(output), left, right, output, rows, inner, right_inner, columns, 0n, a, b, out, le, re, oe, compatible,
1003 %Equal.sym(Nat, Nat.add(Shape.elements(output), 0n), Shape.elements(output), add_zero(Shape.elements(output))) : Shape.LE(_, Shape.elements(output))
1004 Shape.LE.from(Shape.elements(output), Shape.elements(output), Equal.sym(Bool, Nat.is_le(Shape.elements(output), Shape.elements(output)), True{}, Conversion.le_reflexive(Shape.elements(output)))))
1005
1006def multiply_status(+left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Plan<left, right>, a: Core.Tensor<left>, b: Core.Tensor<right>) ->
1007 Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & Core.Tensor<Matrix.output_shape(left, right, plan)>, Matrix.multiply(left, right, plan, a, b)>:
1008 match plan:
1009 case Matrix.Plan{+output, +rows, +inner, +right_inner, +columns, le, re, oe, compatible}:
1010 created_status(left, right, output, rows, inner, right_inner, columns, Core.new(output, 0.0), a, b,
1011 AllocationProof.core_new_done(output, 0.0), le, re, oe, compatible)
1012
1013type PlanStatus<-left: Shape.Shape, -right: Shape.Shape, -result: Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>> is Data:
1014 PlanStatus{-successful: {Result.is_done(&2, &2, Matrix.Error, Matrix.Plan<left, right>, result) == True{} : Bool}}
1015
1016def plan_output_status(+left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1017 result: Shape.ConstructResult<[rows, columns]>,
1018 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1019 -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1020 -built: {ShapeLaws.built([rows, columns], result) == Some{[rows, columns]} : Maybe<&2, List<&2, U32>>}) ->
1021 PlanStatus<left, right, Matrix.plan_output(left, right, rows, inner, right_inner, columns, le, re, compatible, result)>:
1022 match result:
1023 case Shape.SError{error}:
1024 PlanStatus{Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool,
1025 value => Maybe.is_some(&2, List<&2, U32>, value), None{}, Some{[rows, columns]}, built)))}
1026 case Shape.SBuilt{shape, preserved}:
1027 PlanStatus{{==}}
1028
1029def plan_compatible_status(+left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1030 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(inner), U32.to_nat(right_inner))>,
1031 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1032 -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}, -supported: Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)) ->
1033 PlanStatus<left, right, Matrix.plan_compatible(left, right, rows, inner, right_inner, columns, le, re, decision)>:
1034 match decision:
1035 case Shape.BFalse{equal}:
1036 PlanStatus{Empty.absurd({False{} == True{} : Bool}, MathProof.conversion_clash(U32.to_nat(inner), U32.to_nat(right_inner), compatible, equal))}
1037 case Shape.BTrue{equal}:
1038 plan_output_status(left, right, rows, inner, right_inner, columns, Shape.construct([rows, columns]), le, re,
1039 Lifecycle.natural_equal(U32.to_nat(inner), U32.to_nat(right_inner), equal),
1040 ShapeLaws.construction_complete([rows, columns], Unit{}, supported))
1041
1042def first_equal(+a: U32, +b: U32, +x: U32, +y: U32, same: {[a, b] == [x, y] : List<&2, U32>}) -> {a == x : U32}:
1043 Equal.cong(List<&2, U32>, U32, values => Maybe.default(&2, U32, List.get(&2, U32, values, 0n), 0), [a, b], [x, y], same)
1044
1045def second_equal(+a: U32, +b: U32, +x: U32, +y: U32, same: {[a, b] == [x, y] : List<&2, U32>}) -> {b == y : U32}:
1046 Equal.cong(List<&2, U32>, U32, values => Maybe.default(&2, U32, List.get(&2, U32, values, 1n), 0), [a, b], [x, y], same)
1047
1048def actual_admission(+left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1049 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1050 -valid: Totality.MatrixInputs<left, right>) -> Totality.MatrixBounds<rows, inner, right_inner, columns>:
1051 Totality.MatrixBounds{
1052 {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
1053 Equal.trans(Nat, U32.to_nat(inner), U32.to_nat(old_inner), U32.to_nat(right_inner),
1054 Equal.cong(U32, Nat, U32.to_nat, inner, old_inner, second_equal(rows, inner, old_rows, old_inner,
1055 Equal.trans(List<&2, U32>, [rows, inner], Shape.dimensions(left), [old_rows, old_inner], Equal.sym(List<&2, U32>, Shape.dimensions(left), [rows, inner], le), old_le))),
1056 Equal.trans(Nat, U32.to_nat(old_inner), U32.to_nat(old_right_inner), U32.to_nat(right_inner), compatible,
1057 Equal.cong(U32, Nat, U32.to_nat, old_right_inner, right_inner, Equal.sym(U32, right_inner, old_right_inner,
1058 first_equal(right_inner, columns, old_right_inner, old_columns,
1059 Equal.trans(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), [old_right_inner, old_columns], Equal.sym(List<&2, U32>, Shape.dimensions(right), [right_inner, columns], re), old_re))))))} :
1060 Totality.MatrixInputs<left, right> -> {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}}(valid),
1061 {\{Totality.MatrixInputs: old_rows => old_inner => old_right_inner => old_columns => old_le => old_re => compatible => supported =>
1062 %Equal.sym(U32, rows, old_rows, first_equal(rows, inner, old_rows, old_inner,
1063 Equal.trans(List<&2, U32>, [rows, inner], Shape.dimensions(left), [old_rows, old_inner], Equal.sym(List<&2, U32>, Shape.dimensions(left), [rows, inner], le), old_le))) :
1064 Shape.LE(Shape.logical_numel([_, columns]), 1048576n)
1065 %Equal.sym(U32, columns, old_columns, second_equal(right_inner, columns, old_right_inner, old_columns,
1066 Equal.trans(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), [old_right_inner, old_columns], Equal.sym(List<&2, U32>, Shape.dimensions(right), [right_inner, columns], re), old_re))) :
1067 Shape.LE(Shape.logical_numel([old_rows, _]), 1048576n)
1068 supported} : Totality.MatrixInputs<left, right> -> Shape.LE(Shape.logical_numel([rows, columns]), 1048576n)}(valid)}
1069
1070def rank_clash(+left: Shape.Shape, +right: Shape.Shape, +dimensions: List<&2, U32>,
1071 +same: {dimensions == Shape.dimensions(left) : List<&2, U32>}, +different: {Nat.is_eq(Shape.rank_dimensions(dimensions), 2n) == False{} : Bool},
1072 -valid: Totality.MatrixInputs<left, right>) -> Totality.Impossible:
1073 Totality.Impossible{{\{Totality.MatrixInputs: rows => inner => right_inner => columns => le => re => compatible => supported =>
1074 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), True{},
1075 Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), False{}, different),
1076 Equal.cong(List<&2, U32>, Bool, values => Nat.is_eq(Shape.rank_dimensions(values), 2n), dimensions, [rows, inner],
1077 Equal.trans(List<&2, U32>, dimensions, Shape.dimensions(left), [rows, inner], same, le))))} :
1078 Totality.MatrixInputs<left, right> -> Empty}(valid)}
1079
1080def swapped_inputs(+left: Shape.Shape, +right: Shape.Shape, -valid: Totality.MatrixInputs<left, right>) ->
1081 Totality.RankTwo<right>:
1082 Totality.RankTwo{{\{Totality.MatrixInputs: rows => inner => right_inner => columns => le => re => compatible => supported =>
1083 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, Shape.dimensions(right), [right_inner, columns], re)} :
1084 Totality.MatrixInputs<left, right> -> {Shape.rank_dimensions(Shape.dimensions(right)) == 2n : Nat}}(valid)}
1085
1086def right_rank_clash(+left: Shape.Shape, +right: Shape.Shape, +dimensions: List<&2, U32>,
1087 +same: {dimensions == Shape.dimensions(right) : List<&2, U32>}, +different: {Nat.is_eq(Shape.rank_dimensions(dimensions), 2n) == False{} : Bool},
1088 +rank: {Shape.rank_dimensions(Shape.dimensions(right)) == 2n : Nat}) -> Empty:
1089 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), True{},
1090 Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), False{}, different),
1091 Equal.cong(Nat, Bool, n => Nat.is_eq(n, 2n), Shape.rank_dimensions(dimensions), 2n,
1092 Equal.trans(Nat, Shape.rank_dimensions(dimensions), Shape.rank_dimensions(Shape.dimensions(right)), 2n,
1093 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, dimensions, Shape.dimensions(right), same), rank))))
1094
1095def plan_right_status(dimensions: List<&2, U32>, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32,
1096 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -same: {dimensions == Shape.dimensions(right) : List<&2, U32>},
1097 -valid: Totality.MatrixInputs<left, right>) -> PlanStatus<left, right, Matrix.plan_right(left, right, rows, inner, le, dimensions, same)>:
1098 match dimensions:
1099 case +right_inner <> +columns <> Nil{}:
1100 PlanStatus{{\{Totality.MatrixBounds: compatible => supported =>
1101 {\{PlanStatus: successful => successful} : PlanStatus<left, right,
1102 Matrix.plan_compatible(left, right, rows, inner, right_inner, columns, le, Equal.sym(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), same),
1103 Shape.bool_case(Nat.is_eq(U32.to_nat(inner), U32.to_nat(right_inner))))> ->
1104 {Result.is_done(&2, &2, Matrix.Error, Matrix.Plan<left, right>, Matrix.plan_right(left, right, rows, inner, le, [right_inner, columns], same)) == True{} : Bool}}(
1105 plan_compatible_status(left, right, rows, inner, right_inner, columns, Shape.bool_case(Nat.is_eq(U32.to_nat(inner), U32.to_nat(right_inner))), le,
1106 Equal.sym(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), same), compatible, supported))} :
1107 Totality.MatrixBounds<rows, inner, right_inner, columns> -> {Result.is_done(&2, &2, Matrix.Error, Matrix.Plan<left, right>, Matrix.plan_right(left, right, rows, inner, le, [right_inner, columns], same)) == True{} : Bool}}(
1108 actual_admission(left, right, rows, inner, right_inner, columns, le, Equal.sym(List<&2, U32>, [right_inner, columns], Shape.dimensions(right), same), valid))}
1109 case Nil{}:
1110 PlanStatus{Empty.absurd({False{} == True{} : Bool}, right_rank_clash(left, right, Nil{}, same, {==},
1111 {\{Totality.RankTwo: rank => rank} : Totality.RankTwo<right> -> {Shape.rank_dimensions(Shape.dimensions(right)) == 2n : Nat}}(swapped_inputs(left, right, valid))))}
1112 case head <> Nil{}:
1113 PlanStatus{Empty.absurd({False{} == True{} : Bool}, right_rank_clash(left, right, [head], same, {==},
1114 {\{Totality.RankTwo: rank => rank} : Totality.RankTwo<right> -> {Shape.rank_dimensions(Shape.dimensions(right)) == 2n : Nat}}(swapped_inputs(left, right, valid))))}
1115 case first <> second <> third <> rest:
1116 PlanStatus{Empty.absurd({False{} == True{} : Bool}, right_rank_clash(left, right, first <> second <> third <> rest, same, {==},
1117 {\{Totality.RankTwo: rank => rank} : Totality.RankTwo<right> -> {Shape.rank_dimensions(Shape.dimensions(right)) == 2n : Nat}}(swapped_inputs(left, right, valid))))}
1118
1119def plan_left_status(dimensions: List<&2, U32>, +left: Shape.Shape, +right: Shape.Shape,
1120 -same: {dimensions == Shape.dimensions(left) : List<&2, U32>}, -valid: Totality.MatrixInputs<left, right>) ->
1121 PlanStatus<left, right, Matrix.plan_left(left, right, dimensions, same)>:
1122 match dimensions:
1123 case +rows <> +inner <> Nil{}:
1124 plan_right_status(Shape.dimensions(right), left, right, rows, inner, Equal.sym(List<&2, U32>, [rows, inner], Shape.dimensions(left), same), {==}, valid)
1125 case Nil{}:
1126 PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, Nil{}, same, {==}, valid)))}
1127 case head <> Nil{}:
1128 PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, [head], same, {==}, valid)))}
1129 case first <> second <> third <> rest:
1130 PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, first <> second <> third <> rest, same, {==}, valid)))}
1131
1132def plan_status(+left: Shape.Shape, +right: Shape.Shape, -valid: Totality.MatrixInputs<left, right>) -> PlanStatus<left, right, Matrix.plan(left, right)>:
1133 plan_left_status(Shape.dimensions(left), left, right, {==}, valid)
1134
1135def plan_left_rank(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1136 -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1137 not_matrix: {Shape.rank_dimensions(dims) != 2n : Nat}) ->
1138 {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1139 match dims:
1140 case Nil{}:
1141 {==}
1142 case +x <> Nil{}:
1143 {==}
1144 case +rows <> +inner <> Nil{}:
1145 Empty.absurd({Matrix.plan_left(left, right, [rows, inner], same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1146 not_matrix({==}))
1147 case +x <> +y <> +z <> +t:
1148 {==}
1149
1150def Laws.matmul_left_rank_error(left, right, a, b, not_matrix):
1151 %Equal.sym(Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>, Matrix.plan_left(left, right, Shape.dimensions(left), {==}), Fail{Matrix.RankMismatch{}},
1152 plan_left_rank(left, right, Shape.dimensions(left), {==}, not_matrix)) :
1153 {Matrix.parallel_planned(left, right, a, b, _) == Fail{Matrix.RankMismatch{}} : Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic>}
1154 {==}
1155
1156def plan_right_rank(-left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32,
1157 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, +dims: List<&2, U32>,
1158 -same: {dims == Shape.dimensions(right) : List<&2, U32>},
1159 not_matrix: {Shape.rank_dimensions(dims) != 2n : Nat}) ->
1160 {Matrix.plan_right(left, right, rows, inner, le, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1161 match dims:
1162 case Nil{}:
1163 {==}
1164 case +x <> Nil{}:
1165 {==}
1166 case +right_inner <> +columns <> Nil{}:
1167 Empty.absurd({Matrix.plan_right(left, right, rows, inner, le, [right_inner, columns], same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1168 not_matrix({==}))
1169 case +x <> +y <> +z <> +t:
1170 {==}
1171
1172def plan_left_right_rank(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1173 -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1174 not_matrix: {Shape.rank_dimensions(Shape.dimensions(right)) != 2n : Nat}) ->
1175 {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1176 match dims:
1177 case Nil{}:
1178 {==}
1179 case +x <> Nil{}:
1180 {==}
1181 case +rows <> +inner <> Nil{}:
1182 plan_right_rank(left, right, rows, inner, Equal.sym(List<&2, U32>, [rows, inner], Shape.dimensions(left), same),
1183 Shape.dimensions(right), {==}, not_matrix)
1184 case +x <> +y <> +z <> +t:
1185 {==}
1186
1187def Laws.matmul_right_rank_error(left, right, a, b, not_matrix):
1188 %Equal.sym(Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>, Matrix.plan_left(left, right, Shape.dimensions(left), {==}), Fail{Matrix.RankMismatch{}},
1189 plan_left_right_rank(left, right, Shape.dimensions(left), {==}, not_matrix)) :
1190 {Matrix.parallel_planned(left, right, a, b, _) == Fail{Matrix.RankMismatch{}} : Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic>}
1191 {==}
1192
1193def compatible_inner(-left: Shape.Shape, -right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1194 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>},
1195 -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1196 mismatch: {U32.to_nat(inner) != U32.to_nat(right_inner) : Nat},
1197 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(inner), U32.to_nat(right_inner))>) ->
1198 {Matrix.plan_compatible(left, right, rows, inner, right_inner, columns, le, re, decision) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1199 match decision:
1200 case Shape.BFalse{equal}:
1201 {==}
1202 case Shape.BTrue{equal}:
1203 Empty.absurd({Matrix.plan_compatible(left, right, rows, inner, right_inner, columns, le, re, Shape.BTrue{equal}) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1204 mismatch(Lifecycle.natural_equal(U32.to_nat(inner), U32.to_nat(right_inner), equal)))
1205
1206def first_nat(values: List<&2, U32>) -> Nat:
1207 match values:
1208 case first <> rest:
1209 U32.to_nat(first)
1210 case Nil{}:
1211 0n
1212
1213def second_nat(values: List<&2, U32>) -> Nat:
1214 match values:
1215 case first <> second <> rest:
1216 U32.to_nat(second)
1217 case rest:
1218 0n
1219
1220def inner_right(-left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32,
1221 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, +dims: List<&2, U32>,
1222 -same: {dims == Shape.dimensions(right) : List<&2, U32>},
1223 -wanted_inner: U32, -right_inner: U32, -columns: U32,
1224 right_matrix: {dims == [right_inner, columns] : List<&2, U32>},
1225 inner_same: {U32.to_nat(inner) == U32.to_nat(wanted_inner) : Nat},
1226 mismatch: {U32.to_nat(wanted_inner) != U32.to_nat(right_inner) : Nat}) ->
1227 {Matrix.plan_right(left, right, rows, inner, le, dims, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1228 match dims:
1229 case +ri <> +c <> Nil{}:
1230 compatible_inner(left, right, rows, inner, ri, c, le, Equal.sym(List<&2, U32>, [ri, c], Shape.dimensions(right), same),
1231 equal => mismatch(Equal.trans(Nat, U32.to_nat(wanted_inner), U32.to_nat(inner), U32.to_nat(right_inner),
1232 Equal.sym(Nat, U32.to_nat(inner), U32.to_nat(wanted_inner), inner_same),
1233 Equal.trans(Nat, U32.to_nat(inner), U32.to_nat(ri), U32.to_nat(right_inner), equal,
1234 Equal.cong(List<&2, U32>, Nat, first_nat, [ri, c], [right_inner, columns], right_matrix)))),
1235 Shape.bool_case(Nat.is_eq(U32.to_nat(inner), U32.to_nat(ri))))
1236 case Nil{}:
1237 Empty.absurd({Matrix.plan_right(left, right, rows, inner, le, Nil{}, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1238 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), Nil{}, [right_inner, columns], right_matrix)))
1239 case +x <> Nil{}:
1240 Empty.absurd({Matrix.plan_right(left, right, rows, inner, le, [x], same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1241 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), [x], [right_inner, columns], right_matrix)))
1242 case +x <> +y <> +z <> +t:
1243 Empty.absurd({Matrix.plan_right(left, right, rows, inner, le, x <> y <> z <> t, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1244 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), x <> y <> z <> t, [right_inner, columns], right_matrix)))
1245
1246def inner_left(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1247 -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1248 -rows: U32, -inner: U32, -right_inner: U32, -columns: U32,
1249 left_matrix: {dims == [rows, inner] : List<&2, U32>},
1250 right_matrix: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1251 mismatch: {U32.to_nat(inner) != U32.to_nat(right_inner) : Nat}) ->
1252 {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1253 match dims:
1254 case +r <> +i <> Nil{}:
1255 inner_right(left, right, r, i, Equal.sym(List<&2, U32>, [r, i], Shape.dimensions(left), same), Shape.dimensions(right), {==},
1256 inner, right_inner, columns, right_matrix,
1257 Equal.cong(List<&2, U32>, Nat, second_nat, [r, i], [rows, inner], left_matrix), mismatch)
1258 case Nil{}:
1259 Empty.absurd({Matrix.plan_left(left, right, Nil{}, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1260 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), Nil{}, [rows, inner], left_matrix)))
1261 case +x <> Nil{}:
1262 Empty.absurd({Matrix.plan_left(left, right, [x], same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1263 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), [x], [rows, inner], left_matrix)))
1264 case +x <> +y <> +z <> +t:
1265 Empty.absurd({Matrix.plan_left(left, right, x <> y <> z <> t, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1266 Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), x <> y <> z <> t, [rows, inner], left_matrix)))
1267
1268def Laws.matmul_inner_error(left, right, a, b, rows, inner, right_inner, columns, left_matrix, right_matrix, mismatch):
1269 %Equal.sym(Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>, Matrix.plan_left(left, right, Shape.dimensions(left), {==}), Fail{Matrix.InnerDimensionMismatch{}},
1270 inner_left(left, right, Shape.dimensions(left), {==}, rows, inner, right_inner, columns, left_matrix, right_matrix, mismatch)) :
1271 {Matrix.parallel_planned(left, right, a, b, _) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic>}
1272 {==}
1273
1274
1275
1276
1277
1278def KeptCopy(+shape: Shape.Shape, -a: Core.Tensor<shape>, -Q: Core.Dynamic & Array<F32> -> Type) -> Type:
1279 @-kept: Core.Tensor<shape> -> @-copy: Array<F32> ->
1280 @-taken: Parallel.Taken<Core.Packed{shape, a}, (Core.Packed{shape, kept}, copy)> ->
1281 Q((Core.Packed{shape, kept}, copy))
1282
1283def take_owned_lift(+shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
1284 -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -balanced: Model.Balanced(F32, depth, array),
1285 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
1286 -Q: Core.Dynamic & Array<F32> -> Type,
1287 h: KeptCopy(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, Q)) ->
1288 Q(Elementwise.take_owned(shape, depth, length, array, pair, same, balanced, valid, exact)):
1289 (kept, copy) = pair
1290 h(Core.TTensor{Storage.Owned{depth, length, kept, Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid}, exact})(copy)(
1291 Parallel.taken_owned(shape, depth, length, array, (kept, copy), same, balanced, valid, exact))
1292
1293def take_lift(+shape: Shape.Shape, a: Core.Tensor<shape>, -Q: Core.Dynamic & Array<F32> -> Type, h: KeptCopy(shape, a, Q)) ->
1294 Q(Elementwise.take(Core.Packed{shape, a})):
1295 Core.TTensor{storage, exact} = a
1296 match storage:
1297 case Storage.Empty{}:
1298 h(Core.TTensor{Storage.Empty{}, exact})(Array.new(F32, 0n, 0.0))(Parallel.taken(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}))
1299 case Storage.Owned{+depth, +length, array, balanced, valid}:
1300 take_owned_lift(shape, depth, length, array, Array.clone(F32, array), {==}, balanced, valid, exact, Q, h)
1301
1302def inspected(found: ElementwiseTotality.Inspection) -> Maybe<&2, F32>:
1303 match found:
1304 case ElementwiseTotality.Dims{dimensions}:
1305 None{}
1306 case ElementwiseTotality.Value{value}:
1307 value
1308
1309def kept_observe(+shape: Shape.Shape, -a: Core.Tensor<shape>, -kept: Core.Tensor<shape>,
1310 -same: ElementwiseTotality.SameSource(Core.Packed{shape, a}, Core.Packed{shape, kept}), +other: U32) ->
1311 Parallel.Fact<{Core.checked_observe(shape, kept, other) == Core.checked_observe(shape, a, other) : Maybe<&2, F32>}>:
1312 Parallel.Fact{Equal.cong(ElementwiseTotality.Inspection, Maybe<&2, F32>, inspected,
1313 ElementwiseTotality.inspect(ElementwiseTotality.Checked{other}, Core.Packed{shape, kept}),
1314 ElementwiseTotality.inspect(ElementwiseTotality.Checked{other}, Core.Packed{shape, a}), same(ElementwiseTotality.Checked{other}))}
1315
1316def taken_keeps(+shape: Shape.Shape, -a: Core.Tensor<shape>, -kept: Core.Tensor<shape>, -copy: Array<F32>,
1317 -taken: Parallel.Taken<Core.Packed{shape, a}, (Core.Packed{shape, kept}, copy)>, +other: U32) ->
1318 Parallel.Fact<{Core.checked_observe(shape, kept, other) == Core.checked_observe(shape, a, other) : Maybe<&2, F32>}>:
1319 kept_observe(shape, a, kept, {\{Parallel.Taken: depth => balanced => reads => retained => retained} :
1320 Parallel.Taken<Core.Packed{shape, a}, (Core.Packed{shape, kept}, copy)> -> ElementwiseTotality.SameSource(Core.Packed{shape, a}, Core.Packed{shape, kept})}(taken), other)
1321
1322
1323def coordinate_read(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, -index: U32,
1324 result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
1325 found: {ShapeLaws.index_result(shape, result) == Some{index} : Maybe<&2, U32>}) ->
1326 {Laws.coordinate_observe_result(shape, tensor, result) == Core.checked_observe(shape, tensor, index) : Maybe<&2, F32>}:
1327 match result:
1328 case Fail{error}:
1329 Empty.absurd({Laws.coordinate_observe_result(shape, tensor, Fail{error}) == Core.checked_observe(shape, tensor, index) : Maybe<&2, F32>},
1330 Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, value => Maybe.is_some(&2, U32, value), None{}, Some{index}, found)))
1331 case Done{flat}:
1332 %MatrixIndex.some_equal(U32, Shape.index_value(shape, flat), index, found) :
1333 {Core.checked_observe(shape, tensor, Shape.index_value(shape, flat)) == Core.checked_observe(shape, tensor, _) : Maybe<&2, F32>}
1334 {==}
1335
1336def left_flat(+left: Shape.Shape, +rows: U32, +inner: U32, +row: Nat, +k: Nat,
1337 +le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>},
1338 +row_below: {Nat.is_lt(row, U32.to_nat(rows)) == True{} : Bool}, +below: {Nat.is_lt(k, U32.to_nat(inner)) == True{} : Bool}) ->
1339 {ShapeLaws.index_result(left, Shape.flatten_checked(left, [U32.from_nat(row), U32.from_nat(k)])) ==
1340 Some{Matrix.left_index(U32.to_nat(inner), row, k)} : Maybe<&2, U32>}:
1341 +k_exact = MatrixIndex.word_below(k, inner, below)
1342 +row_exact = MatrixIndex.word_below(row, rows, row_below)
1343 Equal.trans(Maybe<&2, U32>, ShapeLaws.index_result(left, Shape.flatten_checked(left, [U32.from_nat(row), U32.from_nat(k)])),
1344 Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(row)), U32.to_nat(inner)), U32.to_nat(U32.from_nat(k))))},
1345 Some{U32.from_nat(Nat.add(Nat.mul(row, U32.to_nat(inner)), k))},
1346 MatrixIndex.flat_pair(left, rows, inner, U32.from_nat(row), U32.from_nat(k), le,
1347 MatrixIndex.lt_same(U32.to_nat(U32.from_nat(row)), row, U32.to_nat(rows), row_exact, row_below),
1348 MatrixIndex.lt_same(U32.to_nat(U32.from_nat(k)), k, U32.to_nat(inner), k_exact, below)),
1349 MatrixIndex.index_same(U32.to_nat(U32.from_nat(row)), U32.to_nat(U32.from_nat(k)), row, k, U32.to_nat(inner), row_exact, k_exact))
1350
1351def right_flat(+right: Shape.Shape, +inner: U32, +right_inner: U32, +columns: U32, +column: Nat, +k: Nat,
1352 +re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1353 +compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1354 +column_below: {Nat.is_lt(column, U32.to_nat(columns)) == True{} : Bool}, +below: {Nat.is_lt(k, U32.to_nat(inner)) == True{} : Bool}) ->
1355 {ShapeLaws.index_result(right, Shape.flatten_checked(right, [U32.from_nat(k), U32.from_nat(column)])) ==
1356 Some{Matrix.right_index(U32.to_nat(columns), column, k)} : Maybe<&2, U32>}:
1357 +k_exact = MatrixIndex.word_below(k, inner, below)
1358 +column_exact = MatrixIndex.word_below(column, columns, column_below)
1359 Equal.trans(Maybe<&2, U32>, ShapeLaws.index_result(right, Shape.flatten_checked(right, [U32.from_nat(k), U32.from_nat(column)])),
1360 Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(U32.from_nat(k)), U32.to_nat(columns)), U32.to_nat(U32.from_nat(column))))},
1361 Some{U32.from_nat(Nat.add(Nat.mul(k, U32.to_nat(columns)), column))},
1362 MatrixIndex.flat_pair(right, right_inner, columns, U32.from_nat(k), U32.from_nat(column), re,
1363 MatrixIndex.lt_same(U32.to_nat(U32.from_nat(k)), k, U32.to_nat(right_inner), k_exact,
1364 MatrixIndex.lt_bound(k, U32.to_nat(inner), U32.to_nat(right_inner), compatible, below)),
1365 MatrixIndex.lt_same(U32.to_nat(U32.from_nat(column)), column, U32.to_nat(columns), column_exact, column_below)),
1366 MatrixIndex.index_same(U32.to_nat(U32.from_nat(k)), U32.to_nat(U32.from_nat(column)), k, column, U32.to_nat(columns), k_exact, column_exact))
1367
1368def left_extents(+left: Shape.Shape, +rows: U32, +inner: U32, +le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}) ->
1369 {Shape.extents(left) == [U32.to_nat(rows), U32.to_nat(inner)] : List<&2, Nat>}:
1370 Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(left), [rows, inner], le)
1371
1372def right_extents(+right: Shape.Shape, +inner: U32, +right_inner: U32, +columns: U32,
1373 +re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1374 +compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}) ->
1375 {Shape.extents(right) == [U32.to_nat(inner), U32.to_nat(columns)] : List<&2, Nat>}:
1376 Equal.trans(List<&2, Nat>, Shape.extents(right), [U32.to_nat(right_inner), U32.to_nat(columns)], [U32.to_nat(inner), U32.to_nat(columns)],
1377 Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(right), [right_inner, columns], re),
1378 Equal.cong(Nat, List<&2, Nat>, n => [n, U32.to_nat(columns)], U32.to_nat(right_inner), U32.to_nat(inner),
1379 Equal.sym(Nat, U32.to_nat(inner), U32.to_nat(right_inner), compatible)))
1380
1381
1382
1383def logical_dot(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1384 +row: Nat, +column: Nat, +le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>},
1385 +re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1386 +compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1387 +row_below: {Nat.is_lt(row, U32.to_nat(rows)) == True{} : Bool},
1388 +column_below: {Nat.is_lt(column, U32.to_nat(columns)) == True{} : Bool},
1389 -a: Core.Tensor<left>, -b: Core.Tensor<right>, +dl: Nat, +dr: Nat, -cl: Array<F32>, -cr: Array<F32>,
1390 -left_reads: Parallel.SourceReads(Core.Packed{left, a}, dl, cl), -right_reads: Parallel.SourceReads(Core.Packed{right, b}, dr, cr),
1391 +cursor: Nat, +steps: {Nat.add(cursor, fuel) == U32.to_nat(inner) : Nat}, values: List<&2, DotFold.Factors>,
1392 -arr: MatmulParallel.LogicalArr(fuel, dl, dr, cl, cr, U32.to_nat(inner), U32.to_nat(columns), row, column, cursor, values)) ->
1393 Parallel.Fact<Laws.LogicalDot(fuel, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, values)>:
1394 match fuel values:
1395 case 0n Nil{}:
1396 Parallel.Fact{Unit{}}
1397 case 1n+tail DotFold.Factors{lv, rv} <> rest:
1398 +below = MatrixIndex.cursor_below(cursor, tail, U32.to_nat(inner), steps)
1399 +left_at = Matrix.left_index(U32.to_nat(inner), row, cursor)
1400 +right_at = Matrix.right_index(U32.to_nat(columns), column, cursor)
1401 +left_inside = MatrixIndex.word_inside(Nat.add(Nat.mul(row, U32.to_nat(inner)), cursor), left,
1402 MatrixIndex.left_below(U32.to_nat(rows), U32.to_nat(inner), row, row_below, left, left_extents(left, rows, inner, le), cursor, below))
1403 +right_inside = MatrixIndex.word_inside(Nat.add(Nat.mul(cursor, U32.to_nat(columns)), column), right,
1404 MatrixIndex.right_below(U32.to_nat(inner), U32.to_nat(columns), column, column_below, right,
1405 right_extents(right, inner, right_inner, columns, re, compatible), cursor, below))
1406 Parallel.Fact{{\{MatmulParallel.ArrStep: left_observed => right_observed => remaining =>
1407 Laws.DotStep{MatrixIndex.word_below(cursor, inner, below),
1408 Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(left, a, [U32.from_nat(row), U32.from_nat(cursor)]),
1409 Core.checked_observe(left, a, left_at), Some{lv},
1410 coordinate_read(left, a, left_at, Shape.flatten_checked(left, [U32.from_nat(row), U32.from_nat(cursor)]),
1411 left_flat(left, rows, inner, row, cursor, le, row_below, below)),
1412 Equal.trans(Maybe<&2, F32>, Core.checked_observe(left, a, left_at), Model.observe(F32, dl, cl, Refinement.route(dl, left_at)), Some{lv},
1413 Equal.sym(Maybe<&2, F32>, Model.observe(F32, dl, cl, Refinement.route(dl, left_at)), Core.checked_observe(left, a, left_at),
1414 left_reads(left_at)(left_inside)),
1415 left_observed)),
1416 Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), U32.from_nat(column)]),
1417 Core.checked_observe(right, b, right_at), Some{rv},
1418 coordinate_read(right, b, right_at, Shape.flatten_checked(right, [U32.from_nat(cursor), U32.from_nat(column)]),
1419 right_flat(right, inner, right_inner, columns, column, cursor, re, compatible, column_below, below)),
1420 Equal.trans(Maybe<&2, F32>, Core.checked_observe(right, b, right_at), Model.observe(F32, dr, cr, Refinement.route(dr, right_at)), Some{rv},
1421 Equal.sym(Maybe<&2, F32>, Model.observe(F32, dr, cr, Refinement.route(dr, right_at)), Core.checked_observe(right, b, right_at),
1422 right_reads(right_at)(right_inside)),
1423 right_observed)),
1424 {\{Parallel.Fact: p => p} : Parallel.Fact<Laws.LogicalDot(tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 1n+cursor, rest)> ->
1425 Laws.LogicalDot(tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 1n+cursor, rest)}(
1426 logical_dot(tail, left, right, rows, inner, right_inner, columns, row, column, le, re, compatible, row_below, column_below, a, b, dl, dr, cl, cr, left_reads, right_reads,
1427 1n+cursor, MatrixIndex.steps_next(cursor, tail, U32.to_nat(inner), steps), rest, remaining))}} :
1428 MatmulParallel.ArrStep<tail, dl, dr, cl, cr, U32.to_nat(inner), U32.to_nat(columns), row, column, cursor, lv, rv, rest> ->
1429 Laws.DotStep<tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, lv, rv, rest>}(arr)}
1430 case 0n DotFold.Factors{lv, rv} <> rest:
1431 Parallel.Fact{Empty.absurd(Laws.LogicalDot(0n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, DotFold.Factors{lv, rv} <> rest), arr)}
1432 case 1n+tail Nil{}:
1433 Parallel.Fact{Empty.absurd(Laws.LogicalDot(1n+tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, Nil{}), arr)}
1434
1435type Decoded<-output: Shape.Shape, -index: U32, -row: U32, -column: U32> is Data:
1436 Decoded{-coordinate: Shape.CheckedCoordinate<output>,
1437 -decoded: {Shape.unflatten_checked(output, index) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
1438 -coordinates: {Shape.coordinate_values(output, coordinate) == [row, column] : List<&2, U32>}}
1439
1440def decoded_of(+output: Shape.Shape, +index: U32, +row: U32, +column: U32,
1441 result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>,
1442 -same: {result == Shape.unflatten_checked(output, index) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
1443 -found: {ShapeLaws.coordinate_result(output, result) == Some{[row, column]} : Maybe<&2, List<&2, U32>>}) ->
1444 Parallel.Fact<Decoded<output, index, row, column>>:
1445 match result:
1446 case Fail{error}:
1447 Parallel.Fact{Empty.absurd(Decoded<output, index, row, column>,
1448 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, value => Maybe.is_some(&2, List<&2, U32>, value), None{}, Some{[row, column]}, found)))}
1449 case Done{coordinate}:
1450 Parallel.Fact{Decoded{coordinate,
1451 Equal.sym(Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>, Done{coordinate}, Shape.unflatten_checked(output, index), same),
1452 MatrixIndex.some_equal(List<&2, U32>, Shape.coordinate_values(output, coordinate), [row, column], found)}}
1453
1454
1455
1456def product_cell(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1457 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1458 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1459 +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
1460 -exact: {length == Shape.logical_numel(Shape.dimensions(output)) : Nat},
1461 -a: Core.Tensor<left>, -b: Core.Tensor<right>, -dl: Nat, -dr: Nat, -cl: Array<F32>, -cr: Array<F32>,
1462 -bl: Model.Balanced(F32, dl, cl), -br: Model.Balanced(F32, dr, cr),
1463 -left_reads: Parallel.SourceReads(Core.Packed{left, a}, dl, cl), -right_reads: Parallel.SourceReads(Core.Packed{right, b}, dr, cr),
1464 +position: Nat, -earlier: {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
1465 Parallel.Fact<Laws.ProductCell<inner, left, right, a, b, output,
1466 Core.TTensor{Storage.Owned{depth, length,
1467 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, cl, cr),
1468 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, cl, cr),
1469 valid}, exact}, position>>:
1470 -inner_n = U32.to_nat(inner)
1471 -columns_n = U32.to_nat(columns)
1472 -row = Matrix.row_of(columns_n, position)
1473 -column = Matrix.column_of(columns_n, position)
1474 -index = U32.from_nat(position)
1475 -extents = Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(output), [rows, columns], oe)
1476 -fit = MatrixIndex.position_fits(output, U32.to_nat(rows), columns_n, extents, position, earlier)
1477 -row_below = Arith.and_left(Nat.is_lt(row, U32.to_nat(rows)), Bool.and(Nat.is_lt(column, columns_n), True{}), fit)
1478 -column_below = Arith.and_left(Nat.is_lt(column, columns_n), True{},
1479 Arith.and_right(Nat.is_lt(row, U32.to_nat(rows)), Bool.and(Nat.is_lt(column, columns_n), True{}), fit))
1480 -word_exact = MatrixIndex.word_exact(position, output, earlier)
1481 -below = MatrixIndex.lt_bound(position, Shape.logical_numel(Shape.dimensions(output)), length,
1482 Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(output)), exact), earlier)
1483 -inside = MatrixIndex.lt_same(U32.to_nat(index), position, length, word_exact, below)
1484 -tree = Matrix.build(depth, Matrix.product_splits(depth, inner_n), inner_n, columns_n, length, 0n, cl, cr)
1485 -path = Refinement.route(depth, index)
1486 -cells = {\{Parallel.Fact: p => p} :
1487 Parallel.Fact<MatmulParallel.Cells(depth, dl, dr, cl, cr, inner_n, columns_n, length, 0n, tree)> ->
1488 MatmulParallel.Cells(depth, dl, dr, cl, cr, inner_n, columns_n, length, 0n, tree)}(
1489 MatmulParallel.build_cells(depth, Matrix.product_splits(depth, inner_n), dl, dr, cl, cr, inner_n, columns_n, length, 0n, cl, cr, {==}, {==}, bl, br))
1490 -position_eq = Equal.trans(Nat, Nat.add(Model.offset(depth, path), 0n), U32.to_nat(index), position,
1491 Parallel.output_position(depth, length, index, valid, inside), word_exact)
1492 -at = {\{Parallel.Fact: p => p} :
1493 Parallel.Fact<MatmulParallel.CellIs(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path))> ->
1494 MatmulParallel.CellIs(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path))}(
1495 MatmulParallel.cell_shift(dl, dr, cl, cr, inner_n, columns_n, length, Nat.add(Model.offset(depth, path), 0n), position,
1496 Model.observe(F32, depth, tree, path), position_eq, cells(path)))
1497 -cell = {\{Parallel.Fact: p => p} :
1498 Parallel.Fact<MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)>> ->
1499 MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)>}(
1500 MatmulParallel.cell_below(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path), below, at))
1501 -matched = Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), Route.index_complete(depth, length, index, valid, inside))
1502 -decoded = {\{Parallel.Fact: p => p} : Parallel.Fact<Decoded<output, index, U32.from_nat(row), U32.from_nat(column)>> ->
1503 Decoded<output, index, U32.from_nat(row), U32.from_nat(column)>}(
1504 decoded_of(output, index, U32.from_nat(row), U32.from_nat(column), Shape.unflatten_checked(output, index), {==},
1505 MatrixIndex.unflatten_at(output, U32.to_nat(rows), columns_n, extents, position, earlier)))
1506 Parallel.Fact{{\{MatmulParallel.CellAt: word => observed => values => logical => fold =>
1507 {\{Decoded: coordinate => found => coordinates =>
1508 Laws.ProductCell{U32.from_nat(row), U32.from_nat(column), coordinate, found, coordinates, word_exact, values,
1509 {\{Parallel.Fact: p => p} :
1510 Parallel.Fact<Laws.LogicalDot(inner_n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, values)> ->
1511 Laws.LogicalDot(inner_n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, values)}(
1512 logical_dot(inner_n, left, right, rows, inner, right_inner, columns, row, column, le, re, compatible, row_below, column_below,
1513 a, b, dl, dr, cl, cr, left_reads, right_reads, 0n, {==}, values, logical)),
1514 word, fold, matched,
1515 Equal.trans(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, tree, index, Nat.is_lt(U32.to_nat(index), length)),
1516 Model.observe(F32, depth, tree, path), Some{word},
1517 Parallel.observe_allowed_equal(depth, length, tree, index, Nat.is_lt(U32.to_nat(index), length), inside, matched), observed)}} :
1518 Decoded<output, index, U32.from_nat(row), U32.from_nat(column)> ->
1519 Laws.ProductCell<inner, left, right, a, b, output,
1520 Core.TTensor{Storage.Owned{depth, length, tree, Matrix.build_balanced(depth, Matrix.product_splits(depth, inner_n), inner_n, columns_n, length, 0n, cl, cr), valid}, exact},
1521 position>}(decoded)} :
1522 MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)> ->
1523 Laws.ProductCell<inner, left, right, a, b, output,
1524 Core.TTensor{Storage.Owned{depth, length, tree, Matrix.build_balanced(depth, Matrix.product_splits(depth, inner_n), inner_n, columns_n, length, 0n, cl, cr), valid}, exact},
1525 position>}(cell)}
1526
1527def output_source(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1528 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1529 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1530 +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
1531 -exact: {length == Shape.logical_numel(Shape.dimensions(output)) : Nat},
1532 -a: Core.Tensor<left>, -b: Core.Tensor<right>,
1533 -kept_left: Core.Tensor<left>, -copy_left: Array<F32>, -taken_left: Parallel.Taken<Core.Packed{left, a}, (Core.Packed{left, kept_left}, copy_left)>,
1534 -kept_right: Core.Tensor<right>, -copy_right: Array<F32>, -taken_right: Parallel.Taken<Core.Packed{right, b}, (Core.Packed{right, kept_right}, copy_right)>) ->
1535 Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b}, Matrix.parallel_output(output, U32.to_nat(inner), U32.to_nat(columns), depth, length,
1536 valid, exact, (Core.Packed{left, kept_left}, copy_left), (Core.Packed{right, kept_right}, copy_right))>:
1537 Laws.SourceMatmul{unit => Laws.MatmulSuccess{left, right, Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible},
1538 a, b, kept_left, kept_right,
1539 Core.TTensor{Storage.Owned{depth, length,
1540 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1541 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1542 valid}, exact},
1543 {==}, {==}, {==}, {==}, {==},
1544 Laws.ProductPrefix{
1545 other => {\{Parallel.Fact: p => p} : Parallel.Fact<{Core.checked_observe(left, kept_left, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>}> ->
1546 {Core.checked_observe(left, kept_left, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>}}(
1547 taken_keeps(left, a, kept_left, copy_left, taken_left, other)),
1548 other => {\{Parallel.Fact: p => p} : Parallel.Fact<{Core.checked_observe(right, kept_right, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}> ->
1549 {Core.checked_observe(right, kept_right, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}}(
1550 taken_keeps(right, b, kept_right, copy_right, taken_right, other)),
1551 position => earlier =>
1552 {\{Parallel.Taken: dl => bl => left_reads => left_same =>
1553 {\{Parallel.Taken: dr => br => right_reads => right_same =>
1554 {\{Parallel.Fact: p => p} :
1555 Parallel.Fact<Laws.ProductCell<inner, left, right, a, b, output,
1556 Core.TTensor{Storage.Owned{depth, length,
1557 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1558 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1559 valid}, exact}, position>> ->
1560 Laws.ProductCell<inner, left, right, a, b, output,
1561 Core.TTensor{Storage.Owned{depth, length,
1562 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1563 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1564 valid}, exact}, position>}(
1565 product_cell(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible, depth, length, valid, exact,
1566 a, b, dl, dr, copy_left, copy_right, bl, br, left_reads, right_reads, position, earlier))} :
1567 Parallel.Taken<Core.Packed{right, b}, (Core.Packed{right, kept_right}, copy_right)> ->
1568 Laws.ProductCell<inner, left, right, a, b, output,
1569 Core.TTensor{Storage.Owned{depth, length,
1570 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1571 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1572 valid}, exact}, position>}(taken_right)} :
1573 Parallel.Taken<Core.Packed{left, a}, (Core.Packed{left, kept_left}, copy_left)> ->
1574 Laws.ProductCell<inner, left, right, a, b, output,
1575 Core.TTensor{Storage.Owned{depth, length,
1576 Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1577 Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, copy_left, copy_right),
1578 valid}, exact}, position>}(taken_left)}}}
1579
1580def allocated_source(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
1581 -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1582 -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
1583 a: Core.Tensor<left>, b: Core.Tensor<right>, result: Result<&2, &1, Core.Error, Core.Tensor<output>>) ->
1584 Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b},
1585 Matrix.parallel_allocated(left, right, output, U32.to_nat(inner), U32.to_nat(columns), a, b, result)>:
1586 match result:
1587 case Fail{error}:
1588 Laws.SourceMatmul{unit => Unit{}}
1589 case Done{Core.TTensor{storage, exact}}:
1590 match storage:
1591 case Storage.Empty{}:
1592 Laws.SourceMatmul{unit => Laws.MatmulSuccess{left, right, Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible},
1593 a, b, a, b, Core.TTensor{Storage.Empty{}, exact}, {==}, {==}, {==}, {==}, {==},
1594 Laws.ProductPrefix{other => {==}, other => {==}, position => earlier =>
1595 Empty.absurd(Laws.ProductCell<inner, left, right, a, b, output, Core.TTensor{Storage.Empty{}, exact}, position>,
1596 Arith.lt_zero(position,
1597 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(output)), exact) : {Nat.is_lt(position, _) == True{} : Bool}
1598 earlier))}}}
1599 case Storage.Owned{+depth, +length, array, balanced, valid}:
1600 take_lift(left, a, taken => Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b},
1601 Matrix.parallel_output(output, U32.to_nat(inner), U32.to_nat(columns), depth, length, valid, exact, taken, Elementwise.take(Core.pack(right, b)))>,
1602 kept_left => copy_left => taken_left =>
1603 take_lift(right, b, taken => Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b},
1604 Matrix.parallel_output(output, U32.to_nat(inner), U32.to_nat(columns), depth, length, valid, exact,
1605 (Core.Packed{left, kept_left}, copy_left), taken)>,
1606 kept_right => copy_right => taken_right =>
1607 output_source(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible, depth, length, valid, exact,
1608 a, b, kept_left, copy_left, taken_left, kept_right, copy_right, taken_right)))
1609
1610def multiply_source(+left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Plan<left, right>, a: Core.Tensor<left>, b: Core.Tensor<right>) ->
1611 Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b}, Matrix.parallel_multiply(left, right, plan, a, b)>:
1612 match plan:
1613 case Matrix.Plan{+output, +rows, +inner, +right_inner, +columns, le, re, oe, compatible}:
1614 allocated_source(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible, a, b, Core.new(output, 0.0))
1615
1616def planned_source(+left: Shape.Shape, +right: Shape.Shape, a: Core.Tensor<left>, b: Core.Tensor<right>,
1617 result: Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>) ->
1618 Laws.SourceMatmul<Core.Packed{left, a}, Core.Packed{right, b}, Matrix.parallel_planned(left, right, a, b, result)>:
1619 match result:
1620 case Fail{error}:
1621 Laws.SourceMatmul{unit => Unit{}}
1622 case Done{+plan}:
1623 multiply_source(left, right, plan, a, b)
1624
1625
1626
1627def output_status(+output: Shape.Shape, +inner: Nat, +columns: Nat, +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
1628 -exact: {length == Shape.logical_numel(Shape.dimensions(output)) : Nat},
1629 +left: Shape.Shape, a: Core.Tensor<left>, +right: Shape.Shape, b: Core.Tensor<right>) ->
1630 Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1631 Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, Elementwise.take(Core.pack(left, a)), Elementwise.take(Core.pack(right, b)))>:
1632 take_lift(left, a, taken => Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1633 Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, taken, Elementwise.take(Core.pack(right, b)))>,
1634 kept_left => copy_left => taken_left =>
1635 take_lift(right, b, taken => Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1636 Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, (Core.Packed{left, kept_left}, copy_left), taken)>,
1637 kept_right => copy_right => taken_right => Totality.Status{{==}}))
1638
1639def allocated_status(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: Nat, +columns: Nat,
1640 a: Core.Tensor<left>, b: Core.Tensor<right>, result: Result<&2, &1, Core.Error, Core.Tensor<output>>,
1641 -done: Allocation.TensorDone<output, result>) ->
1642 Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic, Matrix.parallel_allocated(left, right, output, inner, columns, a, b, result)>:
1643 match result:
1644 case Fail{error}:
1645 Totality.Status{{\{Allocation.TensorDone: tensor => exact =>
1646 Empty.absurd({False{} == True{} : Bool}, Shape.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<output>>, Bool,
1647 Result.is_done(&2, &1, Core.Error, Core.Tensor<output>), Done{tensor}, Fail{error}, exact)))} :
1648 Allocation.TensorDone<output, Fail{error}> -> {False{} == True{} : Bool}}(done)}
1649 case Done{Core.TTensor{storage, exact}}:
1650 match storage:
1651 case Storage.Empty{}:
1652 Totality.Status{{==}}
1653 case Storage.Owned{+depth, +length, array, balanced, valid}:
1654 output_status(output, inner, columns, depth, length, valid, exact, left, a, right, b)
1655
1656def multiply_parallel_status(+left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Plan<left, right>, a: Core.Tensor<left>, b: Core.Tensor<right>) ->
1657 Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic, Matrix.parallel_multiply(left, right, plan, a, b)>:
1658 match plan:
1659 case Matrix.Plan{+output, rows, +inner, right_inner, +columns, le, re, oe, compatible}:
1660 allocated_status(left, right, output, U32.to_nat(inner), U32.to_nat(columns), a, b, Core.new(output, 0.0),
1661 AllocationProof.core_new_done(output, 0.0))
1662
1663def planned_parallel_status(+left: Shape.Shape, +right: Shape.Shape, result: Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>,
1664 a: Core.Tensor<left>, b: Core.Tensor<right>, -status: PlanStatus<left, right, result>) ->
1665 Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic, Matrix.parallel_planned(left, right, a, b, result)>:
1666 match result:
1667 case Fail{error}:
1668 Totality.Status{{\{PlanStatus: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
1669 PlanStatus<left, right, Fail{error}> -> {False{} == True{} : Bool}}(status)}
1670 case Done{+plan}:
1671 multiply_parallel_status(left, right, plan, a, b)
1672
1673def Laws.successful_matmul_interpretation(left, right):
1674 Core.Packed{+left_shape, a} = left
1675 Core.Packed{+right_shape, b} = right
1676 planned_source(left_shape, right_shape, a, b, Matrix.plan(left_shape, right_shape))
1677
1678def Laws.matmul_valid_success(left, right, a, b, valid):
1679 Laws.TotalMatmul{
1680 MathProof.success(Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic, Matrix.matmul(Core.Packed{left, a}, Core.Packed{right, b}),
1681 planned_parallel_status(left, right, Matrix.plan(left, right), a, b, plan_status(left, right, valid))),
1682 Laws.successful_matmul_interpretation(Core.Packed{left, a}, Core.Packed{right, b})}