AESNistTamperVectorProof.checkpoint_changed_ciphertext_rejected: 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 108-112 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=108&end_line=112

import Base
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 checkpoint_changed_ciphertext_rejected() ->
    {Obs.decrypt_expanded(Key.words_60(), changed_ciphertext_aad(), changed_ciphertext_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}:
    Obs.finish_auth(Key.words_60(), changed_ciphertext_aad(), changed_ciphertext_envelope(),
        changed_ciphertext_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}},
        checkpoint_changed_ciphertext_tag(), {==}, {==})

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/libs/AES256GCM.bend&name=Error
  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=decrypt_expanded
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&name=finish_auth
  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_computed_tag
  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_tag