proofs/containers/lru/elfr.bend checks

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

11 imports

import Base
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../hash_table/state.bend as HT
import ../hash_table/tools.bend as TL
import ./state.bend as ST
import ./lists.bend as LS
import ./touch.bend as TO
import ../../lib/nat_list.bend as NL

Templates

template live_el source · line 16 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+m:Maybe<&2, V> -> @+x:Nat -> @+h:{Nat.is_eq(y, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, m), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.live(V, el, x) : Bool}

template slok_el source · line 19 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+m:Maybe<&2, V> -> @+fr:Nat -> @+xs:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) : Bool}

template flok_el source · line 28 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+m:Maybe<&2, V> -> @+fr:Nat -> @+xs:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.flok(V, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.flok(V, xs, fr, el) : Bool}

template es_el source · line 37 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+y:Nat -> @+m:Maybe<&2, V> -> @+xs:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, V>, el, y, m), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, xs) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template spec_drop source · line 47 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>} -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), key) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

THEOREM (model side of a removal): dropping key's entry is the model of a ++ b