1	import Base
2	import ../libs/AES256GCMCore.bend as Core
3	import ./AES_NistKeyScheduleProof.bend as Key
4	
5	# Candidate NIST h block stages. Only kernel acceptance certifies them.
6	
7	def block() -> List<&2, U32>:
8	    [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
9	
10	def state_0() -> List<&2, U32>:
11	    [254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8]
12	
13	def state_1() -> List<&2, U32>:
14	    [7, 123, 169, 26, 171, 69, 39, 160, 155, 224, 52, 233, 225, 49, 115, 65]
15	
16	def state_2() -> List<&2, U32>:
17	    [67, 161, 220, 40, 172, 229, 209, 156, 89, 19, 112, 108, 45, 199, 222, 85]
18	
19	def state_3() -> List<&2, U32>:
20	    [226, 50, 179, 95, 26, 147, 52, 166, 100, 146, 82, 51, 20, 31, 212, 69]
21	
22	def state_4() -> List<&2, U32>:
23	    [11, 113, 151, 179, 69, 121, 252, 116, 200, 5, 219, 180, 122, 53, 255, 176]
24	
25	def state_5() -> List<&2, U32>:
26	    [51, 79, 89, 198, 109, 32, 191, 114, 231, 128, 200, 247, 124, 62, 44, 8]
27	
28	def state_6() -> List<&2, U32>:
29	    [164, 187, 38, 171, 158, 214, 214, 74, 70, 239, 135, 11, 207, 19, 152, 58]
30	
31	def state_7() -> List<&2, U32>:
32	    [83, 243, 220, 241, 104, 61, 9, 247, 165, 1, 84, 145, 80, 229, 175, 226]
33	
34	def state_8() -> List<&2, U32>:
35	    [69, 43, 40, 150, 236, 171, 32, 196, 155, 104, 143, 135, 32, 149, 159, 180]
36	
37	def state_9() -> List<&2, U32>:
38	    [81, 30, 137, 82, 246, 53, 149, 171, 60, 226, 141, 31, 56, 243, 176, 130]
39	
40	def state_10() -> List<&2, U32>:
41	    [86, 150, 237, 202, 234, 227, 57, 161, 44, 231, 220, 82, 80, 133, 232, 132]
42	
43	def state_11() -> List<&2, U32>:
44	    [213, 144, 246, 62, 238, 44, 26, 237, 214, 49, 93, 168, 11, 142, 26, 194]
45	
46	def state_12() -> List<&2, U32>:
47	    [172, 192, 117, 199, 120, 154, 187, 207, 146, 185, 155, 71, 237, 226, 212, 217]
48	
49	def state_13() -> List<&2, U32>:
50	    [172, 59, 160, 40, 195, 156, 109, 136, 31, 120, 114, 152, 4, 69, 39, 2]
51	
52	def result() -> List<&2, U32>:
53	    [172, 190, 242, 5, 121, 180, 184, 235, 206, 136, 155, 172, 135, 50, 218, 215]
54	
55	def initial_matches() ->
56	    {Core.aes_add_key(block(), Key.words_60(), 0n) == state_0() : List<&2, U32>}:
57	    {==}
58	
59	def round_1_matches() ->
60	    {Core.aes_middle_round(state_0(), Key.words_60(), 1n) == state_1() : List<&2, U32>}:
61	    {==}
62	
63	def round_2_matches() ->
64	    {Core.aes_middle_round(state_1(), Key.words_60(), 2n) == state_2() : List<&2, U32>}:
65	    {==}
66	
67	def round_3_matches() ->
68	    {Core.aes_middle_round(state_2(), Key.words_60(), 3n) == state_3() : List<&2, U32>}:
69	    {==}
70	
71	def round_4_matches() ->
72	    {Core.aes_middle_round(state_3(), Key.words_60(), 4n) == state_4() : List<&2, U32>}:
73	    {==}
74	
75	def round_5_matches() ->
76	    {Core.aes_middle_round(state_4(), Key.words_60(), 5n) == state_5() : List<&2, U32>}:
77	    {==}
78	
79	def round_6_matches() ->
80	    {Core.aes_middle_round(state_5(), Key.words_60(), 6n) == state_6() : List<&2, U32>}:
81	    {==}
82	
83	def round_7_matches() ->
84	    {Core.aes_middle_round(state_6(), Key.words_60(), 7n) == state_7() : List<&2, U32>}:
85	    {==}
86	
87	def round_8_matches() ->
88	    {Core.aes_middle_round(state_7(), Key.words_60(), 8n) == state_8() : List<&2, U32>}:
89	    {==}
90	
91	def round_9_matches() ->
92	    {Core.aes_middle_round(state_8(), Key.words_60(), 9n) == state_9() : List<&2, U32>}:
93	    {==}
94	
95	def round_10_matches() ->
96	    {Core.aes_middle_round(state_9(), Key.words_60(), 10n) == state_10() : List<&2, U32>}:
97	    {==}
98	
99	def round_11_matches() ->
100	    {Core.aes_middle_round(state_10(), Key.words_60(), 11n) == state_11() : List<&2, U32>}:
101	    {==}
102	
103	def round_12_matches() ->
104	    {Core.aes_middle_round(state_11(), Key.words_60(), 12n) == state_12() : List<&2, U32>}:
105	    {==}
106	
107	def round_13_matches() ->
108	    {Core.aes_middle_round(state_12(), Key.words_60(), 13n) == state_13() : List<&2, U32>}:
109	    {==}
110	
111	def final_matches() ->
112	    {Core.aes_final_round(state_13(), Key.words_60()) == result() : List<&2, U32>}:
113	    {==}