def suffix_59

qasim-bend-kit@0.1.0.2 · proof/AES_NistKeyScheduleProof.bend:589

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as Trace

589def 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())