~/bend-docscommunity

proofs/containers/hash_table/words.bend checks

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

3 imports
import Base
import ../../lib/logic.bend as L
import ../../../src/containers/hash_table.bend as H

Definitions

def top source · line 10 · raw

@+p:Nat -> Word(1n+p)

def low source · line 17 · raw

@+p:Nat -> Word(1n+p)

def one source · line 24 · raw

@+p:Nat -> Word(2n+p)

def topb source · line 28 · raw

@+p:Nat -> @w:Word(1n+p) -> Bool

the top bit

def tag_top source · line 35 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag == U32{top(31n)} : U32}

def low_lit source · line 38 · raw

{2147483647 == U32{low(31n)} : U32}

def one_lit source · line 41 · raw

{1 == U32{one(30n)} : U32}

def zero_lit source · line 44 · raw

{0 == U32{Word.zero(32n)} : U32}

def ge_fin_false source · line 49 · raw

@+c:Cmp -> @+b:Bool -> {Cmp.is_ge(Word.cmp.fin(b, False{}, c)) == Cmp.is_ge(c) : Bool}

def ge_top_leaf source · line 60 · raw

@+b:Bool -> {Cmp.is_ge(Word.cmp(1n, WCon{b, WNil{}}, top(0n))) == b : Bool}

def ge_top source · line 68 · raw

@+p:Nat -> @+w:Word(1n+p) -> {Cmp.is_ge(Word.cmp(1n+p, w, top(p))) == topb(p, w) : Bool}

w >= 2^p is its top bit

def or_true source · line 77 · raw

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

def or_false source · line 84 · raw

@+b:Bool -> {Bool.or(b, False{}) == b : Bool}

def and_true source · line 91 · raw

@+b:Bool -> {Bool.and(b, True{}) == b : Bool}

def and_false source · line 98 · raw

@+b:Bool -> {Bool.and(b, False{}) == False{} : Bool}

def topb_or_top source · line 105 · raw

@+p:Nat -> @+x:Word(1n+p) -> {topb(p, Word.or(1n+p, x, top(p))) == True{} : Bool}

def topb_and_low source · line 112 · raw

@+p:Nat -> @+x:Word(1n+p) -> {topb(p, Word.and(1n+p, x, low(p))) == False{} : Bool}

def topb_or source · line 119 · raw

@+p:Nat -> @+x:Word(1n+p) -> @+y:Word(1n+p) -> {topb(p, Word.or(1n+p, x, y)) == Bool.or(topb(p, x), topb(p, y)) : Bool}

def topb_zero source · line 126 · raw

@+p:Nat -> {topb(p, Word.zero(1n+p)) == False{} : Bool}

def topb_one source · line 133 · raw

@+p:Nat -> {topb(1n+p, one(p)) == False{} : Bool}

def and_low_or_top source · line 137 · raw

@+p:Nat -> @+x:Word(1n+p) -> @+h:{topb(p, x) == False{} : Bool} -> {Word.and(1n+p, Word.or(1n+p, x, top(p)), low(p)) == x : Word(1n+p)}

clearing the top bit of x with the top bit set gives back x without it

def eq_fin_false source · line 150 · raw

@+b:Bool -> @+c:Cmp -> @+h:{Cmp.is_eq(c) == False{} : Bool} -> {Cmp.is_eq(Word.cmp.fin(b, False{}, c)) == False{} : Bool}

def top_nonzero_g source · line 159 · raw

@+p:Nat -> @+w:Word(1n+p) -> @+h:{topb(p, w) == True{} : Bool} -> {Cmp.is_eq(Word.cmp(1n+p, w, Word.zero(1n+p))) == False{} : Bool}

def fin_tf source · line 168 · raw

@+c:Cmp -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, c)) == False{} : Bool}

def bit0_nonzero source · line 177 · raw

@+p:Nat -> @+t:Word(p) -> {Cmp.is_eq(Word.cmp(1n+p, WCon{True{}, t}, Word.zero(1n+p))) == False{} : Bool}

def lt_ge source · line 182 · raw

@+c:Cmp -> {Cmp.is_lt(c) == Bool.not(Cmp.is_ge(c)) : Bool}

def not_true source · line 191 · raw

@+b:Bool -> @+h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def small_top source · line 199 · raw

@+cw:Word(32n) -> @+h:{U32.is_lt(U32{cw}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> {topb(31n, cw) == False{} : Bool}

a code below 2^31 has its top bit clear

def is_short_top source · line 203 · raw

@+w:Word(32n) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(U32{w}) == topb(31n, w) : Bool}

def short_is_short source · line 206 · raw

@+c:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c)) == True{} : Bool}

def short_nonzero source · line 211 · raw

@+c:U32 -> {U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c), 0) == False{} : Bool}

def short_back source · line 217 · raw

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

masking a short word gives back its character code

def short_inj source · line 222 · raw

@+a:U32 -> @+b:U32 -> @+ha:{U32.is_lt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+hb:{U32.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(b) : U32} -> {a == b : U32}

def lw_word source · line 226 · raw

@+hw:Word(32n) -> Word(32n)

def long_top source · line 229 · raw

@+hw:Word(32n) -> {topb(31n, lw_word(hw)) == False{} : Bool}

def long_is_long source · line 235 · raw

@+h:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.is_short(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.long_word(h)) == False{} : Bool}

def or_bit0 source · line 240 · raw

@+p:Nat -> @+b:Bool -> @+t:Word(p) -> {Word.or(1n+p, WCon{b, t}, WCon{True{}, Word.zero(p)}) == WCon{True{}, Word.or(p, t, Word.zero(p))} : Word(1n+p)}

def long_nonzero source · line 243 · raw

@+h:U32 -> {U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.long_word(h), 0) == False{} : Bool}

def long_not_short source · line 252 · raw

@+h:U32 -> @+c:U32 -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.long_word(h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c) : U32} -> Empty

a long word is never a short word

def or_and_low_top source · line 259 · raw

@+p:Nat -> @+x:Word(1n+p) -> @+h:{topb(p, x) == True{} : Bool} -> {Word.or(1n+p, Word.and(1n+p, x, low(p)), top(p)) == x : Word(1n+p)}

a word with its top bit set is its low bits with the top bit set

def short_eta source · line 269 · raw

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