~/jendhub

def suffix_12

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

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

130def suffix_12(+fuel: Nat) ->
131    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n) ==
132     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
133    Equal.trans(List<&2, U32>,
134        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))))))), Block.state_1(), Key.words_60(), 2n),
135        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_2(), Key.words_60(), 3n),
136        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
137        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))), Block.state_1(), Key.words_60(), 2n,
138            Block.state_2(), 3n, Block.round_2_matches(), {==}),
139        suffix_11(fuel))

Uses (12)

Used by (1)