word64.bend

bend-osdev-word64@0.1.1.0 · 387 lines · 65 definitions

1# bend-osdev-word64: unsigned 64-bit words for bend-osdev, wrapping on overflow.
2#
3# Every bend-osdev package that needs 64 bits uses W64, and only through these
4# defs. A W64 is its two 32-bit halves, each a native U32, so a W64 costs two
5# machine words (a Word(64n) of bits, used before, cost sixty-four, and records
6# of several of them were more than Bend's C backend can compile:
7# bendlang/bend#1069). When Base gains a native U64 (bendlang/bend#1027), only
8# this file changes. The type is not named U64, so that it cannot clash with
9# Base's when it arrives.
10import Base
11
12type W64 is Data:
13  W64{hi: U32, lo: U32}
14
15def W64.zero() -> W64:
16  W64{0, 0}
17
18def W64.one() -> W64:
19  W64{0, 1}
20
21def W64.max() -> W64:
22  W64{4294967295, 4294967295}
23
24# Conversions
25
26def W64.from_u32(a: U32) -> W64:
27  W64{0, a}
28
29# Splitting a Word(m + n) into its low m and high n bits (bits are stored
30# least significant first), and joining them back. Named under W64, not Word,
31# so that they cannot clash with Base if it gains Word.lo, Word.hi or Word.cat.
32def W64.bits.lo(m: Nat, n: Nat, w: Word(Nat.add(m, n))) -> Word(m):
33  match m:
34    case 0n:
35      WNil{}
36    case 1n+p:
37      match w:
38        case WCon{h, t}:
39          WCon{h, W64.bits.lo(p, n, t)}
40
41def W64.bits.hi(m: Nat, n: Nat, w: Word(Nat.add(m, n))) -> Word(n):
42  match m:
43    case 0n:
44      w
45    case 1n+p:
46      match w:
47        case WCon{h, t}:
48          W64.bits.hi(p, n, t)
49
50def W64.bits.cat(m: Nat, n: Nat, a: Word(m), b: Word(n)) -> Word(Nat.add(m, n)):
51  match m:
52    case 0n:
53      b
54    case 1n+p:
55      match a:
56        case WCon{h, t}:
57          WCon{h, W64.bits.cat(p, n, t, b)}
58
59# the low 32 bits
60def W64.lo(a: W64) -> U32:
61  match a:
62    case W64{h, l}:
63      l
64
65# the high 32 bits
66def W64.hi(a: W64) -> U32:
67  match a:
68    case W64{h, l}:
69      h
70
71# the word whose high and low 32 bits are hi and lo
72def W64.from_parts(hi: U32, lo: U32) -> W64:
73  W64{hi, lo}
74
75# 2^32, built from literals Bend reads (a literal is at most 2^32 - 1)
76def W64.two32() -> Nat:
77  Nat.add(4294967295n, 1n)
78
79# x * 2^n: x doubled n times
80def W64.dbl(n: Nat, x: Nat) -> Nat:
81  match n:
82    case 0n:
83      x
84    case 1n+p:
85      Nat.double(W64.dbl(p, x))
86
87# lo + hi * 2^32. The high half's weight is 32 doublings of its value, not a
88# product with the closed number 2^32: the checkers count a Nat in unary, so
89# a proof that unfolds to_nat on unknown halves stays symbolic this way
90# (see README.md, Laws).
91def W64.to_nat(a: W64) -> Nat:
92  match a:
93    case W64{h, l}:
94      Nat.add(U32.to_nat(l), W64.dbl(32n, U32.to_nat(h)))
95
96def W64.from_nat.pair(qr: Nat & Nat) -> W64:
97  (q, r) = qr
98  W64{U32.from_nat(q), U32.from_nat(r)}
99
100# k mod 2^64
101def W64.from_nat(k: Nat) -> W64:
102  W64.from_nat.pair(Nat.divmod(k, W64.two32()))
103
104# Selecting without branching on a computed value in a recursive def
105
106def W64.bit(b: Bool) -> U32:
107  match b:
108    case True{}:
109      1
110    case False{}:
111      0
112
113def W64.sel(b: Bool, x: W64, y: W64) -> W64:
114  match b:
115    case True{}:
116      x
117    case False{}:
118      y
119
120# Arithmetic, modulo 2^64
121
122def W64.add.go(+al: U32, ah: U32, bh: U32, +l: U32) -> W64:
123  W64{U32.add(U32.add(ah, bh), W64.bit(U32.is_lt(l, al))), l}
124
125def W64.add(a: W64, b: W64) -> W64:
126  match a b:
127    case W64{ah, +al} W64{bh, bl}:
128      W64.add.go(al, ah, bh, U32.add(al, bl))
129
130def W64.sub(a: W64, b: W64) -> W64:
131  match a b:
132    case W64{ah, +al} W64{bh, +bl}:
133      W64{U32.sub(U32.sub(ah, bh), W64.bit(U32.is_lt(al, bl))), U32.sub(al, bl)}
134
135# the high 32 bits of the 64-bit product of two 32-bit words, from their
136# 16-bit halves (every partial product fits in 32 bits)
137def W64.mulhi.go(+p00: U32, +p01: U32, +p10: U32, p11: U32) -> U32:
138  +mid = U32.add(U32.add(U32.shrn(p00, 16n), U32.and(p01, 65535)), U32.and(p10, 65535))
139  U32.add(U32.add(U32.add(p11, U32.shrn(p01, 16n)), U32.shrn(p10, 16n)), U32.shrn(mid, 16n))
140
141def W64.mulhi(+a: U32, +b: U32) -> U32:
142  +a0 = U32.and(a, 65535)
143  +a1 = U32.shrn(a, 16n)
144  +b0 = U32.and(b, 65535)
145  +b1 = U32.shrn(b, 16n)
146  W64.mulhi.go(U32.mul(a0, b0), U32.mul(a0, b1), U32.mul(a1, b0), U32.mul(a1, b1))
147
148def W64.mul(a: W64, b: W64) -> W64:
149  match a b:
150    case W64{ah, +al} W64{bh, +bl}:
151      W64{U32.add(U32.add(W64.mulhi(al, bl), U32.mul(al, bh)), U32.mul(ah, bl)), U32.mul(al, bl)}
152
153# Bits
154
155def W64.and(a: W64, b: W64) -> W64:
156  match a b:
157    case W64{ah, al} W64{bh, bl}:
158      W64{U32.and(ah, bh), U32.and(al, bl)}
159
160def W64.or(a: W64, b: W64) -> W64:
161  match a b:
162    case W64{ah, al} W64{bh, bl}:
163      W64{U32.or(ah, bh), U32.or(al, bl)}
164
165def W64.xor(a: W64, b: W64) -> W64:
166  match a b:
167    case W64{ah, al} W64{bh, bl}:
168      W64{U32.xor(ah, bh), U32.xor(al, bl)}
169
170def W64.not(a: W64) -> W64:
171  match a:
172    case W64{h, l}:
173      W64{U32.not(h), U32.not(l)}
174
175# shifts by k bits: 0 leaves the word, 64 or more gives 0
176def W64.shl.pick(z: Bool, lt32: Bool, lt64: Bool, +k: Nat, a: W64) -> W64:
177  match z lt32 lt64:
178    case True{} _ _:
179      a
180    case False{} True{} _:
181      match a:
182        case W64{h, +l}:
183          W64{U32.or(U32.shln(h, k), U32.shrn(l, Nat.sub(32n, k))), U32.shln(l, k)}
184    case False{} False{} True{}:
185      match a:
186        case W64{h, l}:
187          W64{U32.shln(l, Nat.sub(k, 32n)), 0}
188    case False{} False{} False{}:
189      W64.zero()
190
191def W64.shl(a: W64, +k: Nat) -> W64:
192  W64.shl.pick(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, a)
193
194def W64.shr.pick(z: Bool, lt32: Bool, lt64: Bool, +k: Nat, a: W64) -> W64:
195  match z lt32 lt64:
196    case True{} _ _:
197      a
198    case False{} True{} _:
199      match a:
200        case W64{+h, l}:
201          W64{U32.shrn(h, k), U32.or(U32.shrn(l, k), U32.shln(h, Nat.sub(32n, k)))}
202    case False{} False{} True{}:
203      match a:
204        case W64{h, l}:
205          W64{0, U32.shrn(h, Nat.sub(k, 32n))}
206    case False{} False{} False{}:
207      W64.zero()
208
209def W64.shr(a: W64, +k: Nat) -> W64:
210  W64.shr.pick(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, a)
211
212# Comparisons
213
214def W64.cmp.pick(c: Cmp, al: U32, bl: U32) -> Cmp:
215  match c:
216    case EQ{}:
217      U32.cmp(al, bl)
218    case LT{}:
219      LT{}
220    case GT{}:
221      GT{}
222
223def W64.cmp(a: W64, b: W64) -> Cmp:
224  match a b:
225    case W64{ah, al} W64{bh, bl}:
226      W64.cmp.pick(U32.cmp(ah, bh), al, bl)
227
228def W64.is_eq(a: W64, b: W64) -> Bool:
229  Cmp.is_eq(W64.cmp(a, b))
230
231def W64.is_lt(a: W64, b: W64) -> Bool:
232  Cmp.is_lt(W64.cmp(a, b))
233
234def W64.is_le(a: W64, b: W64) -> Bool:
235  Cmp.is_le(W64.cmp(a, b))
236
237def W64.is_gt(a: W64, b: W64) -> Bool:
238  Cmp.is_gt(W64.cmp(a, b))
239
240def W64.is_ge(a: W64, b: W64) -> Bool:
241  Cmp.is_ge(W64.cmp(a, b))
242
243def W64.is_zero(a: W64) -> Bool:
244  W64.is_eq(a, W64.zero())
245
246# Division: shift-and-subtract over the 64 bits of a, most significant first.
247# r stays below b; when doubling r overflows 64 bits (its top bit was set),
248# the true value is past b, and the wrapping subtraction is still exact.
249
250#
251# The loop runs over the bits of a's two halves (as Base's U32.divmod.go
252# does over a word), not over a count: on an unknown dividend it is stuck
253# at once, so a proof checker never unrolls its 64 steps.
254
255# one step: the bit x comes in below r
256def W64.div.step(x: Bool, +b: W64, qr: W64 & W64) -> W64 & W64:
257  (+q, +r) = qr
258  +r2 = W64.or(W64.shl(r, 1n), W64.from_u32(W64.bit(x)))
259  +ge = Bool.or(U32.is_eq(U32.shrn(W64.hi(r), 31n), 1), W64.is_ge(r2, b))
260  (W64.or(W64.shl(q, 1n), W64.from_u32(W64.bit(ge))), W64.sel(ge, W64.sub(r2, b), r2))
261
262# the m bits of w (least significant first) read onto qr, most significant
263# first
264def W64.div.bits(m: Nat, w: Word(m), +b: W64, qr: W64 & W64) -> W64 & W64:
265  match m w:
266    case 0n WNil{}:
267      qr
268    case 1n+p WCon{x, hi}:
269      W64.div.step(x, b, W64.div.bits(p, hi, b, qr))
270
271def W64.div.go(a: W64, +b: W64) -> W64 & W64:
272  match a:
273    case W64{U32{hw}, U32{lw}}:
274      W64.div.bits(32n, lw, b, W64.div.bits(32n, hw, b, (W64.zero(), W64.zero())))
275
276def W64.divmod.pick(z: Bool, +a: W64, +b: W64) -> W64 & W64:
277  match z:
278    case True{}:
279      (W64.zero(), a)
280    case False{}:
281      W64.div.go(a, b)
282
283# the quotient and the remainder; by zero, the quotient is 0 and the
284# remainder is a (as bend-kit-int's U64, used before, answered)
285def W64.divmod(+a: W64, +b: W64) -> W64 & W64:
286  W64.divmod.pick(W64.is_zero(b), a, b)
287
288def W64.fst(p: W64 & W64) -> W64:
289  (x, y) = p
290  x
291
292def W64.snd(p: W64 & W64) -> W64:
293  (x, y) = p
294  y
295
296def W64.div(+a: W64, +b: W64) -> W64:
297  W64.fst(W64.divmod(a, b))
298
299def W64.mod(+a: W64, +b: W64) -> W64:
300  W64.snd(W64.divmod(a, b))
301
302# Text
303
304# a divided by a small d (1 to 65536) and the remainder, through the four
305# 16-bit pieces of a, most significant first: every step fits in 32 bits
306def W64.small.step(+d: U32, qr: U32 & U32, +c: U32) -> U32 & U32:
307  (q, r) = qr
308  +v = U32.add(U32.mul(r, 65536), c)
309  (U32.or(U32.shln(q, 16n), U32.div(v, d)), U32.mod(v, d))
310
311# a quotient and a small remainder
312type W64Small is Data:
313  W64Small{q: W64, r: U32}
314
315def W64.small.join(qhi: U32, ql: U32 & U32) -> W64Small:
316  (qlo, r) = ql
317  W64Small{W64{qhi, qlo}, r}
318
319def W64.small.fin(qh: U32 & U32, +d: U32, +l: U32) -> W64Small:
320  (qhi, r) = qh
321  W64.small.join(qhi, W64.small.step(d, W64.small.step(d, (0, r), U32.shrn(l, 16n)), U32.and(l, 65535)))
322
323def W64.small.divmod(a: W64, +d: U32) -> W64Small:
324  match a:
325    case W64{+h, l}:
326      W64.small.fin(W64.small.step(d, W64.small.step(d, (0, 0), U32.shrn(h, 16n)), U32.and(h, 65535)), d, l)
327
328def W64.digit(+d: U32) -> Char:
329  Chr{U32.add(48, d)}
330
331def W64.show.push(z: Bool, acc: String, +d: U32) -> String:
332  match z:
333    case True{}:
334      acc
335    case False{}:
336      SCon{W64.digit(d), acc}
337
338def W64.small.q(p: W64Small) -> W64:
339  match p:
340    case W64Small{q, r}:
341      q
342
343def W64.small.r(p: W64Small) -> U32:
344  match p:
345    case W64Small{q, r}:
346      r
347
348# the decimal digits of a, consuming one of 20 steps per digit (after a
349# reaches 0 the steps add nothing)
350def W64.show.go(n: Nat, +a: W64, acc: String) -> String:
351  match n:
352    case 0n:
353      acc
354    case 1n+p:
355      +dm = W64.small.divmod(a, 10)
356      W64.show.go(p, W64.small.q(dm), W64.show.push(W64.is_zero(a), acc, W64.small.r(dm)))
357
358def W64.show.pick(z: Bool, +a: W64) -> String:
359  match z:
360    case True{}:
361      "0"
362    case False{}:
363      W64.show.go(20n, a, "")
364
365def W64.show(+a: W64) -> String:
366  W64.show.pick(W64.is_zero(a), a)
367
368# the 16 hex digits, lower case, most significant first
369def W64.hex.pick(lt: Bool, d: U32) -> Char:
370  match lt:
371    case True{}:
372      Chr{U32.add(48, d)}
373    case False{}:
374      Chr{U32.add(87, d)}
375
376def W64.hex.digit(+d: U32) -> Char:
377  W64.hex.pick(U32.is_lt(d, 10), d)
378
379def W64.hex.go(n: Nat, +a: W64, acc: String) -> String:
380  match n:
381    case 0n:
382      acc
383    case 1n+p:
384      W64.hex.go(p, W64.shr(a, 4n), SCon{W64.hex.digit(U32.and(W64.lo(a), 15)), acc})
385
386def W64.show_hex(a: W64) -> String:
387  W64.hex.go(16n, a, "")