1	# Laws about AES (aes.bend): its decryption undoes its encryption for
2	# every key and block, and FIPS 197's C.1 vector.
3	import Base
4	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
5	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
6	import ./aes.bend as X
7	
8	# AES (aes.bend): decryption undoes encryption, for every key (every value
9	# of CmAesKey, whatever its number of rounds and round keys: AES-128, AES-192
10	# and AES-256 among them) and every block
11	law aes_round_trip:
12	  for k: X.CmAesKey
13	  for +b: M.CmBlock
14	  {X.CmAes.decrypt(k, X.CmAes.encrypt(k, b)) == b : M.CmBlock}
15	
16	# Vectors: the specifications' own test values, proved by computation. The
17	# checker evaluates AES slowly and keeps what it evaluates, so only these fit
18	# in its memory; every other vector of the four specifications (all of SP
19	# 800-38A F.2.1, F.2.2, F.2.5 and F.2.6; IEEE 1619 vectors 2 and 15 to 18;
20	# RFC 3610 packets 1 to 3; RFC 4493 examples 2 to 4; and every decryption)
21	# runs compiled in check.bend.
22	
23	# FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block
24	law aes128_fips197_c1:
25	  {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key128(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, M.CmError, B.Octets>}