law part2

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

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

190law part2:
191  for +w: U32
192  {R.word(R.byte(w,0n),R.byte(w,1n),0,0) == U32.and(65535,w) : U32}