1	# Proof helpers for bend-osdev-algo: the Array binary search, through
2	# bend-osdev-array's laws. PROOF.bend uses them for the laws that tie
3	# bsearch.array_lower_bound and bsearch.array_find to the list reference.
4	#
5	# A perfect array is reflected, once, into Arrays.of_list(d, l, 0) for a
6	# Data list l (array's `reflect`); array's of_list_get then turns each read
7	# of the search into a literal pair: the same array, and the element of l at
8	# the masked index. So the search on the array is bq.run, the same halving
9	# on Data (bq.go), which hands the array back. The value of each index is
10	# then followed as a Nat (proof_u32.bend): mid is lo + (hi - lo) / 2, and a
11	# halving at least halves hi - lo.
12	import Base
13	import ./bsearch.bend as S
14	import bend-osdev-array@0.1.0.0/array.bend as A
15	import bend-osdev-array@0.1.0.0/LAWS.bend as AL
16	import bend-osdev-array@0.1.0.0/PROOF.bend as APF
17	import ./proof_u32.bend as U
18	
19	# Shorthands (they unfold to the defs they name)
20	
21	def bq.ol(+d: Nat, +l: List<&2, U32>) -> Array<U32>:
22	  A.Arrays.of_list(U32, d, l, 0)
23	
24	def bq.mid(+lo: U32, +hi: U32) -> U32:
25	  U32.add(lo, U32.shr(U32.sub(hi, lo)))
26	
27	# the element the search reads between lo and hi
28	def bq.x(+d: Nat, +l: List<&2, U32>, +lo: U32, +hi: U32) -> U32:
29	  A.Arrays.nth(U32, l, A.Arrays.index(d, bq.mid(lo, hi)), 0)
30	
31	# the searched prefix, its lower bound, and the range's size and middle as
32	# Nats
33	def bq.pre(+l: List<&2, U32>, +n: U32) -> List<&2, U32>:
34	  List.take(&2, U32, l, U32.to_nat(n))
35	
36	def bq.lb(+l: List<&2, U32>, +n: U32, +key: U32) -> Nat:
37	  S.bsearch.lower_bound(List.take(&2, U32, l, U32.to_nat(n)), key)
38	
39	def bq.s(+lo: U32, +hi: U32) -> Nat:
40	  Nat.sub(U32.to_nat(hi), U32.to_nat(lo))
41	
42	def bq.m(+lo: U32, +hi: U32) -> Nat:
43	  Nat.add(U32.to_nat(lo), U.uq.half(Nat.sub(U32.to_nat(hi), U32.to_nat(lo))))
44	
45	# The search on Data: one halving of [lo, hi), as bsearch.array.advance
46	
47	def bq.lo_b(b: Bool, +lo: U32, +mid: U32) -> U32:
48	  match b:
49	    case True{}:
50	      U32.inc(mid)
51	    case False{}:
52	      lo
53	
54	def bq.hi_b(b: Bool, +hi: U32, +mid: U32) -> U32:
55	  match b:
56	    case True{}:
57	      hi
58	    case False{}:
59	      mid
60	
61	def bq.nlo.a(c: Bool, b: Bool, +lo: U32, +mid: U32) -> U32:
62	  match c:
63	    case True{}:
64	      bq.lo_b(b, lo, mid)
65	    case False{}:
66	      lo
67	
68	def bq.nhi.a(c: Bool, b: Bool, +hi: U32, +mid: U32) -> U32:
69	  match c:
70	    case True{}:
71	      bq.hi_b(b, hi, mid)
72	    case False{}:
73	      hi
74	
75	def bq.nlo(+d: Nat, +l: List<&2, U32>, +lo: U32, +hi: U32, +key: U32) -> U32:
76	  bq.nlo.a(U32.is_lt(lo, hi), U32.is_lt(bq.x(d, l, lo, hi), key), lo, bq.mid(lo, hi))
77	
78	def bq.nhi(+d: Nat, +l: List<&2, U32>, +lo: U32, +hi: U32, +key: U32) -> U32:
79	  bq.nhi.a(U32.is_lt(lo, hi), U32.is_lt(bq.x(d, l, lo, hi), key), hi, bq.mid(lo, hi))
80	
81	# f halvings, then lo
82	def bq.run(f: Nat, +d: Nat, +l: List<&2, U32>, +lo: U32, +hi: U32, +key: U32) -> U32:
83	  match f:
84	    case 0n:
85	      lo
86	    case 1n+g:
87	      bq.run(g, d, l, bq.nlo(d, l, lo, hi, key), bq.nhi(d, l, lo, hi, key), key)
88	
89	# The search on a reflected array is the search on Data
90	
91	def bq.pick_eq(b: Bool, -a: Array<U32>, +lo: U32, +hi: U32, +mid: U32) -> {S.bsearch.array.pick(b, a, lo, hi, mid) == S.BsearchState{a, bq.lo_b(b, lo, mid), bq.hi_b(b, hi, mid)} : S.BsearchState}:
92	  match b:
93	    case True{}:
94	      {==}
95	    case False{}:
96	      {==}
97	
98	def bq.step_eq(c: Bool, -a: Array<U32>, +x: U32, +key: U32, +lo: U32, +hi: U32, +mid: U32) -> {S.bsearch.array.step(c, (a, x), key, lo, hi, mid) == S.BsearchState{a, bq.nlo.a(c, U32.is_lt(x, key), lo, mid), bq.nhi.a(c, U32.is_lt(x, key), hi, mid)} : S.BsearchState}:
99	  match c:
100	    case True{}:
101	      bq.pick_eq(U32.is_lt(x, key), a, lo, hi, mid)
102	    case False{}:
103	      {==}
104	
105	def bq.go(f: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +lo: U32, +hi: U32, +key: U32) -> {S.bsearch.array.go(f, S.BsearchState{bq.ol(d, l), lo, hi}, key) == (bq.ol(d, l), bq.run(f, d, l, lo, hi, key)) : Array<U32> & U32}:
106	  match f:
107	    case 0n:
108	      {==}
109	    case 1n+ +g:
110	      -a0 = bq.ol(d, l)
111	      +mid = bq.mid(lo, hi)
112	      +x = bq.x(d, l, lo, hi)
113	      %Equal.sym(Array<U32> & U32, Array.get(U32, a0, mid), (a0, x), AL.of_list_get(U32, d, l, 0, hl, hd, mid)) : {S.bsearch.array.go(g, S.bsearch.array.step(U32.is_lt(lo, hi), _, key, lo, hi, mid), key) == (a0, bq.run(1n+g, d, l, lo, hi, key)) : Array<U32> & U32}
114	      %Equal.sym(S.BsearchState, S.bsearch.array.step(U32.is_lt(lo, hi), (a0, x), key, lo, hi, mid), S.BsearchState{a0, bq.nlo(d, l, lo, hi, key), bq.nhi(d, l, lo, hi, key)}, bq.step_eq(U32.is_lt(lo, hi), a0, x, key, lo, hi, mid)) : {S.bsearch.array.go(g, _, key) == (a0, bq.run(1n+g, d, l, lo, hi, key)) : Array<U32> & U32}
115	      bq.go(g, d, l, hl, hd, bq.nlo(d, l, lo, hi, key), bq.nhi(d, l, lo, hi, key), key)
116	
117	# Contradictions
118	
119	def bq.bt(b: Bool) -> Type:
120	  match b:
121	    case True{}:
122	      Unit
123	    case False{}:
124	      Empty
125	
126	def bq.ft(e: {False{} == True{} : Bool}) -> Empty:
127	  %Equal.sym(Bool, False{}, True{}, e) : bq.bt(_)
128	  Unit{}
129	
130	def bq.tf(e: {True{} == False{} : Bool}) -> Empty:
131	  %e : bq.bt(_)
132	  Unit{}
133	
134	def bq.nt(n: Nat) -> Type:
135	  match n:
136	    case 0n:
137	      Unit
138	    case 1n+p:
139	      Empty
140	
141	def bq.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
142	  %Equal.sym(Nat, 1n+k, 0n, e) : bq.nt(_)
143	  Unit{}
144	
145	# Nat order
146	
147	def bq.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
148	  match x:
149	    case 0n:
150	      {==}
151	    case 1n+p:
152	      {==}
153	
154	def bq.le_refl(x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
155	  match x:
156	    case 0n:
157	      {==}
158	    case 1n+p:
159	      bq.le_refl(p)
160	
161	def bq.le_succ_r(x: Nat, y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x, 1n+y) == True{} : Bool}:
162	  match x y:
163	    case 0n _:
164	      {==}
165	    case 1n+xp 0n:
166	      Empty.absurd({Nat.is_le(1n+xp, 1n) == True{} : Bool}, bq.ft(h))
167	    case 1n+xp 1n+yp:
168	      bq.le_succ_r(xp, yp, h)
169	
170	def bq.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
171	  match x y:
172	    case 0n _:
173	      bq.le_zero(y)
174	    case 1n+xp 0n:
175	      Empty.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, bq.ft(h))
176	    case 1n+xp 1n+yp:
177	      bq.lt_le(xp, yp, h)
178	
179	def bq.le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
180	  match a b c:
181	    case 0n _ _:
182	      bq.le_zero(c)
183	    case 1n+ap 0n _:
184	      Empty.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, bq.ft(e))
185	    case 1n+ap 1n+bp 0n:
186	      Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, bq.ft(f))
187	    case 1n+ap 1n+bp 1n+cp:
188	      bq.le_trans(ap, bp, cp, e, f)
189	
190	def bq.lt_le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
191	  match a b c:
192	    case 0n 0n _:
193	      Empty.absurd({Nat.is_lt(0n, c) == True{} : Bool}, bq.ft(e))
194	    case 0n 1n+bp 0n:
195	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(f))
196	    case 0n 1n+bp 1n+cp:
197	      {==}
198	    case 1n+ap 0n _:
199	      Empty.absurd({Nat.is_lt(1n+ap, c) == True{} : Bool}, bq.ft(e))
200	    case 1n+ap 1n+bp 0n:
201	      Empty.absurd({Nat.is_lt(1n+ap, 0n) == True{} : Bool}, bq.ft(f))
202	    case 1n+ap 1n+bp 1n+cp:
203	      bq.lt_le_trans(ap, bp, cp, e, f)
204	
205	def bq.le_antisym(x: Nat, y: Nat, h1: {Nat.is_le(x, y) == True{} : Bool}, h2: {Nat.is_le(y, x) == True{} : Bool}) -> {x == y : Nat}:
206	  match x y:
207	    case 0n 0n:
208	      {==}
209	    case 0n 1n+yp:
210	      Empty.absurd({0n == 1n+yp : Nat}, bq.ft(h2))
211	    case 1n+xp 0n:
212	      Empty.absurd({1n+xp == 0n : Nat}, bq.ft(h1))
213	    case 1n+xp 1n+yp:
214	      U.uq.succ_cong(xp, yp, bq.le_antisym(xp, yp, h1, h2))
215	
216	def bq.not_lt(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
217	  match x y:
218	    case 0n 0n:
219	      {==}
220	    case 0n 1n+yp:
221	      Empty.absurd({Nat.is_le(1n+yp, 0n) == True{} : Bool}, bq.tf(e))
222	    case 1n+xp 0n:
223	      {==}
224	    case 1n+xp 1n+yp:
225	      bq.not_lt(xp, yp, e)
226	
227	def bq.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
228	  match x:
229	    case 0n:
230	      {==}
231	    case 1n+p:
232	      match p:
233	        case 0n:
234	          Empty.absurd({1n == 0n : Nat}, bq.ft(e))
235	        case 1n+q:
236	          Empty.absurd({2n+q == 0n : Nat}, bq.ft(e))
237	
238	def bq.lt_succ_le(x: Nat, y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
239	  match x y:
240	    case 0n _:
241	      {==}
242	    case 1n+xp 0n:
243	      Empty.absurd({Nat.is_lt(1n+xp, 1n) == True{} : Bool}, bq.ft(h))
244	    case 1n+xp 1n+yp:
245	      bq.lt_succ_le(xp, yp, h)
246	
247	def bq.lt_rw(-x: Nat, -y: Nat, -x2: Nat, -y2: Nat, ex: {x == x2 : Nat}, ey: {y == y2 : Nat}, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x2, y2) == True{} : Bool}:
248	  %ex : {Nat.is_lt(_, y2) == True{} : Bool}
249	  %ey : {Nat.is_lt(x, _) == True{} : Bool}
250	  h
251	
252	def bq.le_rw(-x: Nat, -y: Nat, -x2: Nat, -y2: Nat, ex: {x == x2 : Nat}, ey: {y == y2 : Nat}, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(x2, y2) == True{} : Bool}:
253	  %ex : {Nat.is_le(_, y2) == True{} : Bool}
254	  %ey : {Nat.is_le(x, _) == True{} : Bool}
255	  h
256	
257	def bq.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
258	  match s:
259	    case 0n:
260	      {==}
261	    case 1n+p:
262	      bq.lt_cancel(p, r, u)
263	
264	def bq.pw_pos(f: Nat) -> {Nat.is_lt(0n, U.uq.pw(f)) == True{} : Bool}:
265	  match f:
266	    case 0n:
267	      {==}
268	    case 1n+ +g:
269	      U.uq.lt_dbl_self(0n, U.uq.pw(g), bq.pw_pos(g))
270	
271	# Nat arithmetic
272	
273	def bq.sub_zero(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
274	  match x:
275	    case 0n:
276	      {==}
277	    case 1n+p:
278	      {==}
279	
280	def bq.add_sub(d: Nat, s: Nat, e: {Nat.is_le(d, s) == True{} : Bool}) -> {Nat.add(d, Nat.sub(s, d)) == s : Nat}:
281	  match d s:
282	    case 0n +ss:
283	      bq.sub_zero(ss)
284	    case 1n+dp 0n:
285	      Empty.absurd({1n+Nat.add(dp, 0n) == 0n : Nat}, bq.ft(e))
286	    case 1n+ +dp 1n+ +sp:
287	      U.uq.succ_cong(Nat.add(dp, Nat.sub(sp, dp)), sp, bq.add_sub(dp, sp, e))
288	
289	def bq.sub_cancel(l: Nat, -s: Nat, -t: Nat) -> {Nat.sub(Nat.add(l, s), Nat.add(l, t)) == Nat.sub(s, t) : Nat}:
290	  match l:
291	    case 0n:
292	      {==}
293	    case 1n+p:
294	      bq.sub_cancel(p, s, t)
295	
296	def bq.sub_pos(l: Nat, h: Nat, e: {Nat.is_lt(l, h) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(h, l)) == True{} : Bool}:
297	  match l h:
298	    case 0n 0n:
299	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(e))
300	    case 0n 1n+hp:
301	      {==}
302	    case 1n+lp 0n:
303	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(e))
304	    case 1n+lp 1n+hp:
305	      bq.sub_pos(lp, hp, e)
306	
307	def bq.sub_le0(h: Nat, l: Nat, e: {Nat.is_le(h, l) == True{} : Bool}) -> {Nat.sub(h, l) == 0n : Nat}:
308	  match h l:
309	    case 0n _:
310	      {==}
311	    case 1n+hp 0n:
312	      Empty.absurd({1n+hp == 0n : Nat}, bq.ft(e))
313	    case 1n+hp 1n+lp:
314	      bq.sub_le0(hp, lp, e)
315	
316	def bq.sub0_le(h: Nat, l: Nat, e: {Nat.sub(h, l) == 0n : Nat}) -> {Nat.is_le(h, l) == True{} : Bool}:
317	  match h l:
318	    case 0n 0n:
319	      {==}
320	    case 0n 1n+lp:
321	      {==}
322	    case 1n+hp 0n:
323	      Empty.absurd({Nat.is_le(1n+hp, 0n) == True{} : Bool}, bq.sz(hp, e))
324	    case 1n+hp 1n+lp:
325	      bq.sub0_le(hp, lp, e)
326	
327	def bq.sub_step(q: Nat, k: Nat) -> {Nat.is_le(Nat.sub(q, k), 1n+Nat.sub(q, 1n+k)) == True{} : Bool}:
328	  match q k:
329	    case 0n _:
330	      {==}
331	    case 1n+ +qp 0n:
332	      %Equal.sym(Nat, Nat.sub(qp, 0n), qp, bq.sub_zero(qp)) : {Nat.is_le(1n+qp, 1n+_) == True{} : Bool}
333	      bq.le_refl(qp)
334	    case 1n+qp 1n+kp:
335	      bq.sub_step(qp, kp)
336	
337	# Halving
338	
339	def bq.half_le(q: Nat) -> {Nat.is_le(U.uq.half(q), q) == True{} : Bool}:
340	  match q:
341	    case 0n:
342	      {==}
343	    case 1n+p:
344	      match p:
345	        case 0n:
346	          {==}
347	        case 1n+ +r:
348	          bq.le_succ_r(U.uq.half(r), r, bq.half_le(r))
349	
350	def bq.half_lt(s: Nat, h: {Nat.is_lt(0n, s) == True{} : Bool}) -> {Nat.is_lt(U.uq.half(s), s) == True{} : Bool}:
351	  match s:
352	    case 0n:
353	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
354	    case 1n+p:
355	      match p:
356	        case 0n:
357	          {==}
358	        case 1n+ +q:
359	          bq.lt_succ_le(U.uq.half(q), q, bq.half_le(q))
360	
361	# s < 2p: s / 2 < p
362	def bq.half_lt_pw(s: Nat, p: Nat, h: {Nat.is_lt(s, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(U.uq.half(s), p) == True{} : Bool}:
363	  match s:
364	    case 0n:
365	      match p:
366	        case 0n:
367	          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
368	        case 1n+pp:
369	          {==}
370	    case 1n+sp:
371	      match sp:
372	        case 0n:
373	          match p:
374	            case 0n:
375	              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
376	            case 1n+pp:
377	              {==}
378	        case 1n+q:
379	          match p:
380	            case 0n:
381	              Empty.absurd({Nat.is_lt(1n+U.uq.half(q), 0n) == True{} : Bool}, bq.ft(h))
382	            case 1n+pp:
383	              bq.half_lt_pw(q, pp, h)
384	
385	# s < 2p: s - (1 + s / 2) < p
386	def bq.hr_lt_pw(s: Nat, p: Nat, h: {Nat.is_lt(s, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(s, 1n+U.uq.half(s)), p) == True{} : Bool}:
387	  match s:
388	    case 0n:
389	      match p:
390	        case 0n:
391	          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
392	        case 1n+pp:
393	          {==}
394	    case 1n+sp:
395	      match sp:
396	        case 0n:
397	          match p:
398	            case 0n:
399	              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
400	            case 1n+pp:
401	              {==}
402	        case 1n+ +q:
403	          match p:
404	            case 0n:
405	              Empty.absurd({Nat.is_lt(Nat.sub(q, U.uq.half(q)), 0n) == True{} : Bool}, bq.ft(h))
406	            case 1n+ +pp:
407	              U.uq.le_lt_trans(Nat.sub(q, U.uq.half(q)), 1n+Nat.sub(q, 1n+U.uq.half(q)), 1n+pp, bq.sub_step(q, U.uq.half(q)), bq.hr_lt_pw(q, pp, h))
408	
409	# Lists
410	
411	def bq.get_take(xs: List<&2, U32>, k: Nat, m: Nat, h: {Nat.is_lt(m, k) == True{} : Bool}) -> {List.get(&2, U32, List.take(&2, U32, xs, k), m) == List.get(&2, U32, xs, m) : Maybe<&2, U32>}:
412	  match xs k m:
413	    case Nil{} _ _:
414	      {==}
415	    case Con{x, t} 0n 0n:
416	      Empty.absurd({List.get(&2, U32, List.take(&2, U32, Con{x, t}, 0n), 0n) == List.get(&2, U32, Con{x, t}, 0n) : Maybe<&2, U32>}, bq.ft(h))
417	    case Con{x, t} 0n 1n+mp:
418	      Empty.absurd({List.get(&2, U32, List.take(&2, U32, Con{x, t}, 0n), 1n+mp) == List.get(&2, U32, Con{x, t}, 1n+mp) : Maybe<&2, U32>}, bq.ft(h))
419	    case Con{x, t} 1n+kp 0n:
420	      {==}
421	    case Con{x, t} 1n+kp 1n+mp:
422	      bq.get_take(t, kp, mp, h)
423	
424	def bq.get_nth(xs: List<&2, U32>, m: Nat, h: {Nat.is_lt(m, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.get(&2, U32, xs, m) == Some{A.Arrays.nth(U32, xs, m, 0)} : Maybe<&2, U32>}:
425	  match xs m:
426	    case Nil{} 0n:
427	      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
428	    case Nil{} 1n+mp:
429	      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
430	    case Con{x, t} 0n:
431	      {==}
432	    case Con{x, t} 1n+mp:
433	      bq.get_nth(t, mp, h)
434	
435	def bq.len_take(xs: List<&2, U32>, k: Nat, h: {Nat.is_le(k, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.length(&2, U32, List.take(&2, U32, xs, k)) == k : Nat}:
436	  match xs k:
437	    case Nil{} 0n:
438	      {==}
439	    case Nil{} 1n+kp:
440	      Empty.absurd({0n == 1n+kp : Nat}, bq.ft(h))
441	    case Con{x, t} 0n:
442	      {==}
443	    case Con{x, t} 1n+kp:
444	      U.uq.succ_cong(List.length(&2, U32, List.take(&2, U32, t, kp)), kp, bq.len_take(t, kp, h))
445	
446	def bq.get_len(xs: List<&2, U32>) -> {List.get(&2, U32, xs, List.length(&2, U32, xs)) == None{} : Maybe<&2, U32>}:
447	  match xs:
448	    case Nil{}:
449	      {==}
450	    case Con{x, t}:
451	      bq.get_len(t)