def decrypt_auth_tag_canonical

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:497

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_TagCompareProof.bend as TagCompareProof

497def decrypt_auth_tag_canonical(+words: List<&2, U32>,
498    +nonce: List<&2, U32>, +aad: List<&2, U32>,
499    +ciphertext: List<&2, U32>, +envelope: AES.Envelope, +tag: AES.Tag,
500    canonical: {AES.tag_bytes(tag) == Core.gcm_tag_bytes(
501        Core.gcm_tag_output(words, nonce, aad, ciphertext)) : List<&2, U32>}) ->
502    {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope,
503        tag) == AES.decrypt_auth_result(words, envelope, True{}) :
504        Result<&2, &2, AES.Error, List<&2, U32>>}:
505    match tag:
506        case AES.Tag{bytes, size, valid}:
507            Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
508                ok => AES.decrypt_auth_result(words, envelope, ok),
509                AES.bytes_equal_full_scan(bytes, Core.gcm_tag_bytes(
510                    Core.gcm_tag_output(words, nonce, aad, ciphertext))),
511                True{}, TagCompareProof.equal_of_equal(bytes,
512                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
513                        aad, ciphertext)), canonical))