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/u32alg.bend as A 6 import ../../lib/array.bend as AR 7 import ../../../spec/lib/common.bend as SC 8 import ../../../spec/containers/hash_table.bend as S 9 import ../../lib/u32div.bend as UD 10 import ../../../src/math/hash.bend as HS 11 import ../../../src/containers/hash_table.bend as H 12 import ./keys.bend as K 13 import ./table.bend as TB 14 import ./buckets.bend as B 15 import ./modn.bend as M 16 import ./cyc.bend as CY 17 import ./arr.bend as AX 18 import ./inv.bend as IV 19 import ./state.bend as ST 20 import ./probe_all.bend as PA 21 import ./insm.bend as IM 22 import ./insu.bend as IU 23 import ./insf.bend as IF 24 import ./insert.bend as IS 25 import ./arena.bend as AN 26 import ./insgrow.bend as IG 27 import ./words.bend as WR 28 import ../../lib/nat_list.bend as NL 29 import ../../lib/words32.bend as W32 30 31 # Choosing the new entry's slot: the head of the free list, or the next 32 # fresh slot when the arena has room. 33 34 35 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}: 36 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)) 37 38 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}: 39 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)))) 40 41 # ---- the free list's head ---- 42 43 44 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})): 45 +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)) 46 +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)) 47 +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) 48 +x1 = Bool.not(U32.is_eq(f, 0)) 49 +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{})))) 50 +tl = ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Nil{}}) 51 +a2 = L.and_left(y, tl, L.and_right(x1, Bool.and(y, tl), h2)) 52 +a5 = L.and_right(y, tl, L.and_right(x1, Bool.and(y, tl), h2)) 53 +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)) 54 +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)) 55 +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) 56 +z = Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), Nil{}))) 57 (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))))) 58 59 60 # THEOREM: taking the free list's head for the new entry refines set 61 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{})): 62 +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) 63 +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) 64 +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) 65 +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)) 66 +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))) 67 +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)))) 68 +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)))) 69 +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) 70 +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)) 71 +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) 72 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 73 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) 74 75 # ---- a fresh slot ---- 76 77 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}: 78 match m: 79 case 0n: 80 {==} 81 case 1n+q: 82 +hq = N.succ_le_lt(q, n, hm) 83 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))) 84 85 86 # with the free list empty, every slot below fresh is in use: fresh = n 87 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}: 88 +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) 89 +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) 90 +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)) 91 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)) 92 93 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}: 94 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)) 95 96 # THEOREM: taking the next fresh slot, when the arena has room, refines set 97 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{})): 98 +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) 99 +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) 100 +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))) 101 +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) 102 +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)) 103 +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)) 104 +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))) 105 +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)))) 106 +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, {==}) 107 +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))) 108 +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))) 109 +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))) 110 +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) 111 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.s 112 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) 113 114 # ---- growing the arena ---- 115 116 117 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}: 118 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)) 119 120 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>}: 121 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)) 122 123 # the grown arrays are the shadow's trees with blank second halves 124 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>}: 125 +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, ""))) 126 +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))) 127 +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))) 128 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), 129 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), 130 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))) 131 132 # a full arena with an empty free list: n = fresh = sz = 2^sd 133 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}: 134 +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) 135 +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)) 136 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))) 137 138 # without table growth the grown arena is still smaller than the table 139 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}: 140 +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) 141 +le = IU.gt_false_le(Nat.double(1n+UD.v(n)), SC.pow2(k), hov) 142 +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)))) 143 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)) 144 145 146 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}: 147 +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)) 148 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))) 149 150 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}: 151 +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)) 152 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))) 153 154 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}: 155 match c: 156 case True{}: 157 {==} 158 case False{}: 159 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)))))) 160 161 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}: 162 ple_c(a, b, h, Nat.is_le(a, b), {==}) 163 164 # a full arena of 2^sd live entries fits in half the table: sd + 1 <= k 165 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}: 166 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))) 167 168 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}: 169 match c: 170 case False{}: 171 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)), {==}) 172 case True{}: 173 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))) 174 175 # THEOREM: growing the arena for the new entry refines set 176 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{})): 177 +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) 178 +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) 179 +efp = Equal.trans(Nat, UD.v(fresh), UD.v(n), SC.pow2(sd), efn, en) 180 +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)) 181 +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)) 182 +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)) 183 +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))) 184 +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)))) 185 +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, {==}) 186 +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))) 187 +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)))) 188 +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)) 189 +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)) 190 +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))) 191 +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))) 192 +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) 193 +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)))) 194 +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)))) 195 +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, "")) 196 +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{})) 197 +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)) 198 +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)) 199 +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)) 200 +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) 201 +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)) 202 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 203 +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)))) 204 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) 205 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)