proofs/containers/hash_table/table.bend
bend-collections-laws-containers@1.0.0.0 · 97 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
5import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
8
9# Reading the implementation's arrays as a bucket list.
10# tab (check word, link) pairs: bucket i is (tab[2i], tab[2i+1])
11# ks the slot arena's stored keys: a long key's String, "" for a
12# one-character key (its word is the key)
13
14
15def nths(ks: List<&2, String>, +i: Nat) -> String:
16 match ks i:
17 case Nil{} _:
18 SNil{}
19 case Con{x, t} 0n:
20 x
21 case Con{x, t} 1n+p:
22 nths(t, p)
23
24# the key of a full bucket with word w and stored string s
25def keyof_c(+w: U32, s: String, short: Bool) -> String:
26 match short:
27 case True{}:
28 SCon{Chr{U32.and(w, 2147483647)}, SNil{}}
29 case False{}:
30 s
31
32def keyof(+w: U32, s: String) -> String:
33 keyof_c(w, s, H.is_short(w))
34
35def dec_c(+w: U32, +l: U32, +ks: List<&2, String>, empty: Bool) -> B.Bk:
36 match empty:
37 case True{}:
38 B.BE{}
39 case False{}:
40 B.BF{w, l, keyof(w, nths(ks, UD.v(H.slot(l))))}
41
42# bucket i of the arrays
43def dec(+tb: List<&2, U32>, +ks: List<&2, String>, +i: Nat) -> B.Bk:
44 dec_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, 1n+Nat.double(i)), ks, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0))
45
46# buckets i .. i + m - 1
47def dlist(+tb: List<&2, U32>, +ks: List<&2, String>, +m: Nat, +i: Nat) -> List<&2, B.Bk>:
48 match m:
49 case 0n:
50 Nil{}
51 case 1n+p:
52 Con{dec(tb, ks, i), dlist(tb, ks, p, 1n+i)}
53
54def at_dlist(+tb: List<&2, U32>, +ks: List<&2, String>, +m: Nat, +i: Nat, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {B.at(dlist(tb, ks, m, i), j) == dec(tb, ks, Nat.add(i, j)) : B.Bk}:
55 match m j:
56 case 0n _:
57 Empty.absurd({B.at(dlist(tb, ks, 0n, i), j) == dec(tb, ks, Nat.add(i, j)) : B.Bk}, N.lt_zero_absurd(j, hj))
58 case 1n+p 0n:
59 Equal.cong(Nat, B.Bk, z => dec(tb, ks, z), i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, N.add_zero(i)))
60 case 1n+p 1n+q:
61 Equal.trans(B.Bk, B.at(dlist(tb, ks, p, 1n+i), q), dec(tb, ks, Nat.add(1n+i, q)), dec(tb, ks, Nat.add(i, 1n+q)), at_dlist(tb, ks, p, 1n+i, q, hj), Equal.cong(Nat, B.Bk, z => dec(tb, ks, z), 1n+Nat.add(i, q), Nat.add(i, 1n+q), Equal.sym(Nat, Nat.add(i, 1n+q), 1n+Nat.add(i, q), N.add_succ(i, q))))
62
63# the bucket list of a table of n buckets
64def buckets(+tb: List<&2, U32>, +ks: List<&2, String>, +n: Nat) -> List<&2, B.Bk>:
65 dlist(tb, ks, n, 0n)
66
67def at_buckets(+tb: List<&2, U32>, +ks: List<&2, String>, +n: Nat, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}) -> {B.at(buckets(tb, ks, n), j) == dec(tb, ks, j) : B.Bk}:
68 at_dlist(tb, ks, n, 0n, j, hj)
69
70# a list index below the length reads its element
71
72def nths_some(+ks: List<&2, String>, +i: Nat, +h: {Nat.is_lt(i, SC.length(String, ks)) == True{} : Bool}) -> {SC.nth(String, ks, i) == Some{nths(ks, i)} : Maybe<&2, String>}:
73 match ks i:
74 case Nil{} _:
75 Empty.absurd({SC.nth(String, Nil{}, i) == Some{nths(Nil{}, i)} : Maybe<&2, String>}, N.lt_zero_absurd(i, h))
76 case Con{x, t} 0n:
77 {==}
78 case Con{x, t} 1n+p:
79 nths_some(t, p, h)
80
81def upd_upd(+xs: List<&2, String>, +i: Nat, +a: String, +b: String) -> {SC.update(String, SC.update(String, xs, i, a), i, b) == SC.update(String, xs, i, b) : List<&2, String>}:
82 match xs i:
83 case Nil{} _:
84 {==}
85 case Con{h, t} 0n:
86 {==}
87 case Con{h, t} 1n+p:
88 Equal.cong(List<&2, String>, List<&2, String>, r => Con{h, r}, SC.update(String, SC.update(String, t, p, a), p, b), SC.update(String, t, p, b), upd_upd(t, p, a, b))
89
90def upd_self(+xs: List<&2, String>, +i: Nat) -> {SC.update(String, xs, i, nths(xs, i)) == xs : List<&2, String>}:
91 match xs i:
92 case Nil{} _:
93 {==}
94 case Con{h, t} 0n:
95 {==}
96 case Con{h, t} 1n+p:
97 Equal.cong(List<&2, String>, List<&2, String>, r => Con{h, r}, SC.update(String, t, p, nths(t, p)), t, upd_self(t, p))