1 import Base 2 import ../shape/core.bend as Shape 3 import ./core.bend as Core 4 import ./core_PROOF.bend as CoreProof 5 import ./lifecycle.bend as Lifecycle 6 import ./matmul.bend as Matrix 7 import ./matmul_LAWS.bend as Laws 8 import ./dot_fold.bend as DotFold 9 import ./math_totality.bend as Totality 10 import ./reduction_PROOF.bend as MathProof 11 import ./word_conversion.bend as Conversion 12 import ./allocation_PROOF.bend as AllocationProof 13 import ./allocation_spec.bend as Allocation 14 import ./transform_PROOF.bend as TransformProof 15 import ./transform_LAWS.bend as TransformLaws 16 import ./transform_totality.bend as TransformTotality 17 import ../shape/LAWS.bend as ShapeLaws 18 import ../shape/PROOF.bend as ShapeProof 19 import ../shape/boundary_proofs.bend as Boundary 20 import ../shape/coordinate_proofs.bend as Coordinates 21 import ../shape/nat_proofs.bend as Nats 22 import ../storage/arith.bend as Arith 23 import ../storage/main.bend as Storage 24 import ../storage/model.bend as Model 25 import ../storage/refinement.bend as Refinement 26 import ../storage/route.bend as Route 27 import ../storage/certificates.bend as Certificates 28 import ./elementwise.bend as Elementwise 29 import ./elementwise_totality.bend as ElementwiseTotality 30 import ./elementwise_parallel_proof.bend as Parallel 31 import ./matmul_parallel_proof.bend as MatmulParallel 32 import ./matrix_index_proof.bend as MatrixIndex 33 34 type CoordinateRead<-shape: Shape.Shape, -original: Core.Tensor, -coordinates: List<&2, U32>> is Type: 35 CoordinateRead{tensor: Core.Tensor, result: Result<&2, &2, Core.Error, F32>, 36 exact: {(tensor, result) == Core.read_coordinate(shape, original, coordinates) : Core.Tensor & 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 40 def coordinate_flat(+shape: Shape.Shape, -original: Core.Tensor, -coordinates: List<&2, U32>, +index: Shape.FlatIndex, 41 same: {Done{index} == Shape.flatten_checked(shape, coordinates) : Result<&2, &2, Shape.Error, Shape.FlatIndex>}, 42 certificate: Core.Read, 43 -source: Core.SourceRead, 44 -retention: Core.SourceReadKeeps) -> CoordinateRead: 45 Core.Read{tensor, +result, +exact} = certificate 46 CoordinateRead{tensor, result, 47 %same : {(tensor, result) == Core.read_coordinate_result(shape, original, _) : Core.Tensor & Result<&2, &2, Core.Error, F32>} 48 exact, 49 unit => 50 prove : @source: Core.SourceRead -> 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 & 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 -> 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 & 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 68 def coordinate_decided(+shape: Shape.Shape, tensor: Core.Tensor, -coordinates: List<&2, U32>, 69 result: Result<&2, &2, Shape.Error, Shape.FlatIndex>, 70 same: {result == Shape.flatten_checked(shape, coordinates) : Result<&2, &2, Shape.Error, Shape.FlatIndex>}) -> CoordinateRead: 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 & 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 82 def coordinate_certificate(+shape: Shape.Shape, tensor: Core.Tensor, +coordinates: List<&2, U32>) -> CoordinateRead: 83 coordinate_decided(shape, tensor, coordinates, Shape.flatten_checked(shape, coordinates), {==}) 84 85 def coordinate_keeps_result(+shape: Shape.Shape, -original: Core.Tensor, -tensor: Core.Tensor, 86 result: Result<&2, &2, Shape.Error, Shape.FlatIndex>, 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 95 def coordinate_keeps(+shape: Shape.Shape, -original: Core.Tensor, -tensor: Core.Tensor, +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 100 def logical_dot_original(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 101 -ra: Core.Tensor, -rb: Core.Tensor, +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 126 def dot_extend(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 127 -ra: Core.Tensor, -rb: Core.Tensor, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32, +rv: F32, 128 result: Result<&2, &1, Matrix.Error, Core.Tensor & Core.Tensor & 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 149 def right_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 150 -ra: Core.Tensor, rb: Core.Tensor, result: Result<&2, &2, Core.Error, F32>, 151 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32, 152 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> 153 Laws.SourceDot, 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 -> 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 176 def right_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, -ra: Core.Tensor, 177 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, +lv: F32, 178 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> 179 Laws.SourceDot, 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) -> 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 198 def left_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, b: Core.Tensor, 199 ra: Core.Tensor, result: Result<&2, &2, Core.Error, F32>, 200 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, 201 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> 202 Laws.SourceDot, 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 216 def left_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 217 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, 218 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> 219 Laws.SourceDot, 220 -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, 221 certificate: CoordinateRead) -> 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 236 def dot_decision(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, a: Core.Tensor, -b: Core.Tensor, 237 +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, 238 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> 239 Laws.SourceDot, 240 decision: Shape.BoolCase) -> 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 250 def 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 259 def 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 266 def 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 270 def 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 278 def 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 290 def 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 301 def 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 309 def frame_cell(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 310 +output: Shape.Shape, -before: Core.Tensor, -after: Core.Tensor, +cursor: Nat, +position: Nat, 311 cell: Laws.ProductCell, 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: 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 329 def prefix_cell_case(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 330 +output: Shape.Shape, -out: Core.Tensor, +cursor: Nat, +position: Nat, 331 current: Laws.ProductCell, 332 prior: @+position: Nat -> @earlier: {Nat.is_lt(position, cursor) == True{} : Bool} -> Laws.ProductCell, 333 split: Either<&2, &2, {Nat.is_lt(position, cursor) == True{} : Bool}, {position == cursor : Nat}>) -> Laws.ProductCell: 334 match split: 335 case Inl{earlier}: 336 prior(position, earlier) 337 case Inr{equal}: 338 %Equal.sym(Nat, position, cursor, equal) : Laws.ProductCell 339 current 340 341 def advance_prefix(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 342 -before_a: Core.Tensor, -before_b: Core.Tensor, -after_a: Core.Tensor, -after_b: Core.Tensor, 343 +output: Shape.Shape, -before: Core.Tensor, -after: Core.Tensor, +cursor: Nat, 344 +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate, +value: F32, 345 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 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, 349 dot: Laws.DotMeaning, 350 update: Core.CheckedUpdateMeaning(output, before, U32.from_nat(cursor), value, (after, Done{Unit{}}))) -> 351 Laws.ProductPrefix: 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 367 def 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 374 def 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 381 def write_product_pair(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 382 -a: Core.Tensor, -b: Core.Tensor, -before_a: Core.Tensor, -before_b: Core.Tensor, 383 -ra: Core.Tensor, -rb: Core.Tensor, -before: Core.Tensor, out: Core.Tensor, result: Result<&2, &2, Core.Error, Unit>, 384 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate, +value: F32, 385 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 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, 389 -dot: Laws.DotMeaning, 390 -update: Core.CheckedUpdateMeaning(output, before, U32.from_nat(cursor), value, (out, result)), 391 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 392 @prefix: Laws.ProductPrefix -> 393 Laws.SourceProduct) -> 395 Laws.SourceProduct 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 -> 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 412 def write_product_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 413 -a: Core.Tensor, -b: Core.Tensor, -before_a: Core.Tensor, -before_b: Core.Tensor, 414 -ra: Core.Tensor, -rb: Core.Tensor, -before: Core.Tensor, 415 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate, +value: F32, 416 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 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, 420 -dot: Laws.DotMeaning, 421 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 422 @prefix: Laws.ProductPrefix -> 423 Laws.SourceProduct, 425 certificate: Core.Write, -model: Core.CheckedUpdateModel) -> 426 Laws.SourceProduct 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 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 -> 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 & 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 450 def product_dot_result(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 451 -a: Core.Tensor, -b: Core.Tensor, -before_a: Core.Tensor, -before_b: Core.Tensor, -out: Core.Tensor, 452 +cursor: Nat, +row: U32, +column: U32, +coordinate: Shape.CheckedCoordinate, 453 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 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, 457 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 458 @prefix: Laws.ProductPrefix -> 459 Laws.SourceProduct, 461 result: Result<&2, &1, Matrix.Error, Core.Tensor & Core.Tensor & F32>, 462 -source: Laws.SourceDot) -> 463 Laws.SourceProduct 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 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 -> 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 & Core.Tensor & 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 491 def product_coordinates_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 492 -a: Core.Tensor, -b: Core.Tensor, before_a: Core.Tensor, before_b: Core.Tensor, -out: Core.Tensor, 493 +cursor: Nat, +coordinate: Shape.CheckedCoordinate, 494 -decoded: {Shape.unflatten_checked(output, U32.from_nat(cursor)) == Done{coordinate} : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 495 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, 496 -prefix: Laws.ProductPrefix, 497 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 498 @prefix: Laws.ProductPrefix -> 499 Laws.SourceProduct, 501 values: List<&2, U32>, -same: {values == Shape.coordinate_values(output, coordinate) : List<&2, U32>}) -> 502 Laws.SourceProduct 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 517 def product_unflattened_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 518 -a: Core.Tensor, -b: Core.Tensor, before_a: Core.Tensor, before_b: Core.Tensor, -out: Core.Tensor, +cursor: Nat, 519 -word_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}, 520 -prefix: Laws.ProductPrefix, 521 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 522 @prefix: Laws.ProductPrefix -> 523 Laws.SourceProduct, 525 result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>, 526 -same: {result == Shape.unflatten_checked(output, U32.from_nat(cursor)) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}) -> 527 Laws.SourceProduct 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>, Done{coordinate}, Shape.unflatten_checked(output, U32.from_nat(cursor)), same), 535 word_exact, prefix, rec, Shape.coordinate_values(output, coordinate), {==}) 536 537 def product_decision_proof(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 538 -a: Core.Tensor, -b: Core.Tensor, before_a: Core.Tensor, before_b: Core.Tensor, -out: Core.Tensor, +cursor: Nat, 539 -prefix: Laws.ProductPrefix, 540 -rec: @ra: Core.Tensor -> @rb: Core.Tensor -> @out: Core.Tensor -> 541 @prefix: Laws.ProductPrefix -> 542 Laws.SourceProduct, 544 decision: Shape.BoolCase) -> 545 Laws.SourceProduct 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 555 def 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 564 def empty_prefix(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, 565 +output: Shape.Shape, -out: Core.Tensor) -> Laws.ProductPrefix: 566 Laws.ProductPrefix{other => {==}, other => {==}, position => earlier => 567 Empty.absurd(Laws.ProductCell, no_earlier_zero(position, earlier))} 568 569 def created_product(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, 570 a: Core.Tensor, b: Core.Tensor, result: Result<&2, &1, Core.Error, Core.Tensor>) -> 571 Laws.SourceProduct: 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 -> 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 591 def 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 596 def zero_fold(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, +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 604 type ZeroCell<-output: Shape.Shape, -out: Core.Tensor, -position: Nat> is Data: 605 ZeroCell{-observed: {Core.checked_observe(output, out, U32.from_nat(position)) == Some{0.0} : Maybe<&2, F32>}} 606 607 def zero_cell(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, +output: Shape.Shape, 608 -out: Core.Tensor, +position: Nat, cell: Laws.ProductCell<0, left, right, a, b, output, out, position>) -> ZeroCell: 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 614 def zero_prefix(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, +output: Shape.Shape, 615 -ra: Core.Tensor, -rb: Core.Tensor, -out: Core.Tensor, +end: Nat, 616 prefix: Laws.ProductPrefix<0, left, right, a, b, output, ra, rb, out, end>) -> Laws.ZeroPrefix: 617 Laws.ProductPrefix{left_kept, right_kept, cells} = prefix 618 Laws.ZeroPrefix{position => earlier => 619 claim : @certificate: ZeroCell -> {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 623 def zero_result(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor, -b: Core.Tensor, +output: Shape.Shape, -end: Nat, 624 result: Result<&2, &1, Matrix.Error, Core.Tensor & Core.Tensor & Core.Tensor>, 625 -source: Laws.SourceProduct<0, left, right, a, b, output, end, result>) -> Laws.ZeroResult: 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 & Core.Tensor & Core.Tensor>)> -> 634 Laws.ZeroPrefix = \{Laws.SourceProduct: meaning => 635 zero_prefix(left, right, a, b, output, ra, rb, out, end, meaning(Unit{}))} 636 prove(source)} 637 638 def 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 643 def Laws.zero_inner_dot(left, right, a, b, row, column): 644 {==} 645 646 def Laws.output_dimensions(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible): 647 oe 648 649 def 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 659 def 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 670 def 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 681 def flatten_done(+shape: Shape.Shape, +coordinates: List<&2, U32>, 682 result: Result<&2, &2, Shape.Error, Shape.FlatIndex>, 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>}) -> 685 {Result.is_done(&2, &2, Shape.Error, Shape.FlatIndex, 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>, 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 700 def coordinate_read_result_status(+shape: Shape.Shape, result: Result<&2, &2, Shape.Error, Shape.FlatIndex>, 701 tensor: Core.Tensor, -successful: {Result.is_done(&2, &2, Shape.Error, Shape.FlatIndex, result) == True{} : Bool}) -> 702 Totality.ReadStatus: 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 -> 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 713 def coordinate_read_status(+shape: Shape.Shape, tensor: Core.Tensor, +coordinates: List<&2, U32>, 714 -fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(coordinates))) -> 715 Totality.ReadStatus: 716 coordinate_read_result_status(shape, Shape.flatten_checked(shape, coordinates), tensor, 717 flatten_done(shape, coordinates, Shape.flatten_checked(shape, coordinates), fits, {==})) 718 719 def 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 & Result<&2, &2, Core.Error, F32>, a: Core.Tensor, 722 -successful: {TransformTotality.read_succeeded(right, pair) == True{} : Bool}, 723 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @+value: F32 -> Totality.Status & Core.Tensor & F32, 724 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) -> 725 Totality.Status & Core.Tensor & 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 & Core.Tensor & 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 & Core.Tensor & 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 739 def dot_left_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, 740 pair: Core.Tensor & Result<&2, &2, Core.Error, F32>, b: Core.Tensor, 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 -> @b: Core.Tensor -> @+value: F32 -> Totality.Status & Core.Tensor & F32, 744 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) -> 745 Totality.Status & Core.Tensor & 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 -> 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 758 def dot_decision_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, 759 decision: Shape.BoolCase, a: Core.Tensor, b: Core.Tensor, 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 -> @b: Core.Tensor -> @+value: F32 -> Totality.Status & Core.Tensor & F32, 764 Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>) -> 765 Totality.Status & Core.Tensor & 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 -> 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 776 def 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, b: Core.Tensor, 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 & Core.Tensor & 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 802 def product_write_status(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +inner: U32, +columns: U32, +cursor: Nat, 803 pair: Core.Tensor & Result<&2, &2, Core.Error, Unit>, a: Core.Tensor, b: Core.Tensor, 804 -successful: {TransformTotality.write_succeeded(output, pair) == True{} : Bool}, 805 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @out: Core.Tensor -> 806 Totality.Status & Core.Tensor & Core.Tensor, 807 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 808 Totality.Status & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 819 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)) == True{} : Bool}}(rec(a, b, out))} 820 821 def 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 & Core.Tensor & F32>, out: Core.Tensor, 823 -status: Totality.Status & Core.Tensor & F32, result>, 824 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}, 825 -rec: @a: Core.Tensor -> @b: Core.Tensor -> @out: Core.Tensor -> 826 Totality.Status & Core.Tensor & Core.Tensor, 827 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 828 Totality.Status & Core.Tensor & Core.Tensor, 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 & Core.Tensor & 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 -> 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 841 def 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 848 def 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, b: Core.Tensor, out: Core.Tensor, 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 -> @b: Core.Tensor -> @out: Core.Tensor -> 856 Totality.Status & Core.Tensor & Core.Tensor, 857 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 858 Totality.Status & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 897 def 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, 899 a: Core.Tensor, b: Core.Tensor, out: Core.Tensor, 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 -> @b: Core.Tensor -> @out: Core.Tensor -> 904 Totality.Status & Core.Tensor & Core.Tensor, 905 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 906 Totality.Status & Core.Tensor & Core.Tensor, 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 913 def unflatten_done(+shape: Shape.Shape, +index: U32, result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>, 914 same: {result == Shape.unflatten_checked(shape, index) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate>}, 915 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> 916 {Result.is_done(&2, &2, Shape.Error, Shape.CheckedCoordinate, 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>, 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 930 def 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>, a: Core.Tensor, b: Core.Tensor, out: Core.Tensor, 933 -successful: {Result.is_done(&2, &2, Shape.Error, Shape.CheckedCoordinate, 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 -> @b: Core.Tensor -> @out: Core.Tensor -> 938 Totality.Status & Core.Tensor & Core.Tensor, 939 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 940 Totality.Status & Core.Tensor & Core.Tensor, 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 948 def 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, a: Core.Tensor, b: Core.Tensor, out: Core.Tensor, 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 -> @b: Core.Tensor -> @out: Core.Tensor -> 956 Totality.Status & Core.Tensor & Core.Tensor, 957 Matrix.natural_product_loop(fuel, left, right, output, inner, columns, a, b, out, 1n+cursor)>) -> 958 Totality.Status & Core.Tensor & Core.Tensor, 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 970 def 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, b: Core.Tensor, out: Core.Tensor, 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 & Core.Tensor & Core.Tensor, 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 989 def 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>, a: Core.Tensor, b: Core.Tensor, 991 -done: Allocation.TensorDone, 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 & Core.Tensor & Core.Tensor, 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>, Bool, 999 Result.is_done(&2, &1, Core.Error, Core.Tensor), Done{tensor}, Fail{error}, exact)))} : 1000 Allocation.TensorDone -> {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 1006 def multiply_status(+left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Plan, a: Core.Tensor