def suffix_23

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

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

841def suffix_23() ->
842    {Core.aes_expand.go(37n, 23, 4, words_23()) == words_60() : List<&2, U32>}:
843    Equal.trans(List<&2, U32>, Core.aes_expand.go(37n, 23, 4, words_23()),
844        Core.aes_expand.go(36n, 24, 4, words_24()), words_60(),
845        Trace.expand_step_number_at(36n, 37n, {==}, 23, 4, words_23(), words_24(), 4, 24,
846            next_words_23(), next_rcon_23(), {==}), suffix_24())