def aes_hex_bytes_split_single

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

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

300def aes_hex_bytes_split_single(+bytes: List<&2, U32>) ->
301    {String.split(AES.hex_bytes(bytes), Chr{46}) == [AES.hex_bytes(bytes)] : List<&2, String>}:
302    match bytes:
303        case Nil{}: {==}
304        case byte <> tail:
305            +normalized = AES.hex_mask(byte, 255)
306            +encoded_tail = AES.hex_bytes(tail)
307            +high = U32.shrn(normalized, 4n)
308            +low = normalized
309            tail_proof = aes_hex_bytes_split_single(tail)
310            low_shift = Equal.cong(List<&2, String>, List<&2, String>,
311                parts => String.split.fin(AES.hex_digit(low), parts,
312                    Char.is_eq(AES.hex_digit(low), Chr{46})),
313                String.split(encoded_tail, Chr{46}), [encoded_tail], tail_proof)
314            low_join = Equal.trans(List<&2, String>,
315                String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
316                    Char.is_eq(AES.hex_digit(low), Chr{46})),
317                String.split.push(AES.hex_digit(low), [encoded_tail]),
318                [SCon{AES.hex_digit(low), encoded_tail}],
319                Equal.trans(List<&2, String>,
320                    String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
321                        Char.is_eq(AES.hex_digit(low), Chr{46})),
322                    String.split.fin(AES.hex_digit(low), [encoded_tail],
323                        Char.is_eq(AES.hex_digit(low), Chr{46})),
324                    String.split.push(AES.hex_digit(low), [encoded_tail]),
325                    low_shift, aes_split_hex_digit_no_dot(low, [encoded_tail])),
326                aes_split_push_single(low, encoded_tail))
327            inner_split = Equal.trans(List<&2, String>,
328                String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
329                String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
330                    Char.is_eq(AES.hex_digit(low), Chr{46})),
331                [SCon{AES.hex_digit(low), encoded_tail}],
332                {==}, low_join)
333            high_shift = Equal.cong(List<&2, String>, List<&2, String>,
334                parts => String.split.fin(AES.hex_digit(high), parts,
335                    Char.is_eq(AES.hex_digit(high), Chr{46})),
336                String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
337                [SCon{AES.hex_digit(low), encoded_tail}], inner_split)
338            high_join = Equal.trans(List<&2, String>,
339                String.split.fin(AES.hex_digit(high),
340                    String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
341                    Char.is_eq(AES.hex_digit(high), Chr{46})),
342                String.split.push(AES.hex_digit(high),
343                    [SCon{AES.hex_digit(low), encoded_tail}]),
344                [SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}}],
345                Equal.trans(List<&2, String>,
346                    String.split.fin(AES.hex_digit(high),
347                        String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
348                        Char.is_eq(AES.hex_digit(high), Chr{46})),
349                    String.split.fin(AES.hex_digit(high),
350                        [SCon{AES.hex_digit(low), encoded_tail}],
351                        Char.is_eq(AES.hex_digit(high), Chr{46})),
352                    String.split.push(AES.hex_digit(high),
353                        [SCon{AES.hex_digit(low), encoded_tail}]),
354                    high_shift, aes_split_hex_digit_no_dot(high,
355                        [SCon{AES.hex_digit(low), encoded_tail}])),
356                aes_split_push_single(high,
357                    SCon{AES.hex_digit(low), encoded_tail}))
358            Equal.trans(List<&2, String>,
359                String.split(AES.hex_bytes(byte <> tail), Chr{46}),
360                String.split(SCon{AES.hex_digit(high),
361                    SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
362                [AES.hex_bytes(byte <> tail)],
363                {==},
364                Equal.trans(List<&2, String>,
365                    String.split(SCon{AES.hex_digit(high),
366                        SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
367                    [SCon{AES.hex_digit(high),
368                        SCon{AES.hex_digit(low), encoded_tail}}],
369                    [AES.hex_bytes(byte <> tail)], high_join,
370                    {==}))