def aes_hex_bytes_split_before_period

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

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

377def aes_hex_bytes_split_before_period(+bytes: List<&2, U32>, +suffix: String) ->
378    {String.split(AES.hex_bytes(bytes) ++ "." ++ suffix, Chr{46}) ==
379     AES.hex_bytes(bytes) <> String.split(suffix, Chr{46}) : List<&2, String>}:
380    match bytes:
381        case Nil{}: {==}
382        case byte <> tail:
383            +normalized = AES.hex_mask(byte, 255)
384            +encoded_tail = AES.hex_bytes(tail)
385            +suffix_fields = String.split(suffix, Chr{46})
386            +tail_text = encoded_tail ++ "." ++ suffix
387            +high = U32.shrn(normalized, 4n)
388            +low = normalized
389            tail_proof = aes_hex_bytes_split_before_period(tail, suffix)
390            low_shift = Equal.cong(List<&2, String>, List<&2, String>,
391                parts => String.split.fin(AES.hex_digit(low), parts,
392                    Char.is_eq(AES.hex_digit(low), Chr{46})),
393                String.split(tail_text, Chr{46}), encoded_tail <> suffix_fields,
394                tail_proof)
395            low_join = Equal.trans(List<&2, String>,
396                String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
397                    Char.is_eq(AES.hex_digit(low), Chr{46})),
398                String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
399                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
400                Equal.trans(List<&2, String>,
401                    String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
402                        Char.is_eq(AES.hex_digit(low), Chr{46})),
403                    String.split.fin(AES.hex_digit(low), encoded_tail <> suffix_fields,
404                        Char.is_eq(AES.hex_digit(low), Chr{46})),
405                    String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
406                    low_shift, aes_split_hex_digit_no_dot(low,
407                        encoded_tail <> suffix_fields)),
408                aes_split_push_cons(low, encoded_tail, suffix_fields))
409            inner_split = Equal.trans(List<&2, String>,
410                String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
411                String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
412                    Char.is_eq(AES.hex_digit(low), Chr{46})),
413                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
414                {==}, low_join)
415            high_shift = Equal.cong(List<&2, String>, List<&2, String>,
416                parts => String.split.fin(AES.hex_digit(high), parts,
417                    Char.is_eq(AES.hex_digit(high), Chr{46})),
418                String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
419                SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
420                inner_split)
421            high_join = Equal.trans(List<&2, String>,
422                String.split.fin(AES.hex_digit(high),
423                    String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
424                    Char.is_eq(AES.hex_digit(high), Chr{46})),
425                String.split.push(AES.hex_digit(high),
426                    SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
427                SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
428                Equal.trans(List<&2, String>,
429                    String.split.fin(AES.hex_digit(high),
430                        String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
431                        Char.is_eq(AES.hex_digit(high), Chr{46})),
432                    String.split.fin(AES.hex_digit(high),
433                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
434                        Char.is_eq(AES.hex_digit(high), Chr{46})),
435                    String.split.push(AES.hex_digit(high),
436                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
437                    high_shift, aes_split_hex_digit_no_dot(high,
438                        SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields)),
439                aes_split_push_cons(high,
440                    SCon{AES.hex_digit(low), encoded_tail}, suffix_fields))
441            Equal.trans(List<&2, String>,
442                String.split(AES.hex_bytes(byte <> tail) ++ "." ++ suffix, Chr{46}),
443                String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
444                AES.hex_bytes(byte <> tail) <> suffix_fields,
445                {==}, Equal.trans(List<&2, String>,
446                    String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
447                    SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
448                    AES.hex_bytes(byte <> tail) <> suffix_fields,
449                    high_join, {==}))