def logical_dot

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1381

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend as MatmulParallel
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex

1381# The factor pairs the parallel build reads from its copies are the
1382# coordinate reads of the inputs the copies came from.
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)}