spec/math/hash.bend

bend-collections-laws-math@1.0.0.0 · 17 lines · 2 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as N
3import bend-collections-laws-math@1.0.0.0/src/math/hash.bend as H
4
5# Specification of src/math/hash.bend: every bucket index a hash can take
6# lies inside its table.
7#
8#   function   clauses                  proved in
9#   bucket     Bucket.le, Bucket.lt     proofs/math/proof.bend (hash_bucket_le/lt)
10
11# bucket(w, mask) never exceeds the mask
12def Bucket.le(+w: U32, +mask: U32) -> Type:
13  {Nat.is_le(U32.to_nat(H.bucket(w, mask)), U32.to_nat(mask)) == True{} : Bool}
14
15# with mask = 2^k - 1 (the low k bits) the bucket indexes a table of 2^k
16def Bucket.lt(+w: U32, +k: Nat, +mask: U32, +hm: {mask == U32{N.mask(32n, k)} : U32}) -> Type:
17  {Nat.is_lt(U32.to_nat(H.bucket(w, mask)), N.scale_binary(k, 1n)) == True{} : Bool}