def xor_inv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:39

import Base

39def xor_inv(+x: U32, +k: U32) -> {U32.xor(U32.xor(x, k), k) == x : U32}:
40  match x k:
41    case U32{a} U32{b}:
42      Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, Word.xor(32n, a, b), b), a, word_xor_inv(32n, a, b))