def and32_ltw

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:71

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD

71def and32_ltw(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: U32) -> {Nat.is_lt(UD.v(U32.and(x, U32{WD.mask(32n, k)})), WD.sc(k, one)) == True{} : Bool}:
72  match x:
73    case U32{+w}:
74      %Equal.sym(Nat, UD.v(U32{Word.and(32n, w, WD.mask(32n, k))}), WD.uw(32n, Word.and(32n, w, WD.mask(32n, k))), UD.vw(Word.and(32n, w, WD.mask(32n, k)))) : {Nat.is_lt(_, WD.sc(k, one)) == True{} : Bool}
75      WD.mask_lt(32n, k, one, h1, w)