def decrypt_auth_shape

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:200

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

200def decrypt_auth_shape(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope) ->
201    {decrypt_expanded(words, aad, envelope) == AES.decrypt_auth_result(words, envelope,
202        auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))) : Result<&2, &2, AES.Error, List<&2, U32>>}:
203    match envelope:
204        case AES.Envelope{nonce, bytes, tag, valid}:
205            match tag:
206                case AES.Tag{tag_bytes, tag_size, tag_valid}: {==}