def suffix_20

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

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

862def suffix_20() ->
863    {Core.aes_expand.go(40n, 20, 4, words_20()) == words_60() : List<&2, U32>}:
864    Equal.trans(List<&2, U32>, Core.aes_expand.go(40n, 20, 4, words_20()),
865        Core.aes_expand.go(39n, 21, 4, words_21()), words_60(),
866        Trace.expand_step_number_at(39n, 40n, {==}, 20, 4, words_20(), words_21(), 4, 21,
867            next_words_20(), next_rcon_20(), {==}), suffix_21())