AES256GCMCore.gcm_mask_bytes_valid: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as AES256GCMCore
Lines 264-280 of qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&start_line=264&end_line=280

import Base

def gcm_mask_bytes_valid(+bytes: List<&2, U32>) ->
    {gcm_bytes_valid(gcm_mask_bytes(bytes)) == True{} : Bool}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            Equal.trans(Bool,
                gcm_bytes_valid(gcm_mask_bytes(byte <> tail)),
                Bool.and(True{}, gcm_bytes_valid(gcm_mask_bytes(tail))),
                True{},
                Equal.cong(Bool, Bool,
                    head => Bool.and(head,
                        gcm_bytes_valid(gcm_mask_bytes(tail))),
                    U32.is_lt(gcm_hex_mask(byte, 255), 256), True{},
                    gcm_mask_byte_valid(byte)),
                Equal.cong(Bool, Bool, tail_ok => Bool.and(True{}, tail_ok),
                    gcm_bytes_valid(gcm_mask_bytes(tail)), True{},
                    gcm_mask_bytes_valid(tail)))

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/AES256GCMCore.bend&name=gcm_bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_mask_byte_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_mask_bytes