import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/u32.bend as U import ../../lib/u32alg.bend as A import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC import ../../../spec/containers/hash_table.bend as S import ../../lib/u32div.bend as UD import ../../../src/math/hash.bend as HS import ../../../src/containers/hash_table.bend as H import ./keys.bend as K import ./table.bend as TB import ./buckets.bend as B import ./modn.bend as M import ./cyc.bend as CY import ./arr.bend as AX import ./inv.bend as IV import ./state.bend as ST import ./probe_all.bend as PA import ./insm.bend as IM import ./insu.bend as IU import ./insf.bend as IF import ./insert.bend as IS import ./arena.bend as AN import ./insgrow.bend as IG import ./words.bend as WR import ../../lib/nat_list.bend as NL import ../../lib/words32.bend as W32 # Choosing the new entry's slot: the head of the free list, or the next # fresh slot when the arena has room. def sz_pow(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {UD.v(sz) == SC.pow2(sd) : Nat}: N.eq_from_is_eq(UD.v(sz), SC.pow2(sd), ST.g_csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) def below_sd(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +t: Nat, +ht: {Nat.is_lt(t, UD.v(fresh)) == True{} : Bool}) -> {Nat.is_lt(t, SC.pow2(sd)) == True{} : Bool}: N.lt_le_trans(t, UD.v(fresh), SC.pow2(sd), ht, N.le_trans(UD.v(fresh), UD.v(sz), SC.pow2(sd), ST.g_cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), N.eq_le(UD.v(sz), SC.pow2(sd), sz_pow(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)))) # ---- the free list's head ---- def fl_pop(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +fr: Nat, +n: Nat, +f: U32, +hle: {Nat.is_le(n, fr) == True{} : Bool}, +hfl: {ST.fl_ok(bs, nb, nxl, Nat.sub(fr, n), f, fr, Nil{}) == True{} : Bool}, +hf: {U32.is_eq(f, 0) == False{} : Bool}) -> {Nat.is_le(1n+n, fr) == True{} : Bool} & ({ST.fl_ok(bs, nb, nxl, Nat.sub(fr, 1n+n), W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Nil{}}) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(f)), fr) == True{} : Bool} & {ST.noslot(bs, UD.v(H.slot(f)), nb) == True{} : Bool})): +p = L.sfst(Nat, q => {Nat.sub(fr, n) == 1n+q : Nat}, IF.cnt_pos(bs, nb, nxl, Nat.sub(fr, n), f, fr, Nil{}, hf, hfl)) +hp = L.ssnd(Nat, q => {Nat.sub(fr, n) == 1n+q : Nat}, IF.cnt_pos(bs, nb, nxl, Nat.sub(fr, n), f, fr, Nil{}, hf, hfl)) +h2 = L.subst(Nat, c => {ST.fl_ok(bs, nb, nxl, c, f, fr, Nil{}) == True{} : Bool}, Nat.sub(fr, n), 1n+p, hp, hfl) +x1 = Bool.not(U32.is_eq(f, 0)) +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), Nil{})))) +tl = ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Nil{}}) +a2 = L.and_left(y, tl, L.and_right(x1, Bool.and(y, tl), h2)) +a5 = L.and_right(y, tl, L.and_right(x1, Bool.and(y, tl), h2)) +es = Pair.fst({Nat.sub(fr, 1n+n) == p : Nat}, {Nat.is_le(1n+n, fr) == True{} : Bool}, IF.sub_step(fr, n, p, hle, hp)) +el = Pair.snd({Nat.sub(fr, 1n+n) == p : Nat}, {Nat.is_le(1n+n, fr) == True{} : Bool}, IF.sub_step(fr, n, p, hle, hp)) +t2 = L.subst(Nat, c => {ST.fl_ok(bs, nb, nxl, c, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Nil{}}) == True{} : Bool}, p, Nat.sub(fr, 1n+n), Equal.sym(Nat, Nat.sub(fr, 1n+n), p, es), a5) +z = Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), Nil{}))) (el, (t2, (L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2), L.and_left(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), Nil{})), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))))) # THEOREM: taking the free list's head for the new entry refines set def set_free(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == False{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}) -> IS.SetM(~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, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, False{})): +cf = ST.g_cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg) +hle = L.and_left(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +hfl0 = L.and_right(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +hnf = Pair.fst({Nat.is_le(1n+UD.v(n), UD.v(fresh)) == True{} : Bool}, {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}), fl_pop(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), UD.v(fresh), UD.v(n), free, hle, hfl0, hf)) +hfl = Pair.fst({ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool}, {Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}, Pair.snd({Nat.is_le(1n+UD.v(n), UD.v(fresh)) == True{} : Bool}, {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}), fl_pop(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), UD.v(fresh), UD.v(n), free, hle, hfl0, hf))) +hs = Pair.fst({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool}, {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}, Pair.snd({ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool}, {Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}, Pair.snd({Nat.is_le(1n+UD.v(n), UD.v(fresh)) == True{} : Bool}, {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}), fl_pop(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), UD.v(fresh), UD.v(n), free, hle, hfl0, hf)))) +hns = Pair.snd({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool}, {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}, Pair.snd({ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool}, {Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}, Pair.snd({Nat.is_le(1n+UD.v(n), UD.v(fresh)) == True{} : Bool}, {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), 1n+UD.v(n)), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), UD.v(fresh), Con{UD.v(H.slot(free)), Nil{}}) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(free)), UD.v(fresh)) == True{} : Bool} & {ST.noslot(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(free)), SC.pow2(k)) == True{} : Bool}), fl_pop(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), UD.v(fresh), UD.v(n), free, hle, hfl0, hf)))) +hsp = below_sd(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, UD.v(H.slot(free)), hs) +gw = AX.getw(sd, nxT, H.slot(free), 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), hsp, ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) +eq = Equal.cong(Array & U32, H.HashMap<&2, V>, r => H.ins_free(&2, V, n, CY.msk(k), td, fresh, sz, sdU, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), H.slot(free), U32.from_nat(e), K.kword(key), PA.stored(key), x, r), Array.get(U32, AR.thaw(U32, nxT), H.slot(free)), (AR.thaw(U32, nxT), W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free)))), gw) res = IG.ins_any(~V, one, h1, n, k, td, fresh, sz, sd, sdU, W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), tabT, ksT, vsT, nxT, H.slot(free), e, key, x, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), L.and_right(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), 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), N.lt_le(sd, k, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), 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), 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), ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), 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), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cload(~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, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hnf, hfl, hs, hns, hno, ST.g_cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.subst(Bool, b => {Bool.or(b, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) == True{} : Bool}, True{}, Nat.is_lt(sd, k), Equal.sym(Bool, Nat.is_lt(sd, k), True{}, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), {==}), he, hz, hp, cap, hc30, hcap) L.subst(H.HashMap<&2, V>, r => IS.SetM(~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, r), H.ins_slot(&2, V, n, CY.msk(k), td, fresh, sz, sdU, W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), H.slot(free), U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, False{}), Equal.sym(H.HashMap<&2, V>, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, False{}), H.ins_slot(&2, V, n, CY.msk(k), td, fresh, sz, sdU, W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(free))), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), H.slot(free), U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), eq), res) # ---- a fresh slot ---- def live_all(+bs: List<&2, B.Bk>, +lv: List<&2, Bool>, +f: Nat, +f2: Nat, +hle: {Nat.is_le(f, f2) == True{} : Bool}, +n: Nat, +h: {B.all_lt(B.PLive{bs, lv, f}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PLive{bs, lv, f2}, m) == True{} : Bool}: match m: case 0n: {==} case 1n+q: +hq = N.succ_le_lt(q, n, hm) L.and_intro(B.live_b(lv, f2, B.at(bs, q)), B.all_lt(B.PLive{bs, lv, f2}, q), IM.live_mono(lv, f, f2, hle, B.at(bs, q), B.all_inst(B.PLive{bs, lv, f}, n, h, q, hq)), live_all(bs, lv, f, f2, hle, n, h, q, N.lt_le(q, n, hq))) # with the free list empty, every slot below fresh is in use: fresh = n def fresh_n(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}) -> {UD.v(fresh) == UD.v(n) : Nat}: +cf = ST.g_cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg) +hle = L.and_left(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +hfl0 = L.subst(U32, f => {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), f, UD.v(fresh), Nil{}) == True{} : Bool}, free, 0, A.eq_of(free, 0, hf), L.and_right(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf)) IF.sub_zero_eq(UD.v(fresh), UD.v(n), hle, IF.cnt_zero(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), UD.v(fresh), Nil{}, hfl0)) def inc_fresh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hsp: {Nat.is_lt(UD.v(fresh), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(U32.inc(fresh)) == 1n+UD.v(fresh) : Nat}: W32.inc_val(one, h1, fresh, W32.bound32(one, h1, UD.v(fresh), sd, N.lt_trans(sd, k, 31n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))), hsp)) # THEOREM: taking the next fresh slot, when the arena has room, refines set def set_room(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}) -> IS.SetM(~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, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{})): +efn = fresh_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf) +hlt = Equal.trans(Bool, Nat.is_lt(UD.v(fresh), UD.v(sz)), U32.is_lt(fresh, sz), True{}, Equal.sym(Bool, U32.is_lt(fresh, sz), Nat.is_lt(UD.v(fresh), UD.v(sz)), U.is_lt_nat(fresh, sz)), hr) +hsp = N.lt_le_trans(UD.v(fresh), UD.v(sz), SC.pow2(sd), hlt, N.eq_le(UD.v(sz), SC.pow2(sd), sz_pow(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno))) +ei = inc_fresh(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hsp) +hfr = L.subst(Nat, z => {Nat.is_le(z, UD.v(sz)) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), N.lt_succ_le_succ(UD.v(fresh), UD.v(sz), hlt)) +e1n = Equal.trans(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), 1n+UD.v(n), ei, Equal.cong(Nat, Nat, z => 1n+z, UD.v(fresh), UD.v(n), efn)) +hnf = L.subst(Nat, z => {Nat.is_le(1n+UD.v(n), z) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(n), e1n), N.le_refl(1n+UD.v(n))) +hcnt = Equal.sym(Nat, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), 0n, Equal.trans(Nat, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), Nat.sub(1n+UD.v(n), 1n+UD.v(n)), 0n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+UD.v(n)), UD.v(U32.inc(fresh)), 1n+UD.v(n), e1n), N.sub_self(UD.v(n)))) +hfl = L.subst(Nat, c => {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), c, 0, UD.v(U32.inc(fresh)), Con{UD.v(fresh), Nil{}}) == True{} : Bool}, 0n, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), hcnt, {==}) +hs = L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), N.lt_succ(UD.v(fresh))) +hns = IF.noslot_live(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, 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))) +hl = live_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh), UD.v(U32.inc(fresh)), N.lt_le(UD.v(fresh), UD.v(U32.inc(fresh)), hs), 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))) +eq = Equal.cong(Bool, H.HashMap<&2, V>, b => H.ins_fresh(&2, V, n, CY.msk(k), td, fresh, sz, sdU, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, b), U32.is_lt(fresh, sz), True{}, hr) res = IG.ins_any(~V, one, h1, n, k, td, U32.inc(fresh), sz, sd, sdU, 0, tabT, ksT, vsT, nxT, fresh, e, key, x, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), L.and_right(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), 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), N.lt_le(sd, k, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), 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), 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), ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), 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), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hl, hfr, hnf, hfl, hs, hns, hno, ST.g_cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.subst(Bool, b => {Bool.or(b, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) == True{} : Bool}, True{}, Nat.is_lt(sd, k), Equal.sym(Bool, Nat.is_lt(sd, k), True{}, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), {==}), he, hz, hp, cap, hc30, hcap) L.subst(H.HashMap<&2, V>, r => IS.SetM(~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, r), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), sz, sdU, 0, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{}), Equal.sym(H.HashMap<&2, V>, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{}), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), sz, sdU, 0, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), eq), res) # ---- growing the arena ---- def esdu(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {UD.v(sdU) == sd : Nat}: N.eq_from_is_eq(UD.v(sdU), sd, ST.g_csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) def ebs(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)) == TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}: AN.bs_app(AR.slots(U32, tabT), AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, "")), sd, AR.slots_length(String, sd, ksT, 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)), SC.pow2(k), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) # the grown arrays are the shadow's trees with blank second halves def raw_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(sdU), "")}, ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) == H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) : H.HashMap<&2, V>}: +ek = Equal.cong(Array, Array, a => ANode{AR.thaw(String, ksT), a}, Array.new(String, UD.v(sdU), ""), AR.thaw(String, AR.trep(String, sd, "")), Equal.trans(Array, Array.new(String, UD.v(sdU), ""), Array.new(String, sd, ""), AR.thaw(String, AR.trep(String, sd, "")), Equal.cong(Nat, Array, d => Array.new(String, d, ""), UD.v(sdU), sd, esdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), AR.new(String, sd, ""))) +ev = Equal.cong(Array>, Array>, a => ANode{AR.thaw(Maybe<&2, V>, vsT), a}, H.vac(&2, V, UD.v(sdU)), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), Equal.trans(Array>, H.vac(&2, V, UD.v(sdU)), H.vac(&2, V, sd), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), Equal.cong(Nat, Array>, d => H.vac(&2, V, d), UD.v(sdU), sd, esdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), AN.vac_eq(~V, sd))) +en = Equal.cong(Array, Array, a => ANode{AR.thaw(U32, nxT), a}, Array.new(U32, UD.v(sdU), 0), AR.thaw(U32, AR.trep(U32, sd, 0)), Equal.trans(Array, Array.new(U32, UD.v(sdU), 0), Array.new(U32, sd, 0), AR.thaw(U32, AR.trep(U32, sd, 0)), Equal.cong(Nat, Array, d => Array.new(U32, d, 0), UD.v(sdU), sd, esdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), AR.new(U32, sd, 0))) Equal.trans(H.HashMap<&2, V>, H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(sdU), "")}, ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), Equal.cong(Array, H.HashMap<&2, V>, a => H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), a, ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(sdU), "")}, AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), ek), Equal.trans(H.HashMap<&2, V>, H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), Equal.cong(Array>, H.HashMap<&2, V>, a => H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), a, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), ev), Equal.cong(Array, H.HashMap<&2, V>, a => H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), a, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), en))) # a full arena with an empty free list: n = fresh = sz = 2^sd def full_n(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == False{} : Bool}) -> {UD.v(n) == SC.pow2(sd) : Nat}: +hlt = Equal.trans(Bool, Nat.is_lt(UD.v(fresh), UD.v(sz)), U32.is_lt(fresh, sz), False{}, Equal.sym(Bool, U32.is_lt(fresh, sz), Nat.is_lt(UD.v(fresh), UD.v(sz)), U.is_lt_nat(fresh, sz)), hr) +efs = N.le_antisym(UD.v(fresh), UD.v(sz), ST.g_cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), N.not_lt_le(UD.v(fresh), UD.v(sz), hlt)) Equal.trans(Nat, UD.v(n), UD.v(fresh), SC.pow2(sd), Equal.sym(Nat, UD.v(fresh), UD.v(n), fresh_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf)), Equal.trans(Nat, UD.v(fresh), UD.v(sz), SC.pow2(sd), efs, sz_pow(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno))) # without table growth the grown arena is still smaller than the table def sd_k2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == False{} : Bool}, +hovi: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == False{} : Bool}) -> {Nat.is_lt(1n+sd, k) == True{} : Bool}: +hov = Equal.trans(Bool, Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), False{}, Equal.sym(Bool, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), IU.over_val(one, h1, k, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), L.and_right(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), n, ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))), hovi) +le = IU.gt_false_le(Nat.double(1n+UD.v(n)), SC.pow2(k), hov) +lt = L.subst(Nat, z => {Nat.is_lt(Nat.double(z), Nat.double(1n+UD.v(n))) == True{} : Bool}, UD.v(n), SC.pow2(sd), full_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr), N.double_lt(UD.v(n), 1n+UD.v(n), N.lt_succ(UD.v(n)))) IG.pow2_lt_inv(1n+sd, k, N.lt_le_trans(SC.pow2(1n+sd), Nat.double(1n+UD.v(n)), SC.pow2(k), lt, le)) def shl_sz(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {UD.v(U32.shl(sz)) == SC.pow2(1n+sd) : Nat}: +h = L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(2n+sd)) == True{} : Bool}, SC.pow2(sd), UD.v(sz), Equal.sym(Nat, UD.v(sz), SC.pow2(sd), sz_pow(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), N.pow2_lt_succ(1n+sd)) Equal.trans(Nat, UD.v(U32.shl(sz)), Nat.double(UD.v(sz)), SC.pow2(1n+sd), U.shl_value(sz, 2n+sd, N.lt_le(2n+sd, 32n, N.lt_le_trans(sd, k, 30n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), N.lt_succ_le(k, 30n, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))))), h), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(sz), SC.pow2(sd), sz_pow(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno))) def inc_sdu(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> {UD.v(U32.inc(sdU)) == 1n+sd : Nat}: +h = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(5n)) == True{} : Bool}, sd, UD.v(sdU), Equal.sym(Nat, UD.v(sdU), sd, esdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), 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)) Equal.trans(Nat, UD.v(U32.inc(sdU)), 1n+UD.v(sdU), 1n+sd, W32.inc_val(one, h1, sdU, W32.bound32(one, h1, UD.v(sdU), 5n, {==}, h)), Equal.cong(Nat, Nat, z => 1n+z, UD.v(sdU), sd, esdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno))) def ple_c(+a: Nat, +b: Nat, +h: {Nat.is_le(SC.pow2(a), SC.pow2(b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(a, b) == c : Bool}) -> {c == True{} : Bool}: match c: case True{}: {==} case False{}: Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(SC.pow2(a), SC.pow2(b)), False{}, Equal.sym(Bool, Nat.is_le(SC.pow2(a), SC.pow2(b)), True{}, h), N.lt_not_le(SC.pow2(b), SC.pow2(a), N.pow2_strict(b, a, N.not_le_lt(a, b, hc)))))) def pow2_le_inv(+a: Nat, +b: Nat, +h: {Nat.is_le(SC.pow2(a), SC.pow2(b)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}: ple_c(a, b, h, Nat.is_le(a, b), {==}) # a full arena of 2^sd live entries fits in half the table: sd + 1 <= k def sdk1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == False{} : Bool}) -> {Nat.is_le(1n+sd, k) == True{} : Bool}: pow2_le_inv(1n+sd, k, L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, UD.v(n), SC.pow2(sd), full_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr), ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))) def sdk2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == False{} : Bool}, +c: Bool, +hc: {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == c : Bool}) -> {Bool.or(Nat.is_lt(1n+sd, k), U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) == True{} : Bool}: match c: case False{}: L.subst(Bool, b => {Bool.or(b, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))) == True{} : Bool}, True{}, Nat.is_lt(1n+sd, k), Equal.sym(Bool, Nat.is_lt(1n+sd, k), True{}, sd_k2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr, hc)), {==}) case True{}: L.subst(Bool, b => {Bool.or(Nat.is_lt(1n+sd, k), b) == True{} : Bool}, True{}, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), Equal.sym(Bool, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), True{}, hc), WR.or_true(Nat.is_lt(1n+sd, k))) # THEOREM: growing the arena for the new entry refines set def set_arena(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree, +ksT: AR.Tree, +vsT: AR.Tree>, +nxT: AR.Tree, +hg: {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT) == True{} : Bool}, +key: String, +x: V, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hf: {U32.is_eq(free, 0) == True{} : Bool}, +hr: {U32.is_lt(fresh, sz) == False{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(cap)) == True{} : Bool}) -> IS.SetM(~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, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{})): +efn = fresh_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf) +en = full_n(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr) +efp = Equal.trans(Nat, UD.v(fresh), UD.v(n), SC.pow2(sd), efn, en) +hsp = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+sd)) == True{} : Bool}, SC.pow2(sd), UD.v(fresh), Equal.sym(Nat, UD.v(fresh), SC.pow2(sd), efp), N.pow2_lt_succ(sd)) +ei = W32.inc_val(one, h1, fresh, W32.bound32(one, h1, UD.v(fresh), 1n+sd, N.lt_le_trans(sd, k, 30n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), N.lt_succ_le(k, 30n, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)))), hsp)) +e1n = Equal.trans(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), 1n+UD.v(n), ei, Equal.cong(Nat, Nat, z => 1n+z, UD.v(fresh), UD.v(n), efn)) +hnf = L.subst(Nat, z => {Nat.is_le(1n+UD.v(n), z) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(n), e1n), N.le_refl(1n+UD.v(n))) +hcnt = Equal.sym(Nat, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), 0n, Equal.trans(Nat, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), Nat.sub(1n+UD.v(n), 1n+UD.v(n)), 0n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+UD.v(n)), UD.v(U32.inc(fresh)), 1n+UD.v(n), e1n), N.sub_self(UD.v(n)))) +hfl = L.subst(Nat, c => {ST.fl_ok(TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), c, 0, UD.v(U32.inc(fresh)), Con{UD.v(fresh), Nil{}}) == True{} : Bool}, 0n, Nat.sub(UD.v(U32.inc(fresh)), 1n+UD.v(n)), hcnt, {==}) +hs = L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), N.lt_succ(UD.v(fresh))) +hfr = L.subst(Nat, z => {Nat.is_le(UD.v(U32.inc(fresh)), z) == True{} : Bool}, SC.pow2(1n+sd), UD.v(U32.shl(sz)), Equal.sym(Nat, UD.v(U32.shl(sz)), SC.pow2(1n+sd), shl_sz(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), L.subst(Nat, z => {Nat.is_le(z, SC.pow2(1n+sd)) == True{} : Bool}, 1n+SC.pow2(sd), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+SC.pow2(sd), Equal.trans(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), 1n+SC.pow2(sd), ei, Equal.cong(Nat, Nat, z => 1n+z, UD.v(fresh), SC.pow2(sd), efp))), N.double_succ_le(SC.pow2(sd), N.pow2_pos(sd)))) +hlv = AR.slots_length(Maybe<&2, V>, sd, vsT, 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)) +hfv = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), 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), hlv), N.eq_le(UD.v(fresh), SC.pow2(sd), efp)) +hl0 = AN.live_app(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), UD.v(fresh), hfv, 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))) +hl1 = live_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})))), UD.v(fresh), UD.v(U32.inc(fresh)), N.lt_le(UD.v(fresh), UD.v(U32.inc(fresh)), hs), SC.pow2(k), hl0, SC.pow2(k), N.le_refl(SC.pow2(k))) +hl = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PLive{z, ST.lvs(~V, SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})))), UD.v(U32.inc(fresh))}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), hl1) +hns = L.subst(List<&2, B.Bk>, z => {ST.noslot(z, UD.v(fresh), SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), IF.noslot_live(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, 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)))) +hw = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PWell{z, 1n+sd}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), AN.well_mono(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, 1n+sd, N.lt_le(SC.pow2(sd), SC.pow2(1n+sd), N.pow2_lt_succ(sd)), SC.pow2(k), ST.g_cwell(~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)))) +pk = L.and_intro(AR.perfect(String, sd, ksT), AR.perfect(String, sd, AR.trep(String, sd, "")), 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), AR.trep_perfect(String, sd, "")) +pv = L.and_intro(AR.perfect(Maybe<&2, V>, sd, vsT), AR.perfect(Maybe<&2, V>, sd, AR.trep(Maybe<&2, V>, sd, None{})), 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), AR.trep_perfect(Maybe<&2, V>, sd, None{})) +pn = L.and_intro(AR.perfect(U32, sd, nxT), AR.perfect(U32, sd, AR.trep(U32, sd, 0)), ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), AR.trep_perfect(U32, sd, 0)) +hsz = IS.eq_is_eq(UD.v(U32.shl(sz)), SC.pow2(1n+sd), shl_sz(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)) +hsdu = IS.eq_is_eq(UD.v(U32.inc(sdU)), 1n+sd, inc_sdu(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)) +eqf = Equal.cong(Bool, H.HashMap<&2, V>, b => H.ins_fresh(&2, V, n, CY.msk(k), td, fresh, sz, sdU, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, b), U32.is_lt(fresh, sz), False{}, hr) +eq = Equal.trans(H.HashMap<&2, V>, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{}), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), ANode{AR.thaw(String, ksT), Array.new(String, UD.v(sdU), "")}, ANode{AR.thaw(Maybe<&2, V>, vsT), H.vac(&2, V, UD.v(sdU))}, ANode{AR.thaw(U32, nxT), Array.new(U32, UD.v(sdU), 0)}, fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), eqf, raw_eq(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)) res = IG.ins_any(~V, one, h1, n, k, td, U32.inc(fresh), U32.shl(sz), 1n+sd, U32.inc(sdU), 0, tabT, AR.TNode{ksT, AR.trep(String, sd, "")}, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}, AR.TNode{nxT, AR.trep(U32, sd, 0)}, fresh, e, key, x, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), L.and_right(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), N.lt_trans(sd, k, 31n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))), sdk1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr), ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), pk, pv, pn, ST.g_ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hsz, hsdu, hw, L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), 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)), L.subst(List<&2, B.Bk>, z => {Nat.is_eq(UD.v(n), IV.occn(z, SC.pow2(k))) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hl, hfr, hnf, hfl, hs, hns, L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PNo{z, key}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), hno), L.subst(List<&2, B.Bk>, z => {B.cluster(z, SC.pow2(k), CY.msk(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), ST.g_cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), sdk2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno, hf, hr, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), {==}), he, L.subst(List<&2, B.Bk>, z => {B.at(z, e) == B.BE{} : B.Bk} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), hz), L.subst(List<&2, B.Bk>, z => {B.occpath(z, SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool} , TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), hp), cap, hc30, hcap) +em = Equal.trans(List<&2, S.Entry>, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), SC.pow2(k), 0n), ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), SC.pow2(k), 0n), 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), Equal.cong(List<&2, B.Bk>, List<&2, S.Entry>, z => ST.absm(~V, z, SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), SC.pow2(k), 0n), TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ebs(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, x, e, he, hz, hp, hno)), AN.absm_app(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{})), sd, hlv, SC.pow2(k), ST.g_cwell(~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), 0n, N.le_refl(SC.pow2(k)))) r1 = L.subst(H.HashMap<&2, V>, r => IS.SetM(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), SC.pow2(k), 0n), key, x, r), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{}), Equal.sym(H.HashMap<&2, V>, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{}), H.ins_slot(&2, V, n, CY.msk(k), td, U32.inc(fresh), U32.shl(sz), U32.inc(sdU), 0, AR.thaw(U32, tabT), AR.thaw(String, AR.TNode{ksT, AR.trep(String, sd, "")}), AR.thaw(Maybe<&2, V>, AR.TNode{vsT, AR.trep(Maybe<&2, V>, sd, None{})}), AR.thaw(U32, AR.TNode{nxT, AR.trep(U32, sd, 0)}), fresh, U32.from_nat(e), K.kword(key), PA.stored(key), x, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k)))), eq), res) L.subst(List<&2, S.Entry>, m => IS.SetM(~V, m, key, x, H.ins_new(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), K.kword(key), PA.stored(key), x, True{})), ST.absm(~V, TB.buckets(AR.slots(U32, tabT), SC.append(String, AR.slots(String, ksT), AR.slots(String, AR.trep(String, sd, ""))), SC.pow2(k)), SC.append(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), AR.slots(Maybe<&2, V>, AR.trep(Maybe<&2, V>, sd, None{}))), SC.pow2(k), 0n), 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), em, r1)