proofs/containers/hash_table/step.bend
bend-collections-laws-containers@1.0.0.0 · 131 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/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
8import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/strings.bend as STR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/arr.bend as AX
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
14
15# The implementation's probe step for a long key, on arrays built from mirror
16# trees: it reads bucket i's word x and link l; on a word match it swaps the
17# stored key out, compares and puts it back (the stored keys are unchanged).
18
19def step_of(ms: B.MS, tab: Array<U32>, ks: Array<String>, key: String) -> H.Step:
20 match ms:
21 case B.MEnd{}:
22 H.SEnd{tab, ks, key}
23 case B.MHit{l}:
24 H.SHit{tab, ks, key, l}
25 case B.MNext{}:
26 H.SNext{tab, ks, key}
27
28def pick_step(tab: Array<U32>, +l: U32, ks: Array<String>, key: String, +e: Bool) -> {H.sk_pick(tab, l, ks, key, e) == step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, ks, key) : H.Step}:
29 match e:
30 case True{}:
31 {==}
32 case False{}:
33 {==}
34
35# the stored keys after a compare at link l: taken out, put back
36def kcmp(+sd: Nat, +ksT: AR.Tree<String>, +l: U32) -> AR.Tree<String>:
37 AR.upd(String, sd, AR.upd(String, sd, ksT, UD.v(H.slot(l)), SNil{}), UD.v(H.slot(l)), TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))))
38
39def kcmp_slots(+sd: Nat, +ksT: AR.Tree<String>, +l: U32, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {AR.slots(String, kcmp(sd, ksT, l)) == AR.slots(String, ksT) : List<&2, String>}:
40 +j = UD.v(H.slot(l))
41 +kl = AR.slots(String, ksT)
42 +k1 = AR.upd(String, sd, ksT, j, SNil{})
43 +p1 = AR.upd_perfect(String, sd, ksT, j, SNil{}, pk)
44 +e1 = AR.upd_slots(String, sd, k1, j, TB.nths(kl, j), hs, p1)
45 +e2 = Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, j, TB.nths(kl, j)), AR.slots(String, k1), SC.update(String, kl, j, SNil{}), AR.upd_slots(String, sd, ksT, j, SNil{}, hs, pk))
46 Equal.trans(List<&2, String>, AR.slots(String, kcmp(sd, ksT, l)), SC.update(String, AR.slots(String, k1), j, TB.nths(kl, j)), kl, e1,
47 Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, k1), j, TB.nths(kl, j)), SC.update(String, SC.update(String, kl, j, SNil{}), j, TB.nths(kl, j)), kl, e2,
48 Equal.trans(List<&2, String>, SC.update(String, SC.update(String, kl, j, SNil{}), j, TB.nths(kl, j)), SC.update(String, kl, j, TB.nths(kl, j)), kl, TB.upd_upd(kl, j, SNil{}, TB.nths(kl, j)), TB.upd_self(kl, j))))
49
50def kcmp_perfect(+sd: Nat, +ksT: AR.Tree<String>, +l: U32, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {AR.perfect(String, sd, kcmp(sd, ksT, l)) == True{} : Bool}:
51 AR.upd_perfect(String, sd, AR.upd(String, sd, ksT, UD.v(H.slot(l)), SNil{}), UD.v(H.slot(l)), TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), AR.upd_perfect(String, sd, ksT, UD.v(H.slot(l)), SNil{}, pk))
52
53# comparing the probed key with the key stored at link l
54def cmp_path(tab: Array<U32>, +sd: Nat, +ksT: AR.Tree<String>, +l: U32, +key: String, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {H.sk_same(tab, AR.thaw(String, ksT), l, key, True{}) == step_of(Bool.pick(B.MS, S.str_eq(key, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l)))), B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key) : H.Step}:
55 +j = UD.v(H.slot(l))
56 +kl = AR.slots(String, ksT)
57 +k = TB.nths(kl, j)
58 +k1 = AR.upd(String, sd, ksT, j, SNil{})
59 +e = S.str_eq(key, k)
60 +hsw = AR.swap(String, sd, ksT, H.slot(l), SNil{}, k, hsd, hs, AX.nths_of(sd, ksT, j, hs, pk), pk)
61 +hk1 = L.subst(List<&2, String>, ys => {SC.nth(String, ys, j) == Some{SNil{}} : Maybe<&2, String>}, SC.update(String, kl, j, SNil{}), AR.slots(String, k1), Equal.sym(List<&2, String>, AR.slots(String, k1), SC.update(String, kl, j, SNil{}), AR.upd_slots(String, sd, ksT, j, SNil{}, hs, pk)), LL.nth_update_same(String, kl, j, SNil{}, LL.nth_lt_length(String, kl, j, k, AX.nths_of(sd, ksT, j, hs, pk))))
62 +hset = AR.set(String, sd, k1, H.slot(l), k, SNil{}, hsd, hs, hk1, AR.upd_perfect(String, sd, ksT, j, SNil{}, pk))
63 +s1 = Equal.cong(Array<String> & String, H.Step, r => H.sk_cmp(tab, l, key, r), Array.swap(String, AR.thaw(String, ksT), H.slot(l), SNil{}), (AR.thaw(String, k1), k), hsw)
64 +s2 = Equal.cong((String & String) & Bool, H.Step, r => H.sk_fin(tab, l, AR.thaw(String, k1), r), H.eq(key, k), ((key, k), e), STR.eq(key, k))
65 +s3 = Equal.cong(Array<String>, H.Step, a => H.sk_pick(tab, l, a, key, e), Array.set(String, AR.thaw(String, k1), H.slot(l), k), AR.thaw(String, kcmp(sd, ksT, l)), hset)
66 Equal.trans(H.Step, H.sk_cmp(tab, l, key, Array.swap(String, AR.thaw(String, ksT), H.slot(l), SNil{})), H.sk_fin(tab, l, AR.thaw(String, k1), H.eq(key, k)), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s1,
67 Equal.trans(H.Step, H.sk_fin(tab, l, AR.thaw(String, k1), H.eq(key, k)), H.sk_pick(tab, l, Array.set(String, AR.thaw(String, k1), H.slot(l), k), key, e), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s2,
68 Equal.trans(H.Step, H.sk_pick(tab, l, Array.set(String, AR.thaw(String, k1), H.slot(l), k), key, e), H.sk_pick(tab, l, AR.thaw(String, kcmp(sd, ksT, l)), key, e), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s3, pick_step(tab, l, AR.thaw(String, kcmp(sd, ksT, l)), key, e))))
69
70# the decision of a long-key step on word x, link l, stored key k
71def ld_w(+key: String, +l: U32, +k: String, same: Bool) -> B.MS:
72 match same:
73 case False{}:
74 B.MNext{}
75 case True{}:
76 Bool.pick(B.MS, S.str_eq(key, k), B.MHit{l}, B.MNext{})
77
78def ld_e(+key: String, +w: U32, +x: U32, +l: U32, +k: String, empty: Bool) -> B.MS:
79 match empty:
80 case True{}:
81 B.MEnd{}
82 case False{}:
83 ld_w(key, l, k, U32.is_eq(x, w))
84
85def ldec(+key: String, +w: U32, +x: U32, +l: U32, +k: String) -> B.MS:
86 ld_e(key, w, x, l, k, U32.is_eq(x, 0))
87
88def ka_w(+sd: Nat, +ksT: AR.Tree<String>, +l: U32, same: Bool) -> AR.Tree<String>:
89 match same:
90 case False{}:
91 ksT
92 case True{}:
93 kcmp(sd, ksT, l)
94
95def ka_e(+sd: Nat, +ksT: AR.Tree<String>, +w: U32, +x: U32, +l: U32, empty: Bool) -> AR.Tree<String>:
96 match empty:
97 case True{}:
98 ksT
99 case False{}:
100 ka_w(sd, ksT, l, U32.is_eq(x, w))
101
102# the stored keys after a long-key step
103def kafter(+sd: Nat, +ksT: AR.Tree<String>, +w: U32, +x: U32, +l: U32) -> AR.Tree<String>:
104 ka_e(sd, ksT, w, x, l, U32.is_eq(x, 0))
105
106def st_same(tab: Array<U32>, +sd: Nat, +ksT: AR.Tree<String>, +l: U32, +key: String, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +same: Bool) -> {H.sk_same(tab, AR.thaw(String, ksT), l, key, same) == step_of(ld_w(key, l, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), same), tab, AR.thaw(String, ka_w(sd, ksT, l, same)), key) : H.Step}:
107 match same:
108 case False{}:
109 {==}
110 case True{}:
111 cmp_path(tab, sd, ksT, l, key, hsd, hs, pk)
112
113def st_empty(+td: Nat, +tabT: AR.Tree<U32>, +sd: Nat, +ksT: AR.Tree<String>, +i: U32, +key: String, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +x: U32, +hs: {B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), SC.pow2(sd))) == True{} : Bool}, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}) -> {H.sk_empty(AR.thaw(U32, tabT), AR.thaw(String, ksT), i, key, w, x, e) == step_of(ld_e(key, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i))))))), e), AR.thaw(U32, tabT), AR.thaw(String, ka_e(sd, ksT, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), e)), key) : H.Step}:
114 match e:
115 case True{}:
116 {==}
117 case False{}:
118 +l = W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i))))
119 +hs2 = B.imp_elim(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), hs, L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, False{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), False{}, he), {==}))
120 +g = AX.getw(td, tabT, U32.inc(U32.shl(i)), hd, hl, pt)
121 Equal.trans(H.Step, H.sk_l(AR.thaw(String, ksT), key, x, w, Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(i)))), H.sk_l(AR.thaw(String, ksT), key, x, w, (AR.thaw(U32, tabT), l)), step_of(ld_w(key, l, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), U32.is_eq(x, w)), AR.thaw(U32, tabT), AR.thaw(String, ka_w(sd, ksT, l, U32.is_eq(x, w))), key),
122 Equal.cong(Array<U32> & U32, H.Step, r => H.sk_l(AR.thaw(String, ksT), key, x, w, r), Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(i))), (AR.thaw(U32, tabT), l), g),
123 st_same(AR.thaw(U32, tabT), sd, ksT, l, key, hsd, hs2, pk, U32.is_eq(x, w)))
124
125# THEOREM: a long-key probe step reads bucket i and decides as ldec.
126def step_long(+td: Nat, +tabT: AR.Tree<U32>, +sd: Nat, +ksT: AR.Tree<String>, +i: U32, +key: String, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +hw: {Nat.is_lt(UD.v(U32.shl(i)), SC.pow2(td)) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +hs: {B.implies(Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), 0)), Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), SC.pow2(sd))) == True{} : Bool}) -> {H.step(AR.thaw(U32, tabT), AR.thaw(String, ksT), i, key, w) == step_of(ldec(key, w, W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))))), AR.thaw(U32, tabT), AR.thaw(String, kafter(sd, ksT, w, W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), key) : H.Step}:
127 +x = W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i)))
128 +g = AX.getw(td, tabT, U32.shl(i), hd, hw, pt)
129 Equal.trans(H.Step, H.sk_w(AR.thaw(String, ksT), i, key, w, Array.get(U32, AR.thaw(U32, tabT), U32.shl(i))), H.sk_w(AR.thaw(String, ksT), i, key, w, (AR.thaw(U32, tabT), x)), step_of(ldec(key, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))))), AR.thaw(U32, tabT), AR.thaw(String, kafter(sd, ksT, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), key),
130 Equal.cong(Array<U32> & U32, H.Step, r => H.sk_w(AR.thaw(String, ksT), i, key, w, r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(i)), (AR.thaw(U32, tabT), x), g),
131 st_empty(td, tabT, sd, ksT, i, key, w, hd, hsd, pt, pk, hl, x, hs, U32.is_eq(x, 0), {==}))