law byte_shrn

lawful-words@0.1.0.0 · LAWS.bend:415

import Base
import lawful-words@0.1.0.0/defs.bend as D

415# Shifting by whole bytes moves bytes.
416law byte_shrn:
417  for w: U32
418  for s: Nat
419  for j: Nat
420  {D.byte(U32.shrn(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.add(j, s)) : U32}