law xopen_eq

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

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

171law xopen_eq:
172  for +key: List<&2, U32>
173  for +nonce: List<&2, U32>
174  for +aad: List<&2, U32>
175  for +data: List<&2, U32>
176  {I.xopen(key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}