law expand_ok
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/cipher.bend:349
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
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
349law expand_ok:
350 for +nk: Nat
351 for +nr: Nat
352 for +key: List<&2, U32>
353 {I.expand(nk, nr, key) == I.round_keys(S.key_expansion(nk, nr, key)) : List<&2, T.State>}