proofs/containers/hash_table/qprobe.bend
bend-collections-laws-containers@1.0.0.0 · 210 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/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/words.bend as WR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
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/containers/hash_table/arr.bend as AX
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/decide.bend as DC
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_impl.bend as PI
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as WD
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as UW
20import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
21
22# One-character keys below 2^31: the probe decides on bucket words alone.
23
24def qd_w(+l: U32, same: Bool) -> B.MS:
25 match same:
26 case True{}:
27 B.MHit{l}
28 case False{}:
29 B.MNext{}
30
31def qd_e(+w: U32, +x: U32, +l: U32, empty: Bool) -> B.MS:
32 match empty:
33 case True{}:
34 B.MEnd{}
35 case False{}:
36 qd_w(l, U32.is_eq(x, w))
37
38def qdec(+w: U32, +x: U32, +l: U32) -> B.MS:
39 qd_e(w, x, l, U32.is_eq(x, 0))
40
41def qstep_of(ms: B.MS, tab: Array<U32>) -> H.QStep:
42 match ms:
43 case B.MEnd{}:
44 H.QEnd{tab}
45 case B.MHit{l}:
46 H.QHit{tab, l}
47 case B.MNext{}:
48 H.QNext{tab}
49
50def qs_same(+td: Nat, +tabT: AR.Tree<U32>, +i: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +same: Bool) -> {H.qs_same(AR.thaw(U32, tabT), i, same) == qstep_of(qd_w(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), same), AR.thaw(U32, tabT)) : H.QStep}:
51 match same:
52 case True{}:
53 Equal.cong(Array<U32> & U32, H.QStep, r => H.qs_l(r), Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(i))), (AR.thaw(U32, tabT), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i))))), AX.getw(td, tabT, U32.inc(U32.shl(i)), hd, hl, pt))
54 case False{}:
55 {==}
56
57def qs_if(+td: Nat, +tabT: AR.Tree<U32>, +i: U32, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +x: U32, +e: Bool) -> {H.qs_if(AR.thaw(U32, tabT), i, w, x, e) == qstep_of(qd_e(w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), e), AR.thaw(U32, tabT)) : H.QStep}:
58 match e:
59 case True{}:
60 {==}
61 case False{}:
62 qs_same(td, tabT, i, hd, pt, hl, U32.is_eq(x, w))
63
64# THEOREM: a short-key probe step reads bucket i and decides as qdec.
65def qstep(+td: Nat, +tabT: AR.Tree<U32>, +i: U32, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == 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}) -> {H.qstep(AR.thaw(U32, tabT), i, w) == qstep_of(qdec(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))))), AR.thaw(U32, tabT)) : H.QStep}:
66 +x = W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i)))
67 Equal.trans(H.QStep, H.qs_w(i, w, Array.get(U32, AR.thaw(U32, tabT), U32.shl(i))), H.qs_w(i, w, (AR.thaw(U32, tabT), x)), qstep_of(qdec(w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i))))), AR.thaw(U32, tabT)),
68 Equal.cong(Array<U32> & U32, H.QStep, r => H.qs_w(i, w, r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(i)), (AR.thaw(U32, tabT), x), AX.getw(td, tabT, U32.shl(i), hd, hw, pt)),
69 qs_if(td, tabT, i, w, hd, pt, hl, x, U32.is_eq(x, 0)))
70
71
72
73# ---- the short-key decision ----
74
75def eqc_false(+x: U32, +c: U32, +hx: {H.is_short(x) == True{} : Bool}, +hs: {U32.is_eq(x, H.short_word(c)) == False{} : Bool}, +e: Bool, +he: {U32.is_eq(U32.and(x, 2147483647), c) == e : Bool}) -> {e == False{} : Bool}:
76 match e:
77 case False{}:
78 {==}
79 case True{}:
80 +xc = Equal.trans(U32, x, H.short_word(U32.and(x, 2147483647)), H.short_word(c), Equal.sym(U32, H.short_word(U32.and(x, 2147483647)), x, WR.short_eta(x, hx)), Equal.cong(U32, U32, z => H.short_word(z), U32.and(x, 2147483647), c, A.eq_of(U32.and(x, 2147483647), c, he)))
81 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, U32.is_eq(x, H.short_word(c)), False{}, L.subst(U32, z => {True{} == U32.is_eq(x, z) : Bool}, x, H.short_word(c), xc, Equal.sym(Bool, U32.is_eq(x, x), True{}, UW.u32_eq_refl(x))), hs)))
82
83def qd_short(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +x: U32, +l: U32, +hx: {H.is_short(x) == True{} : Bool}, +s: Bool, +hs: {U32.is_eq(x, H.short_word(c)) == s : Bool}) -> {qd_w(l, s) == Bool.pick(B.MS, S.str_eq(SCon{Chr{U32.and(x, 2147483647)}, SNil{}}, SCon{Chr{c}, SNil{}}), B.MHit{l}, B.MNext{}) : B.MS}:
84 match s:
85 case True{}:
86 +ac = Equal.trans(U32, U32.and(x, 2147483647), U32.and(H.short_word(c), 2147483647), c, Equal.cong(U32, U32, z => U32.and(z, 2147483647), x, H.short_word(c), A.eq_of(x, H.short_word(c), hs)), WR.short_back(c, hc))
87 +t = L.subst(U32, z => {U32.is_eq(z, c) == True{} : Bool}, c, U32.and(x, 2147483647), Equal.sym(U32, U32.and(x, 2147483647), c, ac), UW.u32_eq_refl(c))
88 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), True{}, Bool.and(U32.is_eq(U32.and(x, 2147483647), c), True{}), Equal.sym(Bool, Bool.and(U32.is_eq(U32.and(x, 2147483647), c), True{}), True{}, L.subst(Bool, b => {Bool.and(b, True{}) == True{} : Bool}, True{}, U32.is_eq(U32.and(x, 2147483647), c), Equal.sym(Bool, U32.is_eq(U32.and(x, 2147483647), c), True{}, t), {==})))
89 case False{}:
90 +f = eqc_false(x, c, hx, hs, U32.is_eq(U32.and(x, 2147483647), c), {==})
91 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), False{}, Bool.and(U32.is_eq(U32.and(x, 2147483647), c), True{}), Equal.sym(Bool, Bool.and(U32.is_eq(U32.and(x, 2147483647), c), True{}), False{}, L.subst(Bool, b => {Bool.and(b, True{}) == False{} : Bool}, False{}, U32.is_eq(U32.and(x, 2147483647), c), Equal.sym(Bool, U32.is_eq(U32.and(x, 2147483647), c), False{}, f), {==})))
92
93# a long bucket never holds a one-character key below 2^31
94def ql_false(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +x: U32, +k: String, +hx: {H.is_short(x) == False{} : Bool}, +hinv: {x == K.kword(k) : U32}, +e: Bool, +he: {S.str_eq(k, SCon{Chr{c}, SNil{}}) == e : Bool}) -> {e == False{} : Bool}:
95 match e:
96 case False{}:
97 {==}
98 case True{}:
99 +xs = Equal.trans(U32, x, K.kword(k), H.short_word(c), hinv, Equal.trans(U32, K.kword(k), K.kword(SCon{Chr{c}, SNil{}}), H.short_word(c), Equal.cong(String, U32, z => K.kword(z), k, SCon{Chr{c}, SNil{}}, K.str_eq_of(k, SCon{Chr{c}, SNil{}}, he)), K.kword_short(c, hc)))
100 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, H.is_short(x), False{}, Equal.trans(Bool, True{}, H.is_short(H.short_word(c)), H.is_short(x), Equal.sym(Bool, H.is_short(H.short_word(c)), True{}, WR.short_is_short(c)), Equal.cong(U32, Bool, z => H.is_short(z), H.short_word(c), x, Equal.sym(U32, x, H.short_word(c), xs))), hx)))
101
102def qsh(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : 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}) -> {qd_w(l, U32.is_eq(x, H.short_word(c))) == B.mstep(SCon{Chr{c}, SNil{}}, B.BF{x, l, TB.keyof_c(x, k, sh)}) : B.MS}:
103 match sh:
104 case True{}:
105 qd_short(c, hc, x, l, hsh, U32.is_eq(x, H.short_word(c)), {==})
106 case False{}:
107 +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), {==}))
108 +ne = DC.kinds_ne(H.short_word(c), x, WR.short_is_short(c), hsh, U32.is_eq(H.short_word(c), x), {==})
109 +ne2 = Equal.trans(Bool, U32.is_eq(x, H.short_word(c)), U32.is_eq(H.short_word(c), x), False{}, W32.eq_sym_u32(x, H.short_word(c)), ne)
110 Equal.trans(B.MS, qd_w(l, U32.is_eq(x, H.short_word(c))), B.MNext{}, Bool.pick(B.MS, S.str_eq(k, SCon{Chr{c}, SNil{}}), B.MHit{l}, B.MNext{}),
111 Equal.cong(Bool, B.MS, b => qd_w(l, b), U32.is_eq(x, H.short_word(c)), False{}, ne2),
112 Equal.cong(Bool, B.MS, b => Bool.pick(B.MS, b, B.MHit{l}, B.MNext{}), False{}, S.str_eq(k, SCon{Chr{c}, SNil{}}), Equal.sym(Bool, S.str_eq(k, SCon{Chr{c}, SNil{}}), False{}, ql_false(c, hc, x, k, hsh, A.eq_of(x, K.kword(k), e), S.str_eq(k, SCon{Chr{c}, SNil{}}), {==}))))
113
114def qde(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +x: U32, +l: U32, +kl: 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(kl, UD.v(H.slot(l))))))) == True{} : Bool}, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}) -> {qd_e(H.short_word(c), x, l, e) == B.mstep(SCon{Chr{c}, SNil{}}, TB.dec_c(x, l, kl, e)) : B.MS}:
115 match e:
116 case True{}:
117 {==}
118 case False{}:
119 +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(kl, 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), {==}))
120 qsh(c, hc, x, l, TB.nths(kl, UD.v(H.slot(l))), h2, H.is_short(x), {==})
121
122# THEOREM: a short-key step decides as the model's step on the decoded bucket.
123def qdecide(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +x: U32, +l: U32, +kl: 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(kl, UD.v(H.slot(l))))))) == True{} : Bool}) -> {qdec(H.short_word(c), x, l) == B.mstep(SCon{Chr{c}, SNil{}}, TB.dec_c(x, l, kl, U32.is_eq(x, 0))) : B.MS}:
124 qde(c, hc, x, l, kl, hinv, U32.is_eq(x, 0), {==})
125
126# ---- the loop ----
127
128def qf_of(r: B.Res, tab: Array<U32>) -> H.QFound:
129 match r:
130 case B.RHit{+a, +l}:
131 H.QF{tab, U32.from_nat(a), l}
132 case B.REnd{+a}:
133 H.QF{tab, U32.from_nat(a), 0}
134
135def qm0(+tabT: AR.Tree<U32>, +key: String, +bs: List<&2, B.Bk>, +n: Nat, +mask: U32, +w: U32, +i: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}, +ms: B.MS) -> {H.qfind(0n, qstep_of(ms, AR.thaw(U32, tabT)), mask, w, i) == qf_of(B.pf(key, bs, n, 0n, ms, UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}:
136 match ms:
137 case B.MEnd{}:
138 Equal.cong(U32, H.QFound, z => H.QF{AR.thaw(U32, tabT), z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
139 case B.MHit{+l}:
140 Equal.cong(U32, H.QFound, z => H.QF{AR.thaw(U32, tabT), z, l}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
141 case B.MNext{}:
142 Equal.cong(U32, H.QFound, z => H.QF{AR.thaw(U32, tabT), z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
143
144def qm1(+tabT: AR.Tree<U32>, +key: String, +bs: List<&2, B.Bk>, +n: Nat, +mask: U32, +w: U32, +i: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}, +p: Nat, +hnext: {UD.v(H.bnext(i, mask)) == Nat.mod(1n+UD.v(i), n) : Nat}, +rec: {H.qfind(p, H.qstep(AR.thaw(U32, tabT), H.bnext(i, mask), w), mask, w, H.bnext(i, mask)) == qf_of(B.pf(key, bs, n, p, B.mstep(key, B.at(bs, UD.v(H.bnext(i, mask)))), UD.v(H.bnext(i, mask))), AR.thaw(U32, tabT)) : H.QFound}, +ms: B.MS) -> {H.qfind(1n+p, qstep_of(ms, AR.thaw(U32, tabT)), mask, w, i) == qf_of(B.pf(key, bs, n, 1n+p, ms, UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}:
145 match ms:
146 case B.MEnd{}:
147 Equal.cong(U32, H.QFound, z => H.QF{AR.thaw(U32, tabT), z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
148 case B.MHit{+l}:
149 Equal.cong(U32, H.QFound, z => H.QF{AR.thaw(U32, tabT), z, l}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, PI.from_v(i, k, hk, hi)))
150 case B.MNext{}:
151 L.subst(Nat, z => {H.qfind(p, H.qstep(AR.thaw(U32, tabT), H.bnext(i, mask), w), mask, w, H.bnext(i, mask)) == qf_of(B.pf(key, bs, n, p, B.mstep(key, B.at(bs, z)), z), AR.thaw(U32, tabT)) : H.QFound}, UD.v(H.bnext(i, mask)), Nat.mod(1n+UD.v(i), n), hnext, rec)
152
153# THEOREM: the implementation's short-key probe loop is the model loop B.pf
154# on the decoded buckets for the key SCon{Chr{c}, ""}.
155def qfind_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree<U32>, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +kl0: List<&2, String>, +c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +f: Nat, +i: U32, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}) -> {H.qfind(f, H.qstep(AR.thaw(U32, tabT), i, H.short_word(c)), CY.msk(k), H.short_word(c), i) == qf_of(B.pf(SCon{Chr{c}, SNil{}}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), f, B.mstep(SCon{Chr{c}, SNil{}}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(i))), UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}:
156 match f:
157 case 0n:
158 +tb = AR.slots(U32, tabT)
159 +n = SC.pow2(k)
160 +bs = TB.buckets(tb, kl0, n)
161 +w = H.short_word(c)
162 +key = {SCon{Chr{c}, SNil{}} : String}
163 +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
164 +ew = AX.ix_w(i, 1n+k, hk31, hb)
165 +el = AX.ix_l(i, 1n+k, hk31, hb)
166 +hwb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(UD.v(i)), UD.v(U32.shl(i)), Equal.sym(Nat, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew), N.lt_trans(Nat.double(UD.v(i)), 1n+Nat.double(UD.v(i)), SC.pow2(1n+k), N.lt_succ(Nat.double(UD.v(i))), hb))
167 +hlb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(UD.v(i)), UD.v(U32.inc(U32.shl(i))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(i))), 1n+Nat.double(UD.v(i)), el), hb)
168 +x = W32.nth0(tb, UD.v(U32.shl(i)))
169 +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
170 +dx = PI.dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
171 +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
172 +dd = Equal.trans(B.Bk, B.at(bs, UD.v(i)), TB.dec(tb, kl0, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dat, Equal.sym(B.Bk, TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), TB.dec(tb, kl0, UD.v(i)), dx))
173 +hwb = L.subst(B.Bk, b => {B.wb(sd, b) == True{} : Bool}, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd, B.all_inst(B.PWell{bs, sd}, n, hwell, UD.v(i), hi))
174 +hvI = Pair.snd({B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, {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(kl0, UD.v(H.slot(l))))))) == True{} : Bool}, PI.wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
175 +ms = qdec(w, x, l)
176 +em = Equal.trans(B.MS, ms, B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), qdecide(c, hc, x, l, kl0, hvI), Equal.cong(B.Bk, B.MS, b => B.mstep(key, b), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), B.at(bs, UD.v(i)), Equal.sym(B.Bk, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd)))
177 +es = qstep(1n+k, tabT, i, w, hk31, pt, hwb0, hlb0)
178 +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
179 +p3 = qm0(tabT, key, bs, n, CY.msk(k), w, i, k, hk32, hi, ms)
180 +p2 = L.subst(B.MS, m => {H.qfind(0n, qstep_of(ms, AR.thaw(U32, tabT)), CY.msk(k), w, i) == qf_of(B.pf(key, bs, n, 0n, m, UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}, ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
181 L.subst(H.QStep, s => {H.qfind(0n, s, CY.msk(k), w, i) == qf_of(B.pf(key, bs, n, 0n, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}, qstep_of(ms, AR.thaw(U32, tabT)), H.qstep(AR.thaw(U32, tabT), i, w), Equal.sym(H.QStep, H.qstep(AR.thaw(U32, tabT), i, w), qstep_of(ms, AR.thaw(U32, tabT)), es), p2)
182 case 1n+p:
183 +tb = AR.slots(U32, tabT)
184 +n = SC.pow2(k)
185 +bs = TB.buckets(tb, kl0, n)
186 +w = H.short_word(c)
187 +key = {SCon{Chr{c}, SNil{}} : String}
188 +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
189 +ew = AX.ix_w(i, 1n+k, hk31, hb)
190 +el = AX.ix_l(i, 1n+k, hk31, hb)
191 +hwb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, Nat.double(UD.v(i)), UD.v(U32.shl(i)), Equal.sym(Nat, UD.v(U32.shl(i)), Nat.double(UD.v(i)), ew), N.lt_trans(Nat.double(UD.v(i)), 1n+Nat.double(UD.v(i)), SC.pow2(1n+k), N.lt_succ(Nat.double(UD.v(i))), hb))
192 +hlb0 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+k)) == True{} : Bool}, 1n+Nat.double(UD.v(i)), UD.v(U32.inc(U32.shl(i))), Equal.sym(Nat, UD.v(U32.inc(U32.shl(i))), 1n+Nat.double(UD.v(i)), el), hb)
193 +x = W32.nth0(tb, UD.v(U32.shl(i)))
194 +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
195 +dx = PI.dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
196 +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
197 +dd = Equal.trans(B.Bk, B.at(bs, UD.v(i)), TB.dec(tb, kl0, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dat, Equal.sym(B.Bk, TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), TB.dec(tb, kl0, UD.v(i)), dx))
198 +hwb = L.subst(B.Bk, b => {B.wb(sd, b) == True{} : Bool}, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd, B.all_inst(B.PWell{bs, sd}, n, hwell, UD.v(i), hi))
199 +hvI = Pair.snd({B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, {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(kl0, UD.v(H.slot(l))))))) == True{} : Bool}, PI.wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
200 +ms = qdec(w, x, l)
201 +em = Equal.trans(B.MS, ms, B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), qdecide(c, hc, x, l, kl0, hvI), Equal.cong(B.Bk, B.MS, b => B.mstep(key, b), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), B.at(bs, UD.v(i)), Equal.sym(B.Bk, B.at(bs, UD.v(i)), TB.dec_c(x, l, kl0, U32.is_eq(x, 0)), dd)))
202 +es = qstep(1n+k, tabT, i, w, hk31, pt, hwb0, hlb0)
203 +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
204 +hks = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k), N.lt_le_trans(SC.pow2(k), SC.pow2(1n+k), WD.sc(32n, one), N.pow2_lt_succ(k), W32.pow_le32(one, h1, 1n+k, hk31)))
205 +hi1 = L.subst(Nat, z => {Nat.is_lt(UD.v(i), z) == True{} : Bool}, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k), hi)
206 +hnext = Equal.trans(Nat, UD.v(H.bnext(i, CY.msk(k))), Nat.mod(1n+UD.v(i), WD.sc(k, one)), Nat.mod(1n+UD.v(i), n), CY.next_val(one, h1, k, i, hks, hi1), Equal.cong(Nat, Nat, z => Nat.mod(1n+UD.v(i), z), WD.sc(k, one), SC.pow2(k), Equal.sym(Nat, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k))))
207 +hi2 = L.subst(Nat, z => {Nat.is_lt(z, n) == True{} : Bool}, Nat.mod(1n+UD.v(i), n), UD.v(H.bnext(i, CY.msk(k))), Equal.sym(Nat, UD.v(H.bnext(i, CY.msk(k))), Nat.mod(1n+UD.v(i), n), hnext), PI.mod_lt(n, N.succ_le_lt(0n, n, N.pow2_pos(k)), 1n+UD.v(i)))
208 +p3 = qm1(tabT, key, bs, n, CY.msk(k), w, i, k, hk32, hi, p, hnext, qfind_ok(one, h1, k, hk31, tabT, pt, sd, kl0, c, hc, hwell, p, H.bnext(i, CY.msk(k)), hi2), ms)
209 +p2 = L.subst(B.MS, m => {H.qfind(1n+p, qstep_of(ms, AR.thaw(U32, tabT)), CY.msk(k), w, i) == qf_of(B.pf(key, bs, n, 1n+p, m, UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}, ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
210 L.subst(H.QStep, s => {H.qfind(1n+p, s, CY.msk(k), w, i) == qf_of(B.pf(key, bs, n, 1n+p, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), AR.thaw(U32, tabT)) : H.QFound}, qstep_of(ms, AR.thaw(U32, tabT)), H.qstep(AR.thaw(U32, tabT), i, w), Equal.sym(H.QStep, H.qstep(AR.thaw(U32, tabT), i, w), qstep_of(ms, AR.thaw(U32, tabT)), es), p2)