def suffix_57

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

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

603def suffix_57() ->
604    {Core.aes_expand.go(3n, 57, 128, words_57()) == words_60() : List<&2, U32>}:
605    Equal.trans(List<&2, U32>, Core.aes_expand.go(3n, 57, 128, words_57()),
606        Core.aes_expand.go(2n, 58, 128, words_58()), words_60(),
607        Trace.expand_step_number_at(2n, 3n, {==}, 57, 128, words_57(), words_58(), 128, 58,
608            next_words_57(), next_rcon_57(), {==}), suffix_58())