def chunk_3

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

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

170def chunk_3(+fuel: Nat) ->
171    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n) ==
172     Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n) : List<&2, U32>}:
173    Equal.trans(List<&2, U32>,
174        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_3(), Key.words_60(), 4n),
175        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),
176        Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),
177        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_3(), Key.words_60(), 4n,
178            Block.state_4(), 5n, Block.round_4_matches(), {==}),
179        Equal.trans(List<&2, U32>,
180            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_4(), Key.words_60(), 5n),
181            Core.aes_rounds.go(1n+(fuel), Block.state_5(), Key.words_60(), 6n),
182            Core.aes_rounds.go(fuel, Block.state_6(), Key.words_60(), 7n),
183            Trace.rounds_step_at(1n+(fuel), Block.state_4(), Key.words_60(), 5n,
184                Block.state_5(), 6n, Block.round_5_matches(), {==}),
185            Trace.rounds_step_at(fuel, Block.state_5(), Key.words_60(), 6n,
186                Block.state_6(), 7n, Block.round_6_matches(), {==})))