def suffix_40

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

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

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