proofs/containers/lru/ent.bend checks

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

8 imports

import Base
import ../../lib/array.bend as AR
import ../../../spec/containers/lru.bend as SP
import ../../../src/math/u64.bend as W
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Templates

template EntOK source · line 13 · raw

@-V:Data -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> Type

template ent_d source · line 17 · raw

@-V:Data -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> @+d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.add(now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n)) == d : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64} -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.entry_of(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), v, now) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.ent_dl(&2, V, v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.add(now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n)))) : Pair(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Ent<&2, V>)} -> @+hsp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{key, v, 1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.add(now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.w64(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 4n))} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.mk(V, 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), key, v, now) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>} -> EntOK(V, mT, pm, v, now, key)

template ent_c source · line 25 · raw

@-V:Data -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, mT), 3n), 0) == c : Bool} -> @+e0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.entry_of(&2, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), v, now) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.ent_if(&2, V, v, now, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, mT), Bool.not(c)) : Pair(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Ent<&2, V>)} -> EntOK(V, mT, pm, v, now, key)

template ent_ok source · line 40 · raw

@-V:Data -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 5n, mT) == True{} : Bool} -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> EntOK(V, mT, pm, v, now, key)

THEOREM: entry_of builds an entry whose timing is the specification's mk