def suffix_56

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

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

610def suffix_56() ->
611    {Core.aes_expand.go(4n, 56, 64, words_56()) == words_60() : List<&2, U32>}:
612    Equal.trans(List<&2, U32>, Core.aes_expand.go(4n, 56, 64, words_56()),
613        Core.aes_expand.go(3n, 57, 128, words_57()), words_60(),
614        Trace.expand_step_number_at(3n, 4n, {==}, 56, 64, words_56(), words_57(), 128, 57,
615            next_words_56(), next_rcon_56(), {==}), suffix_57())