def suffix_12

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

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

918def suffix_12() ->
919    {Core.aes_expand.go(48n, 12, 2, words_12()) == words_60() : List<&2, U32>}:
920    Equal.trans(List<&2, U32>, Core.aes_expand.go(48n, 12, 2, words_12()),
921        Core.aes_expand.go(47n, 13, 2, words_13()), words_60(),
922        Trace.expand_step_number_at(47n, 48n, {==}, 12, 2, words_12(), words_13(), 2, 13,
923            next_words_12(), next_rcon_12(), {==}), suffix_13())