def left_start_spec

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:388

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex

388def left_start_spec(+lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat, +rows: Nat, +columns: Nat, +l1: Nat, +l2: Nat, +r1: Nat, +r2: Nat, +o2: Nat,
389  +b1: Nat, +b2: Nat, +row: Nat, +column: Nat,
390  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +column_below: {Nat.is_lt(column, columns) == True{} : Bool},
391  +batch_below: {Nat.is_lt(b2, o2) == True{} : Bool}) ->
392  {Batched.left_start(Laws.layout_of(lo, ro, inner, rows, columns, l1, l2, r1, r2, o2), Laws.cell_position(o2, rows, columns, b1, b2, row, column)) ==
393    Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}:
394  +q = Nat.add(Nat.mul(b1, o2), b2)
395  +r = Nat.add(Nat.mul(row, columns), column)
396  +rc = Nat.mul(rows, columns)
397  +within = MatrixIndex.lt_mul_add(row, rows, column, columns, row_below, column_below)
398  %Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(q, rc), r), rc), q, div_exact(q, rc, r, within)) :
399    {left_from(lo, inner, rows, columns, l1, l2, o2, _, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc)) == Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
400  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc), r, mod_exact(q, rc, r, within)) :
401    {left_from(lo, inner, rows, columns, l1, l2, o2, q, _) == Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
402  %Equal.sym(Nat, Nat.div(q, o2), b1, div_exact(b1, o2, b2, batch_below)) :
403    {Nat.add(Nat.mul(Batched.batch_number(l1, l2, _, Nat.mod(q, o2)), Nat.mul(rows, inner)), Matrix.read_offset(lo, inner, rows, Nat.div(r, columns), 0n)) ==
404      Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
405  %Equal.sym(Nat, Nat.mod(q, o2), b2, mod_exact(b1, o2, b2, batch_below)) :
406    {Nat.add(Nat.mul(Batched.batch_number(l1, l2, b1, _), Nat.mul(rows, inner)), Matrix.read_offset(lo, inner, rows, Nat.div(r, columns), 0n)) ==
407      Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
408  %Equal.sym(Nat, Nat.div(r, columns), row, div_exact(row, columns, column, column_below)) :
409    {Nat.add(Nat.mul(Batched.batch_number(l1, l2, b1, b2), Nat.mul(rows, inner)), Matrix.read_offset(lo, inner, rows, _, 0n)) ==
410      Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
411  %Equal.sym(Nat, Batched.batch_number(l1, l2, b1, b2), Nat.add(Nat.mul(Shape.broadcast_index(l1, b1), l2), Shape.broadcast_index(l2, b2)),
412    batch_number_spec(l1, l2, b1, b2)) :
413    {Nat.add(Nat.mul(_, Nat.mul(rows, inner)), Matrix.read_offset(lo, inner, rows, row, 0n)) ==
414      Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
415  %Equal.sym(Nat, Matrix.read_offset(lo, inner, rows, row, 0n), Laws.matrix_offset(lo, inner, rows, row, 0n), read_offset_spec(lo, inner, rows, row, 0n)) :
416    {Nat.add(Nat.mul(Nat.add(Nat.mul(Shape.broadcast_index(l1, b1), l2), Shape.broadcast_index(l2, b2)), Nat.mul(rows, inner)), _) ==
417      Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 0n) : Nat}
418  {==}