AESMaskedXorProof.bool_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 8-20 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=8&end_line=20

import Base

def bool_mask_xor_inv(+mask: Bool, +x: Bool, +y: Bool) ->
    {Bool.and(mask,
        Bool.xor(Bool.and(mask, Bool.xor(x, y)), y)) ==
     Bool.and(mask, x) : Bool}:
    match mask x y:
        case False{} False{} False{}: {==}
        case False{} False{} True{}: {==}
        case False{} True{} False{}: {==}
        case False{} True{} True{}: {==}
        case True{} False{} False{}: {==}
        case True{} False{} True{}: {==}
        case True{} True{} False{}: {==}
        case True{} True{} True{}: {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.xor