proof/AES_KnownAnswerProof.bend checks

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

5 imports

import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_CoreTagProof.bend as Fields
import ./AES_CertificateProof.bend as Certificate

Definitions

def tag_equal source · line 7 · raw

@+bytes:List<&2, U32> -> @+size:{List.length(&2, U32, bytes) == 16n : Nat} -> @+valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @+expected:List<&2, U32> -> @same:{bytes == expected : List<&2, U32>} -> @+expected_size:{List.length(&2, U32, expected) == 16n : Nat} -> @+expected_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(expected) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{bytes, size, valid} == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{expected, expected_size, expected_valid} : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag}

def envelope_equal source · line 33 · raw

@+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+ciphertext:List<&2, U32> -> @+tag:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag -> @+valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(ciphertext) == True{} : Bool} -> @+expected_ciphertext:List<&2, U32> -> @+expected_tag:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag -> @same_ciphertext:{ciphertext == expected_ciphertext : List<&2, U32>} -> @same_tag:{tag == expected_tag : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag} -> @+expected_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(expected_ciphertext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{nonce, ciphertext, tag, valid} == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{nonce, expected_ciphertext, expected_tag, expected_valid} : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope}

def output_matches source · line 61 · raw

@+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> @+ciphertext:List<&2, U32> -> @+tag_bytes:List<&2, U32> -> @ciphertext_matches:{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_ciphertext(output) == ciphertext : List<&2, U32>} -> @tag_matches:{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_tag(output) == tag_bytes : List<&2, U32>} -> @+tag_size:{List.length(&2, U32, tag_bytes) == 16n : Nat} -> @+tag_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(tag_bytes) == True{} : Bool} -> @+ciphertext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(ciphertext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_output_from_gcm(nonce, output) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{nonce, ciphertext, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

def encrypt_matches source · line 97 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @+tag_bytes:List<&2, U32> -> @aad_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @ciphertext_matches:{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid_output(key, nonce, aad, plaintext)) == ciphertext : List<&2, U32>} -> @tag_matches:{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_CoreTagProof.output_tag(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid_output(key, nonce, aad, plaintext)) == tag_bytes : List<&2, U32>} -> @+tag_size:{List.length(&2, U32, tag_bytes) == 16n : Nat} -> @+tag_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(tag_bytes) == True{} : Bool} -> @+ciphertext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(ciphertext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope{nonce, ciphertext, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}