LAWS.aes_fips197_c1: law of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
Lines 365-370 of bend-osdev-crypto@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&start_line=365&end_line=370

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

# FIPS 197 Appendix C.1 through the block-cipher interface: AES-128, its
# encryption key schedule then one block of bytes (with CrAes.key, which
# computes the decryption round keys too, the vector checks but runs past
# --verdict's kernel; check.bend runs it both ways)
law aes_fips197_c1:
  {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>}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/aes.bend&name=CmAes.encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/aes.bend&name=CmAesKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/block.bend&name=CrBlockCipher.encrypt_with
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/crypto.bend&name=CrError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/inst_aes.bend&name=CrAes.key_enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/inst_cm.bend&name=CrBlk128.of_octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/inst_cm.bend&name=CrBlk128.to_octets