~/jendhub

def suffix_10

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

import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3ComposeProof.bend as AESNistCtr3ComposeProof
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

108def suffix_10(+fuel: Nat) ->
109    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n) ==
110     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
111    Equal.trans(List<&2, U32>,
112        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))), Block.state_3(), Key.words_60(), 4n),
113        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_4(), Key.words_60(), 5n),
114        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
115        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))), Block.state_3(), Key.words_60(), 4n,
116            Block.state_4(), 5n, Block.round_4_matches(), {==}),
117        suffix_9(fuel))

Uses (12)

Used by (1)