def aes_parse_decoded_checked_map
qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:873
import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
873def aes_parse_decoded_checked_map(+nonce: List<&2, U32>,
874 +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
875 nonce_size: {List.length(&2, U32, nonce) == 12n : Nat},
876 tag_size: {List.length(&2, U32, tag) == 16n : Nat}) ->
877 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
878 AES.parse_decoded(aes_hex_mask_bytes(nonce),
879 aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext),
880 AES.aes_nat_eq_proof(
881 List.length(&2, U32, aes_hex_mask_bytes(nonce)), 12n),
882 AES.aes_nat_eq_proof(
883 List.length(&2, U32, aes_hex_mask_bytes(tag)), 16n),
884 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(nonce)),
885 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(tag)),
886 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(ciphertext)))) ==
887 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
888 "." ++ AES.hex_bytes(ciphertext)} :
889 Result<&2, &2, AES.Error, String>}:
890 aes_parse_decoded_if_some(nonce, tag, ciphertext,
891 AES.aes_nat_eq_proof(
892 List.length(&2, U32, aes_hex_mask_bytes(nonce)), 12n),
893 AES.aes_nat_eq_proof(
894 List.length(&2, U32, aes_hex_mask_bytes(tag)), 16n),
895 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(nonce)),
896 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(tag)),
897 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(ciphertext)),
898 aes_masked_size_is_some(nonce, 12n, nonce_size),
899 aes_masked_size_is_some(tag, 16n, tag_size),
900 aes_masked_bytes_cert_is_some(nonce),
901 aes_masked_bytes_cert_is_some(tag),
902 aes_masked_bytes_cert_is_some(ciphertext))