~/bend-docscommunity

proofs/containers/hash_table/probe_impl.bend checks

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

19 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./strings.bend as STR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./step.bend as SP
import ./decide.bend as DC
import ./arr.bend as AX
import ./cyc.bend as CY
import ./modn.bend as MN
import ../../lib/word.bend as WD
import ../../lib/words32.bend as W32

Definitions

def or_true_r source · line 24 · raw

@+a:Bool -> {Bool.or(a, True{}) == True{} : Bool}

def wb_sh source · line 31 · raw

@+x:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+sh:Bool -> @+hsh:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == sh : Bool} -> @+h:{U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof_c(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(kl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))), sh))) == True{} : Bool} -> {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}

def wb_facts source · line 38 · raw

@+sd:Nat -> @+x:U32 -> @+l:U32 -> @+kl:List<&2, String> -> @+e:Bool -> @+he:{U32.is_eq(x, 0) == e : Bool} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.wb(sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(x, l, kl, e)) == True{} : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd))) == True{} : Bool}, {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})

def ka_w_ok source · line 52 · raw

@+sd:Nat -> @+K:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+l:U32 -> @+hs:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K) == True{} : Bool} -> @+same:Bool -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ka_w(sd, K, l, same)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K) : List<&2, String>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ka_w(sd, K, l, same)) == True{} : Bool})

def ka_e_ok source · line 59 · raw

@+sd:Nat -> @+K:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+w:U32 -> @+x:U32 -> @+l:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd))) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K) == True{} : Bool} -> @+e:Bool -> @+he:{U32.is_eq(x, 0) == e : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ka_e(sd, K, w, x, l, e)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K) : List<&2, String>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ka_e(sd, K, w, x, l, e)) == True{} : Bool})

def kafter_ok source · line 66 · raw

@+sd:Nat -> @+K:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+w:U32 -> @+x:U32 -> @+l:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd))) == True{} : Bool} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K) == True{} : Bool} -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.kafter(sd, K, w, x, l)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K) : List<&2, String>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.kafter(sd, K, w, x, l)) == True{} : Bool})

def fd_of source · line 71 · raw

@r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @tab:Array<U32> -> @ks:Array<String> -> @key:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Found

def FindOK source · line 78 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+kl0:List<&2, String> -> @+key:String -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Res -> @fd:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.Found -> Type

def from_v source · line 82 · raw

@+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} -> {U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)) == i : U32}

a U32 is the U32 of its value

def dec_ix source · line 86 · raw

@+tb:List<&2, U32> -> @+kl:List<&2, String> -> @+i:Nat -> @+a:Nat -> @+b:Nat -> @+ea:{a == Nat.double(i) : Nat} -> @+eb:{b == 1n+Nat.double(i) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, b), kl, U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(tb, a), 0)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec(tb, kl, i) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk}

bucket i read through the word/link indices 2i, 2i + 1

def fm0 source · line 91 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+kl0:List<&2, String> -> @+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} -> @+K1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hs1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K1) == kl0 : List<&2, String>} -> @+pk1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K1) == True{} : Bool} -> @+ms:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS -> FindOK(tabT, sd, kl0, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, 0n, ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.find(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.step_of(ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K1), key), mask, w, i))

def fm1 source · line 100 · raw

@+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sd:Nat -> @+kl0:List<&2, String> -> @+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} -> @+K1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hs1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K1) == kl0 : List<&2, String>} -> @+pk1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K1) == 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:FindOK(tabT, sd, kl0, key, 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/src/containers/hash_table.find(p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask), key, w), mask, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bnext(i, mask))) -> @+ms:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS -> FindOK(tabT, sd, kl0, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, bs, n, 1n+p, ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.find(1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.step_of(ms, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K1), key), mask, w, i))

def mod_lt source · line 109 · raw

@+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+x:Nat -> {Nat.is_lt(Nat.mod(x, n), n) == True{} : Bool}

def find_ok source · line 119 · 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 -> @+hsd:{Nat.is_lt(sd, 32n) == True{} : Bool} -> @+kl0:List<&2, String> -> @+key:String -> @+hkey:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : 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} -> @+K:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<String> -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(String, K) == kl0 : List<&2, String>} -> @+pk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(String, sd, K) == True{} : Bool} -> FindOK(tabT, sd, kl0, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.pf(key, 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(key, 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/src/containers/hash_table.find(f, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tabT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(String, K), i, key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.msk(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key), i))

THEOREM: the implementation's long-key probe loop is the model loop B.pf on the decoded buckets (a table of 2^k buckets, word/link pairs in tabT, the stored keys unchanged).