AESIdentityProof.encode_injective: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend as AESIdentityProof
Lines 103-138 of qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&start_line=103&end_line=138

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend as Constructor
import qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend as Known

def encode_injective(+first: AES.Envelope, +second: AES.Envelope,
    same: {AES.encode(first) == AES.encode(second) : String}) -> {first == second : AES.Envelope}:
    match first second:
        case AES.Envelope{AES.Nonce{+bytes_a, +size_a, +nonce_valid_a},
                 +cipher_a, AES.Tag{+tag_bytes_a, +tag_size_a, +tag_valid_a}, +valid_a}
             AES.Envelope{AES.Nonce{+bytes_b, +size_b, +nonce_valid_b},
                 +cipher_b, AES.Tag{+tag_bytes_b, +tag_size_b, +tag_valid_b}, +valid_b}:
            +size_a_copy = size_a
            +size_b_copy = size_b
            +nonce_valid_a_copy = nonce_valid_a
            +nonce_valid_b_copy = nonce_valid_b
            +nonce_a = {AES.Nonce{bytes_a, size_a_copy, nonce_valid_a_copy} : AES.Nonce}
            +nonce_b = {AES.Nonce{bytes_b, size_b_copy, nonce_valid_b_copy} : AES.Nonce}
            +tag_a = {AES.Tag{tag_bytes_a, tag_size_a, tag_valid_a} : AES.Tag}
            +tag_b = {AES.Tag{tag_bytes_b, tag_size_b, tag_valid_b} : AES.Tag}
            +parts_same = fields_equal(first, second, same)
            nonce_hex = Equal.cong(List<&2, String>, String, parts => field_text(1n, parts),
                fields(first), fields(second), parts_same)
            tag_hex = Equal.cong(List<&2, String>, String, parts => field_text(2n, parts),
                fields(first), fields(second), parts_same)
            cipher_hex = Equal.cong(List<&2, String>, String, parts => field_text(3n, parts),
                fields(first), fields(second), parts_same)
            nonce_bytes_same = hex_injective(bytes_a, bytes_b, nonce_valid_a_copy, nonce_valid_b_copy,
                fixed_hex_equal(12n, bytes_a, bytes_b, size_a_copy, size_b_copy, nonce_hex))
            tag_bytes_same = hex_injective(tag_bytes_a, tag_bytes_b, tag_valid_a, tag_valid_b,
                fixed_hex_equal(16n, tag_bytes_a, tag_bytes_b, tag_size_a, tag_size_b, tag_hex))
            cipher_same = hex_injective(cipher_a, cipher_b, valid_a, valid_b, cipher_hex)
            nonce_same = Constructor.nonce_equal(bytes_a, size_a_copy, nonce_valid_a_copy, bytes_b,
                nonce_bytes_same, size_b_copy, nonce_valid_b_copy)
            tag_same = Known.tag_equal(tag_bytes_a, tag_size_a, tag_valid_a, tag_bytes_b,
                tag_bytes_same, tag_size_b, tag_valid_b)
            fields_same = Known.envelope_equal(nonce_a, cipher_a, tag_a, valid_a,
                cipher_b, tag_b, cipher_same, tag_same, valid_b)
            Equal.trans(AES.Envelope, first, AES.Envelope{nonce_a, cipher_b, tag_b, valid_b}, second,
                fields_same, Equal.cong(AES.Nonce, AES.Envelope,
                    nonce => AES.Envelope{nonce, cipher_b, tag_b, valid_b}, nonce_a, nonce_b, nonce_same))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Envelope
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=Tag
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend&name=nonce_equal
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=field_text
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=fields
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=fields_equal
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=fixed_hex_equal
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=hex_injective
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&name=envelope_equal
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_KnownAnswerProof.bend&name=tag_equal