def suffix_42

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

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

708def suffix_42() ->
709    {Core.aes_expand.go(18n, 42, 32, words_42()) == words_60() : List<&2, U32>}:
710    Equal.trans(List<&2, U32>, Core.aes_expand.go(18n, 42, 32, words_42()),
711        Core.aes_expand.go(17n, 43, 32, words_43()), words_60(),
712        Trace.expand_step_number_at(17n, 18n, {==}, 42, 32, words_42(), words_43(), 32, 43,
713            next_words_42(), next_rcon_42(), {==}), suffix_43())