def u32_xx2

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8588

import Base

8588def u32_xx2(a: U32, b: U32) -> {b == U32.xor(a, U32.xor(a, b)) : U32}:
8589  match a b:
8590    case U32{x} U32{y}:
8591      %word_xx2(32n, x, y) : {U32{y} == U32{_} : U32}
8592      {==}