def suffix_15

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

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

897def suffix_15() ->
898    {Core.aes_expand.go(45n, 15, 2, words_15()) == words_60() : List<&2, U32>}:
899    Equal.trans(List<&2, U32>, Core.aes_expand.go(45n, 15, 2, words_15()),
900        Core.aes_expand.go(44n, 16, 2, words_16()), words_60(),
901        Trace.expand_step_number_at(44n, 45n, {==}, 15, 2, words_15(), words_16(), 2, 16,
902            next_words_15(), next_rcon_15(), {==}), suffix_16())