proof/AES_NistKeyScheduleProof.bend source
proof/AES_NistKeyScheduleProof.bend on the hub · documented module
import Base import ../libs/AES256GCMCore.bend as Core import ./AES_TraceProof.bend as Traceimport ./AES_TraceBridgeProof.bend as Bridge # NIST AES-256 example key. Every expansion step is independently checked. def key_bytes() -> List<&2, U32>: [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] def words_8() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520] def words_9() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975] def words_10() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779] def words_11() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095] def words_12() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935] def words_13() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994] def words_14() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062] def words_15() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218] def words_16() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754] def words_17() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712] def words_18() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347] def words_19() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756] def words_20() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251] def words_21() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097] def words_22() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207] def words_23() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765] def words_24() -> List<&2, U32>: [4278184338, 2254795548, 1835700116, 1731232520, 4278184338, 2254795548, 1835700116, 1731232520, 4212381975, 2104928779, 270280095, 1999414935, 193907994, 2381037062, 3766563218, 2276569754, 824467712, 1280494347, 1548676756, 727861251, 4196704097, 2010063207, 2538475765, 285188719] def words_25() -> List<&2, U32>: [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] def words_26() -> List<&2, U32>: [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] def words_27() -> List<&2, U32>: [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] def words_28() -> List<&2, U32>: [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] def words_29() -> List<&2, U32>: [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] def words_30() -> List<&2, U32>: [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] def words_31() -> List<&2, U32>: [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] def words_32() -> List<&2, U32>: [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] def words_33() -> List<&2, U32>: [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] def words_34() -> List<&2, U32>: [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] def words_35() -> List<&2, U32>: [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] def words_36() -> List<&2, U32>: [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] def words_37() -> List<&2, U32>: [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] def words_38() -> List<&2, U32>: [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] def words_39() -> List<&2, U32>: [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] def words_40() -> List<&2, U32>: [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] def words_41() -> List<&2, U32>: [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] def words_42() -> List<&2, U32>: [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] def words_43() -> List<&2, U32>: [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] def words_44() -> List<&2, U32>: [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] def words_45() -> List<&2, U32>: [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] def words_46() -> List<&2, U32>: [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] def words_47() -> List<&2, U32>: [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] def words_48() -> List<&2, U32>: [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] def words_49() -> List<&2, U32>: [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] def words_50() -> List<&2, U32>: [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] def words_51() -> List<&2, U32>: [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] def words_52() -> List<&2, U32>: [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] def words_53() -> List<&2, U32>: [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] def words_54() -> List<&2, U32>: [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] def words_55() -> List<&2, U32>: [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] def words_56() -> List<&2, U32>: [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] def words_57() -> List<&2, U32>: [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] def words_58() -> List<&2, U32>: [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] def words_59() -> List<&2, U32>: [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] def words_60() -> List<&2, U32>: [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] def next_words_8() -> {List.append(&2, U32, words_8(), [Trace.next_word(8, 1, words_8())]) == words_9() : List<&2, U32>}: {==} def next_rcon_8() -> {Core.aes_rcon_kind(1, U32.is_eq(U32.mod(8, 8), 0)) == 2 : U32}: {==} def next_words_9() -> {List.append(&2, U32, words_9(), [Trace.next_word(9, 2, words_9())]) == words_10() : List<&2, U32>}: {==} def next_rcon_9() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(9, 8), 0)) == 2 : U32}: {==} def next_words_10() -> {List.append(&2, U32, words_10(), [Trace.next_word(10, 2, words_10())]) == words_11() : List<&2, U32>}: {==} def next_rcon_10() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(10, 8), 0)) == 2 : U32}: {==} def next_words_11() -> {List.append(&2, U32, words_11(), [Trace.next_word(11, 2, words_11())]) == words_12() : List<&2, U32>}: {==} def next_rcon_11() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(11, 8), 0)) == 2 : U32}: {==} def next_words_12() -> {List.append(&2, U32, words_12(), [Trace.next_word(12, 2, words_12())]) == words_13() : List<&2, U32>}: {==} def next_rcon_12() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(12, 8), 0)) == 2 : U32}: {==} def next_words_13() -> {List.append(&2, U32, words_13(), [Trace.next_word(13, 2, words_13())]) == words_14() : List<&2, U32>}: {==} def next_rcon_13() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(13, 8), 0)) == 2 : U32}: {==} def next_words_14() -> {List.append(&2, U32, words_14(), [Trace.next_word(14, 2, words_14())]) == words_15() : List<&2, U32>}: {==} def next_rcon_14() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(14, 8), 0)) == 2 : U32}: {==} def next_words_15() -> {List.append(&2, U32, words_15(), [Trace.next_word(15, 2, words_15())]) == words_16() : List<&2, U32>}: {==} def next_rcon_15() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(15, 8), 0)) == 2 : U32}: {==} def next_words_16() -> {List.append(&2, U32, words_16(), [Trace.next_word(16, 2, words_16())]) == words_17() : List<&2, U32>}: {==} def next_rcon_16() -> {Core.aes_rcon_kind(2, U32.is_eq(U32.mod(16, 8), 0)) == 4 : U32}: {==} def next_words_17() -> {List.append(&2, U32, words_17(), [Trace.next_word(17, 4, words_17())]) == words_18() : List<&2, U32>}: {==} def next_rcon_17() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(17, 8), 0)) == 4 : U32}: {==} def next_words_18() -> {List.append(&2, U32, words_18(), [Trace.next_word(18, 4, words_18())]) == words_19() : List<&2, U32>}: {==} def next_rcon_18() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(18, 8), 0)) == 4 : U32}: {==} def next_words_19() -> {List.append(&2, U32, words_19(), [Trace.next_word(19, 4, words_19())]) == words_20() : List<&2, U32>}: {==} def next_rcon_19() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(19, 8), 0)) == 4 : U32}: {==} def next_words_20() -> {List.append(&2, U32, words_20(), [Trace.next_word(20, 4, words_20())]) == words_21() : List<&2, U32>}: {==} def next_rcon_20() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(20, 8), 0)) == 4 : U32}: {==} def next_words_21() -> {List.append(&2, U32, words_21(), [Trace.next_word(21, 4, words_21())]) == words_22() : List<&2, U32>}: {==} def next_rcon_21() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(21, 8), 0)) == 4 : U32}: {==} def next_words_22() -> {List.append(&2, U32, words_22(), [Trace.next_word(22, 4, words_22())]) == words_23() : List<&2, U32>}: {==} def next_rcon_22() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(22, 8), 0)) == 4 : U32}: {==} def next_words_23() -> {List.append(&2, U32, words_23(), [Trace.next_word(23, 4, words_23())]) == words_24() : List<&2, U32>}: {==} def next_rcon_23() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(23, 8), 0)) == 4 : U32}: {==} def next_words_24() -> {List.append(&2, U32, words_24(), [Trace.next_word(24, 4, words_24())]) == words_25() : List<&2, U32>}: {==} def next_rcon_24() -> {Core.aes_rcon_kind(4, U32.is_eq(U32.mod(24, 8), 0)) == 8 : U32}: {==} def next_words_25() -> {List.append(&2, U32, words_25(), [Trace.next_word(25, 8, words_25())]) == words_26() : List<&2, U32>}: {==} def next_rcon_25() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(25, 8), 0)) == 8 : U32}: {==} def next_words_26() -> {List.append(&2, U32, words_26(), [Trace.next_word(26, 8, words_26())]) == words_27() : List<&2, U32>}: {==} def next_rcon_26() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(26, 8), 0)) == 8 : U32}: {==} def next_words_27() -> {List.append(&2, U32, words_27(), [Trace.next_word(27, 8, words_27())]) == words_28() : List<&2, U32>}: {==} def next_rcon_27() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(27, 8), 0)) == 8 : U32}: {==} def next_words_28() -> {List.append(&2, U32, words_28(), [Trace.next_word(28, 8, words_28())]) == words_29() : List<&2, U32>}: {==} def next_rcon_28() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(28, 8), 0)) == 8 : U32}: {==} def next_words_29() -> {List.append(&2, U32, words_29(), [Trace.next_word(29, 8, words_29())]) == words_30() : List<&2, U32>}: {==} def next_rcon_29() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(29, 8), 0)) == 8 : U32}: {==} def next_words_30() -> {List.append(&2, U32, words_30(), [Trace.next_word(30, 8, words_30())]) == words_31() : List<&2, U32>}: {==} def next_rcon_30() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(30, 8), 0)) == 8 : U32}: {==} def next_words_31() -> {List.append(&2, U32, words_31(), [Trace.next_word(31, 8, words_31())]) == words_32() : List<&2, U32>}: {==} def next_rcon_31() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(31, 8), 0)) == 8 : U32}: {==} def next_words_32() -> {List.append(&2, U32, words_32(), [Trace.next_word(32, 8, words_32())]) == words_33() : List<&2, U32>}: {==} def next_rcon_32() -> {Core.aes_rcon_kind(8, U32.is_eq(U32.mod(32, 8), 0)) == 16 : U32}: {==} def next_words_33() -> {List.append(&2, U32, words_33(), [Trace.next_word(33, 16, words_33())]) == words_34() : List<&2, U32>}: {==} def next_rcon_33() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(33, 8), 0)) == 16 : U32}: {==} def next_words_34() -> {List.append(&2, U32, words_34(), [Trace.next_word(34, 16, words_34())]) == words_35() : List<&2, U32>}: {==} def next_rcon_34() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(34, 8), 0)) == 16 : U32}: {==} def next_words_35() -> {List.append(&2, U32, words_35(), [Trace.next_word(35, 16, words_35())]) == words_36() : List<&2, U32>}: {==} def next_rcon_35() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(35, 8), 0)) == 16 : U32}: {==} def next_words_36() -> {List.append(&2, U32, words_36(), [Trace.next_word(36, 16, words_36())]) == words_37() : List<&2, U32>}: {==} def next_rcon_36() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(36, 8), 0)) == 16 : U32}: {==} def next_words_37() -> {List.append(&2, U32, words_37(), [Trace.next_word(37, 16, words_37())]) == words_38() : List<&2, U32>}: {==} def next_rcon_37() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(37, 8), 0)) == 16 : U32}: {==} def next_words_38() -> {List.append(&2, U32, words_38(), [Trace.next_word(38, 16, words_38())]) == words_39() : List<&2, U32>}: {==} def next_rcon_38() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(38, 8), 0)) == 16 : U32}: {==} def next_words_39() -> {List.append(&2, U32, words_39(), [Trace.next_word(39, 16, words_39())]) == words_40() : List<&2, U32>}: {==} def next_rcon_39() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(39, 8), 0)) == 16 : U32}: {==} def next_words_40() -> {List.append(&2, U32, words_40(), [Trace.next_word(40, 16, words_40())]) == words_41() : List<&2, U32>}: {==} def next_rcon_40() -> {Core.aes_rcon_kind(16, U32.is_eq(U32.mod(40, 8), 0)) == 32 : U32}: {==} def next_words_41() -> {List.append(&2, U32, words_41(), [Trace.next_word(41, 32, words_41())]) == words_42() : List<&2, U32>}: {==} def next_rcon_41() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(41, 8), 0)) == 32 : U32}: {==} def next_words_42() -> {List.append(&2, U32, words_42(), [Trace.next_word(42, 32, words_42())]) == words_43() : List<&2, U32>}: {==} def next_rcon_42() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(42, 8), 0)) == 32 : U32}: {==} def next_words_43() -> {List.append(&2, U32, words_43(), [Trace.next_word(43, 32, words_43())]) == words_44() : List<&2, U32>}: {==} def next_rcon_43() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(43, 8), 0)) == 32 : U32}: {==} def next_words_44() -> {List.append(&2, U32, words_44(), [Trace.next_word(44, 32, words_44())]) == words_45() : List<&2, U32>}: {==} def next_rcon_44() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(44, 8), 0)) == 32 : U32}: {==} def next_words_45() -> {List.append(&2, U32, words_45(), [Trace.next_word(45, 32, words_45())]) == words_46() : List<&2, U32>}: {==} def next_rcon_45() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(45, 8), 0)) == 32 : U32}: {==} def next_words_46() -> {List.append(&2, U32, words_46(), [Trace.next_word(46, 32, words_46())]) == words_47() : List<&2, U32>}: {==} def next_rcon_46() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(46, 8), 0)) == 32 : U32}: {==} def next_words_47() -> {List.append(&2, U32, words_47(), [Trace.next_word(47, 32, words_47())]) == words_48() : List<&2, U32>}: {==} def next_rcon_47() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(47, 8), 0)) == 32 : U32}: {==} def next_words_48() -> {List.append(&2, U32, words_48(), [Trace.next_word(48, 32, words_48())]) == words_49() : List<&2, U32>}: {==} def next_rcon_48() -> {Core.aes_rcon_kind(32, U32.is_eq(U32.mod(48, 8), 0)) == 64 : U32}: {==} def next_words_49() -> {List.append(&2, U32, words_49(), [Trace.next_word(49, 64, words_49())]) == words_50() : List<&2, U32>}: {==} def next_rcon_49() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(49, 8), 0)) == 64 : U32}: {==} def next_words_50() -> {List.append(&2, U32, words_50(), [Trace.next_word(50, 64, words_50())]) == words_51() : List<&2, U32>}: {==} def next_rcon_50() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(50, 8), 0)) == 64 : U32}: {==} def next_words_51() -> {List.append(&2, U32, words_51(), [Trace.next_word(51, 64, words_51())]) == words_52() : List<&2, U32>}: {==} def next_rcon_51() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(51, 8), 0)) == 64 : U32}: {==} def next_words_52() -> {List.append(&2, U32, words_52(), [Trace.next_word(52, 64, words_52())]) == words_53() : List<&2, U32>}: {==} def next_rcon_52() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(52, 8), 0)) == 64 : U32}: {==} def next_words_53() -> {List.append(&2, U32, words_53(), [Trace.next_word(53, 64, words_53())]) == words_54() : List<&2, U32>}: {==} def next_rcon_53() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(53, 8), 0)) == 64 : U32}: {==} def next_words_54() -> {List.append(&2, U32, words_54(), [Trace.next_word(54, 64, words_54())]) == words_55() : List<&2, U32>}: {==} def next_rcon_54() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(54, 8), 0)) == 64 : U32}: {==} def next_words_55() -> {List.append(&2, U32, words_55(), [Trace.next_word(55, 64, words_55())]) == words_56() : List<&2, U32>}: {==} def next_rcon_55() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(55, 8), 0)) == 64 : U32}: {==} def next_words_56() -> {List.append(&2, U32, words_56(), [Trace.next_word(56, 64, words_56())]) == words_57() : List<&2, U32>}: {==} def next_rcon_56() -> {Core.aes_rcon_kind(64, U32.is_eq(U32.mod(56, 8), 0)) == 128 : U32}: {==} def next_words_57() -> {List.append(&2, U32, words_57(), [Trace.next_word(57, 128, words_57())]) == words_58() : List<&2, U32>}: {==} def next_rcon_57() -> {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(57, 8), 0)) == 128 : U32}: {==} def next_words_58() -> {List.append(&2, U32, words_58(), [Trace.next_word(58, 128, words_58())]) == words_59() : List<&2, U32>}: {==} def next_rcon_58() -> {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(58, 8), 0)) == 128 : U32}: {==} def next_words_59() -> {List.append(&2, U32, words_59(), [Trace.next_word(59, 128, words_59())]) == words_60() : List<&2, U32>}: {==} def next_rcon_59() -> {Core.aes_rcon_kind(128, U32.is_eq(U32.mod(59, 8), 0)) == 128 : U32}: {==} def suffix_60() -> {Core.aes_expand.go(0n, 60, 128, words_60()) == words_60() : List<&2, U32>}: {==} def suffix_59() -> {Core.aes_expand.go(1n, 59, 128, words_59()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(1n, 59, 128, words_59()), Core.aes_expand.go(0n, 60, 128, words_60()), words_60(), Trace.expand_step_number_at(0n, 1n, {==}, 59, 128, words_59(), words_60(), 128, 60, next_words_59(), next_rcon_59(), {==}), suffix_60()) def suffix_58() -> {Core.aes_expand.go(2n, 58, 128, words_58()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(2n, 58, 128, words_58()), Core.aes_expand.go(1n, 59, 128, words_59()), words_60(), Trace.expand_step_number_at(1n, 2n, {==}, 58, 128, words_58(), words_59(), 128, 59, next_words_58(), next_rcon_58(), {==}), suffix_59()) def suffix_57() -> {Core.aes_expand.go(3n, 57, 128, words_57()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(3n, 57, 128, words_57()), Core.aes_expand.go(2n, 58, 128, words_58()), words_60(), Trace.expand_step_number_at(2n, 3n, {==}, 57, 128, words_57(), words_58(), 128, 58, next_words_57(), next_rcon_57(), {==}), suffix_58()) def suffix_56() -> {Core.aes_expand.go(4n, 56, 64, words_56()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(4n, 56, 64, words_56()), Core.aes_expand.go(3n, 57, 128, words_57()), words_60(), Trace.expand_step_number_at(3n, 4n, {==}, 56, 64, words_56(), words_57(), 128, 57, next_words_56(), next_rcon_56(), {==}), suffix_57()) def suffix_55() -> {Core.aes_expand.go(5n, 55, 64, words_55()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(5n, 55, 64, words_55()), Core.aes_expand.go(4n, 56, 64, words_56()), words_60(), Trace.expand_step_number_at(4n, 5n, {==}, 55, 64, words_55(), words_56(), 64, 56, next_words_55(), next_rcon_55(), {==}), suffix_56()) def suffix_54() -> {Core.aes_expand.go(6n, 54, 64, words_54()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(6n, 54, 64, words_54()), Core.aes_expand.go(5n, 55, 64, words_55()), words_60(), Trace.expand_step_number_at(5n, 6n, {==}, 54, 64, words_54(), words_55(), 64, 55, next_words_54(), next_rcon_54(), {==}), suffix_55()) def suffix_53() -> {Core.aes_expand.go(7n, 53, 64, words_53()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(7n, 53, 64, words_53()), Core.aes_expand.go(6n, 54, 64, words_54()), words_60(), Trace.expand_step_number_at(6n, 7n, {==}, 53, 64, words_53(), words_54(), 64, 54, next_words_53(), next_rcon_53(), {==}), suffix_54()) def suffix_52() -> {Core.aes_expand.go(8n, 52, 64, words_52()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(8n, 52, 64, words_52()), Core.aes_expand.go(7n, 53, 64, words_53()), words_60(), Trace.expand_step_number_at(7n, 8n, {==}, 52, 64, words_52(), words_53(), 64, 53, next_words_52(), next_rcon_52(), {==}), suffix_53()) def suffix_51() -> {Core.aes_expand.go(9n, 51, 64, words_51()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(9n, 51, 64, words_51()), Core.aes_expand.go(8n, 52, 64, words_52()), words_60(), Trace.expand_step_number_at(8n, 9n, {==}, 51, 64, words_51(), words_52(), 64, 52, next_words_51(), next_rcon_51(), {==}), suffix_52()) def suffix_50() -> {Core.aes_expand.go(10n, 50, 64, words_50()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(10n, 50, 64, words_50()), Core.aes_expand.go(9n, 51, 64, words_51()), words_60(), Trace.expand_step_number_at(9n, 10n, {==}, 50, 64, words_50(), words_51(), 64, 51, next_words_50(), next_rcon_50(), {==}), suffix_51()) def suffix_49() -> {Core.aes_expand.go(11n, 49, 64, words_49()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(11n, 49, 64, words_49()), Core.aes_expand.go(10n, 50, 64, words_50()), words_60(), Trace.expand_step_number_at(10n, 11n, {==}, 49, 64, words_49(), words_50(), 64, 50, next_words_49(), next_rcon_49(), {==}), suffix_50()) def suffix_48() -> {Core.aes_expand.go(12n, 48, 32, words_48()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(12n, 48, 32, words_48()), Core.aes_expand.go(11n, 49, 64, words_49()), words_60(), Trace.expand_step_number_at(11n, 12n, {==}, 48, 32, words_48(), words_49(), 64, 49, next_words_48(), next_rcon_48(), {==}), suffix_49()) def suffix_47() -> {Core.aes_expand.go(13n, 47, 32, words_47()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(13n, 47, 32, words_47()), Core.aes_expand.go(12n, 48, 32, words_48()), words_60(), Trace.expand_step_number_at(12n, 13n, {==}, 47, 32, words_47(), words_48(), 32, 48, next_words_47(), next_rcon_47(), {==}), suffix_48()) def suffix_46() -> {Core.aes_expand.go(14n, 46, 32, words_46()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(14n, 46, 32, words_46()), Core.aes_expand.go(13n, 47, 32, words_47()), words_60(), Trace.expand_step_number_at(13n, 14n, {==}, 46, 32, words_46(), words_47(), 32, 47, next_words_46(), next_rcon_46(), {==}), suffix_47()) def suffix_45() -> {Core.aes_expand.go(15n, 45, 32, words_45()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(15n, 45, 32, words_45()), Core.aes_expand.go(14n, 46, 32, words_46()), words_60(), Trace.expand_step_number_at(14n, 15n, {==}, 45, 32, words_45(), words_46(), 32, 46, next_words_45(), next_rcon_45(), {==}), suffix_46()) def suffix_44() -> {Core.aes_expand.go(16n, 44, 32, words_44()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(16n, 44, 32, words_44()), Core.aes_expand.go(15n, 45, 32, words_45()), words_60(), Trace.expand_step_number_at(15n, 16n, {==}, 44, 32, words_44(), words_45(), 32, 45, next_words_44(), next_rcon_44(), {==}), suffix_45()) def suffix_43() -> {Core.aes_expand.go(17n, 43, 32, words_43()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(17n, 43, 32, words_43()), Core.aes_expand.go(16n, 44, 32, words_44()), words_60(), Trace.expand_step_number_at(16n, 17n, {==}, 43, 32, words_43(), words_44(), 32, 44, next_words_43(), next_rcon_43(), {==}), suffix_44()) def suffix_42() -> {Core.aes_expand.go(18n, 42, 32, words_42()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(18n, 42, 32, words_42()), Core.aes_expand.go(17n, 43, 32, words_43()), words_60(), Trace.expand_step_number_at(17n, 18n, {==}, 42, 32, words_42(), words_43(), 32, 43, next_words_42(), next_rcon_42(), {==}), suffix_43()) def suffix_41() -> {Core.aes_expand.go(19n, 41, 32, words_41()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(19n, 41, 32, words_41()), Core.aes_expand.go(18n, 42, 32, words_42()), words_60(), Trace.expand_step_number_at(18n, 19n, {==}, 41, 32, words_41(), words_42(), 32, 42, next_words_41(), next_rcon_41(), {==}), suffix_42()) def suffix_40() -> {Core.aes_expand.go(20n, 40, 16, words_40()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(20n, 40, 16, words_40()), Core.aes_expand.go(19n, 41, 32, words_41()), words_60(), Trace.expand_step_number_at(19n, 20n, {==}, 40, 16, words_40(), words_41(), 32, 41, next_words_40(), next_rcon_40(), {==}), suffix_41()) def suffix_39() -> {Core.aes_expand.go(21n, 39, 16, words_39()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(21n, 39, 16, words_39()), Core.aes_expand.go(20n, 40, 16, words_40()), words_60(), Trace.expand_step_number_at(20n, 21n, {==}, 39, 16, words_39(), words_40(), 16, 40, next_words_39(), next_rcon_39(), {==}), suffix_40()) def suffix_38() -> {Core.aes_expand.go(22n, 38, 16, words_38()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(22n, 38, 16, words_38()), Core.aes_expand.go(21n, 39, 16, words_39()), words_60(), Trace.expand_step_number_at(21n, 22n, {==}, 38, 16, words_38(), words_39(), 16, 39, next_words_38(), next_rcon_38(), {==}), suffix_39()) def suffix_37() -> {Core.aes_expand.go(23n, 37, 16, words_37()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(23n, 37, 16, words_37()), Core.aes_expand.go(22n, 38, 16, words_38()), words_60(), Trace.expand_step_number_at(22n, 23n, {==}, 37, 16, words_37(), words_38(), 16, 38, next_words_37(), next_rcon_37(), {==}), suffix_38()) def suffix_36() -> {Core.aes_expand.go(24n, 36, 16, words_36()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(24n, 36, 16, words_36()), Core.aes_expand.go(23n, 37, 16, words_37()), words_60(), Trace.expand_step_number_at(23n, 24n, {==}, 36, 16, words_36(), words_37(), 16, 37, next_words_36(), next_rcon_36(), {==}), suffix_37()) def suffix_35() -> {Core.aes_expand.go(25n, 35, 16, words_35()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(25n, 35, 16, words_35()), Core.aes_expand.go(24n, 36, 16, words_36()), words_60(), Trace.expand_step_number_at(24n, 25n, {==}, 35, 16, words_35(), words_36(), 16, 36, next_words_35(), next_rcon_35(), {==}), suffix_36()) def suffix_34() -> {Core.aes_expand.go(26n, 34, 16, words_34()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(26n, 34, 16, words_34()), Core.aes_expand.go(25n, 35, 16, words_35()), words_60(), Trace.expand_step_number_at(25n, 26n, {==}, 34, 16, words_34(), words_35(), 16, 35, next_words_34(), next_rcon_34(), {==}), suffix_35()) def suffix_33() -> {Core.aes_expand.go(27n, 33, 16, words_33()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(27n, 33, 16, words_33()), Core.aes_expand.go(26n, 34, 16, words_34()), words_60(), Trace.expand_step_number_at(26n, 27n, {==}, 33, 16, words_33(), words_34(), 16, 34, next_words_33(), next_rcon_33(), {==}), suffix_34()) def suffix_32() -> {Core.aes_expand.go(28n, 32, 8, words_32()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(28n, 32, 8, words_32()), Core.aes_expand.go(27n, 33, 16, words_33()), words_60(), Trace.expand_step_number_at(27n, 28n, {==}, 32, 8, words_32(), words_33(), 16, 33, next_words_32(), next_rcon_32(), {==}), suffix_33()) def suffix_31() -> {Core.aes_expand.go(29n, 31, 8, words_31()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(29n, 31, 8, words_31()), Core.aes_expand.go(28n, 32, 8, words_32()), words_60(), Trace.expand_step_number_at(28n, 29n, {==}, 31, 8, words_31(), words_32(), 8, 32, next_words_31(), next_rcon_31(), {==}), suffix_32()) def suffix_30() -> {Core.aes_expand.go(30n, 30, 8, words_30()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(30n, 30, 8, words_30()), Core.aes_expand.go(29n, 31, 8, words_31()), words_60(), Trace.expand_step_number_at(29n, 30n, {==}, 30, 8, words_30(), words_31(), 8, 31, next_words_30(), next_rcon_30(), {==}), suffix_31()) def suffix_29() -> {Core.aes_expand.go(31n, 29, 8, words_29()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(31n, 29, 8, words_29()), Core.aes_expand.go(30n, 30, 8, words_30()), words_60(), Trace.expand_step_number_at(30n, 31n, {==}, 29, 8, words_29(), words_30(), 8, 30, next_words_29(), next_rcon_29(), {==}), suffix_30()) def suffix_28() -> {Core.aes_expand.go(32n, 28, 8, words_28()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(32n, 28, 8, words_28()), Core.aes_expand.go(31n, 29, 8, words_29()), words_60(), Trace.expand_step_number_at(31n, 32n, {==}, 28, 8, words_28(), words_29(), 8, 29, next_words_28(), next_rcon_28(), {==}), suffix_29()) def suffix_27() -> {Core.aes_expand.go(33n, 27, 8, words_27()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(33n, 27, 8, words_27()), Core.aes_expand.go(32n, 28, 8, words_28()), words_60(), Trace.expand_step_number_at(32n, 33n, {==}, 27, 8, words_27(), words_28(), 8, 28, next_words_27(), next_rcon_27(), {==}), suffix_28()) def suffix_26() -> {Core.aes_expand.go(34n, 26, 8, words_26()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(34n, 26, 8, words_26()), Core.aes_expand.go(33n, 27, 8, words_27()), words_60(), Trace.expand_step_number_at(33n, 34n, {==}, 26, 8, words_26(), words_27(), 8, 27, next_words_26(), next_rcon_26(), {==}), suffix_27()) def suffix_25() -> {Core.aes_expand.go(35n, 25, 8, words_25()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(35n, 25, 8, words_25()), Core.aes_expand.go(34n, 26, 8, words_26()), words_60(), Trace.expand_step_number_at(34n, 35n, {==}, 25, 8, words_25(), words_26(), 8, 26, next_words_25(), next_rcon_25(), {==}), suffix_26()) def suffix_24() -> {Core.aes_expand.go(36n, 24, 4, words_24()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(36n, 24, 4, words_24()), Core.aes_expand.go(35n, 25, 8, words_25()), words_60(), Trace.expand_step_number_at(35n, 36n, {==}, 24, 4, words_24(), words_25(), 8, 25, next_words_24(), next_rcon_24(), {==}), suffix_25()) def suffix_23() -> {Core.aes_expand.go(37n, 23, 4, words_23()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(37n, 23, 4, words_23()), Core.aes_expand.go(36n, 24, 4, words_24()), words_60(), Trace.expand_step_number_at(36n, 37n, {==}, 23, 4, words_23(), words_24(), 4, 24, next_words_23(), next_rcon_23(), {==}), suffix_24()) def suffix_22() -> {Core.aes_expand.go(38n, 22, 4, words_22()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(38n, 22, 4, words_22()), Core.aes_expand.go(37n, 23, 4, words_23()), words_60(), Trace.expand_step_number_at(37n, 38n, {==}, 22, 4, words_22(), words_23(), 4, 23, next_words_22(), next_rcon_22(), {==}), suffix_23()) def suffix_21() -> {Core.aes_expand.go(39n, 21, 4, words_21()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(39n, 21, 4, words_21()), Core.aes_expand.go(38n, 22, 4, words_22()), words_60(), Trace.expand_step_number_at(38n, 39n, {==}, 21, 4, words_21(), words_22(), 4, 22, next_words_21(), next_rcon_21(), {==}), suffix_22()) def suffix_20() -> {Core.aes_expand.go(40n, 20, 4, words_20()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(40n, 20, 4, words_20()), Core.aes_expand.go(39n, 21, 4, words_21()), words_60(), Trace.expand_step_number_at(39n, 40n, {==}, 20, 4, words_20(), words_21(), 4, 21, next_words_20(), next_rcon_20(), {==}), suffix_21()) def suffix_19() -> {Core.aes_expand.go(41n, 19, 4, words_19()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(41n, 19, 4, words_19()), Core.aes_expand.go(40n, 20, 4, words_20()), words_60(), Trace.expand_step_number_at(40n, 41n, {==}, 19, 4, words_19(), words_20(), 4, 20, next_words_19(), next_rcon_19(), {==}), suffix_20()) def suffix_18() -> {Core.aes_expand.go(42n, 18, 4, words_18()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(42n, 18, 4, words_18()), Core.aes_expand.go(41n, 19, 4, words_19()), words_60(), Trace.expand_step_number_at(41n, 42n, {==}, 18, 4, words_18(), words_19(), 4, 19, next_words_18(), next_rcon_18(), {==}), suffix_19()) def suffix_17() -> {Core.aes_expand.go(43n, 17, 4, words_17()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(43n, 17, 4, words_17()), Core.aes_expand.go(42n, 18, 4, words_18()), words_60(), Trace.expand_step_number_at(42n, 43n, {==}, 17, 4, words_17(), words_18(), 4, 18, next_words_17(), next_rcon_17(), {==}), suffix_18()) def suffix_16() -> {Core.aes_expand.go(44n, 16, 2, words_16()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(44n, 16, 2, words_16()), Core.aes_expand.go(43n, 17, 4, words_17()), words_60(), Trace.expand_step_number_at(43n, 44n, {==}, 16, 2, words_16(), words_17(), 4, 17, next_words_16(), next_rcon_16(), {==}), suffix_17()) def suffix_15() -> {Core.aes_expand.go(45n, 15, 2, words_15()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(45n, 15, 2, words_15()), Core.aes_expand.go(44n, 16, 2, words_16()), words_60(), Trace.expand_step_number_at(44n, 45n, {==}, 15, 2, words_15(), words_16(), 2, 16, next_words_15(), next_rcon_15(), {==}), suffix_16()) def suffix_14() -> {Core.aes_expand.go(46n, 14, 2, words_14()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(46n, 14, 2, words_14()), Core.aes_expand.go(45n, 15, 2, words_15()), words_60(), Trace.expand_step_number_at(45n, 46n, {==}, 14, 2, words_14(), words_15(), 2, 15, next_words_14(), next_rcon_14(), {==}), suffix_15()) def suffix_13() -> {Core.aes_expand.go(47n, 13, 2, words_13()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(47n, 13, 2, words_13()), Core.aes_expand.go(46n, 14, 2, words_14()), words_60(), Trace.expand_step_number_at(46n, 47n, {==}, 13, 2, words_13(), words_14(), 2, 14, next_words_13(), next_rcon_13(), {==}), suffix_14()) def suffix_12() -> {Core.aes_expand.go(48n, 12, 2, words_12()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(48n, 12, 2, words_12()), Core.aes_expand.go(47n, 13, 2, words_13()), words_60(), Trace.expand_step_number_at(47n, 48n, {==}, 12, 2, words_12(), words_13(), 2, 13, next_words_12(), next_rcon_12(), {==}), suffix_13()) def suffix_11() -> {Core.aes_expand.go(49n, 11, 2, words_11()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(49n, 11, 2, words_11()), Core.aes_expand.go(48n, 12, 2, words_12()), words_60(), Trace.expand_step_number_at(48n, 49n, {==}, 11, 2, words_11(), words_12(), 2, 12, next_words_11(), next_rcon_11(), {==}), suffix_12()) def suffix_10() -> {Core.aes_expand.go(50n, 10, 2, words_10()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(50n, 10, 2, words_10()), Core.aes_expand.go(49n, 11, 2, words_11()), words_60(), Trace.expand_step_number_at(49n, 50n, {==}, 10, 2, words_10(), words_11(), 2, 11, next_words_10(), next_rcon_10(), {==}), suffix_11()) def suffix_9() -> {Core.aes_expand.go(51n, 9, 2, words_9()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(51n, 9, 2, words_9()), Core.aes_expand.go(50n, 10, 2, words_10()), words_60(), Trace.expand_step_number_at(50n, 51n, {==}, 9, 2, words_9(), words_10(), 2, 10, next_words_9(), next_rcon_9(), {==}), suffix_10()) def suffix_8() -> {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}: Equal.trans(List<&2, U32>, Core.aes_expand.go(52n, 8, 1, words_8()), Core.aes_expand.go(51n, 9, 2, words_9()), words_60(), Trace.expand_step_number_at(51n, 52n, {==}, 8, 1, words_8(), words_9(), 2, 9, next_words_8(), next_rcon_8(), {==}), suffix_9()) def expanded_words_matches() -> {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}: suffix_8() def key_schedule_matches() -> {Core.aes256_expand(key_bytes()) == words_60() : List<&2, U32>}: Bridge.public_expansion_matches(key_bytes(), words_60(), Bridge.expand_key_matches(52n, key_bytes(), words_8(), words_60(), {==}, expanded_words_matches()))