def aes_parse_decoded_masked_map

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

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

582def aes_parse_decoded_masked_map(+nonce: List<&2, U32>, +tag: List<&2, U32>,
583    +ciphertext: List<&2, U32>,
584    nonce_size: {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat},
585    tag_size: {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat},
586    nonce_valid: {AES.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool},
587    tag_valid: {AES.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool},
588    ciphertext_valid: {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}) ->
589    {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
590        AES.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag),
591            aes_hex_mask_bytes(ciphertext),
592            Some{nonce_size}, Some{tag_size}, Some{nonce_valid},
593            Some{tag_valid}, Some{ciphertext_valid})) ==
594     Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++ "." ++
595        AES.hex_bytes(ciphertext)} : Result<&2, &2, AES.Error, String>}:
596    +masked_nonce = aes_hex_mask_bytes(nonce)
597    +masked_tag = aes_hex_mask_bytes(tag)
598    +masked_ciphertext = aes_hex_mask_bytes(ciphertext)
599    encoded_fixed = "v1." ++
600        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
601        AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)) ++ "." ++
602        AES.hex_bytes(masked_ciphertext)
603    encoded_masked = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
604        AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(masked_ciphertext)
605    encoded_raw = "v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
606        "." ++ AES.hex_bytes(ciphertext)
607    cipher_equal = aes_hex_bytes_mask_idempotent(ciphertext)
608    tag_equal = aes_hex_bytes_mask_idempotent(tag)
609    nonce_equal = aes_hex_bytes_mask_idempotent(nonce)
610    cipher_path = Equal.cong(String, String,
611        last => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
612            AES.hex_bytes(masked_tag) ++ "." ++ last),
613        AES.hex_bytes(masked_ciphertext), AES.hex_bytes(ciphertext), cipher_equal)
614    tag_path = Equal.cong(String, String,
615        value => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++ value ++
616            "." ++ AES.hex_bytes(ciphertext)),
617        AES.hex_bytes(masked_tag), AES.hex_bytes(tag), tag_equal)
618    nonce_path = Equal.cong(String, String,
619        value => ("v1." ++ value ++ "." ++ AES.hex_bytes(tag) ++ "." ++
620            AES.hex_bytes(ciphertext)),
621        AES.hex_bytes(masked_nonce), AES.hex_bytes(nonce), nonce_equal)
622    cipher_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
623        AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(ciphertext)
624    tag_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
625        AES.hex_bytes(tag) ++ "." ++ AES.hex_bytes(ciphertext)
626    cipher_tag_path = Equal.trans(String, encoded_masked,
627        cipher_intermediate, tag_intermediate, cipher_path, tag_path)
628    encode_fields_equal = Equal.trans(String, encoded_masked,
629        tag_intermediate, encoded_raw, cipher_tag_path, nonce_path)
630    fixed_nonce_equal = Equal.cong(List<&2, U32>, String,
631        xs => AES.hex_bytes(xs),
632        AES.fixed_bytes(12n, masked_nonce), masked_nonce,
633        aes_fixed_bytes_identity(12n, masked_nonce, nonce_size))
634    fixed_tag_equal = Equal.cong(List<&2, U32>, String,
635        xs => AES.hex_bytes(xs),
636        AES.fixed_bytes(16n, masked_tag), masked_tag,
637        aes_fixed_bytes_identity(16n, masked_tag, tag_size))
638    fixed_tag_intermediate = "v1." ++
639        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
640        AES.hex_bytes(masked_tag) ++ "." ++
641        AES.hex_bytes(masked_ciphertext)
642    fixed_tag_path = Equal.cong(String, String,
643        value => "v1." ++
644            AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
645            value ++ "." ++ AES.hex_bytes(masked_ciphertext),
646        AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)),
647        AES.hex_bytes(masked_tag), fixed_tag_equal)
648    fixed_nonce_path = Equal.cong(String, String,
649        value => "v1." ++ value ++ "." ++ AES.hex_bytes(masked_tag) ++
650            "." ++ AES.hex_bytes(masked_ciphertext),
651        AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)),
652        AES.hex_bytes(masked_nonce), fixed_nonce_equal)
653    fixed_to_masked = Equal.trans(String, encoded_fixed,
654        fixed_tag_intermediate, encoded_masked,
655        fixed_tag_path, fixed_nonce_path)
656    fixed_to_raw = Equal.trans(String, encoded_fixed,
657        encoded_masked, encoded_raw,
658        fixed_to_masked, encode_fields_equal)
659    Equal.cong(String, Result<&2, &2, AES.Error, String>,
660        text => Done{text}, encoded_fixed, encoded_raw, fixed_to_raw)