proof_bsearch.bend

bend-osdev-algo@0.1.0.0 · 451 lines · 51 definitions

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.
12import Base
13import bend-osdev-algo@0.1.0.0/bsearch.bend as S
14import bend-osdev-array@0.1.0.0/array.bend as A
15import bend-osdev-array@0.1.0.0/LAWS.bend as AL
16import bend-osdev-array@0.1.0.0/PROOF.bend as APF
17import bend-osdev-algo@0.1.0.0/proof_u32.bend as U
18
19# Shorthands (they unfold to the defs they name)
20
21def bq.ol(+d: Nat, +l: List<&2, U32>) -> Array<U32>:
22  A.Arrays.of_list(U32, d, l, 0)
23
24def 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
28def 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
33def bq.pre(+l: List<&2, U32>, +n: U32) -> List<&2, U32>:
34  List.take(&2, U32, l, U32.to_nat(n))
35
36def 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
39def bq.s(+lo: U32, +hi: U32) -> Nat:
40  Nat.sub(U32.to_nat(hi), U32.to_nat(lo))
41
42def 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
47def 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
54def bq.hi_b(b: Bool, +hi: U32, +mid: U32) -> U32:
55  match b:
56    case True{}:
57      hi
58    case False{}:
59      mid
60
61def 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
68def 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
75def 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
78def 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
82def 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
91def 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
98def 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
105def 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
119def bq.bt(b: Bool) -> Type:
120  match b:
121    case True{}:
122      Unit
123    case False{}:
124      Empty
125
126def bq.ft(e: {False{} == True{} : Bool}) -> Empty:
127  %Equal.sym(Bool, False{}, True{}, e) : bq.bt(_)
128  Unit{}
129
130def bq.tf(e: {True{} == False{} : Bool}) -> Empty:
131  %e : bq.bt(_)
132  Unit{}
133
134def bq.nt(n: Nat) -> Type:
135  match n:
136    case 0n:
137      Unit
138    case 1n+p:
139      Empty
140
141def 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
147def 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
154def 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
161def 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
170def 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
179def 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
190def 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
205def 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
216def 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
227def 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
238def 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
247def 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
252def 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
257def 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
264def 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
273def bq.sub_zero(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
274  match x:
275    case 0n:
276      {==}
277    case 1n+p:
278      {==}
279
280def 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
289def 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
296def 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
307def 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
316def 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
327def 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
339def 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
350def 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
362def 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
386def 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
411def 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
424def 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
435def 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
446def 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)