proofs/containers/hash_table/lookup.bend
bend-collections-laws-containers@1.0.0.0 · 158 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/spec/lib/common.bend as SC
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/containers/hash_table.bend as H
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/state.bend as ST
11
12# Lookup in the abstraction: the entries of the buckets, in bucket order.
13
14def nohb_c(+bs: List<&2, B.Bk>, +key: String, +q: Nat, +h: {Bool.and(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, q) == c : Bool}, rec: @hlt: {Nat.is_lt(j, q) == True{} : Bool} -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}:
15 match c:
16 case True{}:
17 L.subst(Nat, z => {Bool.not(B.hold(key, B.at(bs, z))) == True{} : Bool}, q, j, Equal.sym(Nat, j, q, N.eq_from_is_eq(j, q, hc)), L.and_left(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q), h))
18 case False{}:
19 rec(N.lt_or_eq(j, q, N.lt_succ_le(j, q, hj), hc))
20
21def nohb_inst(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +h: {B.nohb(bs, key, m) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}:
22 match m:
23 case 0n:
24 Empty.absurd({Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}, N.lt_zero_absurd(j, hj))
25 case 1n+q:
26 nohb_c(bs, key, q, h, j, hj, Nat.is_eq(j, q), {==}, hlt => nohb_inst(bs, key, q, L.and_right(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q), h), j, hlt))
27
28# bucket b (at index i, i above x) holds key, which bucket x also holds: impossible
29def uq_clash(+bs: List<&2, B.Bk>, +key: String, +i: Nat, +x: Nat, +hxi: {Nat.is_lt(x, i) == True{} : Bool}, +b: B.Bk, +hu: {B.uq_b(bs, i, b) == True{} : Bool}, +hb: {B.hold(key, b) == True{} : Bool}, +hx: {B.hold(key, B.at(bs, x)) == True{} : Bool}) -> Empty:
30 match b:
31 case B.BE{}:
32 L.false_true(hb)
33 case B.BF{w, +l, +k}:
34 +nb = L.and_left(B.nohb(bs, k, i), B.nolb(bs, l, i), hu)
35 +nx = nohb_inst(bs, k, i, nb, x, hxi)
36 +ek = K.str_eq_of(k, key, hb)
37 +hx2 = L.subst(String, z => {B.hold(z, B.at(bs, x)) == True{} : Bool}, key, k, Equal.sym(String, k, key, ek), hx)
38 L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, B.hold(k, B.at(bs, x)), True{}, hx2, nx))
39
40def other_lt(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}, +hkx: {B.hold(key, B.at(bs, x)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(x, i) == b : Bool}) -> Empty:
41 match b:
42 case True{}:
43 uq_clash(bs, key, i, x, hb, B.at(bs, i), B.all_inst(B.PUniq{bs}, n, huq, i, hi), hki, hkx)
44 case False{}:
45 +hix = N.lt_or_eq(i, x, N.not_lt_le(x, i, hb), N.is_eq_sym_false(x, i, hne))
46 uq_clash(bs, key, x, i, hix, B.at(bs, x), B.all_inst(B.PUniq{bs}, n, huq, x, hx), hkx, hki)
47
48def other_c(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}, +c: Bool, +hc: {B.hold(key, B.at(bs, x)) == c : Bool}) -> {Bool.not(c) == True{} : Bool}:
49 match c:
50 case False{}:
51 {==}
52 case True{}:
53 Empty.absurd({Bool.not(True{}) == True{} : Bool}, other_lt(bs, n, key, huq, i, hi, hki, x, hx, hne, hc, Nat.is_lt(x, i), {==}))
54
55# THEOREM: if bucket i holds key, no other bucket does
56def other(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, x))) == True{} : Bool}:
57 L.subst(Bool, c => {Bool.not(c) == True{} : Bool}, B.hold(key, B.at(bs, x)), B.hold(key, B.at(bs, x)), {==}, other_c(bs, n, key, huq, i, hi, hki, x, hx, hne, B.hold(key, B.at(bs, x)), {==}))
58
59# ---- lookup over the entries of a range of buckets ----
60
61def lk_skip_m(~V: Data, +k: String, +key: String, +m: Maybe<&2, V>, +r: List<&2, S.Entry<V>>, +h: {S.str_eq(k, key) == False{} : Bool}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent_m(~V, k, m), r), key) == S.lookup(~V, r, key) : Maybe<&2, V>}:
62 match m:
63 case None{}:
64 {==}
65 case Some{+v}:
66 L.subst(Bool, c => {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, r, key)) == S.lookup(~V, r, key) : Maybe<&2, V>}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, h), {==})
67
68# a bucket not holding key adds nothing to its lookup
69def lk_skip(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +key: String, +r: List<&2, S.Entry<V>>, +h: {Bool.not(B.hold(key, b)) == True{} : Bool}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, b, vsl), r), key) == S.lookup(~V, r, key) : Maybe<&2, V>}:
70 match b:
71 case B.BE{}:
72 {==}
73 case B.BF{w, +l, +k}:
74 lk_skip_m(~V, k, key, ST.nthm(~V, vsl, UD.v(H.slot(l))), r, K.not_true_eq(S.str_eq(k, key), h))
75
76def lk_take_m(~V: Data, +k: String, +key: String, +m: Maybe<&2, V>, +r: List<&2, S.Entry<V>>, +h: {S.str_eq(k, key) == True{} : Bool}, +hr: {S.lookup(~V, r, key) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent_m(~V, k, m), r), key) == m : Maybe<&2, V>}:
77 match m:
78 case None{}:
79 hr
80 case Some{+v}:
81 L.subst(Bool, c => {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, r, key)) == Some{v} : Maybe<&2, V>}, True{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), True{}, h), {==})
82
83# the bucket holding key decides its lookup
84def lk_take(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +key: String, +r: List<&2, S.Entry<V>>, +h: {B.hold(key, b) == True{} : Bool}, +hr: {S.lookup(~V, r, key) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, b, vsl), r), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(b)))) : Maybe<&2, V>}:
85 match b:
86 case B.BE{}:
87 Empty.absurd({S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.BE{}, vsl), r), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.BE{})))) : Maybe<&2, V>}, L.false_true(h))
88 case B.BF{w, +l, +k}:
89 lk_take_m(~V, k, key, ST.nthm(~V, vsl, UD.v(H.slot(l))), r, h, hr)
90
91# no bucket in j .. j + m - 1 holds key
92def nob(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +j: Nat) -> Bool:
93 match m:
94 case 0n:
95 True{}
96 case 1n+p:
97 Bool.and(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j))
98
99def lk_nob(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +m: Nat, +j: Nat, +h: {nob(bs, key, m, j) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, m, j), key) == None{} : Maybe<&2, V>}:
100 match m:
101 case 0n:
102 {==}
103 case 1n+p:
104 Equal.trans(Maybe<&2, V>, S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)), key), S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key), None{},
105 lk_skip(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), L.and_left(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), h)),
106 lk_nob(~V, bs, vsl, key, p, 1n+j, L.and_right(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), h)))
107
108def nob_pno(+bs: List<&2, B.Bk>, +key: String, +n: Nat, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {nob(bs, key, m, j) == True{} : Bool}:
109 match m:
110 case 0n:
111 {==}
112 case 1n+p:
113 +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
114 +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
115 L.and_intro(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), B.all_inst(B.PNo{bs, key}, n, hno, j, hj), nob_pno(bs, key, n, hno, p, 1n+j, hjm2))
116
117# the buckets past the one holding key do not hold it
118def nob_past(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}, +hij: {Nat.is_lt(i, j) == True{} : Bool}) -> {nob(bs, key, m, j) == True{} : Bool}:
119 match m:
120 case 0n:
121 {==}
122 case 1n+p:
123 +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
124 +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
125 +hne = N.is_eq_sym_false(i, j, N.is_eq_lt(i, j, hij))
126 L.and_intro(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), other(bs, n, key, huq, i, hi, hki, j, hj, hne), nob_past(bs, n, key, huq, i, hi, hki, p, 1n+j, hjm2, N.lt_trans(i, j, 1n+j, hij, N.lt_succ(j))))
127
128def lk_hit_c(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +p: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, 1n+p), n) == True{} : Bool}, +hji: {Nat.is_le(j, i) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, i) == c : Bool}, rec: @hji2: {Nat.is_le(1n+j, i) == True{} : Bool} -> {S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, 1n+p, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
129 match c:
130 case True{}:
131 +eji = N.eq_from_is_eq(j, i, hc)
132 +hkj = L.subst(Nat, z => {B.hold(key, B.at(bs, z)) == True{} : Bool}, i, j, Equal.sym(Nat, j, i, eji), hki)
133 +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
134 +hr = lk_nob(~V, bs, vsl, key, p, 1n+j, nob_past(bs, n, key, huq, i, hi, hki, p, 1n+j, hjm2, L.subst(Nat, z => {Nat.is_lt(z, 1n+j) == True{} : Bool}, j, i, eji, N.lt_succ(j))))
135 L.subst(Nat, z => {S.lookup(~V, ST.absm(~V, bs, vsl, 1n+p, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, z))))) : Maybe<&2, V>}, j, i, eji, lk_take(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), hkj, hr))
136 case False{}:
137 +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
138 +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
139 +hlt = N.lt_or_eq(j, i, hji, hc)
140 Equal.trans(Maybe<&2, V>, S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)), key), S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key), ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))),
141 lk_skip(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), other(bs, n, key, huq, i, hi, hki, j, hj, hc)),
142 rec(N.lt_succ_le_succ(j, i, hlt)))
143
144def lk_hit(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}, +hji: {Nat.is_le(j, i) == True{} : Bool}, +him: {Nat.is_lt(i, Nat.add(j, m)) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, m, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
145 match m:
146 case 0n:
147 Empty.absurd({S.lookup(~V, ST.absm(~V, bs, vsl, 0n, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(j, i), False{}, Equal.sym(Bool, Nat.is_le(j, i), True{}, hji), N.lt_not_le(i, j, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(j, 0n), j, N.add_zero(j), him)))))
148 case 1n+p:
149 +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
150 lk_hit_c(~V, bs, vsl, key, n, huq, i, hi, hki, p, j, hjm, hji, Nat.is_eq(j, i), {==}, hji2 => lk_hit(~V, bs, vsl, key, n, huq, i, hi, hki, p, 1n+j, hjm2, hji2, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), him)))
151
152# THEOREM: with keys unique, the lookup of the key held by bucket i is the
153# value in i's slot; with key held nowhere, it is None.
154def lookup_hit(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
155 lk_hit(~V, bs, vsl, key, n, huq, i, hi, hki, n, 0n, N.le_refl(n), N.zero_le(i), hi)
156
157def lookup_none(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), key) == None{} : Maybe<&2, V>}:
158 lk_nob(~V, bs, vsl, key, n, 0n, nob_pno(bs, key, n, hno, n, 0n, N.le_refl(n)))