proof/AES_NistBlockComposeProof.bend checks
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockComposeProof.bend as AES_NistBlockComposeProof
6 imports
import Base import ../libs/AES256GCMCore.bend as Core import ./AES_NistKeyScheduleProof.bend as Key import ./AES_NistBlockProof.bend as Block import ./AES_TraceProof.bend as Trace import ./AES_BlockBridgeProof.bend as Bridge
Definitions
def suffix_1 source · line 10 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(1n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_12, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 13n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_2 source · line 20 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(2n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_11, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 12n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_3 source · line 31 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(3n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_10, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 11n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_4 source · line 42 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(4n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_9, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 10n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_5 source · line 53 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(5n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_8, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 9n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_6 source · line 64 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(6n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_7, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 8n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_7 source · line 75 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(7n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_8 source · line 86 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(8n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_5, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 6n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_9 source · line 97 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(9n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_4, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 5n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_10 source · line 108 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(10n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_3, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 4n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_11 source · line 119 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(11n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_2, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 3n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_12 source · line 130 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(12n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_1, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 2n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def suffix_13 source · line 141 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def chunk_0 source · line 152 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(3n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_3, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 4n) : List<&2, U32>}
def chunk_3 source · line 170 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(3n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_3, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 4n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) : List<&2, U32>}
def chunk_6 source · line 188 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(3n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_9, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 10n) : List<&2, U32>}
def chunk_9 source · line 206 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(3n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_9, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 10n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_12, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 13n) : List<&2, U32>}
def rounds_0_to_6 source · line 224 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(7n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) : List<&2, U32>}
def rounds_6_to_12 source · line 231 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(7n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(1n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_12, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 13n) : List<&2, U32>}
def full_rounds_match source · line 238 · raw
@+fuel:Nat -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n+fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def full_nist_rounds_match source · line 246 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(0n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 14n) : List<&2, U32>}
def final_nist_block_match source · line 254 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_rounds.go(13n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.result : List<&2, U32>}
def expanded_block_matches source · line 261 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.block) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.result : List<&2, U32>}