def suffix_25

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

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

827def suffix_25() ->
828    {Core.aes_expand.go(35n, 25, 8, words_25()) == words_60() : List<&2, U32>}:
829    Equal.trans(List<&2, U32>, Core.aes_expand.go(35n, 25, 8, words_25()),
830        Core.aes_expand.go(34n, 26, 8, words_26()), words_60(),
831        Trace.expand_step_number_at(34n, 35n, {==}, 25, 8, words_25(), words_26(), 8, 26,
832            next_words_25(), next_rcon_25(), {==}), suffix_26())