proofs/containers/hash_table/probe_impl.bend
bend-collections-laws-containers@1.0.0.0 · 184 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/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
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/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/step.bend as SP
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/arr.bend as AX
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/containers/hash_table/modn.bend as MN
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/words32.bend as W32
20
21# The implementation's long-key probe loop (find over step) refines the
22# model loop B.pf on the decoded buckets; the stored keys are unchanged.
23
24def or_true_r(+a: Bool) -> {Bool.or(a, True{}) == True{} : Bool}:
25 match a:
26 case True{}:
27 {==}
28 case False{}:
29 {==}
30
31def wb_sh(+x: U32, +l: U32, +kl: List<&2, String>, +sh: Bool, +hsh: {H.is_short(x) == sh : Bool}, +h: {U32.is_eq(x, K.kword(TB.keyof_c(x, TB.nths(kl, UD.v(H.slot(l))), sh))) == True{} : Bool}) -> {B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(kl, UD.v(H.slot(l)))))) == True{} : Bool}:
32 match sh:
33 case True{}:
34 L.subst(Bool, b => {B.implies(Bool.not(b), U32.is_eq(x, K.kword(TB.nths(kl, UD.v(H.slot(l)))))) == True{} : Bool}, True{}, H.is_short(x), Equal.sym(Bool, H.is_short(x), True{}, hsh), {==})
35 case False{}:
36 L.subst(Bool, b => {B.implies(Bool.not(b), U32.is_eq(x, K.kword(TB.nths(kl, UD.v(H.slot(l)))))) == True{} : Bool}, False{}, H.is_short(x), Equal.sym(Bool, H.is_short(x), False{}, hsh), h)
37
38def wb_facts(+sd: Nat, +x: U32, +l: U32, +kl: List<&2, String>, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}, +hw: {B.wb(sd, TB.dec_c(x, l, kl, e)) == True{} : Bool}) -> {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(kl, UD.v(H.slot(l))))))) == True{} : Bool}:
39 match e:
40 case True{}:
41 (L.subst(Bool, b => {B.implies(Bool.not(b), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, True{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), True{}, he), {==}),
42 L.subst(Bool, b => {B.implies(Bool.not(b), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(TB.nths(kl, UD.v(H.slot(l))))))) == True{} : Bool}, True{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), True{}, he), {==}))
43 case False{}:
44 +s = TB.nths(kl, UD.v(H.slot(l)))
45 +ha = L.and_left(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(x, K.kword(TB.keyof(x, s))), Bool.not(U32.is_eq(l, 0))), hw)
46 +hb = L.and_left(U32.is_eq(x, K.kword(TB.keyof(x, s))), 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(TB.keyof(x, s))), Bool.not(U32.is_eq(l, 0))), hw))
47 (L.subst(Bool, b => {B.implies(Bool.not(b), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, False{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), False{}, he), ha),
48 L.subst(Bool, b => {B.implies(Bool.not(b), B.implies(Bool.not(H.is_short(x)), U32.is_eq(x, K.kword(s)))) == True{} : Bool}, False{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), False{}, he), wb_sh(x, l, kl, H.is_short(x), {==}, hb)))
49
50# ---- the stored keys after a step ----
51
52def ka_w_ok(+sd: Nat, +K: AR.Tree<String>, +l: U32, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +same: Bool) -> {AR.slots(String, SP.ka_w(sd, K, l, same)) == AR.slots(String, K) : List<&2, String>} & {AR.perfect(String, sd, SP.ka_w(sd, K, l, same)) == True{} : Bool}:
53 match same:
54 case False{}:
55 ({==}, pk)
56 case True{}:
57 (SP.kcmp_slots(sd, K, l, hs, pk), SP.kcmp_perfect(sd, K, l, pk))
58
59def ka_e_ok(+sd: Nat, +K: AR.Tree<String>, +w: U32, +x: U32, +l: U32, +hs: {B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}) -> {AR.slots(String, SP.ka_e(sd, K, w, x, l, e)) == AR.slots(String, K) : List<&2, String>} & {AR.perfect(String, sd, SP.ka_e(sd, K, w, x, l, e)) == True{} : Bool}:
60 match e:
61 case True{}:
62 ({==}, pk)
63 case False{}:
64 ka_w_ok(sd, K, l, 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), {==})), pk, U32.is_eq(x, w))
65
66def kafter_ok(+sd: Nat, +K: AR.Tree<String>, +w: U32, +x: U32, +l: U32, +hs: {B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd))) == True{} : Bool}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}) -> {AR.slots(String, SP.kafter(sd, K, w, x, l)) == AR.slots(String, K) : List<&2, String>} & {AR.perfect(String, sd, SP.kafter(sd, K, w, x, l)) == True{} : Bool}:
67 ka_e_ok(sd, K, w, x, l, hs, pk, U32.is_eq(x, 0), {==})
68
69# ---- the result of the loop ----
70
71def fd_of(r: B.Res, tab: Array<U32>, ks: Array<String>, key: String) -> H.Found:
72 match r:
73 case B.RHit{+a, +l}:
74 H.FD{tab, ks, key, U32.from_nat(a), l}
75 case B.REnd{+a}:
76 H.FD{tab, ks, key, U32.from_nat(a), 0}
77
78def FindOK(+tabT: AR.Tree<U32>, +sd: Nat, +kl0: List<&2, String>, +key: String, r: B.Res, fd: H.Found) -> Type:
79 Sigma<&1, &1, AR.Tree<String>, K2 => {fd == fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), key) : H.Found} & ({AR.slots(String, K2) == kl0 : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})>
80
81# a U32 is the U32 of its value
82def from_v(+i: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), SC.pow2(k)) == True{} : Bool}) -> {U32.from_nat(UD.v(i)) == i : U32}:
83 U.injective(U32.from_nat(UD.v(i)), i, U.to_nat_from_nat(UD.v(i), k, hk, hi))
84
85# bucket i read through the word/link indices 2i, 2i + 1
86def dec_ix(+tb: List<&2, U32>, +kl: List<&2, String>, +i: Nat, +a: Nat, +b: Nat, +ea: {a == Nat.double(i) : Nat}, +eb: {b == 1n+Nat.double(i) : Nat}) -> {TB.dec_c(W32.nth0(tb, a), W32.nth0(tb, b), kl, U32.is_eq(W32.nth0(tb, a), 0)) == TB.dec(tb, kl, i) : B.Bk}:
87 +e1 = L.subst(Nat, z => {TB.dec_c(W32.nth0(tb, z), W32.nth0(tb, b), kl, U32.is_eq(W32.nth0(tb, z), 0)) == TB.dec_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, b), kl, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0)) : B.Bk}, Nat.double(i), a, Equal.sym(Nat, a, Nat.double(i), ea), {==})
88 Equal.trans(B.Bk, TB.dec_c(W32.nth0(tb, a), W32.nth0(tb, b), kl, U32.is_eq(W32.nth0(tb, a), 0)), TB.dec_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, b), kl, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0)), TB.dec(tb, kl, i), e1,
89 Equal.cong(Nat, B.Bk, z => TB.dec_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, z), kl, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0)), b, 1n+Nat.double(i), eb))
90
91def fm0(+tabT: AR.Tree<U32>, +sd: Nat, +kl0: List<&2, String>, +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}, +K1: AR.Tree<String>, +hs1: {AR.slots(String, K1) == kl0 : List<&2, String>}, +pk1: {AR.perfect(String, sd, K1) == True{} : Bool}, +ms: B.MS) -> FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 0n, ms, UD.v(i)), H.find(0n, SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), mask, w, i)):
92 match ms:
93 case B.MEnd{}:
94 (K1, (Equal.cong(U32, H.Found, z => H.FD{AR.thaw(U32, tabT), AR.thaw(String, K1), key, z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, from_v(i, k, hk, hi))), (hs1, pk1)))
95 case B.MHit{+l}:
96 (K1, (Equal.cong(U32, H.Found, z => H.FD{AR.thaw(U32, tabT), AR.thaw(String, K1), key, z, l}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, from_v(i, k, hk, hi))), (hs1, pk1)))
97 case B.MNext{}:
98 (K1, (Equal.cong(U32, H.Found, z => H.FD{AR.thaw(U32, tabT), AR.thaw(String, K1), key, z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, from_v(i, k, hk, hi))), (hs1, pk1)))
99
100def fm1(+tabT: AR.Tree<U32>, +sd: Nat, +kl0: List<&2, String>, +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}, +K1: AR.Tree<String>, +hs1: {AR.slots(String, K1) == kl0 : List<&2, String>}, +pk1: {AR.perfect(String, sd, K1) == True{} : Bool}, +p: Nat, +hnext: {UD.v(H.bnext(i, mask)) == Nat.mod(1n+UD.v(i), n) : Nat}, rec: FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, p, B.mstep(key, B.at(bs, UD.v(H.bnext(i, mask)))), UD.v(H.bnext(i, mask))), H.find(p, H.step(AR.thaw(U32, tabT), AR.thaw(String, K1), H.bnext(i, mask), key, w), mask, w, H.bnext(i, mask))), +ms: B.MS) -> FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 1n+p, ms, UD.v(i)), H.find(1n+p, SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), mask, w, i)):
101 match ms:
102 case B.MEnd{}:
103 (K1, (Equal.cong(U32, H.Found, z => H.FD{AR.thaw(U32, tabT), AR.thaw(String, K1), key, z, 0}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, from_v(i, k, hk, hi))), (hs1, pk1)))
104 case B.MHit{+l}:
105 (K1, (Equal.cong(U32, H.Found, z => H.FD{AR.thaw(U32, tabT), AR.thaw(String, K1), key, z, l}, i, U32.from_nat(UD.v(i)), Equal.sym(U32, U32.from_nat(UD.v(i)), i, from_v(i, k, hk, hi))), (hs1, pk1)))
106 case B.MNext{}:
107 L.subst(Nat, z => FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, p, B.mstep(key, B.at(bs, z)), z), H.find(p, H.step(AR.thaw(U32, tabT), AR.thaw(String, K1), H.bnext(i, mask), key, w), mask, w, H.bnext(i, mask))), UD.v(H.bnext(i, mask)), Nat.mod(1n+UD.v(i), n), hnext, rec)
108
109def mod_lt(+n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +x: Nat) -> {Nat.is_lt(Nat.mod(x, n), n) == True{} : Bool}:
110 match n:
111 case 0n:
112 Empty.absurd({Nat.is_lt(Nat.mod(x, 0n), 0n) == True{} : Bool}, L.false_true(hn))
113 case 1n+bp:
114 MN.dm_lt(bp, x)
115
116# THEOREM: the implementation's long-key probe loop is the model loop B.pf on
117# the decoded buckets (a table of 2^k buckets, word/link pairs in tabT, the
118# stored keys unchanged).
119def find_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, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +key: String, +hkey: {K.shortk(key) == False{} : 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}, +K: AR.Tree<String>, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}) -> FindOK(tabT, sd, kl0, key, B.pf(key, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), f, B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(i))), UD.v(i)), H.find(f, H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, STR.lword(key)), CY.msk(k), STR.lword(key), i)):
120 match f:
121 case 0n:
122 +tb = AR.slots(U32, tabT)
123 +n = SC.pow2(k)
124 +bs = TB.buckets(tb, kl0, n)
125 +w = STR.lword(key)
126 +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
127 +ew = AX.ix_w(i, 1n+k, hk31, hb)
128 +el = AX.ix_l(i, 1n+k, hk31, hb)
129 +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))
130 +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)
131 +x = W32.nth0(tb, UD.v(U32.shl(i)))
132 +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
133 +dx = dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
134 +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
135 +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))
136 +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))
137 +hsI = Pair.fst({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}, wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
138 +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}, wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
139 +ms = SP.ldec(key, w, x, l, TB.nths(AR.slots(String, K), UD.v(H.slot(l))))
140 +em = Equal.trans(B.MS, ms, SP.ldec(key, w, x, l, TB.nths(kl0, UD.v(H.slot(l)))), B.mstep(key, B.at(bs, UD.v(i))),
141 Equal.cong(List<&2, String>, B.MS, z => SP.ldec(key, w, x, l, TB.nths(z, UD.v(H.slot(l)))), AR.slots(String, K), kl0, hsl),
142 Equal.trans(B.MS, SP.ldec(key, w, x, l, TB.nths(kl0, UD.v(H.slot(l)))), B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), DC.decide(key, hkey, 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))))
143 +K1 = SP.kafter(sd, K, w, x, l)
144 +hs1 = Equal.trans(List<&2, String>, AR.slots(String, K1), AR.slots(String, K), kl0, Pair.fst({AR.slots(String, K1) == AR.slots(String, K) : List<&2, String>}, {AR.perfect(String, sd, K1) == True{} : Bool}, kafter_ok(sd, K, w, x, l, hsI, pk)), hsl)
145 +pk1 = Pair.snd({AR.slots(String, K1) == AR.slots(String, K) : List<&2, String>}, {AR.perfect(String, sd, K1) == True{} : Bool}, kafter_ok(sd, K, w, x, l, hsI, pk))
146 +es = SP.step_long(1n+k, tabT, sd, K, i, key, w, hk31, hsd, pt, pk, hwb0, hlb0, hsI)
147 +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
148 p3 = fm0(tabT, sd, kl0, key, bs, n, CY.msk(k), w, i, k, hk32, hi, K1, hs1, pk1, ms)
149 p2 = L.subst(B.MS, m => FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 0n, m, UD.v(i)), H.find(0n, SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), CY.msk(k), w, i)), ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
150 L.subst(H.Step, s => FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 0n, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), H.find(0n, s, CY.msk(k), w, i)), SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), Equal.sym(H.Step, H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), es), p2)
151 case 1n+p:
152 +tb = AR.slots(U32, tabT)
153 +n = SC.pow2(k)
154 +bs = TB.buckets(tb, kl0, n)
155 +w = STR.lword(key)
156 +hb = N.double_lt_bit(True{}, UD.v(i), SC.pow2(k), hi)
157 +ew = AX.ix_w(i, 1n+k, hk31, hb)
158 +el = AX.ix_l(i, 1n+k, hk31, hb)
159 +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))
160 +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)
161 +x = W32.nth0(tb, UD.v(U32.shl(i)))
162 +l = W32.nth0(tb, UD.v(U32.inc(U32.shl(i))))
163 +dx = dec_ix(tb, kl0, UD.v(i), UD.v(U32.shl(i)), UD.v(U32.inc(U32.shl(i))), ew, el)
164 +dat = TB.at_buckets(tb, kl0, n, UD.v(i), hi)
165 +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))
166 +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))
167 +hsI = Pair.fst({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}, wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
168 +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}, wb_facts(sd, x, l, kl0, U32.is_eq(x, 0), {==}, hwb))
169 +ms = SP.ldec(key, w, x, l, TB.nths(AR.slots(String, K), UD.v(H.slot(l))))
170 +em = Equal.trans(B.MS, ms, SP.ldec(key, w, x, l, TB.nths(kl0, UD.v(H.slot(l)))), B.mstep(key, B.at(bs, UD.v(i))),
171 Equal.cong(List<&2, String>, B.MS, z => SP.ldec(key, w, x, l, TB.nths(z, UD.v(H.slot(l)))), AR.slots(String, K), kl0, hsl),
172 Equal.trans(B.MS, SP.ldec(key, w, x, l, TB.nths(kl0, UD.v(H.slot(l)))), B.mstep(key, TB.dec_c(x, l, kl0, U32.is_eq(x, 0))), B.mstep(key, B.at(bs, UD.v(i))), DC.decide(key, hkey, 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))))
173 +K1 = SP.kafter(sd, K, w, x, l)
174 +hs1 = Equal.trans(List<&2, String>, AR.slots(String, K1), AR.slots(String, K), kl0, Pair.fst({AR.slots(String, K1) == AR.slots(String, K) : List<&2, String>}, {AR.perfect(String, sd, K1) == True{} : Bool}, kafter_ok(sd, K, w, x, l, hsI, pk)), hsl)
175 +pk1 = Pair.snd({AR.slots(String, K1) == AR.slots(String, K) : List<&2, String>}, {AR.perfect(String, sd, K1) == True{} : Bool}, kafter_ok(sd, K, w, x, l, hsI, pk))
176 +es = SP.step_long(1n+k, tabT, sd, K, i, key, w, hk31, hsd, pt, pk, hwb0, hlb0, hsI)
177 +hk32 = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==}))
178 +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)))
179 +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)
180 +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))))
181 +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), mod_lt(n, N.succ_le_lt(0n, n, N.pow2_pos(k)), 1n+UD.v(i)))
182 p3 = fm1(tabT, sd, kl0, key, bs, n, CY.msk(k), w, i, k, hk32, hi, K1, hs1, pk1, p, hnext, find_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, key, hkey, hwell, p, H.bnext(i, CY.msk(k)), hi2, K1, hs1, pk1), ms)
183 p2 = L.subst(B.MS, m => FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 1n+p, m, UD.v(i)), H.find(1n+p, SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), CY.msk(k), w, i)), ms, B.mstep(key, B.at(bs, UD.v(i))), em, p3)
184 L.subst(H.Step, s => FindOK(tabT, sd, kl0, key, B.pf(key, bs, n, 1n+p, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)), H.find(1n+p, s, CY.msk(k), w, i)), SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), Equal.sym(H.Step, H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), SP.step_of(ms, AR.thaw(U32, tabT), AR.thaw(String, K1), key), es), p2)