def tag_shape

qasim-bend-kit@0.1.0.2 · proof/AES_NistTagProof.bend:18

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

18def tag_shape(+words: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>) ->
19    {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) ==
20     tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))) : List<&2, U32>}:
21    match nonce:
22        case Nil{}: {==}
23        case head <> tail: {==}