proofs/containers/lru/keys.bend

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

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/basic.bend as BA
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpsh.bend as BS
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touch.bend as TO
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmat.bend as RM
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as GO
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
20
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as RD
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/evict.bend as EV
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/walk.bend as WL
24import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LI
25import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
26import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
27import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
28
29# keys: the expired oldest prefix removed (each a removal), then the keys
30# oldest first.
31
32
33
34# the value of a live slot
35def 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>}>:
36  match m:
37    case None{}:
38      Empty.absurd(Sigma<&1, &1, V, v => {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}>, L.false_true(hsm))
39    case Some{+v}:
40      (v, hmm)
41
42# an empty cache: nothing to expire
43def 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})})):
44  match f:
45    case 0n:
46      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}, ({==}, ({==}, hg)))
47    case 1n+p:
48      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Nil{}, fl}, ({==}, ({==}, hg)))
49
50def 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))):
51  +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)
52  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))
53
54# a nonempty cache: the check is whether the oldest entry is gone
55def 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>}:
56  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl, hg)
57  +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))
58  +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))
59  +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))
60  +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))
61  +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)
62  +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))
63  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)
64
65def 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))):
66  match g:
67    case True{}:
68      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg)))
69    case False{}:
70      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg)))
71
72# the oldest entry gone: removed, and the loop goes on
73def 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))):
74  match co:
75    case Tuple{+sh1, Tuple{+e1, Tuple{+em1, g1}}}:
76      ok = rec(sh1, g1)
77      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)
78      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)
79
80def 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))):
81  match g:
82    case True{}:
83      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)
84    case False{}:
85      (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, Con{s0, t}, fl}, ({==}, ({==}, hg)))
86
87def 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))):
88  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)))
89
90
91def 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))):
92  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)
93  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)
94  +e = TO.es_cons(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s0, v, hm, t)
95  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)
96  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)
97
98
99def 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))):
100  match pv:
101    case Tuple{+v, hm}:
102      kx_c0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0, t, fl, hg, one, h1, now, v)
103
104def 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))):
105  match pv:
106    case Tuple{+v, hm}:
107      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)
108
109
110def 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))):
111  match sl:
112    case Nil{}:
113      kx_nil(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, fl, hg, now, 0n)
114    case Con{+s0, +t}:
115      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)))))
116
117def 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))):
118  match sl:
119    case Nil{}:
120      kx_nil(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, fl, hg, now, 1n+p)
121    case Con{+s0, +t}:
122      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)
123
124# THEOREM: the expiry loop is the specification's expire
125def 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))):
126  match f sh:
127    case 0n ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:
128      kx_z(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1, now)
129    case 1n+p ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:
130      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))
131
132def 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}))):
133  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))
134
135# ---- the key walk ----
136
137
138# the walk starts at the tail, the first slot of sl reversed
139def 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}:
140  +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))
141  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)
142
143def 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}))):
144  match wo:
145    case Tuple{+K2, Tuple{+a2, Tuple{+ew, Tuple{+hs2, pk2}}}}:
146      +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))))
147      +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)
148      +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)))))
149      +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)
150      +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)
151      +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)
152      +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))
153      +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)
154      +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)
155      +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)
156      (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))))
157
158def 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}))):
159  +hsd = RD.f_hsd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg)
160  +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), {==}, {==})
161  +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)))
162  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))
163
164def 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))):
165  match sh:
166    case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:
167      kl_ok(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, one, h1)
168
169
170def 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})))):
171  match co:
172    case Tuple{+sh2, Tuple{+e1, Tuple{+em1, g2}}}:
173      ok = kl_sh(~V, one, h1, sh2, g2)
174      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)
175      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)
176
177# THEOREM: keys refines the specification
178def 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)):
179  match sh:
180    case ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}:
181      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))