def suffix_16

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

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

890def suffix_16() ->
891    {Core.aes_expand.go(44n, 16, 2, words_16()) == words_60() : List<&2, U32>}:
892    Equal.trans(List<&2, U32>, Core.aes_expand.go(44n, 16, 2, words_16()),
893        Core.aes_expand.go(43n, 17, 4, words_17()), words_60(),
894        Trace.expand_step_number_at(43n, 44n, {==}, 16, 2, words_16(), words_17(), 4, 17,
895            next_words_16(), next_rcon_16(), {==}), suffix_17())