def suffix_31

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

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

785def suffix_31() ->
786    {Core.aes_expand.go(29n, 31, 8, words_31()) == words_60() : List<&2, U32>}:
787    Equal.trans(List<&2, U32>, Core.aes_expand.go(29n, 31, 8, words_31()),
788        Core.aes_expand.go(28n, 32, 8, words_32()), words_60(),
789        Trace.expand_step_number_at(28n, 29n, {==}, 31, 8, words_31(), words_32(), 8, 32,
790            next_words_31(), next_rcon_31(), {==}), suffix_32())