def suffix_30

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

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

792def suffix_30() ->
793    {Core.aes_expand.go(30n, 30, 8, words_30()) == words_60() : List<&2, U32>}:
794    Equal.trans(List<&2, U32>, Core.aes_expand.go(30n, 30, 8, words_30()),
795        Core.aes_expand.go(29n, 31, 8, words_31()), words_60(),
796        Trace.expand_step_number_at(29n, 30n, {==}, 30, 8, words_30(), words_31(), 8, 31,
797            next_words_30(), next_rcon_30(), {==}), suffix_31())