AESEnvelopeProof.aes_hex_bytes_split_single: 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 300-370 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=300&end_line=370

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

def aes_hex_bytes_split_single(+bytes: List<&2, U32>) ->
    {String.split(AES.hex_bytes(bytes), Chr{46}) == [AES.hex_bytes(bytes)] : List<&2, String>}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            +normalized = AES.hex_mask(byte, 255)
            +encoded_tail = AES.hex_bytes(tail)
            +high = U32.shrn(normalized, 4n)
            +low = normalized
            tail_proof = aes_hex_bytes_split_single(tail)
            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(encoded_tail, Chr{46}), [encoded_tail], tail_proof)
            low_join = Equal.trans(List<&2, String>,
                String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
                    Char.is_eq(AES.hex_digit(low), Chr{46})),
                String.split.push(AES.hex_digit(low), [encoded_tail]),
                [SCon{AES.hex_digit(low), encoded_tail}],
                Equal.trans(List<&2, String>,
                    String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
                        Char.is_eq(AES.hex_digit(low), Chr{46})),
                    String.split.fin(AES.hex_digit(low), [encoded_tail],
                        Char.is_eq(AES.hex_digit(low), Chr{46})),
                    String.split.push(AES.hex_digit(low), [encoded_tail]),
                    low_shift, aes_split_hex_digit_no_dot(low, [encoded_tail])),
                aes_split_push_single(low, encoded_tail))
            inner_split = Equal.trans(List<&2, String>,
                String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
                String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
                    Char.is_eq(AES.hex_digit(low), Chr{46})),
                [SCon{AES.hex_digit(low), encoded_tail}],
                {==}, 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), encoded_tail}, Chr{46}),
                [SCon{AES.hex_digit(low), encoded_tail}], inner_split)
            high_join = Equal.trans(List<&2, String>,
                String.split.fin(AES.hex_digit(high),
                    String.split(SCon{AES.hex_digit(low), encoded_tail}, 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}]),
                [SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}}],
                Equal.trans(List<&2, String>,
                    String.split.fin(AES.hex_digit(high),
                        String.split(SCon{AES.hex_digit(low), encoded_tail}, 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}],
                        Char.is_eq(AES.hex_digit(high), Chr{46})),
                    String.split.push(AES.hex_digit(high),
                        [SCon{AES.hex_digit(low), encoded_tail}]),
                    high_shift, aes_split_hex_digit_no_dot(high,
                        [SCon{AES.hex_digit(low), encoded_tail}])),
                aes_split_push_single(high,
                    SCon{AES.hex_digit(low), encoded_tail}))
            Equal.trans(List<&2, String>,
                String.split(AES.hex_bytes(byte <> tail), Chr{46}),
                String.split(SCon{AES.hex_digit(high),
                    SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
                [AES.hex_bytes(byte <> tail)],
                {==},
                Equal.trans(List<&2, String>,
                    String.split(SCon{AES.hex_digit(high),
                        SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
                    [SCon{AES.hex_digit(high),
                        SCon{AES.hex_digit(low), encoded_tail}}],
                    [AES.hex_bytes(byte <> tail)], high_join,
                    {==}))

Uses (16):
  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.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_single