def suffix_45

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

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

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