law part3

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

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

181law part3:
182  for +w: U32
183  {R.word(R.byte(w,0n),R.byte(w,1n),R.byte(w,2n),0) == U32.and(16777215,w) : U32}