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