def bucket_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/hash/hash.bend:58

import Base
import bend-collections-laws-math@1.0.0.0/src/math/hash.bend as HS
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

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))