def bool_mask_xor_inv

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:8

import Base

8def bool_mask_xor_inv(+mask: Bool, +x: Bool, +y: Bool) ->
9    {Bool.and(mask,
10        Bool.xor(Bool.and(mask, Bool.xor(x, y)), y)) ==
11     Bool.and(mask, x) : Bool}:
12    match mask x y:
13        case False{} False{} False{}: {==}
14        case False{} False{} True{}: {==}
15        case False{} True{} False{}: {==}
16        case False{} True{} True{}: {==}
17        case True{} False{} False{}: {==}
18        case True{} False{} True{}: {==}
19        case True{} True{} False{}: {==}
20        case True{} True{} True{}: {==}