def gcm_mask_bytes_valid

qasim-bend-kit@0.1.0.2 · libs/AES256GCMCore.bend:264

import Base

264def gcm_mask_bytes_valid(+bytes: List<&2, U32>) ->
265    {gcm_bytes_valid(gcm_mask_bytes(bytes)) == True{} : Bool}:
266    match bytes:
267        case Nil{}: {==}
268        case byte <> tail:
269            Equal.trans(Bool,
270                gcm_bytes_valid(gcm_mask_bytes(byte <> tail)),
271                Bool.and(True{}, gcm_bytes_valid(gcm_mask_bytes(tail))),
272                True{},
273                Equal.cong(Bool, Bool,
274                    head => Bool.and(head,
275                        gcm_bytes_valid(gcm_mask_bytes(tail))),
276                    U32.is_lt(gcm_hex_mask(byte, 255), 256), True{},
277                    gcm_mask_byte_valid(byte)),
278                Equal.cong(Bool, Bool, tail_ok => Bool.and(True{}, tail_ok),
279                    gcm_bytes_valid(gcm_mask_bytes(tail)), True{},
280                    gcm_mask_bytes_valid(tail)))