def finish_tag

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

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

46def finish_tag(+words: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>,
47    +auth: List<&2, U32>, +mask: List<&2, U32>, +tag: List<&2, U32>,
48    auth_matches: {Core.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>},
49    mask_matches: {Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce)) == mask : List<&2, U32>},
50    xor_matches: {tag_from_parts(auth, mask) == tag : List<&2, U32>}) ->
51    {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>}:
52    Equal.trans(List<&2, U32>, Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)),
53        tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))), tag,
54        tag_shape(words, nonce, aad, bytes),
55        Equal.trans(List<&2, U32>,
56            tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
57            tag_from_parts(auth, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))), tag,
58            Equal.cong(List<&2, U32>, List<&2, U32>, value => tag_from_parts(value, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
59                Core.ghash_auth_expanded(words, aad, bytes), auth, auth_matches),
60            Equal.trans(List<&2, U32>, tag_from_parts(auth, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
61                tag_from_parts(auth, mask), tag,
62                Equal.cong(List<&2, U32>, List<&2, U32>, value => tag_from_parts(auth, value),
63                    Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce)), mask, mask_matches), xor_matches)))