def bx.ru32

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1355

import Base

1355def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}:
1356  match a b:
1357    case U32{x} U32{y}:
1358      %bx.rword(32n, x, y) : {U32{Word.xor(32n, Word.xor(32n, x, y), y)} == U32{_} : U32}
1359      {==}