def gcm_zip_xor_valid

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

import Base

538def gcm_zip_xor_valid(+bytes: List<&2, U32>, +stream: List<&2, U32>) ->
539    {gcm_bytes_valid(gcm_zip_xor(bytes, stream)) == True{} : Bool}:
540    match bytes stream:
541        case Nil{} _:
542            Equal.trans(Bool,
543                gcm_bytes_valid(gcm_zip_xor(Nil{}, stream)),
544                gcm_bytes_valid(Nil{}), True{},
545                Equal.cong(List<&2, U32>, Bool, gcm_bytes_valid,
546                    gcm_zip_xor(Nil{}, stream), Nil{},
547                    gcm_zip_xor_nil_left(stream)),
548                {==})
549        case _ Nil{}:
550            Equal.trans(Bool,
551                gcm_bytes_valid(gcm_zip_xor(bytes, Nil{})),
552                gcm_bytes_valid(Nil{}), True{},
553                Equal.cong(List<&2, U32>, Bool, gcm_bytes_valid,
554                    gcm_zip_xor(bytes, Nil{}), Nil{},
555                    gcm_zip_xor_nil_right(bytes)),
556                {==})
557        case byte <> tail stream_byte <> stream_tail:
558            recursive = gcm_zip_xor_valid(tail, stream_tail)
559            range = gcm_mask_byte_valid(U32.xor(byte, stream_byte))
560            head_changed = Equal.cong(Bool, Bool,
561                head => Bool.and(head,
562                    gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
563                U32.is_lt(gcm_hex_mask(U32.xor(byte, stream_byte), 255), 256),
564                True{}, range)
565            tail_changed = Equal.cong(Bool, Bool,
566                valid => Bool.and(True{}, valid),
567                gcm_bytes_valid(gcm_zip_xor(tail, stream_tail)), True{},
568                recursive)
569            Equal.trans(Bool,
570                Bool.and(
571                    U32.is_lt(gcm_hex_mask(U32.xor(byte, stream_byte), 255), 256),
572                    gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
573                Bool.and(True{}, gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
574                True{}, head_changed,
575                Equal.trans(Bool,
576                    Bool.and(True{}, gcm_bytes_valid(gcm_zip_xor(tail, stream_tail))),
577                    Bool.and(True{}, True{}), True{}, tail_changed, {==}))