def suffix_18

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

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

876def suffix_18() ->
877    {Core.aes_expand.go(42n, 18, 4, words_18()) == words_60() : List<&2, U32>}:
878    Equal.trans(List<&2, U32>, Core.aes_expand.go(42n, 18, 4, words_18()),
879        Core.aes_expand.go(41n, 19, 4, words_19()), words_60(),
880        Trace.expand_step_number_at(41n, 42n, {==}, 18, 4, words_18(), words_19(), 4, 19,
881            next_words_18(), next_rcon_18(), {==}), suffix_19())