def suffix_58

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

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

596def suffix_58() ->
597    {Core.aes_expand.go(2n, 58, 128, words_58()) == words_60() : List<&2, U32>}:
598    Equal.trans(List<&2, U32>, Core.aes_expand.go(2n, 58, 128, words_58()),
599        Core.aes_expand.go(1n, 59, 128, words_59()), words_60(),
600        Trace.expand_step_number_at(1n, 2n, {==}, 58, 128, words_58(), words_59(), 128, 59,
601            next_words_58(), next_rcon_58(), {==}), suffix_59())