def suffix_26

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

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

820def suffix_26() ->
821    {Core.aes_expand.go(34n, 26, 8, words_26()) == words_60() : List<&2, U32>}:
822    Equal.trans(List<&2, U32>, Core.aes_expand.go(34n, 26, 8, words_26()),
823        Core.aes_expand.go(33n, 27, 8, words_27()), words_60(),
824        Trace.expand_step_number_at(33n, 34n, {==}, 26, 8, words_26(), words_27(), 8, 27,
825            next_words_26(), next_rcon_26(), {==}), suffix_27())