def suffix_13

qasim-bend-kit@0.1.0.2 · proof/AES_NistCtr4ComposeProof.bend:141

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

141def suffix_13(+fuel: Nat) ->
142    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) ==
143     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
144    Equal.trans(List<&2, U32>,
145        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n),
146        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),
147        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
148        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_0(), Key.words_60(), 1n,
149            Block.state_1(), 2n, Block.round_1_matches(), {==}),
150        suffix_12(fuel))