def suffix_4

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

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

42def suffix_4(+fuel: Nat) ->
43    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n) ==
44     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
45    Equal.trans(List<&2, U32>,
46        Core.aes_rounds.go(1n+(1n+(1n+(1n+(fuel)))), Block.state_9(), Key.words_60(), 10n),
47        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_10(), Key.words_60(), 11n),
48        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
49        Trace.rounds_step_at(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n,
50            Block.state_10(), 11n, Block.round_10_matches(), {==}),
51        suffix_3(fuel))