PROOF.b64_xx2: def of bend-osdev-cipher-core@0.1.0.0
Import: import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as PROOF
Lines 248-253 of bend-osdev-cipher-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&start_line=248&end_line=253

import Base
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L

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

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=u32_xx2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.xor