~/bend-docscommunity

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