def suffix_28

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

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

806def suffix_28() ->
807    {Core.aes_expand.go(32n, 28, 8, words_28()) == words_60() : List<&2, U32>}:
808    Equal.trans(List<&2, U32>, Core.aes_expand.go(32n, 28, 8, words_28()),
809        Core.aes_expand.go(31n, 29, 8, words_29()), words_60(),
810        Trace.expand_step_number_at(31n, 32n, {==}, 28, 8, words_28(), words_29(), 8, 29,
811            next_words_28(), next_rcon_28(), {==}), suffix_29())