def right_start_spec

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

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
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

420def right_start_spec(+lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat, +rows: Nat, +columns: Nat, +l1: Nat, +l2: Nat, +r1: Nat, +r2: Nat, +o2: Nat,
421  +b1: Nat, +b2: Nat, +row: Nat, +column: Nat,
422  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +column_below: {Nat.is_lt(column, columns) == True{} : Bool},
423  +batch_below: {Nat.is_lt(b2, o2) == True{} : Bool}) ->
424  {Batched.right_start(Laws.layout_of(lo, ro, inner, rows, columns, l1, l2, r1, r2, o2), Laws.cell_position(o2, rows, columns, b1, b2, row, column)) ==
425    Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}:
426  +q = Nat.add(Nat.mul(b1, o2), b2)
427  +r = Nat.add(Nat.mul(row, columns), column)
428  +rc = Nat.mul(rows, columns)
429  +within = MatrixIndex.lt_mul_add(row, rows, column, columns, row_below, column_below)
430  %Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(q, rc), r), rc), q, div_exact(q, rc, r, within)) :
431    {right_from(ro, inner, rows, columns, r1, r2, o2, _, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc)) == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
432  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, rc), r), rc), r, mod_exact(q, rc, r, within)) :
433    {right_from(ro, inner, rows, columns, r1, r2, o2, q, _) == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
434  %Equal.sym(Nat, Nat.div(q, o2), b1, div_exact(b1, o2, b2, batch_below)) :
435    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, _, Nat.mod(q, o2)), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, Nat.mod(r, columns), 0n)) ==
436      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
437  %Equal.sym(Nat, Nat.mod(q, o2), b2, mod_exact(b1, o2, b2, batch_below)) :
438    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, b1, _), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, Nat.mod(r, columns), 0n)) ==
439      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
440  %Equal.sym(Nat, Nat.mod(r, columns), column, mod_exact(row, columns, column, column_below)) :
441    {Nat.add(Nat.mul(Batched.batch_number(r1, r2, b1, b2), Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, _, 0n)) ==
442      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
443  %Equal.sym(Nat, Batched.batch_number(r1, r2, b1, b2), Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)),
444    batch_number_spec(r1, r2, b1, b2)) :
445    {Nat.add(Nat.mul(_, Nat.mul(inner, columns)), Matrix.read_offset(ro, inner, columns, column, 0n)) ==
446      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
447  %Equal.sym(Nat, Matrix.read_offset(ro, inner, columns, column, 0n), Laws.matrix_offset(ro, inner, columns, column, 0n), read_offset_spec(ro, inner, columns, column, 0n)) :
448    {Nat.add(Nat.mul(Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)), Nat.mul(inner, columns)), _) ==
449      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
450  %Equal.sym(Nat, Nat.mul(inner, columns), Nat.mul(columns, inner), Nats.mul_comm(inner, columns)) :
451    {Nat.add(Nat.mul(Nat.add(Nat.mul(Shape.broadcast_index(r1, b1), r2), Shape.broadcast_index(r2, b2)), _), Laws.matrix_offset(ro, inner, columns, column, 0n)) ==
452      Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 0n) : Nat}
453  {==}