def aes_split_v1_hex_fields

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

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

470def aes_split_v1_hex_fields(+nonce: List<&2, U32>, +tag: List<&2, U32>,
471    +ciphertext: List<&2, U32>) ->
472    {String.split("v1." ++ AES.hex_bytes(nonce) ++ "." ++
473        AES.hex_bytes(tag) ++ "." ++ AES.hex_bytes(ciphertext), Chr{46}) ==
474     ["v1", AES.hex_bytes(nonce), AES.hex_bytes(tag), AES.hex_bytes(ciphertext)] : List<&2, String>}:
475    +nonce_hex = AES.hex_bytes(nonce)
476    +tag_hex = AES.hex_bytes(tag)
477    +cipher_hex = AES.hex_bytes(ciphertext)
478    +tag_suffix = tag_hex ++ "." ++ cipher_hex
479    +nonce_suffix = nonce_hex ++ "." ++ tag_suffix
480    cipher_split = aes_hex_bytes_split_single(ciphertext)
481    tag_split = aes_hex_bytes_split_before_period(tag, cipher_hex)
482    nonce_split = aes_hex_bytes_split_before_period(nonce, tag_suffix)
483    tag_final = Equal.cong(List<&2, String>, List<&2, String>,
484        fields => tag_hex <> fields,
485        String.split(cipher_hex, Chr{46}), [cipher_hex], cipher_split)
486    tag_complete = Equal.trans(List<&2, String>,
487        String.split(tag_suffix, Chr{46}),
488        tag_hex <> String.split(cipher_hex, Chr{46}),
489        tag_hex <> [cipher_hex], tag_split, tag_final)
490    nonce_final = Equal.cong(List<&2, String>, List<&2, String>,
491        fields => nonce_hex <> fields,
492        String.split(tag_suffix, Chr{46}), tag_hex <> [cipher_hex], tag_complete)
493    rest_fields = Equal.cong(List<&2, String>, List<&2, String>,
494        fields => "v1" <> fields,
495        String.split(nonce_suffix, Chr{46}), nonce_hex <> (tag_hex <> [cipher_hex]),
496        Equal.trans(List<&2, String>,
497            String.split(nonce_suffix, Chr{46}),
498            nonce_hex <> String.split(tag_suffix, Chr{46}),
499            nonce_hex <> (tag_hex <> [cipher_hex]),
500            nonce_split, nonce_final))
501    Equal.trans(List<&2, String>,
502        String.split("v1." ++ nonce_suffix, Chr{46}),
503        "v1" <> String.split(nonce_suffix, Chr{46}),
504        ["v1", nonce_hex, tag_hex, cipher_hex],
505        aes_split_v1_prefix(nonce_suffix),
506        Equal.trans(List<&2, String>,
507            "v1" <> String.split(nonce_suffix, Chr{46}),
508            "v1" <> (nonce_hex <> (tag_hex <> [cipher_hex])),
509            ["v1", nonce_hex, tag_hex, cipher_hex],
510            rest_fields, {==}))