proof/AES_NistCtr2BlockProof.bend checks
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr2BlockProof.bend as AES_NistCtr2BlockProof
3 imports
import Base import ../libs/AES256GCMCore.bend as Core import ./AES_NistKeyScheduleProof.bend as Key
Definitions
def block source · line 7 · raw
List<&2, U32>
def state_0 source · line 10 · raw
List<&2, U32>
def state_1 source · line 13 · raw
List<&2, U32>
def state_2 source · line 16 · raw
List<&2, U32>
def state_3 source · line 19 · raw
List<&2, U32>
def state_4 source · line 22 · raw
List<&2, U32>
def state_5 source · line 25 · raw
List<&2, U32>
def state_6 source · line 28 · raw
List<&2, U32>
def state_7 source · line 31 · raw
List<&2, U32>
def state_8 source · line 34 · raw
List<&2, U32>
def state_9 source · line 37 · raw
List<&2, U32>
def state_10 source · line 40 · raw
List<&2, U32>
def state_11 source · line 43 · raw
List<&2, U32>
def state_12 source · line 46 · raw
List<&2, U32>
def state_13 source · line 49 · raw
List<&2, U32>
def result source · line 52 · raw
List<&2, U32>
def initial_matches source · line 55 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_add_key(block, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0n) == state_0 : List<&2, U32>}
def round_1_matches source · line 59 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_0, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 1n) == state_1 : List<&2, U32>}
def round_2_matches source · line 63 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_1, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 2n) == state_2 : List<&2, U32>}
def round_3_matches source · line 67 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_2, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 3n) == state_3 : List<&2, U32>}
def round_4_matches source · line 71 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_3, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 4n) == state_4 : List<&2, U32>}
def round_5_matches source · line 75 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_4, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 5n) == state_5 : List<&2, U32>}
def round_6_matches source · line 79 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_5, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 6n) == state_6 : List<&2, U32>}
def round_7_matches source · line 83 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_6, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 7n) == state_7 : List<&2, U32>}
def round_8_matches source · line 87 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_7, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 8n) == state_8 : List<&2, U32>}
def round_9_matches source · line 91 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_8, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 9n) == state_9 : List<&2, U32>}
def round_10_matches source · line 95 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_9, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 10n) == state_10 : List<&2, U32>}
def round_11_matches source · line 99 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_10, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 11n) == state_11 : List<&2, U32>}
def round_12_matches source · line 103 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_11, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 12n) == state_12 : List<&2, U32>}
def round_13_matches source · line 107 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_middle_round(state_12, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 13n) == state_13 : List<&2, U32>}
def final_matches source · line 111 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_final_round(state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60) == result : List<&2, U32>}