AESIdentityProof.hex_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 39-58 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=39&end_line=58

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_EnvelopeProof.bend as Encoding

def hex_injective(+first: List<&2, U32>, +second: List<&2, U32>,
    first_valid: {AES.bytes_valid(first) == True{} : Bool},
    second_valid: {AES.bytes_valid(second) == True{} : Bool},
    same: {AES.hex_bytes(first) == AES.hex_bytes(second) : String}) ->
    {first == second : List<&2, U32>}:
    decoded = Equal.trans(Maybe<&2, List<&2, U32>>,
        Some{Encoding.aes_hex_mask_bytes(first)}, AES.decode_hex(AES.hex_bytes(first)),
        Some{Encoding.aes_hex_mask_bytes(second)},
        Equal.sym(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
            Some{Encoding.aes_hex_mask_bytes(first)}, Encoding.aes_decode_hex_bytes(first)),
        Equal.trans(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
            AES.decode_hex(AES.hex_bytes(second)), Some{Encoding.aes_hex_mask_bytes(second)},
            Equal.cong(String, Maybe<&2, List<&2, U32>>, AES.decode_hex,
                AES.hex_bytes(first), AES.hex_bytes(second), same), Encoding.aes_decode_hex_bytes(second)))
    masks_equal = Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, decoded_or_empty,
        Some{Encoding.aes_hex_mask_bytes(first)}, Some{Encoding.aes_hex_mask_bytes(second)}, decoded)
    Equal.trans(List<&2, U32>, first, Encoding.aes_hex_mask_bytes(first), second,
        Equal.sym(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), first, mask_identity(first, first_valid)),
        Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), Encoding.aes_hex_mask_bytes(second),
            second, masks_equal, mask_identity(second, second_valid)))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.sym
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decode_hex
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_decode_hex_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=decoded_or_empty
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=mask_identity