def suffix_49

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

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

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