~/jendhub

def full_rounds_match

qasim-bend-kit@0.1.0.2 · proof/AES_NistHashBlockComposeProof.bend:238

import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend as AESNistHashBlockComposeProof
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_NistHashBlockProof.bend as Block

238def full_rounds_match(+fuel: Nat) ->
239    {Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n) == Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n) : List<&2, U32>}:
240    Equal.trans(List<&2, U32>,
241        Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), Core.aes_rounds.go(fuel, Block.state_13(), Key.words_60(), 14n),
242        Equal.trans(List<&2, U32>,
243            Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))))))))), Block.state_0(), Key.words_60(), 1n), Core.aes_rounds.go(1n+(1n+(1n+(1n+(1n+(1n+(1n+(fuel))))))), Block.state_6(), Key.words_60(), 7n), Core.aes_rounds.go(1n+(fuel), Block.state_12(), Key.words_60(), 13n), rounds_0_to_6(fuel), rounds_6_to_12(fuel)),
244        suffix_1(fuel))

Uses (13)

Used by (1)