proofs/containers/lru/ins1.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ins1.bend as Ins1
25 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/list.bend as LI import ../../../spec/lib/common.bend as SC import ../../../spec/containers/hash_table.bend as S import ../../../spec/containers/lru.bend as SP import ../../lib/u32div.bend as UD import ../../../src/math/u64.bend as W import ../../../src/containers/hash_table.bend as H import ../hash_table/buckets.bend as B import ../hash_table/state.bend as HT import ../hash_table/table.bend as TB import ../hash_table/insm.bend as IM import ../hash_table/insa.bend as IA import ./state.bend as ST import ./dll.bend as DL import ./lists.bend as LS import ./tabsl.bend as TS import ./walk.bend as WL import ../../lib/array.bend as AR import ../../lib/u32.bend as U import ../hash_table/arr.bend as AX import ../../lib/nat_list.bend as NL import ../../lib/links.bend as LK
Definitions
def nsb_of source · line 32 · raw
@+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+s:Nat -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == False{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> {Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b))), s))) == True{} : Bool}
def noslot_bsl source · line 41 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+s:Nat -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, sl) == False{} : Bool} -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(bs, s, m) == True{} : Bool}
def bslb_ns source · line 52 · raw
@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hb:{Bool.not(Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.occ(b), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.lnk(b))), y))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) : Bool}
def bsl_ns source · line 60 · raw
@+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+m:Nat -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.noslot(bs, y, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) : Bool}
def bu_c source · line 71 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+j:Nat -> @+hj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j)) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(e, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), j)) == True{} : Bool}
def bsl_up source · line 78 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, bs)) == True{} : Bool} -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) == True{} : Bool} -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), sl, ll, m) == True{} : Bool}
def isbf_be source · line 87 · raw
@+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{}, w, l) == False{} : Bool}
def ab_c source · line 90 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+l:U32 -> @+w:U32 -> @+m:Nat -> @+j:Nat -> @+hj:{Nat.is_lt(j, m) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.isbf(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, j), w, l) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(e, j) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), m, l, w) == True{} : Bool}
def ab_w source · line 100 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+l:U32 -> @+w:U32 -> @+m:Nat -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/tabsl.AnybAt(bs, m, l, w) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), m, l, w) == True{} : Bool}
def anyb_up source · line 106 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+l:U32 -> @+w:U32 -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(bs, m, l, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.anyb(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), m, l, w) == True{} : Bool}filling an empty bucket keeps every bucket of a slot
def skey_ks source · line 132 · raw
@+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+y:Nat -> @+kk:String -> @+x:Nat -> @+h:{Nat.is_eq(y, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, y, kk), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, x) : String}
def len_snoc source · line 163 · raw
@+xs:List<&2, Nat> -> @+s:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, xs, [s])) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, xs) : Nat}
def nd_snoc source · line 171 · raw
@+xs:List<&2, Nat> -> @+s:Nat -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(xs) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, xs, [s])) == True{} : Bool}
def nds_snoc source · line 178 · raw
@+ks:List<&2, String> -> @+kk:String -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(ks) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(kk, ks) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.nodup(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, ks, [kk])) == True{} : Bool}
def tp_ev source · line 198 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(e)) == e : Nat}
def tp_h source · line 201 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {Nat.is_lt(1n+Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(e))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool}
def tp_i1 source · line 204 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))) == Nat.double(e) : Nat}
def tp_i2 source · line 207 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))) == 1n+Nat.double(e) : Nat}
def tp_p source · line 210 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+k, tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == True{} : Bool}
def tp_sl source · line 214 · raw
@+k:Nat -> @+hk30:{Nat.is_lt(k, 30n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+w:U32 -> @+l:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, 1n+k, tabT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(U32.from_nat(e))), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(U32.from_nat(e)))), l)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), Nat.double(e), w), 1n+Nat.double(e), l) : List<&2, U32>}the written table's slots
def tp_len source · line 227 · raw
@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+k:Nat -> @+e:Nat -> @+he:{Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {Nat.is_lt(e, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(tb, kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)))) == True{} : Bool}the table index e is below the table's length
Templates
template has_up source · line 109 · raw
@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+e:Nat -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BE{} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk} -> @+m:Nat -> @+ll:List<&2, U32> -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, ll, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bupd(bs, e, b), m, ll, xs) == True{} : Bool}
template has_fs source · line 120 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+y:Nat -> @+o:Nat -> @+v:U32 -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+xs:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.off(y, o), v), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, ll, xs) : Bool}
template sent_ks source · line 135 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+y:Nat -> @+kk:String -> @+x:Nat -> @+h:{Nat.is_eq(y, x) == False{} : Bool} -> @+m:Maybe<&2, V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, y, kk), x, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, x, m) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}
template es_ks source · line 142 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+y:Nat -> @+kk:String -> @+el:List<&2, 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(String, kl, y, kk), el, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, xs) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}
template slok_mono source · line 154 · raw
@-V:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+fr2:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+hle:{Nat.is_le(fr, fr2) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr2, el) == True{} : Bool}
template nokey_nm source · line 185 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+xs:List<&2, Nat> -> @+key:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.nokey(V, ll, kl, xs, key) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.mem(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/walk.mapk(ll, kl, xs)) == False{} : Bool}a key no listed slot holds is not among their keys