src/u32.bend

bend-lawful-stdlib@0.1.0.0 · 330 lines · 20 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat
3import bend-lawful-stdlib@0.1.0.0/src/class.bend as C
4
5# u32.bend: U32 laws that hold for every input.
6#
7#   import ./u32.bend as U32
8#
9# cmp_nat says U32.cmp(a, b) is Nat.cmp of the two numbers; it is proven
10# by induction on the word width. The laws after it use it to reduce U32
11# order to Nat order. LE(a, b) is Nat.LE on the numbers. The clamp laws
12# are about Base's own U32.min, U32.max and U32.clamp. sub_add and add_sub
13# say wrapping + and - undo each other.
14
15def bit(b: Bool) -> Nat:
16  match b:
17    case False{}:
18      0n
19    case True{}:
20      1n
21
22# comparing bit + 2*rest compares the rests first, then the bits, which is
23# what Word.cmp.fin does
24law cmp_bits:
25  for x: Bool
26  for y: Bool
27  for a: Nat
28  for b: Nat
29  {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(Nat.add(bit(x), Nat.double(a)), Nat.add(bit(y), Nat.double(b))) : Cmp}
30
31def cmp_bits(x, y, a, b):
32  match x y a b:
33    case False{} False{} 0n 0n:
34      {==}
35    case False{} True{} 0n 0n:
36      {==}
37    case True{} False{} 0n 0n:
38      {==}
39    case True{} True{} 0n 0n:
40      {==}
41    case False{} False{} 0n 1n+q:
42      {==}
43    case False{} True{} 0n 1n+q:
44      {==}
45    case True{} False{} 0n 1n+q:
46      {==}
47    case True{} True{} 0n 1n+q:
48      {==}
49    case False{} False{} 1n+p 0n:
50      {==}
51    case False{} True{} 1n+p 0n:
52      {==}
53    case True{} False{} 1n+p 0n:
54      {==}
55    case True{} True{} 1n+p 0n:
56      {==}
57    case False{} False{} 1n+p 1n+q:
58      cmp_bits(False{}, False{}, p, q)
59    case False{} True{} 1n+p 1n+q:
60      cmp_bits(False{}, True{}, p, q)
61    case True{} False{} 1n+p 1n+q:
62      cmp_bits(True{}, False{}, p, q)
63    case True{} True{} 1n+p 1n+q:
64      cmp_bits(True{}, True{}, p, q)
65
66law Word.cmp_nat:
67  for +n: Nat
68  for a: Word(n)
69  for b: Word(n)
70  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}
71
72def Word.cmp_nat(n, a, b):
73  match n:
74    case 0n:
75      match a b:
76        case WNil{} WNil{}:
77          {==}
78    case 1n+p:
79      match a b:
80        case WCon{False{}, +at} WCon{False{}, +bt}:
81          %Word.cmp_nat(p, at, bt) : {Nat.cmp(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt))) == Word.cmp.fin(False{}, False{}, _) : Cmp}
82          Equal.sym(Cmp, Word.cmp.fin(False{}, False{}, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))), Nat.cmp(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt))), cmp_bits(False{}, False{}, Word.to_nat(p, at), Word.to_nat(p, bt)))
83        case WCon{False{}, +at} WCon{True{}, +bt}:
84          %Word.cmp_nat(p, at, bt) : {Nat.cmp(Nat.double(Word.to_nat(p, at)), 1n+Nat.double(Word.to_nat(p, bt))) == Word.cmp.fin(False{}, True{}, _) : Cmp}
85          Equal.sym(Cmp, Word.cmp.fin(False{}, True{}, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))), Nat.cmp(Nat.double(Word.to_nat(p, at)), 1n+Nat.double(Word.to_nat(p, bt))), cmp_bits(False{}, True{}, Word.to_nat(p, at), Word.to_nat(p, bt)))
86        case WCon{True{}, +at} WCon{False{}, +bt}:
87          %Word.cmp_nat(p, at, bt) : {Nat.cmp(1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt))) == Word.cmp.fin(True{}, False{}, _) : Cmp}
88          Equal.sym(Cmp, Word.cmp.fin(True{}, False{}, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))), Nat.cmp(1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt))), cmp_bits(True{}, False{}, Word.to_nat(p, at), Word.to_nat(p, bt)))
89        case WCon{True{}, +at} WCon{True{}, +bt}:
90          %Word.cmp_nat(p, at, bt) : {Nat.cmp(1n+Nat.double(Word.to_nat(p, at)), 1n+Nat.double(Word.to_nat(p, bt))) == Word.cmp.fin(True{}, True{}, _) : Cmp}
91          Equal.sym(Cmp, Word.cmp.fin(True{}, True{}, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))), Nat.cmp(1n+Nat.double(Word.to_nat(p, at)), 1n+Nat.double(Word.to_nat(p, bt))), cmp_bits(True{}, True{}, Word.to_nat(p, at), Word.to_nat(p, bt)))
92
93law cmp_nat:
94  for a: U32
95  for b: U32
96  {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}
97
98def cmp_nat(a, b):
99  match a b:
100    case U32{x} U32{y}:
101      Word.cmp_nat(32n, x, y)
102
103# a <= b on U32
104def LE(a: U32, b: U32) -> Data:
105  Nat.LE(U32.to_nat(a), U32.to_nat(b))
106
107# a result of U32.is_lt is the same result of Nat.is_lt on the numbers
108law is_lt_nat:
109  for +a: U32
110  for +b: U32
111  for -c: Bool
112  for e: {U32.is_lt(a, b) == c : Bool}
113  {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}
114
115def is_lt_nat(a, b, c, e):
116  %Equal.sym(Cmp, Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U32.cmp(a, b), cmp_nat(a, b)) : {Cmp.is_lt(_) == c : Bool}
117  e
118
119# Base's U32.min(a, b) is Bool.pick(U32.is_lt(a, b), a, b). A match cannot
120# inspect the computed test, so each .go lemma takes its result c and
121# {U32.is_lt(a, b) == c} as parameters; callers pass the test and {==}.
122
123law min_le_r.go:
124  for +a: U32
125  for +b: U32
126  for c: Bool
127  for e: {U32.is_lt(a, b) == c : Bool}
128  LE(Bool.pick(U32, c, a, b), b)
129
130def min_le_r.go(a, b, c, e):
131  match c:
132    case True{}:
133      Nat.le_of_is_lt(U32.to_nat(a), U32.to_nat(b), is_lt_nat(a, b, True{}, e))
134    case False{}:
135      Nat.le_refl(U32.to_nat(b))
136
137# min(a, b) <= b
138law min_le_r:
139  for +a: U32
140  for +b: U32
141  LE(U32.min(a, b), b)
142
143def min_le_r(a, b):
144  min_le_r.go(a, b, U32.is_lt(a, b), {==})
145
146law le_max_r.go:
147  for +a: U32
148  for +b: U32
149  for c: Bool
150  for e: {U32.is_lt(a, b) == c : Bool}
151  LE(b, Bool.pick(U32, c, b, a))
152
153def le_max_r.go(a, b, c, e):
154  match c:
155    case True{}:
156      Nat.le_refl(U32.to_nat(b))
157    case False{}:
158      Nat.ge_of_not_lt(U32.to_nat(a), U32.to_nat(b), is_lt_nat(a, b, False{}, e))
159
160# b <= max(a, b)
161law le_max_r:
162  for +a: U32
163  for +b: U32
164  LE(b, U32.max(a, b))
165
166def le_max_r(a, b):
167  le_max_r.go(a, b, U32.is_lt(a, b), {==})
168
169# clamp(x, lo, hi) <= hi, even when lo > hi
170law clamp_le_hi:
171  for +x: U32
172  for +lo: U32
173  for +hi: U32
174  LE(U32.clamp(x, lo, hi), hi)
175
176def clamp_le_hi(x, lo, hi):
177  min_le_r(U32.max(x, lo), hi)
178
179law lo_le_clamp.go:
180  for +lo: U32
181  for +m: U32
182  for +hi: U32
183  for lm: LE(lo, m)
184  for lh: LE(lo, hi)
185  for c: Bool
186  LE(lo, Bool.pick(U32, c, m, hi))
187
188def lo_le_clamp.go(lo, m, hi, lm, lh, c):
189  match c:
190    case True{}:
191      lm
192    case False{}:
193      lh
194
195# lo <= clamp(x, lo, hi) when lo <= hi
196law lo_le_clamp:
197  for +x: U32
198  for +lo: U32
199  for +hi: U32
200  for lh: LE(lo, hi)
201  LE(lo, U32.clamp(x, lo, hi))
202
203def lo_le_clamp(x, lo, hi, lh):
204  lo_le_clamp.go(lo, U32.max(x, lo), hi, le_max_r(x, lo), lh, U32.is_lt(U32.max(x, lo), hi))
205
206# Wrapping + and - undo each other
207# ---------------------------------
208# Word.adc(n, a, b, flip, c) adds a, b (negated when flip) and carry c.
209# Adding b with carry c and then subtracting b with carry not(c) returns
210# a, and the carry out of each bit is again not(c)'s counterpart, so the
211# induction runs bit by bit. U32.add uses carry False, U32.sub carry True.
212
213# (a + b + c) - b, with carry not(c), is a. Each case passes the carry
214# out of its bit.
215law Word.sub_add:
216  for +n: Nat
217  for a: Word(n)
218  for +b: Word(n)
219  for c: Bool
220  {a == Word.adc(n, Word.adc(n, a, b, False{}, c), b, True{}, Bool.not(c)) : Word(n)}
221
222# one bit: the bit is kept, and e is the law for the rest at the carry k
223law Word.sub_add.arm:
224  for -p: Nat
225  for -h: Bool
226  for -at: Word(p)
227  for -bt: Word(p)
228  for -k: Bool
229  for e: {at == Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k)) : Word(p)}
230  {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k))} : Word(1n+p)}
231
232def Word.sub_add.arm(p, h, at, bt, k, e):
233  Equal.cong(Word(p), Word(1n+p), w => WCon{h, w}, at, Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k)), e)
234
235def Word.sub_add(n, a, b, c):
236  match n:
237    case 0n:
238      match a b:
239        case WNil{} WNil{}:
240          {==}
241    case 1n+p:
242      match a b c:
243        case WCon{False{}, at} WCon{False{}, +bt} False{}:
244          Word.sub_add.arm(p, False{}, at, bt, False{}, Word.sub_add(p, at, bt, False{}))
245        case WCon{False{}, at} WCon{False{}, +bt} True{}:
246          Word.sub_add.arm(p, False{}, at, bt, False{}, Word.sub_add(p, at, bt, False{}))
247        case WCon{False{}, at} WCon{True{}, +bt} False{}:
248          Word.sub_add.arm(p, False{}, at, bt, False{}, Word.sub_add(p, at, bt, False{}))
249        case WCon{False{}, at} WCon{True{}, +bt} True{}:
250          Word.sub_add.arm(p, False{}, at, bt, True{}, Word.sub_add(p, at, bt, True{}))
251        case WCon{True{}, at} WCon{False{}, +bt} False{}:
252          Word.sub_add.arm(p, True{}, at, bt, False{}, Word.sub_add(p, at, bt, False{}))
253        case WCon{True{}, at} WCon{False{}, +bt} True{}:
254          Word.sub_add.arm(p, True{}, at, bt, True{}, Word.sub_add(p, at, bt, True{}))
255        case WCon{True{}, at} WCon{True{}, +bt} False{}:
256          Word.sub_add.arm(p, True{}, at, bt, True{}, Word.sub_add(p, at, bt, True{}))
257        case WCon{True{}, at} WCon{True{}, +bt} True{}:
258          Word.sub_add.arm(p, True{}, at, bt, True{}, Word.sub_add(p, at, bt, True{}))
259
260# (a - b) + b, with carry not(c), is a
261law Word.add_sub:
262  for +n: Nat
263  for a: Word(n)
264  for +b: Word(n)
265  for c: Bool
266  {a == Word.adc(n, Word.adc(n, a, b, True{}, c), b, False{}, Bool.not(c)) : Word(n)}
267
268# one bit: the bit is kept, and e is the law for the rest at the carry k
269law Word.add_sub.arm:
270  for -p: Nat
271  for -h: Bool
272  for -at: Word(p)
273  for -bt: Word(p)
274  for -k: Bool
275  for e: {at == Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k)) : Word(p)}
276  {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k))} : Word(1n+p)}
277
278def Word.add_sub.arm(p, h, at, bt, k, e):
279  Equal.cong(Word(p), Word(1n+p), w => WCon{h, w}, at, Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k)), e)
280
281def Word.add_sub(n, a, b, c):
282  match n:
283    case 0n:
284      match a b:
285        case WNil{} WNil{}:
286          {==}
287    case 1n+p:
288      match a b c:
289        case WCon{False{}, at} WCon{False{}, +bt} False{}:
290          Word.add_sub.arm(p, False{}, at, bt, False{}, Word.add_sub(p, at, bt, False{}))
291        case WCon{False{}, at} WCon{False{}, +bt} True{}:
292          Word.add_sub.arm(p, False{}, at, bt, True{}, Word.add_sub(p, at, bt, True{}))
293        case WCon{False{}, at} WCon{True{}, +bt} False{}:
294          Word.add_sub.arm(p, False{}, at, bt, False{}, Word.add_sub(p, at, bt, False{}))
295        case WCon{False{}, at} WCon{True{}, +bt} True{}:
296          Word.add_sub.arm(p, False{}, at, bt, False{}, Word.add_sub(p, at, bt, False{}))
297        case WCon{True{}, at} WCon{False{}, +bt} False{}:
298          Word.add_sub.arm(p, True{}, at, bt, True{}, Word.add_sub(p, at, bt, True{}))
299        case WCon{True{}, at} WCon{False{}, +bt} True{}:
300          Word.add_sub.arm(p, True{}, at, bt, True{}, Word.add_sub(p, at, bt, True{}))
301        case WCon{True{}, at} WCon{True{}, +bt} False{}:
302          Word.add_sub.arm(p, True{}, at, bt, False{}, Word.add_sub(p, at, bt, False{}))
303        case WCon{True{}, at} WCon{True{}, +bt} True{}:
304          Word.add_sub.arm(p, True{}, at, bt, True{}, Word.add_sub(p, at, bt, True{}))
305
306# subtracting b undoes adding b, with wraparound
307law sub_add:
308  for a: U32
309  for b: U32
310  {a == U32.sub(U32.add(a, b), b) : U32}
311
312def sub_add(a, b):
313  match a b:
314    case U32{x} U32{+y}:
315      Equal.cong(Word(32n), U32, w => U32{w}, x, Word.sub(32n, Word.add(32n, x, y), y), Word.sub_add(32n, x, y, False{}))
316
317# adding b undoes subtracting b, with wraparound
318law add_sub:
319  for a: U32
320  for b: U32
321  {a == U32.add(U32.sub(a, b), b) : U32}
322
323def add_sub(a, b):
324  match a b:
325    case U32{x} U32{+y}:
326      Equal.cong(Word(32n), U32, w => U32{w}, x, Word.add(32n, Word.sub(32n, x, y), y), Word.add_sub(32n, x, y, True{}))
327
328# wrapping + and - as a C.Group
329def group() -> C.Group<U32>:
330  C.Group{U32.add, U32.sub, sub_add, add_sub}