MatmulParallelProof.run_next: 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 516-549 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=516&end_line=549 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/tensor/matrix_index_proof.bend as MatrixIndex import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build import bendtorch-core@0.1.0.0/src/storage/api.bend as Api # A term with more after it: the reads hold the replayed words, the offsets # step to the next term's, and the run goes on from its reads of the same # copies. def run_next(+rest: 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, +rsrc: Source, +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>}, +below: {Nat.is_lt(cursor, span) == True{} : Bool}, pl: Array & F32, +exact_l: {pl == Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)) : Array & F32}, pr: Array & F32, +exact_r: {pr == Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)) : Array & F32}, next: DotIs(1n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, 1n+cursor, F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Matrix.product_run(rest, 1n, columns, Nat.add(Nat.mul(row, span), 1n+cursor), Nat.add(Nat.mul(1n+cursor, columns), column), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, 1n+cursor)), Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, 1n+cursor))))) -> DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(1n+rest, 1n, columns, Nat.add(Nat.mul(row, span), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)): (la, x) = pl (ra, y) = pr +ex = source_read(left, left_fill, left_ops, ha, dl, fa, lsrc, Matrix.left_index(span, row, cursor), index_inside(left, Nat.add(Nat.mul(row, span), cursor), MatrixIndex.left_below(rows, span, row, row_below, left, left_extents, cursor, below)), (la, x), exact_l) +ey = source_read(right, right_fill, right_ops, hb, dr, fb, rsrc, Matrix.right_index(columns, column, cursor), index_inside(right, Nat.add(Nat.mul(cursor, columns), column), MatrixIndex.right_below(span, columns, column, column_below, right, right_extents, cursor, below)), (ra, y), exact_r) +el = Build.got_kept(dl, ha, fa, Matrix.left_index(span, row, cursor), (la, x), exact_l) +er = Build.got_kept(dr, hb, fb, Matrix.right_index(columns, column, cursor), (ra, y), exact_r) %Equal.sym(F32, x, Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), ex) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(_, y)), Array.get(F32, la, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)))))) %Equal.sym(F32, y, Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)), ey) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), _)), Array.get(F32, la, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)))))) %Equal.sym(Array, la, Api.arr(ha, dl, fa), el) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, _, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, ra, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)))))) %Equal.sym(Array, ra, Api.arr(hb, dr, fb), er) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)))), Array.get(F32, _, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)))))) %Equal.sym(Nat, Nat.add(1n, Nat.add(Nat.mul(row, span), cursor)), Nat.add(Nat.mul(row, span), 1n+cursor), MatrixIndex.stepped_left(span, row, cursor)) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, _, Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(_)), Array.get(F32, Api.arr(hb, dr, fb), U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)))))) %Equal.sym(Nat, Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), Nat.add(Nat.mul(1n+cursor, columns), column), MatrixIndex.stepped_right(columns, column, cursor)) : DotIs(2n+rest, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, Matrix.product_run(rest, 1n, columns, Nat.add(Nat.mul(row, span), 1n+cursor), _, F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)))), Array.get(F32, Api.arr(ha, dl, fa), U32.from_nat(Nat.add(Nat.mul(row, span), 1n+cursor))), Array.get(F32, Api.arr(hb, dr, fb), U32.from_nat(_)))) next Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array 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=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.mul 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=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_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=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/binary_build_proof.bend&name=got_kept 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=index_inside https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=source_read https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value 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=product_run https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=right_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=left_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=right_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=stepped_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=stepped_right