def u32_xx

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

import Base

51def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}:
52  match a b:
53    case U32{x} U32{y}:
54      %word_xx(32n, x, y) : {U32{x} == U32{_} : U32}
55      {==}