proof/AES_NistBlockProof.bend checks
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockProof.bend as AES_NistBlockProof
3 imports
import Base import ../libs/AES256GCMCore.bend as Core import ./AES_NistKeyScheduleProof.bend as Key
Definitions
def block source · line 6 · raw
List<&2, U32>
Concrete stages of the NIST J0 block, checked by the independent kernel.
def state_0 source · line 9 · raw
List<&2, U32>
def state_1 source · line 12 · raw
List<&2, U32>
def state_2 source · line 15 · raw
List<&2, U32>
def state_3 source · line 18 · raw
List<&2, U32>
def state_4 source · line 21 · raw
List<&2, U32>
def state_5 source · line 24 · raw
List<&2, U32>
def state_6 source · line 27 · raw
List<&2, U32>
def state_7 source · line 30 · raw
List<&2, U32>
def state_8 source · line 33 · raw
List<&2, U32>
def state_9 source · line 36 · raw
List<&2, U32>
def state_10 source · line 39 · raw
List<&2, U32>
def state_11 source · line 42 · raw
List<&2, U32>
def state_12 source · line 45 · raw
List<&2, U32>
def state_13 source · line 48 · raw
List<&2, U32>
def result source · line 51 · raw
List<&2, U32>
def initial_matches source · line 54 · 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 58 · 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 62 · 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 66 · 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 70 · 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 74 · 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 78 · 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 82 · 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 86 · 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 90 · 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 94 · 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 98 · 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 102 · 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 106 · 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 110 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_final_round(state_13, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60) == result : List<&2, U32>}