def checkpoint_empty_authenticated

qasim-bend-kit@0.1.0.2 · proof/AES_NistVectorProof.bend:55

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

55def checkpoint_empty_authenticated() ->
56    {Obs.decrypt_expanded(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty()) == Done{empty_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
57    Obs.finish_auth(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty(),
58        empty_tag(), True{}, Done{empty_plaintext()},
59        Obs.tag_parameters(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty(),
60            AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_ciphertext(), empty_tag(),
61            {==}, {==}, checkpoint_empty_tag()), {==},
62        Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_empty(),
63            AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_ciphertext(), empty_plaintext(),
64            {==}, {==}, checkpoint_empty_plaintext()))