1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/lru.bend as SP 8 import ../../lib/u32div.bend as UD 9 import ../../../src/math/u64.bend as W 10 import ../../../src/containers/hash_table.bend as H 11 import ../../../src/containers/lru.bend as LR 12 import ../hash_table/state.bend as HT 13 import ./state.bend as ST 14 import ./basic.bend as BA 15 import ./bumpsh.bend as BS 16 import ./touch.bend as TO 17 import ./rmat.bend as RM 18 import ./gone.bend as GO 19 import ./unlink.bend as UL 20 21 import ./read.bend as RD 22 import ./evict.bend as EV 23 import ./walk.bend as WL 24 import ../../lib/list.bend as LI 25 import ../../lib/nat_list.bend as NL 26 import ../../lib/links.bend as LK 27 import ../../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 35 def 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 43 def kx_nf(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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 50 def kx_nil(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +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 55 def kx_ce(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 & 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 65 def kx_g0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 73 def kx_rm(~V: Data, +now: W.U64, +p: Nat, -r: LR.LRU<&2, V>, +spec: SP.Lru, co: BS.CountOK(~V, spec, r), rec: @sh1: ST.Sh -> @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, 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 80 def kx_g1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 -> @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, 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 87 def kx_c0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 91 def kx_c1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 -> @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, 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>, z => BS.CountOK(~V, Bool.pick(SP.Lru, 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>, 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>, 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 99 def kx_w0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 104 def kx_w1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +s0: Nat, +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 -> @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 110 def kx_z(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +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 117 def kx_s(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +p: Nat, rec: @sh1: ST.Sh -> @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 125 def kx_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +f: Nat, +sh: ST.Sh, +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 132 def kn_ok(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +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 139 def 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 143 def kl_w(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, 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 & 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 158 def kl_ok(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> 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 164 def kl_sh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sh: ST.Sh, +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 170 def ky(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree, +k: Nat, +sd: Nat, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +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, 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 178 def keys_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +now: W.U64, +sh: ST.Sh, +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))