def suffix_10

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

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

932def suffix_10() ->
933    {Core.aes_expand.go(50n, 10, 2, words_10()) == words_60() : List<&2, U32>}:
934    Equal.trans(List<&2, U32>, Core.aes_expand.go(50n, 10, 2, words_10()),
935        Core.aes_expand.go(49n, 11, 2, words_11()), words_60(),
936        Trace.expand_step_number_at(49n, 50n, {==}, 10, 2, words_10(), words_11(), 2, 11,
937            next_words_10(), next_rcon_10(), {==}), suffix_11())