def suffix_19

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

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

869def suffix_19() ->
870    {Core.aes_expand.go(41n, 19, 4, words_19()) == words_60() : List<&2, U32>}:
871    Equal.trans(List<&2, U32>, Core.aes_expand.go(41n, 19, 4, words_19()),
872        Core.aes_expand.go(40n, 20, 4, words_20()), words_60(),
873        Trace.expand_step_number_at(40n, 41n, {==}, 19, 4, words_19(), words_20(), 4, 20,
874            next_words_19(), next_rcon_19(), {==}), suffix_20())