def aes_hex_bytes_mask_idempotent

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

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

189def aes_hex_bytes_mask_idempotent(+bytes: List<&2, U32>) ->
190    {AES.hex_bytes(aes_hex_mask_bytes(bytes)) == AES.hex_bytes(bytes) : String}:
191    match bytes:
192        case Nil{}: {==}
193        case byte <> tail:
194            +left_tail = AES.hex_bytes(aes_hex_mask_bytes(tail))
195            +right_tail = AES.hex_bytes(tail)
196            tail_equal = aes_hex_bytes_mask_idempotent(tail)
197            prefix_equal = aes_hex_byte_prefix_idempotent(byte, left_tail)
198            tail_congruent = Equal.cong(String, String,
199                rest => SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
200                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), rest}},
201                left_tail, right_tail, tail_equal)
202            Equal.trans(String,
203                SCon{AES.hex_digit(U32.shrn(
204                    AES.hex_mask(AES.hex_mask(byte, 255), 255), 4n)),
205                    SCon{AES.hex_digit(AES.hex_mask(
206                        AES.hex_mask(byte, 255), 255)), left_tail}},
207                SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
208                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), left_tail}},
209                SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
210                    SCon{AES.hex_digit(AES.hex_mask(byte, 255)), right_tail}},
211                prefix_equal, tail_congruent)