u32.bend
1# bend-osdev-u32: the arithmetic of Base's words as Nat arithmetic.
2#
3# This package has no word type of its own: its laws (LAWS.bend) are about
4# Base's Word(n) and U32 operations, stated through their values
5# (Word.to_nat, U32.to_nat): comparison is the order of the values, and
6# addition, subtraction, increment and the shifts are the Nat operations on
7# the values when nothing wraps, and the wrapping ones otherwise. Other
8# packages' proofs use these laws instead of each proving them again.
9#
10# The defs below are the Nat functions the laws are stated with. None of
11# them names a power of two as a closed number: 2^n is U32Nat.dbl(n, 1n),
12# and 2^32 itself is never written out (see README.md, "Stating the
13# bounds").
14import Base
15
16# x times 2^n: x doubled n times
17def U32Nat.dbl(n: Nat, x: Nat) -> Nat:
18 match n:
19 case 0n:
20 x
21 case 1n+p:
22 Nat.double(U32Nat.dbl(p, x))
23
24# 1 for True, 0 for False
25def U32Nat.bit(b: Bool) -> Nat:
26 match b:
27 case True{}:
28 1n
29 case False{}:
30 0n
31
32# n / 2, rounded down
33def U32Nat.half(n: Nat) -> Nat:
34 match n:
35 case 0n:
36 0n
37 case 1n+p:
38 match p:
39 case 0n:
40 0n
41 case 1n+q:
42 1n+U32Nat.half(q)
43
44# x mod 2: 1 for an odd x, 0 for an even one
45def U32Nat.odd(n: Nat) -> Nat:
46 match n:
47 case 0n:
48 0n
49 case 1n+p:
50 match p:
51 case 0n:
52 1n
53 case 1n+q:
54 U32Nat.odd(q)
55
56# the low k bits of x (x mod 2^k), and the rest (x / 2^k, rounded down):
57# x = low(k, x) + 2^k high(k, x)
58def U32Nat.low(k: Nat, +x: Nat) -> Nat:
59 match k:
60 case 0n:
61 0n
62 case 1n+j:
63 Nat.add(U32Nat.odd(x), Nat.double(U32Nat.low(j, U32Nat.half(x))))
64
65def U32Nat.high(k: Nat, x: Nat) -> Nat:
66 match k:
67 case 0n:
68 x
69 case 1n+j:
70 U32Nat.high(j, U32Nat.half(x))
71
72# the word of width n whose low k bits are set (2^k - 1, for k <= n): the
73# mask that U32.and(x, m) takes x's low k bits with
74def U32Word.mask(n: Nat, k: Nat) -> Word(n):
75 match n:
76 case 0n:
77 WNil{}
78 case 1n+p:
79 match k:
80 case 0n:
81 Word.zero(1n+p)
82 case 1n+j:
83 WCon{True{}, U32Word.mask(p, j)}