law aes_fips197_c1

bend-osdev-crypto@0.1.0.0 · LAWS.bend:365

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/aes.bend as X
import bend-osdev-crc@0.1.0.0/crc.bend as C
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-crypto@0.1.0.0/block.bend as Bk
import bend-osdev-crypto@0.1.0.0/inst_cm.bend as CM
import bend-osdev-crypto@0.1.0.0/inst_aes.bend as A

365# FIPS 197 Appendix C.1 through the block-cipher interface: AES-128, its
366# encryption key schedule then one block of bytes (with CrAes.key, which
367# computes the decryption round keys too, the vector checks but runs past
368# --verdict's kernel; check.bend runs it both ways)
369law aes_fips197_c1:
370  {Bk.CrBlockCipher.encrypt_with(~X.CmAesKey, ~M.CmBlock, ~A.CrAes.key_enc, ~X.CmAes.encrypt, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255])) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, Cr.CrError, B.Octets>}