def raw_output_tag_canonical

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

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

44def raw_output_tag_canonical(+key: List<&2, U32>,
45    +nonce: List<&2, U32>, +aad: List<&2, U32>,
46    +plaintext: List<&2, U32>) ->
47    {CoreTagProof.output_tag(Core.gcm_encrypt_raw(key, nonce, aad,
48        plaintext)) == Core.gcm_tag_bytes(Core.gcm_tag_output(
49            Core.aes256_expand(key), nonce, aad,
50            CoreTagProof.output_ciphertext(Core.gcm_encrypt_raw(key, nonce,
51                aad, plaintext)))) : List<&2, U32>}:
52    +output = Core.gcm_encrypt_raw(key, nonce, aad, plaintext)
53    +context = output_tag_context(output)
54    +expected_context = {TagContext{Core.aes256_expand(key), nonce, aad,
55        CoreTagProof.output_ciphertext(output)} : TagContext}
56    context_eq: {context == expected_context : TagContext} = {==}
57    Equal.trans(List<&2, U32>, CoreTagProof.output_tag(output),
58        tag_for_context(context), tag_for_context(expected_context),
59        output_tag_matches_context(output),
60        Equal.cong(TagContext, List<&2, U32>, tag_for_context,
61            context, expected_context, context_eq))