algo.bend

bend-osdev-algo@0.1.0.0 · 192 lines · 30 definitions

1# bend-osdev-algo: the small algorithms an operating system kernel uses
2# everywhere. This file: bit search in a word.
3#
4# Bit search works on the bits of Base's Word(n) (least significant bit
5# first), generic in the width, so that one proof covers U32 and W64:
6#
7#   popcount   the number of set bits (the kernel's hweight)
8#   ffs        1 + the index of the lowest set bit, 0 for zero (the kernel's
9#              and C's ffs)
10#   fls        1 + the index of the highest set bit, 0 for zero (the
11#              kernel's fls)
12#   first_set  the index of the lowest set bit, None for zero (__ffs)
13#   last_set   the index of the highest set bit, None for zero (__fls)
14#   ctz        the number of zero bits below the lowest set bit (the width
15#              for zero)
16#   clz        the number of zero bits above the highest set bit (the width
17#              for zero)
18#
19# Bitmaps are in bitmap.bend, binary search in bsearch.bend.
20import Base
21import bend-osdev-word64@0.1.0.0/word64.bend as W
22
23# Bits of a word of any width
24
25# bit k (False at or past the width)
26def bitw.test(n: Nat, w: Word(n), k: Nat) -> Bool:
27  match n:
28    case 0n:
29      False{}
30    case 1n+p:
31      match w k:
32        case WCon{b, t} 0n:
33          b
34        case WCon{b, t} 1n+j:
35          bitw.test(p, t, j)
36
37def bitw.popcount.step(b: Bool, k: Nat) -> Nat:
38  match b:
39    case True{}:
40      1n+k
41    case False{}:
42      k
43
44def bitw.popcount(n: Nat, w: Word(n)) -> Nat:
45  match n:
46    case 0n:
47      0n
48    case 1n+p:
49      match w:
50        case WCon{b, t}:
51          bitw.popcount.step(b, bitw.popcount(p, t))
52
53# k is ffs of the bits above the lowest one
54def bitw.ffs.step(b: Bool, k: Nat) -> Nat:
55  match b:
56    case True{}:
57      1n
58    case False{}:
59      match k:
60        case 0n:
61          0n
62        case 1n+j:
63          2n+j
64
65def bitw.ffs(n: Nat, w: Word(n)) -> Nat:
66  match n:
67    case 0n:
68      0n
69    case 1n+p:
70      match w:
71        case WCon{b, t}:
72          bitw.ffs.step(b, bitw.ffs(p, t))
73
74# k is fls of the bits above the lowest one
75def bitw.fls.step(k: Nat, b: Bool) -> Nat:
76  match k:
77    case 0n:
78      match b:
79        case True{}:
80          1n
81        case False{}:
82          0n
83    case 1n+j:
84      2n+j
85
86def bitw.fls(n: Nat, w: Word(n)) -> Nat:
87  match n:
88    case 0n:
89      0n
90    case 1n+p:
91      match w:
92        case WCon{b, t}:
93          bitw.fls.step(bitw.fls(p, t), b)
94
95def bitw.ctz.step(b: Bool, k: Nat) -> Nat:
96  match b:
97    case True{}:
98      0n
99    case False{}:
100      1n+k
101
102def bitw.ctz(n: Nat, w: Word(n)) -> Nat:
103  match n:
104    case 0n:
105      0n
106    case 1n+p:
107      match w:
108        case WCon{b, t}:
109          bitw.ctz.step(b, bitw.ctz(p, t))
110
111def bitw.clz(+n: Nat, w: Word(n)) -> Nat:
112  Nat.sub(n, bitw.fls(n, w))
113
114# a 1-based position (ffs, fls) as a 0-based index
115def bitw.index(m: Nat) -> Maybe<&2, Nat>:
116  match m:
117    case 0n:
118      None{}
119    case 1n+k:
120      Some{k}
121
122# the bits of w, least significant first, in front of rest
123def bitw.to_list(n: Nat, w: Word(n), rest: List<&2, Bool>) -> List<&2, Bool>:
124  match n:
125    case 0n:
126      rest
127    case 1n+p:
128      match w:
129        case WCon{b, t}:
130          Con{b, bitw.to_list(p, t, rest)}
131
132# U32
133
134def bits32.word(x: U32) -> Word(32n):
135  match x:
136    case U32{w}:
137      w
138
139# bit k of x (False for k >= 32)
140def bits32.test(x: U32, k: Nat) -> Bool:
141  bitw.test(32n, bits32.word(x), k)
142
143def bits32.popcount(x: U32) -> Nat:
144  bitw.popcount(32n, bits32.word(x))
145
146def bits32.ffs(x: U32) -> Nat:
147  bitw.ffs(32n, bits32.word(x))
148
149def bits32.fls(x: U32) -> Nat:
150  bitw.fls(32n, bits32.word(x))
151
152def bits32.first_set(x: U32) -> Maybe<&2, Nat>:
153  bitw.index(bits32.ffs(x))
154
155def bits32.last_set(x: U32) -> Maybe<&2, Nat>:
156  bitw.index(bits32.fls(x))
157
158def bits32.ctz(x: U32) -> Nat:
159  bitw.ctz(32n, bits32.word(x))
160
161def bits32.clz(x: U32) -> Nat:
162  bitw.clz(32n, bits32.word(x))
163
164# W64: the low 32 bits, then the high 32
165
166def bits64.word(+a: W.W64) -> Word(64n):
167  W.W64.bits.cat(32n, 32n, bits32.word(W.W64.lo(a)), bits32.word(W.W64.hi(a)))
168
169# bit k of a (False for k >= 64)
170def bits64.test(a: W.W64, k: Nat) -> Bool:
171  bitw.test(64n, bits64.word(a), k)
172
173def bits64.popcount(a: W.W64) -> Nat:
174  bitw.popcount(64n, bits64.word(a))
175
176def bits64.ffs(a: W.W64) -> Nat:
177  bitw.ffs(64n, bits64.word(a))
178
179def bits64.fls(a: W.W64) -> Nat:
180  bitw.fls(64n, bits64.word(a))
181
182def bits64.first_set(a: W.W64) -> Maybe<&2, Nat>:
183  bitw.index(bits64.ffs(a))
184
185def bits64.last_set(a: W.W64) -> Maybe<&2, Nat>:
186  bitw.index(bits64.fls(a))
187
188def bits64.ctz(a: W.W64) -> Nat:
189  bitw.ctz(64n, bits64.word(a))
190
191def bits64.clz(a: W.W64) -> Nat:
192  bitw.clz(64n, bits64.word(a))