proofs/containers/hash_table/inv.bend
bend-collections-laws-containers@1.0.0.0 · 91 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/proofs/lib/u32alg.bend as A
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/keys.bend as K
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as M
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
12import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
13import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
14
15# Facts derived from the table invariants for a probed key.
16
17def hb_bf(+sd: Nat, +mask: U32, +key: String, +x: U32, +l: U32, +k: String, +hw: {B.wb(sd, B.BF{x, l, k}) == True{} : Bool}, +e: Bool, +he: {S.str_eq(k, key) == e : Bool}) -> {B.implies(e, Nat.is_eq(UD.v(HS.bucket(x, mask)), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}:
18 match e:
19 case False{}:
20 {==}
21 case True{}:
22 +xw = Equal.trans(U32, x, K.kword(k), K.kword(key), A.eq_of(x, K.kword(k), L.and_left(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0)), L.and_right(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw))), Equal.cong(String, U32, z => K.kword(z), k, key, K.str_eq_of(k, key, he)))
23 L.subst(U32, z => {B.implies(True{}, Nat.is_eq(UD.v(HS.bucket(z, mask)), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}, K.kword(key), x, Equal.sym(U32, x, K.kword(key), xw), N.is_eq_refl(UD.v(HS.bucket(K.kword(key), mask))))
24
25def hb_hold(+sd: Nat, +mask: U32, +key: String, +b: B.Bk, +hw: {B.wb(sd, b) == True{} : Bool}) -> {B.implies(B.hold(key, b), Nat.is_eq(B.hb(mask, b), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}:
26 match b:
27 case B.BE{}:
28 {==}
29 case B.BF{+x, +l, +k}:
30 hb_bf(sd, mask, key, x, l, k, hw, S.str_eq(k, key), {==})
31
32
33# every bucket holding key has key's home
34def home_all(+bs: List<&2, B.Bk>, +sd: Nat, +mask: U32, +key: String, +n: Nat, +hwell: {B.all_lt(B.PWell{bs, sd}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, m) == True{} : Bool}:
35 match m:
36 case 0n:
37 {==}
38 case 1n+q:
39 +hq = N.succ_le_lt(q, n, hm)
40 L.and_intro(B.eval(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, q), B.all_lt(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, q), hb_hold(sd, mask, key, B.at(bs, q), B.all_inst(B.PWell{bs, sd}, n, hwell, q, hq)), home_all(bs, sd, mask, key, n, hwell, q, N.lt_le(q, n, hq)))
41
42# ---- occupancy ----
43
44def bitv(b: Bool) -> Nat:
45 match b:
46 case True{}:
47 1n
48 case False{}:
49 0n
50
51# the number of full buckets among the first m
52def occn(+bs: List<&2, B.Bk>, +m: Nat) -> Nat:
53 match m:
54 case 0n:
55 0n
56 case 1n+q:
57 Nat.add(bitv(B.occ(B.at(bs, q))), occn(bs, q))
58
59def Empty0(+bs: List<&2, B.Bk>, +m: Nat) -> Type:
60 Sigma<&1, &1, Nat, j => {Nat.is_lt(j, m) == True{} : Bool} & {B.at(bs, j) == B.BE{} : B.Bk}>
61
62def emp_up(+bs: List<&2, B.Bk>, +q: Nat, e: Empty0(bs, q)) -> Empty0(bs, 1n+q):
63 match e:
64 case Tuple{+j, Tuple{hj, hz}}:
65 (j, (N.lt_trans(j, q, 1n+q, hj, N.lt_succ(q)), hz))
66
67def emp_c(+bs: List<&2, B.Bk>, +q: Nat, +b: B.Bk, +hb: {B.at(bs, q) == b : B.Bk}, +h: {Nat.is_lt(Nat.add(bitv(B.occ(b)), occn(bs, q)), 1n+q) == True{} : Bool}, rec: @hq: {Nat.is_lt(occn(bs, q), q) == True{} : Bool} -> Empty0(bs, q)) -> Empty0(bs, 1n+q):
68 match b:
69 case B.BE{}:
70 (q, (N.lt_succ(q), hb))
71 case B.BF{x, l, k}:
72 emp_up(bs, q, rec(h))
73
74# fewer full buckets than buckets: some bucket is empty
75def find_empty(+bs: List<&2, B.Bk>, +m: Nat, +h: {Nat.is_lt(occn(bs, m), m) == True{} : Bool}) -> Empty0(bs, m):
76 match m:
77 case 0n:
78 Empty.absurd(Empty0(bs, 0n), N.lt_zero_absurd(occn(bs, 0n), h))
79 case 1n+q:
80 emp_c(bs, q, B.at(bs, q), {==}, h, hq => find_empty(bs, q, hq))
81
82# the probe theorem for a table size n > 0 started at its home h
83def pos0(+bp: Nat, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}) -> {M.pos(1n+bp, h, 0n) == h : Nat}:
84 Equal.trans(Nat, Nat.mod(Nat.add(h, 0n), 1n+bp), Nat.mod(h, 1n+bp), h, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(h, 0n), h, N.add_zero(h)), CY.mod_small(1n+bp, h, hh))
85
86def pf_ok_n(+bs: List<&2, B.Bk>, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, n) == True{} : Bool}, +cl: {B.cluster(bs, n, mask) == True{} : Bool}, +ho: {B.all_lt(B.PHome{bs, mask, key, h}, n) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, n) == True{} : Bool}, +hz0: {B.at(bs, e0) == B.BE{} : B.Bk}) -> B.ResOK(bs, n, h, key, B.pf(key, bs, n, n, B.mstep(key, B.at(bs, h)), h)):
87 match n:
88 case 0n:
89 Empty.absurd(B.ResOK(bs, 0n, h, key, B.pf(key, bs, 0n, 0n, B.mstep(key, B.at(bs, h)), h)), L.false_true(hn))
90 case 1n+bp:
91 L.subst(Nat, z => B.ResOK(bs, 1n+bp, h, key, B.pf(key, bs, 1n+bp, 1n+bp, B.mstep(key, B.at(bs, z)), z)), M.pos(1n+bp, h, 0n), h, pos0(bp, h, hh), B.pf_ok(bs, bp, mask, key, h, hh, cl, ho, e0, he0, hz0, 1n+bp, 0n, hn, {==}, {==}))