~/bend-docscommunity

proofs/containers/hash_table/qprobe.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/qprobe.bend as Qprobe

20 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./words.bend as WR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./arr.bend as AX
import ./decide.bend as DC
import ./probe_impl.bend as PI
import ./cyc.bend as CY
import ../../lib/nat.bend as N
import ../../lib/word.bend as WD
import ../../lib/u32.bend as UW
import ../../lib/words32.bend as W32

Definitions

def qd_w source · line 24 · raw

@+l:U32 -> @same:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS

def qd_e source · line 31 · raw

@+w:U32 -> @+x:U32 -> @+l:U32 -> @empty:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS

def qdec source · line 38 · raw

@+w:U32 -> @+x:U32 -> @+l:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS

def qstep_of source · line 41 · raw

@ms:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS -> @tab:Array<U32> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QStep

def qs_same source · line 50 · raw

@+td:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:U32 -> @+hd:{Nat.is_lt(td, 32n) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, td, tabT) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(td)) == True{} : Bool} -> @+same:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qs_same(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), i, same) == qstep_of(qd_w(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i)))), same), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QStep}

def qs_if source · line 57 · raw

@+td:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:U32 -> @+w:U32 -> @+hd:{Nat.is_lt(td, 32n) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, td, tabT) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(td)) == True{} : Bool} -> @+x:U32 -> @+e:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qs_if(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), i, w, x, e) == qstep_of(qd_e(w, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i)))), e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QStep}

def qstep source · line 65 · raw

@+td:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+i:U32 -> @+w:U32 -> @+hd:{Nat.is_lt(td, 32n) == True{} : Bool} -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, td, tabT) == True{} : Bool} -> @+hw:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(td)) == True{} : Bool} -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(td)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), i, w) == qstep_of(qdec(w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.shl(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.inc(U32.shl(i))))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QStep}

THEOREM: a short-key probe step reads bucket i and decides as qdec.

def eqc_false source · line 75 · raw

@+x:U32 -> @+c:U32 -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == True{} : Bool} -> @+hs:{U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c)) == False{} : Bool} -> @+e:Bool -> @+he:{U32.is_eq(U32.and(x, 2147483647), c) == e : Bool} -> {e == False{} : Bool}

def qd_short source · line 83 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+x:U32 -> @+l:U32 -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == True{} : Bool} -> @+s:Bool -> @+hs:{U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c)) == s : Bool} -> {qd_w(l, s) == Bool.pick(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(SCon{Chr{U32.and(x, 2147483647)}, ""}, SCon{Chr{c}, ""}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MHit{l}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MNext{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def ql_false source · line 94 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+x:U32 -> @+k:String -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == False{} : Bool} -> @+hinv:{x == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(k) : U32} -> @+e:Bool -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k, SCon{Chr{c}, ""}) == e : Bool} -> {e == False{} : Bool}

a long bucket never holds a one-character key below 2^31

def qsh source · line 102 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+x:U32 -> @+l:U32 -> @+k:String -> @+hinv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x)), U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(k))) == True{} : Bool} -> @+sh:Bool -> @+hsh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == sh : Bool} -> {qd_w(l, U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(SCon{Chr{c}, ""}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{x, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof_c(x, k, sh)}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def qde source · line 114 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+x:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+hinv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(U32.is_eq(x, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x)), U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))))) == True{} : Bool} -> @+e:Bool -> @+he:{U32.is_eq(x, 0) == e : Bool} -> {qd_e(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c), x, l, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(SCon{Chr{c}, ""}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(x, l, kl, e)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def qdecide source · line 123 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+x:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+hinv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(U32.is_eq(x, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x)), U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))))) == True{} : Bool} -> {qdec(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c), x, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(SCon{Chr{c}, ""}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(x, l, kl, U32.is_eq(x, 0))) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

THEOREM: a short-key step decides as the model's step on the decoded bucket.

def qf_of source · line 128 · raw

@r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @tab:Array<U32> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QFound

def qm0 source · line 135 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+key:String -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+mask:U32 -> @+w:U32 -> @+i:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+ms:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qfind(0n, qstep_of(ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)), mask, w, i) == qf_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, 0n, ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QFound}

def qm1 source · line 144 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+key:String -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+n:Nat -> @+mask:U32 -> @+w:U32 -> @+i:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+p:Nat -> @+hnext:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask)) == Nat.mod(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), n) : Nat} -> @+rec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qfind(p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask), w), mask, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask)) == qf_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask)))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QFound} -> @+ms:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qfind(1n+p, qstep_of(ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)), mask, w, i) == qf_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, 1n+p, ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QFound}

def qfind_ok source · line 155 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk31:{Nat.is_lt(k, 31n) == True{} : Bool} -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, 1n+k, tabT) == True{} : Bool} -> @+sd:Nat -> @+kl0:List<&2, String> -> @+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+hwell:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.all_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.PWell{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), sd}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+f:Nat -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qfind(f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.qstep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c), i) == qf_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(SCon{Chr{c}, ""}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k), f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(SCon{Chr{c}, ""}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.at(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.buckets(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tabT), kl0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.QFound}

THEOREM: the implementation's short-key probe loop is the model loop B.pf on the decoded buckets for the key SCon{Chr{c}, ""}.