def suffix_36

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

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

750def suffix_36() ->
751    {Core.aes_expand.go(24n, 36, 16, words_36()) == words_60() : List<&2, U32>}:
752    Equal.trans(List<&2, U32>, Core.aes_expand.go(24n, 36, 16, words_36()),
753        Core.aes_expand.go(23n, 37, 16, words_37()), words_60(),
754        Trace.expand_step_number_at(23n, 24n, {==}, 36, 16, words_36(), words_37(), 16, 37,
755            next_words_36(), next_rcon_36(), {==}), suffix_37())