1	import Base
2	import ../lib/numeric.bend as N
3	import ../../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
12	def 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
16	def 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}