law cipher_ok

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

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

210law cipher_ok:
211  for +nr: Nat
212  for +s: T.State
213  for +w: List<&2, T.Quad>
214  {I.cipher(nr, s, I.round_keys(w)) == S.cipher(nr, s, w) : T.State}