def chunk_6

qasim-bend-kit@0.1.0.2 · proof/AES_NistCtr5ComposeProof.bend:188

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

188def chunk_6(+fuel: Nat) ->
189    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n) ==
190     Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n) : List<&2, U32>}:
191    Equal.trans(List<&2, U32>,
192        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_6(), Key.words_60(), 7n),
193        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
194        Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
195        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_6(), Key.words_60(), 7n,
196            Block.state_7(), 8n, Block.round_7_matches(), {==}),
197        Equal.trans(List<&2, U32>,
198            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_7(), Key.words_60(), 8n),
199            Core.aes_rounds.go(1n+(fuel), Block.state_8(), Key.words_60(), 9n),
200            Core.aes_rounds.go(fuel, Block.state_9(), Key.words_60(), 10n),
201            Trace.rounds_step_at(1n+(fuel), Block.state_7(), Key.words_60(), 8n,
202                Block.state_8(), 9n, Block.round_8_matches(), {==}),
203            Trace.rounds_step_at(fuel, Block.state_8(), Key.words_60(), 9n,
204                Block.state_9(), 10n, Block.round_9_matches(), {==})))