law open256_same
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/proof.bend:199
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/proof.bend as Proof
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend as API
199law open256_same:
200 for +key: List<&2, U32>
201 for +nonce: List<&2, U32>
202 for +aad: List<&2, U32>
203 for +m: Maybe<&2, List<&2, U32>>
204 {Laws.open256(key, nonce, aad, m) == API.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}