proofs/containers/lru/evict.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/evict.bend as Evict
30 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/hash_table.bend as S import ../../../spec/containers/lru.bend as SP import ../../lib/u32div.bend as UD import ../../../src/containers/hash_table.bend as H import ../../../src/containers/lru.bend as LR import ../hash_table/table.bend as TB import ../hash_table/buckets.bend as B import ../hash_table/cyc.bend as CY import ../hash_table/state.bend as HT import ../hash_table/keys.bend as K import ./state.bend as ST 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 ./dellink.bend as DK import ./tabsl.bend as TS import ./linktail.bend as LT import ./idx.bend as ID import ../../lib/links.bend as LK import ../../lib/words32.bend as W32 import ../../lib/u32_tree.bend as UT
Templates
template drop_first source · line 39 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s0:Nat -> @+t:List<&2, Nat> -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s0) == Some{v} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s0 <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s0)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.tail(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s0 <> t)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}the first entry has the first slot's key: dropping it is the tail
template dv_ev source · line 45 · 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> -> @+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>} -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, Maybe<&2, V>) -> @pk:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Maybe<&2, 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/spec/containers/lru.drop(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/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.c_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, Some{v}), r) -> 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/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_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, r))
template eb_ev 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} -> @+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>} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbe0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), e) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0)) == True{} : Bool} -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+el:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0) : U32} -> 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/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_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_slot(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.del_link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head), 1)))
template ek_ev source · line 71 · 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} -> @+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>} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> @ea:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/tabsl.AnybAt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n)) -> 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/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_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_slot(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.del_link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head), 1)))
template ev_m_ev source · line 81 · 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} -> @+m:Maybe<&2, V> -> @+hmm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0) == m : Maybe<&2, V>} -> @+hsm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> 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/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_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.remove_slot(&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/src/containers/hash_table.slot(head), 1)))
template old_ev source · line 101 · 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} -> 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/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_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.remove_slot(&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/src/containers/hash_table.slot(head), 1)))THEOREM: the oldest entry removed (c_ev counted); the model's tail
template dv_rm source · line 111 · 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> -> @+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>} -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, Maybe<&2, V>) -> @pk:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.POK(V, Maybe<&2, 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/spec/containers/lru.drop(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/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), s0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.c_rm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, Some{v}), r) -> 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/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)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, r))
template eb_rm source · line 120 · 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} -> @+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>} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbe0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), e) == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0)) == True{} : Bool} -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+el:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0) : U32} -> 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/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)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_slot(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.del_link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head), 2)))
template ek_rm source · line 137 · 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} -> @+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>} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> @ea:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/tabsl.AnybAt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(s0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n)) -> 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/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)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_slot(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.del_link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, lkT), s0, 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head), 2)))
template ev_m_rm source · line 146 · 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} -> @+m:Maybe<&2, V> -> @+hmm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s0) == m : Maybe<&2, V>} -> @+hsm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(head)) == s0 : Nat} -> 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/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)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.remove_slot(&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/src/containers/hash_table.slot(head), 2)))
template old_rm source · line 166 · 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} -> 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/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)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_v(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.remove_slot(&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/src/containers/hash_table.slot(head), 2)))THEOREM: the oldest entry removed (c_rm counted); the model's tail