def mask_word

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:260

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

260def mask_word(+x: U32, +y: U32, +d: Nat, +hy: {U32.to_nat(y) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(U32.to_nat(x), SC.pow2(d)) == True{} : Bool}) -> {U32.and(x, y) == x : U32}:
261  match x y:
262    case U32{+wx} U32{+wy}:
263      Equal.cong(Word(32n), U32, w => U32{w}, Word.and(32n, wx, wy), wx,
264        and_low(32n, d, wx, wy,
265          Equal.trans(Nat, S.unsigned(32n, wy), U32.to_nat(U32{wy}), Nat.sub(SC.pow2(d), 1n), Equal.sym(Nat, U32.to_nat(U32{wy}), S.unsigned(32n, wy), to_nat_word(wy)), hy),
266          mask_hx(wx, d, hx)))