Involution.xor_append: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as Involution
Lines 126-130 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend&start_line=126&end_line=130

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

law xor_append:
  for +bs: List<&2, U32>
  for +xs: List<&2, U32>
  for +k: List<&2, U32>
  {R.xor_bytes(xs, List.append(&2, U32, bs, k)) == List.append(&2, U32, R.xor_bytes(R.prefix(List.length(&2, U32, bs), xs), bs), R.xor_bytes(R.suffix(List.length(&2, U32, bs), xs), k)) : List<&2, U32>}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend&name=prefix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend&name=xor_bytes