~/jendhub

def checkpoint_partial_block_authenticated

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

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

315def checkpoint_partial_block_authenticated() ->
316    {Obs.decrypt_expanded(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block()) == Done{partial_block_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
317    Obs.finish_auth(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block(),
318        partial_block_tag(), True{}, Done{partial_block_plaintext()},
319        Obs.tag_parameters(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block(),
320            AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext(), partial_block_tag(),
321            {==}, {==}, checkpoint_partial_block_tag()), {==},
322        Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_partial_block(),
323            AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext(), partial_block_plaintext(),
324            {==}, {==}, checkpoint_partial_block_plaintext()))

Uses (19)

Used by (1)