AESEnvelopeProof.aes_decode_hex_bytes: 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 261-294 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=261&end_line=294

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

def aes_decode_hex_bytes(+bytes: List<&2, U32>) ->
    {AES.decode_hex(AES.hex_bytes(bytes)) == Some{aes_hex_mask_bytes(bytes)} : Maybe<&2, List<&2, U32>>}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            +normalized = AES.hex_mask(byte, 255)
            +rest_pairs = AES.hex_pairs(String.to_list(AES.hex_bytes(tail)))
            +rest_decoded = AES.collect_hex(rest_pairs)
            tail_proof = aes_decode_hex_bytes(tail)
            pair_proof = aes_hex_pair_roundtrip(byte)
            pair_changed = Equal.cong(Maybe<&2, U32>,
                Maybe<&2, List<&2, U32>>,
                pair => AES.collect_hex.cons(pair, rest_decoded),
                AES.hex_pair(
                    AES.hex_digit(U32.shrn(normalized, 4n)),
                    AES.hex_digit(normalized)),
                Some{normalized}, pair_proof)
            tail_changed = Equal.cong(Maybe<&2, List<&2, U32>>,
                Maybe<&2, List<&2, U32>>,
                result => AES.collect_hex.cons(Some{normalized}, result),
                rest_decoded, Some{aes_hex_mask_bytes(tail)}, tail_proof)
            Equal.trans(Maybe<&2, List<&2, U32>>,
                AES.collect_hex.cons(
                    AES.hex_pair(
                        AES.hex_digit(U32.shrn(normalized, 4n)),
                        AES.hex_digit(normalized)), rest_decoded),
                AES.collect_hex.cons(Some{normalized}, rest_decoded),
                Some{normalized <> aes_hex_mask_bytes(tail)},
                pair_changed,
                Equal.trans(Maybe<&2, List<&2, U32>>,
                    AES.collect_hex.cons(Some{normalized}, rest_decoded),
                    Some{normalized <> aes_hex_mask_bytes(tail)},
                    Some{normalized <> aes_hex_mask_bytes(tail)},
                    tail_changed, {==}))

Uses (17):
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.to_list
  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=collect_hex
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=collect_hex.cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=decode_hex
  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/libs/AES256GCM.bend&name=hex_pair
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_pairs
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_pair_roundtrip