Bytes.words_serialize: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend as Bytes
Lines 228-231 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend&start_line=228&end_line=231

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

# Whole blocks: reassembling the serialized words gives the words back.
law words_serialize:
  for +ws: List<&2,U32>
  {R.words(R.serialize(ws)) == ws : List<&2,U32>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend&name=full
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=serialize
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=words