1	import Base
2	import ../../../src/math/hash.bend as HS
3	import ../../lib/lemmas/spec/numeric.bend as S
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/word.bend as WD
7	import ../../lib/u32div.bend as UD
8	
9	# src/math/hash.bend: every bucket index lies inside the table.
10	#   bucket_le: bucket(w, mask) <= mask for every mask
11	#   bucket_lt: bucket(w, mask) < 2^k when mask is the low k bits (a table of
12	#              2^k buckets)
13	
14	def bit_and_le(+a: Bool, +b: Bool) -> {Nat.is_le(S.bit_value(Bool.and(a, b)), S.bit_value(b)) == True{} : Bool}:
15	  match a b:
16	    case True{} True{}:
17	      {==}
18	    case True{} False{}:
19	      {==}
20	    case False{} True{}:
21	      {==}
22	    case False{} False{}:
23	      {==}
24	
25	def add_le(+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}:
26	  +l1 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(c, b)) == True{} : Bool}, Nat.add(c, a), Nat.add(a, c), N.add_comm(c, a), N.le_add_left(a, b, c, h1))
27	  +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(a, c), z) == True{} : Bool}, Nat.add(c, b), Nat.add(b, c), N.add_comm(c, b), l1)
28	  N.le_trans(Nat.add(a, c), Nat.add(b, c), Nat.add(b, d), l2, N.le_add_left(c, d, b, h2))
29	
30	# masking never exceeds the mask
31	def and_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.and(n, x, m)), WD.uw(n, m)) == True{} : Bool}:
32	  match n x m:
33	    case 0n WNil{} WNil{}:
34	      {==}
35	    case 1n+p WCon{a, t1} WCon{b, t2}:
36	      add_le(S.bit_value(Bool.and(a, b)), S.bit_value(b), Nat.double(WD.uw(p, Word.and(p, t1, t2))), Nat.double(WD.uw(p, t2)), bit_and_le(a, b), N.double_le(WD.uw(p, Word.and(p, t1, t2)), WD.uw(p, t2), and_le(p, t1, t2)))
37	
38	def and_le32(+x: U32, +m: U32) -> {Nat.is_le(UD.v(U32.and(x, m)), UD.v(m)) == True{} : Bool}:
39	  match x m:
40	    case U32{+a} U32{+b}:
41	      %Equal.sym(Nat, UD.v(U32{Word.and(32n, a, b)}), WD.uw(32n, Word.and(32n, a, b)), UD.vw(Word.and(32n, a, b))) : {Nat.is_le(_, UD.v(U32{b})) == True{} : Bool}
42	      %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.is_le(WD.uw(32n, Word.and(32n, a, b)), _) == True{} : Bool}
43	      and_le(32n, a, b)
44	
45	# THEOREM: a bucket never exceeds the mask.
46	def bucket_le(+w: U32, +mask: U32) -> {Nat.is_le(UD.v(HS.bucket(w, mask)), UD.v(mask)) == True{} : Bool}:
47	  and_le32(U32.xor(U32.mul(w, HS.phi32()), U32.shrn(U32.mul(w, HS.phi32()), 16n)), mask)
48	
49	def and_mask_lt(+x: U32, +k: Nat) -> {Nat.is_lt(UD.v(U32.and(x, U32{WD.mask(32n, k)})), WD.sc(k, 1n)) == True{} : Bool}:
50	  match x:
51	    case U32{+xw}:
52	      %Equal.sym(Nat, UD.v(U32{Word.and(32n, xw, WD.mask(32n, k))}), WD.uw(32n, Word.and(32n, xw, WD.mask(32n, k))), UD.vw(Word.and(32n, xw, WD.mask(32n, k)))) : {Nat.is_lt(_, WD.sc(k, 1n)) == True{} : Bool}
53	      WD.mask_lt(32n, k, 1n, {==}, xw)
54	
55	def bucket_ltw(+w: U32, +k: Nat) -> {Nat.is_lt(UD.v(HS.bucket(w, U32{WD.mask(32n, k)})), WD.sc(k, 1n)) == True{} : Bool}:
56	  and_mask_lt(U32.xor(U32.mul(w, HS.phi32()), U32.shrn(U32.mul(w, HS.phi32()), 16n)), k)
57	
58	# THEOREM: with mask = 2^k - 1 (k low bits) the bucket indexes a table of 2^k.
59	def bucket_lt(+w: U32, +k: Nat, +mask: U32, +hm: {mask == U32{WD.mask(32n, k)} : U32}) -> {Nat.is_lt(UD.v(HS.bucket(w, mask)), WD.sc(k, 1n)) == True{} : Bool}:
60	  L.subst(U32, z => {Nat.is_lt(UD.v(HS.bucket(w, z)), WD.sc(k, 1n)) == True{} : Bool}, U32{WD.mask(32n, k)}, mask, Equal.sym(U32, mask, U32{WD.mask(32n, k)}, hm), bucket_ltw(w, k))