AESNistTamperVectorProof.rejects_changed_ciphertext: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend as AESNistTamperVectorProof
Lines 114-117 of qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend&start_line=114&end_line=117

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
import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as V

def rejects_changed_ciphertext() ->
    {AES.decrypt(L.aes256gcm_nist_key(), changed_ciphertext_aad(), changed_ciphertext_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}:
    Obs.finish_decrypt(L.aes256gcm_nist_key(), changed_ciphertext_aad(), changed_ciphertext_envelope(),
        Key.words_60(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, V.checkpoint_nist_schedule(), checkpoint_changed_ciphertext_rejected())

Uses (12):
  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_key
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decrypt
  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_decrypt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend&name=changed_ciphertext_aad
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend&name=changed_ciphertext_envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend&name=checkpoint_changed_ciphertext_rejected
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend&name=checkpoint_nist_schedule