def and_mask_lt

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

import Base
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

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)