~/bend-docscommunity

proofs/containers/hash_table/decide.bend checks

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

13 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/u32alg.bend as A
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ./strings.bend as STR
import ./words.bend as WR
import ./keys.bend as K
import ./table.bend as TB
import ./buckets.bend as B
import ./step.bend as SP
import ../../lib/u32.bend as UW

Definitions

def not_false source · line 19 · raw

{Bool.not(False{}) == True{} : Bool}

def masked_small source · line 23 · raw

@+x:U32 -> {U32.is_lt(U32.and(x, 2147483647), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool}

a short word masked is a code below 2^31

def lword_long source · line 30 · raw

@+key:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key)) == False{} : Bool}

def short_ne_long source · line 34 · raw

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

a one-character key below 2^31 is not a long-probed key

def kinds_ne source · line 43 · raw

@+x:U32 -> @+w:U32 -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == True{} : Bool} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(w) == False{} : Bool} -> @+s:Bool -> @+hs:{U32.is_eq(x, w) == s : Bool} -> {s == False{} : Bool}

words of different kinds differ

def dl_short source · line 51 · raw

@+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : Bool} -> @+x:U32 -> @+l:U32 -> @+k:String -> @+hxs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(x) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ld_w(key, l, k, U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.BF{x, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.keyof_c(x, k, True{})}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def le_false source · line 58 · raw

@+k:String -> @+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : Bool} -> @+x:U32 -> @+hinv:{x == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(k) : U32} -> @+hs:{U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key)) == False{} : Bool} -> @+e:Bool -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k, key) == e : Bool} -> {e == False{} : Bool}

a long bucket whose word is not the probed word does not hold the key

def dl_long source · line 66 · raw

@+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : Bool} -> @+x:U32 -> @+l:U32 -> @+k:String -> @+hinv:{x == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.kword(k) : U32} -> @+s:Bool -> @+hs:{U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key)) == s : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ld_w(key, l, k, s) == Bool.pick(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(k, key), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MHit{l}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MNext{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def dsh source · line 73 · raw

@+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : 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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ld_w(key, l, k, U32.is_eq(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 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 dec_e source · line 81 · raw

@+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : Bool} -> @+x:U32 -> @+l:U32 -> @+ks: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(ks, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))))) == True{} : Bool} -> @+e:Bool -> @+he:{U32.is_eq(x, 0) == e : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ld_e(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key), x, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(ks, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))), e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(x, l, ks, e)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

def decide source · line 90 · raw

@+key:String -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.shortk(key) == False{} : Bool} -> @+x:U32 -> @+l:U32 -> @+ks: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(ks, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l))))))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.ldec(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key), x, l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.nths(ks, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(l)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.mstep(key, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.dec_c(x, l, ks, U32.is_eq(x, 0))) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.MS}

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