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.
10	import Base
11	
12	type W64 is Data:
13	  W64{hi: U32, lo: U32}
14	
15	def W64.zero() -> W64:
16	  W64{0, 0}
17	
18	def W64.one() -> W64:
19	  W64{0, 1}
20	
21	def W64.max() -> W64:
22	  W64{4294967295, 4294967295}
23	
24	# Conversions
25	
26	def 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.
32	def 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	
41	def 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	
50	def 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
60	def W64.lo(a: W64) -> U32:
61	  match a:
62	    case W64{h, l}:
63	      l
64	
65	# the high 32 bits
66	def 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
72	def 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)
76	def W64.two32() -> Nat:
77	  Nat.add(4294967295n, 1n)
78	
79	# x * 2^n: x doubled n times
80	def 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).
91	def 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	
96	def 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
101	def 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	
106	def W64.bit(b: Bool) -> U32:
107	  match b:
108	    case True{}:
109	      1
110	    case False{}:
111	      0
112	
113	def 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	
122	def 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	
125	def 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	
130	def 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)
137	def 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	
141	def 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	
148	def 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	
155	def 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	
160	def 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	
165	def 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	
170	def 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
176	def 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	
191	def 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	
194	def 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	
209	def 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	
214	def 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	
223	def 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	
228	def W64.is_eq(a: W64, b: W64) -> Bool:
229	  Cmp.is_eq(W64.cmp(a, b))
230	
231	def W64.is_lt(a: W64, b: W64) -> Bool:
232	  Cmp.is_lt(W64.cmp(a, b))
233	
234	def W64.is_le(a: W64, b: W64) -> Bool:
235	  Cmp.is_le(W64.cmp(a, b))
236	
237	def W64.is_gt(a: W64, b: W64) -> Bool:
238	  Cmp.is_gt(W64.cmp(a, b))
239	
240	def W64.is_ge(a: W64, b: W64) -> Bool:
241	  Cmp.is_ge(W64.cmp(a, b))
242	
243	def 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
256	def 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
264	def 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	
271	def 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	
276	def 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)
285	def W64.divmod(+a: W64, +b: W64) -> W64 & W64:
286	  W64.divmod.pick(W64.is_zero(b), a, b)
287	
288	def W64.fst(p: W64 & W64) -> W64:
289	  (x, y) = p
290	  x
291	
292	def W64.snd(p: W64 & W64) -> W64:
293	  (x, y) = p
294	  y
295	
296	def W64.div(+a: W64, +b: W64) -> W64:
297	  W64.fst(W64.divmod(a, b))
298	
299	def 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
306	def 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
312	type W64Small is Data:
313	  W64Small{q: W64, r: U32}
314	
315	def W64.small.join(qhi: U32, ql: U32 & U32) -> W64Small:
316	  (qlo, r) = ql
317	  W64Small{W64{qhi, qlo}, r}
318	
319	def 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	
323	def 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	
328	def W64.digit(+d: U32) -> Char:
329	  Chr{U32.add(48, d)}
330	
331	def 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	
338	def W64.small.q(p: W64Small) -> W64:
339	  match p:
340	    case W64Small{q, r}:
341	      q
342	
343	def 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)
350	def 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	
358	def 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	
365	def 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
369	def 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	
376	def W64.hex.digit(+d: U32) -> Char:
377	  W64.hex.pick(U32.is_lt(d, 10), d)
378	
379	def 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	
386	def W64.show_hex(a: W64) -> String:
387	  W64.hex.go(16n, a, "")