AESNistInputProof.encrypt_inputs: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend as AESNistInputProof
Lines 5-26 of qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistInputProof.bend&start_line=5&end_line=26

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

# Transport fixture aliases before entering the encryption or decryption code.
# Equal fixtures must not force a fresh evaluation of the entire cipher.
def encrypt_inputs(+key: AES.SecretKey, +nonce: AES.Nonce,
    +aad: List<&2, U32>, +fixture_aad: List<&2, U32>,
    +plaintext: List<&2, U32>, +fixture_plaintext: List<&2, U32>,
    +expected: List<&2, U32>,
    aad_matches: {aad == fixture_aad : List<&2, U32>},
    plaintext_matches: {plaintext == fixture_plaintext : List<&2, U32>},
    computed: {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)) == expected : List<&2, U32>}) ->
    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) == expected : List<&2, U32>}:
    Equal.trans(List<&2, U32>,
        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)), expected,
        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, value, plaintext)),
            aad, fixture_aad, aad_matches),
        Equal.trans(List<&2, U32>,
            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, plaintext)),
            L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, fixture_plaintext)), expected,
            Equal.cong(List<&2, U32>, List<&2, U32>, value =>
                L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, fixture_aad, value)),
                plaintext, fixture_plaintext, plaintext_matches), computed))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_encrypt_observation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt