def valid_encrypt

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:70

import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

70def valid_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
71                  +aad: List<&2, U32>, +plaintext: List<&2, U32>) ->
72    {L.aes256gcm_nist_encrypt_observation(AES.encrypt_valid(key, nonce, aad, plaintext)) ==
73     expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}:
74    from_ciphertext(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad,
75        Core.gcm_ctr_encrypt(Core.aes256_expand(AES.secret_key_bytes(key)),
76            AES.raw_nonce_bytes(nonce), plaintext))