law encrypt_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/cipher.bend:360

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S

360# The implementation's cipher with its expanded key is FIPS 197's Cipher
361# with KeyExpansion, for every Nk, Nr, key and block.
362law encrypt_ok:
363  for +nk: Nat
364  for +nr: Nat
365  for +key: List<&2, U32>
366  for +s: T.State
367  {I.encrypt(nk, nr, key, s) == S.encrypt(nk, nr, key, s) : T.State}