AESEnvelopeProof.aes_hex_mask_bytes_valid: 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 673-693 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=673&end_line=693

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

def aes_hex_mask_bytes_valid(+bytes: List<&2, U32>) ->
    {AES.bytes_valid(aes_hex_mask_bytes(bytes)) == True{} : Bool}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            recursive = aes_hex_mask_bytes_valid(tail)
            range = aes_hex_mask_255_lt_256(byte)
            head_changed = Equal.cong(Bool, Bool,
                head => Bool.and(head, AES.bytes_valid(aes_hex_mask_bytes(tail))),
                U32.is_lt(AES.hex_mask(byte, 255), 256), True{}, range)
            tail_changed = Equal.cong(Bool, Bool,
                valid => Bool.and(True{}, valid),
                AES.bytes_valid(aes_hex_mask_bytes(tail)), True{}, recursive)
            Equal.trans(Bool,
                Bool.and(U32.is_lt(AES.hex_mask(byte, 255), 256),
                    AES.bytes_valid(aes_hex_mask_bytes(tail))),
                Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
                True{}, head_changed,
                Equal.trans(Bool,
                    Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
                    Bool.and(True{}, True{}), True{}, tail_changed, {==}))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  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_255_lt_256
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes