import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/u32alg.bend as A import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC import ../../../spec/containers/hash_table.bend as S import ../../../spec/containers/lru.bend as SP import ../../lib/u32div.bend as UD import ../../../src/math/u64.bend as W import ../../../src/containers/hash_table.bend as H import ../../../src/containers/lru.bend as LR import ../hash_table/table.bend as TB import ../hash_table/buckets.bend as B import ../hash_table/cyc.bend as CY import ../hash_table/inv.bend as IV import ../hash_table/keys.bend as K import ./state.bend as ST import ./basic.bend as BA import ./bumpsh.bend as BS import ./tfind.bend as TF import ./unlink.bend as UL import ./lists.bend as LS import ../../../src/math/hash.bend as HS import ../hash_table/probe_all.bend as PA import ./read.bend as RD import ./insp.bend as IP import ./grow.bend as GW import ./evictk.bend as EK import ./bumpk.bend as BK import ./walk.bend as WL import ./linktail.bend as LT import ../hash_table/rawins.bend as RI import ../hash_table/grow.bend as GR import ./ins1.bend as I1 import ../../lib/u32.bend as U import ../hash_table/modn.bend as M import ../../lib/nat_list.bend as NL import ../../lib/links.bend as LK import ../../lib/words32.bend as W32 import ../../lib/u32_tree.bend as UT # add, a new key missing from the table: not full, the probe's empty bucket # takes it; full, the oldest entry is evicted first and the key re-probed. # the entries the specification's add leaves, a new entry appended and counted def ins_spec(~V: Data, l: SP.Lru, +key: String, v: V, +t: U32, +lo: U32, +hi: U32) -> SP.Lru: match l: case SP.L{+cap, +on, +life, +es, +c}: SP.L{cap, on, life, SP.snoc(~V, es, SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(c)} # the free list's head link is the link of its slot def fl_link(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +hfz: {U32.is_eq(free, 0) == False{} : Bool}) -> {H.link(H.slot(free)) == free : U32}: match fl: case Nil{}: Empty.absurd({H.link(H.slot(free)) == free : U32}, L.true_false(Equal.trans(Bool, True{}, U32.is_eq(free, 0), False{}, Equal.sym(Bool, U32.is_eq(free, 0), True{}, ST.g_cfree(~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, sl, Nil{}, hg)), hfz))) case Con{+s0, +tl}: +gc = ST.g_cfl(~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, sl, Con{s0, tl}, hg) +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, Con{s0, tl}, hg) +hf0 = L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0))), ST.flok(~V, tl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), gc) +hs0 = N.lt_le_trans(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), L.and_left(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), hf0), ST.g_cfresh(~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, sl, Con{s0, tl}, hg)) +ef = A.eq_of(free, LK.lnk(s0), ST.g_cfree(~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, sl, Con{s0, tl}, hg)) +el = LT.lnk_su(H.slot(LK.lnk(s0)), s0, sd, hsd, UL.ix_o(one, h1, s0, sd, hsd, hs0), hs0) L.subst(U32, z => {H.link(H.slot(z)) == z : U32}, LK.lnk(s0), free, Equal.sym(U32, free, LK.lnk(s0), ef), el) def fr_c(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +free2: U32, +hf2: {U32.is_eq(free2, 0) == True{} : Bool}, +hfz: {U32.is_eq(free, 0) == True{} : Bool}, +c: Bool, +hc: {U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)) == c : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.fresh_room(&2, V, cap, n, head, tail, free2, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), c)): match c: case True{}: IP.ip_fresh(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, free2, hf2, hfz, hc) case False{}: GW.ip_grow(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, free2, hf2, hfz, hc) def mr_b(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +b: Bool, +hb: {U32.is_eq(free, 0) == b : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, b)): match b: case True{}: +pm = 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, sl, fl, hg) +x1 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.mr_fresh(&2, V, cap, n, head, tail, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, r), Array.get(U32, AR.thaw(U32, mT), 0), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 0n)), UT.uget(5n, {==}, mT, pm, 0, {==})) +x2 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.mr_size(&2, V, cap, n, head, tail, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), r), Array.get(U32, AR.thaw(U32, mT), 1), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 1n)), UT.uget(5n, {==}, mT, pm, 1, {==})) +x3 = Equal.cong(Array, LR.LRU<&2, V>, tb => LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), tb, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(W32.nth0(AR.slots(U32, mT), 0n))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), GR.put_eq(k, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), e, he, K.kword(key), H.link(W32.nth0(AR.slots(U32, mT), 0n)))) +X = Equal.trans(LR.LRU<&2, V>, LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, True{}), LR.mr_size(&2, V, cap, n, head, tail, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), Array.get(U32, AR.thaw(U32, mT), 1)), LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), x1, Equal.trans(LR.LRU<&2, V>, LR.mr_size(&2, V, cap, n, head, tail, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), Array.get(U32, AR.thaw(U32, mT), 1)), LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(W32.nth0(AR.slots(U32, mT), 0n))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), x2, x3)) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, True{}), Equal.sym(LR.LRU<&2, V>, LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, True{}), LR.fresh_room(&2, V, cap, n, head, tail, 0, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), X), fr_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, 0, {==}, hb, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), {==})) case False{}: +fk = fl_link(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, hb) +y1 = Equal.cong(U32, LR.LRU<&2, V>, z => LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), z), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), free, H.link(H.slot(free)), Equal.sym(U32, H.link(H.slot(free)), free, fk)) +y2 = Equal.cong(Array, LR.LRU<&2, V>, tb => LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), tb, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(H.slot(free))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), GR.put_eq(k, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), e, he, K.kword(key), H.link(H.slot(free)))) +Y = Equal.trans(LR.LRU<&2, V>, LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, False{}), LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(H.slot(free))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), y1, y2) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, False{}), Equal.sym(LR.LRU<&2, V>, LR.mr_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi}, False{}), LR.free_next(&2, V, cap, n, head, tail, H.slot(free), AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(H.slot(free)))), Y), IP.ip_free(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, hb)) # THEOREM (add, a missing key, room: the probe's empty bucket takes it) def mr_ok(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.miss_room(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), U32.from_nat(e), K.kword(key), LR.E{v, t, lo, hi})): mr_b(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, U32.is_eq(free, 0), {==}) # ---- a full cache ---- def is_le_nat(+a: U32, +b: U32) -> {U32.is_le(a, b) == Nat.is_le(UD.v(a), UD.v(b)) : Bool}: Equal.cong(Cmp, Bool, c => Cmp.is_le(c), U32.cmp(a, b), Nat.cmp(UD.v(a), UD.v(b)), U.u32_cmp(a, b)) def is_eq_nat(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(UD.v(a), UD.v(b)) : Bool}: Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b), Nat.cmp(UD.v(a), UD.v(b)), U.u32_cmp(a, b)) def nm_nokey(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +xs: List<&2, Nat>, +key: String, +h: {S.mem(key, WL.mapk(ll, kl, xs)) == False{} : Bool}) -> {ST.nokey(~V, ll, kl, xs, key) == True{} : Bool}: match xs: case Nil{}: {==} case Con{+x, +r}: +h1 = NL.or_ff_l(S.str_eq(ST.skey(ll, kl, x), key), S.mem(key, WL.mapk(ll, kl, r)), h) +h2 = NL.or_ff_r(S.str_eq(ST.skey(ll, kl, x), key), S.mem(key, WL.mapk(ll, kl, r)), h) L.and_intro(Bool.not(S.str_eq(ST.skey(ll, kl, x), key)), ST.nokey(~V, ll, kl, r, key), NL.not_f(S.str_eq(ST.skey(ll, kl, x), key), h1), nm_nokey(~V, ll, kl, r, key, h2)) def pn_c(~V: Data, +tb: List<&2, U32>, +kl: List<&2, String>, +nb: Nat, +ll: List<&2, U32>, +sl: List<&2, Nat>, +hbsl: {ST.bsl(TB.buckets(tb, kl, nb), sl, ll, nb) == True{} : Bool}, +key: String, +hnk: {ST.nokey(~V, ll, kl, sl, key) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, nb) == True{} : Bool}, +c: Bool, +hc: {B.hold(key, B.at(TB.buckets(tb, kl, nb), j)) == c : Bool}) -> {Bool.not(c) == True{} : Bool}: match c: case False{}: {==} case True{}: +hbl = TF.bsl_inst(TB.buckets(tb, kl, nb), sl, ll, nb, hbsl, j, hj) +hmem = TF.hit_mem(sl, ll, key, B.at(TB.buckets(tb, kl, nb), j), hc, hbl) +hkey = TF.hit_key(sl, ll, kl, key, B.at(TB.buckets(tb, kl, nb), j), hc, hbl, TF.bkok_at(tb, kl, nb, j, hj)) +hn = LS.sall_mem(~V, ST.PNk{ll, kl, key}, UD.v(H.slot(B.lnk(B.at(TB.buckets(tb, kl, nb), j)))), sl, hnk, hmem) Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Bool.not(S.str_eq(ST.skey(ll, kl, UD.v(H.slot(B.lnk(B.at(TB.buckets(tb, kl, nb), j))))), key)), True{}, L.subst(Bool, z => {False{} == Bool.not(z) : Bool}, True{}, S.str_eq(ST.skey(ll, kl, UD.v(H.slot(B.lnk(B.at(TB.buckets(tb, kl, nb), j))))), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, UD.v(H.slot(B.lnk(B.at(TB.buckets(tb, kl, nb), j))))), key), True{}, hkey), {==}), hn))) # a key no listed slot holds is held by no bucket def pno_of(~V: Data, +tb: List<&2, U32>, +kl: List<&2, String>, +nb: Nat, +ll: List<&2, U32>, +sl: List<&2, Nat>, +hbsl: {ST.bsl(TB.buckets(tb, kl, nb), sl, ll, nb) == True{} : Bool}, +key: String, +hnk: {ST.nokey(~V, ll, kl, sl, key) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, nb) == True{} : Bool}) -> {B.all_lt(B.PNo{TB.buckets(tb, kl, nb), key}, m) == True{} : Bool}: match m: case 0n: {==} case 1n+j: +hj = N.succ_le_lt(j, nb, hm) L.and_intro(Bool.not(B.hold(key, B.at(TB.buckets(tb, kl, nb), j))), B.all_lt(B.PNo{TB.buckets(tb, kl, nb), key}, j), pn_c(~V, tb, kl, nb, ll, sl, hbsl, key, hnk, j, hj, B.hold(key, B.at(TB.buckets(tb, kl, nb), j)), {==}), pno_of(~V, tb, kl, nb, ll, sl, hbsl, key, hnk, j, N.le_trans(j, 1n+j, nb, N.le_succ(j), hm))) def mt_e(~V: Data, +e: SP.Ent, +r: List<&2, SP.Ent>, +key: String, +h: {S.mem(key, SP.keys_of(~V, Con{e, r})) == False{} : Bool}) -> {S.mem(key, SP.keys_of(~V, r)) == False{} : Bool}: match e: case SP.LE{+kk, +w, +t, +d}: NL.or_ff_r(S.str_eq(kk, key), S.mem(key, SP.keys_of(~V, r)), h) def mem_tail(~V: Data, +es: List<&2, SP.Ent>, +key: String, +h: {S.mem(key, SP.keys_of(~V, es)) == False{} : Bool}) -> {S.mem(key, SP.keys_of(~V, SP.tail(~V, es))) == False{} : Bool}: match es: case Nil{}: {==} case Con{+e, +r}: mt_e(~V, e, r, key, h) def len_tail(~V: Data, +es: List<&2, SP.Ent>, +h: {Nat.is_lt(0n, SP.length(~V, es)) == True{} : Bool}) -> {1n+SP.length(~V, SP.tail(~V, es)) == SP.length(~V, es) : Nat}: match es: case Nil{}: Empty.absurd({1n+SP.length(~V, SP.tail(~V, Nil{})) == SP.length(~V, Nil{}) : Nat}, L.false_true(h)) case Con{+x, +r}: {==} def mfe_c(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +b: Bool, +hb: {U32.is_eq(free, 0) == b : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, b)): match b: case True{}: +pm = 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, sl, fl, hg) +x1 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.fresh_f(&2, V, cap, n, head, tail, free, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, r), Array.get(U32, AR.thaw(U32, mT), 0), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 0n)), UT.uget(5n, {==}, mT, pm, 0, {==})) +x2 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.fresh_sz(&2, V, cap, n, head, tail, free, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), r), Array.get(U32, AR.thaw(U32, mT), 1), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 1n)), UT.uget(5n, {==}, mT, pm, 1, {==})) +X = Equal.trans(LR.LRU<&2, V>, LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, True{}), LR.fresh_sz(&2, V, cap, n, head, tail, free, AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), Array.get(U32, AR.thaw(U32, mT), 1)), LR.fresh_room(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), x1, x2) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.fresh_room(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, True{}), Equal.sym(LR.LRU<&2, V>, LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, True{}), LR.fresh_room(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(W32.nth0(AR.slots(U32, mT), 0n)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n))), X), fr_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, free, hb, hb, U32.is_lt(W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n)), {==})) case False{}: IP.ip_free(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, hb) def mfe_b(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, +b: Bool, +hb: {U32.is_eq(free, 0) == b : Bool}) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): +pm = 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, sl, fl, hg) +er = Equal.trans(Array, H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), H.put_bucket(AR.thaw(U32, tabT), U32.from_nat(e), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), RI.raw_ok(one, h1, k, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), AR.slots(String, ksT), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))), e, he, hz, hp), GR.put_eq(k, 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, sl, fl, hg)), {==}), 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, sl, fl, hg), e, he, K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))) +e1 = Equal.cong(Array, LR.LRU<&2, V>, tb => LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), tb, AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), er) +e2 = Equal.cong(Bool, LR.LRU<&2, V>, c => LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, c), U32.is_eq(free, 0), b, hb) ok = mfe_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, b, hb) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, b), LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Equal.sym(LR.LRU<&2, V>, LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, b), Equal.trans(LR.LRU<&2, V>, LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.alloc_pick(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, AR.upd(U32, 1n+k, AR.upd(U32, 1n+k, tabT, UD.v(U32.shl(U32.from_nat(e))), K.kword(key)), UD.v(U32.inc(U32.shl(U32.from_nat(e)))), H.link(LR.pick(b, W32.nth0(AR.slots(U32, mT), 0n), H.slot(free))))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}, b), e1, e2)), ok) # the full path after the eviction: re-probe for an empty bucket, then place def mf_e(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +e: Nat, +he: {Nat.is_lt(e, SC.pow2(k)) == True{} : Bool}, +hz: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), e) == B.BE{} : B.Bk}, +hp: {B.occpath(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), M.dist(SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), e)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.miss_full(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): +x1 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.insert_slot(&2, V, LR.ins_mask(&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), K.kword(key), r), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), 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, sl, 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, sl, fl, hg))))) +x2 = Equal.cong(Array & U32, LR.LRU<&2, V>, r => LR.insert_slot(&2, V, LR.ins_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), K.kword(key), CY.msk(k), LR.next_slot_m(free, r)), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Array.get(U32, AR.thaw(U32, mT), 0), (AR.thaw(U32, mT), W32.nth0(AR.slots(U32, mT), 0n)), 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, sl, fl, hg), 0, {==})) +X = Equal.trans(LR.LRU<&2, V>, LR.miss_full(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.insert_slot(&2, V, LR.ins_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), K.kword(key), CY.msk(k), LR.next_slot_m(free, Array.get(U32, AR.thaw(U32, mT), 0))), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(U32.is_eq(free, 0), W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), x1, x2) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, z), LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(U32.is_eq(free, 0), W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.miss_full(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), Equal.sym(LR.LRU<&2, V>, LR.miss_full(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), LR.insert_slot(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), H.ins_raw(AR.thaw(U32, tabT), CY.msk(k), K.kword(key), H.link(LR.pick(U32.is_eq(free, 0), W32.nth0(AR.slots(U32, mT), 0n), H.slot(free)))), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi}), X), mfe_b(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi, U32.is_eq(free, 0), {==})) def mf_f(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, fe: RI.FirstE(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))))) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(ST.ctr(AR.slots(U32, mT)))}, LR.miss_full(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): match fe: case Tuple{+e, Tuple{+he, Tuple{+hz, hp}}}: mf_e(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, e, he, hz, hp, hroom, v, t, lo, hi) def mf_sh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}, +k0: Nat, +hk: {BK.shk(~V, sh) == k0 : Nat}, +key: String, +hroom: {Nat.is_le(Nat.double(1n+SP.length(~V, ST.lru_es(~V, ST.model(~V, sh)))), SC.pow2(k0)) == True{} : Bool}, +hnm: {S.mem(key, SP.keys_of(~V, ST.lru_es(~V, ST.model(~V, sh)))) == False{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> BS.CountOK(~V, ins_spec(~V, ST.model(~V, sh), key, v, t, lo, hi), LR.miss_full(&2, V, ST.real(~V, sh), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: +hr1 = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), SC.pow2(z)) == True{} : Bool}, k0, k, Equal.sym(Nat, k, k0, hk), hroom) +hr2 = L.subst(Nat, z => {Nat.is_le(Nat.double(1n+z), SC.pow2(k)) == True{} : Bool}, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), UD.v(n), BA.len_model(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg), hr1) +hm2 = L.subst(List<&2, String>, z => {S.mem(key, z) == False{} : Bool}, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), WL.km(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), sl, 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, sl, fl, hg)), hnm) +hnk = nm_nokey(~V, AR.slots(U32, lkT), AR.slots(String, ksT), sl, key, hm2) +hno = pno_of(~V, AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), AR.slots(U32, lkT), sl, ST.g_cbsl(~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, sl, fl, hg), key, hnk, SC.pow2(k), N.le_refl(SC.pow2(k))) +hn = N.succ_le_lt(0n, SC.pow2(k), N.pow2_pos(k)) +cn = N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~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, sl, fl, hg)) +hem = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(k)) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), cn, BA.n_lt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)) mf_f(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, key, hno, hr2, v, t, lo, hi, RI.find_e(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), hn, CY.msk(k), key, UD.v(HS.bucket(K.kword(key), CY.msk(k))), PA.home_lt(K.kword(key), k), 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, sl, fl, hg), hno, hem)) def mf_c(~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, +t0: 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, t0}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hnk: {ST.nokey(~V, AR.slots(U32, lkT), AR.slots(String, ksT), Con{s0, t0}, key) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32, co: 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, t0})), 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, t0}, fl}), H.slot(head), 1)), k)) -> BS.CountOK(~V, ins_spec(~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, t0})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, key, v, t, lo, hi), LR.miss_full(&2, V, 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, t0}, fl}), H.slot(head), 1)), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): match co: case Tuple{+sh1, Tuple{+e1, Tuple{+em1, Tuple{+g1, hk1}}}}: +ees = Equal.cong(SP.Lru, List<&2, SP.Ent>, z => ST.lru_es(~V, z), ST.model(~V, sh1), 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, t0})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, em1) +eln = BA.len_model(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t0}, fl, hg) +hpos = L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, 1n+SC.length(Nat, t0), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), Equal.sym(Nat, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), 1n+SC.length(Nat, t0), BA.es_len(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Con{s0, t0}, 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, t0}, fl, hg))), {==}) +elt = Equal.trans(Nat, 1n+SP.length(~V, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0}))), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), UD.v(n), len_tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0}), hpos), eln) +hr0 = L.subst(Nat, z => {Nat.is_le(Nat.double(z), SC.pow2(k)) == True{} : Bool}, UD.v(n), 1n+SP.length(~V, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0}))), Equal.sym(Nat, 1n+SP.length(~V, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0}))), UD.v(n), elt), N.le_trans(Nat.double(UD.v(n)), Nat.double(1n+UD.v(n)), SC.pow2(k), N.double_le(UD.v(n), 1n+UD.v(n), N.le_succ(UD.v(n))), hroom)) +hr1 = L.subst(List<&2, SP.Ent>, z => {Nat.is_le(Nat.double(1n+SP.length(~V, z)), SC.pow2(k)) == True{} : Bool}, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), ST.lru_es(~V, ST.model(~V, sh1)), Equal.sym(List<&2, SP.Ent>, ST.lru_es(~V, ST.model(~V, sh1)), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), ees), hr0) +hm0 = L.subst(List<&2, String>, z => {S.mem(key, z) == False{} : Bool}, WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), Con{s0, t0}), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), Con{s0, t0}), WL.km(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), Con{s0, t0}, 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, t0}, fl, hg))), I1.nokey_nm(~V, AR.slots(U32, lkT), AR.slots(String, ksT), Con{s0, t0}, key, hnk)) +hm1 = L.subst(List<&2, SP.Ent>, z => {S.mem(key, SP.keys_of(~V, z)) == False{} : Bool}, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), ST.lru_es(~V, ST.model(~V, sh1)), Equal.sym(List<&2, SP.Ent>, ST.lru_es(~V, ST.model(~V, sh1)), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0})), ees), mem_tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t0}), key, hm0)) ok = mf_sh(~V, one, h1, sh1, g1, k, hk1, key, hr1, hm1, v, t, lo, hi) ok2 = L.subst(SP.Lru, z => BS.CountOK(~V, ins_spec(~V, z, key, v, t, lo, hi), LR.miss_full(&2, V, ST.real(~V, sh1), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})), ST.model(~V, sh1), 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, t0})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, em1, ok) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, ins_spec(~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, t0})), SP.c_ev(ST.ctr(AR.slots(U32, mT)))}, key, v, t, lo, hi), LR.miss_full(&2, V, z, PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})), ST.real(~V, sh1), 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, t0}, fl}), H.slot(head), 1)), Equal.sym(LR.LRU<&2, V>, 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, t0}, fl}), H.slot(head), 1)), ST.real(~V, sh1), e1), ok2) # THEOREM (add, a missing key, a full cache: the oldest is evicted first) def mf_ok(~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, +sl: 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, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +key: String, +hnk: {ST.nokey(~V, AR.slots(U32, lkT), AR.slots(String, ksT), sl, key) == True{} : Bool}, +hroom: {Nat.is_le(Nat.double(1n+UD.v(n)), SC.pow2(k)) == True{} : Bool}, +hfull: {U32.is_le(cap, n) == True{} : Bool}, +v: V, +t: U32, +lo: U32, +hi: U32) -> BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(SP.c_ev(ST.ctr(AR.slots(U32, mT))))}, LR.miss_full(&2, V, LR.evict_oldest(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})): match sl: case Nil{}: +gn = ST.g_clen(~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, Nil{}, fl, hg) +en = Equal.sym(Nat, 0n, UD.v(n), N.eq_from_is_eq(0n, UD.v(n), gn)) +hc0 = L.subst(Nat, z => {Nat.is_le(UD.v(cap), z) == True{} : Bool}, UD.v(n), 0n, en, Equal.trans(Bool, Nat.is_le(UD.v(cap), UD.v(n)), U32.is_le(cap, n), True{}, Equal.sym(Bool, U32.is_le(cap, n), Nat.is_le(UD.v(cap), UD.v(n)), is_le_nat(cap, n)), hfull)) +ec = N.le_antisym(UD.v(cap), 0n, hc0, N.zero_le(UD.v(cap))) +hce = Equal.trans(Bool, U32.is_eq(cap, 0), Nat.is_eq(UD.v(cap), 0n), True{}, is_eq_nat(cap, 0), L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, 0n, UD.v(cap), Equal.sym(Nat, UD.v(cap), 0n, ec), {==})) +hcc = ST.g_ccap(~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, Nil{}, fl, hg) Empty.absurd(BS.CountOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Nil{})), SP.LE{key, v, t, W.U64{lo, hi}}), SP.c_ins(SP.c_ev(ST.ctr(AR.slots(U32, mT))))}, LR.miss_full(&2, V, LR.evict_oldest(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl})), PA.stored(key), K.kword(key), LR.E{v, t, lo, hi})), L.false_true(Equal.trans(Bool, False{}, Bool.not(U32.is_eq(cap, 0)), True{}, L.subst(Bool, z => {False{} == Bool.not(z) : Bool}, True{}, U32.is_eq(cap, 0), Equal.sym(Bool, U32.is_eq(cap, 0), True{}, hce), {==}), hcc))) case Con{+s0, +t0}: mf_c(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t0, fl, hg, one, h1, key, hnk, hroom, v, t, lo, hi, EK.old_evk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t0, fl, hg, one, h1))