proofs/math/hash/hash.bend

bend-collections-laws-crypto@1.0.0.0 · 60 lines · 8 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/math/hash.bend as HS
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
7import bend-collections-laws-crypto@1.0.0.0/proofs/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
14def 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
25def 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
31def 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
38def 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.
46def 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
49def 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
55def 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.
59def 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))