def mask_bytes_identity

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:180

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

180def mask_bytes_identity(+bytes: List<&2, U32>,
181    +valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) ->
182    {Core.gcm_mask_bytes(bytes) == bytes : List<&2, U32>}:
183    match bytes:
184        case Nil{}: {==}
185        case byte <> tail:
186            head_valid = bool_and_true_left(U32.is_lt(byte, 256),
187                Core.gcm_bytes_valid(tail), valid)
188            tail_valid = bool_and_true_right(U32.is_lt(byte, 256),
189                Core.gcm_bytes_valid(tail), valid)
190            recursive = mask_bytes_identity(tail, tail_valid)
191            Equal.trans(List<&2, U32>,
192                Core.gcm_mask_bytes(byte <> tail),
193                byte <> Core.gcm_mask_bytes(tail),
194                byte <> tail,
195                Equal.cong(U32, List<&2, U32>,
196                    head => head <> Core.gcm_mask_bytes(tail),
197                    Core.gcm_hex_mask(byte, 255), byte,
198                    byte_mask_identity(byte, head_valid)),
199                Equal.cong(List<&2, U32>, List<&2, U32>,
200                    rest => byte <> rest,
201                    Core.gcm_mask_bytes(tail), tail, recursive))