law xinvolution

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I

126law xinvolution:
127  for +key: List<&2, U32>
128  for +counter: U32
129  for +nonce: List<&2, U32>
130  for +plaintext: List<&2, U32>
131  {I.xencrypt_unchecked(key, counter, nonce, I.xencrypt_unchecked(key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}