proofs/containers/lru/read.bend source
proofs/containers/lru/read.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/math/u64.bend as Wimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ../hash_table/state.bend as HTimport ../hash_table/keys.bend as Kimport ./state.bend as STimport ./basic.bend as BAimport ./bump.bend as BUimport ./bumpsh.bend as BSimport ./find.bend as FDimport ./tfind.bend as TFimport ./touch.bend as TOimport ./touchsh.bend as TSHimport ./rmat.bend as RMimport ./gone.bend as GOimport ./unlink.bend as ULimport ../hash_table/get.bend as Gimport ../../../src/math/hash.bend as HSimport ../hash_table/probe_impl.bend as PIimport ../hash_table/probe_all.bend as PAimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# get and peek (read): the implementation's read is the specification's.# a miss is counteddef rd_miss(~V: Data, +sh: ST.Sh<V>, co: BS.CountOK(~V, BS.cg_miss(~V, ST.model(~V, sh)), LR.fbump(&2, V, 4, ST.real(~V, sh)))) -> RM.POK(~V, Maybe<&2, V>, (BS.cg_miss(~V, ST.model(~V, sh)), None{}), (LR.fbump(&2, V, 4, ST.real(~V, sh)), None{})): match co: case Tuple{+sh2, Tuple{+e, Tuple{+em, g}}}: (sh2, (None{}, (Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (z, None{}), LR.fbump(&2, V, 4, ST.real(~V, sh)), ST.real(~V, sh2), e), (Equal.cong(SP.Lru<V>, SP.Lru<V> & Maybe<&2, V>, z => (z, None{}), BS.cg_miss(~V, ST.model(~V, sh)), ST.model(~V, sh2), Equal.sym(SP.Lru<V>, ST.model(~V, sh2), BS.cg_miss(~V, ST.model(~V, sh)), em)), g))))# ---- the key is absent ----def rd_end0(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +at: U32) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, None{}), LR.rd_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), at, 0, now, tracked, True{})): match tracked: case True{}: rd_miss(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, BS.countg_miss(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, hg)) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (None{}, ({==}, ({==}, hg))))def rd_end(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +at: U32, +hf: {SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key) == None{} : Maybe<&2, SP.Ent<V>>}) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), at, 0, now, tracked, True{})): L.subst(Maybe<&2, SP.Ent<V>>, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, z), LR.rd_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), at, 0, now, tracked, True{})), None{}, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), None{}, hf), rd_end0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, at))# ---- the key's slot s holds value v ----def l_on(~V: Data, l: SP.Lru<V>) -> U32: match l: case SP.L{cap, on, life, es, c}: ondef l_life(~V: Data, l: SP.Lru<V>) -> W.U64: match l: case SP.L{cap, on, life, es, c}: lifedef l_c(~V: Data, l: SP.Lru<V>) -> SP.Ctr: match l: case SP.L{cap, on, life, es, c}: cdef rd_tch(~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>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +m2: AR.Tree<U32>, +em: {ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.c_hit(ST.ctr(AR.slots(U32, mT)))} : SP.Lru<V>}, -r: LR.LRU<&2, V>, to: TSH.TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, m2), 3n), ST.w64(AR.slots(U32, m2), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, m2))}, r)) -> RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), True{}), (r, Some{v})): match to: case Tuple{+sh3, Tuple{+e3, Tuple{+em3, g3}}}: +eo = Equal.cong(SP.Lru<V>, U32, w => l_on(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, em) +el = Equal.cong(SP.Lru<V>, W.U64, w => l_life(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, em) +ec = Equal.cong(SP.Lru<V>, SP.Ctr, w => l_c(~V, w), ST.model(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, em) +es1 = BA.lru_eq(~V, cap, W32.nth0(AR.slots(U32, m2), 3n), W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, m2), 4n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, m2)), SP.c_hit(ST.ctr(AR.slots(U32, mT))), eo, el, {==}, ec) +esp = Equal.trans(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, m2), 3n), ST.w64(AR.slots(U32, m2), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, m2))}, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, em3, es1) (sh3, (Some{v}, (Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, z => (z, Some{v}), r, ST.real(~V, sh3), e3), (Equal.cong(SP.Lru<V>, SP.Lru<V> & Maybe<&2, V>, z => (z, Some{v}), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, ST.model(~V, sh3), Equal.sym(SP.Lru<V>, ST.model(~V, sh3), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, esp)), g3))))def rd_hitc(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, cm: BS.CntM(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), SP.c_hit(ST.ctr(AR.slots(U32, mT)))}, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))) -> RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), True{}), (LR.touch(&2, V, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), su), Some{v})): match cm: case Tuple{+m2, Tuple{+e1, Tuple{+em, g1}}}: +E = Equal.cong(LR.LRU<&2, V>, LR.LRU<&2, V>, z => LR.touch(&2, V, z, su), LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), e1) ok = rd_tch(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk, m2, em, LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), su), TSH.touch_sh(~V, one, h1, cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl, g1, s, hmem, su, hsv, key, hk, v, hm)) L.subst(LR.LRU<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), True{}), (z, Some{v})), LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), su), LR.touch(&2, V, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), su), Equal.sym(LR.LRU<&2, V>, LR.touch(&2, V, LR.fbump(&2, V, 3, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), su), LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, m2, k, sd, tabT, ksT, eT, lkT, sl, fl}), su), E), ok)# a live entry read: tracked, it is counted and touched; untracked, nothingdef rd_lv(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), tracked), LR.rd_live(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked, v)): match tracked: case True{}: rd_hitc(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, True{}, one, h1, s, hmem, su, hsv, v, hm, hk, BS.cntm_hit(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, BU.bump_ok(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), 3, 22n, {==}, {==}, {==}))) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, (Some{v}, ({==}, ({==}, hg))))def f_hsd(~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>, +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}) -> {Nat.is_lt(3n+sd, 32n) == True{} : Bool}: TSH.sd29(k, sd, 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)), ST.g_csdk(~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))def f_s0(~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>, +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}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}) -> {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}: UL.bnd_of(~V, s, sl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), sd, 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, fl, hg), 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), hmem)# reading the value cell of a live slotdef rd_lf(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), tracked), LR.rd_live_f(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked)): +hs0 = f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem) +hsu = GO.su_lt(su, s, sd, hsv, hs0) +hd = N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)) +hn = Equal.trans(Maybe<&2, V>, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, Equal.cong(Nat, Maybe<&2, V>, z => HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), z), UD.v(su), s, hsv), hm) +hx = L.subst(Maybe<&2, V>, z => {SC.nth(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su)) == Some{z} : Maybe<&2, Maybe<&2, V>>}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su)), Some{v}, hn, HT.nthm_some(~V, AR.slots(Maybe<&2, V>, eT), UD.v(su), UT.len_of(Maybe<&2, V>, sd, eT, ST.g_cpe(~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), UD.v(su), hsu))) +eg = AR.get(Maybe<&2, V>, sd, eT, su, Some{v}, hd, hsu, hx, ST.g_cpe(~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 = Equal.cong(Array<Maybe<&2, V>> & Maybe<&2, V>, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rd_v(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(U32, lkT), su, tracked, r), Array.get(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, eT), su), (AR.thaw(Maybe<&2, V>, eT), Some{v}), eg) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), tracked), z), LR.rd_live(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked, v), LR.rd_live_f(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rd_live_f(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked), LR.rd_live(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, tracked, v), E), rd_lv(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk))# after the removal of the expired entry: a miss, counted when trackeddef rd_gn(~V: Data, +tracked: Bool, +sh2: ST.Sh<V>, +hg2: {ST.good(~V, sh2) == True{} : Bool}, +x: Maybe<&2, V>, +cap: U32, +on: U32, +life: W.U64, +es2: List<&2, SP.Ent<V>>, +c: SP.Ctr, +hm2: {SP.L{cap, on, life, es2, c} == ST.model(~V, sh2) : SP.Lru<V>}) -> RM.POK(~V, Maybe<&2, V>, (SP.L{cap, on, life, es2, SP.c_miss_if(c, tracked)}, None{}), LR.rd_gone(&2, V, tracked, (ST.real(~V, sh2), x))): match tracked: case True{}: L.subst(SP.Lru<V>, z => RM.POK(~V, Maybe<&2, V>, (BS.cg_miss(~V, z), None{}), (LR.fbump(&2, V, 4, ST.real(~V, sh2)), None{})), ST.model(~V, sh2), SP.L{cap, on, life, es2, c}, Equal.sym(SP.Lru<V>, SP.L{cap, on, life, es2, c}, ST.model(~V, sh2), hm2), rd_miss(~V, sh2, BS.countg_miss(~V, sh2, hg2))) case False{}: (sh2, (None{}, ({==}, (Equal.cong(SP.Lru<V>, SP.Lru<V> & Maybe<&2, V>, z => (z, None{}), SP.L{cap, on, life, es2, c}, ST.model(~V, sh2), hm2), hg2))))def rd_ex2(~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>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, -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), sl), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}), r)) -> 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), sl), key), SP.c_miss_if(SP.c_rm(ST.ctr(AR.slots(U32, mT))), tracked)}, None{}), LR.rd_gone(&2, V, tracked, r)): match pk: case Tuple{+sh2, Tuple{+x, Tuple{+er, Tuple{+es, g2}}}}: +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), sl), key), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, Some{v}, ST.model(~V, sh2), x, es) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => 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), sl), key), SP.c_miss_if(SP.c_rm(ST.ctr(AR.slots(U32, mT))), tracked)}, None{}), LR.rd_gone(&2, V, tracked, z)), (ST.real(~V, sh2), x), r, Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, r, (ST.real(~V, sh2), x), er), rd_gn(~V, tracked, sh2, g2, x, 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), sl), key), SP.c_rm(ST.ctr(AR.slots(U32, mT))), hm2))# an expired entry: removed, then read as a missdef rd_ex(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}) -> 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), sl), key), SP.c_miss_if(SP.c_rm(ST.ctr(AR.slots(U32, mT))), tracked)}, None{}), LR.rd_expire(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked)): +em6 = 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)) +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, sl, 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), em6)) +E = Equal.cong(Array<U32> & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rd_exp_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), su, U32.from_nat(i), tracked, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), g6) ok = rd_ex2(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk, 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(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2), RM.rm_at_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem, one, h1, i, hi, hoi, hsi, su, hsv, v, hm, key, hk)) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => 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), sl), key), SP.c_miss_if(SP.c_rm(ST.ctr(AR.slots(U32, mT))), tracked)}, None{}), z), LR.rd_gone(&2, V, tracked, 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(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)), LR.rd_expire(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rd_expire(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked), LR.rd_gone(&2, V, tracked, 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(i)), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su, 2)), E), ok)def rd_gp(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +g: Bool) -> RM.POK(~V, Maybe<&2, V>, Bool.pick(SP.Lru<V> & Maybe<&2, V>, g, (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), sl), key), SP.c_miss_if(SP.c_rm(ST.ctr(AR.slots(U32, mT))), tracked)}, None{}), SP.read_live(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), tracked)), LR.rd_gone_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked, g)): match g: case True{}: rd_ex(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk, i, hi, hoi, hsi) case False{}: rd_lf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk)# a hit: the expiry test, then the live or the expired readdef rd_h(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}), LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked)): +eg = GO.gone_ok(~V, one, h1, lkT, sd, f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg), 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, sl, fl, hg), su, s, hsv, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, hmem), now, ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), v) +E = Equal.cong(Array<U32> & Bool, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rd_g(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), su, U32.from_nat(i), tracked, r), LR.gone(AR.thaw(U32, lkT), su, now), (AR.thaw(U32, lkT), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), now)), eg) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}), z), LR.rd_gone_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), now)), LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked), LR.rd_gone_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), tracked, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), now)), E), rd_gp(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk, i, hi, hoi, hsi, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v), now)))# ---- the probe's result ----def lnz(+sd: Nat, +key: String, +b: B.Bk, +hw: {B.wb(sd, b) == True{} : Bool}, +hk: {B.hold(key, b) == True{} : Bool}) -> {U32.is_eq(B.lnk(b), 0) == False{} : Bool}: match b: case B.BE{}: Empty.absurd({U32.is_eq(B.lnk(B.BE{}), 0) == False{} : Bool}, L.false_true(hk)) case B.BF{+w, +l, +k}: L.not_true(U32.is_eq(l, 0), L.and_right(U32.is_eq(w, K.kword(k)), Bool.not(U32.is_eq(l, 0)), L.and_right(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(w, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw)))def rd_v0(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +m: Maybe<&2, V>, +hmm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == m : Maybe<&2, V>}, +hsm: {HT.some_b(~V, m) == True{} : Bool}) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked)): match m: case None{}: Empty.absurd(RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked)), L.false_true(hsm)) case Some{+v}: +hm = {hmm : {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}} +hlv = L.subst(Maybe<&2, V>, z => {HT.some_b(~V, z) == True{} : Bool}, Some{v}, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Equal.sym(Maybe<&2, V>, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm), {==}) +hf = Equal.trans(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), FD.fnd(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s)), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, FD.find_hit(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s, hlv, key, hk, sl, hmem, ST.g_ckeys(~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)), Equal.cong(Maybe<&2, V>, Maybe<&2, SP.Ent<V>>, z => FD.fnd(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, z), HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s), Some{v}, hm)) L.subst(Maybe<&2, SP.Ent<V>>, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, z), LR.rd_hit(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su, U32.from_nat(i), now, tracked)), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), Some{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)}, hf), rd_h(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, s, hmem, su, hsv, v, hm, hk, i, hi, hoi, hsi))def rd_hi(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk0: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), U32.from_nat(i), l, now, tracked, U32.is_eq(l, 0))): +hwb = B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k), ST.g_cwell(~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), i, hi) +hz = L.subst(U32, z => {U32.is_eq(z, 0) == False{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, lnz(sd, key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hwb, hk0)) +hsi = Equal.cong(U32, Nat, z => UD.v(H.slot(z)), B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl) +hbl = TF.bsl_inst(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sl, AR.slots(U32, lkT), SC.pow2(k), 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), i, hi) +hmem = L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), hsi, TF.hit_mem(sl, AR.slots(U32, lkT), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0, hbl)) +hk = L.subst(Nat, z => {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), z), key) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), hsi, TF.hit_key(sl, AR.slots(U32, lkT), AR.slots(String, ksT), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0, hbl, TF.bkok_at(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), i, hi))) +hls = TF.slok_mem(~V, AR.slots(Maybe<&2, V>, eT), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), UD.v(H.slot(l)), 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), hmem) ok = rd_v0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, UD.v(H.slot(l)), hmem, H.slot(l), {==}, hk, i, hi, B.hold_occ(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk0), hsi, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), UD.v(H.slot(l))), {==}, L.and_right(Nat.is_lt(UD.v(H.slot(l)), UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), UD.v(H.slot(l))), hls)) L.subst(Bool, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_pick(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), U32.from_nat(i), l, now, tracked, z)), False{}, U32.is_eq(l, 0), Equal.sym(Bool, U32.is_eq(l, 0), False{}, hz), ok)def rd_r(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +h: Nat, +r0: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), h, key, r0)) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_fd(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, ksT), PA.stored(key)))): match r0: case B.RHit{+i, +l}: (+hi, rest) = hres (+hk0, hl) = rest rd_hi(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, i, l, hi, hk0, hl) case B.REnd{+e0}: (+he, rest) = hres (+hz, rest2) = rest (+hp, hno) = rest2 +hsd1 = UL.sd1(sd, f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)) +hnk = TF.nokey_of(~V, one, h1, AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), key, hno, AR.slots(U32, lkT), AR.slots(Maybe<&2, V>, eT), sd, hsd1, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 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, fl, hg), 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), 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, sl, fl, hg)) rd_end(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, U32.from_nat(e0), FD.find_miss(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), key, sl, hnk))# ---- read ----def rd_po(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}, +r0: B.Res, hres: B.ResOK(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))), key, r0), po: PA.ProbeOK(tabT, sd, AR.slots(String, ksT), PA.stored(key), K.kword(key), r0, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))) -> RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))): match po: case Tuple{+K2, Tuple{+e, Tuple{+hsl, pk2}}}: +pk = ST.g_cpk(~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) +g1 = L.subst(List<&2, String>, z => {ST.goodF(~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, z, AR.perfect(String, sd, ksT), eT, lkT, sl, fl) == True{} : Bool}, AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl), hg) +hg2 = L.subst(Bool, z => {ST.goodF(~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, K2), z, eT, lkT, sl, fl) == True{} : Bool}, AR.perfect(String, sd, ksT), AR.perfect(String, sd, K2), Equal.trans(Bool, AR.perfect(String, sd, ksT), True{}, AR.perfect(String, sd, K2), pk, Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2)), g1) hres2 = L.subst(List<&2, String>, z => B.ResOK(TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r0), AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hsl), hres) ok = rd_r(~V, cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl, hg2, key, now, tracked, one, h1, UD.v(HS.bucket(K.kword(key), CY.msk(k))), r0, hres2) +E = Equal.cong(H.Found & U32, LR.LRU<&2, V> & Maybe<&2, V>, x => LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, x), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key), (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)), e) ok2 = L.subst(List<&2, String>, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), z, AR.slots(Maybe<&2, V>, eT), sl), key)), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)))), AR.slots(String, K2), AR.slots(String, ksT), hsl, ok) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.read_found(~V, cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), ST.ctr(AR.slots(U32, mT)), key, now, tracked, SP.find(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key)), z), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, (PI.fd_of(r0, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), E), ok2)def read_sh(~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>, +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}, +key: String, +now: W.U64, +tracked: Bool, +one: Nat, +h1: {one == 1n : Nat}) -> RM.POK(~V, Maybe<&2, V>, SP.read(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key, now, tracked), LR.read(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key, now, tracked)): +hk30 = 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)) +hk31 = N.lt_trans(k, 30n, 31n, hk30, {==}) +hsd32 = N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)) +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)) +hocc = 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)) hres = G.res_e0(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), IV.home_all(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd, CY.msk(k), key, SC.pow2(k), ST.g_cwell(~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), SC.pow2(k), N.le_refl(SC.pow2(k))), IV.find_empty(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), hocc)) ok = rd_po(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1, B.pf(key, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k)))), hres, PA.probe_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, sl, fl, hg), sd, hsd32, AR.slots(String, ksT), ksT, {==}, ST.g_cpk(~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), ST.g_cwell(~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)) +em6 = 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)) +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, sl, 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), em6)) +E = Equal.cong(Array<U32> & U32, LR.LRU<&2, V> & Maybe<&2, V>, r => LR.rd_m(V, cap, n, head, tail, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), key, now, tracked, r), Array.get(U32, AR.thaw(U32, mT), 6), (AR.thaw(U32, mT), CY.msk(k)), g6) L.subst(LR.LRU<&2, V> & Maybe<&2, V>, z => RM.POK(~V, Maybe<&2, V>, SP.read(~V, ST.model(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key, now, tracked), z), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), LR.read(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key, now, tracked), Equal.sym(LR.LRU<&2, V> & Maybe<&2, V>, LR.read(V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), key, now, tracked), LR.rd_found(V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT), now, tracked, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key)), E), ok)# THEOREM (read): get (tracked) and peek (untracked) are the specification'sdef read_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64, +tracked: Bool) -> RM.POK(~V, Maybe<&2, V>, SP.read(~V, ST.model(~V, sh), key, now, tracked), LR.read(V, ST.real(~V, sh), key, now, tracked)): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: read_sh(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, key, now, tracked, one, h1)