AESMaskedXorProof.mask_bytes_identity: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as AESMaskedXorProof
Lines 180-201 of qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&start_line=180&end_line=201

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

def mask_bytes_identity(+bytes: List<&2, U32>,
    +valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) ->
    {Core.gcm_mask_bytes(bytes) == bytes : List<&2, U32>}:
    match bytes:
        case Nil{}: {==}
        case byte <> tail:
            head_valid = bool_and_true_left(U32.is_lt(byte, 256),
                Core.gcm_bytes_valid(tail), valid)
            tail_valid = bool_and_true_right(U32.is_lt(byte, 256),
                Core.gcm_bytes_valid(tail), valid)
            recursive = mask_bytes_identity(tail, tail_valid)
            Equal.trans(List<&2, U32>,
                Core.gcm_mask_bytes(byte <> tail),
                byte <> Core.gcm_mask_bytes(tail),
                byte <> tail,
                Equal.cong(U32, List<&2, U32>,
                    head => head <> Core.gcm_mask_bytes(tail),
                    Core.gcm_hex_mask(byte, 255), byte,
                    byte_mask_identity(byte, head_valid)),
                Equal.cong(List<&2, U32>, List<&2, U32>,
                    rest => byte <> rest,
                    Core.gcm_mask_bytes(tail), tail, recursive))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_bytes_valid
  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_MaskedXorProof.bend&name=bool_and_true_left
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=bool_and_true_right
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=byte_mask_identity