~/bend-docscommunity

proofs/containers/lru/lists.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
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 ../../lib/nat_list.bend as NL

Definitions

def mem_app_s source · line 35 · raw

@+x:String -> @+a:List<&2, String> -> @+b:List<&2, String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, b)) == Bool.or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, b)) : Bool}

def mem_mid_s source · line 42 · raw

@+x:String -> @+a:List<&2, String> -> @+s:String -> @+b:List<&2, String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, s <> b)) == Bool.or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(s, x)) : Bool}

def nd_mid_s source · line 49 · raw

@+a:List<&2, String> -> @+s:String -> @+b:List<&2, String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, s <> b)) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, b)), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, a, b)))) : Bool}

Templates

template sall_app source · line 65 · raw

@-V:Data -> @+p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.SP1<V> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, b)) : Bool}

template sa_c source · line 72 · raw

@-V:Data -> @+p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.SP1<V> -> @+x:Nat -> @+s0:Nat -> @+t:List<&2, Nat> -> @+h:{Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sev(V, p, s0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, t)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(s0, x) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t)) == True{} : Bool} -> @rec:(@hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, t) == True{} : Bool} -> @hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sev(V, p, x) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sev(V, p, x) == True{} : Bool}

template sall_mem source · line 80 · raw

@-V:Data -> @+p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.SP1<V> -> @+x:Nat -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sall(V, p, xs) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sev(V, p, x) == True{} : Bool}

p holds at a member

template es_app source · line 90 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, b)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template keys_app source · line 98 · raw

@-V:Data -> @+a:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+b: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>, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.keys_of(V, b)) : List<&2, String>}

template snoc_app source · line 105 · raw

@-V:Data -> @+a:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.snoc(V, a, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, a, [e]) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template enk source · line 113 · raw

@-V:Data -> @a:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+key:String -> Bool

no entry of a has key

template drop_c source · line 120 · raw

@-V:Data -> @+k:String -> @+v:V -> @+t:U32 -> @+d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+r:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+b:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+key:String -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k, key) == c : Bool} -> @+h:{Bool.not(c) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, r, b), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, b, key)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{k, v, t, d} <> r, b), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.LE{k, v, t, d} <> r, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, b, key)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

template drop_app source · line 128 · raw

@-V:Data -> @+a:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+b:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>> -> @+key:String -> @+h:{enk(V, a, key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, a, b), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.drop(V, b, key)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}

drop skips a prefix without key