proof/AES_EncryptProof.bend checks

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

8 imports

import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_ZipLengthProof.bend as ZipLengthProof
import ./AES_CoreTagProof.bend as CoreTagProof
import ./AES_MaskedXorProof.bend as MaskedXorProof
import ./AES_LengthLimitProof.bend as LengthLimitProof
import ./AES_TagCompareProof.bend as TagCompareProof

Types

type TagContext source · line 10 · raw

Data

TagContext

@words:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> TagContext

Definitions

def result_ciphertext source · line 18 · raw

@fallback:List<&2, U32> -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> List<&2, U32>

def output_tag_context source · line 24 · raw

@output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> TagContext

def tag_for_context source · line 30 · raw

@context:TagContext -> List<&2, U32>

def output_tag_matches_context source · line 36 · raw

@+output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> {0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_tag(output) == tag_for_context(output_tag_context(output)) : List<&2, U32>}

def raw_output_tag_canonical source · line 44 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_tag(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_encrypt_raw(key, nonce, aad, plaintext)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(key), nonce, aad, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_encrypt_raw(key, nonce, aad, plaintext)))) : List<&2, U32>}

def result_tag_bytes source · line 63 · raw

@fallback:List<&2, U32> -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> List<&2, U32>

def valid_output_ciphertext_length source · line 69 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_from_gcm_checked(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid_output(key, nonce, aad, plaintext)))) == List.length(&2, U32, plaintext) : Nat}

def encrypt_checked_with_flags source · line 79 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+aad_flag:Bool -> @+plaintext_flag:Bool -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == aad_flag : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == plaintext_flag : Bool} -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_checked(key, nonce, aad, plaintext, aad_flag, plaintext_flag) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

def successful_encrypt_aad_valid source · line 123 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+aad_flag:Bool -> @+plaintext_flag:Bool -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == aad_flag : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == plaintext_flag : Bool} -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {aad_flag == True{} : Bool}

def successful_encrypt_plaintext_valid source · line 149 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+aad_flag:Bool -> @+plaintext_flag:Bool -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == aad_flag : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == plaintext_flag : Bool} -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {plaintext_flag == True{} : Bool}

def result_ciphertext_length source · line 190 · raw

@result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> Nat

def successful_encrypt_preserves_length source · line 197 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope)) == List.length(&2, U32, plaintext) : Nat}

def successful_encrypt_ciphertext_matches_gcm source · line 229 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid_output(key, nonce, aad, plaintext)) : List<&2, U32>}

def successful_encrypt_tag_matches_gcm source · line 256 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_tag(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid_output(key, nonce, aad, plaintext)) : List<&2, U32>}

def successful_encrypt_tag_canonical source · line 282 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @+plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), aad, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))) : List<&2, U32>}

def successful_encrypt_ciphertext_matches_ctr source · line 323 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(plaintext, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce))))) : List<&2, U32>}

def successful_encrypt_ciphertext_valid source · line 350 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope)) == True{} : Bool}

def successful_encrypt_ctr_decrypts source · line 364 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @+plaintext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_raw(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope)) == plaintext : List<&2, U32>}

def result_nonce source · line 406 · raw

@fallback:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce

def output_nonce source · line 412 · raw

@+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> {result_nonce(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_output_from_gcm(nonce, output)) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def valid_nonce source · line 421 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> {result_nonce(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid(key, nonce, aad, plaintext)) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def checked_nonce source · line 428 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @aad_ok:Bool -> @plaintext_ok:Bool -> {result_nonce(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_checked(key, nonce, aad, plaintext, aad_ok, plaintext_ok)) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def encrypt_nonce source · line 438 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> {result_nonce(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def preserves_nonce source · line 445 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope) == nonce : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def successful_encrypt_envelope_tag_canonical source · line 464 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)), aad, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))) : List<&2, U32>}

def decrypt_auth_tag_canonical source · line 497 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tag:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag -> @canonical:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(tag) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, nonce, aad, ciphertext)) : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope, tag) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, True{}) : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def successful_encrypt_decrypt_authenticated source · line 515 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @+plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_authenticated(key, aad, envelope) == Done{plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def successful_encrypt_decrypt_roundtrip source · line 565 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, envelope) == Done{plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def output_is_done source · line 612 · raw

@+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> {Result.is_done(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_output_from_gcm(nonce, output)) == True{} : Bool}

def valid_is_done source · line 617 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> {Result.is_done(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid(key, nonce, aad, plaintext)) == True{} : Bool}

def valid_input_is_done source · line 624 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> {Result.is_done(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}