def core_bytes_valid_eq

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:12

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

12def core_bytes_valid_eq(+bytes: List<&2, U32>) ->
13    {bytes_valid(bytes) == Core.gcm_bytes_valid(bytes) : Bool}:
14    match bytes:
15        case Nil{}: {==}
16        case head <> tail:
17            recursive = core_bytes_valid_eq(tail)
18            Equal.cong(Bool, Bool,
19                valid => Bool.and(U32.is_lt(head, 256), valid),
20                bytes_valid(tail), Core.gcm_bytes_valid(tail), recursive)