def aes_parse_decoded_hex_map

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:904

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

904def aes_parse_decoded_hex_map(+nonce: List<&2, U32>,
905    +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
906    nonce_size: {List.length(&2, U32, nonce) == 12n : Nat},
907    tag_size: {List.length(&2, U32, tag) == 16n : Nat}) ->
908    {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
909        AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
910            AES.decode_hex(AES.hex_bytes(tag)),
911            AES.decode_hex(AES.hex_bytes(ciphertext)))) ==
912     Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
913        "." ++ AES.hex_bytes(ciphertext)} :
914        Result<&2, &2, AES.Error, String>}:
915    +n = aes_hex_mask_bytes(nonce)
916    +t = aes_hex_mask_bytes(tag)
917    +c = aes_hex_mask_bytes(ciphertext)
918    nonce_step = Equal.cong(Maybe<&2, List<&2, U32>>,
919        Result<&2, &2, AES.Error, String>,
920        value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
921            AES.encode, AES.parse_decoded_hex(value,
922                AES.decode_hex(AES.hex_bytes(tag)),
923                AES.decode_hex(AES.hex_bytes(ciphertext)))),
924        AES.decode_hex(AES.hex_bytes(nonce)), Some{n},
925        aes_decode_hex_bytes(nonce))
926    tag_step = Equal.cong(Maybe<&2, List<&2, U32>>,
927        Result<&2, &2, AES.Error, String>,
928        value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
929            AES.encode, AES.parse_decoded_hex(Some{n}, value,
930                AES.decode_hex(AES.hex_bytes(ciphertext)))),
931        AES.decode_hex(AES.hex_bytes(tag)), Some{t},
932        aes_decode_hex_bytes(tag))
933    cipher_step = Equal.cong(Maybe<&2, List<&2, U32>>,
934        Result<&2, &2, AES.Error, String>,
935        value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
936            AES.encode, AES.parse_decoded_hex(Some{n}, Some{t}, value)),
937        AES.decode_hex(AES.hex_bytes(ciphertext)), Some{c},
938        aes_decode_hex_bytes(ciphertext))
939    first_two = Equal.trans(Result<&2, &2, AES.Error, String>,
940        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
941            AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
942                AES.decode_hex(AES.hex_bytes(tag)),
943                AES.decode_hex(AES.hex_bytes(ciphertext)))),
944        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
945            AES.parse_decoded_hex(Some{n},
946                AES.decode_hex(AES.hex_bytes(tag)),
947                AES.decode_hex(AES.hex_bytes(ciphertext)))),
948        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
949            AES.parse_decoded_hex(Some{n}, Some{t},
950                AES.decode_hex(AES.hex_bytes(ciphertext)))),
951        nonce_step, tag_step)
952    all_three = Equal.trans(Result<&2, &2, AES.Error, String>,
953        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
954            AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
955                AES.decode_hex(AES.hex_bytes(tag)),
956                AES.decode_hex(AES.hex_bytes(ciphertext)))),
957        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
958            AES.parse_decoded_hex(Some{n}, Some{t},
959                AES.decode_hex(AES.hex_bytes(ciphertext)))),
960        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
961            AES.parse_decoded_hex(Some{n}, Some{t}, Some{c})),
962        first_two, cipher_step)
963    Equal.trans(Result<&2, &2, AES.Error, String>,
964        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
965            AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
966                AES.decode_hex(AES.hex_bytes(tag)),
967                AES.decode_hex(AES.hex_bytes(ciphertext)))),
968        Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
969            AES.parse_decoded_hex(Some{n}, Some{t}, Some{c})),
970        Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
971            "." ++ AES.hex_bytes(ciphertext)},
972        all_three,
973        aes_parse_decoded_checked_map(nonce, tag, ciphertext,
974            nonce_size, tag_size))