law tn_reads_transpose

bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_LAWS.bend:470

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/dot_fold.bend as DotFold
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts

470# matmul_tn likewise: for a left operand of dimensions [inner, rows], the
471# pairs of a product of two `Swapped` operands (`matmul_tn`), left[k, row] and
472# right[k, column], are the pairs `left_transposed_factors` reads through
473# `permute_source` on left^T, the pairs `tensor_matmul_vjp_values` states for
474# x^T @ g.
475law tn_reads_transpose:
476  for +row: Nat
477  for +column: Nat
478  for +columns: Nat
479  for +left: Shape.Shape
480  for +left_fill: F32
481  for +left_ops: List<&2, StorageLaws.Op>
482  for +right: Shape.Shape
483  for +right_fill: F32
484  for +right_ops: List<&2, StorageLaws.Op>
485  for +inner: U32
486  for +rows: U32
487  for matrix: {Shape.dimensions(left) == [inner, rows] : List<&2, U32>}
488  for row_below: {Nat.is_lt(row, U32.to_nat(rows)) == True{} : Bool}
489  for +count: Nat
490  for room: {Nat.is_le(count, U32.to_nat(inner)) == True{} : Bool}
491  {Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, U32.to_nat(inner), U32.to_nat(rows), columns,
492    left, left_fill, left_ops, right, right_fill, right_ops, count) ==
493    left_transposed_factors(row, column, U32.to_nat(inner), columns, left, left_fill, left_ops, swapped(left),
494      right, right_fill, right_ops, count) : List<&2, DotFold.Factors>}