proofs/containers/hash_table/decide.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/u32alg.bend as A
4import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
6import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/strings.bend as STR
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/words.bend as WR
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
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/buckets.bend as B
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/step.bend as SP
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as UW
14
15# The implementation's step decision (word match, then String compare)
16# equals the model's "does the bucket hold the key", for a long key, when a
17# long bucket's word is its stored key's word.
18
19def not_false() -> {Bool.not(False{}) == True{} : Bool}:
20 {==}
21
22# a short word masked is a code below 2^31
23def masked_small(+x: U32) -> {U32.is_lt(U32.and(x, 2147483647), H.tag()) == True{} : Bool}:
24 match x:
25 case U32{+w}:
26 +a = Word.and(32n, w, WR.low(31n))
27 +c = Word.cmp(32n, a, WR.top(31n))
28 Equal.trans(Bool, Cmp.is_lt(c), Bool.not(Cmp.is_ge(c)), True{}, WR.lt_ge(c), L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, False{}, Cmp.is_ge(c), Equal.sym(Bool, Cmp.is_ge(c), False{}, Equal.trans(Bool, Cmp.is_ge(c), WR.topb(31n, a), False{}, WR.ge_top(31n, a), WR.topb_and_low(31n, w))), {==}))
29
30def lword_long(+key: String) -> {H.is_short(STR.lword(key)) == False{} : Bool}:
31 WR.long_is_long(STR.fold(key, 0))
32
33# a one-character key below 2^31 is not a long-probed key
34def short_ne_long(+c: U32, +key: String, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +hk: {K.shortk(key) == False{} : Bool}, +e: Bool, +he: {S.str_eq(SCon{Chr{c}, SNil{}}, key) == e : Bool}) -> {e == False{} : Bool}:
35 match e:
36 case False{}:
37 {==}
38 case True{}:
39 +eq = K.str_eq_of(SCon{Chr{c}, SNil{}}, key, he)
40 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, K.shortk(key), False{}, Equal.trans(Bool, True{}, K.shortk(SCon{Chr{c}, SNil{}}), K.shortk(key), Equal.sym(Bool, K.shortk(SCon{Chr{c}, SNil{}}), True{}, hc), Equal.cong(String, Bool, z => K.shortk(z), SCon{Chr{c}, SNil{}}, key, eq)), hk)))
41
42# words of different kinds differ
43def kinds_ne(+x: U32, +w: U32, +hx: {H.is_short(x) == True{} : Bool}, +hw: {H.is_short(w) == False{} : Bool}, +s: Bool, +hs: {U32.is_eq(x, w) == s : Bool}) -> {s == False{} : Bool}:
44 match s:
45 case False{}:
46 {==}
47 case True{}:
48 +eq = A.eq_of(x, w, hs)
49 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, H.is_short(w), False{}, Equal.trans(Bool, True{}, H.is_short(x), H.is_short(w), Equal.sym(Bool, H.is_short(x), True{}, hx), Equal.cong(U32, Bool, z => H.is_short(z), x, w, eq)), hw)))
50
51def dl_short(+key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +l: U32, +k: String, +hxs: {H.is_short(x) == True{} : Bool}) -> {SP.ld_w(key, l, k, U32.is_eq(x, STR.lword(key))) == B.mstep(key, B.BF{x, l, TB.keyof_c(x, k, True{})}) : B.MS}:
52 +sk = {SCon{Chr{U32.and(x, 2147483647)}, SNil{}} : String}
53 Equal.trans(B.MS, SP.ld_w(key, l, k, U32.is_eq(x, STR.lword(key))), B.MNext{}, Bool.pick(B.MS, S.str_eq(sk, key), B.MHit{l}, B.MNext{}),
54 Equal.cong(Bool, B.MS, b => SP.ld_w(key, l, k, b), U32.is_eq(x, STR.lword(key)), False{}, kinds_ne(x, STR.lword(key), hxs, lword_long(key), U32.is_eq(x, STR.lword(key)), {==})),
55 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), False{}, S.str_eq(sk, key), Equal.sym(Bool, S.str_eq(sk, key), False{}, short_ne_long(U32.and(x, 2147483647), key, masked_small(x), hk, S.str_eq(sk, key), {==}))))
56
57# a long bucket whose word is not the probed word does not hold the key
58def le_false(+k: String, +key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +hinv: {x == K.kword(k) : U32}, +hs: {U32.is_eq(x, STR.lword(key)) == False{} : Bool}, +e: Bool, +he: {S.str_eq(k, key) == e : Bool}) -> {e == False{} : Bool}:
59 match e:
60 case False{}:
61 {==}
62 case True{}:
63 +xw = Equal.trans(U32, x, K.kword(k), STR.lword(key), hinv, Equal.trans(U32, K.kword(k), K.kword(key), STR.lword(key), Equal.cong(String, U32, z => K.kword(z), k, key, K.str_eq_of(k, key, he)), K.kword_long(key, hk)))
64 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, U32.is_eq(x, STR.lword(key)), False{}, L.subst(U32, z => {True{} == U32.is_eq(x, z) : Bool}, x, STR.lword(key), xw, Equal.sym(Bool, U32.is_eq(x, x), True{}, UW.u32_eq_refl(x))), hs)))
65
66def dl_long(+key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +l: U32, +k: String, +hinv: {x == K.kword(k) : U32}, +s: Bool, +hs: {U32.is_eq(x, STR.lword(key)) == s : Bool}) -> {SP.ld_w(key, l, k, s) == Bool.pick(B.MS, S.str_eq(k, key), B.MHit{l}, B.MNext{}) : B.MS}:
67 match s:
68 case True{}:
69 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), S.str_eq(key, k), S.str_eq(k, key), K.str_sym(key, k))
70 case False{}:
71 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, le_false(k, key, hk, x, hinv, hs, S.str_eq(k, key), {==})))
72
73def dsh(+key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +l: U32, +k: String, +hinv: {B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(k))) == True{} : Bool}, +sh: Bool, +hsh: {H.is_short(x) == sh : Bool}) -> {SP.ld_w(key, l, k, U32.is_eq(x, STR.lword(key))) == B.mstep(key, B.BF{x, l, TB.keyof_c(x, k, sh)}) : B.MS}:
74 match sh:
75 case True{}:
76 dl_short(key, hk, x, l, k, hsh)
77 case False{}:
78 +e = B.imp_elim(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(k)), hinv, L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, False{}, H.is_short(x), Equal.sym(Bool, H.is_short(x), False{}, hsh), {==}))
79 dl_long(key, hk, x, l, k, A.eq_of(x, K.kword(k), e), U32.is_eq(x, STR.lword(key)), {==})
80
81def dec_e(+key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +l: U32, +ks: List<&2, String>, +hinv: {B.implies(Bool.not(U32.is_eq(x, 0)), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(ks, UD.v(H.slot(l))))))) == True{} : Bool}, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}) -> {SP.ld_e(key, STR.lword(key), x, l, TB.nths(ks, UD.v(H.slot(l))), e) == B.mstep(key, TB.dec_c(x, l, ks, e)) : B.MS}:
82 match e:
83 case True{}:
84 {==}
85 case False{}:
86 +h2 = B.imp_elim(Bool.not(U32.is_eq(x, 0)), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(ks, UD.v(H.slot(l)))))), hinv, 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), {==}))
87 dsh(key, hk, x, l, TB.nths(ks, UD.v(H.slot(l))), h2, H.is_short(x), {==})
88
89# THEOREM: a long-key step decides as the model's step on the decoded bucket.
90def decide(+key: String, +hk: {K.shortk(key) == False{} : Bool}, +x: U32, +l: U32, +ks: List<&2, String>, +hinv: {B.implies(Bool.not(U32.is_eq(x, 0)), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(ks, UD.v(H.slot(l))))))) == True{} : Bool}) -> {SP.ldec(key, STR.lword(key), x, l, TB.nths(ks, UD.v(H.slot(l)))) == B.mstep(key, TB.dec_c(x, l, ks, U32.is_eq(x, 0))) : B.MS}:
91 dec_e(key, hk, x, l, ks, hinv, U32.is_eq(x, 0), {==})