AESIdentityProof.mask_same: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend as AESIdentityProof
Lines 15-25 of qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&start_line=15&end_line=25

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

def mask_same(+bytes: List<&2, U32>) ->
    {Encoding.aes_hex_mask_bytes(bytes) == Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            Equal.trans(List<&2, U32>, Encoding.aes_hex_mask_bytes(byte <> tail),
                Core.gcm_hex_mask(byte, 255) <> Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(byte <> tail),
                Equal.cong(U32, List<&2, U32>, value => value <> Encoding.aes_hex_mask_bytes(tail),
                    AES.hex_mask(byte, 255), Core.gcm_hex_mask(byte, 255), mask_word_same(byte)),
                Equal.cong(List<&2, U32>, List<&2, U32>, xs => Core.gcm_hex_mask(byte, 255) <> xs,
                    Encoding.aes_hex_mask_bytes(tail), Core.gcm_mask_bytes(tail), mask_same(tail)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_hex_mask_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&name=mask_word_same