~/bend-docscommunity

proofs/containers/lru/find.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../../../src/math/u64.bend as W
import ../hash_table/keys.bend as K
import ../hash_table/words.bend as WR
import ../hash_table/state.bend as HT
import ./state.bend as ST
import ../../lib/nat_list.bend as NL

Definitions

def or_r source · line 25 · raw

@+a:Bool -> @+b:Bool -> @+h:{b == True{} : Bool} -> {Bool.or(a, b) == True{} : Bool}

def not_true_f source · line 62 · raw

@+b:Bool -> @+h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

Templates

template fnd source · line 18 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> @m:Maybe<&2, V> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>

slot s's entry as find returns it (m is its value cell)

template mk_here source · line 30 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s, m), r))) == True{} : Bool}

template mk_there source · line 37 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+x:String -> @+s0:Nat -> @+m:Maybe<&2, V> -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, r)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s0, m), r))) == True{} : Bool}

template mk_c source · line 44 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+s0:Nat -> @+t:List<&2, Nat> -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == 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:(@h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t))) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s0 <> t))) == True{} : Bool}

template mem_keys source · line 53 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl))) == True{} : Bool}

a live slot on the list has its key among the model's keys

template find_skip source · line 66 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s0:Nat -> @+m:Maybe<&2, V> -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+key:String -> @+hk:{Bool.or(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m)), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s0), key))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s0, m), r), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, r, key) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

an entry whose key is not key is skipped

template find_here source · line 75 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> @+m:Maybe<&2, V> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m) == True{} : Bool} -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s, m), r), key) == fnd(V, ll, kl, s, m) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

the entry holding key is found

template split_d source · line 84 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == True{} : Bool} -> @+t:List<&2, Nat> -> @+hmt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == True{} : Bool} -> @+s0:Nat -> @+d:Bool -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s0), key) == d : Bool} -> @+hn:{Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t)))) == True{} : Bool} -> {Bool.not(d) == True{} : Bool}

the key of an earlier slot differs (keys are unique), and the rest of the keys are unique

template split_m1 source · line 95 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == True{} : Bool} -> @+t:List<&2, Nat> -> @+hmt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == True{} : Bool} -> @+s0:Nat -> @+m:Maybe<&2, V> -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s0, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t)))) == True{} : Bool} -> {Bool.or(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.some_b(V, m)), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s0), key))) == True{} : Bool}

template nd_tail source · line 104 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+t:List<&2, Nat> -> @+s0:Nat -> @+m:Maybe<&2, V> -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, s0, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t)))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t))) == True{} : Bool}

the keys after an entry are unique

template fh_c source · line 111 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == True{} : Bool} -> @+s0:Nat -> @+t:List<&2, Nat> -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s0 <> t))) == 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:(@h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, t) == True{} : Bool} -> @hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, t), key) == fnd(V, ll, kl, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s0 <> t), key) == fnd(V, ll, kl, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template find_hit source · line 120 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, s) == True{} : Bool} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl), key) == fnd(V, ll, kl, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

THEOREM (model side): a live listed slot holding key is what find returns

template find_miss source · line 128 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+key:String -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.nokey(V, ll, kl, sl, key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.find(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, sl), key) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

no listed slot holds key: find returns nothing