AESEnvelopeProof.aes_hex_bytes_split_before_period: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 377-449 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=377&end_line=449

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

def aes_hex_bytes_split_before_period(+bytes: List<&2, U32>, +suffix: String) ->
    {String.split(AES.hex_bytes(bytes) ++ "." ++ suffix, Chr{46}) ==
     AES.hex_bytes(bytes) <> String.split(suffix, Chr{46}) : List<&2, String>}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            +normalized = AES.hex_mask(byte, 255)
            +encoded_tail = AES.hex_bytes(tail)
            +suffix_fields = String.split(suffix, Chr{46})
            +tail_text = encoded_tail ++ "." ++ suffix
            +high = U32.shrn(normalized, 4n)
            +low = normalized
            tail_proof = aes_hex_bytes_split_before_period(tail, suffix)
            low_shift = Equal.cong(List<&2, String>, List<&2, String>,
                parts => String.split.fin(AES.hex_digit(low), parts,
                    Char.is_eq(AES.hex_digit(low), Chr{46})),
                String.split(tail_text, Chr{46}), encoded_tail <> suffix_fields,
                tail_proof)
            low_join = Equal.trans(List<&2, String>,
                String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
                    Char.is_eq(AES.hex_digit(low), Chr{46})),
                String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
                Equal.trans(List<&2, String>,
                    String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
                        Char.is_eq(AES.hex_digit(low), Chr{46})),
                    String.split.fin(AES.hex_digit(low), encoded_tail <> suffix_fields,
                        Char.is_eq(AES.hex_digit(low), Chr{46})),
                    String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
                    low_shift, aes_split_hex_digit_no_dot(low,
                        encoded_tail <> suffix_fields)),
                aes_split_push_cons(low, encoded_tail, suffix_fields))
            inner_split = Equal.trans(List<&2, String>,
                String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
                String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
                    Char.is_eq(AES.hex_digit(low), Chr{46})),
                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
                {==}, low_join)
            high_shift = Equal.cong(List<&2, String>, List<&2, String>,
                parts => String.split.fin(AES.hex_digit(high), parts,
                    Char.is_eq(AES.hex_digit(high), Chr{46})),
                String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
                inner_split)
            high_join = Equal.trans(List<&2, String>,
                String.split.fin(AES.hex_digit(high),
                    String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
                    Char.is_eq(AES.hex_digit(high), Chr{46})),
                String.split.push(AES.hex_digit(high),
                    SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
                SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
                Equal.trans(List<&2, String>,
                    String.split.fin(AES.hex_digit(high),
                        String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
                        Char.is_eq(AES.hex_digit(high), Chr{46})),
                    String.split.fin(AES.hex_digit(high),
                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
                        Char.is_eq(AES.hex_digit(high), Chr{46})),
                    String.split.push(AES.hex_digit(high),
                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
                    high_shift, aes_split_hex_digit_no_dot(high,
                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields)),
                aes_split_push_cons(high,
                    SCon{AES.hex_digit(low), encoded_tail}, suffix_fields))
            Equal.trans(List<&2, String>,
                String.split(AES.hex_bytes(byte <> tail) ++ "." ++ suffix, Chr{46}),
                String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
                AES.hex_bytes(byte <> tail) <> suffix_fields,
                {==}, Equal.trans(List<&2, String>,
                    String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
                    SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
                    AES.hex_bytes(byte <> tail) <> suffix_fields,
                    high_join, {==}))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.split
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.split.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.split.push
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_digit
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_split_hex_digit_no_dot
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_split_push_cons