def mask_same

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

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

15def mask_same(+bytes: List<&2, U32>) ->
16    {Encoding.aes_hex_mask_bytes(bytes) == Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
17    match bytes:
18        case Nil{}: {==}
19        case byte <> tail:
20            Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(byte <> tail),
21                Core.gcm_hex_mask(byte, 255) <> Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(byte <> tail),
22                Equal.cong(U32, List<&2, U32>, value => value <> Encoding.aes_hex_mask_bytes(tail),
23                    AES.hex_mask(byte, 255), Core.gcm_hex_mask(byte, 255), mask_word_same(byte)),
24                Equal.cong(List<&2, U32>, List<&2, U32>, xs => Core.gcm_hex_mask(byte, 255) <> xs,
25                    Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(tail), mask_same(tail)))