def chunk_0

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

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

152def chunk_0(+fuel: Nat) ->
153    {Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n) ==
154     Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n) : List<&2, U32>}:
155    Equal.trans(List<&2, U32>,
156        Core.aes_rounds.go(1n+(1n+(1n+(fuel))), Block.state_0(), Key.words_60(), 1n),
157        Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),
158        Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),
159        Trace.rounds_step_at(1n+(1n+(fuel)), Block.state_0(), Key.words_60(), 1n,
160            Block.state_1(), 2n, Block.round_1_matches(), {==}),
161        Equal.trans(List<&2, U32>,
162            Core.aes_rounds.go(1n+(1n+(fuel)), Block.state_1(), Key.words_60(), 2n),
163            Core.aes_rounds.go(1n+(fuel), Block.state_2(), Key.words_60(), 3n),
164            Core.aes_rounds.go(fuel, Block.state_3(), Key.words_60(), 4n),
165            Trace.rounds_step_at(1n+(fuel), Block.state_1(), Key.words_60(), 2n,
166                Block.state_2(), 3n, Block.round_2_matches(), {==}),
167            Trace.rounds_step_at(fuel, Block.state_2(), Key.words_60(), 3n,
168                Block.state_3(), 4n, Block.round_3_matches(), {==})))