def suffix_17

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

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

883def suffix_17() ->
884    {Core.aes_expand.go(43n, 17, 4, words_17()) == words_60() : List<&2, U32>}:
885    Equal.trans(List<&2, U32>, Core.aes_expand.go(43n, 17, 4, words_17()),
886        Core.aes_expand.go(42n, 18, 4, words_18()), words_60(),
887        Trace.expand_step_number_at(42n, 43n, {==}, 17, 4, words_17(), words_18(), 4, 18,
888            next_words_17(), next_rcon_17(), {==}), suffix_18())