proofs/containers/lru/keys.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/keys.bend as Keys
26 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/u32alg.bend as A import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC import ../../../spec/containers/lru.bend as SP import ../../lib/u32div.bend as UD import ../../../src/math/u64.bend as W import ../../../src/containers/hash_table.bend as H import ../../../src/containers/lru.bend as LR import ../hash_table/state.bend as HT import ./state.bend as ST import ./basic.bend as BA import ./bumpsh.bend as BS import ./touch.bend as TO import ./rmat.bend as RM import ./gone.bend as GO import ./unlink.bend as UL import ./read.bend as RD import ./evict.bend as EV import ./walk.bend as WL import ../../lib/list.bend as LI import ../../lib/nat_list.bend as NL import ../../lib/links.bend as LK import ../../lib/words32.bend as W32
Definitions
def hat_of source · line 139 · raw
@+sl:List<&2, Nat> -> @+tail:U32 -> @+et:{tail == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(sl, 0) : U32} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(sl, []), tail) == tail : U32}the walk starts at the tail, the first slot of sl reversed
Templates
template some_v source · line 35 · raw
@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+hmm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == m : Maybe<&2, V>} -> @+hsm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> Sigma<&1, &1, V, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>}>the value of a live slot
template kx_nf source · line 43 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, [], fl}) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+f:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, f, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.KDone{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, [], fl})}))an empty cache: nothing to expire
template kx_nil source · line 50 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, [], fl}) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+f:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, f, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, [], fl}), now)))
template kx_ce source · line 55 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+v:V -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), now) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_pick(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.gone(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.ev(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s0, v), now)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Kx<&2, V>}a nonempty cache: the check is whether the oldest entry is gone
template kx_g0 source · line 65 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+g:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 0n, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_pick(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), g)))
template kx_rm source · line 73 · raw
@-V:Data -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+p:Nat -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> @+spec:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V> -> @co:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, spec, r) -> @rec:(@sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh1) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh1), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh1), now)))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, spec, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, r, now)))the oldest entry gone: removed, and the loop goes on
template kx_g1 source · line 80 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+p:Nat -> @+g:Bool -> @rec:(@sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh1) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh1), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh1), now)))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, Bool.pick(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V>, g, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.tail(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.c_rm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 1n+p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_pick(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), g)))
template kx_c0 source · line 87 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 0n, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), now)))
template kx_c1 source · line 91 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+p:Nat -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>} -> @rec:(@sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh1) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh1), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh1), now)))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 1n+p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), now)))
template kx_w0 source · line 99 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @pv:Sigma<&1, &1, V, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 0n, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), now)))
template kx_w1 source · line 104 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+p:Nat -> @pv:Sigma<&1, &1, V, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0) == Some{v} : Maybe<&2, V>}> -> @rec:(@sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh1) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh1), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh1), now)))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 1n+p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, s0 <> t, fl}), now)))
template kx_z source · line 110 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 0n, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), now)))
template kx_s source · line 117 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+p:Nat -> @rec:(@sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @g1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh1) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh1), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh1), now)))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, 1n+p, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), now)))
template kx_ok source · line 125 · raw
@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+f:Nat -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_go(&2, V, f, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.kx_check(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), now)))THEOREM: the expiry loop is the specification's expire
template kn_ok source · line 132 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_n(&2, V, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))
template kl_w source · line 143 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @wo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/walk.WOK(lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(sl, []), [], tail, ksT) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_fin(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_list(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))
template kl_ok source · line 158 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_fin(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_list(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl})))
template kl_sh source · line 164 · raw
@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_fin(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_list(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh)))
template ky source · line 170 · raw
@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ksT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @co:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.CountOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_n(&2, V, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_fin(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.expire(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.length(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.L{cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), sl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT))}, now)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_list(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys_n(&2, V, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}))))
template keys_ok source · line 178 · raw
@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, List<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.model(V, sh), now), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.keys(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.real(V, sh), now))THEOREM: keys refines the specification