proof/AES_NistVectorProof.bend timeout
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AES_NistVectorProof
10 imports
import Base import ../LAWS.bend as L import ../libs/AES256GCM.bend as AES import ../libs/AES256GCMCore.bend as Core import ./AES_NistKeyScheduleProof.bend as Key import ./AES_NistObservationProof.bend as Obs import ./AES_NistTagProof.bend as TagProof import ./AES_NistHashBlockProof.bend as Hash import ./AES_NistCtrProof.bend as Ctr import ./AES_NistCtr2BlockProof.bend as Ctr2
Definitions
def checkpoint_nist_schedule source · line 12 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key)) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60 : List<&2, U32>}
def empty_aad source · line 16 · raw
List<&2, U32>
def empty_plaintext source · line 19 · raw
List<&2, U32>
def empty_ciphertext source · line 22 · raw
List<&2, U32>
def empty_tag source · line 25 · raw
List<&2, U32>
def empty_auth source · line 28 · raw
List<&2, U32>
def checkpoint_empty_ciphertext source · line 31 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), empty_plaintext)) == empty_ciphertext : List<&2, U32>}
def checkpoint_empty_ghash source · line 35 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistTagProof.auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, empty_aad, empty_ciphertext) == empty_auth : List<&2, U32>}
def checkpoint_empty_tag source · line 39 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), empty_aad, empty_ciphertext)) == empty_tag : List<&2, U32>}
def empty_encrypt source · line 44 · raw
{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce, empty_aad, empty_plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(Done{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_empty}) : List<&2, U32>}
def checkpoint_empty_plaintext source · line 51 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), empty_ciphertext) == empty_plaintext : List<&2, U32>}
def checkpoint_empty_authenticated source · line 55 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, empty_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_empty) == Done{empty_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def empty_decrypt source · line 66 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, empty_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_empty) == Done{empty_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def multiblock_aad source · line 72 · raw
List<&2, U32>
def multiblock_plaintext source · line 75 · raw
List<&2, U32>
def multiblock_ciphertext source · line 78 · raw
List<&2, U32>
def multiblock_tag source · line 81 · raw
List<&2, U32>
def multiblock_auth source · line 84 · raw
List<&2, U32>
def checkpoint_multiblock_plaintext_stream source · line 87 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, multiblock_plaintext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_64 : List<&2, U32>}
def checkpoint_multiblock_ciphertext_stream source · line 93 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, multiblock_ciphertext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_64 : List<&2, U32>}
def checkpoint_multiblock_ciphertext source · line 99 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), multiblock_plaintext)) == multiblock_ciphertext : List<&2, U32>}
def checkpoint_multiblock_ghash source · line 103 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistTagProof.auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, multiblock_aad, multiblock_ciphertext) == multiblock_auth : List<&2, U32>}
def checkpoint_multiblock_tag source · line 107 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), multiblock_aad, multiblock_ciphertext)) == multiblock_tag : List<&2, U32>}
def multiblock_encrypt source · line 112 · raw
{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce, multiblock_aad, multiblock_plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(Done{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_multiblock}) : List<&2, U32>}
def checkpoint_multiblock_plaintext source · line 119 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), multiblock_ciphertext) == multiblock_plaintext : List<&2, U32>}
def checkpoint_multiblock_authenticated source · line 123 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, multiblock_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_multiblock) == Done{multiblock_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def multiblock_decrypt source · line 134 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, multiblock_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_multiblock) == Done{multiblock_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def aad_only_aad source · line 140 · raw
List<&2, U32>
def aad_only_plaintext source · line 143 · raw
List<&2, U32>
def aad_only_ciphertext source · line 146 · raw
List<&2, U32>
def aad_only_tag source · line 149 · raw
List<&2, U32>
def aad_only_auth source · line 152 · raw
List<&2, U32>
def checkpoint_aad_only_ciphertext source · line 155 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_only_plaintext)) == aad_only_ciphertext : List<&2, U32>}
def checkpoint_aad_only_ghash source · line 159 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistTagProof.auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, aad_only_aad, aad_only_ciphertext) == aad_only_auth : List<&2, U32>}
def checkpoint_aad_only_tag source · line 163 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_only_aad, aad_only_ciphertext)) == aad_only_tag : List<&2, U32>}
def aad_only_encrypt source · line 168 · raw
{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce, aad_only_aad, aad_only_plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(Done{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_only}) : List<&2, U32>}
def checkpoint_aad_only_plaintext source · line 175 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_only_ciphertext) == aad_only_plaintext : List<&2, U32>}
def checkpoint_aad_only_authenticated source · line 179 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, aad_only_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_only) == Done{aad_only_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def aad_only_decrypt source · line 190 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, aad_only_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_only) == Done{aad_only_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def aad_and_multiblock_aad source · line 196 · raw
List<&2, U32>
def aad_and_multiblock_plaintext source · line 199 · raw
List<&2, U32>
def aad_and_multiblock_ciphertext source · line 202 · raw
List<&2, U32>
def aad_and_multiblock_tag source · line 205 · raw
List<&2, U32>
def aad_and_multiblock_auth source · line 208 · raw
List<&2, U32>
def checkpoint_aad_and_multiblock_plaintext_stream source · line 211 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, aad_and_multiblock_plaintext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_64 : List<&2, U32>}
def checkpoint_aad_and_multiblock_ciphertext_stream source · line 217 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, aad_and_multiblock_ciphertext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_64 : List<&2, U32>}
def checkpoint_aad_and_multiblock_ciphertext source · line 223 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_and_multiblock_plaintext)) == aad_and_multiblock_ciphertext : List<&2, U32>}
def checkpoint_aad_and_multiblock_ghash source · line 227 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistTagProof.auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, aad_and_multiblock_aad, aad_and_multiblock_ciphertext) == aad_and_multiblock_auth : List<&2, U32>}
def checkpoint_aad_and_multiblock_tag source · line 231 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_and_multiblock_aad, aad_and_multiblock_ciphertext)) == aad_and_multiblock_tag : List<&2, U32>}
def aad_and_multiblock_encrypt source · line 236 · raw
{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce, aad_and_multiblock_aad, aad_and_multiblock_plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(Done{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_and_multiblock}) : List<&2, U32>}
def checkpoint_aad_and_multiblock_plaintext source · line 243 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), aad_and_multiblock_ciphertext) == aad_and_multiblock_plaintext : List<&2, U32>}
def checkpoint_aad_and_multiblock_authenticated source · line 247 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, aad_and_multiblock_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_and_multiblock) == Done{aad_and_multiblock_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def aad_and_multiblock_decrypt source · line 258 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, aad_and_multiblock_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_aad_and_multiblock) == Done{aad_and_multiblock_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def partial_block_aad source · line 264 · raw
List<&2, U32>
def partial_block_plaintext source · line 267 · raw
List<&2, U32>
def partial_block_ciphertext source · line 270 · raw
List<&2, U32>
def partial_block_tag source · line 273 · raw
List<&2, U32>
def partial_block_auth source · line 276 · raw
List<&2, U32>
def checkpoint_partial_block_plaintext_stream source · line 279 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, partial_block_plaintext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_60 : List<&2, U32>}
def checkpoint_partial_block_ciphertext_stream source · line 285 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, partial_block_ciphertext), 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce)))) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtrProof.stream_60 : List<&2, U32>}
def checkpoint_partial_block_ciphertext source · line 291 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), partial_block_plaintext)) == partial_block_ciphertext : List<&2, U32>}
def checkpoint_partial_block_ghash source · line 295 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistTagProof.auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, partial_block_aad, partial_block_ciphertext) == partial_block_auth : List<&2, U32>}
def checkpoint_partial_block_tag source · line 299 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), partial_block_aad, partial_block_ciphertext)) == partial_block_tag : List<&2, U32>}
def partial_block_encrypt source · line 304 · raw
{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce, partial_block_aad, partial_block_plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(Done{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_partial_block}) : List<&2, U32>}
def checkpoint_partial_block_plaintext source · line 311 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_nonce), partial_block_ciphertext) == partial_block_plaintext : List<&2, U32>}
def checkpoint_partial_block_authenticated source · line 315 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, partial_block_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_partial_block) == Done{partial_block_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def partial_block_decrypt source · line 326 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, partial_block_aad, 0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_partial_block) == Done{partial_block_plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}