proof/AES_TraceBridgeProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_TraceBridgeProof.bend as AES_TraceBridgeProof

2 imports

import Base
import ../libs/AES256GCMCore.bend as Core

Definitions

def expand_input_matches source · line 7 · raw

@+fuel:Nat -> @+key:List<&2, U32> -> @+initial_words:List<&2, U32> -> @+expected:List<&2, U32> -> @initial_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_words(key) == initial_words : List<&2, U32>} -> @expanded_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, 8, 1, initial_words) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, 8, 1, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_words(key)) == expected : List<&2, U32>}

Substitute a certified initial word list with a symbolic fuel parameter. The public bridge below compares function aliases before applying the key, avoiding normalization of all 52 rounds merely to compare the aliases.

def expand_key_matches source · line 17 · raw

@+fuel:Nat -> @+key:List<&2, U32> -> @+initial_words:List<&2, U32> -> @+expected:List<&2, U32> -> @+initial_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_words(key) == initial_words : List<&2, U32>} -> @+expanded_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, 8, 1, initial_words) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand_key(fuel, key) == expected : List<&2, U32>}

def expansion_alias source · line 26 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand == (+key => 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand_key(52n, key)) : @+key:List<&2, U32> -> List<&2, U32>}

def public_expansion_matches source · line 31 · raw

@+key:List<&2, U32> -> @+expected:List<&2, U32> -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand_key(52n, key) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(key) == expected : List<&2, U32>}