proofs/containers/hash_table/buckets.bend checks

type Bk source · line 16 · raw

Data

• BE

  Bk

• BF

  @w:U32 -> @l:U32 -> @k:String -> Bk

type MS source · line 45 · raw

Data

• MEnd

  MS

• MHit

  @l:U32 -> MS

• MNext

  MS

type Res source · line 57 · raw

Data

• RHit

  @at:Nat -> @l:U32 -> Res

• REnd

  @at:Nat -> Res

type Pred source · line 178 · raw

Data

• PClus

  @bs:List<&2, Bk> -> @n:Nat -> @mask:U32 -> Pred

• PVis

  @bs:List<&2, Bk> -> @n:Nat -> @h:Nat -> @key:String -> Pred

• PHome

  @bs:List<&2, Bk> -> @mask:U32 -> @key:String -> @h:Nat -> Pred

• PNo

  @bs:List<&2, Bk> -> @key:String -> Pred

• PWell

  @bs:List<&2, Bk> -> @sd:Nat -> Pred

• PUniq

  @bs:List<&2, Bk> -> Pred

• PLive

  @bs:List<&2, Bk> -> @lv:List<&2, Bool> -> @f:Nat -> Pred

• PFrom

  @bs:List<&2, Bk> -> @src:List<&2, Bk> -> @m:Nat -> Pred

• PTo

  @bs:List<&2, Bk> -> @dst:List<&2, Bk> -> @m:Nat -> Pred

• PHole

  @bs:List<&2, Bk> -> @n:Nat -> @mask:U32 -> @h:Nat -> @dk:Nat -> Pred

def at source · line 20 · raw

@bs:List<&2, Bk> -> @+i:Nat -> Bk

def occ source · line 29 · raw

@b:Bk -> Bool

def hold source · line 37 · raw

@+key:String -> @b:Bk -> Bool

def mstep source · line 50 · raw

@+key:String -> @b:Bk -> MS

def pf source · line 62 · raw

@+key:String -> @+bs:List<&2, Bk> -> @+n:Nat -> @fuel:Nat -> @s:MS -> @+i:Nat -> Res

def hb source · line 80 · raw

@+mask:U32 -> @b:Bk -> Nat

def hold_occ source · line 87 · raw

@+key:String -> @+b:Bk -> @+h:{hold(key, b) == True{} : Bool} -> {occ(b) == True{} : Bool}

def occpath source · line 95 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+m:Nat -> Bool

def lnk source · line 103 · raw

@b:Bk -> U32

def nohb source · line 111 · raw

@+bs:List<&2, Bk> -> @+key:String -> @+i:Nat -> Bool

def nolb source · line 119 · raw

@+bs:List<&2, Bk> -> @+l:U32 -> @+i:Nat -> Bool

def nthb source · line 126 · raw

@bs:List<&2, Bool> -> @+i:Nat -> Bool

def uq_b source · line 135 · raw

@+bs:List<&2, Bk> -> @+i:Nat -> @b:Bk -> Bool

def live_b source · line 142 · raw

@+lv:List<&2, Bool> -> @+f:Nat -> @b:Bk -> Bool

def bk_eq source · line 150 · raw

@a:Bk -> @b:Bk -> Bool

def anyeq source · line 162 · raw

@+bs:List<&2, Bk> -> @+m:Nat -> @+b:Bk -> Bool

def opx source · line 170 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+a:Nat -> @+m:Nat -> @+h:Nat -> Bool

def implies source · line 190 · raw

@a:Bool -> @b:Bool -> Bool

def imp_elim source · line 193 · raw

@+a:Bool -> @+b:Bool -> @+h:{implies(a, b) == True{} : Bool} -> @+ha:{a == True{} : Bool} -> {b == True{} : Bool}

def wb source · line 202 · raw

@+sd:Nat -> @b:Bk -> Bool

def eval source · line 209 · raw

@p:Pred -> @+i:Nat -> Bool

def all_lt source · line 233 · raw

@+p:Pred -> @+n:Nat -> Bool

def all_inst_c source · line 240 · raw

@+p:Pred -> @+q:Nat -> @+h:{Bool.and(eval(p, q), all_lt(p, q)) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+q) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(i, q) == c : Bool} -> @rec:(@hlt:{Nat.is_lt(i, q) == True{} : Bool} -> {eval(p, i) == True{} : Bool}) -> {eval(p, i) == True{} : Bool}

def all_inst source · line 248 · raw

@+p:Pred -> @+n:Nat -> @+h:{all_lt(p, n) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {eval(p, i) == True{} : Bool}

def occ_c source · line 255 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+q:Nat -> @+hp:{Bool.and(occ(at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, q))), occpath(bs, n, h, q)) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, 1n+q) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(i, q) == c : Bool} -> @rec:(@hlt:{Nat.is_lt(i, q) == True{} : Bool} -> {occ(at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, i))) == True{} : Bool}) -> {occ(at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, i))) == True{} : Bool}

def occ_inst source · line 262 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+m:Nat -> @+hp:{occpath(bs, n, h, m) == True{} : Bool} -> @+i:Nat -> @+hi:{Nat.is_lt(i, m) == True{} : Bool} -> {occ(at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, i))) == True{} : Bool}

def cluster source · line 269 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+mask:U32 -> Bool

def ResOK source · line 274 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+key:String -> @r:Res -> Type

def not_true_false source · line 281 · raw

@+e:{Bool.not(True{}) == True{} : Bool} -> Empty

def occ_be source · line 284 · raw

@+e:{occ(BE{}) == True{} : Bool} -> Empty

def occ_at_be source · line 287 · raw

