def mask_identity

qasim-bend-kit@0.1.0.2 · proof/AES_IdentityProof.bend:27

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as Encoding
import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as Masked

27def mask_identity(+bytes: List<&2, U32>, valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
28    {Encoding.aes_hex_mask_bytes(bytes) == bytes : List<&2, U32>}:
29    core_valid = Equal.trans(Bool, Core.gcm_bytes_valid(bytes), AES.bytes_valid(bytes), True{},
30        Equal.sym(Bool, AES.bytes_valid(bytes), Core.gcm_bytes_valid(bytes), AES.core_bytes_valid_eq(bytes)), valid)
31    Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(bytes), Core.gcm_mask_bytes(bytes), bytes,
32        mask_same(bytes), Masked.mask_bytes_identity(bytes, core_valid))