def suffix_11

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

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

119def suffix_11(+fuel: Nat) ->
120    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n) ==
121     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
122    Equal.trans(List<&2, U32>,
123        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),
124        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),
125        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
126        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_2(), Key.words_60(), 3n,
127            Block.state_3(), 4n, Block.round_3_matches(), {==}),
128        suffix_10(fuel))