def suffix_52

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

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

638def suffix_52() ->
639    {Core.aes_expand.go(8n, 52, 64, words_52()) == words_60() : List<&2, U32>}:
640    Equal.trans(List<&2, U32>, Core.aes_expand.go(8n, 52, 64, words_52()),
641        Core.aes_expand.go(7n, 53, 64, words_53()), words_60(),
642        Trace.expand_step_number_at(7n, 8n, {==}, 52, 64, words_52(), words_53(), 64, 53,
643            next_words_52(), next_rcon_52(), {==}), suffix_53())