MatmulPROOF.product_cell: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 1454-1525 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=1454&end_line=1525

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/lifecycle.bend as Lifecycle
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/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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/storage/route.bend as Route
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

# Below the output's element count, the parallel build writes the cell the
# sequential interpretation names.
def product_cell(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
  -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
  -exact: {length == Shape.logical_numel(Shape.dimensions(output)) : Nat},
  -a: Core.Tensor<left>, -b: Core.Tensor<right>, -dl: Nat, -dr: Nat, -cl: Array<F32>, -cr: Array<F32>,
  -bl: Model.Balanced(F32, dl, cl), -br: Model.Balanced(F32, dr, cr),
  -left_reads: Parallel.SourceReads(Core.Packed{left, a}, dl, cl), -right_reads: Parallel.SourceReads(Core.Packed{right, b}, dr, cr),
  +position: Nat, -earlier: {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
  Parallel.Fact<Laws.ProductCell<inner, left, right, a, b, output,
    Core.TTensor{Storage.Owned{depth, length,
      Matrix.build(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, cl, cr),
      Matrix.build_balanced(depth, Matrix.product_splits(depth, U32.to_nat(inner)), U32.to_nat(inner), U32.to_nat(columns), length, 0n, cl, cr),
      valid}, exact}, position>>:
  -inner_n = U32.to_nat(inner)
  -columns_n = U32.to_nat(columns)
  -row = Matrix.row_of(columns_n, position)
  -column = Matrix.column_of(columns_n, position)
  -index = U32.from_nat(position)
  -extents = Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(output), [rows, columns], oe)
  -fit = MatrixIndex.position_fits(output, U32.to_nat(rows), columns_n, extents, position, earlier)
  -row_below = Arith.and_left(Nat.is_lt(row, U32.to_nat(rows)), Bool.and(Nat.is_lt(column, columns_n), True{}), fit)
  -column_below = Arith.and_left(Nat.is_lt(column, columns_n), True{},
    Arith.and_right(Nat.is_lt(row, U32.to_nat(rows)), Bool.and(Nat.is_lt(column, columns_n), True{}), fit))
  -word_exact = MatrixIndex.word_exact(position, output, earlier)
  -below = MatrixIndex.lt_bound(position, Shape.logical_numel(Shape.dimensions(output)), length,
    Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(output)), exact), earlier)
  -inside = MatrixIndex.lt_same(U32.to_nat(index), position, length, word_exact, below)
  -tree = Matrix.build(depth, Matrix.product_splits(depth, inner_n), inner_n, columns_n, length, 0n, cl, cr)
  -path = Refinement.route(depth, index)
  -cells = {\{Parallel.Fact: p => p} :
    Parallel.Fact<MatmulParallel.Cells(depth, dl, dr, cl, cr, inner_n, columns_n, length, 0n, tree)> ->
    MatmulParallel.Cells(depth, dl, dr, cl, cr, inner_n, columns_n, length, 0n, tree)}(
      MatmulParallel.build_cells(depth, Matrix.product_splits(depth, inner_n), dl, dr, cl, cr, inner_n, columns_n, length, 0n, cl, cr, {==}, {==}, bl, br))
  -position_eq = Equal.trans(Nat, Nat.add(Model.offset(depth, path), 0n), U32.to_nat(index), position,
    Parallel.output_position(depth, length, index, valid, inside), word_exact)
  -at = {\{Parallel.Fact: p => p} :
    Parallel.Fact<MatmulParallel.CellIs(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path))> ->
    MatmulParallel.CellIs(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path))}(
      MatmulParallel.cell_shift(dl, dr, cl, cr, inner_n, columns_n, length, Nat.add(Model.offset(depth, path), 0n), position,
        Model.observe(F32, depth, tree, path), position_eq, cells(path)))
  -cell = {\{Parallel.Fact: p => p} :
    Parallel.Fact<MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)>> ->
    MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)>}(
      MatmulParallel.cell_below(dl, dr, cl, cr, inner_n, columns_n, length, position, Model.observe(F32, depth, tree, path), below, at))
  -matched = Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), Route.index_complete(depth, length, index, valid, inside))
  -decoded = {\{Parallel.Fact: p => p} : Parallel.Fact<Decoded<output, index, U32.from_nat(row), U32.from_nat(column)>> ->
    Decoded<output, index, U32.from_nat(row), U32.from_nat(column)>}(
      decoded_of(output, index, U32.from_nat(row), U32.from_nat(column), Shape.unflatten_checked(output, index), {==},
        MatrixIndex.unflatten_at(output, U32.to_nat(rows), columns_n, extents, position, earlier)))
  Parallel.Fact{{\{MatmulParallel.CellAt: word => observed => values => logical => fold =>
    {\{Decoded: coordinate => found => coordinates =>
      Laws.ProductCell{U32.from_nat(row), U32.from_nat(column), coordinate, found, coordinates, word_exact, values,
        {\{Parallel.Fact: p => p} :
          Parallel.Fact<Laws.LogicalDot(inner_n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, values)> ->
          Laws.LogicalDot(inner_n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 0n, values)}(
          logical_dot(inner_n, 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, 0n, {==}, values, logical)),
        word, fold, matched,
        Equal.trans(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, tree, index, Nat.is_lt(U32.to_nat(index), length)),
          Model.observe(F32, depth, tree, path), Some{word},
          Parallel.observe_allowed_equal(depth, length, tree, index, Nat.is_lt(U32.to_nat(index), length), inside, matched), observed)}} :
      Decoded<output, index, U32.from_nat(row), U32.from_nat(column)> ->
      Laws.ProductCell<inner, left, right, a, b, output,
        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},
        position>}(decoded)} :
    MatmulParallel.CellAt<dl, dr, cl, cr, inner_n, columns_n, position, Model.observe(F32, depth, tree, path)> ->
    Laws.ProductCell<inner, left, right, a, b, output,
      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},
      position>}(cell)}

Uses (58):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=index_matches
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=index_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=SourceReads
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=observe_allowed_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=output_position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=observe_allowed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=build_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=column_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=product_splits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=row_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=LogicalDot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=ProductCell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=Decoded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=decoded_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=logical_dot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=CellAt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=CellIs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=build_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=cell_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=cell_shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=lt_bound
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=lt_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=position_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=unflatten_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=word_exact