def suffix_44

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

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

694def suffix_44() ->
695    {Core.aes_expand.go(16n, 44, 32, words_44()) == words_60() : List<&2, U32>}:
696    Equal.trans(List<&2, U32>, Core.aes_expand.go(16n, 44, 32, words_44()),
697        Core.aes_expand.go(15n, 45, 32, words_45()), words_60(),
698        Trace.expand_step_number_at(15n, 16n, {==}, 44, 32, words_44(), words_45(), 32, 45,
699            next_words_44(), next_rcon_44(), {==}), suffix_45())