~/bend-docscommunity

proofs/containers/lru/touch.bend checks

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

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 ../../../src/math/u64.bend as W
import ../hash_table/keys.bend as K
import ../hash_table/state.bend as HT
import ./state.bend as ST
import ./lists.bend as LS
import ../../lib/nat_list.bend as NL

Templates

template ent source · line 25 · raw

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

the entry of a live slot

template enk_of source · line 28 · raw

@-V:Data -> @+x:String -> @+key:String -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(x, key) == True{} : Bool} -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, xs)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/lists.enk(V, xs, key) == True{} : Bool}

template drop_here source · line 38 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+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.drop(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) == r : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template keys_here source · line 45 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+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/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)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, r) : List<&2, String>}

template enk_a source · line 53 · 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> -> @+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} -> @+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/proofs/containers/lru/lists.enk(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, a), key) == True{} : Bool}

keys unique and s holding key: no slot of a holds it

template ev source · line 64 · raw

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

the model entry of slot s holding value v

template es_cons source · line 67 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> @+v:V -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.nthm(V, el, s) == Some{v} : Maybe<&2, V>} -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, s <> b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 5n)}} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, b) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template spec_touch source · line 72 · 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.snoc(V, 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/spec/containers/lru.LE{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, s), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 3n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 4n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, s, 5n)}}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), [s])) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

THEOREM (model side of a touch): dropping the key's entry and appending it is the model of the list a ++ b ++ [s]