~/bend-docscommunity

proofs/containers/lru/drop.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/drop.bend as Drop

13 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
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 ./idx.bend as ID
import ./unlink.bend as UL
import ../../lib/u32_tree.bend as UT

Templates

template drop_ok source · line 20 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+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> -> @+sd:Nat -> @+hsd:{Nat.is_lt(3n+sd, 32n) == True{} : Bool} -> @+hpl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 3n+sd, lkT) == True{} : Bool} -> @+hpe:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, V>, sd, eT) == True{} : Bool} -> @+su:U32 -> @+s:Nat -> @+hsv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su) == s : Nat} -> @+hs0:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+c:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.drop_core(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, n, head, tail, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, eT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, lkT)}, su, c) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.fbump(&2, V, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.F{cap, U32.sub(n, 1), head, tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.link(su), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, ksT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, V>, sd, eT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(su), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 3n+sd, lkT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.nidx(su)), free))}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, V>, eT), s)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>, Maybe<&2, V>)}

THEOREM (drop_core)