def suffix_43

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

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

701def suffix_43() ->
702    {Core.aes_expand.go(17n, 43, 32, words_43()) == words_60() : List<&2, U32>}:
703    Equal.trans(List<&2, U32>, Core.aes_expand.go(17n, 43, 32, words_43()),
704        Core.aes_expand.go(16n, 44, 32, words_44()), words_60(),
705        Trace.expand_step_number_at(16n, 17n, {==}, 43, 32, words_43(), words_44(), 32, 44,
706            next_words_43(), next_rcon_43(), {==}), suffix_44())