1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../lib/u32div.bend as UD 8 import ../../../src/containers/hash_table.bend as H 9 import ./strings.bend as STR 10 import ./keys.bend as K 11 import ./table.bend as TB 12 import ./buckets.bend as B 13 import ./step.bend as SP 14 import ./decide.bend as DC 15 import ./arr.bend as AX 16 import ./cyc.bend as CY 17 import ./modn.bend as MN 18 import ../../lib/word.bend as WD 19 import ../../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 24 def or_true_r(+a: Bool) -> {Bool.or(a, True{}) == True{} : Bool}: 25 match a: 26 case True{}: 27 {==} 28 case False{}: 29 {==} 30 31 def 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 38 def 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 52 def ka_w_ok(+sd: Nat, +K: AR.Tree, +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 59 def ka_e_ok(+sd: Nat, +K: AR.Tree, +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 66 def kafter_ok(+sd: Nat, +K: AR.Tree, +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 71 def fd_of(r: B.Res, tab: Array, ks: Array, 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 78 def FindOK(+tabT: AR.Tree, +sd: Nat, +kl0: List<&2, String>, +key: String, r: B.Res, fd: H.Found) -> Type: 79 Sigma<&1, &1, AR.Tree, 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 82 def 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 86 def 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 91 def fm0(+tabT: AR.Tree, +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, +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 100 def fm1(+tabT: AR.Tree, +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, +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 109 def 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). 119 def find_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +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, +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)