law xseal_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/chacha20poly1305.bend:157

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as R

157law xseal_eq:
158  for +key: List<&2, U32>
159  for +nonce: List<&2, U32>
160  for +aad: List<&2, U32>
161  for +pt: List<&2, U32>
162  {I.xseal(key, nonce, aad, pt) == R.xseal(key, nonce, aad, pt) : List<&2, U32>}