1 import Base 2 import ../libs/AES256GCMCore.bend as Core 3 import ./AES_NistKeyScheduleProof.bend as Key 4 import ./AES_NistBlockProof.bend as Block 5 import ./AES_TraceProof.bend as Trace 6 import ./AES_BlockBridgeProof.bend as Bridge 7 8 # Symbolic remaining fuel prevents every suffix from recomputing the rounds after it. 9 10 def 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 20 def 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 31 def 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 42 def 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 53 def 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 64 def 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 75 def 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 86 def 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 97 def 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 108 def 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 119 def 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 130 def 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 141 def 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 152 def 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 170 def 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 188 def 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 206 def 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 224 def 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 231 def 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 238 def 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 246 def 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 254 def 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 261 def 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())