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/hash_table.bend as S 8 import ../../../spec/containers/lru.bend as SP 9 import ../../lib/u32div.bend as UD 10 import ../../../src/containers/hash_table.bend as H 11 import ../../../src/containers/lru.bend as LR 12 import ../hash_table/table.bend as TB 13 import ../hash_table/buckets.bend as B 14 import ../hash_table/cyc.bend as CY 15 import ../hash_table/state.bend as HT 16 import ../hash_table/keys.bend as K 17 import ./state.bend as ST 18 import ./bumpsh.bend as BS 19 import ./touch.bend as TO 20 import ./rmat.bend as RM 21 import ./gone.bend as GO 22 import ./unlink.bend as UL 23 24 import ./read.bend as RD 25 import ./dellink.bend as DK 26 import ./tabsl.bend as TS 27 import ./linktail.bend as LT 28 import ./idx.bend as ID 29 import ../../lib/links.bend as LK 30 import ../../lib/words32.bend as W32 31 import ../../lib/u32_tree.bend as UT 32 33 # Removing the oldest entry: evict_oldest (an eviction) and drop_head (a 34 # removal, for keys). 35 36 37 38 # the first entry has the first slot's key: dropping it is the tail 39 def drop_first(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s0: Nat, +t: List<&2, Nat>, +v: V, +hm: {HT.nthm(~V, el, s0) == Some{v} : Maybe<&2, V>}) -> {SP.drop(~V, ST.es(~V, ll, kl, el, Con{s0, t}), ST.skey(ll, kl, s0)) == SP.tail(~V, ST.es(~V, ll, kl, el, Con{s0, t})) : List<&2, SP.Ent>}: 40 +e = TO.es_cons(~V, ll, kl, el, s0, v, hm, t) 41 +d = L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent>, z, ST.es(~V, ll, kl, el, t), Con{TO.ev(~V, ll, kl, s0, v), SP.drop(~V, ST.es(~V, ll, kl, el, t), ST.skey(ll, kl, s0))}) == ST.es(~V, ll, kl, el, t) : List<&2, SP.Ent>}, True{}, S.str_eq(ST.skey(ll, kl, s0), ST.skey(ll, kl, s0)), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s0), ST.skey(ll, kl, s0)), True{}, K.str_refl(ST.skey(ll, kl, s0))), {==}) 42 L.subst(List<&2, SP.Ent>, z => {SP.drop(~V, z, ST.skey(ll, kl, s0)) == SP.tail(~V, z) : List<&2, SP.Ent>}, Con{TO.ev(~V, ll, kl, s0, v), ST.es(~V, ll, kl, el, t)}, ST.es(~V, ll, kl, el, Con{s0, t}), Equal.sym(List<&2, SP.Ent>, ST.es(~V, ll, kl, el, Con{s0, t}), Con{TO.ev(~V, ll, kl, s0, v), ST.es(~V, ll, kl, el, t)}, e), d) 43 44 45 def dv_ev(~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: RM.POK(~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)) -> BS.CountOK(~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)): 46 match pk: 47 case Tuple{+sh2, Tuple{+x, Tuple{+er, Tuple{+es, g2}}}}: 48 +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) 49 +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})), drop_first(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s0, t, v, hm)) 50 +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) 51 (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))) 52 53 54 55 def eb_ev(~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}) -> BS.CountOK(~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))): 56 match b: 57 case B.BE{}: 58 Empty.absurd(BS.CountOK(~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))), L.false_true(hb)) 59 case B.BF{+w2, +l2, +k2}: 60 +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)) 61 +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)) 62 +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))) 63 +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), {==}) 64 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 65 +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)) 66 +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)) 67 +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)) 68 ok = dv_ev(~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), RM.rm_at_ev(~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)))) 69 L.subst(Array, z => BS.CountOK(~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))), 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) 70 71 def ek_ev(~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))) -> BS.CountOK(~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))): 72 match ea: 73 case Tuple{+e, Tuple{+he, hb}}: 74 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 75 +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)) 76 +el = LT.lnk_su(H.slot(head), s0, sd, hsd, hsv, hs0) 77 +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)), {==}) 78 eb_ev(~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) 79 80 81 def ev_m_ev(~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}) -> BS.CountOK(~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))): 82 match m: 83 case None{}: 84 Empty.absurd(BS.CountOK(~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))), L.false_true(hsm)) 85 case Some{+v}: 86 +hm = {hmm : {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}} 87 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 88 +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)) 89 +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)), {==}) 90 +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)) 91 ok = ek_ev(~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)) 92 +hsu = GO.su_lt(H.slot(head), s0, sd, hsv, hs0) 93 +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)) 94 +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)) 95 +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)))) 96 +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) 97 +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) 98 L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => BS.CountOK(~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)), 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) 99 100 # THEOREM: the oldest entry removed (c_ev counted); the model's tail 101 def old_ev(~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}) -> BS.CountOK(~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))): 102 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 103 +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)) 104 +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)) 105 +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)) 106 +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)) 107 ev_m_ev(~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) 108 109 110 111 def dv_rm(~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: RM.POK(~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_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), r)) -> BS.CountOK(~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_rm(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, r)): 112 match pk: 113 case Tuple{+sh2, Tuple{+x, Tuple{+er, Tuple{+es, g2}}}}: 114 +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_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}, ST.model(~V, sh2), x, es) 115 +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_rm(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})), drop_first(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s0, t, v, hm)) 116 +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_rm(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_rm(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_rm(ST.ctr(AR.slots(U32, mT)))}, ST.model(~V, sh2), hm2), ed) 117 (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))) 118 119 120 def eb_rm(~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}) -> BS.CountOK(~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_rm(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), 2))): 121 match b: 122 case B.BE{}: 123 Empty.absurd(BS.CountOK(~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_rm(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), 2))), L.false_true(hb)) 124 case B.BF{+w2, +l2, +k2}: 125 +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)) 126 +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)) 127 +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))) 128 +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), {==}) 129 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 130 +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)) 131 +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)) 132 +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)) 133 ok = dv_rm(~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), 2), RM.rm_at_rm(~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)))) 134 L.subst(Array, z => BS.CountOK(~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_rm(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), 2))), 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) 135 136 137 def ek_rm(~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))) -> BS.CountOK(~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_rm(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), 2))): 138 match ea: 139 case Tuple{+e, Tuple{+he, hb}}: 140 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 141 +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)) 142 +el = LT.lnk_su(H.slot(head), s0, sd, hsd, hsv, hs0) 143 +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)), {==}) 144 eb_rm(~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) 145 146 def ev_m_rm(~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}) -> BS.CountOK(~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_rm(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), 2))): 147 match m: 148 case None{}: 149 Empty.absurd(BS.CountOK(~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_rm(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), 2))), L.false_true(hsm)) 150 case Some{+v}: 151 +hm = {hmm : {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}} 152 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 153 +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)) 154 +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)), {==}) 155 +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)) 156 ok = ek_rm(~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)) 157 +hsu = GO.su_lt(H.slot(head), s0, sd, hsv, hs0) 158 +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)) 159 +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), 2, 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)) 160 +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)))) 161 +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), 2, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), G6) 162 +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), 2), 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), 2, 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), 2), E1, E2) 163 L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => BS.CountOK(~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_rm(ST.ctr(AR.slots(U32, mT)))}, LR.drop_v(&2, V, z)), 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), 2), 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), 2), 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), 2), 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), 2), E), ok) 164 165 # THEOREM: the oldest entry removed (c_rm counted); the model's tail 166 def old_rm(~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}) -> BS.CountOK(~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_rm(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), 2))): 167 +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) 168 +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)) 169 +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)) 170 +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)) 171 +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)) 172 ev_m_rm(~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)