src/tensor/signed_PROOF.bend

bendtorch-core@0.1.0.0 · 637 lines · 39 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs
4import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
5import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
6import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
7import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
8import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
9import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
10import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
11import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
12import bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend as Laws
13
14def Laws.signed_first_kept(limit, k):
15  {==}
16
17# n < n is false.
18def 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).
26def 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.
34def 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.
46def 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
53def 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
60def 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
67def 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.
77def 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
101def 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
107def Laws.signed_last_inside(limit, k, inside):
108  last_wrapped(limit, k, inside)
109
110def 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.
116def 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.
129def 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
134def 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
144def 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
151def 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
162def Laws.signed_wrap_all_empty(limit):
163  {==}
164
165def Laws.signed_wrap_all_step(limit, head, tail):
166  {==}
167
168def Laws.signed_wrap_each_step(extent, rest, head, tail):
169  {==}
170
171def Laws.signed_wrap_each_end(dimensions):
172  match dimensions:
173    case Nil{}:
174      {==}
175    case extent <> rest:
176      {==}
177
178def Laws.signed_wrap_each_past_rank(positions):
179  {==}
180
181def Laws.signed_axis_limit(input):
182  {==}
183
184def Laws.signed_permute_wraps(input, source, axes):
185  {==}
186
187def Laws.signed_permute_dynamic_wraps(input, axes):
188  Core.Packed{+shape, tensor} = input
189  {==}
190
191def Laws.signed_transpose_wraps(input, source, a, b):
192  {==}
193
194def Laws.signed_transpose_dynamic_wraps(input, a, b):
195  Core.Packed{+shape, tensor} = input
196  {==}
197
198def Laws.signed_read_coordinate_wraps(shape, tensor, coordinates):
199  {==}
200
201def Laws.signed_write_coordinate_wraps(shape, tensor, coordinates, value):
202  {==}
203
204def Laws.signed_read_flat_wraps(shape, tensor, index):
205  {==}
206
207def Laws.signed_write_flat_wraps(shape, tensor, index, value):
208  {==}
209
210def Laws.signed_read_dynamic_wraps(input, index):
211  Core.Packed{+shape, tensor} = input
212  {==}
213
214def Laws.signed_write_dynamic_wraps(input, index, value):
215  Core.Packed{+shape, tensor} = input
216  {==}
217
218def Laws.signed_reshape_infers(input, tensor, extents):
219  {==}
220
221def Laws.signed_reshape_dynamic_infers(input, tensor, extents):
222  {==}
223
224def 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
231def 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
238def 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
247def 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).
253def 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.
266def 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
273def 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.
288def 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.
304def 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.
310def 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
317def 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
330def 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.
344def 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
358def 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
370def Laws.signed_capped_classifies(bound, extents):
371  capped_classifies(bound, extents)
372
373def 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
382def 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
391def 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
405def 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
414def 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.
423def 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
438def 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
452def 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
461def pred(n: Nat) -> Nat:
462  match n:
463    case 0n:
464      0n
465    case 1n+p:
466      p
467
468def 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
471def 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.
475def 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).
488def 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
495def 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
512def 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.
516def 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
527def 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
540def 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
549def 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
558def 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
567def 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
572def Laws.signed_filled_exact(extent, tail, size):
573  {==}
574
575def Laws.signed_filled_inferred(tail, size):
576  {==}
577
578def Laws.signed_error_codes(error):
579  {==}
580
581# Signed slicing.
582
583def Laws.signed_bound_first(limit, k):
584  {==}
585
586def 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
592def Laws.signed_bound_last_inside(limit, k, inside):
593  bound_inside(limit, k, inside)
594
595def 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
600def Laws.signed_slice_bounds(input, dim, start, stop, step):
601  Core.Packed{+shape, tensor} = input
602  {==}
603
604def Laws.signed_select_wraps(input, dim, index):
605  Core.Packed{+shape, tensor} = input
606  {==}
607
608def Laws.signed_narrow_first(input, dim, k, length):
609  Core.Packed{+shape, tensor} = input
610  {==}
611
612def 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
619def 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
629def 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  {==}