1	import Base
2	import ../../shape/core.bend as Shape
3	import ../../storage/LAWS.bend as StorageLaws
4	import ../core.bend as Core
5	import ../lifecycle.bend as Lifecycle
6	import ../elementwise.bend as Elementwise
7	import ../from_values_contract.bend as FromValues
8	import ../reduction.bend as Reduction
9	import ../matmul.bend as Matrix
10	import ../dot_fold.bend as DotFold
11	import ./replayed.bend as Replayed
12	import ./broadcast.bend as Broadcast
13	import ./pointwise_records.bend as Records
14	import ./sum.bend as Sum
15	import ./dot.bend as Dot
16	import ./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	
22	law 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	
30	law 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	
39	law 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.
53	law 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	
72	def 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.
82	law 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].
94	def 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.
110	law 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	
136	def 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	
140	def 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	
144	def 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.
153	law 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.
176	def 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.
206	law 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].
229	def 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	
241	def 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	
245	def 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	
249	def 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.
260	law 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.
287	def 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.
318	law 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.
339	law 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.
365	law 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}})>