law xor_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/subtle/word.bend:164

import Base

164# zero(x ^ y) == (x == y)
165law xor_zero:
166  for +n: Nat
167  for +x: Word(n)
168  for +y: Word(n)
169  {Cmp.is_eq(Word.cmp(n, Word.xor(n, x, y), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, x, y)) : Bool}