AESEnvelopeProof.aes_hex_byte_prefix_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 150-182 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=150&end_line=182

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

def aes_hex_byte_prefix_idempotent(+byte: U32, +tail: 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)), tail}} ==
     SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
       SCon{AES.hex_digit(AES.hex_mask(byte, 255)), tail}} : String}:
    +normalized = AES.hex_mask(byte, 255)
    +twice = AES.hex_mask(normalized, 255)
    +mask_equal = aes_hex_mask_idempotent(byte, 255)
    low_equal = Equal.cong(U32, Char, value => AES.hex_digit(value),
        twice, normalized,
        mask_equal)
    high_equal = Equal.cong(U32, Char,
        value => AES.hex_digit(U32.shrn(value, 4n)), twice, normalized,
        mask_equal)
    inner_equal = Equal.cong(Char, String,
        value => SCon{value, tail}, AES.hex_digit(twice),
        AES.hex_digit(normalized), low_equal)
    inner_path = Equal.cong(String, String,
        rest => SCon{AES.hex_digit(U32.shrn(twice, 4n)), rest},
        SCon{AES.hex_digit(twice), tail},
        SCon{AES.hex_digit(normalized), tail}, inner_equal)
    high_path = Equal.cong(Char, String,
        value => SCon{value, SCon{AES.hex_digit(normalized), tail}},
        AES.hex_digit(U32.shrn(twice, 4n)),
        AES.hex_digit(U32.shrn(normalized, 4n)), high_equal)
    Equal.trans(String,
        SCon{AES.hex_digit(U32.shrn(twice, 4n)),
            SCon{AES.hex_digit(twice), tail}},
        SCon{AES.hex_digit(U32.shrn(twice, 4n)),
            SCon{AES.hex_digit(normalized), tail}},
        SCon{AES.hex_digit(U32.shrn(normalized, 4n)),
            SCon{AES.hex_digit(normalized), tail}},
        inner_path, high_path)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  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=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_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_mask_idempotent