~/jendhub

def suffix_8

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

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

86def suffix_8(+fuel: Nat) ->
87    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n) ==
88     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
89    Equal.trans(List<&2, U32>,
90        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))))), Block.state_5(), Key.words_60(), 6n),
91        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),
92        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
93        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_5(), Key.words_60(), 6n,
94            Block.state_6(), 7n, Block.round_6_matches(), {==}),
95        suffix_7(fuel))

Uses (12)

Used by (1)