law u32_and_65535

bend-osdev-u32@0.1.0.0 · LAWS.bend:625

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

625# the 16-bit mask, written as Base reads it (65535 = U32Word.mask(32, 16))
626law u32_and_65535:
627  for +a: U32
628  {U32.to_nat(U32.and(a, 65535)) == U.U32Nat.low(16n, U32.to_nat(a)) : Nat}