proof/AES_NistKeyScheduleProof.bend checks
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as AES_NistKeyScheduleProof
4 imports
import Base import ../libs/AES256GCMCore.bend as Core import ./AES_TraceProof.bend as Trace import ./AES_TraceBridgeProof.bend as Bridge
Definitions
def key_bytes source · line 7 · raw
List<&2, U32>
NIST AES-256 example key. Every expansion step is independently checked.
def words_8 source · line 10 · raw
List<&2, U32>
def words_9 source · line 13 · raw
List<&2, U32>
def words_10 source · line 16 · raw
List<&2, U32>
def words_11 source · line 19 · raw
List<&2, U32>
def words_12 source · line 22 · raw
List<&2, U32>
def words_13 source · line 25 · raw
List<&2, U32>
def words_14 source · line 28 · raw
List<&2, U32>
def words_15 source · line 31 · raw
List<&2, U32>
def words_16 source · line 34 · raw
List<&2, U32>
def words_17 source · line 37 · raw
List<&2, U32>
def words_18 source · line 40 · raw
List<&2, U32>
def words_19 source · line 43 · raw
List<&2, U32>
def words_20 source · line 46 · raw
List<&2, U32>
def words_21 source · line 49 · raw
List<&2, U32>
def words_22 source · line 52 · raw
List<&2, U32>
def words_23 source · line 55 · raw
List<&2, U32>
def words_24 source · line 58 · raw
List<&2, U32>
def words_25 source · line 61 · raw
List<&2, U32>
def words_26 source · line 64 · raw
List<&2, U32>
def words_27 source · line 67 · raw
List<&2, U32>
def words_28 source · line 70 · raw
List<&2, U32>
def words_29 source · line 73 · raw
List<&2, U32>
def words_30 source · line 76 · raw
List<&2, U32>
def words_31 source · line 79 · raw
List<&2, U32>
def words_32 source · line 82 · raw
List<&2, U32>
def words_33 source · line 85 · raw
List<&2, U32>
def words_34 source · line 88 · raw
List<&2, U32>
def words_35 source · line 91 · raw
List<&2, U32>
def words_36 source · line 94 · raw
List<&2, U32>
def words_37 source · line 97 · raw
List<&2, U32>
def words_38 source · line 100 · raw
List<&2, U32>
def words_39 source · line 103 · raw
List<&2, U32>
def words_40 source · line 106 · raw
List<&2, U32>
def words_41 source · line 109 · raw
List<&2, U32>
def words_42 source · line 112 · raw
List<&2, U32>
def words_43 source · line 115 · raw
List<&2, U32>
def words_44 source · line 118 · raw
List<&2, U32>
def words_45 source · line 121 · raw
List<&2, U32>
def words_46 source · line 124 · raw
List<&2, U32>
def words_47 source · line 127 · raw
List<&2, U32>
def words_48 source · line 130 · raw
List<&2, U32>
def words_49 source · line 133 · raw
List<&2, U32>
def words_50 source · line 136 · raw
List<&2, U32>
def words_51 source · line 139 · raw
List<&2, U32>
def words_52 source · line 142 · raw
List<&2, U32>
def words_53 source · line 145 · raw
List<&2, U32>
def words_54 source · line 148 · raw
List<&2, U32>
def words_55 source · line 151 · raw
List<&2, U32>
def words_56 source · line 154 · raw
List<&2, U32>
def words_57 source · line 157 · raw
List<&2, U32>
def words_58 source · line 160 · raw
List<&2, U32>
def words_59 source · line 163 · raw
List<&2, U32>
def words_60 source · line 166 · raw
List<&2, U32>
def next_words_8 source · line 169 · raw
{List.append(&2, U32, words_8, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(8, 1, words_8)]) == words_9 : List<&2, U32>}
def next_rcon_8 source · line 173 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(1, U32.is_eq(U32.mod(8, 8), 0)) == 2 : U32}
def next_words_9 source · line 177 · raw
{List.append(&2, U32, words_9, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(9, 2, words_9)]) == words_10 : List<&2, U32>}
def next_rcon_9 source · line 181 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(9, 8), 0)) == 2 : U32}
def next_words_10 source · line 185 · raw
{List.append(&2, U32, words_10, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(10, 2, words_10)]) == words_11 : List<&2, U32>}
def next_rcon_10 source · line 189 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(10, 8), 0)) == 2 : U32}
def next_words_11 source · line 193 · raw
{List.append(&2, U32, words_11, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(11, 2, words_11)]) == words_12 : List<&2, U32>}
def next_rcon_11 source · line 197 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(11, 8), 0)) == 2 : U32}
def next_words_12 source · line 201 · raw
{List.append(&2, U32, words_12, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(12, 2, words_12)]) == words_13 : List<&2, U32>}
def next_rcon_12 source · line 205 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(12, 8), 0)) == 2 : U32}
def next_words_13 source · line 209 · raw
{List.append(&2, U32, words_13, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(13, 2, words_13)]) == words_14 : List<&2, U32>}
def next_rcon_13 source · line 213 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(13, 8), 0)) == 2 : U32}
def next_words_14 source · line 217 · raw
{List.append(&2, U32, words_14, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(14, 2, words_14)]) == words_15 : List<&2, U32>}
def next_rcon_14 source · line 221 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(14, 8), 0)) == 2 : U32}
def next_words_15 source · line 225 · raw
{List.append(&2, U32, words_15, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(15, 2, words_15)]) == words_16 : List<&2, U32>}
def next_rcon_15 source · line 229 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(15, 8), 0)) == 2 : U32}
def next_words_16 source · line 233 · raw
{List.append(&2, U32, words_16, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(16, 2, words_16)]) == words_17 : List<&2, U32>}
def next_rcon_16 source · line 237 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(2, U32.is_eq(U32.mod(16, 8), 0)) == 4 : U32}
def next_words_17 source · line 241 · raw
{List.append(&2, U32, words_17, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(17, 4, words_17)]) == words_18 : List<&2, U32>}
def next_rcon_17 source · line 245 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(17, 8), 0)) == 4 : U32}
def next_words_18 source · line 249 · raw
{List.append(&2, U32, words_18, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(18, 4, words_18)]) == words_19 : List<&2, U32>}
def next_rcon_18 source · line 253 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(18, 8), 0)) == 4 : U32}
def next_words_19 source · line 257 · raw
{List.append(&2, U32, words_19, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(19, 4, words_19)]) == words_20 : List<&2, U32>}
def next_rcon_19 source · line 261 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(19, 8), 0)) == 4 : U32}
def next_words_20 source · line 265 · raw
{List.append(&2, U32, words_20, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(20, 4, words_20)]) == words_21 : List<&2, U32>}
def next_rcon_20 source · line 269 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(20, 8), 0)) == 4 : U32}
def next_words_21 source · line 273 · raw
{List.append(&2, U32, words_21, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(21, 4, words_21)]) == words_22 : List<&2, U32>}
def next_rcon_21 source · line 277 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(21, 8), 0)) == 4 : U32}
def next_words_22 source · line 281 · raw
{List.append(&2, U32, words_22, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(22, 4, words_22)]) == words_23 : List<&2, U32>}
def next_rcon_22 source · line 285 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(22, 8), 0)) == 4 : U32}
def next_words_23 source · line 289 · raw
{List.append(&2, U32, words_23, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(23, 4, words_23)]) == words_24 : List<&2, U32>}
def next_rcon_23 source · line 293 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(23, 8), 0)) == 4 : U32}
def next_words_24 source · line 297 · raw
{List.append(&2, U32, words_24, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(24, 4, words_24)]) == words_25 : List<&2, U32>}
def next_rcon_24 source · line 301 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(4, U32.is_eq(U32.mod(24, 8), 0)) == 8 : U32}
def next_words_25 source · line 305 · raw
{List.append(&2, U32, words_25, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(25, 8, words_25)]) == words_26 : List<&2, U32>}
def next_rcon_25 source · line 309 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(25, 8), 0)) == 8 : U32}
def next_words_26 source · line 313 · raw
{List.append(&2, U32, words_26, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(26, 8, words_26)]) == words_27 : List<&2, U32>}
def next_rcon_26 source · line 317 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(26, 8), 0)) == 8 : U32}
def next_words_27 source · line 321 · raw
{List.append(&2, U32, words_27, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(27, 8, words_27)]) == words_28 : List<&2, U32>}
def next_rcon_27 source · line 325 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(27, 8), 0)) == 8 : U32}
def next_words_28 source · line 329 · raw
{List.append(&2, U32, words_28, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(28, 8, words_28)]) == words_29 : List<&2, U32>}
def next_rcon_28 source · line 333 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(28, 8), 0)) == 8 : U32}
def next_words_29 source · line 337 · raw
{List.append(&2, U32, words_29, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(29, 8, words_29)]) == words_30 : List<&2, U32>}
def next_rcon_29 source · line 341 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(29, 8), 0)) == 8 : U32}
def next_words_30 source · line 345 · raw
{List.append(&2, U32, words_30, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(30, 8, words_30)]) == words_31 : List<&2, U32>}
def next_rcon_30 source · line 349 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(30, 8), 0)) == 8 : U32}
def next_words_31 source · line 353 · raw
{List.append(&2, U32, words_31, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(31, 8, words_31)]) == words_32 : List<&2, U32>}
def next_rcon_31 source · line 357 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(31, 8), 0)) == 8 : U32}
def next_words_32 source · line 361 · raw
{List.append(&2, U32, words_32, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(32, 8, words_32)]) == words_33 : List<&2, U32>}
def next_rcon_32 source · line 365 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(8, U32.is_eq(U32.mod(32, 8), 0)) == 16 : U32}
def next_words_33 source · line 369 · raw
{List.append(&2, U32, words_33, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(33, 16, words_33)]) == words_34 : List<&2, U32>}
def next_rcon_33 source · line 373 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(33, 8), 0)) == 16 : U32}
def next_words_34 source · line 377 · raw
{List.append(&2, U32, words_34, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(34, 16, words_34)]) == words_35 : List<&2, U32>}
def next_rcon_34 source · line 381 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(34, 8), 0)) == 16 : U32}
def next_words_35 source · line 385 · raw
{List.append(&2, U32, words_35, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(35, 16, words_35)]) == words_36 : List<&2, U32>}
def next_rcon_35 source · line 389 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(35, 8), 0)) == 16 : U32}
def next_words_36 source · line 393 · raw
{List.append(&2, U32, words_36, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(36, 16, words_36)]) == words_37 : List<&2, U32>}
def next_rcon_36 source · line 397 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(36, 8), 0)) == 16 : U32}
def next_words_37 source · line 401 · raw
{List.append(&2, U32, words_37, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(37, 16, words_37)]) == words_38 : List<&2, U32>}
def next_rcon_37 source · line 405 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(37, 8), 0)) == 16 : U32}
def next_words_38 source · line 409 · raw
{List.append(&2, U32, words_38, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(38, 16, words_38)]) == words_39 : List<&2, U32>}
def next_rcon_38 source · line 413 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(38, 8), 0)) == 16 : U32}
def next_words_39 source · line 417 · raw
{List.append(&2, U32, words_39, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(39, 16, words_39)]) == words_40 : List<&2, U32>}
def next_rcon_39 source · line 421 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(39, 8), 0)) == 16 : U32}
def next_words_40 source · line 425 · raw
{List.append(&2, U32, words_40, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(40, 16, words_40)]) == words_41 : List<&2, U32>}
def next_rcon_40 source · line 429 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(16, U32.is_eq(U32.mod(40, 8), 0)) == 32 : U32}
def next_words_41 source · line 433 · raw
{List.append(&2, U32, words_41, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(41, 32, words_41)]) == words_42 : List<&2, U32>}
def next_rcon_41 source · line 437 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(41, 8), 0)) == 32 : U32}
def next_words_42 source · line 441 · raw
{List.append(&2, U32, words_42, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(42, 32, words_42)]) == words_43 : List<&2, U32>}
def next_rcon_42 source · line 445 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(42, 8), 0)) == 32 : U32}
def next_words_43 source · line 449 · raw
{List.append(&2, U32, words_43, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(43, 32, words_43)]) == words_44 : List<&2, U32>}
def next_rcon_43 source · line 453 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(43, 8), 0)) == 32 : U32}
def next_words_44 source · line 457 · raw
{List.append(&2, U32, words_44, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(44, 32, words_44)]) == words_45 : List<&2, U32>}
def next_rcon_44 source · line 461 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(44, 8), 0)) == 32 : U32}
def next_words_45 source · line 465 · raw
{List.append(&2, U32, words_45, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(45, 32, words_45)]) == words_46 : List<&2, U32>}
def next_rcon_45 source · line 469 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(45, 8), 0)) == 32 : U32}
def next_words_46 source · line 473 · raw
{List.append(&2, U32, words_46, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(46, 32, words_46)]) == words_47 : List<&2, U32>}
def next_rcon_46 source · line 477 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(46, 8), 0)) == 32 : U32}
def next_words_47 source · line 481 · raw
{List.append(&2, U32, words_47, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(47, 32, words_47)]) == words_48 : List<&2, U32>}
def next_rcon_47 source · line 485 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(47, 8), 0)) == 32 : U32}
def next_words_48 source · line 489 · raw
{List.append(&2, U32, words_48, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(48, 32, words_48)]) == words_49 : List<&2, U32>}
def next_rcon_48 source · line 493 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(32, U32.is_eq(U32.mod(48, 8), 0)) == 64 : U32}
def next_words_49 source · line 497 · raw
{List.append(&2, U32, words_49, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(49, 64, words_49)]) == words_50 : List<&2, U32>}
def next_rcon_49 source · line 501 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(49, 8), 0)) == 64 : U32}
def next_words_50 source · line 505 · raw
{List.append(&2, U32, words_50, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(50, 64, words_50)]) == words_51 : List<&2, U32>}
def next_rcon_50 source · line 509 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(50, 8), 0)) == 64 : U32}
def next_words_51 source · line 513 · raw
{List.append(&2, U32, words_51, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(51, 64, words_51)]) == words_52 : List<&2, U32>}
def next_rcon_51 source · line 517 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(51, 8), 0)) == 64 : U32}
def next_words_52 source · line 521 · raw
{List.append(&2, U32, words_52, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(52, 64, words_52)]) == words_53 : List<&2, U32>}
def next_rcon_52 source · line 525 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(52, 8), 0)) == 64 : U32}
def next_words_53 source · line 529 · raw
{List.append(&2, U32, words_53, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(53, 64, words_53)]) == words_54 : List<&2, U32>}
def next_rcon_53 source · line 533 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(53, 8), 0)) == 64 : U32}
def next_words_54 source · line 537 · raw
{List.append(&2, U32, words_54, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(54, 64, words_54)]) == words_55 : List<&2, U32>}
def next_rcon_54 source · line 541 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(54, 8), 0)) == 64 : U32}
def next_words_55 source · line 545 · raw
{List.append(&2, U32, words_55, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(55, 64, words_55)]) == words_56 : List<&2, U32>}
def next_rcon_55 source · line 549 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(55, 8), 0)) == 64 : U32}
def next_words_56 source · line 553 · raw
{List.append(&2, U32, words_56, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(56, 64, words_56)]) == words_57 : List<&2, U32>}
def next_rcon_56 source · line 557 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(64, U32.is_eq(U32.mod(56, 8), 0)) == 128 : U32}
def next_words_57 source · line 561 · raw
{List.append(&2, U32, words_57, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(57, 128, words_57)]) == words_58 : List<&2, U32>}
def next_rcon_57 source · line 565 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(128, U32.is_eq(U32.mod(57, 8), 0)) == 128 : U32}
def next_words_58 source · line 569 · raw
{List.append(&2, U32, words_58, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(58, 128, words_58)]) == words_59 : List<&2, U32>}
def next_rcon_58 source · line 573 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(128, U32.is_eq(U32.mod(58, 8), 0)) == 128 : U32}
def next_words_59 source · line 577 · raw
{List.append(&2, U32, words_59, [0xaca801afcf3e822677fd6d06895d2c71/proof/AES_TraceProof.next_word(59, 128, words_59)]) == words_60 : List<&2, U32>}
def next_rcon_59 source · line 581 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(128, U32.is_eq(U32.mod(59, 8), 0)) == 128 : U32}
def suffix_60 source · line 585 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(0n, 60, 128, words_60) == words_60 : List<&2, U32>}
def suffix_59 source · line 589 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(1n, 59, 128, words_59) == words_60 : List<&2, U32>}
def suffix_58 source · line 596 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(2n, 58, 128, words_58) == words_60 : List<&2, U32>}
def suffix_57 source · line 603 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(3n, 57, 128, words_57) == words_60 : List<&2, U32>}
def suffix_56 source · line 610 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(4n, 56, 64, words_56) == words_60 : List<&2, U32>}
def suffix_55 source · line 617 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(5n, 55, 64, words_55) == words_60 : List<&2, U32>}
def suffix_54 source · line 624 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(6n, 54, 64, words_54) == words_60 : List<&2, U32>}
def suffix_53 source · line 631 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(7n, 53, 64, words_53) == words_60 : List<&2, U32>}
def suffix_52 source · line 638 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(8n, 52, 64, words_52) == words_60 : List<&2, U32>}
def suffix_51 source · line 645 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(9n, 51, 64, words_51) == words_60 : List<&2, U32>}
def suffix_50 source · line 652 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(10n, 50, 64, words_50) == words_60 : List<&2, U32>}
def suffix_49 source · line 659 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(11n, 49, 64, words_49) == words_60 : List<&2, U32>}
def suffix_48 source · line 666 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(12n, 48, 32, words_48) == words_60 : List<&2, U32>}
def suffix_47 source · line 673 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(13n, 47, 32, words_47) == words_60 : List<&2, U32>}
def suffix_46 source · line 680 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(14n, 46, 32, words_46) == words_60 : List<&2, U32>}
def suffix_45 source · line 687 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(15n, 45, 32, words_45) == words_60 : List<&2, U32>}
def suffix_44 source · line 694 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(16n, 44, 32, words_44) == words_60 : List<&2, U32>}
def suffix_43 source · line 701 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(17n, 43, 32, words_43) == words_60 : List<&2, U32>}
def suffix_42 source · line 708 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(18n, 42, 32, words_42) == words_60 : List<&2, U32>}
def suffix_41 source · line 715 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(19n, 41, 32, words_41) == words_60 : List<&2, U32>}
def suffix_40 source · line 722 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(20n, 40, 16, words_40) == words_60 : List<&2, U32>}
def suffix_39 source · line 729 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(21n, 39, 16, words_39) == words_60 : List<&2, U32>}
def suffix_38 source · line 736 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(22n, 38, 16, words_38) == words_60 : List<&2, U32>}
def suffix_37 source · line 743 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(23n, 37, 16, words_37) == words_60 : List<&2, U32>}
def suffix_36 source · line 750 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(24n, 36, 16, words_36) == words_60 : List<&2, U32>}
def suffix_35 source · line 757 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(25n, 35, 16, words_35) == words_60 : List<&2, U32>}
def suffix_34 source · line 764 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(26n, 34, 16, words_34) == words_60 : List<&2, U32>}
def suffix_33 source · line 771 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(27n, 33, 16, words_33) == words_60 : List<&2, U32>}
def suffix_32 source · line 778 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(28n, 32, 8, words_32) == words_60 : List<&2, U32>}
def suffix_31 source · line 785 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(29n, 31, 8, words_31) == words_60 : List<&2, U32>}
def suffix_30 source · line 792 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(30n, 30, 8, words_30) == words_60 : List<&2, U32>}
def suffix_29 source · line 799 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(31n, 29, 8, words_29) == words_60 : List<&2, U32>}
def suffix_28 source · line 806 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(32n, 28, 8, words_28) == words_60 : List<&2, U32>}
def suffix_27 source · line 813 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(33n, 27, 8, words_27) == words_60 : List<&2, U32>}
def suffix_26 source · line 820 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(34n, 26, 8, words_26) == words_60 : List<&2, U32>}
def suffix_25 source · line 827 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(35n, 25, 8, words_25) == words_60 : List<&2, U32>}
def suffix_24 source · line 834 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(36n, 24, 4, words_24) == words_60 : List<&2, U32>}
def suffix_23 source · line 841 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(37n, 23, 4, words_23) == words_60 : List<&2, U32>}
def suffix_22 source · line 848 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(38n, 22, 4, words_22) == words_60 : List<&2, U32>}
def suffix_21 source · line 855 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(39n, 21, 4, words_21) == words_60 : List<&2, U32>}
def suffix_20 source · line 862 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(40n, 20, 4, words_20) == words_60 : List<&2, U32>}
def suffix_19 source · line 869 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(41n, 19, 4, words_19) == words_60 : List<&2, U32>}
def suffix_18 source · line 876 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(42n, 18, 4, words_18) == words_60 : List<&2, U32>}
def suffix_17 source · line 883 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(43n, 17, 4, words_17) == words_60 : List<&2, U32>}
def suffix_16 source · line 890 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(44n, 16, 2, words_16) == words_60 : List<&2, U32>}
def suffix_15 source · line 897 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(45n, 15, 2, words_15) == words_60 : List<&2, U32>}
def suffix_14 source · line 904 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(46n, 14, 2, words_14) == words_60 : List<&2, U32>}
def suffix_13 source · line 911 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(47n, 13, 2, words_13) == words_60 : List<&2, U32>}
def suffix_12 source · line 918 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(48n, 12, 2, words_12) == words_60 : List<&2, U32>}
def suffix_11 source · line 925 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(49n, 11, 2, words_11) == words_60 : List<&2, U32>}
def suffix_10 source · line 932 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(50n, 10, 2, words_10) == words_60 : List<&2, U32>}
def suffix_9 source · line 939 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(51n, 9, 2, words_9) == words_60 : List<&2, U32>}
def suffix_8 source · line 946 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(52n, 8, 1, words_8) == words_60 : List<&2, U32>}
def expanded_words_matches source · line 953 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(52n, 8, 1, words_8) == words_60 : List<&2, U32>}
def key_schedule_matches source · line 958 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(key_bytes) == words_60 : List<&2, U32>}