def run_last

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_parallel_proof.bend:487

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

487# The last term of a run: both reads hold the replayed words, and both
488# copies come back.
489def run_last(+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,
490  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
491  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
492  +below: {Nat.is_lt(cursor, span) == True{} : Bool},
493  pl: Array<F32> & F32, +exact_l: {pl == Array.get(F32, Api.arr(ha, dl, fa), Matrix.left_index(span, row, cursor)) : Array<F32> & F32},
494  pr: Array<F32> & F32, +exact_r: {pr == Array.get(F32, Api.arr(hb, dr, fb), Matrix.right_index(columns, column, cursor)) : Array<F32> & F32}) ->
495  DotIs(1n, 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(0n, 1n, columns, Nat.add(Nat.mul(row, span), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)):
496  (la, x) = pl
497  (ra, y) = pr
498  +ex = source_read(left, left_fill, left_ops, ha, dl, fa, lsrc, Matrix.left_index(span, row, cursor),
499    index_inside(left, Nat.add(Nat.mul(row, span), cursor), MatrixIndex.left_below(rows, span, row, row_below, left, left_extents, cursor, below)),
500    (la, x), exact_l)
501  +ey = source_read(right, right_fill, right_ops, hb, dr, fb, rsrc, Matrix.right_index(columns, column, cursor),
502    index_inside(right, Nat.add(Nat.mul(cursor, columns), column), MatrixIndex.right_below(span, columns, column, column_below, right, right_extents, cursor, below)),
503    (ra, y), exact_r)
504  +el = Build.got_kept(dl, ha, fa, Matrix.left_index(span, row, cursor), (la, x), exact_l)
505  +er = Build.got_kept(dr, hb, fb, Matrix.right_index(columns, column, cursor), (ra, y), exact_r)
506  %Equal.sym(F32, x, Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), ex) :
507    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(_, y)), (la, ra)))
508  %Equal.sym(F32, y, Replayed.value(right, right_fill, right_ops, Matrix.right_index(columns, column, cursor)), ey) :
509    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (F32.add(accumulator, F32.mul(Replayed.value(left, left_fill, left_ops, Matrix.left_index(span, row, cursor)), _)), (la, ra)))
510  %Equal.sym(Array<F32>, la, Api.arr(ha, dl, fa), el) :
511    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (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)))), (_, ra)))
512  %Equal.sym(Array<F32>, ra, Api.arr(hb, dr, fb), er) :
513    DotIs(1n, span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, row, column, cursor, accumulator, (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)))), (Api.arr(ha, dl, fa), _)))
514  {==}