law to_nat_split

lawful-words@0.1.0.0 · LAWS.bend:231

import Base

231# A word splits into its high part (a >> k) and its low k bits (a & m).
232law to_nat_split:
233  for a: U32
234  for m: U32
235  for k: Nat
236  for h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
237  {U32.to_nat(a) == Nat.add(Nat.mul(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, k)), U32.to_nat(U32.and(a, m))) : Nat}