law u32_and_mask

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

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

618law u32_and_mask:
619  for +a: U32
620  for +m: U32
621  for +k: Nat
622  for h: {1n+U32.to_nat(m) == U.U32Nat.dbl(k, 1n) : Nat}
623  {U32.to_nat(U32.and(a, m)) == U.U32Nat.low(k, U32.to_nat(a)) : Nat}