AESNistVectorProof.aad_only_encrypt: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AESNistVectorProof
Lines 168-173 of qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&start_line=168&end_line=173

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/proof/AES_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as Obs

def aad_only_encrypt() ->
    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), aad_only_aad(), aad_only_plaintext())) ==
     L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_aad_only()}) : List<&2, U32>}:
    Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
        aad_only_aad(), aad_only_plaintext(), Key.words_60(), aad_only_ciphertext(), aad_only_tag(),
        {==}, {==}, checkpoint_nist_schedule(), checkpoint_aad_only_ciphertext(), checkpoint_aad_only_tag())

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  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_aad_only
  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/LAWS.bend&name=aes256gcm_nist_key
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/LAWS.bend&name=aes256gcm_nist_nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend&name=words_60
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=finish_encrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=aad_only_aad
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=aad_only_ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=aad_only_plaintext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=aad_only_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=checkpoint_aad_only_ciphertext
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=checkpoint_aad_only_tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=checkpoint_nist_schedule