proofs/containers/hash_table/buckets.bend
bend-collections-laws-containers@1.0.0.0 · 385 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as M
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11
12# The bucket table as a list of n buckets, and the probe loop over it.
13# BE{} an empty bucket
14# BF{w, l, k} a full bucket: check word w, slot link l, holding key k
15
16type Bk is Data:
17 BE{}
18 BF{w: U32, l: U32, k: String}
19
20def at(bs: List<&2, Bk>, +i: Nat) -> Bk:
21 match bs i:
22 case Nil{} _:
23 BE{}
24 case Con{b, t} 0n:
25 b
26 case Con{b, t} 1n+p:
27 at(t, p)
28
29def occ(b: Bk) -> Bool:
30 match b:
31 case BE{}:
32 False{}
33 case BF{w, l, k}:
34 True{}
35
36# does bucket b hold key
37def hold(+key: String, b: Bk) -> Bool:
38 match b:
39 case BE{}:
40 False{}
41 case BF{w, l, k}:
42 S.str_eq(k, key)
43
44# one probe step on bucket b
45type MS is Data:
46 MEnd{}
47 MHit{l: U32}
48 MNext{}
49
50def mstep(+key: String, b: Bk) -> MS:
51 match b:
52 case BE{}:
53 MEnd{}
54 case BF{w, +l, k}:
55 Bool.pick(MS, S.str_eq(k, key), MHit{l}, MNext{})
56
57type Res is Data:
58 RHit{at: Nat, l: U32}
59 REnd{at: Nat}
60
61# the probe loop, shaped as the implementation's find
62def pf(+key: String, +bs: List<&2, Bk>, +n: Nat, fuel: Nat, s: MS, +i: Nat) -> Res:
63 match fuel s:
64 case 0n MEnd{}:
65 REnd{i}
66 case 0n MHit{l}:
67 RHit{i, l}
68 case 0n MNext{}:
69 REnd{i}
70 case 1n+p MEnd{}:
71 REnd{i}
72 case 1n+p MHit{l}:
73 RHit{i, l}
74 case 1n+p MNext{}:
75 pf(key, bs, n, p, mstep(key, at(bs, Nat.mod(1n+i, n))), Nat.mod(1n+i, n))
76
77# ---- invariants ----
78
79# the home bucket of a full bucket's word
80def hb(+mask: U32, b: Bk) -> Nat:
81 match b:
82 case BE{}:
83 0n
84 case BF{+w, l, k}:
85 UD.v(HS.bucket(w, mask))
86
87def hold_occ(+key: String, +b: Bk, +h: {hold(key, b) == True{} : Bool}) -> {occ(b) == True{} : Bool}:
88 match b:
89 case BE{}:
90 Empty.absurd({occ(BE{}) == True{} : Bool}, L.false_true(h))
91 case BF{w, l, k}:
92 {==}
93
94# the first m buckets from h are full
95def occpath(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +m: Nat) -> Bool:
96 match m:
97 case 0n:
98 True{}
99 case 1n+s:
100 Bool.and(occ(at(bs, M.pos(n, h, s))), occpath(bs, n, h, s))
101
102# (an empty bucket's link is never read; 1 keeps slot(link) small)
103def lnk(b: Bk) -> U32:
104 match b:
105 case BE{}:
106 1
107 case BF{w, l, k}:
108 l
109
110# no bucket below i holds key
111def nohb(+bs: List<&2, Bk>, +key: String, +i: Nat) -> Bool:
112 match i:
113 case 0n:
114 True{}
115 case 1n+j:
116 Bool.and(Bool.not(hold(key, at(bs, j))), nohb(bs, key, j))
117
118# no full bucket below i has link l
119def nolb(+bs: List<&2, Bk>, +l: U32, +i: Nat) -> Bool:
120 match i:
121 case 0n:
122 True{}
123 case 1n+j:
124 Bool.and(Bool.not(Bool.and(occ(at(bs, j)), U32.is_eq(lnk(at(bs, j)), l))), nolb(bs, l, j))
125
126def nthb(bs: List<&2, Bool>, +i: Nat) -> Bool:
127 match bs i:
128 case Nil{} _:
129 False{}
130 case Con{b, t} 0n:
131 b
132 case Con{b, t} 1n+p:
133 nthb(t, p)
134
135def uq_b(+bs: List<&2, Bk>, +i: Nat, b: Bk) -> Bool:
136 match b:
137 case BE{}:
138 True{}
139 case BF{w, +l, +k}:
140 Bool.and(nohb(bs, k, i), nolb(bs, l, i))
141
142def live_b(+lv: List<&2, Bool>, +f: Nat, b: Bk) -> Bool:
143 match b:
144 case BE{}:
145 True{}
146 case BF{w, +l, k}:
147 Bool.and(nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), f))
148
149# equal buckets, as a Bool
150def bk_eq(a: Bk, b: Bk) -> Bool:
151 match a b:
152 case BE{} BE{}:
153 True{}
154 case BE{} BF{w, l, k}:
155 False{}
156 case BF{w, l, k} BE{}:
157 False{}
158 case BF{+w, +l, +k} BF{+w2, +l2, +k2}:
159 Bool.and(U32.is_eq(w, w2), Bool.and(U32.is_eq(l, l2), S.str_eq(k, k2)))
160
161# some bucket below m equals b
162def anyeq(+bs: List<&2, Bk>, +m: Nat, +b: Bk) -> Bool:
163 match m:
164 case 0n:
165 False{}
166 case 1n+j:
167 Bool.or(bk_eq(at(bs, j), b), anyeq(bs, j, b))
168
169# the first m buckets from a are full, except possibly the bucket at h
170def opx(+bs: List<&2, Bk>, +n: Nat, +a: Nat, +m: Nat, +h: Nat) -> Bool:
171 match m:
172 case 0n:
173 True{}
174 case 1n+s:
175 Bool.and(Bool.or(Nat.is_eq(h, M.pos(n, a, s)), occ(at(bs, M.pos(n, a, s)))), opx(bs, n, a, s, h))
176
177# bounded quantifiers over first-order predicates
178type Pred is Data:
179 PClus{bs: List<&2, Bk>, n: Nat, mask: U32}
180 PVis{bs: List<&2, Bk>, n: Nat, h: Nat, key: String}
181 PHome{bs: List<&2, Bk>, mask: U32, key: String, h: Nat}
182 PNo{bs: List<&2, Bk>, key: String}
183 PWell{bs: List<&2, Bk>, sd: Nat}
184 PUniq{bs: List<&2, Bk>}
185 PLive{bs: List<&2, Bk>, lv: List<&2, Bool>, f: Nat}
186 PFrom{bs: List<&2, Bk>, src: List<&2, Bk>, m: Nat}
187 PTo{bs: List<&2, Bk>, dst: List<&2, Bk>, m: Nat}
188 PHole{bs: List<&2, Bk>, n: Nat, mask: U32, h: Nat, dk: Nat}
189
190def implies(a: Bool, b: Bool) -> Bool:
191 Bool.or(Bool.not(a), b)
192
193def imp_elim(+a: Bool, +b: Bool, +h: {implies(a, b) == True{} : Bool}, +ha: {a == True{} : Bool}) -> {b == True{} : Bool}:
194 match a:
195 case True{}:
196 h
197 case False{}:
198 Empty.absurd({b == True{} : Bool}, L.false_true(ha))
199
200# a full bucket's link is a slot of the arena (2^sd slots) and its word is
201# its key's word
202def wb(+sd: Nat, b: Bk) -> Bool:
203 match b:
204 case BE{}:
205 True{}
206 case BF{+w, +l, +k}:
207 Bool.and(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(w, K.kword(k)), Bool.not(U32.is_eq(l, 0))))
208
209def eval(p: Pred, +i: Nat) -> Bool:
210 match p:
211 case PClus{+bs, +n, +mask}:
212 implies(occ(at(bs, i)), occpath(bs, n, hb(mask, at(bs, i)), M.dist(n, hb(mask, at(bs, i)), i)))
213 case PVis{+bs, +n, +h, +key}:
214 Bool.and(occ(at(bs, M.pos(n, h, i))), Bool.not(hold(key, at(bs, M.pos(n, h, i)))))
215 case PHome{+bs, +mask, +key, +h}:
216 implies(hold(key, at(bs, i)), Nat.is_eq(hb(mask, at(bs, i)), h))
217 case PNo{+bs, +key}:
218 Bool.not(hold(key, at(bs, i)))
219 case PWell{+bs, +sd}:
220 wb(sd, at(bs, i))
221 case PUniq{+bs}:
222 uq_b(bs, i, at(bs, i))
223 case PLive{+bs, +lv, +f}:
224 live_b(lv, f, at(bs, i))
225 case PFrom{+bs, +src, +m}:
226 implies(occ(at(bs, i)), anyeq(src, m, at(bs, i)))
227 case PTo{+bs, +dst, +m}:
228 implies(occ(at(bs, i)), anyeq(dst, m, at(bs, i)))
229 case PHole{+bs, +n, +mask, +h, +dk}:
230 implies(occ(at(bs, i)), Bool.and(opx(bs, n, hb(mask, at(bs, i)), M.dist(n, hb(mask, at(bs, i)), i), h), implies(Nat.is_lt(M.dist(n, hb(mask, at(bs, i)), h), M.dist(n, hb(mask, at(bs, i)), i)), Nat.is_le(dk, M.dist(n, h, i)))))
231
232# p(0) && ... && p(n - 1)
233def all_lt(+p: Pred, +n: Nat) -> Bool:
234 match n:
235 case 0n:
236 True{}
237 case 1n+q:
238 Bool.and(eval(p, q), all_lt(p, q))
239
240def all_inst_c(+p: Pred, +q: Nat, +h: {Bool.and(eval(p, q), all_lt(p, q)) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, q) == c : Bool}, rec: @hlt: {Nat.is_lt(i, q) == True{} : Bool} -> {eval(p, i) == True{} : Bool}) -> {eval(p, i) == True{} : Bool}:
241 match c:
242 case True{}:
243 L.subst(Nat, z => {eval(p, z) == True{} : Bool}, q, i, Equal.sym(Nat, i, q, N.eq_from_is_eq(i, q, hc)), L.and_left(eval(p, q), all_lt(p, q), h))
244 case False{}:
245 rec(N.lt_or_eq(i, q, N.lt_succ_le(i, q, hi), hc))
246
247# an instance of a bounded quantifier
248def all_inst(+p: Pred, +n: Nat, +h: {all_lt(p, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {eval(p, i) == True{} : Bool}:
249 match n:
250 case 0n:
251 Empty.absurd({eval(p, i) == True{} : Bool}, N.lt_zero_absurd(i, hi))
252 case 1n+q:
253 all_inst_c(p, q, h, i, hi, Nat.is_eq(i, q), {==}, hlt => all_inst(p, q, L.and_right(eval(p, q), all_lt(p, q), h), i, hlt))
254
255def occ_c(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +q: Nat, +hp: {Bool.and(occ(at(bs, M.pos(n, h, q))), occpath(bs, n, h, q)) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, q) == c : Bool}, rec: @hlt: {Nat.is_lt(i, q) == True{} : Bool} -> {occ(at(bs, M.pos(n, h, i))) == True{} : Bool}) -> {occ(at(bs, M.pos(n, h, i))) == True{} : Bool}:
256 match c:
257 case True{}:
258 L.subst(Nat, z => {occ(at(bs, M.pos(n, h, z))) == True{} : Bool}, q, i, Equal.sym(Nat, i, q, N.eq_from_is_eq(i, q, hc)), L.and_left(occ(at(bs, M.pos(n, h, q))), occpath(bs, n, h, q), hp))
259 case False{}:
260 rec(N.lt_or_eq(i, q, N.lt_succ_le(i, q, hi), hc))
261
262def occ_inst(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +m: Nat, +hp: {occpath(bs, n, h, m) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, m) == True{} : Bool}) -> {occ(at(bs, M.pos(n, h, i))) == True{} : Bool}:
263 match m:
264 case 0n:
265 Empty.absurd({occ(at(bs, M.pos(n, h, i))) == True{} : Bool}, N.lt_zero_absurd(i, hi))
266 case 1n+q:
267 occ_c(bs, n, h, q, hp, i, hi, Nat.is_eq(i, q), {==}, hlt => occ_inst(bs, n, h, q, L.and_right(occ(at(bs, M.pos(n, h, q))), occpath(bs, n, h, q), hp), i, hlt))
268
269def cluster(+bs: List<&2, Bk>, +n: Nat, +mask: U32) -> Bool:
270 all_lt(PClus{bs, n, mask}, n)
271
272# ---- the probe: correctness ----
273
274def ResOK(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +key: String, r: Res) -> Type:
275 match r:
276 case RHit{+i, +l}:
277 {Nat.is_lt(i, n) == True{} : Bool} & ({hold(key, at(bs, i)) == True{} : Bool} & {lnk(at(bs, i)) == l : U32})
278 case REnd{+e}:
279 {Nat.is_lt(e, n) == True{} : Bool} & ({at(bs, e) == BE{} : Bk} & ({occpath(bs, n, h, M.dist(n, h, e)) == True{} : Bool} & {all_lt(PNo{bs, key}, n) == True{} : Bool}))
280
281def not_true_false(+e: {Bool.not(True{}) == True{} : Bool}) -> Empty:
282 L.false_true(e)
283
284def occ_be(+e: {occ(BE{}) == True{} : Bool}) -> Empty:
285 L.false_true(e)
286
287def occ_at_be(+bs: List<&2, Bk>, +i: Nat, +hz: {at(bs, i) == BE{} : Bk}, +ho: {occ(at(bs, i)) == True{} : Bool}) -> Empty:
288 occ_be(L.subst(Bk, b => {occ(b) == True{} : Bool}, at(bs, i), BE{}, hz, ho))
289
290# the probe stopped at the empty bucket pos(h, t), and d >= t is a full
291# key's distance: impossible
292def nh_far(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +t: Nat, +d: Nat, +hz: {at(bs, M.pos(n, h, t)) == BE{} : Bk}, +hp: {occpath(bs, n, h, d) == True{} : Bool}, +oj: {occ(at(bs, M.pos(n, h, d))) == True{} : Bool}, +htd: {Nat.is_le(t, d) == True{} : Bool}, +b2: Bool, +hb2: {Nat.is_eq(t, d) == b2 : Bool}) -> Empty:
293 match b2:
294 case True{}:
295 occ_at_be(bs, M.pos(n, h, t), hz, L.subst(Nat, z => {occ(at(bs, M.pos(n, h, z))) == True{} : Bool}, d, t, Equal.sym(Nat, t, d, N.eq_from_is_eq(t, d, hb2)), oj))
296 case False{}:
297 occ_at_be(bs, M.pos(n, h, t), hz, occ_inst(bs, n, h, d, hp, t, N.lt_or_eq(t, d, htd, hb2)))
298
299# ... and d < t is a visited bucket, which does not hold the key: impossible
300def nh_near(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +t: Nat, +key: String, +d: Nat, +j: Nat, +hv: {all_lt(PVis{bs, n, h, key}, t) == True{} : Bool}, +hpj: {M.pos(n, h, d) == j : Nat}, +hk: {hold(key, at(bs, j)) == True{} : Bool}, +hdt: {Nat.is_lt(d, t) == True{} : Bool}) -> Empty:
301 +vd = all_inst(PVis{bs, n, h, key}, t, hv, d, hdt)
302 +nd = L.and_right(occ(at(bs, M.pos(n, h, d))), Bool.not(hold(key, at(bs, M.pos(n, h, d)))), vd)
303 +nj = L.subst(Nat, z => {Bool.not(hold(key, at(bs, z))) == True{} : Bool}, M.pos(n, h, d), j, hpj, nd)
304 not_true_false(L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, hold(key, at(bs, j)), True{}, hk, nj))
305
306def nh_split(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +t: Nat, +key: String, +d: Nat, +j: Nat, +hv: {all_lt(PVis{bs, n, h, key}, t) == True{} : Bool}, +hz: {at(bs, M.pos(n, h, t)) == BE{} : Bk}, +hp: {occpath(bs, n, h, d) == True{} : Bool}, +hpj: {M.pos(n, h, d) == j : Nat}, +hk: {hold(key, at(bs, j)) == True{} : Bool}, +b1: Bool, +hb1: {Nat.is_lt(d, t) == b1 : Bool}) -> Empty:
307 match b1:
308 case True{}:
309 nh_near(bs, n, h, t, key, d, j, hv, hpj, hk, hb1)
310 case False{}:
311 +oj = L.subst(Nat, z => {occ(at(bs, z)) == True{} : Bool}, j, M.pos(n, h, d), Equal.sym(Nat, M.pos(n, h, d), j, hpj), hold_occ(key, at(bs, j), hk))
312 nh_far(bs, n, h, t, d, hz, hp, oj, N.not_lt_le(d, t, hb1), Nat.is_eq(t, d), {==})
313
314def nh_c(+bs: List<&2, Bk>, +bp: Nat, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +cl: {cluster(bs, 1n+bp, mask) == True{} : Bool}, +ho: {all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool}, +t: Nat, +hv: {all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool}, +hz: {at(bs, M.pos(1n+bp, h, t)) == BE{} : Bk}, +j: Nat, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}, +c: Bool, +hc: {hold(key, at(bs, j)) == c : Bool}) -> {Bool.not(hold(key, at(bs, j))) == True{} : Bool}:
315 match c:
316 case False{}:
317 L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, False{}, hold(key, at(bs, j)), Equal.sym(Bool, hold(key, at(bs, j)), False{}, hc), {==})
318 case True{}:
319 +n = {1n+bp : Nat}
320 +hbj = hb(mask, at(bs, j))
321 +hom = N.eq_from_is_eq(hbj, h, imp_elim(hold(key, at(bs, j)), Nat.is_eq(hbj, h), all_inst(PHome{bs, mask, key, h}, n, ho, j, hj), hc))
322 +clj = imp_elim(occ(at(bs, j)), occpath(bs, n, hbj, M.dist(n, hbj, j)), all_inst(PClus{bs, n, mask}, n, cl, j, hj), hold_occ(key, at(bs, j), hc))
323 +hp = L.subst(Nat, z => {occpath(bs, n, z, M.dist(n, z, j)) == True{} : Bool}, hbj, h, hom, clj)
324 Empty.absurd({Bool.not(hold(key, at(bs, j))) == True{} : Bool}, nh_split(bs, n, h, t, key, M.dist(n, h, j), j, hv, hz, hp, M.pos_dist(bp, h, j, hh, hj), hc, Nat.is_lt(M.dist(n, h, j), t), {==}))
325
326def nh_all(+bs: List<&2, Bk>, +bp: Nat, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +cl: {cluster(bs, 1n+bp, mask) == True{} : Bool}, +ho: {all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool}, +t: Nat, +hv: {all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool}, +hz: {at(bs, M.pos(1n+bp, h, t)) == BE{} : Bk}, +m: Nat, +hm: {Nat.is_le(m, 1n+bp) == True{} : Bool}) -> {all_lt(PNo{bs, key}, m) == True{} : Bool}:
327 match m:
328 case 0n:
329 {==}
330 case 1n+q:
331 +hq = N.succ_le_lt(q, 1n+bp, hm)
332 L.and_intro(Bool.not(hold(key, at(bs, q))), all_lt(PNo{bs, key}, q), nh_c(bs, bp, mask, key, h, hh, cl, ho, t, hv, hz, q, hq, hold(key, at(bs, q)), {==}), nh_all(bs, bp, mask, key, h, hh, cl, ho, t, hv, hz, q, N.lt_le(q, 1n+bp, hq)))
333
334def occ_of_vis(+bs: List<&2, Bk>, +n: Nat, +h: Nat, +key: String, +t: Nat, +hv: {all_lt(PVis{bs, n, h, key}, t) == True{} : Bool}) -> {occpath(bs, n, h, t) == True{} : Bool}:
335 match t:
336 case 0n:
337 {==}
338 case 1n+q:
339 +hq = L.and_left(eval(PVis{bs, n, h, key}, q), all_lt(PVis{bs, n, h, key}, q), hv)
340 L.and_intro(occ(at(bs, M.pos(n, h, q))), occpath(bs, n, h, q), L.and_left(occ(at(bs, M.pos(n, h, q))), Bool.not(hold(key, at(bs, M.pos(n, h, q)))), hq), occ_of_vis(bs, n, h, key, q, L.and_right(eval(PVis{bs, n, h, key}, q), all_lt(PVis{bs, n, h, key}, q), hv)))
341
342# the step past pos(h, t) stays inside the table: the empty bucket e0 lies
343# ahead
344def next_in(+bs: List<&2, Bk>, +bp: Nat, +h: Nat, +key: String, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +hz0: {at(bs, e0) == BE{} : Bk}, +t: Nat, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hv2: {all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(1n+t, 1n+bp) == c : Bool}) -> {Nat.is_lt(1n+t, 1n+bp) == True{} : Bool}:
345 match c:
346 case True{}:
347 hc
348 case False{}:
349 +n = {1n+bp : Nat}
350 +eq = N.le_antisym(1n+t, n, N.lt_succ_le_succ(t, n, ht), N.not_lt_le(1n+t, n, hc))
351 +d0 = M.dist(n, h, e0)
352 +hd0 = L.subst(Nat, z => {Nat.is_lt(d0, z) == True{} : Bool}, n, 1n+t, Equal.sym(Nat, 1n+t, n, eq), M.dist_lt(bp, h, e0))
353 +v0 = all_inst(PVis{bs, n, h, key}, 1n+t, hv2, d0, hd0)
354 +o0 = L.subst(Nat, z => {occ(at(bs, z)) == True{} : Bool}, M.pos(n, h, d0), e0, M.pos_dist(bp, h, e0, hh, he0), L.and_left(occ(at(bs, M.pos(n, h, d0))), Bool.not(hold(key, at(bs, M.pos(n, h, d0)))), v0))
355 Empty.absurd({Nat.is_lt(1n+t, n) == True{} : Bool}, occ_at_be(bs, e0, hz0, o0))
356
357def pf_bf(+bs: List<&2, Bk>, +bp: Nat, +key: String, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +hz0: {at(bs, e0) == BE{} : Bk}, +fp: Nat, +t: Nat, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hv: {all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool}, +x: U32, +l: U32, +k: String, +hb: {at(bs, M.pos(1n+bp, h, t)) == BF{x, l, k} : Bk}, +c: Bool, +hc: {S.str_eq(k, key) == c : Bool}, rec: @hv2: {all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool} -> @ht2: {Nat.is_lt(1n+t, 1n+bp) == True{} : Bool} -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, fp, mstep(key, at(bs, M.pos(1n+bp, h, 1n+t))), M.pos(1n+bp, h, 1n+t)))) -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, 1n+fp, Bool.pick(MS, c, MHit{l}, MNext{}), M.pos(1n+bp, h, t))):
358 match c:
359 case True{}:
360 (M.pos_lt(bp, h, t), (L.subst(Bk, b => {hold(key, b) == True{} : Bool}, BF{x, l, k}, at(bs, M.pos(1n+bp, h, t)), Equal.sym(Bk, at(bs, M.pos(1n+bp, h, t)), BF{x, l, k}, hb), hc), L.subst(Bk, b => {lnk(b) == l : U32}, BF{x, l, k}, at(bs, M.pos(1n+bp, h, t)), Equal.sym(Bk, at(bs, M.pos(1n+bp, h, t)), BF{x, l, k}, hb), {==})))
361 case False{}:
362 +vt = L.subst(Bk, b => {Bool.and(occ(b), Bool.not(hold(key, b))) == True{} : Bool}, BF{x, l, k}, at(bs, M.pos(1n+bp, h, t)), Equal.sym(Bk, at(bs, M.pos(1n+bp, h, t)), BF{x, l, k}, hb), L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, hc), {==}))
363 +hv2 = L.and_intro(eval(PVis{bs, 1n+bp, h, key}, t), all_lt(PVis{bs, 1n+bp, h, key}, t), vt, hv)
364 +ht2 = next_in(bs, bp, h, key, hh, e0, he0, hz0, t, ht, hv2, Nat.is_lt(1n+t, 1n+bp), {==})
365 L.subst(Nat, z => ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, fp, mstep(key, at(bs, z)), z)), M.pos(1n+bp, h, 1n+t), Nat.mod(1n+M.pos(1n+bp, h, t), 1n+bp), Equal.sym(Nat, Nat.mod(1n+M.pos(1n+bp, h, t), 1n+bp), M.pos(1n+bp, h, 1n+t), M.pos_next(bp, h, t)), rec(hv2, ht2))
366
367def pf_b(+bs: List<&2, Bk>, +bp: Nat, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +cl: {cluster(bs, 1n+bp, mask) == True{} : Bool}, +ho: {all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +hz0: {at(bs, e0) == BE{} : Bk}, +fp: Nat, +t: Nat, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hv: {all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool}, +b: Bk, +hb: {at(bs, M.pos(1n+bp, h, t)) == b : Bk}, rec: @hv2: {all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool} -> @ht2: {Nat.is_lt(1n+t, 1n+bp) == True{} : Bool} -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, fp, mstep(key, at(bs, M.pos(1n+bp, h, 1n+t))), M.pos(1n+bp, h, 1n+t)))) -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, 1n+fp, mstep(key, b), M.pos(1n+bp, h, t))):
368 match b:
369 case BE{}:
370 +op = L.subst(Nat, z => {occpath(bs, 1n+bp, h, z) == True{} : Bool}, t, M.dist(1n+bp, h, M.pos(1n+bp, h, t)), Equal.sym(Nat, M.dist(1n+bp, h, M.pos(1n+bp, h, t)), t, M.dist_pos(bp, h, t, hh, ht)), occ_of_vis(bs, 1n+bp, h, key, t, hv))
371 (M.pos_lt(bp, h, t), (hb, (op, nh_all(bs, bp, mask, key, h, hh, cl, ho, t, hv, hb, 1n+bp, N.le_refl(1n+bp)))))
372 case BF{+x, +l, +k}:
373 pf_bf(bs, bp, key, h, hh, e0, he0, hz0, fp, t, ht, hv, x, l, k, hb, S.str_eq(k, key), {==}, rec)
374
375# THEOREM (bucket level): the probe from offset t of h, with the first t
376# buckets full and not holding key and enough fuel, hits the bucket holding
377# key or ends at an empty bucket whose path from h is full, key held nowhere.
378def pf_ok(+bs: List<&2, Bk>, +bp: Nat, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +cl: {cluster(bs, 1n+bp, mask) == True{} : Bool}, +ho: {all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, 1n+bp) == True{} : Bool}, +hz0: {at(bs, e0) == BE{} : Bk}, +f: Nat, +t: Nat, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}, +hft: {Nat.add(t, f) == 1n+bp : Nat}, +hv: {all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool}) -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, f, mstep(key, at(bs, M.pos(1n+bp, h, t))), M.pos(1n+bp, h, t))):
379 match f:
380 case 0n:
381 +et = Equal.trans(Nat, t, Nat.add(t, 0n), 1n+bp, Equal.sym(Nat, Nat.add(t, 0n), t, N.add_zero(t)), hft)
382 Empty.absurd(ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, 0n, mstep(key, at(bs, M.pos(1n+bp, h, t))), M.pos(1n+bp, h, t))), N.lt_ne(t, 1n+bp, ht, et))
383 case 1n+fp:
384 +hft2 = Equal.trans(Nat, 1n+Nat.add(t, fp), Nat.add(t, 1n+fp), 1n+bp, Equal.sym(Nat, Nat.add(t, 1n+fp), 1n+Nat.add(t, fp), N.add_succ(t, fp)), hft)
385 pf_b(bs, bp, mask, key, h, hh, cl, ho, e0, he0, hz0, fp, t, ht, hv, at(bs, M.pos(1n+bp, h, t)), {==}, hv2 => ht2 => pf_ok(bs, bp, mask, key, h, hh, cl, ho, e0, he0, hz0, fp, 1n+t, ht2, hft2, hv2))