def hex_injective

qasim-bend-kit@0.1.0.2 · proof/AES_IdentityProof.bend:39

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

39def hex_injective(+first: List<&2, U32>, +second: List<&2, U32>,
40    first_valid: {AES.bytes_valid(first) == True{} : Bool},
41    second_valid: {AES.bytes_valid(second) == True{} : Bool},
42    same: {AES.hex_bytes(first) == AES.hex_bytes(second) : String}) ->
43    {first == second : List<&2, U32>}:
44    decoded = Equal.trans(Maybe<&2, List<&2, U32>>,
45        Some{Encoding.aes_hex_mask_bytes(first)}, AES.decode_hex(AES.hex_bytes(first)),
46        Some{Encoding.aes_hex_mask_bytes(second)},
47        Equal.sym(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
48            Some{Encoding.aes_hex_mask_bytes(first)}, Encoding.aes_decode_hex_bytes(first)),
49        Equal.trans(Maybe<&2, List<&2, U32>>, AES.decode_hex(AES.hex_bytes(first)),
50            AES.decode_hex(AES.hex_bytes(second)), Some{Encoding.aes_hex_mask_bytes(second)},
51            Equal.cong(String, Maybe<&2, List<&2, U32>>, AES.decode_hex,
52                AES.hex_bytes(first), AES.hex_bytes(second), same), Encoding.aes_decode_hex_bytes(second)))
53    masks_equal = Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, decoded_or_empty,
54        Some{Encoding.aes_hex_mask_bytes(first)}, Some{Encoding.aes_hex_mask_bytes(second)}, decoded)
55    Equal.trans(List<&2, U32>, first, Encoding.aes_hex_mask_bytes(first), second,
56        Equal.sym(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), first, mask_identity(first, first_valid)),
57        Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(first), Encoding.aes_hex_mask_bytes(second),
58            second, masks_equal, mask_identity(second, second_valid)))