AESMaskedXorProof.gcm_mask_xor_inv: 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 74-86 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=74&end_line=86

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

def gcm_mask_xor_inv(+x: U32, +y: U32) ->
    {Core.gcm_hex_mask(
        U32.xor(Core.gcm_hex_mask(U32.xor(x, y), 255), y), 255) ==
     Core.gcm_hex_mask(x, 255) : U32}:
    match x y:
        case U32{xb} U32{yb}:
            Equal.cong(Word(32n), U32, bits => U32{bits},
                Word.and(32n, word_bits(255),
                    Word.xor(32n,
                        Word.and(32n, word_bits(255),
                            Word.xor(32n, xb, yb)), yb)),
                Word.and(32n, word_bits(255), xb),
                word_mask_xor_inv(32n, word_bits(255), xb, yb))

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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.xor
  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/proof/AES_MaskedXorProof.bend&name=word_bits
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=word_mask_xor_inv