~/jendhub

def suffix_7

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

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

75def suffix_7(+fuel: Nat) ->
76    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n) ==
77     Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
78    Equal.trans(List<&2, U32>,
79        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n),
80        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_7(), Key.words_60(), 8n),
81        Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
82        Trace.rounds_step_at(1n+(1n+(1n+(1n+(1n+(1n+(fuel)))))), Block.state_6(), Key.words_60(), 7n,
83            Block.state_7(), 8n, Block.round_7_matches(), {==}),
84        suffix_6(fuel))

Uses (12)

Used by (1)