law open128_same
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/proof.bend:160
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
160law open128_same:
161 for +key: List<&2, U32>
162 for +nonce: List<&2, U32>
163 for +aad: List<&2, U32>
164 for +m: Maybe<&2, List<&2, U32>>
165 {Laws.open128(key, nonce, aad, m) == API.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}