def b64_xx2

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8594

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L

8594def b64_xx2(a: L.LcBlock64, b: L.LcBlock64) -> {b == L.LcBlock64.xor(a, L.LcBlock64.xor(a, b)) : L.LcBlock64}:
8595  match a b:
8596    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}:
8597      %u32_xx2(a0, b0) : {L.LcBlock64{b0, b1} == L.LcBlock64{_, U32.xor(a1, U32.xor(a1, b1))} : L.LcBlock64}
8598      %u32_xx2(a1, b1) : {L.LcBlock64{b0, b1} == L.LcBlock64{b0, _} : L.LcBlock64}
8599      {==}