def suffix_27

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

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

813def suffix_27() ->
814    {Core.aes_expand.go(33n, 27, 8, words_27()) == words_60() : List<&2, U32>}:
815    Equal.trans(List<&2, U32>, Core.aes_expand.go(33n, 27, 8, words_27()),
816        Core.aes_expand.go(32n, 28, 8, words_28()), words_60(),
817        Trace.expand_step_number_at(32n, 33n, {==}, 27, 8, words_27(), words_28(), 8, 28,
818            next_words_27(), next_rcon_27(), {==}), suffix_28())