proofs/containers/lru/pre.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/pre.bend as Pre
21 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/array.bend as AR import ../../../spec/lib/common.bend as SC 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 ../../../src/containers/lru.bend as LR import ../hash_table/buckets.bend as B import ../hash_table/state.bend as HT import ../hash_table/table.bend as TB import ../hash_table/arena.bend as AN import ./state.bend as ST import ./dll.bend as DL import ./idx.bend as ID import ../hash_table/keys.bend as K import ../../lib/nat_list.bend as NL import ../../lib/links.bend as LK import ../../lib/words32.bend as W32
Definitions
def nth0_app source · line 26 · raw
@+xs:List<&2, U32> -> @+r:List<&2, U32> -> @+t:Nat -> @+h:{Nat.is_lt(t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, r), t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(xs, t) : U32}
def lw_app source · line 36 · raw
@+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+o:Nat -> @+ho:{Nat.is_lt(o, 8n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), x, o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.lw(ll, x, o) : U32}
def skey_app source · line 39 · raw
@+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+kl:List<&2, String> -> @+rk:List<&2, String> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, rk), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.skey(ll, kl, x) : String}
def bslb_pre source · line 93 · raw
@+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bslb(sl, ll, b) : Bool}
def bsl_pre source · line 101 · raw
@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+m:Nat -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{bs, sd}, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bsl(bs, sl, ll, m) : Bool}
def upd_comm source · line 113 · raw
@+xs:List<&2, U32> -> @+i:Nat -> @+j:Nat -> @+x:U32 -> @+y:U32 -> @+h:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, i, x), j, y) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, j, y), i, x) : List<&2, U32>}
Templates
template sent_app source · line 42 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+kl:List<&2, String> -> @+rk:List<&2, String> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+m:Maybe<&2, V> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, rk), x, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.sent_m(V, ll, kl, x, m) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}
template es_pre source · line 54 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+kl:List<&2, String> -> @+rk:List<&2, String> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(String, kl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+el:List<&2, Maybe<&2, V>> -> @+re:List<&2, Maybe<&2, V>> -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, el) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(String, kl, rk), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, el, re), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.es(V, ll, kl, el, xs) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>}
template seg_pre source · line 66 · raw
@-V:Data -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+el:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> @+p:U32 -> @+q:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), xs, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.seg(ll, xs, p, q) : Bool}
template has_pre source · line 74 · raw
@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+ll:List<&2, U32> -> @+rl:List<&2, U32> -> @+sd:Nat -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ll) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(3n+sd) : Nat} -> @+el:List<&2, Maybe<&2, V>> -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, ll, rl), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.hasall(V, bs, m, ll, xs) : Bool}
template slok_pre source · line 83 · raw
@-V:Data -> @+sd:Nat -> @+el:List<&2, Maybe<&2, V>> -> @+re:List<&2, Maybe<&2, V>> -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, V>, el) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd) : Nat} -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, el) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.slok(V, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, V>, el, re)) == True{} : Bool}
template vac_eq source · line 127 · raw
@-V:Data -> @+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.vac(&2, V, d) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, V>, d, None{})) : Array<Maybe<&2, V>>}the blank value half