def bx.ru32

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:683

import Base

683def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}:
684  match a b:
685    case U32{x} U32{y}:
686      %bx.rword(32n, x, y) : {U32{Word.xor(32n, Word.xor(32n, x, y), y)} == U32{_} : U32}
687      {==}