def suffix_2

qasim-bend-kit@0.1.0.2 · proof/AES_NistBlockComposeProof.bend:20

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

20def suffix_2(+fuel: Nat) ->
21    {Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n) ==
22     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
23    Equal.trans(List<&2, U32>,
24        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_11(), Key.words_60(), 12n),
25        Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n),
26        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
27        Trace.rounds_step_at(1n+(fuel), Block.state_11(), Key.words_60(), 12n,
28            Block.state_12(), 13n, Block.round_12_matches(), {==}),
29        suffix_1(fuel))