def suffix_50

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

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

652def suffix_50() ->
653    {Core.aes_expand.go(10n, 50, 64, words_50()) == words_60() : List<&2, U32>}:
654    Equal.trans(List<&2, U32>, Core.aes_expand.go(10n, 50, 64, words_50()),
655        Core.aes_expand.go(9n, 51, 64, words_51()), words_60(),
656        Trace.expand_step_number_at(9n, 10n, {==}, 50, 64, words_50(), words_51(), 64, 51,
657            next_words_50(), next_rcon_50(), {==}), suffix_51())