~/jendhub

def full_nist_rounds_match

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

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

246def full_nist_rounds_match() ->
247    {Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
248    Equal.trans(List<&2, U32>,
249        Core.aes_rounds.go(13n, Block.state_0(), Key.words_60(), 1n),
250        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n),
251        Core.aes_rounds.go(0n, Block.state_13(), Key.words_60(), 14n),
252        Trace.rounds_fuel_matches(13n, 1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(0n))))))))))))), Block.state_0(), Key.words_60(), 1n, {==}), full_rounds_match(0n))

Uses (9)

Used by (1)