type GcmOutput

qasim-bend-kit@0.1.0.2 · libs/AES256GCMCore.bend:628

import Base

628type GcmOutput is Data:
629    GcmOutput{
630        ciphertext: List<&2, U32>,
631        ciphertext_valid: {gcm_bytes_valid(ciphertext) == True{} : Bool},
632        tag_bytes: List<&2, U32>,
633        tag_valid: {gcm_bytes_valid(tag_bytes) == True{} : Bool},
634        tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
635        tag_words: List<&2, U32>,
636        tag_nonce: List<&2, U32>,
637        tag_aad: List<&2, U32>,
638        tag_matches: {tag_bytes == gcm_tag_bytes(
639            gcm_tag_output(tag_words, tag_nonce, tag_aad, ciphertext)) :
640            List<&2, U32>}
641    }