@+bs:List<&2, Bk> -> @+i:Nat -> @+hz:{at(bs, i) == BE{} : Bk} -> @+ho:{occ(at(bs, i)) == True{} : Bool} -> Empty

def nh_far source · line 292 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+t:Nat -> @+d:Nat -> @+hz:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, t)) == BE{} : Bk} -> @+hp:{occpath(bs, n, h, d) == True{} : Bool} -> @+oj:{occ(at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, d))) == True{} : Bool} -> @+htd:{Nat.is_le(t, d) == True{} : Bool} -> @+b2:Bool -> @+hb2:{Nat.is_eq(t, d) == b2 : Bool} -> Empty

def nh_near source · line 300 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+t:Nat -> @+key:String -> @+d:Nat -> @+j:Nat -> @+hv:{all_lt(PVis{bs, n, h, key}, t) == True{} : Bool} -> @+hpj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, d) == j : Nat} -> @+hk:{hold(key, at(bs, j)) == True{} : Bool} -> @+hdt:{Nat.is_lt(d, t) == True{} : Bool} -> Empty

def nh_split source · line 306 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+t:Nat -> @+key:String -> @+d:Nat -> @+j:Nat -> @+hv:{all_lt(PVis{bs, n, h, key}, t) == True{} : Bool} -> @+hz:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, t)) == BE{} : Bk} -> @+hp:{occpath(bs, n, h, d) == True{} : Bool} -> @+hpj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(n, h, d) == j : Nat} -> @+hk:{hold(key, at(bs, j)) == True{} : Bool} -> @+b1:Bool -> @+hb1:{Nat.is_lt(d, t) == b1 : Bool} -> Empty

def nh_c source · line 314 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+cl:{cluster(bs, 1n+bp, mask) == True{} : Bool} -> @+ho:{all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool} -> @+t:Nat -> @+hv:{all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool} -> @+hz:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)) == BE{} : Bk} -> @+j:Nat -> @+hj:{Nat.is_lt(j, 1n+bp) == True{} : Bool} -> @+c:Bool -> @+hc:{hold(key, at(bs, j)) == c : Bool} -> {Bool.not(hold(key, at(bs, j))) == True{} : Bool}

def nh_all source · line 326 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+cl:{cluster(bs, 1n+bp, mask) == True{} : Bool} -> @+ho:{all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool} -> @+t:Nat -> @+hv:{all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool} -> @+hz:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)) == BE{} : Bk} -> @+m:Nat -> @+hm:{Nat.is_le(m, 1n+bp) == True{} : Bool} -> {all_lt(PNo{bs, key}, m) == True{} : Bool}

def occ_of_vis source · line 334 · raw

@+bs:List<&2, Bk> -> @+n:Nat -> @+h:Nat -> @+key:String -> @+t:Nat -> @+hv:{all_lt(PVis{bs, n, h, key}, t) == True{} : Bool} -> {occpath(bs, n, h, t) == True{} : Bool}

def next_in source · line 344 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+h:Nat -> @+key:String -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e0:Nat -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+hz0:{at(bs, e0) == BE{} : Bk} -> @+t:Nat -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hv2:{all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(1n+t, 1n+bp) == c : Bool} -> {Nat.is_lt(1n+t, 1n+bp) == True{} : Bool}

def pf_bf source · line 357 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+e0:Nat -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+hz0:{at(bs, e0) == BE{} : Bk} -> @+fp:Nat -> @+t:Nat -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hv:{all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool} -> @+x:U32 -> @+l:U32 -> @+k:String -> @+hb:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)) == BF{x, l, k} : Bk} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k, key) == c : Bool} -> @rec:(@hv2:{all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool} -> @ht2:{Nat.is_lt(1n+t, 1n+bp) == True{} : Bool} -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, fp, mstep(key, at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, 1n+t))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, 1n+t)))) -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, 1n+fp, Bool.pick(MS, c, MHit{l}, MNext{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)))

def pf_b source · line 367 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+cl:{cluster(bs, 1n+bp, mask) == True{} : Bool} -> @+ho:{all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool} -> @+e0:Nat -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+hz0:{at(bs, e0) == BE{} : Bk} -> @+fp:Nat -> @+t:Nat -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hv:{all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool} -> @+b:Bk -> @+hb:{at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)) == b : Bk} -> @rec:(@hv2:{all_lt(PVis{bs, 1n+bp, h, key}, 1n+t) == True{} : Bool} -> @ht2:{Nat.is_lt(1n+t, 1n+bp) == True{} : Bool} -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, fp, mstep(key, at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, 1n+t))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, 1n+t)))) -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, 1n+fp, mstep(key, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)))

def pf_ok source · line 378 · raw

@+bs:List<&2, Bk> -> @+bp:Nat -> @+mask:U32 -> @+key:String -> @+h:Nat -> @+hh:{Nat.is_lt(h, 1n+bp) == True{} : Bool} -> @+cl:{cluster(bs, 1n+bp, mask) == True{} : Bool} -> @+ho:{all_lt(PHome{bs, mask, key, h}, 1n+bp) == True{} : Bool} -> @+e0:Nat -> @+he0:{Nat.is_lt(e0, 1n+bp) == True{} : Bool} -> @+hz0:{at(bs, e0) == BE{} : Bk} -> @+f:Nat -> @+t:Nat -> @+ht:{Nat.is_lt(t, 1n+bp) == True{} : Bool} -> @+hft:{Nat.add(t, f) == 1n+bp : Nat} -> @+hv:{all_lt(PVis{bs, 1n+bp, h, key}, t) == True{} : Bool} -> ResOK(bs, 1n+bp, h, key, pf(key, bs, 1n+bp, f, mstep(key, at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.pos(1n+bp, h, t)))