proofs/containers/lru/keys.bend source
proofs/containers/lru/keys.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/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/state.bend as HTimport ./state.bend as STimport ./basic.bend as BAimport ./bumpsh.bend as BSimport ./touch.bend as TOimport ./rmat.bend as RMimport ./gone.bend as GOimport ./unlink.bend as ULimport ./read.bend as RDimport ./evict.bend as EVimport ./walk.bend as WLimport ../../lib/list.bend as LIimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# keys: the expired oldest prefix removed (each a removal), then the keys# oldest first.# the value of a live slotdef some_v(~V: Data, +el: List<&2, Maybe<&2, V>>, +s: Nat, +m: Maybe<&2, V>, +hmm: {HT.nthm(~V, el, s) == m : Maybe<&2, V>}, +hsm: {HT.some_b(~V, m) == True{} : Bool}) -> Sigma<&1, &1, V, v => {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}>: match m: case None{}: Empty.absurd(Sigma<&1, &1, V, v => {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}>, L.false_true(hsm)) case Some{+v}: (v, hmm)# an empty cache: nothing to expiredef kx_nf(~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>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}) == True{} : Bool}, +now: W.U64, +f: Nat) -> BS.CountOK(~V, SP.expire(~V, f, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), Nil{}, ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, f, now, LR.KDone{ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl})})): match f: case 0n: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}, ({==}, ({==}, hg))) case 1n+p: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}, ({==}, ({==}, hg)))def kx_nil(~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>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}) == True{} : Bool}, +now: W.U64, +f: Nat) -> BS.CountOK(~V, SP.expire(~V, f, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), Nil{}, ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, f, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}), now))): +hz = ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Nil{}, fl, hg) L.subst(Bool, z => BS.CountOK(~V, SP.expire(~V, f, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), Nil{}, ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, f, now, LR.kx_if(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}), now, z))), True{}, U32.is_eq(head, 0), Equal.sym(Bool, U32.is_eq(head, 0), True{}, hz), kx_nf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, fl, hg, now, f))# a nonempty cache: the check is whether the oldest entry is gonedef kx_ce(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +v: V) -> {LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now) == LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)) : LR.Kx<&2, V>}: +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg) +hs0 = RD.f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg, s0, UL.self_in(s0, t)) +eh = A.eq_of(head, LK.lnk(s0), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)) +hsv = Equal.trans(Nat, UD.v(H.slot(head)), UD.v(H.slot(LK.lnk(s0))), s0, Equal.cong(U32, Nat, z => UD.v(H.slot(z)), head, LK.lnk(s0), eh), UL.ix_o(one, h1, s0, sd, hsd, hs0)) +hz = L.subst(U32, z => {U32.is_eq(z, 0) == False{} : Bool}, LK.lnk(s0), head, Equal.sym(U32, head, LK.lnk(s0), eh), UL.lnk_nz(one, h1, s0, sd, hsd, hs0)) +e1 = Equal.cong(Bool, LR.Kx<&2, V>, b => LR.kx_if(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now, b), U32.is_eq(head, 0), False{}, hz) +e2 = Equal.cong(Array<U32> & Bool, LR.Kx<&2, V>, r => LR.kx_g(&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), r), LR.gone(AR.thaw(U32, lkT), H.slot(head), now), (AR.thaw(U32, lkT), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), GO.gone_ok(~V, one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg), H.slot(head), s0, hsv, hs0, now, ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s0), v)) Equal.trans(LR.Kx<&2, V>, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now), LR.kx_if(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now, False{}), LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), e1, e2)def kx_g0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +now: W.U64, +g: Bool) -> BS.CountOK(~V, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, LR.kx_go(&2, V, 0n, now, LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), g))): match g: case True{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg))) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg)))# the oldest entry gone: removed, and the loop goes ondef kx_rm(~V: Data, +now: W.U64, +p: Nat, -r: LR.LRU<&2, V>, +spec: SP.Lru<V>, co: BS.CountOK(~V, spec, r), rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> BS.CountOK(~V, SP.expire(~V, p, ST.model(~V, sh1), now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now)))) -> BS.CountOK(~V, SP.expire(~V, p, spec, now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, r, now))): match co: case Tuple{+sh1, Tuple{+e1, Tuple{+em1, g1}}}: ok = rec(sh1, g1) ok2 = L.subst(SP.Lru<V>, z => BS.CountOK(~V, SP.expire(~V, p, z, now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now))), ST.model(~V, sh1), spec, em1, ok) L.subst(LR.LRU<&2, V>, z => BS.CountOK(~V, SP.expire(~V, p, spec, now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, z, now))), ST.real(~V, sh1), r, Equal.sym(LR.LRU<&2, V>, r, ST.real(~V, sh1), e1), ok2)def kx_g1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +p: Nat, +g: Bool, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> BS.CountOK(~V, SP.expire(~V, p, ST.model(~V, sh1), now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now)))) -> BS.CountOK(~V, Bool.pick(SP.Lru<V>, g, SP.expire(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, now), 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}), LR.kx_go(&2, V, 1n+p, now, LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), g))): match g: case True{}: kx_rm(~V, now, p, LR.drop_head(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl})), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, EV.old_rm(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1), rec) case False{}: (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg)))def kx_c0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +v: V) -> BS.CountOK(~V, SP.expire(~V, 0n, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 0n, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))): L.subst(LR.Kx<&2, V>, z => BS.CountOK(~V, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, LR.kx_go(&2, V, 0n, now, z)), LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now), Equal.sym(LR.Kx<&2, V>, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now), LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), kx_ce(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, v)), kx_g0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, now, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)))def kx_c1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +p: Nat, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> BS.CountOK(~V, SP.expire(~V, p, ST.model(~V, sh1), now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now)))) -> BS.CountOK(~V, SP.expire(~V, 1n+p, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 1n+p, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))): ok = kx_g1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, p, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now), rec) ok2 = L.subst(LR.Kx<&2, V>, z => BS.CountOK(~V, Bool.pick(SP.Lru<V>, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now), SP.expire(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t})), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, now), 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}), LR.kx_go(&2, V, 1n+p, now, z)), LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now), Equal.sym(LR.Kx<&2, V>, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now), LR.kx_pick(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now)), kx_ce(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, v)), ok) +e = TO.es_cons(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s0, v, hm, t) ok3 = L.subst(List<&2, SP.Ent<V>>, z => BS.CountOK(~V, Bool.pick(SP.Lru<V>, SP.gone(~V, TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), now), SP.expire(~V, p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.tail(~V, z), SP.c_rm(ST.ctr(AR.slots(U32, mT)))}, now), SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, ST.ctr(AR.slots(U32, mT))}), LR.kx_go(&2, V, 1n+p, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), Con{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), t)}, e, ok2) L.subst(List<&2, SP.Ent<V>>, z => BS.CountOK(~V, SP.expire(~V, 1n+p, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 1n+p, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))), Con{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), t)}, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), Con{s0, t}), Con{TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s0, v), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), t)}, e), ok3)def kx_w0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, pv: Sigma<&1, &1, V, v => {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}>) -> BS.CountOK(~V, SP.expire(~V, 0n, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 0n, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))): match pv: case Tuple{+v, hm}: kx_c0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, v)def kx_w1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +s0: Nat, +t: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +p: Nat, pv: Sigma<&1, &1, V, v => {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}>, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> BS.CountOK(~V, SP.expire(~V, p, ST.model(~V, sh1), now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now)))) -> BS.CountOK(~V, SP.expire(~V, 1n+p, 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), Con{s0, t}), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 1n+p, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}), now))): match pv: case Tuple{+v, hm}: kx_c1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, p, v, hm, rec)def kx_z(~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}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64) -> BS.CountOK(~V, SP.expire(~V, 0n, 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), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 0n, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), now))): match sl: case Nil{}: kx_nil(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, fl, hg, now, 0n) case Con{+s0, +t}: kx_w0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, some_v(~V, AR.slots(Maybe<&2, V>, eT), s0, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0), {==}, L.and_right(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0), L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), ST.slok(~V, t, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)))))def kx_s(~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}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +p: Nat, rec: @sh1: ST.Sh<V> -> @g1: {ST.good(~V, sh1) == True{} : Bool} -> BS.CountOK(~V, SP.expire(~V, p, ST.model(~V, sh1), now), LR.kx_go(&2, V, p, now, LR.kx_check(&2, V, ST.real(~V, sh1), now)))) -> BS.CountOK(~V, SP.expire(~V, 1n+p, 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), ST.ctr(AR.slots(U32, mT))}, now), LR.kx_go(&2, V, 1n+p, now, LR.kx_check(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), now))): match sl: case Nil{}: kx_nil(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, fl, hg, now, 1n+p) case Con{+s0, +t}: kx_w1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, p, some_v(~V, AR.slots(Maybe<&2, V>, eT), s0, HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s0), {==}, L.and_right(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0), L.and_left(Bool.and(Nat.is_lt(s0, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s0)), ST.slok(~V, t, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, Con{s0, t}, fl, hg)))), rec)# THEOREM: the expiry loop is the specification's expiredef kx_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +f: Nat, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> BS.CountOK(~V, SP.expire(~V, f, ST.model(~V, sh), now), LR.kx_go(&2, V, f, now, LR.kx_check(&2, V, ST.real(~V, sh), now))): match f sh: case 0n ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: kx_z(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, now) case 1n+p ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: kx_s(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, now, p, sh1 => g1 => kx_ok(~V, one, h1, now, p, sh1, g1))def kn_ok(~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}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64) -> BS.CountOK(~V, SP.expire(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), 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), ST.ctr(AR.slots(U32, mT))}, now), LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): L.subst(Nat, z => BS.CountOK(~V, SP.expire(~V, z, 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), ST.ctr(AR.slots(U32, mT))}, now), LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))), UD.v(n), SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), Equal.sym(Nat, 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)), kx_ok(~V, one, h1, now, UD.v(n), ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}, hg))# ---- the key walk ----# the walk starts at the tail, the first slot of sl reverseddef hat_of(+sl: List<&2, Nat>, +tail: U32, +et: {tail == LK.last_or(sl, 0) : U32}) -> {LK.fst_or(NL.rapp(sl, Nil{}), tail) == tail : U32}: +h = Equal.trans(U32, LK.fst_or(NL.rapp(sl, Nil{}), LK.last_or(sl, 0)), LK.last_or(sl, LK.last_or(sl, 0)), LK.last_or(sl, 0), LK.fo_rapp(sl, Nil{}, LK.last_or(sl, 0)), WL.lo_idem(sl, 0)) L.subst(U32, z => {LK.fst_or(NL.rapp(sl, Nil{}), z) == z : U32}, LK.last_or(sl, 0), tail, Equal.sym(U32, tail, LK.last_or(sl, 0), et), h)def kl_w(~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}, wo: WL.WOK(lkT, AR.slots(String, ksT), sd, NL.rapp(sl, Nil{}), Nil{}, tail, ksT)) -> RM.POK(~V, List<&2, String>, SP.keys_fin(~V, 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), ST.ctr(AR.slots(U32, mT))}), LR.keys_list(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): match wo: case Tuple{+K2, Tuple{+a2, Tuple{+ew, Tuple{+hs2, pk2}}}}: +efu = Equal.trans(Nat, SC.length(Nat, NL.rapp(sl, Nil{})), Nat.add(SC.length(Nat, sl), 0n), UD.v(n), NL.len_rapp(sl, Nil{}), Equal.trans(Nat, Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), UD.v(n), N.add_zero(SC.length(Nat, sl)), N.eq_from_is_eq(SC.length(Nat, sl), UD.v(n), 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, sl, fl, hg)))) +ew2 = L.subst(Nat, z => {LR.wk_loop(z, LR.WK{AR.thaw(String, ksT), AR.thaw(U32, lkT), Nil{}, tail}) == LR.WK{AR.thaw(String, K2), AR.thaw(U32, lkT), WL.racc(AR.slots(U32, lkT), AR.slots(String, ksT), NL.rapp(sl, Nil{}), Nil{}), a2} : LR.Walk}, SC.length(Nat, NL.rapp(sl, Nil{})), UD.v(n), efu, ew) +eac = Equal.trans(List<&2, String>, WL.racc(AR.slots(U32, lkT), AR.slots(String, ksT), NL.rapp(sl, Nil{}), Nil{}), SC.append(String, WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), Nil{}), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), WL.ra_rapp(AR.slots(U32, lkT), AR.slots(String, ksT), sl, Nil{}, Nil{}), Equal.trans(List<&2, String>, SC.append(String, WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), Nil{}), WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), LI.append_nil(String, WL.mapk(AR.slots(U32, lkT), AR.slots(String, ksT), sl)), 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), 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))))) +er1 = Equal.cong(LR.Walk, LR.LRU<&2, V> & List<&2, String>, w => LR.keys_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(Maybe<&2, V>, eT), w), LR.wk_loop(UD.v(n), LR.WK{AR.thaw(String, ksT), AR.thaw(U32, lkT), Nil{}, tail}), LR.WK{AR.thaw(String, K2), AR.thaw(U32, lkT), WL.racc(AR.slots(U32, lkT), AR.slots(String, ksT), NL.rapp(sl, Nil{}), Nil{}), a2}, ew2) +er2 = Equal.cong(List<&2, String>, LR.LRU<&2, V> & List<&2, String>, z => (ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl}), z), WL.racc(AR.slots(U32, lkT), AR.slots(String, ksT), NL.rapp(sl, Nil{}), Nil{}), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), eac) +er = Equal.trans(LR.LRU<&2, V> & List<&2, String>, LR.keys_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(Maybe<&2, V>, eT), LR.wk_loop(UD.v(n), LR.WK{AR.thaw(String, ksT), AR.thaw(U32, lkT), Nil{}, tail})), (ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl}), WL.racc(AR.slots(U32, lkT), AR.slots(String, ksT), NL.rapp(sl, Nil{}), Nil{})), (ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl}), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), er1, er2) +em = Equal.cong(List<&2, String>, SP.Lru<V> & List<&2, String>, z => (SP.L{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))}, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl))), AR.slots(String, ksT), AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), AR.slots(String, ksT), hs2)) +hg1 = 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, ksT), z, eT, lkT, sl, fl) == True{} : Bool}, AR.perfect(String, sd, ksT), True{}, 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), 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, ksT), z, eT, lkT, sl, fl) == True{} : Bool}, True{}, AR.perfect(String, sd, K2), Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2), hg1) +hg3 = 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, K2), 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), hs2), hg2) (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, K2, eT, lkT, sl, fl}, (SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), (er, (em, hg3))))def kl_ok(~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}, +one: Nat, +h1: {one == 1n : Nat}) -> RM.POK(~V, List<&2, String>, SP.keys_fin(~V, 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), ST.ctr(AR.slots(U32, mT))}), LR.keys_list(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))): +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg) +hr = WL.rok_app(~V, AR.slots(U32, lkT), AR.slots(Maybe<&2, V>, eT), sl, Nil{}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), 0, 0, ST.g_cdll(~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), {==}, {==}) +hat = hat_of(sl, tail, A.eq_of(tail, LK.last_or(sl, 0), ST.g_ctail(~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))) kl_w(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, WL.walk(one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, sl, fl, hg), AR.slots(String, ksT), 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), NL.rapp(sl, Nil{}), Nil{}, tail, 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), hr, hat))def kl_sh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> RM.POK(~V, List<&2, String>, SP.keys_fin(~V, ST.model(~V, sh)), LR.keys_list(&2, V, ST.real(~V, sh))): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: kl_ok(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1)def ky(~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>, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, co: BS.CountOK(~V, SP.expire(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), 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), ST.ctr(AR.slots(U32, mT))}, now), LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))) -> RM.POK(~V, List<&2, String>, SP.keys_fin(~V, SP.expire(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), 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), ST.ctr(AR.slots(U32, mT))}, now)), LR.keys_list(&2, V, LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))): match co: case Tuple{+sh2, Tuple{+e1, Tuple{+em1, g2}}}: ok = kl_sh(~V, one, h1, sh2, g2) ok2 = L.subst(SP.Lru<V>, z => RM.POK(~V, List<&2, String>, SP.keys_fin(~V, z), LR.keys_list(&2, V, ST.real(~V, sh2))), ST.model(~V, sh2), SP.expire(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), 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), ST.ctr(AR.slots(U32, mT))}, now), em1, ok) L.subst(LR.LRU<&2, V>, z => RM.POK(~V, List<&2, String>, SP.keys_fin(~V, SP.expire(~V, SP.length(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl)), 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), ST.ctr(AR.slots(U32, mT))}, now)), LR.keys_list(&2, V, z)), ST.real(~V, sh2), LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), Equal.sym(LR.LRU<&2, V>, LR.keys_n(&2, V, now, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})), ST.real(~V, sh2), e1), ok2)# THEOREM: keys refines the specificationdef keys_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> RM.POK(~V, List<&2, String>, SP.keys(~V, ST.model(~V, sh), now), LR.keys(&2, V, ST.real(~V, sh), now)): match sh: case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}: ky(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, one, h1, now, kn_ok(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, now))