1	import Base
2	import ../libs/AES256GCMCore.bend as Core
3	import ./AES_NistKeyScheduleProof.bend as Key
4	
5	# Concrete stages of the NIST J0 block, checked by the independent kernel.
6	def block() -> List<&2, U32>:
7	    [202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136, 0, 0, 0, 1]
8	
9	def state_0() -> List<&2, U32>:
10	    [52, 1, 83, 44, 124, 171, 168, 177, 179, 160, 119, 28, 103, 48, 131, 9]
11	
12	def state_1() -> List<&2, U32>:
13	    [156, 38, 97, 47, 0, 240, 211, 194, 158, 235, 100, 65, 172, 140, 90, 1]
14	
15	def state_2() -> List<&2, U32>:
16	    [236, 119, 137, 89, 48, 16, 120, 211, 96, 208, 224, 67, 169, 97, 146, 179]
17	
18	def state_3() -> List<&2, U32>:
19	    [69, 154, 167, 162, 145, 21, 18, 184, 176, 0, 241, 125, 152, 86, 217, 137]
20	
21	def state_4() -> List<&2, U32>:
22	    [0, 167, 253, 31, 255, 112, 13, 177, 113, 88, 180, 147, 66, 240, 37, 93]
23	
24	def state_5() -> List<&2, U32>:
25	    [14, 37, 120, 128, 26, 140, 120, 147, 217, 218, 212, 88, 167, 213, 24, 51]
26	
27	def state_6() -> List<&2, U32>:
28	    [73, 102, 200, 157, 169, 97, 250, 71, 60, 50, 198, 22, 55, 247, 26, 229]
29	
30	def state_7() -> List<&2, U32>:
31	    [102, 20, 1, 111, 4, 13, 186, 228, 138, 205, 84, 191, 183, 70, 127, 8]
32	
33	def state_8() -> List<&2, U32>:
34	    [65, 166, 229, 84, 99, 106, 0, 126, 14, 25, 152, 116, 177, 23, 227, 170]
35	
36	def state_9() -> List<&2, U32>:
37	    [36, 77, 13, 105, 78, 204, 117, 212, 46, 49, 3, 55, 243, 223, 61, 19]
38	
39	def state_10() -> List<&2, U32>:
40	    [183, 212, 41, 223, 232, 146, 128, 96, 119, 186, 11, 144, 1, 46, 232, 8]
41	
42	def state_11() -> List<&2, U32>:
43	    [197, 183, 64, 59, 156, 26, 67, 102, 38, 11, 185, 182, 153, 16, 232, 116]
44	
45	def state_12() -> List<&2, U32>:
46	    [62, 65, 245, 143, 201, 180, 35, 187, 211, 190, 117, 16, 8, 241, 60, 255]
47	
48	def state_13() -> List<&2, U32>:
49	    [31, 209, 218, 183, 4, 93, 109, 1, 29, 206, 52, 97, 35, 119, 70, 140]
50	
51	def result() -> List<&2, U32>:
52	    [253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126]
53	
54	def initial_matches() ->
55	    {Core.aes_add_key(block(), Key.words_60(), 0n) == state_0() : List<&2, U32>}:
56	    {==}
57	
58	def round_1_matches() ->
59	    {Core.aes_middle_round(state_0(), Key.words_60(), 1n) == state_1() : List<&2, U32>}:
60	    {==}
61	
62	def round_2_matches() ->
63	    {Core.aes_middle_round(state_1(), Key.words_60(), 2n) == state_2() : List<&2, U32>}:
64	    {==}
65	
66	def round_3_matches() ->
67	    {Core.aes_middle_round(state_2(), Key.words_60(), 3n) == state_3() : List<&2, U32>}:
68	    {==}
69	
70	def round_4_matches() ->
71	    {Core.aes_middle_round(state_3(), Key.words_60(), 4n) == state_4() : List<&2, U32>}:
72	    {==}
73	
74	def round_5_matches() ->
75	    {Core.aes_middle_round(state_4(), Key.words_60(), 5n) == state_5() : List<&2, U32>}:
76	    {==}
77	
78	def round_6_matches() ->
79	    {Core.aes_middle_round(state_5(), Key.words_60(), 6n) == state_6() : List<&2, U32>}:
80	    {==}
81	
82	def round_7_matches() ->
83	    {Core.aes_middle_round(state_6(), Key.words_60(), 7n) == state_7() : List<&2, U32>}:
84	    {==}
85	
86	def round_8_matches() ->
87	    {Core.aes_middle_round(state_7(), Key.words_60(), 8n) == state_8() : List<&2, U32>}:
88	    {==}
89	
90	def round_9_matches() ->
91	    {Core.aes_middle_round(state_8(), Key.words_60(), 9n) == state_9() : List<&2, U32>}:
92	    {==}
93	
94	def round_10_matches() ->
95	    {Core.aes_middle_round(state_9(), Key.words_60(), 10n) == state_10() : List<&2, U32>}:
96	    {==}
97	
98	def round_11_matches() ->
99	    {Core.aes_middle_round(state_10(), Key.words_60(), 11n) == state_11() : List<&2, U32>}:
100	    {==}
101	
102	def round_12_matches() ->
103	    {Core.aes_middle_round(state_11(), Key.words_60(), 12n) == state_12() : List<&2, U32>}:
104	    {==}
105	
106	def round_13_matches() ->
107	    {Core.aes_middle_round(state_12(), Key.words_60(), 13n) == state_13() : List<&2, U32>}:
108	    {==}
109	
110	def final_matches() ->
111	    {Core.aes_final_round(state_13(), Key.words_60()) == result() : List<&2, U32>}:
112	    {==}