def output_nonce

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

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

412def output_nonce(+nonce: AES.Nonce, +output: Core.GcmOutput) ->
413    {result_nonce(nonce, AES.encrypt_output_from_gcm(nonce, output)) ==
414     nonce : AES.Nonce}:
415    match output:
416        case Core.GcmOutput{+ciphertext, ciphertext_valid,
417            tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
418            tag_matches}:
419            {==}