law xencrypt_correct
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/xchacha.bend:53
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/xchacha.bend as Xchacha
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
53law xencrypt_correct:
54 for +kb: List<&2, U32>
55 for +c: U32
56 for +nb: List<&2, U32>
57 for +pt: List<&2, U32>
58 {I.xencrypt_unchecked(kb, c, nb, pt) == R.xencrypt(kb, c, nb, pt) : List<&2, U32>}