AESEnvelopeProof.aes_hex_bytes_mask_idempotent: 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 189-211 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=189&end_line=211

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

def aes_hex_bytes_mask_idempotent(+bytes: List<&2, U32>) ->
    {AES.hex_bytes(aes_hex_mask_bytes(bytes)) == AES.hex_bytes(bytes) : String}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            +left_tail = AES.hex_bytes(aes_hex_mask_bytes(tail))
            +right_tail = AES.hex_bytes(tail)
            tail_equal = aes_hex_bytes_mask_idempotent(tail)
            prefix_equal = aes_hex_byte_prefix_idempotent(byte, left_tail)
            tail_congruent = Equal.cong(String, String,
                rest => SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), rest}},
                left_tail, right_tail, tail_equal)
            Equal.trans(String,
                SCon{AES.hex_digit(U32.shrn(
                    AES.hex_mask(AES.hex_mask(byte, 255), 255), 4n)),
                    SCon{AES.hex_digit(AES.hex_mask(
                        AES.hex_mask(byte, 255), 255)), left_tail}},
                SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), left_tail}},
                SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), right_tail}},
                prefix_equal, tail_congruent)

Uses (11):
  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=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_hex_byte_prefix_idempotent
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes