~/bend-docscommunity

proofs/containers/hash_table/set.bend source

proofs/containers/hash_table/set.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/hash_table.bend as Himport ./table.bend as TBimport ./buckets.bend as Bimport ./cyc.bend as CYimport ./state.bend as STimport ./lookup.bend as LKimport ./speclem.bend as SLimport ./size.bend as SZimport ./setv.bend as SVimport ./rebuild.bend as RBimport ./inv.bend as IVimport ./keysw.bend as KW# set: the implementation's set agrees with the specification's set, for# every key's lookup and for the size.# If the key was already present, set only replaces its value: the key# sequence (the model's keys, in iteration order) is unchanged.def KeepK(~V: Data, +sh: ST.Sh<V>, +sh2: ST.Sh<V>, +key: String) -> Type:  @+hp: {S.has(~V, ST.model(~V, sh), key) == True{} : Bool} -> {S.keys(~V, ST.model(~V, sh2)) == S.keys(~V, ST.model(~V, sh)) : List<&2, String>}def SetOK(~V: Data, +sh: ST.Sh<V>, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type:  Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & (({ST.good(~V, sh2) == True{} : Bool} & ((@+q: String -> {S.lookup(~V, ST.model(~V, sh2), q) == S.lookup(~V, S.set(~V, ST.model(~V, sh), key, x), q) : Maybe<&2, V>}) & {S.size(~V, ST.model(~V, sh2)) == S.size(~V, S.set(~V, ST.model(~V, sh), key, x)) : Nat})) & KeepK(~V, sh, sh2, key))>def sz_old(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +mv: Maybe<&2, V>, +hmv: {S.lookup(~V, m, key) == mv : Maybe<&2, V>}, +hs: {ST.some_b(~V, mv) == True{} : Bool}) -> {S.size(~V, S.set(~V, m, key, x)) == S.size(~V, m) : Nat}:  match mv:    case None{}:      Empty.absurd({S.size(~V, S.set(~V, m, key, x)) == S.size(~V, m) : Nat}, L.false_true(hs))    case Some{+v0}:      SL.size_set_old(~V, m, key, x, v0, hmv)def hit_lk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +hr: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +q: String) -> {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q) == S.lookup(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x), q) : Maybe<&2, V>}:  +pv = ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +s = UD.v(H.slot(l))  +hlen = L.subst(Nat, z => {Nat.is_lt(s, z) == True{} : Bool}, SC.pow2(sd), SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), Equal.sym(Nat, SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), SC.pow2(sd), AR.slots_length(Maybe<&2, V>, sd, vsT, pv)), hr)  +es2 = AR.upd_slots(Maybe<&2, V>, sd, vsT, s, Some{x}, hr, pv)  +hl0 = Equal.cong(U32, Nat, z => UD.v(H.slot(z)), B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl)  +hlen0 = L.subst(Nat, z => {Nat.is_lt(z, SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT))) == True{} : Bool}, s, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Equal.sym(Nat, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), s, hl0), hlen)  +huq = ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Some{x}), SC.pow2(k), 0n), q), S.lookup(~V, S.set(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, x), q),    Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), s, Some{x}), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Some{x}), SC.pow2(k), 0n), q),      Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), s, Some{x}), SC.pow2(k), 0n), q),        Equal.cong(List<&2, String>, Maybe<&2, V>, z => S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n), q), AR.slots(String, K2), AR.slots(String, ksT), hsl2),        Equal.cong(List<&2, Maybe<&2, V>>, Maybe<&2, V>, z => S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k), 0n), q), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), s, Some{x}), es2)),      Equal.cong(Nat, Maybe<&2, V>, z => S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), z, Some{x}), SC.pow2(k), 0n), q), s, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Equal.sym(Nat, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), s, hl0))),    SV.lookup_upd(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), huq, i, hi, key, hk, hlen0, x, q))# the hit branch: write x into the slot of the bucket holding key# the hit writes a value slot only: the buckets, and so the keys, staydef keep_hit(~V: Data, +tb: List<&2, U32>, +kl: List<&2, String>, +kl2: List<&2, String>, +hsl: {kl2 == kl : List<&2, String>}, +nn: Nat, +vs1: List<&2, Maybe<&2, V>>, +vs2: List<&2, Maybe<&2, V>>, +fr: Nat, +hl1: {B.all_lt(B.PLive{TB.buckets(tb, kl, nn), ST.lvs(~V, vs1), fr}, nn) == True{} : Bool}, +hl2: {B.all_lt(B.PLive{TB.buckets(tb, kl2, nn), ST.lvs(~V, vs2), fr}, nn) == True{} : Bool}) -> {S.keys(~V, ST.absm(~V, TB.buckets(tb, kl2, nn), vs2, nn, 0n)) == S.keys(~V, ST.absm(~V, TB.buckets(tb, kl, nn), vs1, nn, 0n)) : List<&2, String>}:  Equal.trans(List<&2, String>, S.keys(~V, ST.absm(~V, TB.buckets(tb, kl2, nn), vs2, nn, 0n)), KW.kb(TB.buckets(tb, kl2, nn), nn, 0n), S.keys(~V, ST.absm(~V, TB.buckets(tb, kl, nn), vs1, nn, 0n)), KW.keys_absm(~V, TB.buckets(tb, kl2, nn), vs2, fr, nn, hl2, nn, 0n, N.le_refl(nn)),    Equal.trans(List<&2, String>, KW.kb(TB.buckets(tb, kl2, nn), nn, 0n), KW.kb(TB.buckets(tb, kl, nn), nn, 0n), S.keys(~V, ST.absm(~V, TB.buckets(tb, kl, nn), vs1, nn, 0n)), Equal.cong(List<&2, String>, List<&2, String>, z => KW.kb(TB.buckets(tb, z, nn), nn, 0n), kl2, kl, hsl),      Equal.sym(List<&2, String>, S.keys(~V, ST.absm(~V, TB.buckets(tb, kl, nn), vs1, nn, 0n)), KW.kb(TB.buckets(tb, kl, nn), nn, 0n), KW.keys_absm(~V, TB.buckets(tb, kl, nn), vs1, fr, nn, hl1, nn, 0n, N.le_refl(nn)))))def set_hit_case(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +x: V, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +hr: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +hlv: {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}) -> SetOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, x, H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), Some{x}), AR.thaw(U32, nxT)}):  +hsd = ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +pv = ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +s = UD.v(H.slot(l))  +hlen = L.subst(Nat, z => {Nat.is_lt(s, z) == True{} : Bool}, SC.pow2(sd), SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), Equal.sym(Nat, SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT)), SC.pow2(sd), AR.slots_length(Maybe<&2, V>, sd, vsT, pv)), hr)  +hset = AR.set(Maybe<&2, V>, sd, vsT, H.slot(l), Some{x}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), s), hsd, hr, ST.nthm_some(~V, AR.slots(Maybe<&2, V>, vsT), s, hlen), pv)  +es2 = AR.upd_slots(Maybe<&2, V>, sd, vsT, s, Some{x}, hr, pv)  +hl2 = L.subst(List<&2, Maybe<&2, V>>, z => {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, z), UD.v(fresh)}, SC.pow2(k)) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), s, Some{x}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), s, Some{x}), es2), SV.live_upd(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), s, x, hlen, SC.pow2(k), N.le_refl(SC.pow2(k))))  +g1 = RB.good_vs(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), AR.upd_perfect(Maybe<&2, V>, sd, vsT, s, Some{x}, pv), hl2)  +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +g2 = L.subst(List<&2, String>, z => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, z, AR.perfect(String, sd, K2), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), nxT) == True{} : Bool}, AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl2), L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), b, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), nxT) == True{} : Bool}, AR.perfect(String, sd, ksT), AR.perfect(String, sd, K2), Equal.trans(Bool, AR.perfect(String, sd, ksT), True{}, AR.perfect(String, sd, K2), pkT, Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2)), g1))  +hl0 = Equal.cong(U32, Nat, z => UD.v(H.slot(z)), B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl)  +hlen0 = L.subst(Nat, z => {Nat.is_lt(z, SC.length(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT))) == True{} : Bool}, s, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Equal.sym(Nat, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), s, hl0), hlen)  +huq = ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)  +m0 = ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)  +sz2 = Equal.trans(Nat, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), SC.pow2(k), 0n)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), SC.pow2(k)), S.size(~V, S.set(~V, m0, key, x)),    SZ.size_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, K2), AR.perfect(String, sd, K2), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), nxT, g2), SC.pow2(k), N.le_refl(SC.pow2(k))),    Equal.trans(Nat, IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, K2), SC.pow2(k)), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), S.size(~V, S.set(~V, m0, key, x)), Equal.cong(List<&2, String>, Nat, z => IV.occn(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), SC.pow2(k)), AR.slots(String, K2), AR.slots(String, ksT), hsl2),      Equal.trans(Nat, IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), S.size(~V, m0), S.size(~V, S.set(~V, m0, key, x)), Equal.sym(Nat, S.size(~V, m0), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), SZ.size_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), N.le_refl(SC.pow2(k)))),        Equal.sym(Nat, S.size(~V, S.set(~V, m0, key, x)), S.size(~V, m0), sz_old(~V, m0, key, x, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i))))), LK.lookup_hit(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), huq, i, hi, hk), L.subst(Nat, z => {ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), z)) == True{} : Bool}, s, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), Equal.sym(Nat, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), s, hl0), Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), s)), B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), s), True{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), s), ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), s)), ST.lvs_nth(~V, AR.slots(Maybe<&2, V>, vsT), s)), hlv)))))))  (ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), nxT}, (Equal.cong(Array<Maybe<&2, V>>, H.HashMap<&2, V>, a => H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), a, AR.thaw(U32, nxT)}, Array.set(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), Some{x}), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), hset), ((g2, (q => hit_lk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, K2, hsl2, i, l, hi, hk, hl, hr, q), sz2)), hp => keep_hit(~V, AR.slots(U32, tabT), AR.slots(String, ksT), AR.slots(String, K2), hsl2, SC.pow2(k), AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x})), UD.v(fresh), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, K2), AR.perfect(String, sd, K2), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), Some{x}), nxT, g2)))))