LAWS.ProductWith: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as LAWS Lines 282-311 of bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&start_line=282&end_line=311 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/core.bend as Core import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle 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/replayed.bend as Replayed # What the transport form of product_replayed asks of P, as MatmulWith asks # it of a matmul: P holds for both inputs, replayed with any histories that # keep their words, next to the output, of the plan's shape, replayed over # +0.0 with any history whose cell (row, column) holds the total # `product_ordered` states. def ProductWith(+lo: Matrix.Order, +ro: Matrix.Order, +left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Product, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type) -> Type: @+left_kept: List<&2, StorageLaws.Op> -> @left_words: {words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @+output_ops: List<&2, StorageLaws.Op> -> @cells: (@+row: Nat -> @row_below: {Nat.is_lt(row, product_rows(lo, ro, left, right, plan)) == True{} : Bool} -> @+column: Nat -> @column_below: {Nat.is_lt(column, product_columns(lo, ro, left, right, plan)) == True{} : Bool} -> {Replayed.value(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops, U32.from_nat(Nat.add(Nat.mul(row, product_columns(lo, ro, left, right, plan)), column))) == DotFold.dot_fold(product_factors(row, column, lo, ro, product_inner(lo, ro, left, right, plan), product_rows(lo, ro, left, right, plan), product_columns(lo, ro, left, right, plan), left, left_fill, left_ops, right, right_fill, right_ops, product_inner(lo, ro, left, right, plan)), 0.0) : F32}) -> @-output_fits: {Lifecycle.logical_length(Replayed.storage(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops)) == Shape.logical_numel(Shape.dimensions(Matrix.product_shape(lo, ro, left, right, plan))) : Nat} -> P(Done{(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_fits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_fits}}, Core.Packed{Matrix.product_shape(lo, ro, left, right, plan), Core.TTensor{Replayed.storage(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops), output_fits}})}) Uses (30): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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=Result 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=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel 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/tensor/contracts/LAWS.bend&name=product_columns https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=product_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=product_inner https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=product_rows https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage 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/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend&name=dot_fold https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Order https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Product https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=product_shape