def bits.xor_self

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

1607def bits.xor_self(a: U32) -> {B.byte(U32.xor(a, a)) == 0 : U32}:
1608  match a:
1609    case U32{x}:
1610      %Equal.sym(Word(32n), Word.xor(32n, x, x), Word.zero(32n), bx.wself(32n, x)) : {B.byte(U32{_}) == 0 : U32}
1611      {==}