proof/AES_NistBlockComposeProof.bend

qasim-bend-kit@0.1.0.2 · 264 lines · 23 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
4import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockProof.bend as Block
5import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as Trace
6import qasim-bend-kit@0.1.0.2/proof/AES_BlockBridgeProof.bend as Bridge
7
8# Symbolic remaining fuel prevents every suffix from recomputing the rounds after it.
9
10def suffix_1(+fuel: Nat) ->
11    {Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n) ==
12     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
13    Equal.trans(List<&2, U32>,
14        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),
15        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
16        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
17        Trace.rounds_step_at(fuel, Block.state_12(), Key.words_60(), 13n,
18            Block.state_13(), 14n, Block.round_13_matches(), {==}), {==})
19
20def suffix_2(+fuel: Nat) ->
21    {Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n) ==
22     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
23    Equal.trans(List<&2, U32>,
24        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n),
25        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),
26        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
27        Trace.rounds_step_at(1n+(fuel), Block.state_11(), Key.words_60(), 12n,
28            Block.state_12(), 13n, Block.round_12_matches(), {==}),
29        suffix_1(fuel))
30
31def suffix_3(+fuel: Nat) ->
32    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n) ==
33     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
34    Equal.trans(List<&2, U32>,
35        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n),
36        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n),
37        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
38        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n,
39            Block.state_11(), 12n, Block.round_11_matches(), {==}),
40        suffix_2(fuel))
41
42def suffix_4(+fuel: Nat) ->
43    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n) ==
44     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
45    Equal.trans(List<&2, U32>,
46        Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n),
47        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n),
48        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
49        Trace.rounds_step_at(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n,
50            Block.state_10(), 11n, Block.round_10_matches(), {==}),
51        suffix_3(fuel))
52
53def suffix_5(+fuel: Nat) ->
54    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n) ==
55     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
56    Equal.trans(List<&2, U32>,
57        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n),
58        Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n),
59        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
60        Trace.rounds_step_at(1n+(1n+(1n+(1n+(fuel)))), Block.state_8(), Key.words_60(), 9n,
61            Block.state_9(), 10n, Block.round_9_matches(), {==}),
62        suffix_4(fuel))
63
64def suffix_6(+fuel: Nat) ->
65    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n) ==
66     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
67    Equal.trans(List<&2, U32>,
68        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n),
69        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_8(), Key.words_60(), 9n),
70        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
71        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(fuel))))), Block.state_7(), Key.words_60(), 8n,
72            Block.state_8(), 9n, Block.round_8_matches(), {==}),
73        suffix_5(fuel))
74
75def suffix_7(+fuel: Nat) ->
76    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) ==
77     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
78    Equal.trans(List<&2, U32>,
79        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),
80        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n),
81        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
82        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_6(), Key.words_60(), 7n,
83            Block.state_7(), 8n, Block.round_7_matches(), {==}),
84        suffix_6(fuel))
85
86def suffix_8(+fuel: Nat) ->
87    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n) ==
88     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
89    Equal.trans(List<&2, U32>,
90        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n),
91        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),
92        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
93        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_5(), Key.words_60(), 6n,
94            Block.state_6(), 7n, Block.round_6_matches(), {==}),
95        suffix_7(fuel))
96
97def suffix_9(+fuel: Nat) ->
98    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n) ==
99     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
100    Equal.trans(List<&2, U32>,
101        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n),
102        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n),
103        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
104        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_4(), Key.words_60(), 5n,
105            Block.state_5(), 6n, Block.round_5_matches(), {==}),
106        suffix_8(fuel))
107
108def suffix_10(+fuel: Nat) ->
109    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n) ==
110     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
111    Equal.trans(List<&2, U32>,
112        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),
113        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n),
114        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
115        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_3(), Key.words_60(), 4n,
116            Block.state_4(), 5n, Block.round_4_matches(), {==}),
117        suffix_9(fuel))
118
119def suffix_11(+fuel: Nat) ->
120    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n) ==
121     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
122    Equal.trans(List<&2, U32>,
123        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),
124        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),
125        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
126        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_2(), Key.words_60(), 3n,
127            Block.state_3(), 4n, Block.round_3_matches(), {==}),
128        suffix_10(fuel))
129
130def suffix_12(+fuel: Nat) ->
131    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n) ==
132     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
133    Equal.trans(List<&2, U32>,
134        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),
135        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),
136        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
137        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_1(), Key.words_60(), 2n,
138            Block.state_2(), 3n, Block.round_2_matches(), {==}),
139        suffix_11(fuel))
140
141def suffix_13(+fuel: Nat) ->
142    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) ==
143     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
144    Equal.trans(List<&2, U32>,
145        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n),
146        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),
147        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
148        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_0(), Key.words_60(), 1n,
149            Block.state_1(), 2n, Block.round_1_matches(), {==}),
150        suffix_12(fuel))
151
152def chunk_0(+fuel: Nat) ->
153    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n) ==
154     Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n) : List<&2, U32>}:
155    Equal.trans(List<&2, U32>,
156        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n),
157        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),
158        Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),
159        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_0(), Key.words_60(), 1n,
160            Block.state_1(), 2n, Block.round_1_matches(), {==}),
161        Equal.trans(List<&2, U32>,
162            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),
163            Core.aes_rounds.go(1n+(fuel), Block.state_2(), Key.words_60(), 3n),
164            Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),
165            Trace.rounds_step_at(1n+(fuel), Block.state_1(), Key.words_60(), 2n,
166                Block.state_2(), 3n, Block.round_2_matches(), {==}),
167            Trace.rounds_step_at(fuel, Block.state_2(), Key.words_60(), 3n,
168                Block.state_3(), 4n, Block.round_3_matches(), {==})))
169
170def chunk_3(+fuel: Nat) ->
171    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n) ==
172     Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n) : List<&2, U32>}:
173    Equal.trans(List<&2, U32>,
174        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n),
175        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),
176        Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),
177        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_3(), Key.words_60(), 4n,
178            Block.state_4(), 5n, Block.round_4_matches(), {==}),
179        Equal.trans(List<&2, U32>,
180            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),
181            Core.aes_rounds.go(1n+(fuel), Block.state_5(), Key.words_60(), 6n),
182            Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),
183            Trace.rounds_step_at(1n+(fuel), Block.state_4(), Key.words_60(), 5n,
184                Block.state_5(), 6n, Block.round_5_matches(), {==}),
185            Trace.rounds_step_at(fuel, Block.state_5(), Key.words_60(), 6n,
186                Block.state_6(), 7n, Block.round_6_matches(), {==})))
187
188def chunk_6(+fuel: Nat) ->
189    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n) ==
190     Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n) : List<&2, U32>}:
191    Equal.trans(List<&2, U32>,
192        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n),
193        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
194        Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
195        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_6(), Key.words_60(), 7n,
196            Block.state_7(), 8n, Block.round_7_matches(), {==}),
197        Equal.trans(List<&2, U32>,
198            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
199            Core.aes_rounds.go(1n+(fuel), Block.state_8(), Key.words_60(), 9n),
200            Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
201            Trace.rounds_step_at(1n+(fuel), Block.state_7(), Key.words_60(), 8n,
202                Block.state_8(), 9n, Block.round_8_matches(), {==}),
203            Trace.rounds_step_at(fuel, Block.state_8(), Key.words_60(), 9n,
204                Block.state_9(), 10n, Block.round_9_matches(), {==})))
205
206def chunk_9(+fuel: Nat) ->
207    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n) ==
208     Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n) : List<&2, U32>}:
209    Equal.trans(List<&2, U32>,
210        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n),
211        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),
212        Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),
213        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_9(), Key.words_60(), 10n,
214            Block.state_10(), 11n, Block.round_10_matches(), {==}),
215        Equal.trans(List<&2, U32>,
216            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),
217            Core.aes_rounds.go(1n+(fuel), Block.state_11(), Key.words_60(), 12n),
218            Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),
219            Trace.rounds_step_at(1n+(fuel), Block.state_10(), Key.words_60(), 11n,
220                Block.state_11(), 12n, Block.round_11_matches(), {==}),
221            Trace.rounds_step_at(fuel, Block.state_11(), Key.words_60(), 12n,
222                Block.state_12(), 13n, Block.round_12_matches(), {==})))
223
224def rounds_0_to_6(+fuel: Nat) ->
225    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) : List<&2, U32>}:
226    Equal.trans(List<&2, U32>,
227        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),
228        chunk_0(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))),
229        chunk_3(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))
230
231def rounds_6_to_12(+fuel: Nat) ->
232    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) == Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n) : List<&2, U32>}:
233    Equal.trans(List<&2, U32>,
234        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),
235        chunk_6(1n+(1n+(1n+(1n+(fuel))))),
236        chunk_9(1n+(fuel)))
237
238def full_rounds_match(+fuel: Nat) ->
239    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
240    Equal.trans(List<&2, U32>,
241        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
242        Equal.trans(List<&2, U32>,
243            Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), rounds_0_to_6(fuel), rounds_6_to_12(fuel)),
244        suffix_1(fuel))
245
246def full_nist_rounds_match() ->
247    {Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
248    Equal.trans(List<&2, U32>,
249        Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n),
250        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n),
251        Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n),
252        Trace.rounds_fuel_matches(13n, 1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n, {==}), full_rounds_match(0n))
253
254def final_nist_block_match() ->
255    {Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n) == Block.result() : List<&2, U32>}:
256    Equal.trans(List<&2, U32>,
257        Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n),
258        Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n),
259        Block.result(), full_nist_rounds_match(), Block.final_matches())
260
261def expanded_block_matches() ->
262    {Core.aes256_encrypt_expanded(Key.words_60(), Block.block()) == Block.result() : List<&2, U32>}:
263    Bridge.expanded_block_from_initial(Key.words_60(), Block.block(), Block.state_0(),
264        Block.result(), Block.initial_matches(), final_nist_block_match())