law xor_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:126

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

126law xor_append:
127  for +bs: List<&2, U32>
128  for +xs: List<&2, U32>
129  for +k: List<&2, U32>
130  {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>}