src/tensor/contracts/LAWS.bend

bendtorch-core@0.1.0.0 · 386 lines · 23 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
4import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
5import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
6import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
7import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
8import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
9import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
10import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
11import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
12import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as Broadcast
13import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_records.bend as Records
14import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
15import bendtorch-core@0.1.0.0/src/tensor/contracts/dot.bend as Dot
16import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_records.bend as FoldRecords
17
18# Replayed tensors. `Core.new(shape, fill)` is the replayed tensor with an
19# empty history, `Core.from_values` the one that writes each value once in
20# order, and a read on either returns the replayed word.
21
22law new_replayed:
23  for +shape: Shape.Shape
24  for +fill: F32
25  for -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type
26  for h: @-fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, Nil{})) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
27    P(Done{Core.TTensor{Replayed.storage(shape, fill, Nil{}), fits}})
28  P(Core.new(shape, fill))
29
30law from_values_replayed:
31  for +shape: Shape.Shape
32  for +values: List<&2, F32>
33  for counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
34  for -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type
35  for h: @-fits: {Lifecycle.logical_length(Replayed.storage(shape, 0.0, FromValues.writes(values, 0n))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
36    P(Done{Core.TTensor{Replayed.storage(shape, 0.0, FromValues.writes(values, 0n)), fits}})
37  P(Core.from_values(shape, values))
38
39law replayed_read:
40  for +shape: Shape.Shape
41  for +fill: F32
42  for +ops: List<&2, StorageLaws.Op>
43  for -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
44  for +index: U32
45  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
46  {Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, index)) ==
47    Some{Replayed.value(shape, fill, ops, index)} : Maybe<&2, F32>}
48
49# Pointwise family, broadcast instance: for every operation, broadcast plan
50# and pair of replayed inputs, the output has the plan's output dimensions,
51# holds `Elementwise.scalar(operation, left[ia(i)], right[ib(i)])` at every
52# in-bounds index i, and both returned inputs keep every word.
53law broadcast_pointwise:
54  for +operation: Elementwise.Operation
55  for +plan: Shape.BroadcastPlan
56  for +left_fill: F32
57  for +left_ops: List<&2, StorageLaws.Op>
58  for -left_fits: {Lifecycle.logical_length(Replayed.storage(Shape.left_shape(plan), left_fill, left_ops)) ==
59    Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))) : Nat}
60  for +right_fill: F32
61  for +right_ops: List<&2, StorageLaws.Op>
62  for -right_fits: {Lifecycle.logical_length(Replayed.storage(Shape.right_shape(plan), right_fill, right_ops)) ==
63    Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat}
64  Records.PointwiseContract<Shape.output_shape(plan), Shape.left_shape(plan), Shape.right_shape(plan),
65    index => Broadcast.cell(operation, plan, left_fill, left_ops, right_fill, right_ops, index),
66    other => Replayed.value(Shape.left_shape(plan), left_fill, left_ops, other),
67    other => Replayed.value(Shape.right_shape(plan), right_fill, right_ops, other),
68    Broadcast.binary(operation, plan,
69      Core.Packed{Shape.left_shape(plan), Core.TTensor{Replayed.storage(Shape.left_shape(plan), left_fill, left_ops), left_fits}},
70      Core.Packed{Shape.right_shape(plan), Core.TTensor{Replayed.storage(Shape.right_shape(plan), right_fill, right_ops), right_fits}})>
71
72def words(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) -> List<&2, F32>:
73  match count:
74    case 0n:
75      Nil{}
76    case 1n+previous:
77      List.append(&2, F32, words(shape, fill, ops, previous), [Replayed.value(shape, fill, ops, U32.from_nat(previous))])
78
79# Ordered-fold family, sum instance: the sum of a replayed input succeeds with
80# `Reduction.sequential_sum` of all its words in index order, starting at
81# +0.0, and the returned input keeps every word.
82law sum_ordered:
83  for +shape: Shape.Shape
84  for +fill: F32
85  for +ops: List<&2, StorageLaws.Op>
86  for -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
87  FoldRecords.FoldContract<shape, Reduction.sequential_sum(words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), 0.0),
88    other => Replayed.value(shape, fill, ops, other),
89    Sum.sum(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>
90
91# The first `count` factor pairs of output cell (row, column) of a row-major
92# product of a rows x inner and an inner x columns matrix, in increasing k:
93# left[row, k] and right[k, column].
94def factors(+row: Nat, +column: Nat, +inner: Nat, +columns: Nat,
95  +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
96  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat) -> List<&2, DotFold.Factors>:
97  match count:
98    case 0n:
99      Nil{}
100    case 1n+previous:
101      List.append(&2, DotFold.Factors,
102        factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous),
103        [DotFold.Factors{Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, inner), previous))),
104          Replayed.value(right, right_fill, right_ops, U32.from_nat(Nat.add(Nat.mul(previous, columns), column)))}])
105
106# Ordered-fold family, dot instance: for every in-bounds output cell of a
107# product of a rows x inner and an inner x columns replayed matrix, the dot
108# product succeeds with `DotFold.dot_fold` of the cell's factor pairs in
109# increasing k, starting at +0.0, and both returned inputs keep every word.
110law dot_ordered:
111  for +rows: Nat
112  for +inner: Nat
113  for +columns: Nat
114  for +row: Nat
115  for row_below: {Nat.is_lt(row, rows) == True{} : Bool}
116  for +column: Nat
117  for column_below: {Nat.is_lt(column, columns) == True{} : Bool}
118  for +left: Shape.Shape
119  for left_extents: {Shape.extents(left) == [rows, inner] : List<&2, Nat>}
120  for +left_fill: F32
121  for +left_ops: List<&2, StorageLaws.Op>
122  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
123  for +right: Shape.Shape
124  for right_extents: {Shape.extents(right) == [inner, columns] : List<&2, Nat>}
125  for +right_fill: F32
126  for +right_ops: List<&2, StorageLaws.Op>
127  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
128  FoldRecords.PairFoldContract<left, right,
129    DotFold.dot_fold(factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, inner), 0.0),
130    other => Replayed.value(left, left_fill, left_ops, other),
131    other => Replayed.value(right, right_fill, right_ops, other),
132    Dot.dot(Dot.Cell{row, column, inner, columns},
133      Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
134      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>
135
136def matrix_rows(-left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Plan<left, right>) -> Nat:
137  Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
138  U32.to_nat(rows)
139
140def matrix_inner(-left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Plan<left, right>) -> Nat:
141  Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
142  U32.to_nat(inner)
143
144def matrix_columns(-left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Plan<left, right>) -> Nat:
145  Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
146  U32.to_nat(columns)
147
148# Ordered-fold family, matmul: for every plan of a product of two replayed
149# matrices, matmul succeeds with a rows x columns output whose cell
150# (row, column) holds `DotFold.dot_fold` of the cell's factor pairs in
151# increasing k, starting at +0.0, the value `dot_ordered` states for
152# `Dot.dot`, and both returned inputs keep every word.
153law matmul_ordered:
154  for +left: Shape.Shape
155  for +right: Shape.Shape
156  for +plan: Matrix.Plan<left, right>
157  for planned: {Matrix.plan(left, right) == Done{plan} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}
158  for +left_fill: F32
159  for +left_ops: List<&2, StorageLaws.Op>
160  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
161  for +right_fill: F32
162  for +right_ops: List<&2, StorageLaws.Op>
163  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
164  FoldRecords.MatmulContract<left, right, matrix_rows(left, right, plan), matrix_columns(left, right, plan),
165    row => column => DotFold.dot_fold(factors(row, column, matrix_inner(left, right, plan), matrix_columns(left, right, plan),
166      left, left_fill, left_ops, right, right_fill, right_ops, matrix_inner(left, right, plan)), 0.0),
167    other => Replayed.value(left, left_fill, left_ops, other),
168    other => Replayed.value(right, right_fill, right_ops, other),
169    Matrix.matmul(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
170      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>
171
172# What the transport form of matmul_replayed asks of P: P holds for both
173# inputs, replayed with any histories that keep their words, next to the
174# output, of the plan's shape, replayed over +0.0 with any history whose cell
175# (row, column) holds the total `matmul_ordered` states.
176def MatmulWith(+left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Plan<left, right>,
177  +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
178  -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type) -> Type:
179  @+left_kept: List<&2, StorageLaws.Op> ->
180  @left_words: {words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) ==
181    words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} ->
182  @-left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
183  @+right_kept: List<&2, StorageLaws.Op> ->
184  @right_words: {words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) ==
185    words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} ->
186  @-right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
187  @+output_ops: List<&2, StorageLaws.Op> ->
188  @cells: (@+row: Nat -> @row_below: {Nat.is_lt(row, matrix_rows(left, right, plan)) == True{} : Bool} ->
189    @+column: Nat -> @column_below: {Nat.is_lt(column, matrix_columns(left, right, plan)) == True{} : Bool} ->
190    {Replayed.value(Matrix.output_shape(left, right, plan), 0.0, output_ops,
191      U32.from_nat(Nat.add(Nat.mul(row, matrix_columns(left, right, plan)), column))) ==
192      DotFold.dot_fold(factors(row, column, matrix_inner(left, right, plan), matrix_columns(left, right, plan),
193        left, left_fill, left_ops, right, right_fill, right_ops, matrix_inner(left, right, plan)), 0.0) : F32}) ->
194  @-output_fits: {Lifecycle.logical_length(Replayed.storage(Matrix.output_shape(left, right, plan), 0.0, output_ops)) ==
195    Shape.logical_numel(Shape.dimensions(Matrix.output_shape(left, right, plan))) : Nat} ->
196    P(Done{(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_fits}},
197      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_fits}},
198      Core.Packed{Matrix.output_shape(left, right, plan),
199        Core.TTensor{Replayed.storage(Matrix.output_shape(left, right, plan), 0.0, output_ops), output_fits}})})
200
201# matmul_ordered in the transport form of broadcast_to_replayed: for every P,
202# if P holds for every result that hands back both inputs with their words and
203# gives an output of the plan's shape whose cells hold the ordered totals,
204# then P holds for the product. The output is a replayed tensor, so a later
205# family law applies to it.
206law matmul_replayed:
207  for +left: Shape.Shape
208  for +right: Shape.Shape
209  for +plan: Matrix.Plan<left, right>
210  for planned: {Matrix.plan(left, right) == Done{plan} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}
211  for +left_fill: F32
212  for +left_ops: List<&2, StorageLaws.Op>
213  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
214  for +right_fill: F32
215  for +right_ops: List<&2, StorageLaws.Op>
216  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
217  for -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type
218  for h: MatmulWith(left, right, plan, left_fill, left_ops, right_fill, right_ops, P)
219  P(Matrix.matmul(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
220    Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}}))
221
222# The first `count` factor pairs of output cell (row, column) of a rows x
223# columns product whose operands are laid out in orders lo and ro, in
224# increasing k: the left word at `Matrix.read_offset(lo, inner, rows, row,
225# k)` and the right word at `Matrix.read_offset(ro, inner, columns, column,
226# k)`. For two `Kept` operands (`matmul_nt`) they are left[row, k] and
227# right[column, k]; for two `Swapped` ones (`matmul_tn`) left[k, row] and
228# right[k, column].
229def product_factors(+row: Nat, +column: Nat, +lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat, +rows: Nat, +columns: Nat,
230  +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
231  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat) -> List<&2, DotFold.Factors>:
232  match count:
233    case 0n:
234      Nil{}
235    case 1n+previous:
236      List.append(&2, DotFold.Factors,
237        product_factors(row, column, lo, ro, inner, rows, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous),
238        [DotFold.Factors{Replayed.value(left, left_fill, left_ops, Matrix.read_index(lo, inner, rows, row, previous)),
239          Replayed.value(right, right_fill, right_ops, Matrix.read_index(ro, inner, columns, column, previous))}])
240
241def product_rows(-lo: Matrix.Order, -ro: Matrix.Order, -left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Product<lo, ro, left, right>) -> Nat:
242  Matrix.Product{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
243  U32.to_nat(rows)
244
245def product_inner(-lo: Matrix.Order, -ro: Matrix.Order, -left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Product<lo, ro, left, right>) -> Nat:
246  Matrix.Product{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
247  U32.to_nat(inner)
248
249def product_columns(-lo: Matrix.Order, -ro: Matrix.Order, -left: Shape.Shape, -right: Shape.Shape, plan: Matrix.Product<lo, ro, left, right>) -> Nat:
250  Matrix.Product{output, rows, inner, right_inner, columns, le, re, oe, compatible} = plan
251  U32.to_nat(columns)
252
253# Ordered-fold family, product read in place: for every plan of a product of
254# two replayed rank-2 operands laid out in orders lo and ro (`matmul_nt` is
255# `Kept`, `Kept`; `matmul_tn` is `Swapped`, `Swapped`), the product succeeds
256# with a rows x columns output whose cell (row, column) holds
257# `DotFold.dot_fold` of the cell's factor pairs `product_factors` in
258# increasing k, starting at +0.0, and both returned inputs keep every word.
259# No transpose is built: each factor is read at its operand's own index.
260law product_ordered:
261  for +lo: Matrix.Order
262  for +ro: Matrix.Order
263  for +left: Shape.Shape
264  for +right: Shape.Shape
265  for +plan: Matrix.Product<lo, ro, left, right>
266  for planned: {Matrix.product_plan(lo, ro, left, right) == Done{plan} : Result<&2, &2, Matrix.Error, Matrix.Product<lo, ro, left, right>>}
267  for +left_fill: F32
268  for +left_ops: List<&2, StorageLaws.Op>
269  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
270  for +right_fill: F32
271  for +right_ops: List<&2, StorageLaws.Op>
272  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
273  FoldRecords.MatmulContract<left, right, product_rows(lo, ro, left, right, plan), product_columns(lo, ro, left, right, plan),
274    row => column => DotFold.dot_fold(product_factors(row, column, lo, ro, product_inner(lo, ro, left, right, plan),
275      product_rows(lo, ro, left, right, plan), product_columns(lo, ro, left, right, plan),
276      left, left_fill, left_ops, right, right_fill, right_ops, product_inner(lo, ro, left, right, plan)), 0.0),
277    other => Replayed.value(left, left_fill, left_ops, other),
278    other => Replayed.value(right, right_fill, right_ops, other),
279    Matrix.product(lo, ro, Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
280      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>
281
282# What the transport form of product_replayed asks of P, as MatmulWith asks
283# it of a matmul: P holds for both inputs, replayed with any histories that
284# keep their words, next to the output, of the plan's shape, replayed over
285# +0.0 with any history whose cell (row, column) holds the total
286# `product_ordered` states.
287def ProductWith(+lo: Matrix.Order, +ro: Matrix.Order, +left: Shape.Shape, +right: Shape.Shape, +plan: Matrix.Product<lo, ro, left, right>,
288  +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
289  -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type) -> Type:
290  @+left_kept: List<&2, StorageLaws.Op> ->
291  @left_words: {words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) ==
292    words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} ->
293  @-left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
294  @+right_kept: List<&2, StorageLaws.Op> ->
295  @right_words: {words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) ==
296    words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} ->
297  @-right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
298  @+output_ops: List<&2, StorageLaws.Op> ->
299  @cells: (@+row: Nat -> @row_below: {Nat.is_lt(row, product_rows(lo, ro, left, right, plan)) == True{} : Bool} ->
300    @+column: Nat -> @column_below: {Nat.is_lt(column, product_columns(lo, ro, left, right, plan)) == True{} : Bool} ->
301    {Replayed.value(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops,
302      U32.from_nat(Nat.add(Nat.mul(row, product_columns(lo, ro, left, right, plan)), column))) ==
303      DotFold.dot_fold(product_factors(row, column, lo, ro, product_inner(lo, ro, left, right, plan),
304        product_rows(lo, ro, left, right, plan), product_columns(lo, ro, left, right, plan),
305        left, left_fill, left_ops, right, right_fill, right_ops, product_inner(lo, ro, left, right, plan)), 0.0) : F32}) ->
306  @-output_fits: {Lifecycle.logical_length(Replayed.storage(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops)) ==
307    Shape.logical_numel(Shape.dimensions(Matrix.product_shape(lo, ro, left, right, plan))) : Nat} ->
308    P(Done{(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_fits}},
309      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_fits}},
310      Core.Packed{Matrix.product_shape(lo, ro, left, right, plan),
311        Core.TTensor{Replayed.storage(Matrix.product_shape(lo, ro, left, right, plan), 0.0, output_ops), output_fits}})})
312
313# product_ordered in transport form, as matmul_replayed states matmul: for
314# every P, if P holds for every result that hands back both inputs with
315# their words and gives an output of the plan's shape whose cells hold the
316# ordered totals, then P holds for the product. The output is a replayed
317# tensor, so a later family law applies to it.
318law product_replayed:
319  for +lo: Matrix.Order
320  for +ro: Matrix.Order
321  for +left: Shape.Shape
322  for +right: Shape.Shape
323  for +plan: Matrix.Product<lo, ro, left, right>
324  for planned: {Matrix.product_plan(lo, ro, left, right) == Done{plan} : Result<&2, &2, Matrix.Error, Matrix.Product<lo, ro, left, right>>}
325  for +left_fill: F32
326  for +left_ops: List<&2, StorageLaws.Op>
327  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
328  for +right_fill: F32
329  for +right_ops: List<&2, StorageLaws.Op>
330  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
331  for -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type
332  for h: ProductWith(lo, ro, left, right, plan, left_fill, left_ops, right_fill, right_ops, P)
333  P(Matrix.product(lo, ro, Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
334    Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}}))
335
336# `matmul_nt(x, W)` is the product of two `Kept` operands, x @ W^T: cell
337# (row, column) folds x[row, k] * W[column, k], the words of x at
338# row * inner + k and of W at column * inner + k, in increasing k from +0.0.
339law matmul_nt_ordered:
340  for +left: Shape.Shape
341  for +right: Shape.Shape
342  for +plan: Matrix.Product<Matrix.Kept{}, Matrix.Kept{}, left, right>
343  for planned: {Matrix.product_plan(Matrix.Kept{}, Matrix.Kept{}, left, right) == Done{plan} :
344    Result<&2, &2, Matrix.Error, Matrix.Product<Matrix.Kept{}, Matrix.Kept{}, left, right>>}
345  for +left_fill: F32
346  for +left_ops: List<&2, StorageLaws.Op>
347  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
348  for +right_fill: F32
349  for +right_ops: List<&2, StorageLaws.Op>
350  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
351  FoldRecords.MatmulContract<left, right, product_rows(Matrix.Kept{}, Matrix.Kept{}, left, right, plan),
352    product_columns(Matrix.Kept{}, Matrix.Kept{}, left, right, plan),
353    row => column => DotFold.dot_fold(product_factors(row, column, Matrix.Kept{}, Matrix.Kept{},
354      product_inner(Matrix.Kept{}, Matrix.Kept{}, left, right, plan), product_rows(Matrix.Kept{}, Matrix.Kept{}, left, right, plan),
355      product_columns(Matrix.Kept{}, Matrix.Kept{}, left, right, plan),
356      left, left_fill, left_ops, right, right_fill, right_ops, product_inner(Matrix.Kept{}, Matrix.Kept{}, left, right, plan)), 0.0),
357    other => Replayed.value(left, left_fill, left_ops, other),
358    other => Replayed.value(right, right_fill, right_ops, other),
359    Matrix.matmul_nt(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
360      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>
361
362# `matmul_tn(g, x)` is the product of two `Swapped` operands, g^T @ x: cell
363# (row, column) folds g[k, row] * x[k, column], the words of g at
364# k * rows + row and of x at k * columns + column, in increasing k from +0.0.
365law matmul_tn_ordered:
366  for +left: Shape.Shape
367  for +right: Shape.Shape
368  for +plan: Matrix.Product<Matrix.Swapped{}, Matrix.Swapped{}, left, right>
369  for planned: {Matrix.product_plan(Matrix.Swapped{}, Matrix.Swapped{}, left, right) == Done{plan} :
370    Result<&2, &2, Matrix.Error, Matrix.Product<Matrix.Swapped{}, Matrix.Swapped{}, left, right>>}
371  for +left_fill: F32
372  for +left_ops: List<&2, StorageLaws.Op>
373  for -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}
374  for +right_fill: F32
375  for +right_ops: List<&2, StorageLaws.Op>
376  for -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}
377  FoldRecords.MatmulContract<left, right, product_rows(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan),
378    product_columns(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan),
379    row => column => DotFold.dot_fold(product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{},
380      product_inner(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan), product_rows(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan),
381      product_columns(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan),
382      left, left_fill, left_ops, right, right_fill, right_ops, product_inner(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan)), 0.0),
383    other => Replayed.value(left, left_fill, left_ops, other),
384    other => Replayed.value(right, right_fill, right_ops, other),
385    Matrix.matmul_tn(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
386      Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>