1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/hash_table.bend as S
6	import ../../lib/u32div.bend as UD
7	import ../../../src/math/hash.bend as HS
8	import ./modn.bend as M
9	import ./keys.bend as K
10	import ../../../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	
16	type Bk is Data:
17	  BE{}
18	  BF{w: U32, l: U32, k: String}
19	
20	def 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	
29	def 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
37	def 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
45	type MS is Data:
46	  MEnd{}
47	  MHit{l: U32}
48	  MNext{}
49	
50	def 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	
57	type Res is Data:
58	  RHit{at: Nat, l: U32}
59	  REnd{at: Nat}
60	
61	# the probe loop, shaped as the implementation's find
62	def 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
80	def 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	
87	def 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
95	def 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)
103	def 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
111	def 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
119	def 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	
126	def 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	
135	def 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	
142	def 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
150	def 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
162	def 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
170	def 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
178	type 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	
190	def implies(a: Bool, b: Bool) -> Bool:
191	  Bool.or(Bool.not(a), b)
192	
193	def 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
202	def 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	
209	def 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)
233	def 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	
240	def 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
248	def 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	
255	def 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	
262	def 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	
269	def cluster(+bs: List<&2, Bk>, +n: Nat, +mask: U32) -> Bool:
270	  all_lt(PClus{bs, n, mask}, n)
271	
272	# ---- the probe: correctness ----
273	
274	def 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	
281	def not_true_false(+e: {Bool.not(True{}) == True{} : Bool}) -> Empty:
282	  L.false_true(e)
283	
284	def occ_be(+e: {occ(BE{}) == True{} : Bool}) -> Empty:
285	  L.false_true(e)
286	
287	def 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
292	def 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
300	def 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	
306	def 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	
314	def 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	
326	def 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	
334	def 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
344	def 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	
357	def 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	
367	def 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.
378	def 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))