proofs/math/hash/hash.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as Hash

7 imports

import Base
import ../../../src/math/hash.bend as HS
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD

Definitions

def bit_and_le source · line 14 · raw

@+a:Bool -> @+b:Bool -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(Bool.and(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b)) == True{} : Bool}

def add_le source · line 25 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_le(a, b) == True{} : Bool} -> @+h2:{Nat.is_le(c, d) == True{} : Bool} -> {Nat.is_le(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}

def and_le source · line 31 · raw

@+n:Nat -> @+x:Word(n) -> @+m:Word(n) -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(n, Word.and(n, x, m)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(n, m)) == True{} : Bool}

masking never exceeds the mask

def and_le32 source · line 38 · raw

@+x:U32 -> @+m:U32 -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, m)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(m)) == True{} : Bool}

def bucket_le source · line 46 · raw

@+w:U32 -> @+mask:U32 -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/hash.bucket(w, mask)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(mask)) == True{} : Bool}

THEOREM: a bucket never exceeds the mask.

def and_mask_lt source · line 49 · raw

@+x:U32 -> @+k:Nat -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(U32.and(x, U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)})), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, 1n)) == True{} : Bool}

def bucket_ltw source · line 55 · raw

@+w:U32 -> @+k:Nat -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/hash.bucket(w, U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)})), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, 1n)) == True{} : Bool}

def bucket_lt source · line 59 · raw

@+w:U32 -> @+k:Nat -> @+mask:U32 -> @+hm:{mask == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, k)} : U32} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/hash.bucket(w, mask)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, 1n)) == True{} : Bool}

THEOREM: with mask = 2^k - 1 (k low bits) the bucket indexes a table of 2^k.