1 import Base 2 import ../libs/AES256GCMCore.bend as Core 3 import ./AES_TraceProof.bend as Trace 4 import ./AES_TraceBridgeProof.bend as Bridge 5 6 # NIST AES-256 example key. Every expansion step is independently checked. 7 def 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 10 def words_8() -> List<&2, U32>: 11 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520] 12 13 def words_9() -> List<&2, U32>: 14 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975] 15 16 def words_10() -> List<&2, U32>: 17 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779] 18 19 def words_11() -> List<&2, U32>: 20 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095] 21 22 def words_12() -> List<&2, U32>: 23 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935] 24 25 def words_13() -> List<&2, U32>: 26 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994] 27 28 def words_14() -> List<&2, U32>: 29 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062] 30 31 def words_15() -> List<&2, U32>: 32 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218] 33 34 def words_16() -> List<&2, U32>: 35 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754] 36 37 def words_17() -> List<&2, U32>: 38 [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712] 39 40 def 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 43 def 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 46 def 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 49 def 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 52 def 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 55 def 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 58 def 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 61 def 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 64 def 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 67 def 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 70 def 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 73 def 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 76 def 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 79 def 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 82 def 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 85 def 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 88 def 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 91 def 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 94 def 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 97 def 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 100 def 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 103 def 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 106 def 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 109 def 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 112 def 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 115 def 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 118 def 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 121 def 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 124 def 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 127 def 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 130 def 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 133 def 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 136 def 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 139 def 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 142 def 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 145 def 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 148 def 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 151 def 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 154 def 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 157 def 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 160 def 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 163 def 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 166 def 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 169 def next_words_8() -> 170 {List.append(&2, U32, words_8(), [Trace.next_word(8, 1, words_8())]) == words_9() : List<&2, U32>}: 171 {==} 172 173 def next_rcon_8() -> 174 {Core.aes_rcon_kind(1, U32.is_eq(U32.mod(8, 8), 0)) == 2 : U32}: 175 {==} 176 177 def next_words_9() -> 178 {List.append(&2, U32, words_9(), [Trace.next_word(9, 2, words_9())]) == words_10() : List<&2, U32>}: 179 {==} 180 181 def next_rcon_9() -> 182 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(9, 8), 0)) == 2 : U32}: 183 {==} 184 185 def next_words_10() -> 186 {List.append(&2, U32, words_10(), [Trace.next_word(10, 2, words_10())]) == words_11() : List<&2, U32>}: 187 {==} 188 189 def next_rcon_10() -> 190 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(10, 8), 0)) == 2 : U32}: 191 {==} 192 193 def next_words_11() -> 194 {List.append(&2, U32, words_11(), [Trace.next_word(11, 2, words_11())]) == words_12() : List<&2, U32>}: 195 {==} 196 197 def next_rcon_11() -> 198 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(11, 8), 0)) == 2 : U32}: 199 {==} 200 201 def next_words_12() -> 202 {List.append(&2, U32, words_12(), [Trace.next_word(12, 2, words_12())]) == words_13() : List<&2, U32>}: 203 {==} 204 205 def next_rcon_12() -> 206 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(12, 8), 0)) == 2 : U32}: 207 {==} 208 209 def next_words_13() -> 210 {List.append(&2, U32, words_13(), [Trace.next_word(13, 2, words_13())]) == words_14() : List<&2, U32>}: 211 {==} 212 213 def next_rcon_13() -> 214 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(13, 8), 0)) == 2 : U32}: 215 {==} 216 217 def next_words_14() -> 218 {List.append(&2, U32, words_14(), [Trace.next_word(14, 2, words_14())]) == words_15() : List<&2, U32>}: 219 {==} 220 221 def next_rcon_14() -> 222 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(14, 8), 0)) == 2 : U32}: 223 {==} 224 225 def next_words_15() -> 226 {List.append(&2, U32, words_15(), [Trace.next_word(15, 2, words_15())]) == words_16() : List<&2, U32>}: 227 {==} 228 229 def next_rcon_15() -> 230 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(15, 8), 0)) == 2 : U32}: 231 {==} 232 233 def next_words_16() -> 234 {List.append(&2, U32, words_16(), [Trace.next_word(16, 2, words_16())]) == words_17() : List<&2, U32>}: 235 {==} 236 237 def next_rcon_16() -> 238 {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(16, 8), 0)) == 4 : U32}: 239 {==} 240 241 def next_words_17() -> 242 {List.append(&2, U32, words_17(), [Trace.next_word(17, 4, words_17())]) == words_18() : List<&2, U32>}: 243 {==} 244 245 def next_rcon_17() -> 246 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(17, 8), 0)) == 4 : U32}: 247 {==} 248 249 def next_words_18() -> 250 {List.append(&2, U32, words_18(), [Trace.next_word(18, 4, words_18())]) == words_19() : List<&2, U32>}: 251 {==} 252 253 def next_rcon_18() -> 254 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(18, 8), 0)) == 4 : U32}: 255 {==} 256 257 def next_words_19() -> 258 {List.append(&2, U32, words_19(), [Trace.next_word(19, 4, words_19())]) == words_20() : List<&2, U32>}: 259 {==} 260 261 def next_rcon_19() -> 262 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(19, 8), 0)) == 4 : U32}: 263 {==} 264 265 def next_words_20() -> 266 {List.append(&2, U32, words_20(), [Trace.next_word(20, 4, words_20())]) == words_21() : List<&2, U32>}: 267 {==} 268 269 def next_rcon_20() -> 270 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(20, 8), 0)) == 4 : U32}: 271 {==} 272 273 def next_words_21() -> 274 {List.append(&2, U32, words_21(), [Trace.next_word(21, 4, words_21())]) == words_22() : List<&2, U32>}: 275 {==} 276 277 def next_rcon_21() -> 278 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(21, 8), 0)) == 4 : U32}: 279 {==} 280 281 def next_words_22() -> 282 {List.append(&2, U32, words_22(), [Trace.next_word(22, 4, words_22())]) == words_23() : List<&2, U32>}: 283 {==} 284 285 def next_rcon_22() -> 286 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(22, 8), 0)) == 4 : U32}: 287 {==} 288 289 def next_words_23() -> 290 {List.append(&2, U32, words_23(), [Trace.next_word(23, 4, words_23())]) == words_24() : List<&2, U32>}: 291 {==} 292 293 def next_rcon_23() -> 294 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(23, 8), 0)) == 4 : U32}: 295 {==} 296 297 def next_words_24() -> 298 {List.append(&2, U32, words_24(), [Trace.next_word(24, 4, words_24())]) == words_25() : List<&2, U32>}: 299 {==} 300 301 def next_rcon_24() -> 302 {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(24, 8), 0)) == 8 : U32}: 303 {==} 304 305 def next_words_25() -> 306 {List.append(&2, U32, words_25(), [Trace.next_word(25, 8, words_25())]) == words_26() : List<&2, U32>}: 307 {==} 308 309 def next_rcon_25() -> 310 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(25, 8), 0)) == 8 : U32}: 311 {==} 312 313 def next_words_26() -> 314 {List.append(&2, U32, words_26(), [Trace.next_word(26, 8, words_26())]) == words_27() : List<&2, U32>}: 315 {==} 316 317 def next_rcon_26() -> 318 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(26, 8), 0)) == 8 : U32}: 319 {==} 320 321 def next_words_27() -> 322 {List.append(&2, U32, words_27(), [Trace.next_word(27, 8, words_27())]) == words_28() : List<&2, U32>}: 323 {==} 324 325 def next_rcon_27() -> 326 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(27, 8), 0)) == 8 : U32}: 327 {==} 328 329 def next_words_28() -> 330 {List.append(&2, U32, words_28(), [Trace.next_word(28, 8, words_28())]) == words_29() : List<&2, U32>}: 331 {==} 332 333 def next_rcon_28() -> 334 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(28, 8), 0)) == 8 : U32}: 335 {==} 336 337 def next_words_29() -> 338 {List.append(&2, U32, words_29(), [Trace.next_word(29, 8, words_29())]) == words_30() : List<&2, U32>}: 339 {==} 340 341 def next_rcon_29() -> 342 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(29, 8), 0)) == 8 : U32}: 343 {==} 344 345 def next_words_30() -> 346 {List.append(&2, U32, words_30(), [Trace.next_word(30, 8, words_30())]) == words_31() : List<&2, U32>}: 347 {==} 348 349 def next_rcon_30() -> 350 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(30, 8), 0)) == 8 : U32}: 351 {==} 352 353 def next_words_31() -> 354 {List.append(&2, U32, words_31(), [Trace.next_word(31, 8, words_31())]) == words_32() : List<&2, U32>}: 355 {==} 356 357 def next_rcon_31() -> 358 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(31, 8), 0)) == 8 : U32}: 359 {==} 360 361 def next_words_32() -> 362 {List.append(&2, U32, words_32(), [Trace.next_word(32, 8, words_32())]) == words_33() : List<&2, U32>}: 363 {==} 364 365 def next_rcon_32() -> 366 {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(32, 8), 0)) == 16 : U32}: 367 {==} 368 369 def next_words_33() -> 370 {List.append(&2, U32, words_33(), [Trace.next_word(33, 16, words_33())]) == words_34() : List<&2, U32>}: 371 {==} 372 373 def next_rcon_33() -> 374 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(33, 8), 0)) == 16 : U32}: 375 {==} 376 377 def next_words_34() -> 378 {List.append(&2, U32, words_34(), [Trace.next_word(34, 16, words_34())]) == words_35() : List<&2, U32>}: 379 {==} 380 381 def next_rcon_34() -> 382 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(34, 8), 0)) == 16 : U32}: 383 {==} 384 385 def next_words_35() -> 386 {List.append(&2, U32, words_35(), [Trace.next_word(35, 16, words_35())]) == words_36() : List<&2, U32>}: 387 {==} 388 389 def next_rcon_35() -> 390 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(35, 8), 0)) == 16 : U32}: 391 {==} 392 393 def next_words_36() -> 394 {List.append(&2, U32, words_36(), [Trace.next_word(36, 16, words_36())]) == words_37() : List<&2, U32>}: 395 {==} 396 397 def next_rcon_36() -> 398 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(36, 8), 0)) == 16 : U32}: 399 {==} 400 401 def next_words_37() -> 402 {List.append(&2, U32, words_37(), [Trace.next_word(37, 16, words_37())]) == words_38() : List<&2, U32>}: 403 {==} 404 405 def next_rcon_37() -> 406 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(37, 8), 0)) == 16 : U32}: 407 {==} 408 409 def next_words_38() -> 410 {List.append(&2, U32, words_38(), [Trace.next_word(38, 16, words_38())]) == words_39() : List<&2, U32>}: 411 {==} 412 413 def next_rcon_38() -> 414 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(38, 8), 0)) == 16 : U32}: 415 {==} 416 417 def next_words_39() -> 418 {List.append(&2, U32, words_39(), [Trace.next_word(39, 16, words_39())]) == words_40() : List<&2, U32>}: 419 {==} 420 421 def next_rcon_39() -> 422 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(39, 8), 0)) == 16 : U32}: 423 {==} 424 425 def next_words_40() -> 426 {List.append(&2, U32, words_40(), [Trace.next_word(40, 16, words_40())]) == words_41() : List<&2, U32>}: 427 {==} 428 429 def next_rcon_40() -> 430 {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(40, 8), 0)) == 32 : U32}: 431 {==} 432 433 def next_words_41() -> 434 {List.append(&2, U32, words_41(), [Trace.next_word(41, 32, words_41())]) == words_42() : List<&2, U32>}: 435 {==} 436 437 def next_rcon_41() -> 438 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(41, 8), 0)) == 32 : U32}: 439 {==} 440 441 def next_words_42() -> 442 {List.append(&2, U32, words_42(), [Trace.next_word(42, 32, words_42())]) == words_43() : List<&2, U32>}: 443 {==} 444 445 def next_rcon_42() -> 446 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(42, 8), 0)) == 32 : U32}: 447 {==} 448 449 def next_words_43() -> 450 {List.append(&2, U32, words_43(), [Trace.next_word(43, 32, words_43())]) == words_44() : List<&2, U32>}: 451 {==} 452 453 def next_rcon_43() -> 454 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(43, 8), 0)) == 32 : U32}: 455 {==} 456 457 def next_words_44() -> 458 {List.append(&2, U32, words_44(), [Trace.next_word(44, 32, words_44())]) == words_45() : List<&2, U32>}: 459 {==} 460 461 def next_rcon_44() -> 462 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(44, 8), 0)) == 32 : U32}: 463 {==} 464 465 def next_words_45() -> 466 {List.append(&2, U32, words_45(), [Trace.next_word(45, 32, words_45())]) == words_46() : List<&2, U32>}: 467 {==} 468 469 def next_rcon_45() -> 470 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(45, 8), 0)) == 32 : U32}: 471 {==} 472 473 def next_words_46() -> 474 {List.append(&2, U32, words_46(), [Trace.next_word(46, 32, words_46())]) == words_47() : List<&2, U32>}: 475 {==} 476 477 def next_rcon_46() -> 478 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(46, 8), 0)) == 32 : U32}: 479 {==} 480 481 def next_words_47() -> 482 {List.append(&2, U32, words_47(), [Trace.next_word(47, 32, words_47())]) == words_48() : List<&2, U32>}: 483 {==} 484 485 def next_rcon_47() -> 486 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(47, 8), 0)) == 32 : U32}: 487 {==} 488 489 def next_words_48() -> 490 {List.append(&2, U32, words_48(), [Trace.next_word(48, 32, words_48())]) == words_49() : List<&2, U32>}: 491 {==} 492 493 def next_rcon_48() -> 494 {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(48, 8), 0)) == 64 : U32}: 495 {==} 496 497 def next_words_49() -> 498 {List.append(&2, U32, words_49(), [Trace.next_word(49, 64, words_49())]) == words_50() : List<&2, U32>}: 499 {==} 500 501 def next_rcon_49() -> 502 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(49, 8), 0)) == 64 : U32}: 503 {==} 504 505 def next_words_50() -> 506 {List.append(&2, U32, words_50(), [Trace.next_word(50, 64, words_50())]) == words_51() : List<&2, U32>}: 507 {==} 508 509 def next_rcon_50() -> 510 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(50, 8), 0)) == 64 : U32}: 511 {==} 512 513 def next_words_51() -> 514 {List.append(&2, U32, words_51(), [Trace.next_word(51, 64, words_51())]) == words_52() : List<&2, U32>}: 515 {==} 516 517 def next_rcon_51() -> 518 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(51, 8), 0)) == 64 : U32}: 519 {==} 520 521 def next_words_52() -> 522 {List.append(&2, U32, words_52(), [Trace.next_word(52, 64, words_52())]) == words_53() : List<&2, U32>}: 523 {==} 524 525 def next_rcon_52() -> 526 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(52, 8), 0)) == 64 : U32}: 527 {==} 528 529 def next_words_53() -> 530 {List.append(&2, U32, words_53(), [Trace.next_word(53, 64, words_53())]) == words_54() : List<&2, U32>}: 531 {==} 532 533 def next_rcon_53() -> 534 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(53, 8), 0)) == 64 : U32}: 535 {==} 536 537 def next_words_54() -> 538 {List.append(&2, U32, words_54(), [Trace.next_word(54, 64, words_54())]) == words_55() : List<&2, U32>}: 539 {==} 540 541 def next_rcon_54() -> 542 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(54, 8), 0)) == 64 : U32}: 543 {==} 544 545 def next_words_55() -> 546 {List.append(&2, U32, words_55(), [Trace.next_word(55, 64, words_55())]) == words_56() : List<&2, U32>}: 547 {==} 548 549 def next_rcon_55() -> 550 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(55, 8), 0)) == 64 : U32}: 551 {==} 552 553 def next_words_56() -> 554 {List.append(&2, U32, words_56(), [Trace.next_word(56, 64, words_56())]) == words_57() : List<&2, U32>}: 555 {==} 556 557 def next_rcon_56() -> 558 {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(56, 8), 0)) == 128 : U32}: 559 {==} 560 561 def next_words_57() -> 562 {List.append(&2, U32, words_57(), [Trace.next_word(57, 128, words_57())]) == words_58() : List<&2, U32>}: 563 {==} 564 565 def next_rcon_57() -> 566 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(57, 8), 0)) == 128 : U32}: 567 {==} 568 569 def next_words_58() -> 570 {List.append(&2, U32, words_58(), [Trace.next_word(58, 128, words_58())]) == words_59() : List<&2, U32>}: 571 {==} 572 573 def next_rcon_58() -> 574 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(58, 8), 0)) == 128 : U32}: 575 {==} 576 577 def next_words_59() -> 578 {List.append(&2, U32, words_59(), [Trace.next_word(59, 128, words_59())]) == words_60() : List<&2, U32>}: 579 {==} 580 581 def next_rcon_59() -> 582 {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(59, 8), 0)) == 128 : U32}: 583 {==} 584 585 def suffix_60() -> 586 {Core.aes_expand.go(0n, 60, 128, words_60()) == words_60() : List<&2, U32>}: 587 {==} 588 589 def 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 596 def 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 603 def 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 610 def 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 617 def 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 624 def 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 631 def 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 638 def 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 645 def 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 652 def 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 659 def 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 666 def 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 673 def 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 680 def 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 687 def 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 694 def 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 701 def 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 708 def 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 715 def 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 722 def 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 729 def 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 736 def 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 743 def 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 750 def 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 757 def 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 764 def 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 771 def 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 778 def 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 785 def 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 792 def 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 799 def 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 806 def 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 813 def 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 820 def 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 827 def 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 834 def 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 841 def 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 848 def 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 855 def 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 862 def 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 869 def 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 876 def 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 883 def 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 890 def 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 897 def 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 904 def 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 911 def 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 918 def 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 925 def 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 932 def 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 939 def 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 946 def 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 953 def expanded_words_matches() -> 954 {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}: 955 suffix_8() 956 957 958 def 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()))