def pk.xor_self

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:228

import Base

228def pk.xor_self(+a: U32) -> {U32.xor(a, a) == 0 : U32}:
229  match a:
230    case U32{x}:
231      %Equal.sym(Word(32n), Word.xor(32n, x, x), Word.zero(32n), pk.wself(32n, x)) : {U32{_} == 0 : U32}
232      {==}