def suffix_32

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

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

778def suffix_32() ->
779    {Core.aes_expand.go(28n, 32, 8, words_32()) == words_60() : List<&2, U32>}:
780    Equal.trans(List<&2, U32>, Core.aes_expand.go(28n, 32, 8, words_32()),
781        Core.aes_expand.go(27n, 33, 16, words_33()), words_60(),
782        Trace.expand_step_number_at(27n, 28n, {==}, 32, 8, words_32(), words_33(), 16, 33,
783            next_words_32(), next_rcon_32(), {==}), suffix_33())