law part1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/bytes.bend:199

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as R

199law part1:
200  for +w: U32
201  {R.word(R.byte(w,0n),0,0,0) == U32.and(255,w) : U32}