~/bend-docscommunity

proofs/containers/lru/tfind.bend checks

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

15 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../hash_table/keys.bend as K
import ../hash_table/table.bend as TB
import ../hash_table/buckets.bend as B
import ./state.bend as ST
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Definitions

def bkok source · line 21 · raw

@+kl:List<&2, String> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> Bool

a full bucket's key is its word's key over its slot's stored String

def bkok_dec source · line 28 · raw

@+w:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+e:Bool -> {bkok(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(w, l, kl, e)) == True{} : Bool}

def bkok_at source · line 35 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> {bkok(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j)) == True{} : Bool}

def nk_bf source · line 41 · raw

@+kl:List<&2, String> -> @+key:String -> @+w:U32 -> @+l:U32 -> @+w2:U32 -> @+l2:U32 -> @+k2:String -> @+hbk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l2))))) == True{} : Bool} -> @+hno:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k2, key)) == True{} : Bool} -> @+hi:{Bool.and(U32.is_eq(w2, w), U32.is_eq(l2, l)) == True{} : Bool} -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))), key)) == True{} : Bool}

def nk_b source · line 51 · raw

@+kl:List<&2, String> -> @+key:String -> @+w:U32 -> @+l:U32 -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hbk:{bkok(kl, b) == True{} : Bool} -> @+hno:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, b)) == True{} : Bool} -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(b, w, l) == True{} : Bool} -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))), key)) == True{} : Bool}

a bucket with word w and link l does not hold key: nor does that word's key

def nk_c source · line 58 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+key:String -> @+w:U32 -> @+l:U32 -> @+j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hno:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j))) == True{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j), w, l) == c : Bool} -> @+ho:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j, l, w)) == True{} : Bool} -> @rec:(@h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), j, l, w) == True{} : Bool} -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))), key)) == True{} : Bool}) -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))), key)) == True{} : Bool}

def anyb_nk source · line 66 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+key:String -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), key}, n) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> @+m:Nat -> @+hm:{Nat.is_le(m, n) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), m, l, w) == True{} : Bool} -> {Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))), key)) == True{} : Bool}

no bucket holds key, one has word w and link l: that word's key is not key

def bsl_c source · line 90 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+q:Nat -> @+h:{Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, q)) == True{} : Bool} -> @+i:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(i, q) == c : Bool} -> @rec:(@hq:{Nat.is_lt(i, q) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool}) -> @+hi:{Nat.is_lt(i, 1n+q) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool}

def bsl_inst source · line 97 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, i)) == True{} : Bool}

def hit_mem source · line 105 · raw

@+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+key:String -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, b) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b))), sl) == True{} : Bool}

a full bucket holding key: its slot is listed

def hit_key source · line 113 · raw

@+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+key:String -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.hold(key, b) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> @+hk:{bkok(kl, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b)))), key) == True{} : Bool}

... and that slot's key is key

Templates

template nokey_of source · line 77 · raw

@-V:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+n:Nat -> @+key:String -> @+hno:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PNo{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), key}, n) == True{} : Bool} -> @+ll:List<&2, U32> -> @+el:List<&2, Maybe<&2, V>> -> @+sd:Nat -> @+hsd:{Nat.is_lt(1n+sd, 32n) == True{} : Bool} -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, sl, fr, el) == True{} : Bool} -> @+hh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, n), n, ll, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.nokey(V, ll, kl, sl, key) == True{} : Bool}

THEOREM (table side, miss): no bucket holds key, so no listed slot does

template sm_c source · line 123 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+s:Nat -> @+s0:Nat -> @+t:List<&2, Nat> -> @+h:{Bool.and(Bool.and(Nat.is_lt(s0, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, t, fr, el)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(s0, s) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t)) == True{} : Bool} -> @rec:(@hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, t, fr, el) == True{} : Bool} -> @hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(s, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(s, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s)) == True{} : Bool}

template slok_mem source · line 131 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+s:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, sl, fr, el) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == True{} : Bool} -> {Bool.and(Nat.is_lt(s, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s)) == True{} : Bool}

a listed slot is below fr and live