def bx.u32

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

import Base

54def bx.u32(a: U32, b: U32) -> {U32.xor(a, U32.xor(a, b)) == b : U32}:
55  match a b:
56    case U32{x} U32{y}:
57      %bx.word(32n, x, y) : {U32{Word.xor(32n, x, Word.xor(32n, x, y))} == U32{_} : U32}
58      {==}