1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/lru.bend as SP 8 import ../../lib/u32div.bend as UD 9 import ../../../src/containers/hash_table.bend as H 10 import ../../../src/containers/lru.bend as LR 11 import ../hash_table/table.bend as TB 12 import ../hash_table/buckets.bend as B 13 import ../hash_table/cyc.bend as CY 14 import ../hash_table/state.bend as HT 15 import ../hash_table/keys.bend as K 16 import ./state.bend as ST 17 import ./gone.bend as GO 18 import ./unlink.bend as UL 19 20 import ./read.bend as RD 21 import ./dellink.bend as DK 22 import ./tabsl.bend as TS 23 import ./linktail.bend as LT 24 import ./idx.bend as ID 25 26 # Removing the oldest entry: evict_oldest (an eviction) and drop_head (a 27 # removal, for keys). 28 29 import ./evict.bend as EV 30 import ./rmatk.bend as RK 31 import ./bumpk.bend as BK 32 import ../../lib/links.bend as LK 33 import ../../lib/words32.bend as W32 34 import ../../lib/u32_tree.bend as UT 35 36 37 # eviction, keeping k 38 39 def dv_evk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}, -r: LR.LRU<&2, V> & Maybe<&2, V>, pk: RK.POKk(~V, Maybe<&2, V>, (SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}), r, k)) -> BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, r), k): 40 match pk: 41 case Tuple{+sh2, Tuple{+x, Tuple{+er, Tuple{+es, Tuple{+g2, hk2}}}}}: 42 +hm2 = L.pair_fst(SP.Lru, Maybe<&2, V>, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Some{v}, ST.model(~V, sh2), x, es) 43 +ed = Equal.cong(List<&2, SP.Ent>, SP.Lru, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), EV.drop_first(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s0, t, v, hm)) 44 +em = Equal.trans(SP.Lru, ST.model(~V, sh2), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, Equal.sym(SP.Lru, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, ST.model(~V, sh2), hm2), ed) 45 (sh2, (Equal.cong(LR.LRU<&2, V> & Maybe<&2, V>, LR.LRU<&2, V>, z => LR.drop_v(&2, V, z), r, (ST.real(~V, sh2), x), er), (em, (g2, hk2)))) 46 47 def eb_evk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}, +hsv: {UD.v(H.slot(head)) == s0 : Nat}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +b: B.Bk, +hbe0: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == b : B.Bk}, +hb: {ST.isbf(b, ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0)) == True{} : Bool}, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +el: {H.link(H.slot(head)) == LK.lnk(s0) : U32}) -> BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1)), k): 48 match b: 49 case B.BE{}: 50 Empty.absurd(BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1)), k), L.false_true(hb)) 51 case B.BF{+w2, +l2, +k2}: 52 +ew = A.eq_of(w2, ST.lw(AR.slots(U32, lkT), s0, 2n), L.and_left(U32.is_eq(w2, ST.lw(AR.slots(U32, lkT), s0, 2n)), U32.is_eq(l2, LK.lnk(s0)), hb)) 53 +elk = A.eq_of(l2, LK.lnk(s0), L.and_right(U32.is_eq(w2, ST.lw(AR.slots(U32, lkT), s0, 2n)), U32.is_eq(l2, LK.lnk(s0)), hb)) 54 +hbe = Equal.trans(B.Bk, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e), B.BF{w2, l2, k2}, B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2}, hbe0, Equal.trans(B.Bk, B.BF{w2, l2, k2}, B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), l2, k2}, B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2}, Equal.cong(U32, B.Bk, z => B.BF{z, l2, k2}, w2, ST.lw(AR.slots(U32, lkT), s0, 2n), ew), Equal.cong(U32, B.Bk, z => B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), z, k2}, l2, LK.lnk(s0), elk))) 55 +hoi = L.subst(B.Bk, z => {B.occ(z) == True{} : Bool}, B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e), B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2}, hbe), {==}) 56 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 57 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t)) 58 +hsi = Equal.trans(Nat, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e)))), UD.v(H.slot(LK.lnk(s0))), s0, Equal.cong(B.Bk, Nat, z => UD.v(H.slot(B.lnk(z))), B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e), B.BF{ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2}, hbe), UL.ix_o(one, h1, s0, sd, hsd, hs0)) 59 +edl = Equal.trans(Array, LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0)), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(e)), Equal.cong(U32, Array, z => LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), z), H.link(H.slot(head)), LK.lnk(s0), el), DK.del_link_ok(one, h1, k, hk31, tabT, ST.g_cpt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), AR.slots(String, ksT), ST.g_cclus(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), e, he, ST.lw(AR.slots(U32, lkT), s0, 2n), LK.lnk(s0), k2, hbe)) 60 ok = dv_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, v, hm, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(e)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1), RK.rm_at_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t), one, h1, e, he, hoi, hsi, H.slot(head), hsv, v, hm, ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0), K.str_refl(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0)))) 61 L.subst(Array, z => BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), z, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1)), k), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(e)), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), Equal.sym(Array, LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(e)), edl), ok) 62 63 64 def ek_evk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}, +hsv: {UD.v(H.slot(head)) == s0 : Nat}, ea: TS.AnybAt(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), LK.lnk(s0), ST.lw(AR.slots(U32, lkT), s0, 2n))) -> BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1)), k): 65 match ea: 66 case Tuple{+e, Tuple{+he, hb}}: 67 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 68 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t)) 69 +el = LT.lnk_su(H.slot(head), s0, sd, hsd, hsv, hs0) 70 +hk31 = N.lt_trans(k, 30n, 31n, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)), {==}) 71 eb_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, v, hm, hsv, e, he, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e), {==}, hb, hk31, el) 72 73 74 def ev_m_evk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +m: Maybe<&2, V>, +hmm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == m : Maybe<&2, V>}, +hsm: {HT.some_b(~V, m) == True{} : Bool}, +hsv: {UD.v(H.slot(head)) == s0 : Nat}) -> BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1)), k): 75 match m: 76 case None{}: 77 Empty.absurd(BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1)), k), L.false_true(hsm)) 78 case Some{+v}: 79 +hm = {hmm : {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}} 80 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 81 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t)) 82 +hk31 = N.lt_trans(k, 30n, 31n, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)), {==}) 83 +ha = L.and_left(ST.anyb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), LK.lnk(s0), ST.lw(AR.slots(U32, lkT), s0, 2n)), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), t), ST.g_chas(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)) 84 ok = ek_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, v, hm, hsv, TS.find_anyb(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), LK.lnk(s0), ST.lw(AR.slots(U32, lkT), s0, 2n), ha)) 85 +hsu = GO.su_lt(H.slot(head), s0, sd, hsv, hs0) 86 +i2 = Equal.trans(Nat, UD.v(LR.hidx(H.slot(head))), ST.off(UD.v(H.slot(head)), 2n), ST.off(s0, 2n), ID.w2(one, h1, H.slot(head), sd, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 2n), UD.v(H.slot(head)), s0, hsv)) 87 +E2 = Equal.cong(Array & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.dl_h(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), H.slot(head), 1, CY.msk(k), AR.thaw(U32, mT), r), Array.get(U32, AR.thaw(U32, lkT), LR.hidx(H.slot(head))), (AR.thaw(U32, lkT), ST.lw(AR.slots(U32, lkT), s0, 2n)), GO.rd(one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), LR.hidx(H.slot(head)), s0, 2n, {==}, hs0, i2)) 88 +G6 = Equal.trans(Array & U32, Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 6n)), (AR.thaw(U32, mT), CY.msk(k)), UT.uget(5n, {==}, mT, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), 6, {==}), Equal.cong(U32, Array & U32, z => (AR.thaw(U32, mT), z), W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), A.eq_of(W32.nth0(AR.slots(U32, mT), 6n), CY.msk(k), ST.g_cmask(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)))) 89 +E1 = Equal.cong(Array & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.dl_m(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), H.slot(head), 1, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), G6) 90 +E = Equal.trans(LR.LRU<&2, V> & Maybe<&2, V>, LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1), LR.dl_h(&2, V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), H.slot(head), 1, CY.msk(k), AR.thaw(U32, mT), Array.get(U32, AR.thaw(U32, lkT), LR.hidx(H.slot(head)))), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1), E1, E2) 91 L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, z), k), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1), LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1), LR.drop_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), LR.del_link(AR.thaw(U32, tabT), CY.msk(k), ST.lw(AR.slots(U32, lkT), s0, 2n), H.link(H.slot(head))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, H.slot(head), 1), E), ok) 92 93 94 def old_evk(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> BK.CountOKk(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, LR.remove_slot(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), H.slot(head), 1)), k): 95 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 96 +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t)) 97 +eh = A.eq_of(head, LK.lnk(s0), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)) 98 +hsv = Equal.trans(Nat, UD.v(H.slot(head)), UD.v(H.slot(LK.lnk(s0))), s0, Equal.cong(U32, Nat, z => UD.v(H.slot(z)), head, LK.lnk(s0), eh), UL.ix_o(one, h1, s0, sd, hsd, hs0)) 99 +hls = L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), ST.slok(~V, t, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)) 100 ev_m_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0), {==}, L.and_right(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0), hls), hsv) 101 102