1	import Base
2	import ../shape/core.bend as Shape
3	import ../shape/nat_proofs.bend as NatProofs
4	import ../storage/arith.bend as Arith
5	import ./core.bend as Core
6	import ./layout.bend as Layout
7	import ./transforms.bend as Transforms
8	import ./transpose_spec.bend as Transpose
9	import ./elementwise_totality.bend as Totality
10	import ./signed.bend as Signed
11	import ./slice.bend as Slice
12	import ./signed_LAWS.bend as Laws
13	
14	def Laws.signed_first_kept(limit, k):
15	  {==}
16	
17	# n < n is false.
18	def lt_self(+n: Nat) -> {Nat.is_lt(n, n) == False{} : Bool}:
19	  match n:
20	    case 0n:
21	      {==}
22	    case 1n+p:
23	      lt_self(p)
24	
25	# w < w + (k + 1).
26	def lt_past(+w: Nat, +k: Nat) -> {Nat.is_lt(w, Nat.add(w, 1n+k)) == True{} : Bool}:
27	  match w:
28	    case 0n:
29	      {==}
30	    case 1n+p:
31	      lt_past(p, k)
32	
33	# a < 1 + b gives a <= b.
34	def le_from_lt(+a: Nat, +b: Nat, h: {Nat.is_lt(a, 1n+b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
35	  match a:
36	    case 0n:
37	      Arith.le_zero(b)
38	    case 1n+p:
39	      match b:
40	        case 0n:
41	          Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, Arith.lt_zero(p, h))
42	        case 1n+q:
43	          le_from_lt(p, q, h)
44	
45	# a < b gives 1 <= b.
46	def lt_positive(+a: Nat, +b: Nat, h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n, b) == True{} : Bool}:
47	  match b:
48	    case 0n:
49	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, Arith.lt_zero(a, h))
50	    case 1n+q:
51	      Arith.le_zero(q)
52	
53	def add_succ_right(+a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
54	  match a:
55	    case 0n:
56	      {==}
57	    case 1n+p:
58	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 1n+b), 1n+Nat.add(p, b), add_succ_right(p, b))
59	
60	def add_zero_right(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
61	  match a:
62	    case 0n:
63	      {==}
64	    case 1n+p:
65	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero_right(p))
66	
67	def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
68	  match a:
69	    case 0n:
70	      Equal.sym(Nat, Nat.add(b, 0n), b, add_zero_right(b))
71	    case 1n+p:
72	      Equal.trans(Nat, 1n+Nat.add(p, b), 1n+Nat.add(b, p), Nat.add(b, 1n+p),
73	        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)),
74	        Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), add_succ_right(b, p)))
75	
76	# Last{k} in range is limit - 1 - k: the two subtractions borrow nothing.
77	def last_inside(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
78	  {Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
79	  +below = Equal.trans(Bool, Nat.is_lt(U32.to_nat(k), U32.to_nat(limit)), U32.is_lt(k, limit), True{}, Arith.u32_lt(k, limit), inside)
80	  +first = Arith.sub_u32(limit, 1, lt_positive(U32.to_nat(k), U32.to_nat(limit), below))
81	  shifted = Equal.trans(Bool, Nat.is_lt(U32.to_nat(k), 1n+U32.to_nat(U32.sub(limit, 1))), Nat.is_lt(U32.to_nat(k), U32.to_nat(limit)), True{},
82	    Equal.cong(Nat, Bool, x => Nat.is_lt(U32.to_nat(k), x), 1n+U32.to_nat(U32.sub(limit, 1)), U32.to_nat(limit),
83	      Equal.sym(Nat, U32.to_nat(limit), 1n+U32.to_nat(U32.sub(limit, 1)), first)),
84	    below)
85	  second = Arith.sub_u32(U32.sub(limit, 1), k, le_from_lt(U32.to_nat(k), U32.to_nat(U32.sub(limit, 1)), shifted))
86	  Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)),
87	    1n+Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)), U32.to_nat(limit),
88	    add_succ_right(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
89	    Equal.trans(Nat, 1n+Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
90	      1n+Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))), U32.to_nat(limit),
91	      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
92	        Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
93	        add_comm(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k))),
94	      Equal.trans(Nat, 1n+Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
95	        1n+U32.to_nat(U32.sub(limit, 1)), U32.to_nat(limit),
96	        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
97	          U32.to_nat(U32.sub(limit, 1)),
98	          Equal.sym(Nat, U32.to_nat(U32.sub(limit, 1)), Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))), second)),
99	        Equal.sym(Nat, U32.to_nat(limit), 1n+U32.to_nat(U32.sub(limit, 1)), first))))
100	
101	def last_wrapped(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
102	  {Nat.add(U32.to_nat(Signed.wrap(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
103	  %Equal.sym(Bool, U32.is_lt(k, limit), True{}, inside) :
104	    {Nat.add(U32.to_nat(Bool.pick(U32, _, U32.sub(U32.sub(limit, 1), k), limit)), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}
105	  last_inside(limit, k, inside)
106	
107	def Laws.signed_last_inside(limit, k, inside):
108	  last_wrapped(limit, k, inside)
109	
110	def Laws.signed_last_outside(limit, k, outside):
111	  %Equal.sym(Bool, U32.is_lt(k, limit), False{}, outside) :
112	    {Bool.pick(U32, _, U32.sub(U32.sub(limit, 1), k), limit) == limit : U32}
113	  {==}
114	
115	# In range, limit - 1 - k is below limit.
116	def last_below(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
117	  {U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit) == True{} : Bool}:
118	  Equal.trans(Bool, U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit), Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), True{},
119	    Equal.sym(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)), U32.is_lt(U32.sub(U32.sub(limit, 1), k), limit),
120	      Arith.u32_lt(U32.sub(U32.sub(limit, 1), k), limit)),
121	    Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(limit)),
122	      Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k))), True{},
123	      Equal.cong(Nat, Bool, x => Nat.is_lt(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), x), U32.to_nat(limit),
124	        Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)),
125	        Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)), U32.to_nat(limit), last_inside(limit, k, inside))),
126	      lt_past(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k))))
127	
128	# limit is not below itself.
129	def limit_not_below(+limit: U32) -> {U32.is_lt(limit, limit) == False{} : Bool}:
130	  Equal.trans(Bool, U32.is_lt(limit, limit), Nat.is_lt(U32.to_nat(limit), U32.to_nat(limit)), False{},
131	    Equal.sym(Bool, Nat.is_lt(U32.to_nat(limit), U32.to_nat(limit)), U32.is_lt(limit, limit), Arith.u32_lt(limit, limit)),
132	    lt_self(U32.to_nat(limit)))
133	
134	def last_decided(+limit: U32, +k: U32, decision: Shape.BoolCase<U32.is_lt(k, limit)>) ->
135	  {U32.is_lt(Signed.wrap(limit, Signed.Last{k}), limit) == U32.is_lt(k, limit) : Bool}:
136	  match decision:
137	    case Shape.BTrue{+equal}:
138	      %equal : {U32.is_lt(Bool.pick(U32, _, U32.sub(U32.sub(limit, 1), k), limit), limit) == _ : Bool}
139	      last_below(limit, k, Equal.sym(Bool, True{}, U32.is_lt(k, limit), equal))
140	    case Shape.BFalse{equal}:
141	      %equal : {U32.is_lt(Bool.pick(U32, _, U32.sub(U32.sub(limit, 1), k), limit), limit) == _ : Bool}
142	      limit_not_below(limit)
143	
144	def Laws.signed_wrap_inside(limit, position):
145	  match position:
146	    case Signed.First{k}:
147	      {==}
148	    case Signed.Last{+k}:
149	      last_decided(limit, k, Shape.bool_case(U32.is_lt(k, limit)))
150	
151	def Laws.signed_axes_bounded(limit, positions):
152	  match positions:
153	    case Nil{}:
154	      {==}
155	    case +head <> +tail:
156	      %Equal.sym(Bool, U32.is_lt(Signed.wrap(limit, head), limit), Signed.inside(limit, head), Laws.signed_wrap_inside(limit, head)) :
157	        {Bool.and(_, Layout.bounded(Signed.wrap_all(limit, tail), limit)) == Bool.and(Signed.inside(limit, head), Signed.all_inside(limit, tail)) : Bool}
158	      %Equal.sym(Bool, Layout.bounded(Signed.wrap_all(limit, tail), limit), Signed.all_inside(limit, tail), Laws.signed_axes_bounded(limit, tail)) :
159	        {Bool.and(Signed.inside(limit, head), _) == Bool.and(Signed.inside(limit, head), Signed.all_inside(limit, tail)) : Bool}
160	      {==}
161	
162	def Laws.signed_wrap_all_empty(limit):
163	  {==}
164	
165	def Laws.signed_wrap_all_step(limit, head, tail):
166	  {==}
167	
168	def Laws.signed_wrap_each_step(extent, rest, head, tail):
169	  {==}
170	
171	def Laws.signed_wrap_each_end(dimensions):
172	  match dimensions:
173	    case Nil{}:
174	      {==}
175	    case extent <> rest:
176	      {==}
177	
178	def Laws.signed_wrap_each_past_rank(positions):
179	  {==}
180	
181	def Laws.signed_axis_limit(input):
182	  {==}
183	
184	def Laws.signed_permute_wraps(input, source, axes):
185	  {==}
186	
187	def Laws.signed_permute_dynamic_wraps(input, axes):
188	  Core.Packed{+shape, tensor} = input
189	  {==}
190	
191	def Laws.signed_transpose_wraps(input, source, a, b):
192	  {==}
193	
194	def Laws.signed_transpose_dynamic_wraps(input, a, b):
195	  Core.Packed{+shape, tensor} = input
196	  {==}
197	
198	def Laws.signed_read_coordinate_wraps(shape, tensor, coordinates):
199	  {==}
200	
201	def Laws.signed_write_coordinate_wraps(shape, tensor, coordinates, value):
202	  {==}
203	
204	def Laws.signed_read_flat_wraps(shape, tensor, index):
205	  {==}
206	
207	def Laws.signed_write_flat_wraps(shape, tensor, index, value):
208	  {==}
209	
210	def Laws.signed_read_dynamic_wraps(input, index):
211	  Core.Packed{+shape, tensor} = input
212	  {==}
213	
214	def Laws.signed_write_dynamic_wraps(input, index, value):
215	  Core.Packed{+shape, tensor} = input
216	  {==}
217	
218	def Laws.signed_reshape_infers(input, tensor, extents):
219	  {==}
220	
221	def Laws.signed_reshape_dynamic_infers(input, tensor, extents):
222	  {==}
223	
224	def exacts_none(+dimensions: List<&2, U32>) -> {Signed.inferred_count(Laws.exacts(dimensions)) == 0n : Nat}:
225	  match dimensions:
226	    case Nil{}:
227	      {==}
228	    case extent <> +rest:
229	      exacts_none(rest)
230	
231	def exacts_filled(+dimensions: List<&2, U32>, +size: U32) -> {Signed.filled(Laws.exacts(dimensions), size) == dimensions : List<&2, U32>}:
232	  match dimensions:
233	    case Nil{}:
234	      {==}
235	    case +extent <> +rest:
236	      Equal.cong(List<&2, U32>, List<&2, U32>, tail => extent <> tail, Signed.filled(Laws.exacts(rest), size), rest, exacts_filled(rest, size))
237	
238	def Laws.signed_reshape_unsigned(input, tensor, dimensions):
239	  %Equal.sym(Nat, Signed.inferred_count(Laws.exacts(dimensions)), 0n, exacts_none(dimensions)) :
240	    {Signed.reshape_inferred(input, tensor, Signed.inferred_from(Shape.elements(input), Laws.exacts(dimensions), _)) ==
241	      Signed.transformed(Transforms.reshape(input, tensor, dimensions)) : Result<&2, &1, Signed.Error, Core.Dynamic>}
242	  %Equal.sym(List<&2, U32>, Signed.filled(Laws.exacts(dimensions), 0), dimensions, exacts_filled(dimensions, 0)) :
243	    {Signed.reshape_inferred(input, tensor, Done{_}) ==
244	      Signed.transformed(Transforms.reshape(input, tensor, dimensions)) : Result<&2, &1, Signed.Error, Core.Dynamic>}
245	  {==}
246	
247	def Laws.signed_inferred_none(count, extents, none):
248	  %Equal.sym(Nat, Signed.inferred_count(extents), 0n, none) :
249	    {Signed.inferred_from(count, extents, _) == Done{Signed.filled(extents, 0)} : Result<&2, &2, Signed.Error, List<&2, U32>>}
250	  {==}
251	
252	# q * (1 + rest) = count gives count divmod (1 + rest) = (q, 0).
253	def divides(+count: Nat, +rest: Nat, +quotient: Nat, exact: {Nat.mul(quotient, 1n+rest) == count : Nat}) ->
254	  {Nat.divmod(count, 1n+rest) == (quotient, 0n) : Nat & Nat}:
255	  Equal.trans(Nat & Nat, Nat.divmod(count, 1n+rest), Nat.divmod(Nat.add(Nat.mul(quotient, 1n+rest), 0n), 1n+rest), (quotient, 0n),
256	    Equal.cong(Nat, Nat & Nat, x => Nat.divmod(x, 1n+rest), count, Nat.add(Nat.mul(quotient, 1n+rest), 0n),
257	      Equal.sym(Nat, Nat.add(Nat.mul(quotient, 1n+rest), 0n), count,
258	        Equal.trans(Nat, Nat.add(Nat.mul(quotient, 1n+rest), 0n), Nat.mul(quotient, 1n+rest), count,
259	          add_zero_right(Nat.mul(quotient, 1n+rest)), exact))),
260	    Equal.sym(Nat & Nat, (quotient, 0n), Nat.divmod(Nat.add(Nat.mul(quotient, 1n+rest), 0n), 1n+rest),
261	      NatProofs.divmod_exact(quotient, 1n+rest, 0n, Unit{})))
262	
263	# The inference classifies the exact sizes' product against the count
264	# (Signed.capped) instead of forming it. These lemmas give capped as the
265	# classification of exact_product, so the laws stated with exact_product hold.
266	def le_add(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.add(a, b)) == True{} : Bool}:
267	  match a:
268	    case 0n:
269	      Arith.le_zero(b)
270	    case 1n+p:
271	      le_add(p, b)
272	
273	def not_le_add(+a: Nat, +b: Nat, +c: Nat, h: {Nat.is_le(a, c) == False{} : Bool}) ->
274	  {Nat.is_le(Nat.add(a, b), c) == False{} : Bool}:
275	  match a:
276	    case 0n:
277	      Empty.absurd({Nat.is_le(Nat.add(0n, b), c) == False{} : Bool},
278	        Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(0n, c), False{},
279	          Equal.sym(Bool, Nat.is_le(0n, c), True{}, Arith.le_zero(c)), h)))
280	    case 1n+p:
281	      match c:
282	        case 0n:
283	          {==}
284	        case 1n+q:
285	          not_le_add(p, b, q, h)
286	
287	# b < a gives a <= b false.
288	def lt_not_le(+b: Nat, +a: Nat, h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.is_le(a, b) == False{} : Bool}:
289	  match b:
290	    case 0n:
291	      match a:
292	        case 0n:
293	          Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, Arith.clash(h))
294	        case 1n+q:
295	          {==}
296	    case 1n+p:
297	      match a:
298	        case 0n:
299	          Empty.absurd({Nat.is_le(0n, 1n+p) == False{} : Bool}, Arith.clash(h))
300	        case 1n+q:
301	          lt_not_le(p, q, h)
302	
303	# A size past the bound times a nonzero product is past the bound.
304	def past_bound(+bound: Nat, +less: Nat, +rest: Nat, past: {Nat.is_lt(bound, 1n+less) == True{} : Bool}) ->
305	  {Nat.is_le(Nat.mul(1n+less, 1n+rest), bound) == False{} : Bool}:
306	  %NatProofs.mul_comm(1n+rest, 1n+less) : {Nat.is_le(_, bound) == False{} : Bool}
307	  not_le_add(1n+less, Nat.mul(rest, 1n+less), bound, lt_not_le(bound, 1n+less, past))
308	
309	# signed.bend's cap sorts a product as the laws' classified does.
310	def bounded_classified(+product: Nat, +below: Bool) -> {Signed.bounded(product, below) == Laws.classified(product, below) : Signed.Product}:
311	  match below:
312	    case True{}:
313	      {==}
314	    case False{}:
315	      {==}
316	
317	def times_scaled(+bound: Nat, +less: Nat, +rest: Nat, decision: Shape.BoolCase<Nat.is_lt(bound, 1n+less)>) ->
318	  {Signed.scaled(bound, 1n+less, 1n+rest, Nat.is_lt(bound, 1n+less)) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}:
319	  match decision:
320	    case Shape.BTrue{+equal}:
321	      %equal : {Signed.scaled(bound, 1n+less, 1n+rest, _) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
322	      %Equal.sym(Bool, Nat.is_le(Nat.mul(1n+less, 1n+rest), bound), False{},
323	        past_bound(bound, less, rest, Equal.sym(Bool, True{}, Nat.is_lt(bound, 1n+less), equal))) :
324	        {Signed.Beyond{} == Laws.classified(Nat.mul(1n+less, 1n+rest), _) : Signed.Product}
325	      {==}
326	    case Shape.BFalse{equal}:
327	      %equal : {Signed.scaled(bound, 1n+less, 1n+rest, _) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
328	      bounded_classified(Nat.mul(1n+less, 1n+rest), Nat.is_le(Nat.mul(1n+less, 1n+rest), bound))
329	
330	def times_within(+bound: Nat, +less: Nat, +rest: Nat, decision: Shape.BoolCase<Nat.is_le(1n+rest, bound)>) ->
331	  {Signed.times(bound, 1n+less, Laws.classified(1n+rest, Nat.is_le(1n+rest, bound))) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}:
332	  match decision:
333	    case Shape.BTrue{equal}:
334	      %equal : {Signed.times(bound, 1n+less, Laws.classified(1n+rest, _)) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
335	      times_scaled(bound, less, rest, Shape.bool_case(Nat.is_lt(bound, 1n+less)))
336	    case Shape.BFalse{+equal}:
337	      %equal : {Signed.times(bound, 1n+less, Laws.classified(1n+rest, _)) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
338	      %Equal.sym(Bool, Nat.is_le(Nat.mul(1n+less, 1n+rest), bound), False{},
339	        not_le_add(1n+rest, Nat.mul(less, 1n+rest), bound, Equal.sym(Bool, False{}, Nat.is_le(1n+rest, bound), equal))) :
340	        {Signed.Beyond{} == Laws.classified(Nat.mul(1n+less, 1n+rest), _) : Signed.Product}
341	      {==}
342	
343	# times on a classified product classifies the product times the size.
344	def times_classify(+bound: Nat, +size: Nat, +product: Nat) ->
345	  {Signed.times(bound, size, Laws.classify(bound, product)) == Laws.classify(bound, Nat.mul(size, product)) : Signed.Product}:
346	  match size:
347	    case 0n:
348	      {==}
349	    case 1n+less:
350	      match product:
351	        case 0n:
352	          %Equal.sym(Nat, Nat.mul(1n+less, 0n), 0n, NatProofs.mul_zero_right(1n+less)) :
353	            {Signed.ZeroProduct{} == Laws.classify(bound, _) : Signed.Product}
354	          {==}
355	        case 1n+rest:
356	          times_within(bound, less, rest, Shape.bool_case(Nat.is_le(1n+rest, bound)))
357	
358	def capped_classifies(+bound: Nat, +extents: List<&2, Signed.Extent>) ->
359	  {Signed.capped(bound, extents) == Laws.classify(bound, Signed.exact_product(extents)) : Signed.Product}:
360	  match extents:
361	    case Nil{}:
362	      bounded_classified(1n, Nat.is_le(1n, bound))
363	    case Signed.Exact{+size} <> +tail:
364	      %Equal.sym(Signed.Product, Signed.capped(bound, tail), Laws.classify(bound, Signed.exact_product(tail)), capped_classifies(bound, tail)) :
365	        {Signed.times(bound, U32.to_nat(size), _) == Laws.classify(bound, Nat.mul(U32.to_nat(size), Signed.exact_product(tail))) : Signed.Product}
366	      times_classify(bound, U32.to_nat(size), Signed.exact_product(tail))
367	    case Signed.Inferred{} <> +tail:
368	      capped_classifies(bound, tail)
369	
370	def Laws.signed_capped_classifies(bound, extents):
371	  capped_classifies(bound, extents)
372	
373	def is_within(product: Signed.Product) -> Bool:
374	  match product:
375	    case Signed.Within{p}:
376	      True{}
377	    case Signed.ZeroProduct{}:
378	      False{}
379	    case Signed.Beyond{}:
380	      False{}
381	
382	def within_value(product: Signed.Product) -> Nat:
383	  match product:
384	    case Signed.Within{p}:
385	      p
386	    case Signed.ZeroProduct{}:
387	      0n
388	    case Signed.Beyond{}:
389	      0n
390	
391	def within_decided(+bound: Nat, +r: Nat, +p: Nat, +within: {Laws.classified(1n+r, Nat.is_le(1n+r, bound)) == Signed.Within{p} : Signed.Product},
392	  decision: Shape.BoolCase<Nat.is_le(1n+r, bound)>) -> {Nat.is_le(p, bound) == True{} : Bool}:
393	  match decision:
394	    case Shape.BTrue{+equal}:
395	      %Equal.cong(Signed.Product, Nat, within_value, Laws.classified(1n+r, Nat.is_le(1n+r, bound)), Signed.Within{p}, within) :
396	        {Nat.is_le(_, bound) == True{} : Bool}
397	      %equal : {Nat.is_le(within_value(Laws.classified(1n+r, _)), bound) == True{} : Bool}
398	      Equal.sym(Bool, True{}, Nat.is_le(1n+r, bound), equal)
399	    case Shape.BFalse{equal}:
400	      Empty.absurd({Nat.is_le(p, bound) == True{} : Bool},
401	        Arith.clash(Equal.trans(Bool, is_within(Laws.classified(1n+r, False{})), is_within(Laws.classified(1n+r, Nat.is_le(1n+r, bound))), True{},
402	          Equal.cong(Bool, Bool, x => is_within(Laws.classified(1n+r, x)), False{}, Nat.is_le(1n+r, bound), equal),
403	          Equal.cong(Signed.Product, Bool, is_within, Laws.classified(1n+r, Nat.is_le(1n+r, bound)), Signed.Within{p}, within))))
404	
405	def classify_within(+bound: Nat, +product: Nat, +p: Nat, within: {Laws.classify(bound, product) == Signed.Within{p} : Signed.Product}) ->
406	  {Nat.is_le(p, bound) == True{} : Bool}:
407	  match product:
408	    case 0n:
409	      Empty.absurd({Nat.is_le(p, bound) == True{} : Bool},
410	        Arith.clash(Equal.cong(Signed.Product, Bool, is_within, Signed.ZeroProduct{}, Signed.Within{p}, within)))
411	    case 1n+r:
412	      within_decided(bound, r, p, within, Shape.bool_case(Nat.is_le(1n+r, bound)))
413	
414	def Laws.signed_capped_within(bound, extents, product, within):
415	  classify_within(bound, Signed.exact_product(extents), product,
416	    Equal.trans(Signed.Product, Laws.classify(bound, Signed.exact_product(extents)), Signed.capped(bound, extents), Signed.Within{product},
417	      Equal.sym(Signed.Product, Signed.capped(bound, extents), Laws.classify(bound, Signed.exact_product(extents)), capped_classifies(bound, extents)),
418	      within))
419	
420	# The two branches of a single Inferred size with a nonzero product p: p at
421	# most the count divides; p past it leaves an empty input's size 0 and
422	# refuses any other.
423	def size_beyond(+count: Nat, +extents: List<&2, Signed.Extent>, +rest: Nat, +quotient: Nat,
424	  exact: {Nat.mul(quotient, 1n+rest) == count : Nat}, past: {Nat.is_le(1n+rest, count) == False{} : Bool}) ->
425	  {Signed.beyond(count, extents) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}:
426	  match quotient:
427	    case 0n:
428	      %exact : {Signed.beyond(_, extents) == Done{Signed.filled(extents, U32.from_nat(0n))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
429	      {==}
430	    case 1n+q:
431	      Empty.absurd({Signed.beyond(count, extents) == Done{Signed.filled(extents, U32.from_nat(1n+q))} : Result<&2, &2, Signed.Error, List<&2, U32>>},
432	        Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(1n+rest, count), False{},
433	          Equal.trans(Bool, True{}, Nat.is_le(1n+rest, Nat.add(1n+rest, Nat.mul(q, 1n+rest))), Nat.is_le(1n+rest, count),
434	            Equal.sym(Bool, Nat.is_le(1n+rest, Nat.add(1n+rest, Nat.mul(q, 1n+rest))), True{}, le_add(1n+rest, Nat.mul(q, 1n+rest))),
435	            Equal.cong(Nat, Bool, x => Nat.is_le(1n+rest, x), Nat.add(1n+rest, Nat.mul(q, 1n+rest)), count, exact)),
436	          past)))
437	
438	def size_decided(+count: Nat, +extents: List<&2, Signed.Extent>, +rest: Nat, +quotient: Nat,
439	  exact: {Nat.mul(quotient, 1n+rest) == count : Nat}, decision: Shape.BoolCase<Nat.is_le(1n+rest, count)>) ->
440	  {Signed.inferred_one(count, extents, Laws.classified(1n+rest, Nat.is_le(1n+rest, count))) ==
441	    Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}:
442	  match decision:
443	    case Shape.BTrue{equal}:
444	      %equal : {Signed.inferred_one(count, extents, Laws.classified(1n+rest, _)) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
445	      %Equal.sym(Nat & Nat, Nat.divmod(count, 1n+rest), (quotient, 0n), divides(count, rest, quotient, exact)) :
446	        {Signed.divided(extents, _) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
447	      {==}
448	    case Shape.BFalse{+equal}:
449	      %equal : {Signed.inferred_one(count, extents, Laws.classified(1n+rest, _)) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
450	      size_beyond(count, extents, rest, quotient, exact, Equal.sym(Bool, False{}, Nat.is_le(1n+rest, count), equal))
451	
452	def Laws.signed_inferred_size(count, extents, one, rest, product, quotient, exact):
453	  %Equal.sym(Nat, Signed.inferred_count(extents), 1n, one) :
454	    {Signed.inferred_from(count, extents, _) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
455	  %Equal.sym(Signed.Product, Signed.capped(count, extents), Laws.classify(count, Signed.exact_product(extents)), capped_classifies(count, extents)) :
456	    {Signed.inferred_one(count, extents, _) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
457	  %Equal.sym(Nat, Signed.exact_product(extents), 1n+rest, product) :
458	    {Signed.inferred_one(count, extents, Laws.classify(count, _)) == Done{Signed.filled(extents, U32.from_nat(quotient))} : Result<&2, &2, Signed.Error, List<&2, U32>>}
459	  size_decided(count, extents, rest, quotient, exact, Shape.bool_case(Nat.is_le(1n+rest, count)))
460	
461	def pred(n: Nat) -> Nat:
462	  match n:
463	    case 0n:
464	      0n
465	    case 1n+p:
466	      p
467	
468	def succ_not_zero(-x: Nat, equal: {1n+x == 0n : Nat}) -> Empty:
469	  Arith.clash(Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n), 1n+x, 0n, equal))
470	
471	def zero_not_one(equal: {0n == 1n : Nat}) -> Empty:
472	  Arith.clash_true(Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n), 0n, 1n, equal))
473	
474	# With no Inferred size, the filled sizes hold the exact product.
475	def filled_none(+extents: List<&2, Signed.Extent>, +size: U32, none: {Signed.inferred_count(extents) == 0n : Nat}) ->
476	  {Shape.logical_numel(Signed.filled(extents, size)) == Signed.exact_product(extents) : Nat}:
477	  match extents:
478	    case Nil{}:
479	      {==}
480	    case Signed.Exact{+extent} <> +tail:
481	      Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(extent), x), Shape.logical_numel(Signed.filled(tail, size)), Signed.exact_product(tail),
482	        filled_none(tail, size, none))
483	    case Signed.Inferred{} <> +tail:
484	      Empty.absurd({Shape.logical_numel(Signed.filled(Signed.Inferred{} <> tail, size)) == Signed.exact_product(Signed.Inferred{} <> tail) : Nat},
485	        succ_not_zero(Signed.inferred_count(tail), none))
486	
487	# e * (s * p) = s * (e * p).
488	def mul_swap(+e: Nat, +s: Nat, +p: Nat) -> {Nat.mul(e, Nat.mul(s, p)) == Nat.mul(s, Nat.mul(e, p)) : Nat}:
489	  Equal.trans(Nat, Nat.mul(e, Nat.mul(s, p)), Nat.mul(Nat.mul(e, s), p), Nat.mul(s, Nat.mul(e, p)),
490	    Equal.sym(Nat, Nat.mul(Nat.mul(e, s), p), Nat.mul(e, Nat.mul(s, p)), NatProofs.mul_assoc(e, s, p)),
491	    Equal.trans(Nat, Nat.mul(Nat.mul(e, s), p), Nat.mul(Nat.mul(s, e), p), Nat.mul(s, Nat.mul(e, p)),
492	      Equal.cong(Nat, Nat, x => Nat.mul(x, p), Nat.mul(e, s), Nat.mul(s, e), NatProofs.mul_comm(e, s)),
493	      NatProofs.mul_assoc(s, e, p)))
494	
495	def filled_one(+extents: List<&2, Signed.Extent>, one: {Signed.inferred_count(extents) == 1n : Nat}, +size: U32) ->
496	  {Shape.logical_numel(Signed.filled(extents, size)) == Nat.mul(U32.to_nat(size), Signed.exact_product(extents)) : Nat}:
497	  match extents:
498	    case Nil{}:
499	      Empty.absurd({Shape.logical_numel(Signed.filled([], size)) == Nat.mul(U32.to_nat(size), Signed.exact_product([])) : Nat},
500	        zero_not_one(one))
501	    case Signed.Exact{+extent} <> +tail:
502	      Equal.trans(Nat, Nat.mul(U32.to_nat(extent), Shape.logical_numel(Signed.filled(tail, size))),
503	        Nat.mul(U32.to_nat(extent), Nat.mul(U32.to_nat(size), Signed.exact_product(tail))),
504	        Nat.mul(U32.to_nat(size), Nat.mul(U32.to_nat(extent), Signed.exact_product(tail))),
505	        Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(extent), x), Shape.logical_numel(Signed.filled(tail, size)),
506	          Nat.mul(U32.to_nat(size), Signed.exact_product(tail)), filled_one(tail, one, size)),
507	        mul_swap(U32.to_nat(extent), U32.to_nat(size), Signed.exact_product(tail)))
508	    case Signed.Inferred{} <> +tail:
509	      Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(size), x), Shape.logical_numel(Signed.filled(tail, size)), Signed.exact_product(tail),
510	        filled_none(tail, size, Equal.cong(Nat, Nat, pred, 1n+Signed.inferred_count(tail), 1n, one)))
511	
512	def Laws.signed_filled_count(extents, one, size):
513	  filled_one(extents, one, size)
514	
515	# divmod(0, p) is (0, 0): a remainder means a nonempty input.
516	def indivisible_beyond(+count: Nat, +extents: List<&2, Signed.Extent>, +rest: Nat, +quotient: Nat, +remainder: Nat,
517	  split: {Nat.divmod(count, 1n+rest) == (quotient, 1n+remainder) : Nat & Nat}) ->
518	  {Signed.beyond(count, extents) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}:
519	  match count:
520	    case 0n:
521	      Empty.absurd({Signed.beyond(0n, extents) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>},
522	        succ_not_zero(remainder, Equal.sym(Nat, 0n, 1n+remainder,
523	          Equal.cong(Nat & Nat, Nat, pair => Pair.snd(Nat, Nat, pair), (0n, 0n), (quotient, 1n+remainder), split))))
524	    case 1n+c:
525	      {==}
526	
527	def indivisible_decided(+count: Nat, +extents: List<&2, Signed.Extent>, +rest: Nat, +quotient: Nat, +remainder: Nat,
528	  split: {Nat.divmod(count, 1n+rest) == (quotient, 1n+remainder) : Nat & Nat}, decision: Shape.BoolCase<Nat.is_le(1n+rest, count)>) ->
529	  {Signed.inferred_one(count, extents, Laws.classified(1n+rest, Nat.is_le(1n+rest, count))) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}:
530	  match decision:
531	    case Shape.BTrue{equal}:
532	      %equal : {Signed.inferred_one(count, extents, Laws.classified(1n+rest, _)) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
533	      %Equal.sym(Nat & Nat, Nat.divmod(count, 1n+rest), (quotient, 1n+remainder), split) :
534	        {Signed.divided(extents, _) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
535	      {==}
536	    case Shape.BFalse{equal}:
537	      %equal : {Signed.inferred_one(count, extents, Laws.classified(1n+rest, _)) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
538	      indivisible_beyond(count, extents, rest, quotient, remainder, split)
539	
540	def Laws.signed_inferred_indivisible(count, extents, one, rest, product, quotient, remainder, split):
541	  %Equal.sym(Nat, Signed.inferred_count(extents), 1n, one) :
542	    {Signed.inferred_from(count, extents, _) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
543	  %Equal.sym(Signed.Product, Signed.capped(count, extents), Laws.classify(count, Signed.exact_product(extents)), capped_classifies(count, extents)) :
544	    {Signed.inferred_one(count, extents, _) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
545	  %Equal.sym(Nat, Signed.exact_product(extents), 1n+rest, product) :
546	    {Signed.inferred_one(count, extents, Laws.classify(count, _)) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
547	  indivisible_decided(count, extents, rest, quotient, remainder, split, Shape.bool_case(Nat.is_le(1n+rest, count)))
548	
549	def Laws.signed_inferred_ambiguous(extents, one, product):
550	  %Equal.sym(Nat, Signed.inferred_count(extents), 1n, one) :
551	    {Signed.inferred_from(0n, extents, _) == Fail{Signed.AmbiguousInferred{}} : Result<&2, &2, Signed.Error, List<&2, U32>>}
552	  %Equal.sym(Signed.Product, Signed.capped(0n, extents), Laws.classify(0n, Signed.exact_product(extents)), capped_classifies(0n, extents)) :
553	    {Signed.inferred_one(0n, extents, _) == Fail{Signed.AmbiguousInferred{}} : Result<&2, &2, Signed.Error, List<&2, U32>>}
554	  %Equal.sym(Nat, Signed.exact_product(extents), 0n, product) :
555	    {Signed.inferred_one(0n, extents, Laws.classify(0n, _)) == Fail{Signed.AmbiguousInferred{}} : Result<&2, &2, Signed.Error, List<&2, U32>>}
556	  {==}
557	
558	def Laws.signed_inferred_zero_product(count, extents, one, product):
559	  %Equal.sym(Nat, Signed.inferred_count(extents), 1n, one) :
560	    {Signed.inferred_from(1n+count, extents, _) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
561	  %Equal.sym(Signed.Product, Signed.capped(1n+count, extents), Laws.classify(1n+count, Signed.exact_product(extents)), capped_classifies(1n+count, extents)) :
562	    {Signed.inferred_one(1n+count, extents, _) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
563	  %Equal.sym(Nat, Signed.exact_product(extents), 0n, product) :
564	    {Signed.inferred_one(1n+count, extents, Laws.classify(1n+count, _)) == Fail{Signed.count_mismatch()} : Result<&2, &2, Signed.Error, List<&2, U32>>}
565	  {==}
566	
567	def Laws.signed_inferred_repeated(count, extents, more, repeated):
568	  %Equal.sym(Nat, Signed.inferred_count(extents), 2n+more, repeated) :
569	    {Signed.inferred_from(count, extents, _) == Fail{Signed.RepeatedInferred{}} : Result<&2, &2, Signed.Error, List<&2, U32>>}
570	  {==}
571	
572	def Laws.signed_filled_exact(extent, tail, size):
573	  {==}
574	
575	def Laws.signed_filled_inferred(tail, size):
576	  {==}
577	
578	def Laws.signed_error_codes(error):
579	  {==}
580	
581	# Signed slicing.
582	
583	def Laws.signed_bound_first(limit, k):
584	  {==}
585	
586	def bound_inside(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
587	  {Nat.add(U32.to_nat(Signed.bound(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
588	  %Equal.sym(Bool, U32.is_lt(k, limit), True{}, inside) :
589	    {Nat.add(U32.to_nat(Bool.pick(U32, Bool.not(_), 0, Signed.wrap(limit, Signed.Last{k}))), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}
590	  last_wrapped(limit, k, inside)
591	
592	def Laws.signed_bound_last_inside(limit, k, inside):
593	  bound_inside(limit, k, inside)
594	
595	def Laws.signed_bound_last_outside(limit, k, outside):
596	  %Equal.sym(Bool, U32.is_lt(k, limit), False{}, outside) :
597	    {Bool.pick(U32, Bool.not(_), 0, Signed.wrap(limit, Signed.Last{k})) == 0 : U32}
598	  {==}
599	
600	def Laws.signed_slice_bounds(input, dim, start, stop, step):
601	  Core.Packed{+shape, tensor} = input
602	  {==}
603	
604	def Laws.signed_select_wraps(input, dim, index):
605	  Core.Packed{+shape, tensor} = input
606	  {==}
607	
608	def Laws.signed_narrow_first(input, dim, k, length):
609	  Core.Packed{+shape, tensor} = input
610	  {==}
611	
612	def Laws.signed_narrow_last_inside(input, dim, k, length, inside):
613	  Core.Packed{+shape, tensor} = input
614	  %Equal.sym(Bool, U32.is_lt(k, Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim))), True{}, inside) :
615	    {Signed.narrow_started(shape, tensor, Signed.wrap(Shape.rank(shape), dim), Signed.wrap(Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim)), Signed.Last{k}), length, Bool.not(_)) ==
616	      Slice.narrow(Core.Packed{shape, tensor}, Signed.wrap(Shape.rank(shape), dim), Signed.wrap(Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim)), Signed.Last{k}), length) : Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}
617	  {==}
618	
619	def Laws.signed_narrow_before(input, dim, k, length, in_rank, before):
620	  Core.Packed{+shape, tensor} = input
621	  %Equal.sym(Bool, U32.is_lt(k, Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim))), False{}, before) :
622	    {Signed.narrow_started(shape, tensor, Signed.wrap(Shape.rank(shape), dim), Signed.wrap(Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim)), Signed.Last{k}), length, Bool.not(_)) ==
623	      (Core.Packed{shape, tensor}, Fail{Slice.OutOfRange{}}) : Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}
624	  %Equal.sym(Bool, Nat.is_lt(U32.to_nat(Signed.wrap(Shape.rank(shape), dim)), Shape.rank_dimensions(Shape.dimensions(shape))), True{}, in_rank) :
625	    {Signed.narrow_before(Core.Packed{shape, tensor}, Slice.refused(_, Nat.is_lt(0n, U32.to_nat(1)))) ==
626	      (Core.Packed{shape, tensor}, Fail{Slice.OutOfRange{}}) : Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}
627	  {==}
628	
629	def Laws.signed_narrow_before_axis(input, dim, k, length, past_rank, before):
630	  Core.Packed{+shape, tensor} = input
631	  %Equal.sym(Bool, U32.is_lt(k, Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim))), False{}, before) :
632	    {Signed.narrow_started(shape, tensor, Signed.wrap(Shape.rank(shape), dim), Signed.wrap(Signed.extent(Shape.dimensions(shape), Signed.wrap(Shape.rank(shape), dim)), Signed.Last{k}), length, Bool.not(_)) ==
633	      (Core.Packed{shape, tensor}, Fail{Slice.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}
634	  %Equal.sym(Bool, Nat.is_lt(U32.to_nat(Signed.wrap(Shape.rank(shape), dim)), Shape.rank_dimensions(Shape.dimensions(shape))), False{}, past_rank) :
635	    {Signed.narrow_before(Core.Packed{shape, tensor}, Slice.refused(_, Nat.is_lt(0n, U32.to_nat(1)))) ==
636	      (Core.Packed{shape, tensor}, Fail{Slice.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}
637	  {==}