MatmulParallelProof.dot_eq: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as MatmulParallelProof
Lines 568-578 of bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&start_line=568&end_line=578

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

# Cell (row, column) of the build over the two copies folds the replayed
# words in increasing k and hands both copies back.
def dot_eq(+fuel: Nat, +span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>, +rows: Nat, +row: Nat, +column: Nat, +cursor: Nat, +accumulator: F32,
  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>}, +steps: {Nat.add(cursor, fuel) == span : Nat}) ->
  DotIs(fuel, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.cell_dot(fuel, span, columns, row, column, cursor, accumulator, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))):
  match fuel:
    case 0n:
      {==}
    case 1n+rest:
      run_eq(rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, lsrc, rsrc, rows, row, column, cursor, accumulator, row_below, left_extents, column_below, right_extents, steps, Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)), {==}, Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)), {==})

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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=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=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=DotIs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=Source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=run_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=cell_dot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=left_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=right_index