proof/AES_TraceProof.bend checks

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

2 imports

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

Definitions

def next_word source · line 7 · raw

@+i:U32 -> @rcon:U32 -> @+words:List<&2, U32> -> U32

def expand_step source · line 13 · raw

@+fuel:Nat -> @+i:U32 -> @+rcon:U32 -> @+words:List<&2, U32> -> @+next_words:List<&2, U32> -> @+next_rcon:U32 -> @words_match:{List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>} -> @rcon_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(1n+fuel, i, rcon, words) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, U32.add(i, 1), next_rcon, next_words) : List<&2, U32>}

def rounds_step source · line 29 · raw

@+fuel:Nat -> @+state:List<&2, U32> -> @+words:List<&2, U32> -> @+round:Nat -> @+next_state:List<&2, U32> -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state, words, round) == next_state : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(1n+fuel, state, words, round) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, next_state, words, Nat.add(round, 1n)) : List<&2, U32>}

def expand_step_at source · line 38 · raw

@+fuel:Nat -> @+i:U32 -> @+rcon:U32 -> @+words:List<&2, U32> -> @+next_words:List<&2, U32> -> @+next_rcon:U32 -> @+next_i:U32 -> @words_match:{List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>} -> @rcon_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32} -> @index_match:{U32.add(i, 1) == next_i : U32} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(1n+fuel, i, rcon, words) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, next_i, next_rcon, next_words) : List<&2, U32>}

def expand_step_number_at source · line 52 · raw

@+fuel:Nat -> @+remaining:Nat -> @fuel_match:{remaining == 1n+fuel : Nat} -> @+i:U32 -> @+rcon:U32 -> @+words:List<&2, U32> -> @+next_words:List<&2, U32> -> @+next_rcon:U32 -> @+next_i:U32 -> @words_match:{List.append(&2, U32, words, [next_word(i, rcon, words)]) == next_words : List<&2, U32>} -> @rcon_match:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rcon_kind(rcon, U32.is_eq(U32.mod(i, 8), 0)) == next_rcon : U32} -> @index_match:{U32.add(i, 1) == next_i : U32} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(remaining, i, rcon, words) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_expand.go(fuel, next_i, next_rcon, next_words) : List<&2, U32>}

def rounds_fuel_matches source · line 69 · raw

@+left:Nat -> @+right:Nat -> @+state:List<&2, U32> -> @+words:List<&2, U32> -> @+round:Nat -> @same:{left == right : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(left, state, words, round) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(right, state, words, round) : List<&2, U32>}

def rounds_step_at source · line 75 · raw

@+fuel:Nat -> @+state:List<&2, U32> -> @+words:List<&2, U32> -> @+round:Nat -> @+next_state:List<&2, U32> -> @+next_round:Nat -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state, words, round) == next_state : List<&2, U32>} -> @round_match:{Nat.add(round, 1n) == next_round : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(1n+fuel, state, words, round) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, next_state, words, next_round) : List<&2, U32>}