def aes_hex_mask_bytes_valid

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:673

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

673def aes_hex_mask_bytes_valid(+bytes: List<&2, U32>) ->
674    {AES.bytes_valid(aes_hex_mask_bytes(bytes)) == True{} : Bool}:
675    match bytes:
676        case Nil{}: {==}
677        case byte <> tail:
678            recursive = aes_hex_mask_bytes_valid(tail)
679            range = aes_hex_mask_255_lt_256(byte)
680            head_changed = Equal.cong(Bool, Bool,
681                head => Bool.and(head, AES.bytes_valid(aes_hex_mask_bytes(tail))),
682                U32.is_lt(AES.hex_mask(byte, 255), 256), True{}, range)
683            tail_changed = Equal.cong(Bool, Bool,
684                valid => Bool.and(True{}, valid),
685                AES.bytes_valid(aes_hex_mask_bytes(tail)), True{}, recursive)
686            Equal.trans(Bool,
687                Bool.and(U32.is_lt(AES.hex_mask(byte, 255), 256),
688                    AES.bytes_valid(aes_hex_mask_bytes(tail))),
689                Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
690                True{}, head_changed,
691                Equal.trans(Bool,
692                    Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
693                    Bool.and(True{}, True{}), True{}, tail_changed, {==}))