proof/AES_BlockBridgeProof.bend checks

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

2 imports

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

Definitions

def rounds_input_matches source · line 5 · raw

@+fuel:Nat -> @+words:List<&2, U32> -> @+block:List<&2, U32> -> @+initial:List<&2, U32> -> @+expected:List<&2, U32> -> @initial_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_add_key(block, words, 0n) == initial : List<&2, U32>} -> @rounds_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, initial, words, 1n) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_add_key(block, words, 0n), words, 1n) == expected : List<&2, U32>}

Keep fuel symbolic while substituting the certified initial state.

def expanded_block_from_initial source · line 20 · raw

@+words:List<&2, U32> -> @+block:List<&2, U32> -> @+initial:List<&2, U32> -> @+expected:List<&2, U32> -> @initial_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_add_key(block, words, 0n) == initial : List<&2, U32>} -> @rounds_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n, initial, words, 1n) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, block) == expected : List<&2, U32>}

Establish the public-function conversion while inputs remain symbolic. A concrete caller then compares identical public applications instead of unfolding all fourteen rounds to recognize the internal implementation.