def suffix_1

qasim-bend-kit@0.1.0.2 · proof/AES_NistHashBlockComposeProof.bend:10

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_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Block
import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as Trace

10def suffix_1(+fuel: Nat) ->
11    {Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n) ==
12     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
13    Equal.trans(List<&2, U32>,
14        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),
15        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
16        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
17        Trace.rounds_step_at(fuel, Block.state_12(), Key.words_60(), 13n,
18            Block.state_13(), 14n, Block.round_13_matches(), {==}), {==})