def suffix_54

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

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

624def suffix_54() ->
625    {Core.aes_expand.go(6n, 54, 64, words_54()) == words_60() : List<&2, U32>}:
626    Equal.trans(List<&2, U32>, Core.aes_expand.go(6n, 54, 64, words_54()),
627        Core.aes_expand.go(5n, 55, 64, words_55()), words_60(),
628        Trace.expand_step_number_at(5n, 6n, {==}, 54, 64, words_54(), words_55(), 64, 55,
629            next_words_54(), next_rcon_54(), {==}), suffix_55())