law words_pad

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

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

250law words_pad:
251  for +ws: List<&2,U32>
252  for +i: Nat
253  for +len: Nat
254  {R.words(R.pad(R.serialize(ws),i,len)) == masked(ws,i,len) : List<&2,U32>}