proofs/containers/lru/evict.bend

bend-collections-laws-containers@1.0.0.0 · 172 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
8import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpsh.bend as BS
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touch.bend as TO
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmat.bend as RM
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as GO
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
23
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as RD
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dellink.bend as DK
26import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/tabsl.bend as TS
27import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/linktail.bend as LT
28import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
29import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
30import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
31import bend-collections-laws-containers@1.0.0.0/proofs/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
39def 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<V>>}:
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<V>>, 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<V>>}, 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<V>>, z => {SP.drop(~V, z, ST.skey(ll, kl, s0)) == SP.tail(~V, z) : List<&2, SP.Ent<V>>}, 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<V>>, 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
45def dv_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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<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}, ST.model(~V, sh2), x, es)
49      +ed = Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, 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<V>, 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<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)))}, 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
55def eb_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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<U32>, 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<U32>, 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<U32>, 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<U32>, 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
71def ek_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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
81def ev_m_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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> & 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> & 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> & 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> & 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
101def old_ev(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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
111def dv_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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<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}, ST.model(~V, sh2), x, es)
115      +ed = Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, 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<V>, 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<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)))}, 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
120def eb_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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<U32>, 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<U32>, 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<U32>, 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<U32>, 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
137def ek_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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
146def ev_m_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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> & 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> & 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> & 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> & 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
166def old_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +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)