law word_xor_cancel

bend-osdev-cipher-core@0.1.0.0 · LAWS.bend:31

import Base

31# XOR undone, for every word of any width, every 32-bit word and every
32# 64-bit block
33law word_xor_cancel:
34  for n: Nat
35  for a: Word(n)
36  for b: Word(n)
37  {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}