def suffix_48

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

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

666def suffix_48() ->
667    {Core.aes_expand.go(12n, 48, 32, words_48()) == words_60() : List<&2, U32>}:
668    Equal.trans(List<&2, U32>, Core.aes_expand.go(12n, 48, 32, words_48()),
669        Core.aes_expand.go(11n, 49, 64, words_49()), words_60(),
670        Trace.expand_step_number_at(11n, 12n, {==}, 48, 32, words_48(), words_49(), 64, 49,
671            next_words_48(), next_rcon_48(), {==}), suffix_49())