proofs/containers/lru/bumpk.bend checks

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

10 imports

import Base
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/lru.bend as SP
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ./basic.bend as BA
import ./bump.bend as BU
import ./bumpsh.bend as BS
import ../../lib/words32.bend as W32

Templates

template shk source · line 16 · raw

@-V:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V> -> Nat

template CountOKk source · line 21 · raw

@-V:Data -> @+spec:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V> -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V> -> @+k:Nat -> Type

template count_evk source · line 24 · 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} -> @bo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bump.BumpOK(mT, 18n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bump(1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT))) -> CountOKk(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/spec/containers/lru.c_ev(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.ctr(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.fbump(&2, V, 1, 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})), k)