LAWS.bend

bend-osdev-algo@0.1.0.0 · 389 lines · 59 definitions

1# Properties, for every input:
2#
3# * bit search in a U32 and in a W64: popcount is at most the width, and the
4#   popcounts of a word and of its complement add up to the width; the bit
5#   first_set names is set, and no bit below it is; the bit last_set names is
6#   set, and no bit above it is; each is None only for zero; ctz is the index
7#   of the lowest set bit, clz plus the index of the highest set bit is the
8#   width less one, and so for a nonzero word ctz + clz is at most the width
9#   less one;
10# * bitmaps: next_set and next_clear answer at most the size; an answer below
11#   the size is at or after the start and has the bit wanted, and no bit from
12#   the start up to the answer has it;
13# * binary search on a sorted list: every element before lower_bound is below
14#   the key, and every element from it on is not; find answers an index that
15#   holds the key, and None only when no element is the key.
16#
17# * binary search on an Array<U32> (through bend-osdev-array's laws): for
18#   every perfect array whose first n slots are sorted, array_lower_bound
19#   and array_find answer what lower_bound and find answer on the list of
20#   those slots, and hand the array back.
21#
22# Vectors: the values of each function on edge cases, and binary search on a
23# sorted Array<U32>.
24import Base
25import bend-osdev-word64@0.1.0.0/word64.bend as W
26import bend-osdev-array@0.1.0.0/array.bend as AR
27import bend-osdev-algo@0.1.0.0/algo.bend as A
28import bend-osdev-algo@0.1.0.0/bitmap.bend as M
29import bend-osdev-algo@0.1.0.0/bsearch.bend as S
30
31# U32
32
33law popcount_le:
34  for x: U32
35  {Nat.is_le(A.bits32.popcount(x), 32n) == True{} : Bool}
36
37law popcount_not:
38  for x: U32
39  {Nat.add(A.bits32.popcount(x), A.bits32.popcount(U32.not(x))) == 32n : Nat}
40
41law first_set_is_set:
42  for x: U32
43  for k: Nat
44  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
45  {A.bits32.test(x, k) == True{} : Bool}
46
47law first_set_lowest:
48  for x: U32
49  for k: Nat
50  for j: Nat
51  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
52  for l: {Nat.is_lt(j, k) == True{} : Bool}
53  {A.bits32.test(x, j) == False{} : Bool}
54
55law first_set_none:
56  for x: U32
57  for e: {A.bits32.first_set(x) == None{} : Maybe<&2, Nat>}
58  {x == 0 : U32}
59
60law last_set_is_set:
61  for x: U32
62  for k: Nat
63  for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
64  {A.bits32.test(x, k) == True{} : Bool}
65
66law last_set_highest:
67  for x: U32
68  for k: Nat
69  for j: Nat
70  for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
71  for l: {Nat.is_lt(k, j) == True{} : Bool}
72  {A.bits32.test(x, j) == False{} : Bool}
73
74law last_set_none:
75  for x: U32
76  for e: {A.bits32.last_set(x) == None{} : Maybe<&2, Nat>}
77  {x == 0 : U32}
78
79law ctz_first_set:
80  for x: U32
81  for k: Nat
82  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
83  {A.bits32.ctz(x) == k : Nat}
84
85law clz_last_set:
86  for x: U32
87  for k: Nat
88  for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
89  {Nat.add(A.bits32.clz(x), k) == 31n : Nat}
90
91law first_le_last:
92  for x: U32
93  for i: Nat
94  for k: Nat
95  for e: {A.bits32.first_set(x) == Some{i} : Maybe<&2, Nat>}
96  for f: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
97  {Nat.is_le(i, k) == True{} : Bool}
98
99law ctz_clz:
100  for x: U32
101  for k: Nat
102  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
103  {Nat.is_le(Nat.add(A.bits32.ctz(x), A.bits32.clz(x)), 31n) == True{} : Bool}
104
105# W64
106
107law popcount64_le:
108  for a: W.W64
109  {Nat.is_le(A.bits64.popcount(a), 64n) == True{} : Bool}
110
111law first_set64_is_set:
112  for a: W.W64
113  for k: Nat
114  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
115  {A.bits64.test(a, k) == True{} : Bool}
116
117law first_set64_lowest:
118  for a: W.W64
119  for k: Nat
120  for j: Nat
121  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
122  for l: {Nat.is_lt(j, k) == True{} : Bool}
123  {A.bits64.test(a, j) == False{} : Bool}
124
125law first_set64_none:
126  for a: W.W64
127  for e: {A.bits64.first_set(a) == None{} : Maybe<&2, Nat>}
128  {a == W.W64.zero() : W.W64}
129
130law last_set64_is_set:
131  for a: W.W64
132  for k: Nat
133  for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
134  {A.bits64.test(a, k) == True{} : Bool}
135
136law last_set64_highest:
137  for a: W.W64
138  for k: Nat
139  for j: Nat
140  for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
141  for l: {Nat.is_lt(k, j) == True{} : Bool}
142  {A.bits64.test(a, j) == False{} : Bool}
143
144law ctz64_first_set:
145  for a: W.W64
146  for k: Nat
147  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
148  {A.bits64.ctz(a) == k : Nat}
149
150law clz64_last_set:
151  for a: W.W64
152  for k: Nat
153  for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
154  {Nat.add(A.bits64.clz(a), k) == 63n : Nat}
155
156law ctz_clz64:
157  for a: W.W64
158  for k: Nat
159  for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
160  {Nat.is_le(Nat.add(A.bits64.ctz(a), A.bits64.clz(a)), 63n) == True{} : Bool}
161
162# Bitmaps
163
164law next_set_le_size:
165  for words: List<&2, U32>
166  for size: Nat
167  for start: Nat
168  {Nat.is_le(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
169
170law next_set_is_set:
171  for words: List<&2, U32>
172  for size: Nat
173  for start: Nat
174  for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
175  {M.bitmap.test(words, M.bitmap.next_set(words, size, start)) == True{} : Bool}
176
177law next_set_at_least:
178  for words: List<&2, U32>
179  for size: Nat
180  for start: Nat
181  for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
182  {Nat.is_le(start, M.bitmap.next_set(words, size, start)) == True{} : Bool}
183
184law next_set_none_before:
185  for words: List<&2, U32>
186  for size: Nat
187  for start: Nat
188  for j: Nat
189  for l: {Nat.is_le(start, j) == True{} : Bool}
190  for m: {Nat.is_lt(j, M.bitmap.next_set(words, size, start)) == True{} : Bool}
191  {M.bitmap.test(words, j) == False{} : Bool}
192
193law next_clear_le_size:
194  for words: List<&2, U32>
195  for size: Nat
196  for start: Nat
197  {Nat.is_le(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
198
199law next_clear_is_clear:
200  for words: List<&2, U32>
201  for size: Nat
202  for start: Nat
203  for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
204  {M.bitmap.test(words, M.bitmap.next_clear(words, size, start)) == False{} : Bool}
205
206law next_clear_at_least:
207  for words: List<&2, U32>
208  for size: Nat
209  for start: Nat
210  for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
211  {Nat.is_le(start, M.bitmap.next_clear(words, size, start)) == True{} : Bool}
212
213law next_clear_none_before:
214  for words: List<&2, U32>
215  for size: Nat
216  for start: Nat
217  for j: Nat
218  for l: {Nat.is_le(start, j) == True{} : Bool}
219  for m: {Nat.is_lt(j, M.bitmap.next_clear(words, size, start)) == True{} : Bool}
220  {M.bitmap.test(words, j) == True{} : Bool}
221
222# Binary search (the reference, on a list)
223
224law lower_bound_le_length:
225  for xs: List<&2, U32>
226  for key: U32
227  {Nat.is_le(S.bsearch.lower_bound(xs, key), List.length(&2, U32, xs)) == True{} : Bool}
228
229law lower_bound_below:
230  for xs: List<&2, U32>
231  for key: U32
232  for i: Nat
233  for x: U32
234  for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
235  for l: {Nat.is_lt(i, S.bsearch.lower_bound(xs, key)) == True{} : Bool}
236  {U32.is_lt(x, key) == True{} : Bool}
237
238law lower_bound_above:
239  for xs: List<&2, U32>
240  for key: U32
241  for i: Nat
242  for x: U32
243  for s: {S.bsearch.sorted(xs) == True{} : Bool}
244  for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
245  for l: {Nat.is_le(S.bsearch.lower_bound(xs, key), i) == True{} : Bool}
246  {U32.is_lt(x, key) == False{} : Bool}
247
248law find_some:
249  for xs: List<&2, U32>
250  for key: U32
251  for i: Nat
252  for e: {S.bsearch.find(xs, key) == Some{i} : Maybe<&2, Nat>}
253  {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}
254
255law find_none:
256  for xs: List<&2, U32>
257  for key: U32
258  for i: Nat
259  for x: U32
260  for s: {S.bsearch.sorted(xs) == True{} : Bool}
261  for e: {S.bsearch.find(xs, key) == None{} : Maybe<&2, Nat>}
262  for g: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
263  {U32.is_eq(x, key) == False{} : Bool}
264
265# Binary search on an Array<U32> (the fast implementation), against the
266# reference: for an array a that is a perfect tree of depth d < 32 (as
267# Array.new and Array.set build), searched in its first n slots (n <= 2^d)
268# whose elements, in index order (array's Arrays.leaves), are sorted. The
269# array search answers a U32 and Maybe<&2, U32>; algo_index_nat reads the
270# latter as the list search's Maybe<&2, Nat>.
271
272def algo_index_nat(m: Maybe<&2, U32>) -> Maybe<&2, Nat>:
273  match m:
274    case None{}:
275      None{}
276    case Some{i}:
277      Some{U32.to_nat(i)}
278
279law array_lower_bound_list:
280  for +d: Nat
281  for a: Array<U32>
282  for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
283  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
284  for n: U32
285  for hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}
286  for key: U32
287  for hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}
288  {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Nat}
289
290law array_lower_bound_same:
291  for +d: Nat
292  for a: Array<U32>
293  for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
294  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
295  for n: U32
296  for key: U32
297  {Pair.fst(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key)) == a : Array<U32>}
298
299law array_find_list:
300  for +d: Nat
301  for a: Array<U32>
302  for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
303  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
304  for n: U32
305  for hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}
306  for key: U32
307  for hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}
308  {algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key))) == S.bsearch.find(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Maybe<&2, Nat>}
309
310law array_find_same:
311  for +d: Nat
312  for a: Array<U32>
313  for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
314  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
315  for n: U32
316  for key: U32
317  {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key)) == a : Array<U32>}
318
319# Vectors (0x80000000 = 2147483648, 0xFFFFFFFF = 4294967295, 40 = 0b101000)
320
321law vec_popcount:
322  {A.bits32.popcount(4294967295) == 32n : Nat}
323
324law vec_zero:
325  {(A.bits32.ffs(0), A.bits32.fls(0), A.bits32.ctz(0), A.bits32.clz(0)) == (0n, 0n, 32n, 32n) : Nat & Nat & Nat & Nat}
326
327law vec_forty:
328  {(A.bits32.ffs(40), A.bits32.fls(40), A.bits32.ctz(40), A.bits32.clz(40)) == (4n, 6n, 3n, 26n) : Nat & Nat & Nat & Nat}
329
330law vec_top:
331  {(A.bits32.first_set(2147483648), A.bits32.last_set(1)) == (Some{31n}, Some{0n}) : Maybe<&2, Nat> & Maybe<&2, Nat>}
332
333law vec64_halves:
334  {(A.bits64.ctz(W.W64.from_parts(1, 0)), A.bits64.clz(W.W64.from_parts(0, 1)), A.bits64.popcount(W.W64.max())) == (32n, 63n, 64n) : Nat & Nat & Nat}
335
336law vec64_zero:
337  {(A.bits64.first_set(W.W64.zero()), A.bits64.ctz(W.W64.zero())) == (None{}, 64n) : Maybe<&2, Nat> & Nat}
338
339law vec_next_set:
340  {M.bitmap.next_set([0, 8], 64n, 3n) == 35n : Nat}
341
342law vec_next_set_none:
343  {M.bitmap.next_set([0, 8], 35n, 0n) == 35n : Nat}
344
345law vec_next_clear:
346  {M.bitmap.next_clear([4294967295, 1], 64n, 3n) == 33n : Nat}
347
348law vec_next_past_size:
349  {M.bitmap.next_clear([0], 10n, 12n) == 10n : Nat}
350
351law vec_lower_bound:
352  {(S.bsearch.lower_bound([1, 3, 3, 7, 9], 3), S.bsearch.lower_bound([1, 3, 3, 7, 9], 10), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (1n, 5n, Some{3n}, None{}) : Nat & Nat & Maybe<&2, Nat> & Maybe<&2, Nat>}
353
354# the array [1, 3, 3, 7, 9, 0, 0, 0], searched in its first 5 slots
355law vec_array_lower_bound:
356  {Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 3)) == 1 : U32}
357
358law vec_array_lower_bound_end:
359  {Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 10)) == 5 : U32}
360
361law vec_array_find:
362  {Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 7)) == Some{3} : Maybe<&2, U32>}
363
364law vec_array_find_none:
365  {Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 8)) == None{} : Maybe<&2, U32>}
366
367# Witnesses: each hypothesis above can hold
368
369# first_set and last_set answer Some (40 = 0b101000: bits 3 and 5), with a
370# j below and above; and None for zero
371law wit_first_last:
372  {(A.bits32.first_set(40), Nat.is_lt(1n, 3n), A.bits32.last_set(40), Nat.is_lt(5n, 7n), A.bits32.first_set(0), A.bits32.last_set(0)) == (Some{3n}, True{}, Some{5n}, True{}, None{}, None{}) : Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Maybe<&2, Nat>}
373
374law wit_first_last64:
375  {(A.bits64.first_set(W.W64.from_parts(1, 0)), A.bits64.last_set(W.W64.from_parts(1, 0)), A.bits64.first_set(W.W64.zero())) == (Some{32n}, Some{32n}, None{}) : Maybe<&2, Nat> & Maybe<&2, Nat> & Maybe<&2, Nat>}
376
377# an answer below the size, and a j with start <= j < answer
378law wit_next:
379  {(Nat.is_lt(M.bitmap.next_set([0, 8], 64n, 3n), 64n), Nat.is_le(3n, 10n), Nat.is_lt(10n, M.bitmap.next_set([0, 8], 64n, 3n)), Nat.is_lt(M.bitmap.next_clear([4294967295, 1], 64n, 3n), 64n), Nat.is_lt(10n, M.bitmap.next_clear([4294967295, 1], 64n, 3n))) == (True{}, True{}, True{}, True{}, True{}) : Bool & Bool & Bool & Bool & Bool}
380
381# a sorted list; an element before the lower bound of 7 (index 1) and one
382# from it on (index 4); find answering Some and None
383law wit_bsearch:
384  {(S.bsearch.sorted([1, 3, 3, 7, 9]), S.bsearch.lower_bound([1, 3, 3, 7, 9], 7), List.get(&2, U32, [1, 3, 3, 7, 9], 1n), List.get(&2, U32, [1, 3, 3, 7, 9], 4n), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (True{}, 3n, Some{3}, Some{9}, Some{3n}, None{}) : Bool & Nat & Maybe<&2, U32> & Maybe<&2, U32> & Maybe<&2, Nat> & Maybe<&2, Nat>}
385
386# the array [1, 3, 3, 7, 9, 0, 0, 0] (depth 3), searched in its first 5
387# slots: perfect, of depth below 32, 5 <= 2^3, and those slots sorted
388law wit_array_bsearch:
389  {(AR.Arrays.is_perfect(U32, 3n, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9)), Nat.is_lt(3n, 32n), Nat.is_le(U32.to_nat(5), AR.Arrays.slots(3n)), S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9)), U32.to_nat(5)))) == (True{}, True{}, True{}, True{}) : Bool & Bool & Bool & Bool}