def encrypt_inputs

qasim-bend-kit@0.1.0.2 · proof/AES_NistInputProof.bend:5

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

5# Transport fixture aliases before entering the encryption or decryption code.
6# Equal fixtures must not force a fresh evaluation of the entire cipher.
7def encrypt_inputs(+key: AES.SecretKey, +nonce: AES.Nonce,
8    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
9    +plaintext: List<&2, U32>, +fixture_plaintext: List<&2, U32>,
10    +expected: List<&2, U32>,
11    aad_matches: {aad == fixture_aad : List<&2, U32>},
12    plaintext_matches: {plaintext == fixture_plaintext : List<&2, U32>},
13    computed: {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)) == expected : List<&2, U32>}) ->
14    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) == expected : List<&2, U32>}:
15    Equal.trans(List<&2, U32>,
16        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
17        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)), expected,
18        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
19            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, value, plaintext)),
20            aad, fixture_aad, aad_matches),
21        Equal.trans(List<&2, U32>,
22            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)),
23            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)), expected,
24            Equal.cong(List<&2, U32>, List<&2, U32>, value =>
25                L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, value)),
26                plaintext, fixture_plaintext, plaintext_matches), computed))