def suffix_24

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

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

834def suffix_24() ->
835    {Core.aes_expand.go(36n, 24, 4, words_24()) == words_60() : List<&2, U32>}:
836    Equal.trans(List<&2, U32>, Core.aes_expand.go(36n, 24, 4, words_24()),
837        Core.aes_expand.go(35n, 25, 8, words_25()), words_60(),
838        Trace.expand_step_number_at(35n, 36n, {==}, 24, 4, words_24(), words_25(), 8, 25,
839            next_words_24(), next_rcon_24(), {==}), suffix_25())