def suffix_8

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

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

946def suffix_8() ->
947    {Core.aes_expand.go(52n, 8, 1, words_8()) == words_60() : List<&2, U32>}:
948    Equal.trans(List<&2, U32>, Core.aes_expand.go(52n, 8, 1, words_8()),
949        Core.aes_expand.go(51n, 9, 2, words_9()), words_60(),
950        Trace.expand_step_number_at(51n, 52n, {==}, 8, 1, words_8(), words_9(), 2, 9,
951            next_words_8(), next_rcon_8(), {==}), suffix_9())