proof/AES_NistKeyScheduleProof.bend
qasim-bend-kit@0.1.0.2 · 962 lines · 213 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_TraceProof.bend as Trace
4import qasim-bend-kit@0.1.0.2/proof/AES_TraceBridgeProof.bend as Bridge
5
6
7def key_bytes() -> List<&2, U32>:
8 [254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8, 254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8]
9
10def words_8() -> List<&2, U32>:
11 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520]
12
13def words_9() -> List<&2, U32>:
14 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975]
15
16def words_10() -> List<&2, U32>:
17 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779]
18
19def words_11() -> List<&2, U32>:
20 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095]
21
22def words_12() -> List<&2, U32>:
23 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935]
24
25def words_13() -> List<&2, U32>:
26 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994]
27
28def words_14() -> List<&2, U32>:
29 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062]
30
31def words_15() -> List<&2, U32>:
32 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218]
33
34def words_16() -> List<&2, U32>:
35 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754]
36
37def words_17() -> List<&2, U32>:
38 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712]
39
40def words_18() -> List<&2, U32>:
41 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347]
42
43def words_19() -> List<&2, U32>:
44 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756]
45
46def words_20() -> List<&2, U32>:
47 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251]
48
49def words_21() -> List<&2, U32>:
50 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097]
51
52def words_22() -> List<&2, U32>:
53 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207]
54
55def words_23() -> List<&2, U32>:
56 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765]
57
58def words_24() -> List<&2, U32>:
59 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719]
60
61def words_25() -> List<&2, U32>:
62 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298]
63
64def words_26() -> List<&2, U32>:
65 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417]
66
67def words_27() -> List<&2, U32>:
68 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589]
69
70def words_28() -> List<&2, U32>:
71 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710]
72
73def words_29() -> List<&2, U32>:
74 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568]
75
76def words_30() -> List<&2, U32>:
77 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951]
78
79def words_31() -> List<&2, U32>:
80 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442]
81
82def words_32() -> List<&2, U32>:
83 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749]
84
85def words_33() -> List<&2, U32>:
86 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894]
87
88def words_34() -> List<&2, U32>:
89 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639]
90
91def words_35() -> List<&2, U32>:
92 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458]
93
94def words_36() -> List<&2, U32>:
95 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436]
96
97def words_37() -> List<&2, U32>:
98 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624]
99
100def words_38() -> List<&2, U32>:
101 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071]
102
103def words_39() -> List<&2, U32>:
104 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677]
105
106def words_40() -> List<&2, U32>:
107 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864]
108
109def words_41() -> List<&2, U32>:
110 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303]
111
112def words_42() -> List<&2, U32>:
113 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000]
114
115def words_43() -> List<&2, U32>:
116 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322]
117
118def words_44() -> List<&2, U32>:
119 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574]
120
121def words_45() -> List<&2, U32>:
122 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183]
123
124def words_46() -> List<&2, U32>:
125 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160]
126
127def words_47() -> List<&2, U32>:
128 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013]
129
130def words_48() -> List<&2, U32>:
131 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757]
132
133def words_49() -> List<&2, U32>:
134 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389]
135
136def words_50() -> List<&2, U32>:
137 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501]
138
139def words_51() -> List<&2, U32>:
140 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815]
141
142def words_52() -> List<&2, U32>:
143 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953]
144
145def words_53() -> List<&2, U32>:
146 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542]
147
148def words_54() -> List<&2, U32>:
149 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190]
150
151def words_55() -> List<&2, U32>:
152 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827]
153
154def words_56() -> List<&2, U32>:
155 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827, 838532342]
156
157def words_57() -> List<&2, U32>:
158 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827, 838532342, 1029747314]
159
160def words_58() -> List<&2, U32>:
161 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827, 838532342, 1029747314, 1460171999]
162
163def words_59() -> List<&2, U32>:
164 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827, 838532342, 1029747314, 1460171999, 249985896]
165
166def words_60() -> List<&2, U32>:
167 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719, 589220298, 1867252417, 855829589, 408986710, 1475663568, 540800951, 3077957442, 2810856749, 1433407894, 977015639, 155123458, 291396436, 3584880624, 4120320071, 1122172677, 3848845864, 8660303, 985151000, 864471322, 584618574, 1187881183, 3009067160, 4055386013, 349240757, 1355870389, 1785251501, 1508773815, 2067176953, 1741225542, 3566356190, 623509827, 838532342, 1029747314, 1460171999, 249985896, 1976624785]
168
169def next_words_8() ->
170 {List.append(&2, U32, words_8(), [Trace.next_word(8, 1, words_8())]) == words_9() : List<&2, U32>}:
171 {==}
172
173def next_rcon_8() ->
174 {Core.aes_rcon_kind(1, U32.is_eq(U32.mod(8, 8), 0)) == 2 : U32}:
175 {==}
176
177def next_words_9() ->
178 {List.append(&2, U32, words_9(), [Trace.next_word(9, 2, words_9())]) == words_10() : List<&2, U32>}:
179 {==}
180
181def next_rcon_9() ->
182 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(9, 8), 0)) == 2 : U32}:
183 {==}
184
185def next_words_10() ->
186 {List.append(&2, U32, words_10(), [Trace.next_word(10, 2, words_10())]) == words_11() : List<&2, U32>}:
187 {==}
188
189def next_rcon_10() ->
190 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(10, 8), 0)) == 2 : U32}:
191 {==}
192
193def next_words_11() ->
194 {List.append(&2, U32, words_11(), [Trace.next_word(11, 2, words_11())]) == words_12() : List<&2, U32>}:
195 {==}
196
197def next_rcon_11() ->
198 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(11, 8), 0)) == 2 : U32}:
199 {==}
200
201def next_words_12() ->
202 {List.append(&2, U32, words_12(), [Trace.next_word(12, 2, words_12())]) == words_13() : List<&2, U32>}:
203 {==}
204
205def next_rcon_12() ->
206 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(12, 8), 0)) == 2 : U32}:
207 {==}
208
209def next_words_13() ->
210 {List.append(&2, U32, words_13(), [Trace.next_word(13, 2, words_13())]) == words_14() : List<&2, U32>}:
211 {==}
212
213def next_rcon_13() ->
214 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(13, 8), 0)) == 2 : U32}:
215 {==}
216
217def next_words_14() ->
218 {List.append(&2, U32, words_14(), [Trace.next_word(14, 2, words_14())]) == words_15() : List<&2, U32>}:
219 {==}
220
221def next_rcon_14() ->
222 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(14, 8), 0)) == 2 : U32}:
223 {==}
224
225def next_words_15() ->
226 {List.append(&2, U32, words_15(), [Trace.next_word(15, 2, words_15())]) == words_16() : List<&2, U32>}:
227 {==}
228
229def next_rcon_15() ->
230 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(15, 8), 0)) == 2 : U32}:
231 {==}
232
233def next_words_16() ->
234 {List.append(&2, U32, words_16(), [Trace.next_word(16, 2, words_16())]) == words_17() : List<&2, U32>}:
235 {==}
236
237def next_rcon_16() ->
238 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(16, 8), 0)) == 4 : U32}:
239 {==}
240
241def next_words_17() ->
242 {List.append(&2, U32, words_17(), [Trace.next_word(17, 4, words_17())]) == words_18() : List<&2, U32>}:
243 {==}
244
245def next_rcon_17() ->
246 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(17, 8), 0)) == 4 : U32}:
247 {==}
248
249def next_words_18() ->
250 {List.append(&2, U32, words_18(), [Trace.next_word(18, 4, words_18())]) == words_19() : List<&2, U32>}:
251 {==}
252
253def next_rcon_18() ->
254 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(18, 8), 0)) == 4 : U32}:
255 {==}
256
257def next_words_19() ->
258 {List.append(&2, U32, words_19(), [Trace.next_word(19, 4, words_19())]) == words_20() : List<&2, U32>}:
259 {==}
260
261def next_rcon_19() ->
262 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(19, 8), 0)) == 4 : U32}:
263 {==}
264
265def next_words_20() ->
266 {List.append(&2, U32, words_20(), [Trace.next_word(20, 4, words_20())]) == words_21() : List<&2, U32>}:
267 {==}
268
269def next_rcon_20() ->
270 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(20, 8), 0)) == 4 : U32}:
271 {==}
272
273def next_words_21() ->
274 {List.append(&2, U32, words_21(), [Trace.next_word(21, 4, words_21())]) == words_22() : List<&2, U32>}:
275 {==}
276
277def next_rcon_21() ->
278 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(21, 8), 0)) == 4 : U32}:
279 {==}
280
281def next_words_22() ->
282 {List.append(&2, U32, words_22(), [Trace.next_word(22, 4, words_22())]) == words_23() : List<&2, U32>}:
283 {==}
284
285def next_rcon_22() ->
286 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(22, 8), 0)) == 4 : U32}:
287 {==}
288
289def next_words_23() ->
290 {List.append(&2, U32, words_23(), [Trace.next_word(23, 4, words_23())]) == words_24() : List<&2, U32>}:
291 {==}
292
293def next_rcon_23() ->
294 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(23, 8), 0)) == 4 : U32}:
295 {==}
296
297def next_words_24() ->
298 {List.append(&2, U32, words_24(), [Trace.next_word(24, 4, words_24())]) == words_25() : List<&2, U32>}:
299 {==}
300
301def next_rcon_24() ->
302 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(24, 8), 0)) == 8 : U32}:
303 {==}
304
305def next_words_25() ->
306 {List.append(&2, U32, words_25(), [Trace.next_word(25, 8, words_25())]) == words_26() : List<&2, U32>}:
307 {==}
308
309def next_rcon_25() ->
310 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(25, 8), 0)) == 8 : U32}:
311 {==}
312
313def next_words_26() ->
314 {List.append(&2, U32, words_26(), [Trace.next_word(26, 8, words_26())]) == words_27() : List<&2, U32>}:
315 {==}
316
317def next_rcon_26() ->
318 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(26, 8), 0)) == 8 : U32}:
319 {==}
320
321def next_words_27() ->
322 {List.append(&2, U32, words_27(), [Trace.next_word(27, 8, words_27())]) == words_28() : List<&2, U32>}:
323 {==}
324
325def next_rcon_27() ->
326 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(27, 8), 0)) == 8 : U32}:
327 {==}
328
329def next_words_28() ->
330 {List.append(&2, U32, words_28(), [Trace.next_word(28, 8, words_28())]) == words_29() : List<&2, U32>}:
331 {==}
332
333def next_rcon_28() ->
334 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(28, 8), 0)) == 8 : U32}:
335 {==}
336
337def next_words_29() ->
338 {List.append(&2, U32, words_29(), [Trace.next_word(29, 8, words_29())]) == words_30() : List<&2, U32>}:
339 {==}
340
341def next_rcon_29() ->
342 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(29, 8), 0)) == 8 : U32}:
343 {==}
344
345def next_words_30() ->
346 {List.append(&2, U32, words_30(), [Trace.next_word(30, 8, words_30())]) == words_31() : List<&2, U32>}:
347 {==}
348
349def next_rcon_30() ->
350 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(30, 8), 0)) == 8 : U32}:
351 {==}
352
353def next_words_31() ->
354 {List.append(&2, U32, words_31(), [Trace.next_word(31, 8, words_31())]) == words_32() : List<&2, U32>}:
355 {==}
356
357def next_rcon_31() ->
358 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(31, 8), 0)) == 8 : U32}:
359 {==}
360
361def next_words_32() ->
362 {List.append(&2, U32, words_32(), [Trace.next_word(32, 8, words_32())]) == words_33() : List<&2, U32>}:
363 {==}
364
365def next_rcon_32() ->
366 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(32, 8), 0)) == 16 : U32}:
367 {==}
368
369def next_words_33() ->
370 {List.append(&2, U32, words_33(), [Trace.next_word(33, 16, words_33())]) == words_34() : List<&2, U32>}:
371 {==}
372
373def next_rcon_33() ->
374 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(33, 8), 0)) == 16 : U32}:
375 {==}
376
377def next_words_34() ->
378 {List.append(&2, U32, words_34(), [Trace.next_word(34, 16, words_34())]) == words_35() : List<&2, U32>}:
379 {==}
380
381def next_rcon_34() ->
382 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(34, 8), 0)) == 16 : U32}:
383 {==}
384
385def next_words_35() ->
386 {List.append(&2, U32, words_35(), [Trace.next_word(35, 16, words_35())]) == words_36() : List<&2, U32>}:
387 {==}
388
389def next_rcon_35() ->
390 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(35, 8), 0)) == 16 : U32}:
391 {==}
392
393def next_words_36() ->
394 {List.append(&2, U32, words_36(), [Trace.next_word(36, 16, words_36())]) == words_37() : List<&2, U32>}:
395 {==}
396
397def next_rcon_36() ->
398 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(36, 8), 0)) == 16 : U32}:
399 {==}
400
401def next_words_37() ->
402 {List.append(&2, U32, words_37(), [Trace.next_word(37, 16, words_37())]) == words_38() : List<&2, U32>}:
403 {==}
404
405def next_rcon_37() ->
406 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(37, 8), 0)) == 16 : U32}:
407 {==}
408
409def next_words_38() ->
410 {List.append(&2, U32, words_38(), [Trace.next_word(38, 16, words_38())]) == words_39() : List<&2, U32>}:
411 {==}
412
413def next_rcon_38() ->
414 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(38, 8), 0)) == 16 : U32}:
415 {==}
416
417def next_words_39() ->
418 {List.append(&2, U32, words_39(), [Trace.next_word(39, 16, words_39())]) == words_40() : List<&2, U32>}:
419 {==}
420
421def next_rcon_39() ->
422 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(39, 8), 0)) == 16 : U32}:
423 {==}
424
425def next_words_40() ->
426 {List.append(&2, U32, words_40(), [Trace.next_word(40, 16, words_40())]) == words_41() : List<&2, U32>}:
427 {==}
428
429def next_rcon_40() ->
430 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(40, 8), 0)) == 32 : U32}:
431 {==}
432
433def next_words_41() ->
434 {List.append(&2, U32, words_41(), [Trace.next_word(41, 32, words_41())]) == words_42() : List<&2, U32>}:
435 {==}
436
437def next_rcon_41() ->
438 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(41, 8), 0)) == 32 : U32}:
439 {==}
440
441def next_words_42() ->
442 {List.append(&2, U32, words_42(), [Trace.next_word(42, 32, words_42())]) == words_43() : List<&2, U32>}:
443 {==}
444
445def next_rcon_42() ->
446 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(42, 8), 0)) == 32 : U32}:
447 {==}
448
449def next_words_43() ->
450 {List.append(&2, U32, words_43(), [Trace.next_word(43, 32, words_43())]) == words_44() : List<&2, U32>}:
451 {==}
452
453def next_rcon_43() ->
454 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(43, 8), 0)) == 32 : U32}:
455 {==}
456
457def next_words_44() ->
458 {List.append(&2, U32, words_44(), [Trace.next_word(44, 32, words_44())]) == words_45() : List<&2, U32>}:
459 {==}
460
461def next_rcon_44() ->
462 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(44, 8), 0)) == 32 : U32}:
463 {==}
464
465def next_words_45() ->
466 {List.append(&2, U32, words_45(), [Trace.next_word(45, 32, words_45())]) == words_46() : List<&2, U32>}:
467 {==}
468
469def next_rcon_45() ->
470 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(45, 8), 0)) == 32 : U32}:
471 {==}
472
473def next_words_46() ->
474 {List.append(&2, U32, words_46(), [Trace.next_word(46, 32, words_46())]) == words_47() : List<&2, U32>}:
475 {==}
476
477def next_rcon_46() ->
478 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(46, 8), 0)) == 32 : U32}:
479 {==}
480
481def next_words_47() ->
482 {List.append(&2, U32, words_47(), [Trace.next_word(47, 32, words_47())]) == words_48() : List<&2, U32>}:
483 {==}
484
485def next_rcon_47() ->
486 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(47, 8), 0)) == 32 : U32}:
487 {==}
488
489def next_words_48() ->
490 {List.append(&2, U32, words_48(), [Trace.next_word(48, 32, words_48())]) == words_49() : List<&2, U32>}:
491 {==}
492
493def next_rcon_48() ->
494 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(48, 8), 0)) == 64 : U32}:
495 {==}
496
497def next_words_49() ->
498 {List.append(&2, U32, words_49(), [Trace.next_word(49, 64, words_49())]) == words_50() : List<&2, U32>}:
499 {==}
500
501def next_rcon_49() ->
502 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(49, 8), 0)) == 64 : U32}:
503 {==}
504
505def next_words_50() ->
506 {List.append(&2, U32, words_50(), [Trace.next_word(50, 64, words_50())]) == words_51() : List<&2, U32>}:
507 {==}
508
509def next_rcon_50() ->
510 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(50, 8), 0)) == 64 : U32}:
511 {==}
512
513def next_words_51() ->
514 {List.append(&2, U32, words_51(), [Trace.next_word(51, 64, words_51())]) == words_52() : List<&2, U32>}:
515 {==}
516
517def next_rcon_51() ->
518 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(51, 8), 0)) == 64 : U32}:
519 {==}
520
521def next_words_52() ->
522 {List.append(&2, U32, words_52(), [Trace.next_word(52, 64, words_52())]) == words_53() : List<&2, U32>}:
523 {==}
524
525def next_rcon_52() ->
526 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(52, 8), 0)) == 64 : U32}:
527 {==}
528
529def next_words_53() ->
530 {List.append(&2, U32, words_53(), [Trace.next_word(53, 64, words_53())]) == words_54() : List<&2, U32>}:
531 {==}
532
533def next_rcon_53() ->
534 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(53, 8), 0)) == 64 : U32}:
535 {==}
536
537def next_words_54() ->
538 {List.append(&2, U32, words_54(), [Trace.next_word(54, 64, words_54())]) == words_55() : List<&2, U32>}:
539 {==}
540
541def next_rcon_54() ->
542 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(54, 8), 0)) == 64 : U32}:
543 {==}
544
545def next_words_55() ->
546 {List.append(&2, U32, words_55(), [Trace.next_word(55, 64, words_55())]) == words_56() : List<&2, U32>}:
547 {==}
548
549def next_rcon_55() ->
550 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(55, 8), 0)) == 64 : U32}:
551 {==}
552
553def next_words_56() ->
554 {List.append(&2, U32, words_56(), [Trace.next_word(56, 64, words_56())]) == words_57() : List<&2, U32>}:
555 {==}
556
557def next_rcon_56() ->
558 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(56, 8), 0)) == 128 : U32}:
559 {==}
560
561def next_words_57() ->
562 {List.append(&2, U32, words_57(), [Trace.next_word(57, 128, words_57())]) == words_58() : List<&2, U32>}:
563 {==}
564
565def next_rcon_57() ->
566 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(57, 8), 0)) == 128 : U32}:
567 {==}
568
569def next_words_58() ->
570 {List.append(&2, U32, words_58(), [Trace.next_word(58, 128, words_58())]) == words_59() : List<&2, U32>}:
571 {==}
572
573def next_rcon_58() ->
574 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(58, 8), 0)) == 128 : U32}:
575 {==}
576
577def next_words_59() ->
578 {List.append(&2, U32, words_59(), [Trace.next_word(59, 128, words_59())]) == words_60() : List<&2, U32>}:
579 {==}
580
581def next_rcon_59() ->
582 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(59, 8), 0)) == 128 : U32}:
583 {==}
584
585def suffix_60() ->
586 {Core.aes_expand.go(0n, 60, 128, words_60()) == words_60() : List<&2, U32>}:
587 {==}
588
589def suffix_59() ->
590 {Core.aes_expand.go(1n, 59, 128, words_59()) == words_60() : List<&2, U32>}:
591 Equal.trans(List<&2, U32>, Core.aes_expand.go(1n, 59, 128, words_59()),
592 Core.aes_expand.go(0n, 60, 128, words_60()), words_60(),
593 Trace.expand_step_number_at(0n, 1n, {==}, 59, 128, words_59(), words_60(), 128, 60,
594 next_words_59(), next_rcon_59(), {==}), suffix_60())
595
596def suffix_58() ->
597 {Core.aes_expand.go(2n, 58, 128, words_58()) == words_60() : List<&2, U32>}:
598 Equal.trans(List<&2, U32>, Core.aes_expand.go(2n, 58, 128, words_58()),
599 Core.aes_expand.go(1n, 59, 128, words_59()), words_60(),
600 Trace.expand_step_number_at(1n, 2n, {==}, 58, 128, words_58(), words_59(), 128, 59,
601 next_words_58(), next_rcon_58(), {==}), suffix_59())
602
603def suffix_57() ->
604 {Core.aes_expand.go(3n, 57, 128, words_57()) == words_60() : List<&2, U32>}:
605 Equal.trans(List<&2, U32>, Core.aes_expand.go(3n, 57, 128, words_57()),
606 Core.aes_expand.go(2n, 58, 128, words_58()), words_60(),
607 Trace.expand_step_number_at(2n, 3n, {==}, 57, 128, words_57(), words_58(), 128, 58,
608 next_words_57(), next_rcon_57(), {==}), suffix_58())
609
610def suffix_56() ->
611 {Core.aes_expand.go(4n, 56, 64, words_56()) == words_60() : List<&2, U32>}:
612 Equal.trans(List<&2, U32>, Core.aes_expand.go(4n, 56, 64, words_56()),
613 Core.aes_expand.go(3n, 57, 128, words_57()), words_60(),
614 Trace.expand_step_number_at(3n, 4n, {==}, 56, 64, words_56(), words_57(), 128, 57,
615 next_words_56(), next_rcon_56(), {==}), suffix_57())
616
617def suffix_55() ->
618 {Core.aes_expand.go(5n, 55, 64, words_55()) == words_60() : List<&2, U32>}:
619 Equal.trans(List<&2, U32>, Core.aes_expand.go(5n, 55, 64, words_55()),
620 Core.aes_expand.go(4n, 56, 64, words_56()), words_60(),
621 Trace.expand_step_number_at(4n, 5n, {==}, 55, 64, words_55(), words_56(), 64, 56,
622 next_words_55(), next_rcon_55(), {==}), suffix_56())
623
624def suffix_54() ->
625 {Core.aes_expand.go(6n, 54, 64, words_54()) == words_60() : List<&2, U32>}:
626 Equal.trans(List<&2, U32>, Core.aes_expand.go(6n, 54, 64, words_54()),
627 Core.aes_expand.go(5n, 55, 64, words_55()), words_60(),
628 Trace.expand_step_number_at(5n, 6n, {==}, 54, 64, words_54(), words_55(), 64, 55,
629 next_words_54(), next_rcon_54(), {==}), suffix_55())
630
631def suffix_53() ->
632 {Core.aes_expand.go(7n, 53, 64, words_53()) == words_60() : List<&2, U32>}:
633 Equal.trans(List<&2, U32>, Core.aes_expand.go(7n, 53, 64, words_53()),
634 Core.aes_expand.go(6n, 54, 64, words_54()), words_60(),
635 Trace.expand_step_number_at(6n, 7n, {==}, 53, 64, words_53(), words_54(), 64, 54,
636 next_words_53(), next_rcon_53(), {==}), suffix_54())
637
638def suffix_52() ->
639 {Core.aes_expand.go(8n, 52, 64, words_52()) == words_60() : List<&2, U32>}:
640 Equal.trans(List<&2, U32>, Core.aes_expand.go(8n, 52, 64, words_52()),
641 Core.aes_expand.go(7n, 53, 64, words_53()), words_60(),
642 Trace.expand_step_number_at(7n, 8n, {==}, 52, 64, words_52(), words_53(), 64, 53,
643 next_words_52(), next_rcon_52(), {==}), suffix_53())
644
645def suffix_51() ->
646 {Core.aes_expand.go(9n, 51, 64, words_51()) == words_60() : List<&2, U32>}:
647 Equal.trans(List<&2, U32>, Core.aes_expand.go(9n, 51, 64, words_51()),
648 Core.aes_expand.go(8n, 52, 64, words_52()), words_60(),
649 Trace.expand_step_number_at(8n, 9n, {==}, 51, 64, words_51(), words_52(), 64, 52,
650 next_words_51(), next_rcon_51(), {==}), suffix_52())
651
652def suffix_50() ->
653 {Core.aes_expand.go(10n, 50, 64, words_50()) == words_60() : List<&2, U32>}:
654 Equal.trans(List<&2, U32>, Core.aes_expand.go(10n, 50, 64, words_50()),
655 Core.aes_expand.go(9n, 51, 64, words_51()), words_60(),
656 Trace.expand_step_number_at(9n, 10n, {==}, 50, 64, words_50(), words_51(), 64, 51,
657 next_words_50(), next_rcon_50(), {==}), suffix_51())
658
659def suffix_49() ->
660 {Core.aes_expand.go(11n, 49, 64, words_49()) == words_60() : List<&2, U32>}:
661 Equal.trans(List<&2, U32>, Core.aes_expand.go(11n, 49, 64, words_49()),
662 Core.aes_expand.go(10n, 50, 64, words_50()), words_60(),
663 Trace.expand_step_number_at(10n, 11n, {==}, 49, 64, words_49(), words_50(), 64, 50,
664 next_words_49(), next_rcon_49(), {==}), suffix_50())
665
666def suffix_48() ->
667 {Core.aes_expand.go(12n, 48, 32, words_48()) == words_60() : List<&2, U32>}:
668 Equal.trans(List<&2, U32>, Core.aes_expand.go(12n, 48, 32, words_48()),
669 Core.aes_expand.go(11n, 49, 64, words_49()), words_60(),
670 Trace.expand_step_number_at(11n, 12n, {==}, 48, 32, words_48(), words_49(), 64, 49,
671 next_words_48(), next_rcon_48(), {==}), suffix_49())
672
673def suffix_47() ->
674 {Core.aes_expand.go(13n, 47, 32, words_47()) == words_60() : List<&2, U32>}:
675 Equal.trans(List<&2, U32>, Core.aes_expand.go(13n, 47, 32, words_47()),
676 Core.aes_expand.go(12n, 48, 32, words_48()), words_60(),
677 Trace.expand_step_number_at(12n, 13n, {==}, 47, 32, words_47(), words_48(), 32, 48,
678 next_words_47(), next_rcon_47(), {==}), suffix_48())
679
680def suffix_46() ->
681 {Core.aes_expand.go(14n, 46, 32, words_46()) == words_60() : List<&2, U32>}:
682 Equal.trans(List<&2, U32>, Core.aes_expand.go(14n, 46, 32, words_46()),
683 Core.aes_expand.go(13n, 47, 32, words_47()), words_60(),
684 Trace.expand_step_number_at(13n, 14n, {==}, 46, 32, words_46(), words_47(), 32, 47,
685 next_words_46(), next_rcon_46(), {==}), suffix_47())
686
687def suffix_45() ->
688 {Core.aes_expand.go(15n, 45, 32, words_45()) == words_60() : List<&2, U32>}:
689 Equal.trans(List<&2, U32>, Core.aes_expand.go(15n, 45, 32, words_45()),
690 Core.aes_expand.go(14n, 46, 32, words_46()), words_60(),
691 Trace.expand_step_number_at(14n, 15n, {==}, 45, 32, words_45(), words_46(), 32, 46,
692 next_words_45(), next_rcon_45(), {==}), suffix_46())
693
694def suffix_44() ->
695 {Core.aes_expand.go(16n, 44, 32, words_44()) == words_60() : List<&2, U32>}:
696 Equal.trans(List<&2, U32>, Core.aes_expand.go(16n, 44, 32, words_44()),
697 Core.aes_expand.go(15n, 45, 32, words_45()), words_60(),
698 Trace.expand_step_number_at(15n, 16n, {==}, 44, 32, words_44(), words_45(), 32, 45,
699 next_words_44(), next_rcon_44(), {==}), suffix_45())
700
701def suffix_43() ->
702 {Core.aes_expand.go(17n, 43, 32, words_43()) == words_60() : List<&2, U32>}:
703 Equal.trans(List<&2, U32>, Core.aes_expand.go(17n, 43, 32, words_43()),
704 Core.aes_expand.go(16n, 44, 32, words_44()), words_60(),
705 Trace.expand_step_number_at(16n, 17n, {==}, 43, 32, words_43(), words_44(), 32, 44,
706 next_words_43(), next_rcon_43(), {==}), suffix_44())
707
708def suffix_42() ->
709 {Core.aes_expand.go(18n, 42, 32, words_42()) == words_60() : List<&2, U32>}:
710 Equal.trans(List<&2, U32>, Core.aes_expand.go(18n, 42, 32, words_42()),
711 Core.aes_expand.go(17n, 43, 32, words_43()), words_60(),
712 Trace.expand_step_number_at(17n, 18n, {==}, 42, 32, words_42(), words_43(), 32, 43,
713 next_words_42(), next_rcon_42(), {==}), suffix_43())
714
715def suffix_41() ->
716 {Core.aes_expand.go(19n, 41, 32, words_41()) == words_60() : List<&2, U32>}:
717 Equal.trans(List<&2, U32>, Core.aes_expand.go(19n, 41, 32, words_41()),
718 Core.aes_expand.go(18n, 42, 32, words_42()), words_60(),
719 Trace.expand_step_number_at(18n, 19n, {==}, 41, 32, words_41(), words_42(), 32, 42,
720 next_words_41(), next_rcon_41(), {==}), suffix_42())
721
722def suffix_40() ->
723 {Core.aes_expand.go(20n, 40, 16, words_40()) == words_60() : List<&2, U32>}:
724 Equal.trans(List<&2, U32>, Core.aes_expand.go(20n, 40, 16, words_40()),
725 Core.aes_expand.go(19n, 41, 32, words_41()), words_60(),
726 Trace.expand_step_number_at(19n, 20n, {==}, 40, 16, words_40(), words_41(), 32, 41,
727 next_words_40(), next_rcon_40(), {==}), suffix_41())
728
729def suffix_39() ->
730 {Core.aes_expand.go(21n, 39, 16, words_39()) == words_60() : List<&2, U32>}:
731 Equal.trans(List<&2, U32>, Core.aes_expand.go(21n, 39, 16, words_39()),
732 Core.aes_expand.go(20n, 40, 16, words_40()), words_60(),
733 Trace.expand_step_number_at(20n, 21n, {==}, 39, 16, words_39(), words_40(), 16, 40,
734 next_words_39(), next_rcon_39(), {==}), suffix_40())
735
736def suffix_38() ->
737 {Core.aes_expand.go(22n, 38, 16, words_38()) == words_60() : List<&2, U32>}:
738 Equal.trans(List<&2, U32>, Core.aes_expand.go(22n, 38, 16, words_38()),
739 Core.aes_expand.go(21n, 39, 16, words_39()), words_60(),
740 Trace.expand_step_number_at(21n, 22n, {==}, 38, 16, words_38(), words_39(), 16, 39,
741 next_words_38(), next_rcon_38(), {==}), suffix_39())
742
743def suffix_37() ->
744 {Core.aes_expand.go(23n, 37, 16, words_37()) == words_60() : List<&2, U32>}:
745 Equal.trans(List<&2, U32>, Core.aes_expand.go(23n, 37, 16, words_37()),
746 Core.aes_expand.go(22n, 38, 16, words_38()), words_60(),
747 Trace.expand_step_number_at(22n, 23n, {==}, 37, 16, words_37(), words_38(), 16, 38,
748 next_words_37(), next_rcon_37(), {==}), suffix_38())
749
750def suffix_36() ->
751 {Core.aes_expand.go(24n, 36, 16, words_36()) == words_60() : List<&2, U32>}:
752 Equal.trans(List<&2, U32>, Core.aes_expand.go(24n, 36, 16, words_36()),
753 Core.aes_expand.go(23n, 37, 16, words_37()), words_60(),
754 Trace.expand_step_number_at(23n, 24n, {==}, 36, 16, words_36(), words_37(), 16, 37,
755 next_words_36(), next_rcon_36(), {==}), suffix_37())
756
757def suffix_35() ->
758 {Core.aes_expand.go(25n, 35, 16, words_35()) == words_60() : List<&2, U32>}:
759 Equal.trans(List<&2, U32>, Core.aes_expand.go(25n, 35, 16, words_35()),
760 Core.aes_expand.go(24n, 36, 16, words_36()), words_60(),
761 Trace.expand_step_number_at(24n, 25n, {==}, 35, 16, words_35(), words_36(), 16, 36,
762 next_words_35(), next_rcon_35(), {==}), suffix_36())
763
764def suffix_34() ->
765 {Core.aes_expand.go(26n, 34, 16, words_34()) == words_60() : List<&2, U32>}:
766 Equal.trans(List<&2, U32>, Core.aes_expand.go(26n, 34, 16, words_34()),
767 Core.aes_expand.go(25n, 35, 16, words_35()), words_60(),
768 Trace.expand_step_number_at(25n, 26n, {==}, 34, 16, words_34(), words_35(), 16, 35,
769 next_words_34(), next_rcon_34(), {==}), suffix_35())
770
771def suffix_33() ->
772 {Core.aes_expand.go(27n, 33, 16, words_33()) == words_60() : List<&2, U32>}:
773 Equal.trans(List<&2, U32>, Core.aes_expand.go(27n, 33, 16, words_33()),
774 Core.aes_expand.go(26n, 34, 16, words_34()), words_60(),
775 Trace.expand_step_number_at(26n, 27n, {==}, 33, 16, words_33(), words_34(), 16, 34,
776 next_words_33(), next_rcon_33(), {==}), suffix_34())
777
778def suffix_32() ->
779 {Core.aes_expand.go(28n, 32, 8, words_32()) == words_60() : List<&2, U32>}:
780 Equal.trans(List<&2, U32>, Core.aes_expand.go(28n, 32, 8, words_32()),
781 Core.aes_expand.go(27n, 33, 16, words_33()), words_60(),
782 Trace.expand_step_number_at(27n, 28n, {==}, 32, 8, words_32(), words_33(), 16, 33,
783 next_words_32(), next_rcon_32(), {==}), suffix_33())
784
785def suffix_31() ->
786 {Core.aes_expand.go(29n, 31, 8, words_31()) == words_60() : List<&2, U32>}:
787 Equal.trans(List<&2, U32>, Core.aes_expand.go(29n, 31, 8, words_31()),
788 Core.aes_expand.go(28n, 32, 8, words_32()), words_60(),
789 Trace.expand_step_number_at(28n, 29n, {==}, 31, 8, words_31(), words_32(), 8, 32,
790 next_words_31(), next_rcon_31(), {==}), suffix_32())
791
792def suffix_30() ->
793 {Core.aes_expand.go(30n, 30, 8, words_30()) == words_60() : List<&2, U32>}:
794 Equal.trans(List<&2, U32>, Core.aes_expand.go(30n, 30, 8, words_30()),
795 Core.aes_expand.go(29n, 31, 8, words_31()), words_60(),
796 Trace.expand_step_number_at(29n, 30n, {==}, 30, 8, words_30(), words_31(), 8, 31,
797 next_words_30(), next_rcon_30(), {==}), suffix_31())
798
799def suffix_29() ->
800 {Core.aes_expand.go(31n, 29, 8, words_29()) == words_60() : List<&2, U32>}:
801 Equal.trans(List<&2, U32>, Core.aes_expand.go(31n, 29, 8, words_29()),
802 Core.aes_expand.go(30n, 30, 8, words_30()), words_60(),
803 Trace.expand_step_number_at(30n, 31n, {==}, 29, 8, words_29(), words_30(), 8, 30,
804 next_words_29(), next_rcon_29(), {==}), suffix_30())
805
806def suffix_28() ->
807 {Core.aes_expand.go(32n, 28, 8, words_28()) == words_60() : List<&2, U32>}:
808 Equal.trans(List<&2, U32>, Core.aes_expand.go(32n, 28, 8, words_28()),
809 Core.aes_expand.go(31n, 29, 8, words_29()), words_60(),
810 Trace.expand_step_number_at(31n, 32n, {==}, 28, 8, words_28(), words_29(), 8, 29,
811 next_words_28(), next_rcon_28(), {==}), suffix_29())
812
813def suffix_27() ->
814 {Core.aes_expand.go(33n, 27, 8, words_27()) == words_60() : List<&2, U32>}:
815 Equal.trans(List<&2, U32>, Core.aes_expand.go(33n, 27, 8, words_27()),
816 Core.aes_expand.go(32n, 28, 8, words_28()), words_60(),
817 Trace.expand_step_number_at(32n, 33n, {==}, 27, 8, words_27(), words_28(), 8, 28,
818 next_words_27(), next_rcon_27(), {==}), suffix_28())
819
820def suffix_26() ->
821 {Core.aes_expand.go(34n, 26, 8, words_26()) == words_60() : List<&2, U32>}:
822 Equal.trans(List<&2, U32>, Core.aes_expand.go(34n, 26, 8, words_26()),
823 Core.aes_expand.go(33n, 27, 8, words_27()), words_60(),
824 Trace.expand_step_number_at(33n, 34n, {==}, 26, 8, words_26(), words_27(), 8, 27,
825 next_words_26(), next_rcon_26(), {==}), suffix_27())
826
827def suffix_25() ->
828 {Core.aes_expand.go(35n, 25, 8, words_25()) == words_60() : List<&2, U32>}:
829 Equal.trans(List<&2, U32>, Core.aes_expand.go(35n, 25, 8, words_25()),
830 Core.aes_expand.go(34n, 26, 8, words_26()), words_60(),
831 Trace.expand_step_number_at(34n, 35n, {==}, 25, 8, words_25(), words_26(), 8, 26,
832 next_words_25(), next_rcon_25(), {==}), suffix_26())
833
834def suffix_24() ->
835 {Core.aes_expand.go(36n, 24, 4, words_24()) == words_60() : List<&2, U32>}:
836 Equal.trans(List<&2, U32>, Core.aes_expand.go(36n, 24, 4, words_24()),
837 Core.aes_expand.go(35n, 25, 8, words_25()), words_60(),
838 Trace.expand_step_number_at(35n, 36n, {==}, 24, 4, words_24(), words_25(), 8, 25,
839 next_words_24(), next_rcon_24(), {==}), suffix_25())
840
841def suffix_23() ->
842 {Core.aes_expand.go(37n, 23, 4, words_23()) == words_60() : List<&2, U32>}:
843 Equal.trans(List<&2, U32>, Core.aes_expand.go(37n, 23, 4, words_23()),
844 Core.aes_expand.go(36n, 24, 4, words_24()), words_60(),
845 Trace.expand_step_number_at(36n, 37n, {==}, 23, 4, words_23(), words_24(), 4, 24,
846 next_words_23(), next_rcon_23(), {==}), suffix_24())
847
848def suffix_22() ->
849 {Core.aes_expand.go(38n, 22, 4, words_22()) == words_60() : List<&2, U32>}:
850 Equal.trans(List<&2, U32>, Core.aes_expand.go(38n, 22, 4, words_22()),
851 Core.aes_expand.go(37n, 23, 4, words_23()), words_60(),
852 Trace.expand_step_number_at(37n, 38n, {==}, 22, 4, words_22(), words_23(), 4, 23,
853 next_words_22(), next_rcon_22(), {==}), suffix_23())
854
855def suffix_21() ->
856 {Core.aes_expand.go(39n, 21, 4, words_21()) == words_60() : List<&2, U32>}:
857 Equal.trans(List<&2, U32>, Core.aes_expand.go(39n, 21, 4, words_21()),
858 Core.aes_expand.go(38n, 22, 4, words_22()), words_60(),
859 Trace.expand_step_number_at(38n, 39n, {==}, 21, 4, words_21(), words_22(), 4, 22,
860 next_words_21(), next_rcon_21(), {==}), suffix_22())
861
862def suffix_20() ->
863 {Core.aes_expand.go(40n, 20, 4, words_20()) == words_60() : List<&2, U32>}:
864 Equal.trans(List<&2, U32>, Core.aes_expand.go(40n, 20, 4, words_20()),
865 Core.aes_expand.go(39n, 21, 4, words_21()), words_60(),
866 Trace.expand_step_number_at(39n, 40n, {==}, 20, 4, words_20(), words_21(), 4, 21,
867 next_words_20(), next_rcon_20(), {==}), suffix_21())
868
869def suffix_19() ->
870 {Core.aes_expand.go(41n, 19, 4, words_19()) == words_60() : List<&2, U32>}:
871 Equal.trans(List<&2, U32>, Core.aes_expand.go(41n, 19, 4, words_19()),
872 Core.aes_expand.go(40n, 20, 4, words_20()), words_60(),
873 Trace.expand_step_number_at(40n, 41n, {==}, 19, 4, words_19(), words_20(), 4, 20,
874 next_words_19(), next_rcon_19(), {==}), suffix_20())
875
876def suffix_18() ->
877 {Core.aes_expand.go(42n, 18, 4, words_18()) == words_60() : List<&2, U32>}:
878 Equal.trans(List<&2, U32>, Core.aes_expand.go(42n, 18, 4, words_18()),
879 Core.aes_expand.go(41n, 19, 4, words_19()), words_60(),
880 Trace.expand_step_number_at(41n, 42n, {==}, 18, 4, words_18(), words_19(), 4, 19,
881 next_words_18(), next_rcon_18(), {==}), suffix_19())
882
883def suffix_17() ->
884 {Core.aes_expand.go(43n, 17, 4, words_17()) == words_60() : List<&2, U32>}:
885 Equal.trans(List<&2, U32>, Core.aes_expand.go(43n, 17, 4, words_17()),
886 Core.aes_expand.go(42n, 18, 4, words_18()), words_60(),
887 Trace.expand_step_number_at(42n, 43n, {==}, 17, 4, words_17(), words_18(), 4, 18,
888 next_words_17(), next_rcon_17(), {==}), suffix_18())
889
890def suffix_16() ->
891 {Core.aes_expand.go(44n, 16, 2, words_16()) == words_60() : List<&2, U32>}:
892 Equal.trans(List<&2, U32>, Core.aes_expand.go(44n, 16, 2, words_16()),
893 Core.aes_expand.go(43n, 17, 4, words_17()), words_60(),
894 Trace.expand_step_number_at(43n, 44n, {==}, 16, 2, words_16(), words_17(), 4, 17,
895 next_words_16(), next_rcon_16(), {==}), suffix_17())
896
897def suffix_15() ->
898 {Core.aes_expand.go(45n, 15, 2, words_15()) == words_60() : List<&2, U32>}:
899 Equal.trans(List<&2, U32>, Core.aes_expand.go(45n, 15, 2, words_15()),
900 Core.aes_expand.go(44n, 16, 2, words_16()), words_60(),
901 Trace.expand_step_number_at(44n, 45n, {==}, 15, 2, words_15(), words_16(), 2, 16,
902 next_words_15(), next_rcon_15(), {==}), suffix_16())
903
904def suffix_14() ->
905 {Core.aes_expand.go(46n, 14, 2, words_14()) == words_60() : List<&2, U32>}:
906 Equal.trans(List<&2, U32>, Core.aes_expand.go(46n, 14, 2, words_14()),
907 Core.aes_expand.go(45n, 15, 2, words_15()), words_60(),
908 Trace.expand_step_number_at(45n, 46n, {==}, 14, 2, words_14(), words_15(), 2, 15,
909 next_words_14(), next_rcon_14(), {==}), suffix_15())
910
911def suffix_13() ->
912 {Core.aes_expand.go(47n, 13, 2, words_13()) == words_60() : List<&2, U32>}:
913 Equal.trans(List<&2, U32>, Core.aes_expand.go(47n, 13, 2, words_13()),
914 Core.aes_expand.go(46n, 14, 2, words_14()), words_60(),
915 Trace.expand_step_number_at(46n, 47n, {==}, 13, 2, words_13(), words_14(), 2, 14,
916 next_words_13(), next_rcon_13(), {==}), suffix_14())
917
918def suffix_12() ->
919 {Core.aes_expand.go(48n, 12, 2, words_12()) == words_60() : List<&2, U32>}:
920 Equal.trans(List<&2, U32>, Core.aes_expand.go(48n, 12, 2, words_12()),
921 Core.aes_expand.go(47n, 13, 2, words_13()), words_60(),
922 Trace.expand_step_number_at(47n, 48n, {==}, 12, 2, words_12(), words_13(), 2, 13,
923 next_words_12(), next_rcon_12(), {==}), suffix_13())
924
925def suffix_11() ->
926 {Core.aes_expand.go(49n, 11, 2, words_11()) == words_60() : List<&2, U32>}:
927 Equal.trans(List<&2, U32>, Core.aes_expand.go(49n, 11, 2, words_11()),
928 Core.aes_expand.go(48n, 12, 2, words_12()), words_60(),
929 Trace.expand_step_number_at(48n, 49n, {==}, 11, 2, words_11(), words_12(), 2, 12,
930 next_words_11(), next_rcon_11(), {==}), suffix_12())
931
932def suffix_10() ->
933 {Core.aes_expand.go(50n, 10, 2, words_10()) == words_60() : List<&2, U32>}:
934 Equal.trans(List<&2, U32>, Core.aes_expand.go(50n, 10, 2, words_10()),
935 Core.aes_expand.go(49n, 11, 2, words_11()), words_60(),
936 Trace.expand_step_number_at(49n, 50n, {==}, 10, 2, words_10(), words_11(), 2, 11,
937 next_words_10(), next_rcon_10(), {==}), suffix_11())
938
939def suffix_9() ->
940 {Core.aes_expand.go(51n, 9, 2, words_9()) == words_60() : List<&2, U32>}:
941 Equal.trans(List<&2, U32>, Core.aes_expand.go(51n, 9, 2, words_9()),
942 Core.aes_expand.go(50n, 10, 2, words_10()), words_60(),
943 Trace.expand_step_number_at(50n, 51n, {==}, 9, 2, words_9(), words_10(), 2, 10,
944 next_words_9(), next_rcon_9(), {==}), suffix_10())
945
946def suffix_8() ->
947 {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}:
948 Equal.trans(List<&2, U32>, Core.aes_expand.go(52n, 8, 1, words_8()),
949 Core.aes_expand.go(51n, 9, 2, words_9()), words_60(),
950 Trace.expand_step_number_at(51n, 52n, {==}, 8, 1, words_8(), words_9(), 2, 9,
951 next_words_8(), next_rcon_8(), {==}), suffix_9())
952
953def expanded_words_matches() ->
954 {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}:
955 suffix_8()
956
957
958def key_schedule_matches() ->
959 {Core.aes256_expand(key_bytes()) == words_60() : List<&2, U32>}:
960 Bridge.public_expansion_matches(key_bytes(), words_60(),
961 Bridge.expand_key_matches(52n, key_bytes(), words_8(), words_60(),
962 {==}, expanded_words_matches()))