def chunk_9

qasim-bend-kit@0.1.0.2 · proof/AES_NistCtr3ComposeProof.bend:206

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

206def chunk_9(+fuel: Nat) ->
207    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n) ==
208     Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n) : List<&2, U32>}:
209    Equal.trans(List<&2, U32>,
210        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_9(), Key.words_60(), 10n),
211        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),
212        Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),
213        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_9(), Key.words_60(), 10n,
214            Block.state_10(), 11n, Block.round_10_matches(), {==}),
215        Equal.trans(List<&2, U32>,
216            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_10(), Key.words_60(), 11n),
217            Core.aes_rounds.go(1n+(fuel), Block.state_11(), Key.words_60(), 12n),
218            Core.aes_rounds.go(fuel, Block.state_12(), Key.words_60(), 13n),
219            Trace.rounds_step_at(1n+(fuel), Block.state_10(), Key.words_60(), 11n,
220                Block.state_11(), 12n, Block.round_11_matches(), {==}),
221            Trace.rounds_step_at(fuel, Block.state_11(), Key.words_60(), 12n,
222                Block.state_12(), 13n, Block.round_12_matches(), {==})))