def gcm_mask_xor_inv

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

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

74def gcm_mask_xor_inv(+x: U32, +y: U32) ->
75    {Core.gcm_hex_mask(
76        U32.xor(Core.gcm_hex_mask(U32.xor(x, y), 255), y), 255) ==
77     Core.gcm_hex_mask(x, 255) : U32}:
78    match x y:
79        case U32{xb} U32{yb}:
80            Equal.cong(Word(32n), U32, bits => U32{bits},
81                Word.and(32n, word_bits(255),
82                    Word.xor(32n,
83                        Word.and(32n, word_bits(255),
84                            Word.xor(32n, xb, yb)), yb)),
85                Word.and(32n, word_bits(255), xb),
86                word_mask_xor_inv(32n, word_bits(255), xb, yb))