AES256GCMCore.GcmOutput: type of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as AES256GCMCore
Lines 628-641 of qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&start_line=628&end_line=641

import Base

type GcmOutput is Data:
    GcmOutput{
        ciphertext: List<&2, U32>,
        ciphertext_valid: {gcm_bytes_valid(ciphertext) == True{} : Bool},
        tag_bytes: List<&2, U32>,
        tag_valid: {gcm_bytes_valid(tag_bytes) == True{} : Bool},
        tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
        tag_words: List<&2, U32>,
        tag_nonce: List<&2, U32>,
        tag_aad: List<&2, U32>,
        tag_matches: {tag_bytes == gcm_tag_bytes(
            gcm_tag_output(tag_words, tag_nonce, tag_aad, ciphertext)) :
            List<&2, U32>}
    }

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_tag_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_tag_output